%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : LAT387+4 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.MKNUGu2rdX true
% Computer : n010.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:41:49 PM UTC 2025
% Result : Theorem 6.45s 1.47s
% Output : Refutation 6.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.10 % Problem : LAT387+4 : TPTP v9.2.0. Released v4.0.0.
% 0.05/0.11 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.MKNUGu2rdX true
% 0.10/0.31 % Computer : n010.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Wed Oct 1 14:37:08 EDT 2025
% 0.10/0.31 % CPUTime :
% 0.10/0.31 % Running portfolio for 300 s
% 0.10/0.31 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.31 % Number of cores: 8
% 0.15/0.31 % Python version: Python 3.6.8
% 0.15/0.31 % Running in FO mode
% 0.45/0.58 % Total configuration time : 435
% 0.45/0.58 % Estimated wc time : 1092
% 0.45/0.58 % Estimated cpu time (7 cpus) : 156.0
% 0.45/0.67 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.45/0.67 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.45/0.67 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.45/0.67 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.45/0.67 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.45/0.68 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.45/0.68 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.48/0.82 % /export/starexec/sandbox/solver/bin/fo/fo1_lcnf.sh running for 50s
% 6.45/1.47 % Solved by fo/fo6_bce.sh.
% 6.45/1.47 % BCE start: 143
% 6.45/1.47 % BCE eliminated: 1
% 6.45/1.47 % PE start: 142
% 6.45/1.47 logic: eq
% 6.45/1.47 % PE eliminated: 10
% 6.45/1.47 % done 576 iterations in 0.761s
% 6.45/1.47 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 6.45/1.47 % SZS output start Refutation
% 6.45/1.47 thf(xP_type, type, xP: $i).
% 6.45/1.47 thf(xT_type, type, xT: $i).
% 6.45/1.47 thf(szDzozmdt0_type, type, szDzozmdt0: $i > $i).
% 6.45/1.47 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $i > $o).
% 6.45/1.47 thf(aSet0_type, type, aSet0: $i > $o).
% 6.45/1.47 thf(sk__1_type, type, sk__1: $i > $i > $i).
% 6.45/1.47 thf(sk__18_type, type, sk__18: $i).
% 6.45/1.47 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $i > $o).
% 6.45/1.47 thf(aSubsetOf0_type, type, aSubsetOf0: $i > $i > $o).
% 6.45/1.47 thf(isOn0_type, type, isOn0: $i > $i > $o).
% 6.45/1.47 thf(cS1142_type, type, cS1142: $i > $i).
% 6.45/1.47 thf(zip_tseitin_6_type, type, zip_tseitin_6: $i > $i > $o).
% 6.45/1.47 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $o).
% 6.45/1.47 thf(xU_type, type, xU: $i).
% 6.45/1.47 thf(aElement0_type, type, aElement0: $i > $o).
% 6.45/1.47 thf(cS1241_type, type, cS1241: $i > $i > $i > $i).
% 6.45/1.47 thf(aUpperBoundOfIn0_type, type, aUpperBoundOfIn0: $i > $i > $i > $o).
% 6.45/1.47 thf(xS_type, type, xS: $i).
% 6.45/1.47 thf(zip_tseitin_7_type, type, zip_tseitin_7: $i > $i > $o).
% 6.45/1.47 thf(aLowerBoundOfIn0_type, type, aLowerBoundOfIn0: $i > $i > $i > $o).
% 6.45/1.47 thf(aFunction0_type, type, aFunction0: $i > $o).
% 6.45/1.47 thf(xp_type, type, xp: $i).
% 6.45/1.47 thf(aInfimumOfIn0_type, type, aInfimumOfIn0: $i > $i > $i > $o).
% 6.45/1.47 thf(sdtlpdtrp0_type, type, sdtlpdtrp0: $i > $i > $i).
% 6.45/1.47 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $o).
% 6.45/1.47 thf(sk__16_type, type, sk__16: $i > $i).
% 6.45/1.47 thf(zip_tseitin_4_type, type, zip_tseitin_4: $i > $i > $i > $o).
% 6.45/1.47 thf(sk__19_type, type, sk__19: $i).
% 6.45/1.47 thf(xf_type, type, xf: $i).
% 6.45/1.47 thf(aFixedPointOf0_type, type, aFixedPointOf0: $i > $i > $o).
% 6.45/1.47 thf(isMonotone0_type, type, isMonotone0: $i > $o).
% 6.45/1.47 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 6.45/1.47 thf(sdtlseqdt0_type, type, sdtlseqdt0: $i > $i > $o).
% 6.45/1.47 thf(szRzazndt0_type, type, szRzazndt0: $i > $i).
% 6.45/1.47 thf(zip_tseitin_5_type, type, zip_tseitin_5: $i > $i > $o).
% 6.45/1.47 thf(aCompleteLattice0_type, type, aCompleteLattice0: $i > $o).
% 6.45/1.47 thf(aSupremumOfIn0_type, type, aSupremumOfIn0: $i > $i > $i > $o).
% 6.45/1.47 thf(m__1144, axiom,
% 6.45/1.47 (( ( xS ) = ( cS1142 @ xf ) ) &
% 6.45/1.47 ( ![W0:$i]:
% 6.45/1.47 ( ( ( ( ( aElementOf0 @ W0 @ ( szDzozmdt0 @ xf ) ) &
% 6.45/1.47 ( ( sdtlpdtrp0 @ xf @ W0 ) = ( W0 ) ) ) |
% 6.45/1.47 ( aFixedPointOf0 @ W0 @ xf ) ) =>
% 6.45/1.47 ( aElementOf0 @ W0 @ xS ) ) &
% 6.45/1.47 ( ( aElementOf0 @ W0 @ xS ) =>
% 6.45/1.47 ( ( aElementOf0 @ W0 @ ( szDzozmdt0 @ xf ) ) &
% 6.45/1.47 ( ( sdtlpdtrp0 @ xf @ W0 ) = ( W0 ) ) &
% 6.45/1.47 ( aFixedPointOf0 @ W0 @ xf ) ) ) ) ) &
% 6.45/1.47 ( aSet0 @ xS ))).
% 6.45/1.47 thf(zip_derived_cl91, plain,
% 6.45/1.47 (![X0 : $i]:
% 6.45/1.47 (((sdtlpdtrp0 @ xf @ X0) = (X0)) | ~ (aElementOf0 @ X0 @ xS))),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1144])).
% 6.45/1.47 thf(m__1299, axiom,
% 6.45/1.47 (( aUpperBoundOfIn0 @ ( sdtlpdtrp0 @ xf @ xp ) @ xT @ xU ) &
% 6.45/1.47 ( ![W0:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W0 @ xT ) =>
% 6.45/1.47 ( sdtlseqdt0 @ W0 @ ( sdtlpdtrp0 @ xf @ xp ) ) ) ) &
% 6.45/1.47 ( aLowerBoundOfIn0 @ ( sdtlpdtrp0 @ xf @ xp ) @ xP @ xU ) &
% 6.45/1.47 ( ![W0:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W0 @ xP ) =>
% 6.45/1.47 ( sdtlseqdt0 @ ( sdtlpdtrp0 @ xf @ xp ) @ W0 ) ) ))).
% 6.45/1.47 thf(zip_derived_cl115, plain,
% 6.45/1.47 (![X0 : $i]:
% 6.45/1.47 ( (sdtlseqdt0 @ X0 @ (sdtlpdtrp0 @ xf @ xp))
% 6.45/1.47 | ~ (aElementOf0 @ X0 @ xT))),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1299])).
% 6.45/1.47 thf(m__1261, axiom,
% 6.45/1.47 (( aInfimumOfIn0 @ xp @ xP @ xU ) & ( aElementOf0 @ xp @ xU ) &
% 6.45/1.47 ( aLowerBoundOfIn0 @ xp @ xP @ xU ) &
% 6.45/1.47 ( ![W0:$i]:
% 6.45/1.47 ( ( ( ( aElementOf0 @ W0 @ xU ) &
% 6.45/1.47 ( ![W1:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W1 @ xP ) => ( sdtlseqdt0 @ W0 @ W1 ) ) ) ) |
% 6.45/1.47 ( aLowerBoundOfIn0 @ W0 @ xP @ xU ) ) =>
% 6.45/1.47 ( sdtlseqdt0 @ W0 @ xp ) ) ) &
% 6.45/1.47 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xP ) => ( sdtlseqdt0 @ xp @ W0 ) ) ))).
% 6.45/1.47 thf(zip_derived_cl106, plain,
% 6.45/1.47 (![X0 : $i]: ( (sdtlseqdt0 @ xp @ X0) | ~ (aElementOf0 @ X0 @ xP))),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1261])).
% 6.45/1.47 thf(m__1123, axiom,
% 6.45/1.47 (( aSet0 @ xU ) &
% 6.45/1.47 ( ![W0:$i]:
% 6.45/1.47 ( ( ( aSubsetOf0 @ W0 @ xU ) |
% 6.45/1.47 ( ( ![W1:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W1 @ W0 ) => ( aElementOf0 @ W1 @ xU ) ) ) &
% 6.45/1.47 ( aSet0 @ W0 ) ) ) =>
% 6.45/1.47 ( ?[W1:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W1 @ xU ) & ( aElementOf0 @ W1 @ xU ) &
% 6.45/1.47 ( ![W2:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W2 @ W0 ) => ( sdtlseqdt0 @ W1 @ W2 ) ) ) &
% 6.45/1.47 ( aLowerBoundOfIn0 @ W1 @ W0 @ xU ) &
% 6.45/1.47 ( ![W2:$i]:
% 6.45/1.47 ( ( ( aLowerBoundOfIn0 @ W2 @ W0 @ xU ) |
% 6.45/1.47 ( ( ![W3:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W3 @ W0 ) => ( sdtlseqdt0 @ W2 @ W3 ) ) ) &
% 6.45/1.47 ( aElementOf0 @ W2 @ xU ) ) ) =>
% 6.45/1.47 ( sdtlseqdt0 @ W2 @ W1 ) ) ) &
% 6.45/1.47 ( aInfimumOfIn0 @ W1 @ W0 @ xU ) &
% 6.45/1.47 ( ?[W2:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W2 @ xU ) & ( aElementOf0 @ W2 @ xU ) &
% 6.45/1.47 ( ![W3:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W3 @ W0 ) => ( sdtlseqdt0 @ W3 @ W2 ) ) ) &
% 6.45/1.47 ( aUpperBoundOfIn0 @ W2 @ W0 @ xU ) &
% 6.45/1.47 ( ![W3:$i]:
% 6.45/1.47 ( ( ( aUpperBoundOfIn0 @ W3 @ W0 @ xU ) |
% 6.45/1.47 ( ( ![W4:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W4 @ W0 ) =>
% 6.45/1.47 ( sdtlseqdt0 @ W4 @ W3 ) ) ) &
% 6.45/1.47 ( aElementOf0 @ W3 @ xU ) ) ) =>
% 6.45/1.47 ( sdtlseqdt0 @ W2 @ W3 ) ) ) &
% 6.45/1.47 ( aSupremumOfIn0 @ W2 @ W0 @ xU ) ) ) ) ) ) ) &
% 6.45/1.47 ( aCompleteLattice0 @ xU ) & ( aFunction0 @ xf ) &
% 6.45/1.47 ( ![W0:$i,W1:$i]:
% 6.45/1.47 ( ( ( aElementOf0 @ W1 @ ( szDzozmdt0 @ xf ) ) &
% 6.45/1.47 ( aElementOf0 @ W0 @ ( szDzozmdt0 @ xf ) ) ) =>
% 6.45/1.47 ( ( sdtlseqdt0 @ W0 @ W1 ) =>
% 6.45/1.47 ( sdtlseqdt0 @ ( sdtlpdtrp0 @ xf @ W0 ) @ ( sdtlpdtrp0 @ xf @ W1 ) ) ) ) ) &
% 6.45/1.47 ( isMonotone0 @ xf ) & ( ( szDzozmdt0 @ xf ) = ( szRzazndt0 @ xf ) ) &
% 6.45/1.47 ( ( szRzazndt0 @ xf ) = ( xU ) ) & ( isOn0 @ xf @ xU ))).
% 6.45/1.47 thf(zf_stmt_0, type, zip_tseitin_7 : $i > $i > $o).
% 6.45/1.47 thf(zf_stmt_1, axiom,
% 6.45/1.47 (![W1:$i,W0:$i]:
% 6.45/1.47 ( ( zip_tseitin_7 @ W1 @ W0 ) =>
% 6.45/1.47 ( ( ?[W2:$i]: ( zip_tseitin_6 @ W2 @ W0 ) ) &
% 6.45/1.47 ( aInfimumOfIn0 @ W1 @ W0 @ xU ) &
% 6.45/1.47 ( ![W2:$i]:
% 6.45/1.47 ( ( zip_tseitin_3 @ W2 @ W0 ) => ( sdtlseqdt0 @ W2 @ W1 ) ) ) &
% 6.45/1.47 ( aLowerBoundOfIn0 @ W1 @ W0 @ xU ) &
% 6.45/1.47 ( ![W2:$i]: ( ( aElementOf0 @ W2 @ W0 ) => ( sdtlseqdt0 @ W1 @ W2 ) ) ) &
% 6.45/1.47 ( aElementOf0 @ W1 @ xU ) & ( aElementOf0 @ W1 @ xU ) ) ))).
% 6.45/1.47 thf(zf_stmt_2, type, zip_tseitin_6 : $i > $i > $o).
% 6.45/1.47 thf(zf_stmt_3, axiom,
% 6.45/1.47 (![W2:$i,W0:$i]:
% 6.45/1.47 ( ( zip_tseitin_6 @ W2 @ W0 ) =>
% 6.45/1.47 ( ( aSupremumOfIn0 @ W2 @ W0 @ xU ) &
% 6.45/1.47 ( ![W3:$i]:
% 6.45/1.47 ( ( zip_tseitin_5 @ W3 @ W0 ) => ( sdtlseqdt0 @ W2 @ W3 ) ) ) &
% 6.45/1.47 ( aUpperBoundOfIn0 @ W2 @ W0 @ xU ) &
% 6.45/1.47 ( ![W3:$i]: ( ( aElementOf0 @ W3 @ W0 ) => ( sdtlseqdt0 @ W3 @ W2 ) ) ) &
% 6.45/1.47 ( aElementOf0 @ W2 @ xU ) & ( aElementOf0 @ W2 @ xU ) ) ))).
% 6.45/1.47 thf(zf_stmt_4, type, zip_tseitin_5 : $i > $i > $o).
% 6.45/1.47 thf(zf_stmt_5, axiom,
% 6.45/1.47 (![W3:$i,W0:$i]:
% 6.45/1.47 ( ( ( ( aElementOf0 @ W3 @ xU ) &
% 6.45/1.47 ( ![W4:$i]: ( zip_tseitin_4 @ W4 @ W3 @ W0 ) ) ) |
% 6.45/1.47 ( aUpperBoundOfIn0 @ W3 @ W0 @ xU ) ) =>
% 6.45/1.47 ( zip_tseitin_5 @ W3 @ W0 ) ))).
% 6.45/1.47 thf(zf_stmt_6, type, zip_tseitin_4 : $i > $i > $i > $o).
% 6.45/1.47 thf(zf_stmt_7, axiom,
% 6.45/1.47 (![W4:$i,W3:$i,W0:$i]:
% 6.45/1.47 ( ( ( aElementOf0 @ W4 @ W0 ) => ( sdtlseqdt0 @ W4 @ W3 ) ) =>
% 6.45/1.47 ( zip_tseitin_4 @ W4 @ W3 @ W0 ) ))).
% 6.45/1.47 thf(zf_stmt_8, type, zip_tseitin_3 : $i > $i > $o).
% 6.45/1.47 thf(zf_stmt_9, axiom,
% 6.45/1.47 (![W2:$i,W0:$i]:
% 6.45/1.47 ( ( ( ( aElementOf0 @ W2 @ xU ) &
% 6.45/1.47 ( ![W3:$i]: ( zip_tseitin_2 @ W3 @ W2 @ W0 ) ) ) |
% 6.45/1.47 ( aLowerBoundOfIn0 @ W2 @ W0 @ xU ) ) =>
% 6.45/1.47 ( zip_tseitin_3 @ W2 @ W0 ) ))).
% 6.45/1.47 thf(zf_stmt_10, type, zip_tseitin_2 : $i > $i > $i > $o).
% 6.45/1.47 thf(zf_stmt_11, axiom,
% 6.45/1.47 (![W3:$i,W2:$i,W0:$i]:
% 6.45/1.47 ( ( ( aElementOf0 @ W3 @ W0 ) => ( sdtlseqdt0 @ W2 @ W3 ) ) =>
% 6.45/1.47 ( zip_tseitin_2 @ W3 @ W2 @ W0 ) ))).
% 6.45/1.47 thf(zf_stmt_12, type, zip_tseitin_1 : $i > $o).
% 6.45/1.47 thf(zf_stmt_13, axiom,
% 6.45/1.47 (![W0:$i]:
% 6.45/1.47 ( ( ( ( aSet0 @ W0 ) & ( ![W1:$i]: ( zip_tseitin_0 @ W1 @ W0 ) ) ) |
% 6.45/1.47 ( aSubsetOf0 @ W0 @ xU ) ) =>
% 6.45/1.47 ( zip_tseitin_1 @ W0 ) ))).
% 6.45/1.47 thf(zf_stmt_14, type, zip_tseitin_0 : $i > $i > $o).
% 6.45/1.47 thf(zf_stmt_15, axiom,
% 6.45/1.47 (![W1:$i,W0:$i]:
% 6.45/1.47 ( ( ( aElementOf0 @ W1 @ W0 ) => ( aElementOf0 @ W1 @ xU ) ) =>
% 6.45/1.47 ( zip_tseitin_0 @ W1 @ W0 ) ))).
% 6.45/1.47 thf(zf_stmt_16, axiom,
% 6.45/1.47 (( isOn0 @ xf @ xU ) & ( ( szRzazndt0 @ xf ) = ( xU ) ) &
% 6.45/1.47 ( ( szDzozmdt0 @ xf ) = ( szRzazndt0 @ xf ) ) & ( isMonotone0 @ xf ) &
% 6.45/1.47 ( ![W0:$i,W1:$i]:
% 6.45/1.47 ( ( ( aElementOf0 @ W0 @ ( szDzozmdt0 @ xf ) ) &
% 6.45/1.47 ( aElementOf0 @ W1 @ ( szDzozmdt0 @ xf ) ) ) =>
% 6.45/1.47 ( ( sdtlseqdt0 @ W0 @ W1 ) =>
% 6.45/1.47 ( sdtlseqdt0 @ ( sdtlpdtrp0 @ xf @ W0 ) @ ( sdtlpdtrp0 @ xf @ W1 ) ) ) ) ) &
% 6.45/1.47 ( aFunction0 @ xf ) & ( aCompleteLattice0 @ xU ) &
% 6.45/1.47 ( ![W0:$i]:
% 6.45/1.47 ( ( zip_tseitin_1 @ W0 ) => ( ?[W1:$i]: ( zip_tseitin_7 @ W1 @ W0 ) ) ) ) &
% 6.45/1.47 ( aSet0 @ xU ))).
% 6.45/1.47 thf(zip_derived_cl85, plain, (((szRzazndt0 @ xf) = (xU))),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_16])).
% 6.45/1.47 thf(mImgSort, axiom,
% 6.45/1.47 (![W0:$i]:
% 6.45/1.47 ( ( aFunction0 @ W0 ) =>
% 6.45/1.47 ( ![W1:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W1 @ ( szDzozmdt0 @ W0 ) ) =>
% 6.45/1.47 ( aElementOf0 @ ( sdtlpdtrp0 @ W0 @ W1 ) @ ( szRzazndt0 @ W0 ) ) ) ) ))).
% 6.45/1.47 thf(zip_derived_cl44, plain,
% 6.45/1.47 (![X0 : $i, X1 : $i]:
% 6.45/1.47 (~ (aElementOf0 @ X0 @ (szDzozmdt0 @ X1))
% 6.45/1.47 | (aElementOf0 @ (sdtlpdtrp0 @ X1 @ X0) @ (szRzazndt0 @ X1))
% 6.45/1.47 | ~ (aFunction0 @ X1))),
% 6.45/1.47 inference('cnf', [status(esa)], [mImgSort])).
% 6.45/1.47 thf(zip_derived_cl1415, plain,
% 6.45/1.47 (![X0 : $i]:
% 6.45/1.47 (~ (aElementOf0 @ X0 @ (szDzozmdt0 @ xf))
% 6.45/1.47 | (aElementOf0 @ (sdtlpdtrp0 @ xf @ X0) @ xU)
% 6.45/1.47 | ~ (aFunction0 @ xf))),
% 6.45/1.47 inference('s_sup+', [status(thm)], [zip_derived_cl85, zip_derived_cl44])).
% 6.45/1.47 thf(zip_derived_cl84, plain, (((szDzozmdt0 @ xf) = (szRzazndt0 @ xf))),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_16])).
% 6.45/1.47 thf(zip_derived_cl85, plain, (((szRzazndt0 @ xf) = (xU))),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_16])).
% 6.45/1.47 thf(zip_derived_cl1200, plain, (((szDzozmdt0 @ xf) = (xU))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 6.45/1.47 thf(zip_derived_cl81, plain, ( (aFunction0 @ xf)),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_16])).
% 6.45/1.47 thf(zip_derived_cl1417, plain,
% 6.45/1.47 (![X0 : $i]:
% 6.45/1.47 (~ (aElementOf0 @ X0 @ xU)
% 6.45/1.47 | (aElementOf0 @ (sdtlpdtrp0 @ xf @ X0) @ xU))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1415, zip_derived_cl1200, zip_derived_cl81])).
% 6.45/1.47 thf(mEOfElem, axiom,
% 6.45/1.47 (![W0:$i]:
% 6.45/1.47 ( ( aSet0 @ W0 ) =>
% 6.45/1.47 ( ![W1:$i]: ( ( aElementOf0 @ W1 @ W0 ) => ( aElement0 @ W1 ) ) ) ))).
% 6.45/1.47 thf(zip_derived_cl2, plain,
% 6.45/1.47 (![X0 : $i, X1 : $i]:
% 6.45/1.47 (~ (aElementOf0 @ X0 @ X1) | (aElement0 @ X0) | ~ (aSet0 @ X1))),
% 6.45/1.47 inference('cnf', [status(esa)], [mEOfElem])).
% 6.45/1.47 thf(zip_derived_cl1438, plain,
% 6.45/1.47 (![X0 : $i]:
% 6.45/1.47 (~ (aElementOf0 @ X0 @ xU)
% 6.45/1.47 | (aElement0 @ (sdtlpdtrp0 @ xf @ X0))
% 6.45/1.47 | ~ (aSet0 @ xU))),
% 6.45/1.47 inference('s_sup-', [status(thm)], [zip_derived_cl1417, zip_derived_cl2])).
% 6.45/1.47 thf(zip_derived_cl78, plain, ( (aSet0 @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_16])).
% 6.45/1.47 thf(zip_derived_cl1441, plain,
% 6.45/1.47 (![X0 : $i]:
% 6.45/1.47 (~ (aElementOf0 @ X0 @ xU) | (aElement0 @ (sdtlpdtrp0 @ xf @ X0)))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl1438, zip_derived_cl78])).
% 6.45/1.47 thf(zip_derived_cl114, plain,
% 6.45/1.47 ( (aLowerBoundOfIn0 @ (sdtlpdtrp0 @ xf @ xp) @ xP @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1299])).
% 6.45/1.47 thf(zip_derived_cl109, plain,
% 6.45/1.47 (![X0 : $i]:
% 6.45/1.47 ( (sdtlseqdt0 @ X0 @ xp) | ~ (aLowerBoundOfIn0 @ X0 @ xP @ xU))),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1261])).
% 6.45/1.47 thf(zip_derived_cl1453, plain, ( (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ xp) @ xp)),
% 6.45/1.47 inference('s_sup-', [status(thm)], [zip_derived_cl114, zip_derived_cl109])).
% 6.45/1.47 thf(mASymm, axiom,
% 6.45/1.47 (![W0:$i,W1:$i]:
% 6.45/1.47 ( ( ( aElement0 @ W0 ) & ( aElement0 @ W1 ) ) =>
% 6.45/1.47 ( ( ( sdtlseqdt0 @ W0 @ W1 ) & ( sdtlseqdt0 @ W1 @ W0 ) ) =>
% 6.45/1.47 ( ( W0 ) = ( W1 ) ) ) ))).
% 6.45/1.47 thf(zip_derived_cl11, plain,
% 6.45/1.47 (![X0 : $i, X1 : $i]:
% 6.45/1.47 (~ (aElement0 @ X0)
% 6.45/1.47 | ~ (aElement0 @ X1)
% 6.45/1.47 | ((X0) = (X1))
% 6.45/1.47 | ~ (sdtlseqdt0 @ X1 @ X0)
% 6.45/1.47 | ~ (sdtlseqdt0 @ X0 @ X1))),
% 6.45/1.47 inference('cnf', [status(esa)], [mASymm])).
% 6.45/1.47 thf(zip_derived_cl1466, plain,
% 6.45/1.47 ((~ (aElement0 @ xp)
% 6.45/1.47 | ~ (aElement0 @ (sdtlpdtrp0 @ xf @ xp))
% 6.45/1.47 | ((xp) = (sdtlpdtrp0 @ xf @ xp))
% 6.45/1.47 | ~ (sdtlseqdt0 @ xp @ (sdtlpdtrp0 @ xf @ xp)))),
% 6.45/1.47 inference('s_sup-', [status(thm)], [zip_derived_cl1453, zip_derived_cl11])).
% 6.45/1.47 thf(zip_derived_cl111, plain, ( (aElementOf0 @ xp @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1261])).
% 6.45/1.47 thf(zip_derived_cl2, plain,
% 6.45/1.47 (![X0 : $i, X1 : $i]:
% 6.45/1.47 (~ (aElementOf0 @ X0 @ X1) | (aElement0 @ X0) | ~ (aSet0 @ X1))),
% 6.45/1.47 inference('cnf', [status(esa)], [mEOfElem])).
% 6.45/1.47 thf(zip_derived_cl1210, plain, (( (aElement0 @ xp) | ~ (aSet0 @ xU))),
% 6.45/1.47 inference('s_sup-', [status(thm)], [zip_derived_cl111, zip_derived_cl2])).
% 6.45/1.47 thf(zip_derived_cl78, plain, ( (aSet0 @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_16])).
% 6.45/1.47 thf(zip_derived_cl1211, plain, ( (aElement0 @ xp)),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl1210, zip_derived_cl78])).
% 6.45/1.47 thf(zip_derived_cl1469, plain,
% 6.45/1.47 ((~ (aElement0 @ (sdtlpdtrp0 @ xf @ xp))
% 6.45/1.47 | ((xp) = (sdtlpdtrp0 @ xf @ xp))
% 6.45/1.47 | ~ (sdtlseqdt0 @ xp @ (sdtlpdtrp0 @ xf @ xp)))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1466, zip_derived_cl1211])).
% 6.45/1.47 thf(zip_derived_cl1475, plain,
% 6.45/1.47 ((~ (aElementOf0 @ xp @ xU)
% 6.45/1.47 | ((xp) = (sdtlpdtrp0 @ xf @ xp))
% 6.45/1.47 | ~ (sdtlseqdt0 @ xp @ (sdtlpdtrp0 @ xf @ xp)))),
% 6.45/1.47 inference('s_sup-', [status(thm)],
% 6.45/1.47 [zip_derived_cl1441, zip_derived_cl1469])).
% 6.45/1.47 thf(zip_derived_cl111, plain, ( (aElementOf0 @ xp @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1261])).
% 6.45/1.47 thf(zip_derived_cl1477, plain,
% 6.45/1.47 ((((xp) = (sdtlpdtrp0 @ xf @ xp))
% 6.45/1.47 | ~ (sdtlseqdt0 @ xp @ (sdtlpdtrp0 @ xf @ xp)))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl1475, zip_derived_cl111])).
% 6.45/1.47 thf(zip_derived_cl1493, plain,
% 6.45/1.47 ((~ (aElementOf0 @ (sdtlpdtrp0 @ xf @ xp) @ xP)
% 6.45/1.47 | ((xp) = (sdtlpdtrp0 @ xf @ xp)))),
% 6.45/1.47 inference('s_sup-', [status(thm)],
% 6.45/1.47 [zip_derived_cl106, zip_derived_cl1477])).
% 6.45/1.47 thf(zip_derived_cl82, plain,
% 6.45/1.47 (![X0 : $i, X1 : $i]:
% 6.45/1.47 (~ (aElementOf0 @ X0 @ (szDzozmdt0 @ xf))
% 6.45/1.47 | ~ (aElementOf0 @ X1 @ (szDzozmdt0 @ xf))
% 6.45/1.47 | (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ X0) @ (sdtlpdtrp0 @ xf @ X1))
% 6.45/1.47 | ~ (sdtlseqdt0 @ X0 @ X1))),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_16])).
% 6.45/1.47 thf(zip_derived_cl1200, plain, (((szDzozmdt0 @ xf) = (xU))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 6.45/1.47 thf(zip_derived_cl1200, plain, (((szDzozmdt0 @ xf) = (xU))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 6.45/1.47 thf(zip_derived_cl1479, plain,
% 6.45/1.47 (![X0 : $i, X1 : $i]:
% 6.45/1.47 (~ (aElementOf0 @ X0 @ xU)
% 6.45/1.47 | ~ (aElementOf0 @ X1 @ xU)
% 6.45/1.47 | (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ X0) @ (sdtlpdtrp0 @ xf @ X1))
% 6.45/1.47 | ~ (sdtlseqdt0 @ X0 @ X1))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl82, zip_derived_cl1200, zip_derived_cl1200])).
% 6.45/1.47 thf(zip_derived_cl114, plain,
% 6.45/1.47 ( (aLowerBoundOfIn0 @ (sdtlpdtrp0 @ xf @ xp) @ xP @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1299])).
% 6.45/1.47 thf(mDefLB, axiom,
% 6.45/1.47 (![W0:$i]:
% 6.45/1.47 ( ( aSet0 @ W0 ) =>
% 6.45/1.47 ( ![W1:$i]:
% 6.45/1.47 ( ( aSubsetOf0 @ W1 @ W0 ) =>
% 6.45/1.47 ( ![W2:$i]:
% 6.45/1.47 ( ( aLowerBoundOfIn0 @ W2 @ W1 @ W0 ) <=>
% 6.45/1.47 ( ( aElementOf0 @ W2 @ W0 ) &
% 6.45/1.47 ( ![W3:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W3 @ W1 ) => ( sdtlseqdt0 @ W2 @ W3 ) ) ) ) ) ) ) ) ))).
% 6.45/1.47 thf(zip_derived_cl13, plain,
% 6.45/1.47 (![X0 : $i, X1 : $i, X2 : $i]:
% 6.45/1.47 (~ (aSubsetOf0 @ X0 @ X1)
% 6.45/1.47 | ~ (aLowerBoundOfIn0 @ X2 @ X0 @ X1)
% 6.45/1.47 | (aElementOf0 @ X2 @ X1)
% 6.45/1.47 | ~ (aSet0 @ X1))),
% 6.45/1.47 inference('cnf', [status(esa)], [mDefLB])).
% 6.45/1.47 thf(zip_derived_cl1334, plain,
% 6.45/1.47 ((~ (aSubsetOf0 @ xP @ xU)
% 6.45/1.47 | (aElementOf0 @ (sdtlpdtrp0 @ xf @ xp) @ xU)
% 6.45/1.47 | ~ (aSet0 @ xU))),
% 6.45/1.47 inference('s_sup-', [status(thm)], [zip_derived_cl114, zip_derived_cl13])).
% 6.45/1.47 thf(zip_derived_cl78, plain, ( (aSet0 @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_16])).
% 6.45/1.47 thf(zip_derived_cl1337, plain,
% 6.45/1.47 ((~ (aSubsetOf0 @ xP @ xU) | (aElementOf0 @ (sdtlpdtrp0 @ xf @ xp) @ xU))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl1334, zip_derived_cl78])).
% 6.45/1.47 thf(mDefSub, axiom,
% 6.45/1.47 (![W0:$i]:
% 6.45/1.47 ( ( aSet0 @ W0 ) =>
% 6.45/1.47 ( ![W1:$i]:
% 6.45/1.47 ( ( aSubsetOf0 @ W1 @ W0 ) <=>
% 6.45/1.47 ( ( aSet0 @ W1 ) &
% 6.45/1.47 ( ![W2:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W2 @ W1 ) => ( aElementOf0 @ W2 @ W0 ) ) ) ) ) ) ))).
% 6.45/1.47 thf(zip_derived_cl6, plain,
% 6.45/1.47 (![X0 : $i, X1 : $i]:
% 6.45/1.47 (~ (aSet0 @ X0)
% 6.45/1.47 | (aElementOf0 @ (sk__1 @ X0 @ X1) @ X0)
% 6.45/1.47 | (aSubsetOf0 @ X0 @ X1)
% 6.45/1.47 | ~ (aSet0 @ X1))),
% 6.45/1.47 inference('cnf', [status(esa)], [mDefSub])).
% 6.45/1.47 thf(m__1244, axiom,
% 6.45/1.47 (( ( xP ) = ( cS1241 @ xU @ xf @ xT ) ) &
% 6.45/1.47 ( ![W0:$i]:
% 6.45/1.47 ( ( ( ( aElementOf0 @ W0 @ xU ) &
% 6.45/1.47 ( sdtlseqdt0 @ ( sdtlpdtrp0 @ xf @ W0 ) @ W0 ) &
% 6.45/1.47 ( ( ![W1:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W1 @ xT ) => ( sdtlseqdt0 @ W1 @ W0 ) ) ) |
% 6.45/1.47 ( aUpperBoundOfIn0 @ W0 @ xT @ xU ) ) ) =>
% 6.45/1.47 ( aElementOf0 @ W0 @ xP ) ) &
% 6.45/1.47 ( ( aElementOf0 @ W0 @ xP ) =>
% 6.45/1.47 ( ( aElementOf0 @ W0 @ xU ) &
% 6.45/1.47 ( sdtlseqdt0 @ ( sdtlpdtrp0 @ xf @ W0 ) @ W0 ) &
% 6.45/1.47 ( ![W1:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W1 @ xT ) => ( sdtlseqdt0 @ W1 @ W0 ) ) ) &
% 6.45/1.47 ( aUpperBoundOfIn0 @ W0 @ xT @ xU ) ) ) ) ) &
% 6.45/1.47 ( aSet0 @ xP ))).
% 6.45/1.47 thf(zip_derived_cl101, plain,
% 6.45/1.47 (![X0 : $i]: ( (aElementOf0 @ X0 @ xU) | ~ (aElementOf0 @ X0 @ xP))),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1244])).
% 6.45/1.47 thf(zip_derived_cl1361, plain,
% 6.45/1.47 (![X0 : $i]:
% 6.45/1.47 (~ (aSet0 @ X0)
% 6.45/1.47 | (aSubsetOf0 @ xP @ X0)
% 6.45/1.47 | ~ (aSet0 @ xP)
% 6.45/1.47 | (aElementOf0 @ (sk__1 @ xP @ X0) @ xU))),
% 6.45/1.47 inference('s_sup-', [status(thm)], [zip_derived_cl6, zip_derived_cl101])).
% 6.45/1.47 thf(zip_derived_cl97, plain, ( (aSet0 @ xP)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1244])).
% 6.45/1.47 thf(zip_derived_cl1363, plain,
% 6.45/1.47 (![X0 : $i]:
% 6.45/1.47 (~ (aSet0 @ X0)
% 6.45/1.47 | (aSubsetOf0 @ xP @ X0)
% 6.45/1.47 | (aElementOf0 @ (sk__1 @ xP @ X0) @ xU))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl1361, zip_derived_cl97])).
% 6.45/1.47 thf(zip_derived_cl5, plain,
% 6.45/1.47 (![X0 : $i, X1 : $i]:
% 6.45/1.47 (~ (aSet0 @ X0)
% 6.45/1.47 | ~ (aElementOf0 @ (sk__1 @ X0 @ X1) @ X1)
% 6.45/1.47 | (aSubsetOf0 @ X0 @ X1)
% 6.45/1.47 | ~ (aSet0 @ X1))),
% 6.45/1.47 inference('cnf', [status(esa)], [mDefSub])).
% 6.45/1.47 thf(zip_derived_cl2599, plain,
% 6.45/1.47 (( (aSubsetOf0 @ xP @ xU)
% 6.45/1.47 | ~ (aSet0 @ xU)
% 6.45/1.47 | ~ (aSet0 @ xP)
% 6.45/1.47 | (aSubsetOf0 @ xP @ xU)
% 6.45/1.47 | ~ (aSet0 @ xU))),
% 6.45/1.47 inference('s_sup-', [status(thm)], [zip_derived_cl1363, zip_derived_cl5])).
% 6.45/1.47 thf(zip_derived_cl78, plain, ( (aSet0 @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_16])).
% 6.45/1.47 thf(zip_derived_cl97, plain, ( (aSet0 @ xP)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1244])).
% 6.45/1.47 thf(zip_derived_cl78, plain, ( (aSet0 @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_16])).
% 6.45/1.47 thf(zip_derived_cl2603, plain,
% 6.45/1.47 (( (aSubsetOf0 @ xP @ xU) | (aSubsetOf0 @ xP @ xU))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl2599, zip_derived_cl78, zip_derived_cl97,
% 6.45/1.47 zip_derived_cl78])).
% 6.45/1.47 thf(zip_derived_cl2604, plain, ( (aSubsetOf0 @ xP @ xU)),
% 6.45/1.47 inference('simplify', [status(thm)], [zip_derived_cl2603])).
% 6.45/1.47 thf(zip_derived_cl2605, plain,
% 6.45/1.47 ( (aElementOf0 @ (sdtlpdtrp0 @ xf @ xp) @ xU)),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1337, zip_derived_cl2604])).
% 6.45/1.47 thf(zip_derived_cl98, plain,
% 6.45/1.47 (![X0 : $i]:
% 6.45/1.47 ( (aElementOf0 @ X0 @ xP)
% 6.45/1.47 | ~ (aUpperBoundOfIn0 @ X0 @ xT @ xU)
% 6.45/1.47 | ~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ X0) @ X0)
% 6.45/1.47 | ~ (aElementOf0 @ X0 @ xU))),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1244])).
% 6.45/1.47 thf(zip_derived_cl2621, plain,
% 6.45/1.47 (( (aElementOf0 @ (sdtlpdtrp0 @ xf @ xp) @ xP)
% 6.45/1.47 | ~ (aUpperBoundOfIn0 @ (sdtlpdtrp0 @ xf @ xp) @ xT @ xU)
% 6.45/1.47 | ~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ (sdtlpdtrp0 @ xf @ xp)) @
% 6.45/1.47 (sdtlpdtrp0 @ xf @ xp)))),
% 6.45/1.47 inference('s_sup-', [status(thm)], [zip_derived_cl2605, zip_derived_cl98])).
% 6.45/1.47 thf(zip_derived_cl116, plain,
% 6.45/1.47 ( (aUpperBoundOfIn0 @ (sdtlpdtrp0 @ xf @ xp) @ xT @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1299])).
% 6.45/1.47 thf(zip_derived_cl2643, plain,
% 6.45/1.47 (( (aElementOf0 @ (sdtlpdtrp0 @ xf @ xp) @ xP)
% 6.45/1.47 | ~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ (sdtlpdtrp0 @ xf @ xp)) @
% 6.45/1.47 (sdtlpdtrp0 @ xf @ xp)))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl2621, zip_derived_cl116])).
% 6.45/1.47 thf(zip_derived_cl2762, plain,
% 6.45/1.47 ((~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ xp) @ xp)
% 6.45/1.47 | ~ (aElementOf0 @ xp @ xU)
% 6.45/1.47 | ~ (aElementOf0 @ (sdtlpdtrp0 @ xf @ xp) @ xU)
% 6.45/1.47 | (aElementOf0 @ (sdtlpdtrp0 @ xf @ xp) @ xP))),
% 6.45/1.47 inference('s_sup-', [status(thm)],
% 6.45/1.47 [zip_derived_cl1479, zip_derived_cl2643])).
% 6.45/1.47 thf(zip_derived_cl1453, plain, ( (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ xp) @ xp)),
% 6.45/1.47 inference('s_sup-', [status(thm)], [zip_derived_cl114, zip_derived_cl109])).
% 6.45/1.47 thf(zip_derived_cl111, plain, ( (aElementOf0 @ xp @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1261])).
% 6.45/1.47 thf(zip_derived_cl2605, plain,
% 6.45/1.47 ( (aElementOf0 @ (sdtlpdtrp0 @ xf @ xp) @ xU)),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1337, zip_derived_cl2604])).
% 6.45/1.47 thf(zip_derived_cl2766, plain,
% 6.45/1.47 ( (aElementOf0 @ (sdtlpdtrp0 @ xf @ xp) @ xP)),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl2762, zip_derived_cl1453, zip_derived_cl111,
% 6.45/1.47 zip_derived_cl2605])).
% 6.45/1.47 thf(zip_derived_cl2779, plain, (((xp) = (sdtlpdtrp0 @ xf @ xp))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1493, zip_derived_cl2766])).
% 6.45/1.47 thf(zip_derived_cl2825, plain,
% 6.45/1.47 (![X0 : $i]: ( (sdtlseqdt0 @ X0 @ xp) | ~ (aElementOf0 @ X0 @ xT))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl115, zip_derived_cl2779])).
% 6.45/1.47 thf(m__, conjecture,
% 6.45/1.47 (( ( aFixedPointOf0 @ xp @ xf ) |
% 6.45/1.47 ( ( ( sdtlpdtrp0 @ xf @ xp ) = ( xp ) ) &
% 6.45/1.47 ( aElementOf0 @ xp @ ( szDzozmdt0 @ xf ) ) ) ) &
% 6.45/1.47 ( ( aSupremumOfIn0 @ xp @ xT @ xS ) |
% 6.45/1.47 ( ( ![W0:$i]:
% 6.45/1.47 ( ( ( aElementOf0 @ W0 @ xS ) &
% 6.45/1.47 ( ![W1:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W1 @ xT ) => ( sdtlseqdt0 @ W1 @ W0 ) ) ) &
% 6.45/1.47 ( aUpperBoundOfIn0 @ W0 @ xT @ xS ) ) =>
% 6.45/1.47 ( sdtlseqdt0 @ xp @ W0 ) ) ) &
% 6.45/1.47 ( ( aUpperBoundOfIn0 @ xp @ xT @ xS ) |
% 6.45/1.47 ( ![W0:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W0 @ xT ) => ( sdtlseqdt0 @ W0 @ xp ) ) ) ) ) ))).
% 6.45/1.47 thf(zf_stmt_17, negated_conjecture,
% 6.45/1.47 (~( ( ( aFixedPointOf0 @ xp @ xf ) |
% 6.45/1.47 ( ( ( sdtlpdtrp0 @ xf @ xp ) = ( xp ) ) &
% 6.45/1.47 ( aElementOf0 @ xp @ ( szDzozmdt0 @ xf ) ) ) ) &
% 6.45/1.47 ( ( aSupremumOfIn0 @ xp @ xT @ xS ) |
% 6.45/1.47 ( ( ![W0:$i]:
% 6.45/1.47 ( ( ( aElementOf0 @ W0 @ xS ) &
% 6.45/1.47 ( ![W1:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W1 @ xT ) => ( sdtlseqdt0 @ W1 @ W0 ) ) ) &
% 6.45/1.47 ( aUpperBoundOfIn0 @ W0 @ xT @ xS ) ) =>
% 6.45/1.47 ( sdtlseqdt0 @ xp @ W0 ) ) ) &
% 6.45/1.47 ( ( aUpperBoundOfIn0 @ xp @ xT @ xS ) |
% 6.45/1.47 ( ![W0:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W0 @ xT ) => ( sdtlseqdt0 @ W0 @ xp ) ) ) ) ) ) )),
% 6.45/1.47 inference('cnf.neg', [status(esa)], [m__])).
% 6.45/1.47 thf(zip_derived_cl131, plain,
% 6.45/1.47 ((~ (aElementOf0 @ xp @ (szDzozmdt0 @ xf))
% 6.45/1.47 | ((sdtlpdtrp0 @ xf @ xp) != (xp))
% 6.45/1.47 | (aElementOf0 @ sk__18 @ xS)
% 6.45/1.47 | ~ (sdtlseqdt0 @ sk__19 @ xp))),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_17])).
% 6.45/1.47 thf(zip_derived_cl1200, plain, (((szDzozmdt0 @ xf) = (xU))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 6.45/1.47 thf(zip_derived_cl111, plain, ( (aElementOf0 @ xp @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1261])).
% 6.45/1.47 thf(zip_derived_cl1312, plain,
% 6.45/1.47 ((((sdtlpdtrp0 @ xf @ xp) != (xp))
% 6.45/1.47 | (aElementOf0 @ sk__18 @ xS)
% 6.45/1.47 | ~ (sdtlseqdt0 @ sk__19 @ xp))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl131, zip_derived_cl1200, zip_derived_cl111])).
% 6.45/1.47 thf(zip_derived_cl2779, plain, (((xp) = (sdtlpdtrp0 @ xf @ xp))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1493, zip_derived_cl2766])).
% 6.45/1.47 thf(zip_derived_cl2837, plain,
% 6.45/1.47 ((((xp) != (xp))
% 6.45/1.47 | (aElementOf0 @ sk__18 @ xS)
% 6.45/1.47 | ~ (sdtlseqdt0 @ sk__19 @ xp))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1312, zip_derived_cl2779])).
% 6.45/1.47 thf(zip_derived_cl2838, plain,
% 6.45/1.47 ((~ (sdtlseqdt0 @ sk__19 @ xp) | (aElementOf0 @ sk__18 @ xS))),
% 6.45/1.47 inference('simplify', [status(thm)], [zip_derived_cl2837])).
% 6.45/1.47 thf(zip_derived_cl2970, plain,
% 6.45/1.47 ((~ (aElementOf0 @ sk__19 @ xT) | (aElementOf0 @ sk__18 @ xS))),
% 6.45/1.47 inference('s_sup-', [status(thm)],
% 6.45/1.47 [zip_derived_cl2825, zip_derived_cl2838])).
% 6.45/1.47 thf(zip_derived_cl132, plain,
% 6.45/1.47 ((~ (aElementOf0 @ xp @ (szDzozmdt0 @ xf))
% 6.45/1.47 | ((sdtlpdtrp0 @ xf @ xp) != (xp))
% 6.45/1.47 | (aElementOf0 @ sk__18 @ xS)
% 6.45/1.47 | (aElementOf0 @ sk__19 @ xT))),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_17])).
% 6.45/1.47 thf(zip_derived_cl1200, plain, (((szDzozmdt0 @ xf) = (xU))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 6.45/1.47 thf(zip_derived_cl111, plain, ( (aElementOf0 @ xp @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1261])).
% 6.45/1.47 thf(zip_derived_cl1352, plain,
% 6.45/1.47 ((((sdtlpdtrp0 @ xf @ xp) != (xp))
% 6.45/1.47 | (aElementOf0 @ sk__18 @ xS)
% 6.45/1.47 | (aElementOf0 @ sk__19 @ xT))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl132, zip_derived_cl1200, zip_derived_cl111])).
% 6.45/1.47 thf(zip_derived_cl2779, plain, (((xp) = (sdtlpdtrp0 @ xf @ xp))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1493, zip_derived_cl2766])).
% 6.45/1.47 thf(zip_derived_cl2845, plain,
% 6.45/1.47 ((((xp) != (xp))
% 6.45/1.47 | (aElementOf0 @ sk__18 @ xS)
% 6.45/1.47 | (aElementOf0 @ sk__19 @ xT))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1352, zip_derived_cl2779])).
% 6.45/1.47 thf(zip_derived_cl2846, plain,
% 6.45/1.47 (( (aElementOf0 @ sk__19 @ xT) | (aElementOf0 @ sk__18 @ xS))),
% 6.45/1.47 inference('simplify', [status(thm)], [zip_derived_cl2845])).
% 6.45/1.47 thf(zip_derived_cl3050, plain, ( (aElementOf0 @ sk__18 @ xS)),
% 6.45/1.47 inference('clc', [status(thm)], [zip_derived_cl2970, zip_derived_cl2846])).
% 6.45/1.47 thf(zip_derived_cl90, plain,
% 6.45/1.47 (![X0 : $i]:
% 6.45/1.47 ( (aElementOf0 @ X0 @ (szDzozmdt0 @ xf)) | ~ (aElementOf0 @ X0 @ xS))),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1144])).
% 6.45/1.47 thf(zip_derived_cl1200, plain, (((szDzozmdt0 @ xf) = (xU))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 6.45/1.47 thf(zip_derived_cl1318, plain,
% 6.45/1.47 (![X0 : $i]: ( (aElementOf0 @ X0 @ xU) | ~ (aElementOf0 @ X0 @ xS))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl90, zip_derived_cl1200])).
% 6.45/1.47 thf(zip_derived_cl3055, plain, ( (aElementOf0 @ sk__18 @ xU)),
% 6.45/1.47 inference('s_sup-', [status(thm)],
% 6.45/1.47 [zip_derived_cl3050, zip_derived_cl1318])).
% 6.45/1.47 thf(zip_derived_cl100, plain,
% 6.45/1.47 (![X0 : $i]:
% 6.45/1.47 ( (aElementOf0 @ X0 @ xP)
% 6.45/1.47 | (aElementOf0 @ (sk__16 @ X0) @ xT)
% 6.45/1.47 | ~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ X0) @ X0)
% 6.45/1.47 | ~ (aElementOf0 @ X0 @ xU))),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1244])).
% 6.45/1.47 thf(zip_derived_cl3110, plain,
% 6.45/1.47 (( (aElementOf0 @ sk__18 @ xP)
% 6.45/1.47 | (aElementOf0 @ (sk__16 @ sk__18) @ xT)
% 6.45/1.47 | ~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ sk__18) @ sk__18))),
% 6.45/1.47 inference('s_sup-', [status(thm)],
% 6.45/1.47 [zip_derived_cl3055, zip_derived_cl100])).
% 6.45/1.47 thf(zip_derived_cl106, plain,
% 6.45/1.47 (![X0 : $i]: ( (sdtlseqdt0 @ xp @ X0) | ~ (aElementOf0 @ X0 @ xP))),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1261])).
% 6.45/1.47 thf(zip_derived_cl2825, plain,
% 6.45/1.47 (![X0 : $i]: ( (sdtlseqdt0 @ X0 @ xp) | ~ (aElementOf0 @ X0 @ xT))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl115, zip_derived_cl2779])).
% 6.45/1.47 thf(zip_derived_cl140, plain,
% 6.45/1.47 ((~ (aElementOf0 @ xp @ (szDzozmdt0 @ xf))
% 6.45/1.47 | ((sdtlpdtrp0 @ xf @ xp) != (xp))
% 6.45/1.47 | ~ (sdtlseqdt0 @ xp @ sk__18)
% 6.45/1.47 | ~ (sdtlseqdt0 @ sk__19 @ xp))),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_17])).
% 6.45/1.47 thf(zip_derived_cl1200, plain, (((szDzozmdt0 @ xf) = (xU))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 6.45/1.47 thf(zip_derived_cl111, plain, ( (aElementOf0 @ xp @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1261])).
% 6.45/1.47 thf(zip_derived_cl1234, plain,
% 6.45/1.47 ((((sdtlpdtrp0 @ xf @ xp) != (xp))
% 6.45/1.47 | ~ (sdtlseqdt0 @ xp @ sk__18)
% 6.45/1.47 | ~ (sdtlseqdt0 @ sk__19 @ xp))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl140, zip_derived_cl1200, zip_derived_cl111])).
% 6.45/1.47 thf(zip_derived_cl2779, plain, (((xp) = (sdtlpdtrp0 @ xf @ xp))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1493, zip_derived_cl2766])).
% 6.45/1.47 thf(zip_derived_cl2831, plain,
% 6.45/1.47 ((((xp) != (xp))
% 6.45/1.47 | ~ (sdtlseqdt0 @ xp @ sk__18)
% 6.45/1.47 | ~ (sdtlseqdt0 @ sk__19 @ xp))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1234, zip_derived_cl2779])).
% 6.45/1.47 thf(zip_derived_cl2832, plain,
% 6.45/1.47 ((~ (sdtlseqdt0 @ sk__19 @ xp) | ~ (sdtlseqdt0 @ xp @ sk__18))),
% 6.45/1.47 inference('simplify', [status(thm)], [zip_derived_cl2831])).
% 6.45/1.47 thf(zip_derived_cl2966, plain,
% 6.45/1.47 ((~ (aElementOf0 @ sk__19 @ xT) | ~ (sdtlseqdt0 @ xp @ sk__18))),
% 6.45/1.47 inference('s_sup-', [status(thm)],
% 6.45/1.47 [zip_derived_cl2825, zip_derived_cl2832])).
% 6.45/1.47 thf(zip_derived_cl141, plain,
% 6.45/1.47 ((~ (aElementOf0 @ xp @ (szDzozmdt0 @ xf))
% 6.45/1.47 | ((sdtlpdtrp0 @ xf @ xp) != (xp))
% 6.45/1.47 | ~ (sdtlseqdt0 @ xp @ sk__18)
% 6.45/1.47 | (aElementOf0 @ sk__19 @ xT))),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_17])).
% 6.45/1.47 thf(zip_derived_cl1200, plain, (((szDzozmdt0 @ xf) = (xU))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 6.45/1.47 thf(zip_derived_cl111, plain, ( (aElementOf0 @ xp @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1261])).
% 6.45/1.47 thf(zip_derived_cl1315, plain,
% 6.45/1.47 ((((sdtlpdtrp0 @ xf @ xp) != (xp))
% 6.45/1.47 | ~ (sdtlseqdt0 @ xp @ sk__18)
% 6.45/1.47 | (aElementOf0 @ sk__19 @ xT))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl141, zip_derived_cl1200, zip_derived_cl111])).
% 6.45/1.47 thf(zip_derived_cl2779, plain, (((xp) = (sdtlpdtrp0 @ xf @ xp))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1493, zip_derived_cl2766])).
% 6.45/1.47 thf(zip_derived_cl2839, plain,
% 6.45/1.47 ((((xp) != (xp))
% 6.45/1.47 | ~ (sdtlseqdt0 @ xp @ sk__18)
% 6.45/1.47 | (aElementOf0 @ sk__19 @ xT))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1315, zip_derived_cl2779])).
% 6.45/1.47 thf(zip_derived_cl2840, plain,
% 6.45/1.47 (( (aElementOf0 @ sk__19 @ xT) | ~ (sdtlseqdt0 @ xp @ sk__18))),
% 6.45/1.47 inference('simplify', [status(thm)], [zip_derived_cl2839])).
% 6.45/1.47 thf(zip_derived_cl2991, plain, (~ (sdtlseqdt0 @ xp @ sk__18)),
% 6.45/1.47 inference('clc', [status(thm)], [zip_derived_cl2966, zip_derived_cl2840])).
% 6.45/1.47 thf(zip_derived_cl2993, plain, (~ (aElementOf0 @ sk__18 @ xP)),
% 6.45/1.47 inference('s_sup-', [status(thm)],
% 6.45/1.47 [zip_derived_cl106, zip_derived_cl2991])).
% 6.45/1.47 thf(zip_derived_cl3129, plain,
% 6.45/1.47 (( (aElementOf0 @ (sk__16 @ sk__18) @ xT)
% 6.45/1.47 | ~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ sk__18) @ sk__18))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl3110, zip_derived_cl2993])).
% 6.45/1.47 thf(zip_derived_cl2825, plain,
% 6.45/1.47 (![X0 : $i]: ( (sdtlseqdt0 @ X0 @ xp) | ~ (aElementOf0 @ X0 @ xT))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl115, zip_derived_cl2779])).
% 6.45/1.47 thf(zip_derived_cl137, plain,
% 6.45/1.47 ((~ (aElementOf0 @ xp @ (szDzozmdt0 @ xf))
% 6.45/1.47 | ((sdtlpdtrp0 @ xf @ xp) != (xp))
% 6.45/1.47 | (aUpperBoundOfIn0 @ sk__18 @ xT @ xS)
% 6.45/1.47 | ~ (sdtlseqdt0 @ sk__19 @ xp))),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_17])).
% 6.45/1.47 thf(zip_derived_cl1200, plain, (((szDzozmdt0 @ xf) = (xU))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 6.45/1.47 thf(zip_derived_cl111, plain, ( (aElementOf0 @ xp @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1261])).
% 6.45/1.47 thf(zip_derived_cl1323, plain,
% 6.45/1.47 ((((sdtlpdtrp0 @ xf @ xp) != (xp))
% 6.45/1.47 | (aUpperBoundOfIn0 @ sk__18 @ xT @ xS)
% 6.45/1.47 | ~ (sdtlseqdt0 @ sk__19 @ xp))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl137, zip_derived_cl1200, zip_derived_cl111])).
% 6.45/1.47 thf(zip_derived_cl2779, plain, (((xp) = (sdtlpdtrp0 @ xf @ xp))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1493, zip_derived_cl2766])).
% 6.45/1.47 thf(zip_derived_cl2841, plain,
% 6.45/1.47 ((((xp) != (xp))
% 6.45/1.47 | (aUpperBoundOfIn0 @ sk__18 @ xT @ xS)
% 6.45/1.47 | ~ (sdtlseqdt0 @ sk__19 @ xp))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1323, zip_derived_cl2779])).
% 6.45/1.47 thf(zip_derived_cl2842, plain,
% 6.45/1.47 ((~ (sdtlseqdt0 @ sk__19 @ xp) | (aUpperBoundOfIn0 @ sk__18 @ xT @ xS))),
% 6.45/1.47 inference('simplify', [status(thm)], [zip_derived_cl2841])).
% 6.45/1.47 thf(zip_derived_cl2989, plain,
% 6.45/1.47 ((~ (aElementOf0 @ sk__19 @ xT) | (aUpperBoundOfIn0 @ sk__18 @ xT @ xS))),
% 6.45/1.47 inference('s_sup-', [status(thm)],
% 6.45/1.47 [zip_derived_cl2825, zip_derived_cl2842])).
% 6.45/1.47 thf(zip_derived_cl138, plain,
% 6.45/1.47 ((~ (aElementOf0 @ xp @ (szDzozmdt0 @ xf))
% 6.45/1.47 | ((sdtlpdtrp0 @ xf @ xp) != (xp))
% 6.45/1.47 | (aUpperBoundOfIn0 @ sk__18 @ xT @ xS)
% 6.45/1.47 | (aElementOf0 @ sk__19 @ xT))),
% 6.45/1.47 inference('cnf', [status(esa)], [zf_stmt_17])).
% 6.45/1.47 thf(zip_derived_cl1200, plain, (((szDzozmdt0 @ xf) = (xU))),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 6.45/1.47 thf(zip_derived_cl111, plain, ( (aElementOf0 @ xp @ xU)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1261])).
% 6.45/1.47 thf(zip_derived_cl1355, plain,
% 6.45/1.47 ((((sdtlpdtrp0 @ xf @ xp) != (xp))
% 6.45/1.47 | (aUpperBoundOfIn0 @ sk__18 @ xT @ xS)
% 6.45/1.47 | (aElementOf0 @ sk__19 @ xT))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl138, zip_derived_cl1200, zip_derived_cl111])).
% 6.45/1.47 thf(zip_derived_cl2779, plain, (((xp) = (sdtlpdtrp0 @ xf @ xp))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1493, zip_derived_cl2766])).
% 6.45/1.47 thf(zip_derived_cl2847, plain,
% 6.45/1.47 ((((xp) != (xp))
% 6.45/1.47 | (aUpperBoundOfIn0 @ sk__18 @ xT @ xS)
% 6.45/1.47 | (aElementOf0 @ sk__19 @ xT))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl1355, zip_derived_cl2779])).
% 6.45/1.47 thf(zip_derived_cl2848, plain,
% 6.45/1.47 (( (aElementOf0 @ sk__19 @ xT) | (aUpperBoundOfIn0 @ sk__18 @ xT @ xS))),
% 6.45/1.47 inference('simplify', [status(thm)], [zip_derived_cl2847])).
% 6.45/1.47 thf(zip_derived_cl3062, plain, ( (aUpperBoundOfIn0 @ sk__18 @ xT @ xS)),
% 6.45/1.47 inference('clc', [status(thm)], [zip_derived_cl2989, zip_derived_cl2848])).
% 6.45/1.47 thf(mDefUB, axiom,
% 6.45/1.47 (![W0:$i]:
% 6.45/1.47 ( ( aSet0 @ W0 ) =>
% 6.45/1.47 ( ![W1:$i]:
% 6.45/1.47 ( ( aSubsetOf0 @ W1 @ W0 ) =>
% 6.45/1.47 ( ![W2:$i]:
% 6.45/1.47 ( ( aUpperBoundOfIn0 @ W2 @ W1 @ W0 ) <=>
% 6.45/1.47 ( ( aElementOf0 @ W2 @ W0 ) &
% 6.45/1.47 ( ![W3:$i]:
% 6.45/1.47 ( ( aElementOf0 @ W3 @ W1 ) => ( sdtlseqdt0 @ W3 @ W2 ) ) ) ) ) ) ) ) ))).
% 6.45/1.47 thf(zip_derived_cl18, plain,
% 6.45/1.47 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 6.45/1.47 (~ (aSubsetOf0 @ X0 @ X1)
% 6.45/1.47 | ~ (aUpperBoundOfIn0 @ X2 @ X0 @ X1)
% 6.45/1.47 | (sdtlseqdt0 @ X3 @ X2)
% 6.45/1.47 | ~ (aElementOf0 @ X3 @ X0)
% 6.45/1.47 | ~ (aSet0 @ X1))),
% 6.45/1.47 inference('cnf', [status(esa)], [mDefUB])).
% 6.45/1.47 thf(zip_derived_cl3064, plain,
% 6.45/1.47 (![X0 : $i]:
% 6.45/1.47 (~ (aSubsetOf0 @ xT @ xS)
% 6.45/1.47 | (sdtlseqdt0 @ X0 @ sk__18)
% 6.45/1.47 | ~ (aElementOf0 @ X0 @ xT)
% 6.45/1.47 | ~ (aSet0 @ xS))),
% 6.45/1.47 inference('s_sup-', [status(thm)], [zip_derived_cl3062, zip_derived_cl18])).
% 6.45/1.47 thf(m__1173, axiom,
% 6.45/1.47 (( aSubsetOf0 @ xT @ xS ) &
% 6.45/1.47 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xT ) => ( aElementOf0 @ W0 @ xS ) ) ) &
% 6.45/1.47 ( aSet0 @ xT ))).
% 6.45/1.47 thf(zip_derived_cl96, plain, ( (aSubsetOf0 @ xT @ xS)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1173])).
% 6.45/1.47 thf(zip_derived_cl87, plain, ( (aSet0 @ xS)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1144])).
% 6.45/1.47 thf(zip_derived_cl3066, plain,
% 6.45/1.47 (![X0 : $i]: ( (sdtlseqdt0 @ X0 @ sk__18) | ~ (aElementOf0 @ X0 @ xT))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl3064, zip_derived_cl96, zip_derived_cl87])).
% 6.45/1.47 thf(zip_derived_cl3055, plain, ( (aElementOf0 @ sk__18 @ xU)),
% 6.45/1.47 inference('s_sup-', [status(thm)],
% 6.45/1.47 [zip_derived_cl3050, zip_derived_cl1318])).
% 6.45/1.47 thf(zip_derived_cl99, plain,
% 6.45/1.47 (![X0 : $i]:
% 6.45/1.47 ( (aElementOf0 @ X0 @ xP)
% 6.45/1.47 | ~ (sdtlseqdt0 @ (sk__16 @ X0) @ X0)
% 6.45/1.47 | ~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ X0) @ X0)
% 6.45/1.47 | ~ (aElementOf0 @ X0 @ xU))),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1244])).
% 6.45/1.47 thf(zip_derived_cl3109, plain,
% 6.45/1.47 (( (aElementOf0 @ sk__18 @ xP)
% 6.45/1.47 | ~ (sdtlseqdt0 @ (sk__16 @ sk__18) @ sk__18)
% 6.45/1.47 | ~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ sk__18) @ sk__18))),
% 6.45/1.47 inference('s_sup-', [status(thm)], [zip_derived_cl3055, zip_derived_cl99])).
% 6.45/1.47 thf(zip_derived_cl2993, plain, (~ (aElementOf0 @ sk__18 @ xP)),
% 6.45/1.47 inference('s_sup-', [status(thm)],
% 6.45/1.47 [zip_derived_cl106, zip_derived_cl2991])).
% 6.45/1.47 thf(zip_derived_cl3128, plain,
% 6.45/1.47 ((~ (sdtlseqdt0 @ (sk__16 @ sk__18) @ sk__18)
% 6.45/1.47 | ~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ sk__18) @ sk__18))),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl3109, zip_derived_cl2993])).
% 6.45/1.47 thf(zip_derived_cl3225, plain,
% 6.45/1.47 ((~ (aElementOf0 @ (sk__16 @ sk__18) @ xT)
% 6.45/1.47 | ~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ sk__18) @ sk__18))),
% 6.45/1.47 inference('s_sup-', [status(thm)],
% 6.45/1.47 [zip_derived_cl3066, zip_derived_cl3128])).
% 6.45/1.47 thf(zip_derived_cl3338, plain,
% 6.45/1.47 (~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ sk__18) @ sk__18)),
% 6.45/1.47 inference('clc', [status(thm)], [zip_derived_cl3129, zip_derived_cl3225])).
% 6.45/1.47 thf(zip_derived_cl3342, plain,
% 6.45/1.47 ((~ (aElementOf0 @ sk__18 @ xS) | ~ (sdtlseqdt0 @ sk__18 @ sk__18))),
% 6.45/1.47 inference('s_sup-', [status(thm)], [zip_derived_cl91, zip_derived_cl3338])).
% 6.45/1.47 thf(zip_derived_cl3050, plain, ( (aElementOf0 @ sk__18 @ xS)),
% 6.45/1.47 inference('clc', [status(thm)], [zip_derived_cl2970, zip_derived_cl2846])).
% 6.45/1.47 thf(zip_derived_cl3050, plain, ( (aElementOf0 @ sk__18 @ xS)),
% 6.45/1.47 inference('clc', [status(thm)], [zip_derived_cl2970, zip_derived_cl2846])).
% 6.45/1.47 thf(zip_derived_cl2, plain,
% 6.45/1.47 (![X0 : $i, X1 : $i]:
% 6.45/1.47 (~ (aElementOf0 @ X0 @ X1) | (aElement0 @ X0) | ~ (aSet0 @ X1))),
% 6.45/1.47 inference('cnf', [status(esa)], [mEOfElem])).
% 6.45/1.47 thf(zip_derived_cl3051, plain, (( (aElement0 @ sk__18) | ~ (aSet0 @ xS))),
% 6.45/1.47 inference('s_sup-', [status(thm)], [zip_derived_cl3050, zip_derived_cl2])).
% 6.45/1.47 thf(zip_derived_cl87, plain, ( (aSet0 @ xS)),
% 6.45/1.47 inference('cnf', [status(esa)], [m__1144])).
% 6.45/1.47 thf(zip_derived_cl3059, plain, ( (aElement0 @ sk__18)),
% 6.45/1.47 inference('demod', [status(thm)], [zip_derived_cl3051, zip_derived_cl87])).
% 6.45/1.47 thf(mARefl, axiom,
% 6.45/1.47 (![W0:$i]: ( ( aElement0 @ W0 ) => ( sdtlseqdt0 @ W0 @ W0 ) ))).
% 6.45/1.47 thf(zip_derived_cl10, plain,
% 6.45/1.47 (![X0 : $i]: ( (sdtlseqdt0 @ X0 @ X0) | ~ (aElement0 @ X0))),
% 6.45/1.47 inference('cnf', [status(esa)], [mARefl])).
% 6.45/1.47 thf(zip_derived_cl3073, plain, ( (sdtlseqdt0 @ sk__18 @ sk__18)),
% 6.45/1.47 inference('s_sup-', [status(thm)], [zip_derived_cl3059, zip_derived_cl10])).
% 6.45/1.47 thf(zip_derived_cl3344, plain, ($false),
% 6.45/1.47 inference('demod', [status(thm)],
% 6.45/1.47 [zip_derived_cl3342, zip_derived_cl3050, zip_derived_cl3073])).
% 6.45/1.47
% 6.45/1.47 % SZS output end Refutation
% 6.45/1.47
% 6.45/1.47
% 6.45/1.47 % Terminating...
% 7.14/1.58 % Runner terminated.
% 7.14/1.60 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------