%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : LAT386+4 : 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.Xh55rEYgf1 true
% Computer : n024.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:48 PM UTC 2025
% Result : Theorem 34.10s 5.48s
% Output : Refutation 34.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : LAT386+4 : TPTP v9.2.0. Released v4.0.0.
% 0.03/0.14 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.Xh55rEYgf1 true
% 0.13/0.35 % Computer : n024.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Oct 1 14:35:23 EDT 2025
% 0.13/0.35 % CPUTime :
% 0.13/0.35 % Running portfolio for 300 s
% 0.13/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.35 % Number of cores: 8
% 0.13/0.35 % Python version: Python 3.6.8
% 0.13/0.35 % Running in FO mode
% 0.55/0.65 % Total configuration time : 435
% 0.55/0.65 % Estimated wc time : 1092
% 0.55/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.55/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.55/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.56/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.56/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.56/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.56/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.56/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 34.10/5.48 % Solved by fo/fo13.sh.
% 34.10/5.48 % done 3505 iterations in 4.701s
% 34.10/5.48 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 34.10/5.48 % SZS output start Refutation
% 34.10/5.48 thf(xP_type, type, xP: $i).
% 34.10/5.48 thf(xT_type, type, xT: $i).
% 34.10/5.48 thf(sk__17_type, type, sk__17: $i > $i).
% 34.10/5.48 thf(szDzozmdt0_type, type, szDzozmdt0: $i > $i).
% 34.10/5.48 thf(aSet0_type, type, aSet0: $i > $o).
% 34.10/5.48 thf(aSubsetOf0_type, type, aSubsetOf0: $i > $i > $o).
% 34.10/5.48 thf(isOn0_type, type, isOn0: $i > $i > $o).
% 34.10/5.48 thf(cS1142_type, type, cS1142: $i > $i).
% 34.10/5.48 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $i > $o).
% 34.10/5.48 thf(zip_tseitin_7_type, type, zip_tseitin_7: $i > $i > $o).
% 34.10/5.48 thf(sk__18_type, type, sk__18: $i).
% 34.10/5.48 thf(xU_type, type, xU: $i).
% 34.10/5.48 thf(aElement0_type, type, aElement0: $i > $o).
% 34.10/5.48 thf(cS1241_type, type, cS1241: $i > $i > $i > $i).
% 34.10/5.48 thf(sk__19_type, type, sk__19: $i).
% 34.10/5.48 thf(aUpperBoundOfIn0_type, type, aUpperBoundOfIn0: $i > $i > $i > $o).
% 34.10/5.48 thf(xS_type, type, xS: $i).
% 34.10/5.48 thf(aLowerBoundOfIn0_type, type, aLowerBoundOfIn0: $i > $i > $i > $o).
% 34.10/5.48 thf(aFunction0_type, type, aFunction0: $i > $o).
% 34.10/5.48 thf(zip_tseitin_5_type, type, zip_tseitin_5: $i > $i > $o).
% 34.10/5.48 thf(xp_type, type, xp: $i).
% 34.10/5.48 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $o).
% 34.10/5.48 thf(aInfimumOfIn0_type, type, aInfimumOfIn0: $i > $i > $i > $o).
% 34.10/5.48 thf(sdtlpdtrp0_type, type, sdtlpdtrp0: $i > $i > $i).
% 34.10/5.48 thf(zip_tseitin_6_type, type, zip_tseitin_6: $i > $i > $o).
% 34.10/5.48 thf(xf_type, type, xf: $i).
% 34.10/5.48 thf(aFixedPointOf0_type, type, aFixedPointOf0: $i > $i > $o).
% 34.10/5.48 thf(isMonotone0_type, type, isMonotone0: $i > $o).
% 34.10/5.48 thf(zip_tseitin_4_type, type, zip_tseitin_4: $i > $i > $i > $o).
% 34.10/5.48 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 34.10/5.48 thf(sdtlseqdt0_type, type, sdtlseqdt0: $i > $i > $o).
% 34.10/5.48 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $i > $o).
% 34.10/5.48 thf(szRzazndt0_type, type, szRzazndt0: $i > $i).
% 34.10/5.48 thf(aCompleteLattice0_type, type, aCompleteLattice0: $i > $o).
% 34.10/5.48 thf(aSupremumOfIn0_type, type, aSupremumOfIn0: $i > $i > $i > $o).
% 34.10/5.48 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $o).
% 34.10/5.48 thf(m__, conjecture,
% 34.10/5.48 (( ( aLowerBoundOfIn0 @ ( sdtlpdtrp0 @ xf @ xp ) @ xP @ xU ) |
% 34.10/5.48 ( ![W0:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W0 @ xP ) =>
% 34.10/5.48 ( sdtlseqdt0 @ ( sdtlpdtrp0 @ xf @ xp ) @ W0 ) ) ) ) &
% 34.10/5.48 ( ( aUpperBoundOfIn0 @ ( sdtlpdtrp0 @ xf @ xp ) @ xT @ xU ) |
% 34.10/5.48 ( ![W0:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W0 @ xT ) =>
% 34.10/5.48 ( sdtlseqdt0 @ W0 @ ( sdtlpdtrp0 @ xf @ xp ) ) ) ) ))).
% 34.10/5.48 thf(zf_stmt_0, negated_conjecture,
% 34.10/5.48 (~( ( ( aLowerBoundOfIn0 @ ( sdtlpdtrp0 @ xf @ xp ) @ xP @ xU ) |
% 34.10/5.48 ( ![W0:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W0 @ xP ) =>
% 34.10/5.48 ( sdtlseqdt0 @ ( sdtlpdtrp0 @ xf @ xp ) @ W0 ) ) ) ) &
% 34.10/5.48 ( ( aUpperBoundOfIn0 @ ( sdtlpdtrp0 @ xf @ xp ) @ xT @ xU ) |
% 34.10/5.48 ( ![W0:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W0 @ xT ) =>
% 34.10/5.48 ( sdtlseqdt0 @ W0 @ ( sdtlpdtrp0 @ xf @ xp ) ) ) ) ) )),
% 34.10/5.48 inference('cnf.neg', [status(esa)], [m__])).
% 34.10/5.48 thf(zip_derived_cl121, plain,
% 34.10/5.48 ((~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ xp) @ sk__18)
% 34.10/5.48 | ~ (sdtlseqdt0 @ sk__19 @ (sdtlpdtrp0 @ xf @ xp)))),
% 34.10/5.48 inference('cnf', [status(esa)], [zf_stmt_0])).
% 34.10/5.48 thf(zip_derived_cl117, plain,
% 34.10/5.48 (( (aElementOf0 @ sk__18 @ xP) | (aElementOf0 @ sk__19 @ xT))),
% 34.10/5.48 inference('cnf', [status(esa)], [zf_stmt_0])).
% 34.10/5.48 thf(m__1173, axiom,
% 34.10/5.48 (( aSubsetOf0 @ xT @ xS ) &
% 34.10/5.48 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xT ) => ( aElementOf0 @ W0 @ xS ) ) ) &
% 34.10/5.48 ( aSet0 @ xT ))).
% 34.10/5.48 thf(zip_derived_cl95, plain,
% 34.10/5.48 (![X0 : $i]: ( (aElementOf0 @ X0 @ xS) | ~ (aElementOf0 @ X0 @ xT))),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1173])).
% 34.10/5.48 thf(zip_derived_cl200, plain,
% 34.10/5.48 (( (aElementOf0 @ sk__18 @ xP) | (aElementOf0 @ sk__19 @ xS))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl117, zip_derived_cl95])).
% 34.10/5.48 thf(m__1144, axiom,
% 34.10/5.48 (( ( xS ) = ( cS1142 @ xf ) ) &
% 34.10/5.48 ( ![W0:$i]:
% 34.10/5.48 ( ( ( ( ( aElementOf0 @ W0 @ ( szDzozmdt0 @ xf ) ) &
% 34.10/5.48 ( ( sdtlpdtrp0 @ xf @ W0 ) = ( W0 ) ) ) |
% 34.10/5.48 ( aFixedPointOf0 @ W0 @ xf ) ) =>
% 34.10/5.48 ( aElementOf0 @ W0 @ xS ) ) &
% 34.10/5.48 ( ( aElementOf0 @ W0 @ xS ) =>
% 34.10/5.48 ( ( aElementOf0 @ W0 @ ( szDzozmdt0 @ xf ) ) &
% 34.10/5.48 ( ( sdtlpdtrp0 @ xf @ W0 ) = ( W0 ) ) &
% 34.10/5.48 ( aFixedPointOf0 @ W0 @ xf ) ) ) ) ) &
% 34.10/5.48 ( aSet0 @ xS ))).
% 34.10/5.48 thf(zip_derived_cl90, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 ( (aElementOf0 @ X0 @ (szDzozmdt0 @ xf)) | ~ (aElementOf0 @ X0 @ xS))),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1144])).
% 34.10/5.48 thf(m__1123, axiom,
% 34.10/5.48 (( aSet0 @ xU ) &
% 34.10/5.48 ( ![W0:$i]:
% 34.10/5.48 ( ( ( aSubsetOf0 @ W0 @ xU ) |
% 34.10/5.48 ( ( ![W1:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W1 @ W0 ) => ( aElementOf0 @ W1 @ xU ) ) ) &
% 34.10/5.48 ( aSet0 @ W0 ) ) ) =>
% 34.10/5.48 ( ?[W1:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W1 @ xU ) & ( aElementOf0 @ W1 @ xU ) &
% 34.10/5.48 ( ![W2:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W2 @ W0 ) => ( sdtlseqdt0 @ W1 @ W2 ) ) ) &
% 34.10/5.48 ( aLowerBoundOfIn0 @ W1 @ W0 @ xU ) &
% 34.10/5.48 ( ![W2:$i]:
% 34.10/5.48 ( ( ( aLowerBoundOfIn0 @ W2 @ W0 @ xU ) |
% 34.10/5.48 ( ( ![W3:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W3 @ W0 ) => ( sdtlseqdt0 @ W2 @ W3 ) ) ) &
% 34.10/5.48 ( aElementOf0 @ W2 @ xU ) ) ) =>
% 34.10/5.48 ( sdtlseqdt0 @ W2 @ W1 ) ) ) &
% 34.10/5.48 ( aInfimumOfIn0 @ W1 @ W0 @ xU ) &
% 34.10/5.48 ( ?[W2:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W2 @ xU ) & ( aElementOf0 @ W2 @ xU ) &
% 34.10/5.48 ( ![W3:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W3 @ W0 ) => ( sdtlseqdt0 @ W3 @ W2 ) ) ) &
% 34.10/5.48 ( aUpperBoundOfIn0 @ W2 @ W0 @ xU ) &
% 34.10/5.48 ( ![W3:$i]:
% 34.10/5.48 ( ( ( aUpperBoundOfIn0 @ W3 @ W0 @ xU ) |
% 34.10/5.48 ( ( ![W4:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W4 @ W0 ) =>
% 34.10/5.48 ( sdtlseqdt0 @ W4 @ W3 ) ) ) &
% 34.10/5.48 ( aElementOf0 @ W3 @ xU ) ) ) =>
% 34.10/5.48 ( sdtlseqdt0 @ W2 @ W3 ) ) ) &
% 34.10/5.48 ( aSupremumOfIn0 @ W2 @ W0 @ xU ) ) ) ) ) ) ) &
% 34.10/5.48 ( aCompleteLattice0 @ xU ) & ( aFunction0 @ xf ) &
% 34.10/5.48 ( ![W0:$i,W1:$i]:
% 34.10/5.48 ( ( ( aElementOf0 @ W1 @ ( szDzozmdt0 @ xf ) ) &
% 34.10/5.48 ( aElementOf0 @ W0 @ ( szDzozmdt0 @ xf ) ) ) =>
% 34.10/5.48 ( ( sdtlseqdt0 @ W0 @ W1 ) =>
% 34.10/5.48 ( sdtlseqdt0 @ ( sdtlpdtrp0 @ xf @ W0 ) @ ( sdtlpdtrp0 @ xf @ W1 ) ) ) ) ) &
% 34.10/5.48 ( isMonotone0 @ xf ) & ( ( szDzozmdt0 @ xf ) = ( szRzazndt0 @ xf ) ) &
% 34.10/5.48 ( ( szRzazndt0 @ xf ) = ( xU ) ) & ( isOn0 @ xf @ xU ))).
% 34.10/5.48 thf(zf_stmt_1, type, zip_tseitin_7 : $i > $i > $o).
% 34.10/5.48 thf(zf_stmt_2, axiom,
% 34.10/5.48 (![W1:$i,W0:$i]:
% 34.10/5.48 ( ( zip_tseitin_7 @ W1 @ W0 ) =>
% 34.10/5.48 ( ( ?[W2:$i]: ( zip_tseitin_6 @ W2 @ W0 ) ) &
% 34.10/5.48 ( aInfimumOfIn0 @ W1 @ W0 @ xU ) &
% 34.10/5.48 ( ![W2:$i]:
% 34.10/5.48 ( ( zip_tseitin_3 @ W2 @ W0 ) => ( sdtlseqdt0 @ W2 @ W1 ) ) ) &
% 34.10/5.48 ( aLowerBoundOfIn0 @ W1 @ W0 @ xU ) &
% 34.10/5.48 ( ![W2:$i]: ( ( aElementOf0 @ W2 @ W0 ) => ( sdtlseqdt0 @ W1 @ W2 ) ) ) &
% 34.10/5.48 ( aElementOf0 @ W1 @ xU ) & ( aElementOf0 @ W1 @ xU ) ) ))).
% 34.10/5.48 thf(zf_stmt_3, type, zip_tseitin_6 : $i > $i > $o).
% 34.10/5.48 thf(zf_stmt_4, axiom,
% 34.10/5.48 (![W2:$i,W0:$i]:
% 34.10/5.48 ( ( zip_tseitin_6 @ W2 @ W0 ) =>
% 34.10/5.48 ( ( aSupremumOfIn0 @ W2 @ W0 @ xU ) &
% 34.10/5.48 ( ![W3:$i]:
% 34.10/5.48 ( ( zip_tseitin_5 @ W3 @ W0 ) => ( sdtlseqdt0 @ W2 @ W3 ) ) ) &
% 34.10/5.48 ( aUpperBoundOfIn0 @ W2 @ W0 @ xU ) &
% 34.10/5.48 ( ![W3:$i]: ( ( aElementOf0 @ W3 @ W0 ) => ( sdtlseqdt0 @ W3 @ W2 ) ) ) &
% 34.10/5.48 ( aElementOf0 @ W2 @ xU ) & ( aElementOf0 @ W2 @ xU ) ) ))).
% 34.10/5.48 thf(zf_stmt_5, type, zip_tseitin_5 : $i > $i > $o).
% 34.10/5.48 thf(zf_stmt_6, axiom,
% 34.10/5.48 (![W3:$i,W0:$i]:
% 34.10/5.48 ( ( ( ( aElementOf0 @ W3 @ xU ) &
% 34.10/5.48 ( ![W4:$i]: ( zip_tseitin_4 @ W4 @ W3 @ W0 ) ) ) |
% 34.10/5.48 ( aUpperBoundOfIn0 @ W3 @ W0 @ xU ) ) =>
% 34.10/5.48 ( zip_tseitin_5 @ W3 @ W0 ) ))).
% 34.10/5.48 thf(zf_stmt_7, type, zip_tseitin_4 : $i > $i > $i > $o).
% 34.10/5.48 thf(zf_stmt_8, axiom,
% 34.10/5.48 (![W4:$i,W3:$i,W0:$i]:
% 34.10/5.48 ( ( ( aElementOf0 @ W4 @ W0 ) => ( sdtlseqdt0 @ W4 @ W3 ) ) =>
% 34.10/5.48 ( zip_tseitin_4 @ W4 @ W3 @ W0 ) ))).
% 34.10/5.48 thf(zf_stmt_9, type, zip_tseitin_3 : $i > $i > $o).
% 34.10/5.48 thf(zf_stmt_10, axiom,
% 34.10/5.48 (![W2:$i,W0:$i]:
% 34.10/5.48 ( ( ( ( aElementOf0 @ W2 @ xU ) &
% 34.10/5.48 ( ![W3:$i]: ( zip_tseitin_2 @ W3 @ W2 @ W0 ) ) ) |
% 34.10/5.48 ( aLowerBoundOfIn0 @ W2 @ W0 @ xU ) ) =>
% 34.10/5.48 ( zip_tseitin_3 @ W2 @ W0 ) ))).
% 34.10/5.48 thf(zf_stmt_11, type, zip_tseitin_2 : $i > $i > $i > $o).
% 34.10/5.48 thf(zf_stmt_12, axiom,
% 34.10/5.48 (![W3:$i,W2:$i,W0:$i]:
% 34.10/5.48 ( ( ( aElementOf0 @ W3 @ W0 ) => ( sdtlseqdt0 @ W2 @ W3 ) ) =>
% 34.10/5.48 ( zip_tseitin_2 @ W3 @ W2 @ W0 ) ))).
% 34.10/5.48 thf(zf_stmt_13, type, zip_tseitin_1 : $i > $o).
% 34.10/5.48 thf(zf_stmt_14, axiom,
% 34.10/5.48 (![W0:$i]:
% 34.10/5.48 ( ( ( ( aSet0 @ W0 ) & ( ![W1:$i]: ( zip_tseitin_0 @ W1 @ W0 ) ) ) |
% 34.10/5.48 ( aSubsetOf0 @ W0 @ xU ) ) =>
% 34.10/5.48 ( zip_tseitin_1 @ W0 ) ))).
% 34.10/5.48 thf(zf_stmt_15, type, zip_tseitin_0 : $i > $i > $o).
% 34.10/5.48 thf(zf_stmt_16, axiom,
% 34.10/5.48 (![W1:$i,W0:$i]:
% 34.10/5.48 ( ( ( aElementOf0 @ W1 @ W0 ) => ( aElementOf0 @ W1 @ xU ) ) =>
% 34.10/5.48 ( zip_tseitin_0 @ W1 @ W0 ) ))).
% 34.10/5.48 thf(zf_stmt_17, axiom,
% 34.10/5.48 (( isOn0 @ xf @ xU ) & ( ( szRzazndt0 @ xf ) = ( xU ) ) &
% 34.10/5.48 ( ( szDzozmdt0 @ xf ) = ( szRzazndt0 @ xf ) ) & ( isMonotone0 @ xf ) &
% 34.10/5.48 ( ![W0:$i,W1:$i]:
% 34.10/5.48 ( ( ( aElementOf0 @ W0 @ ( szDzozmdt0 @ xf ) ) &
% 34.10/5.48 ( aElementOf0 @ W1 @ ( szDzozmdt0 @ xf ) ) ) =>
% 34.10/5.48 ( ( sdtlseqdt0 @ W0 @ W1 ) =>
% 34.10/5.48 ( sdtlseqdt0 @ ( sdtlpdtrp0 @ xf @ W0 ) @ ( sdtlpdtrp0 @ xf @ W1 ) ) ) ) ) &
% 34.10/5.48 ( aFunction0 @ xf ) & ( aCompleteLattice0 @ xU ) &
% 34.10/5.48 ( ![W0:$i]:
% 34.10/5.48 ( ( zip_tseitin_1 @ W0 ) => ( ?[W1:$i]: ( zip_tseitin_7 @ W1 @ W0 ) ) ) ) &
% 34.10/5.48 ( aSet0 @ xU ))).
% 34.10/5.48 thf(zip_derived_cl84, plain, (((szDzozmdt0 @ xf) = (szRzazndt0 @ xf))),
% 34.10/5.48 inference('cnf', [status(esa)], [zf_stmt_17])).
% 34.10/5.48 thf(zip_derived_cl85, plain, (((szRzazndt0 @ xf) = (xU))),
% 34.10/5.48 inference('cnf', [status(esa)], [zf_stmt_17])).
% 34.10/5.48 thf(zip_derived_cl122, plain, (((szDzozmdt0 @ xf) = (xU))),
% 34.10/5.48 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 34.10/5.48 thf(zip_derived_cl123, plain,
% 34.10/5.48 (![X0 : $i]: ( (aElementOf0 @ X0 @ xU) | ~ (aElementOf0 @ X0 @ xS))),
% 34.10/5.48 inference('demod', [status(thm)], [zip_derived_cl90, zip_derived_cl122])).
% 34.10/5.48 thf(zip_derived_cl224, plain,
% 34.10/5.48 (( (aElementOf0 @ sk__18 @ xP) | (aElementOf0 @ sk__19 @ xU))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl200, zip_derived_cl123])).
% 34.10/5.48 thf(m__1261, axiom,
% 34.10/5.48 (( aInfimumOfIn0 @ xp @ xP @ xU ) & ( aElementOf0 @ xp @ xU ) &
% 34.10/5.48 ( aLowerBoundOfIn0 @ xp @ xP @ xU ) &
% 34.10/5.48 ( ![W0:$i]:
% 34.10/5.48 ( ( ( ( aElementOf0 @ W0 @ xU ) &
% 34.10/5.48 ( ![W1:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W1 @ xP ) => ( sdtlseqdt0 @ W0 @ W1 ) ) ) ) |
% 34.10/5.48 ( aLowerBoundOfIn0 @ W0 @ xP @ xU ) ) =>
% 34.10/5.48 ( sdtlseqdt0 @ W0 @ xp ) ) ) &
% 34.10/5.48 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xP ) => ( sdtlseqdt0 @ xp @ W0 ) ) ))).
% 34.10/5.48 thf(zip_derived_cl107, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 ( (sdtlseqdt0 @ X0 @ xp)
% 34.10/5.48 | ~ (aElementOf0 @ X0 @ xU)
% 34.10/5.48 | (aElementOf0 @ (sk__17 @ X0) @ xP))),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1261])).
% 34.10/5.48 thf(zip_derived_cl707, plain,
% 34.10/5.48 (( (aElementOf0 @ sk__18 @ xP)
% 34.10/5.48 | (sdtlseqdt0 @ sk__19 @ xp)
% 34.10/5.48 | (aElementOf0 @ (sk__17 @ sk__19) @ xP))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl224, zip_derived_cl107])).
% 34.10/5.48 thf(zip_derived_cl117, plain,
% 34.10/5.48 (( (aElementOf0 @ sk__18 @ xP) | (aElementOf0 @ sk__19 @ xT))),
% 34.10/5.48 inference('cnf', [status(esa)], [zf_stmt_0])).
% 34.10/5.48 thf(m__1244, axiom,
% 34.10/5.48 (( ( xP ) = ( cS1241 @ xU @ xf @ xT ) ) &
% 34.10/5.48 ( ![W0:$i]:
% 34.10/5.48 ( ( ( ( aElementOf0 @ W0 @ xU ) &
% 34.10/5.48 ( sdtlseqdt0 @ ( sdtlpdtrp0 @ xf @ W0 ) @ W0 ) &
% 34.10/5.48 ( ( ![W1:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W1 @ xT ) => ( sdtlseqdt0 @ W1 @ W0 ) ) ) |
% 34.10/5.48 ( aUpperBoundOfIn0 @ W0 @ xT @ xU ) ) ) =>
% 34.10/5.48 ( aElementOf0 @ W0 @ xP ) ) &
% 34.10/5.48 ( ( aElementOf0 @ W0 @ xP ) =>
% 34.10/5.48 ( ( aElementOf0 @ W0 @ xU ) &
% 34.10/5.48 ( sdtlseqdt0 @ ( sdtlpdtrp0 @ xf @ W0 ) @ W0 ) &
% 34.10/5.48 ( ![W1:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W1 @ xT ) => ( sdtlseqdt0 @ W1 @ W0 ) ) ) &
% 34.10/5.48 ( aUpperBoundOfIn0 @ W0 @ xT @ xU ) ) ) ) ) &
% 34.10/5.48 ( aSet0 @ xP ))).
% 34.10/5.48 thf(zip_derived_cl103, plain,
% 34.10/5.48 (![X0 : $i, X1 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ xT)
% 34.10/5.48 | (sdtlseqdt0 @ X0 @ X1)
% 34.10/5.48 | ~ (aElementOf0 @ X1 @ xP))),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1244])).
% 34.10/5.48 thf(zip_derived_cl287, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 ( (aElementOf0 @ sk__18 @ xP)
% 34.10/5.48 | (sdtlseqdt0 @ sk__19 @ X0)
% 34.10/5.48 | ~ (aElementOf0 @ X0 @ xP))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl117, zip_derived_cl103])).
% 34.10/5.48 thf(zip_derived_cl805, plain,
% 34.10/5.48 (( (sdtlseqdt0 @ sk__19 @ xp)
% 34.10/5.48 | (aElementOf0 @ sk__18 @ xP)
% 34.10/5.48 | (aElementOf0 @ sk__18 @ xP)
% 34.10/5.48 | (sdtlseqdt0 @ sk__19 @ (sk__17 @ sk__19)))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl707, zip_derived_cl287])).
% 34.10/5.48 thf(zip_derived_cl808, plain,
% 34.10/5.48 (( (sdtlseqdt0 @ sk__19 @ (sk__17 @ sk__19))
% 34.10/5.48 | (aElementOf0 @ sk__18 @ xP)
% 34.10/5.48 | (sdtlseqdt0 @ sk__19 @ xp))),
% 34.10/5.48 inference('simplify', [status(thm)], [zip_derived_cl805])).
% 34.10/5.48 thf(zip_derived_cl224, plain,
% 34.10/5.48 (( (aElementOf0 @ sk__18 @ xP) | (aElementOf0 @ sk__19 @ xU))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl200, zip_derived_cl123])).
% 34.10/5.48 thf(zip_derived_cl108, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 ( (sdtlseqdt0 @ X0 @ xp)
% 34.10/5.48 | ~ (aElementOf0 @ X0 @ xU)
% 34.10/5.48 | ~ (sdtlseqdt0 @ X0 @ (sk__17 @ X0)))),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1261])).
% 34.10/5.48 thf(zip_derived_cl323, plain,
% 34.10/5.48 (( (aElementOf0 @ sk__18 @ xP)
% 34.10/5.48 | (sdtlseqdt0 @ sk__19 @ xp)
% 34.10/5.48 | ~ (sdtlseqdt0 @ sk__19 @ (sk__17 @ sk__19)))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl224, zip_derived_cl108])).
% 34.10/5.48 thf(zip_derived_cl870, plain,
% 34.10/5.48 (( (sdtlseqdt0 @ sk__19 @ xp) | (aElementOf0 @ sk__18 @ xP))),
% 34.10/5.48 inference('clc', [status(thm)], [zip_derived_cl808, zip_derived_cl323])).
% 34.10/5.48 thf(zip_derived_cl200, plain,
% 34.10/5.48 (( (aElementOf0 @ sk__18 @ xP) | (aElementOf0 @ sk__19 @ xS))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl117, zip_derived_cl95])).
% 34.10/5.48 thf(zip_derived_cl91, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 (((sdtlpdtrp0 @ xf @ X0) = (X0)) | ~ (aElementOf0 @ X0 @ xS))),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1144])).
% 34.10/5.48 thf(zip_derived_cl205, plain,
% 34.10/5.48 (( (aElementOf0 @ sk__18 @ xP) | ((sdtlpdtrp0 @ xf @ sk__19) = (sk__19)))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl200, zip_derived_cl91])).
% 34.10/5.48 thf(mDefMonot, axiom,
% 34.10/5.48 (![W0:$i]:
% 34.10/5.48 ( ( aFunction0 @ W0 ) =>
% 34.10/5.48 ( ( isMonotone0 @ W0 ) <=>
% 34.10/5.48 ( ![W1:$i,W2:$i]:
% 34.10/5.48 ( ( ( aElementOf0 @ W1 @ ( szDzozmdt0 @ W0 ) ) &
% 34.10/5.48 ( aElementOf0 @ W2 @ ( szDzozmdt0 @ W0 ) ) ) =>
% 34.10/5.48 ( ( sdtlseqdt0 @ W1 @ W2 ) =>
% 34.10/5.48 ( sdtlseqdt0 @
% 34.10/5.48 ( sdtlpdtrp0 @ W0 @ W1 ) @ ( sdtlpdtrp0 @ W0 @ W2 ) ) ) ) ) ) ))).
% 34.10/5.48 thf(zip_derived_cl52, plain,
% 34.10/5.48 (![X0 : $i, X1 : $i, X2 : $i]:
% 34.10/5.48 (~ (isMonotone0 @ X0)
% 34.10/5.48 | ~ (aElementOf0 @ X1 @ (szDzozmdt0 @ X0))
% 34.10/5.48 | ~ (aElementOf0 @ X2 @ (szDzozmdt0 @ X0))
% 34.10/5.48 | (sdtlseqdt0 @ (sdtlpdtrp0 @ X0 @ X1) @ (sdtlpdtrp0 @ X0 @ X2))
% 34.10/5.48 | ~ (sdtlseqdt0 @ X1 @ X2)
% 34.10/5.48 | ~ (aFunction0 @ X0))),
% 34.10/5.48 inference('cnf', [status(esa)], [mDefMonot])).
% 34.10/5.48 thf(zip_derived_cl564, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 ( (aElementOf0 @ sk__18 @ xP)
% 34.10/5.48 | ~ (isMonotone0 @ xf)
% 34.10/5.48 | ~ (aElementOf0 @ sk__19 @ (szDzozmdt0 @ xf))
% 34.10/5.48 | ~ (aElementOf0 @ X0 @ (szDzozmdt0 @ xf))
% 34.10/5.48 | (sdtlseqdt0 @ sk__19 @ (sdtlpdtrp0 @ xf @ X0))
% 34.10/5.48 | ~ (sdtlseqdt0 @ sk__19 @ X0)
% 34.10/5.48 | ~ (aFunction0 @ xf))),
% 34.10/5.48 inference('s_sup+', [status(thm)], [zip_derived_cl205, zip_derived_cl52])).
% 34.10/5.48 thf(zip_derived_cl83, plain, ( (isMonotone0 @ xf)),
% 34.10/5.48 inference('cnf', [status(esa)], [zf_stmt_17])).
% 34.10/5.48 thf(zip_derived_cl122, plain, (((szDzozmdt0 @ xf) = (xU))),
% 34.10/5.48 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 34.10/5.48 thf(zip_derived_cl122, plain, (((szDzozmdt0 @ xf) = (xU))),
% 34.10/5.48 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 34.10/5.48 thf(zip_derived_cl81, plain, ( (aFunction0 @ xf)),
% 34.10/5.48 inference('cnf', [status(esa)], [zf_stmt_17])).
% 34.10/5.48 thf(zip_derived_cl571, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 ( (aElementOf0 @ sk__18 @ xP)
% 34.10/5.48 | ~ (aElementOf0 @ sk__19 @ xU)
% 34.10/5.48 | ~ (aElementOf0 @ X0 @ xU)
% 34.10/5.48 | (sdtlseqdt0 @ sk__19 @ (sdtlpdtrp0 @ xf @ X0))
% 34.10/5.48 | ~ (sdtlseqdt0 @ sk__19 @ X0))),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl564, zip_derived_cl83, zip_derived_cl122,
% 34.10/5.48 zip_derived_cl122, zip_derived_cl81])).
% 34.10/5.48 thf(zip_derived_cl224, plain,
% 34.10/5.48 (( (aElementOf0 @ sk__18 @ xP) | (aElementOf0 @ sk__19 @ xU))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl200, zip_derived_cl123])).
% 34.10/5.48 thf(zip_derived_cl8495, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 (~ (sdtlseqdt0 @ sk__19 @ X0)
% 34.10/5.48 | (sdtlseqdt0 @ sk__19 @ (sdtlpdtrp0 @ xf @ X0))
% 34.10/5.48 | ~ (aElementOf0 @ X0 @ xU)
% 34.10/5.48 | (aElementOf0 @ sk__18 @ xP))),
% 34.10/5.48 inference('clc', [status(thm)], [zip_derived_cl571, zip_derived_cl224])).
% 34.10/5.48 thf(zip_derived_cl8496, plain,
% 34.10/5.48 (( (aElementOf0 @ sk__18 @ xP)
% 34.10/5.48 | (sdtlseqdt0 @ sk__19 @ (sdtlpdtrp0 @ xf @ xp))
% 34.10/5.48 | ~ (aElementOf0 @ xp @ xU)
% 34.10/5.48 | (aElementOf0 @ sk__18 @ xP))),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl870, zip_derived_cl8495])).
% 34.10/5.48 thf(zip_derived_cl111, plain, ( (aElementOf0 @ xp @ xU)),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1261])).
% 34.10/5.48 thf(zip_derived_cl8522, plain,
% 34.10/5.48 (( (aElementOf0 @ sk__18 @ xP)
% 34.10/5.48 | (sdtlseqdt0 @ sk__19 @ (sdtlpdtrp0 @ xf @ xp))
% 34.10/5.48 | (aElementOf0 @ sk__18 @ xP))),
% 34.10/5.48 inference('demod', [status(thm)], [zip_derived_cl8496, zip_derived_cl111])).
% 34.10/5.48 thf(zip_derived_cl8523, plain,
% 34.10/5.48 (( (sdtlseqdt0 @ sk__19 @ (sdtlpdtrp0 @ xf @ xp))
% 34.10/5.48 | (aElementOf0 @ sk__18 @ xP))),
% 34.10/5.48 inference('simplify', [status(thm)], [zip_derived_cl8522])).
% 34.10/5.48 thf(zip_derived_cl118, plain,
% 34.10/5.48 (( (aElementOf0 @ sk__18 @ xP)
% 34.10/5.48 | ~ (sdtlseqdt0 @ sk__19 @ (sdtlpdtrp0 @ xf @ xp)))),
% 34.10/5.48 inference('cnf', [status(esa)], [zf_stmt_0])).
% 34.10/5.48 thf(zip_derived_cl8547, plain, ( (aElementOf0 @ sk__18 @ xP)),
% 34.10/5.48 inference('clc', [status(thm)], [zip_derived_cl8523, zip_derived_cl118])).
% 34.10/5.48 thf(zip_derived_cl102, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 ( (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ X0) @ X0)
% 34.10/5.48 | ~ (aElementOf0 @ X0 @ xP))),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1244])).
% 34.10/5.48 thf(zip_derived_cl8558, plain,
% 34.10/5.48 ( (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ sk__18) @ sk__18)),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl8547, zip_derived_cl102])).
% 34.10/5.48 thf(zip_derived_cl8547, plain, ( (aElementOf0 @ sk__18 @ xP)),
% 34.10/5.48 inference('clc', [status(thm)], [zip_derived_cl8523, zip_derived_cl118])).
% 34.10/5.48 thf(zip_derived_cl101, plain,
% 34.10/5.48 (![X0 : $i]: ( (aElementOf0 @ X0 @ xU) | ~ (aElementOf0 @ X0 @ xP))),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1244])).
% 34.10/5.48 thf(zip_derived_cl8557, plain, ( (aElementOf0 @ sk__18 @ xU)),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl8547, zip_derived_cl101])).
% 34.10/5.48 thf(zip_derived_cl111, plain, ( (aElementOf0 @ xp @ xU)),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1261])).
% 34.10/5.48 thf(zip_derived_cl82, plain,
% 34.10/5.48 (![X0 : $i, X1 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ (szDzozmdt0 @ xf))
% 34.10/5.48 | ~ (aElementOf0 @ X1 @ (szDzozmdt0 @ xf))
% 34.10/5.48 | (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ X0) @ (sdtlpdtrp0 @ xf @ X1))
% 34.10/5.48 | ~ (sdtlseqdt0 @ X0 @ X1))),
% 34.10/5.48 inference('cnf', [status(esa)], [zf_stmt_17])).
% 34.10/5.48 thf(zip_derived_cl122, plain, (((szDzozmdt0 @ xf) = (xU))),
% 34.10/5.48 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 34.10/5.48 thf(zip_derived_cl122, plain, (((szDzozmdt0 @ xf) = (xU))),
% 34.10/5.48 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 34.10/5.48 thf(zip_derived_cl125, plain,
% 34.10/5.48 (![X0 : $i, X1 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ xU)
% 34.10/5.48 | ~ (aElementOf0 @ X1 @ xU)
% 34.10/5.48 | (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ X0) @ (sdtlpdtrp0 @ xf @ X1))
% 34.10/5.48 | ~ (sdtlseqdt0 @ X0 @ X1))),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl82, zip_derived_cl122, zip_derived_cl122])).
% 34.10/5.48 thf(zip_derived_cl741, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ xU)
% 34.10/5.48 | (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ xp) @ (sdtlpdtrp0 @ xf @ X0))
% 34.10/5.48 | ~ (sdtlseqdt0 @ xp @ X0))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl111, zip_derived_cl125])).
% 34.10/5.48 thf(zip_derived_cl14529, plain,
% 34.10/5.48 (( (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ xp) @ (sdtlpdtrp0 @ xf @ sk__18))
% 34.10/5.48 | ~ (sdtlseqdt0 @ xp @ sk__18))),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl8557, zip_derived_cl741])).
% 34.10/5.48 thf(zip_derived_cl8547, plain, ( (aElementOf0 @ sk__18 @ xP)),
% 34.10/5.48 inference('clc', [status(thm)], [zip_derived_cl8523, zip_derived_cl118])).
% 34.10/5.48 thf(zip_derived_cl106, plain,
% 34.10/5.48 (![X0 : $i]: ( (sdtlseqdt0 @ xp @ X0) | ~ (aElementOf0 @ X0 @ xP))),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1261])).
% 34.10/5.48 thf(zip_derived_cl8560, plain, ( (sdtlseqdt0 @ xp @ sk__18)),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl8547, zip_derived_cl106])).
% 34.10/5.48 thf(zip_derived_cl14541, plain,
% 34.10/5.48 ( (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ xp) @ (sdtlpdtrp0 @ xf @ sk__18))),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl14529, zip_derived_cl8560])).
% 34.10/5.48 thf(mTrans, axiom,
% 34.10/5.48 (![W0:$i,W1:$i,W2:$i]:
% 34.10/5.48 ( ( ( aElement0 @ W0 ) & ( aElement0 @ W1 ) & ( aElement0 @ W2 ) ) =>
% 34.10/5.48 ( ( ( sdtlseqdt0 @ W0 @ W1 ) & ( sdtlseqdt0 @ W1 @ W2 ) ) =>
% 34.10/5.48 ( sdtlseqdt0 @ W0 @ W2 ) ) ))).
% 34.10/5.48 thf(zip_derived_cl12, plain,
% 34.10/5.48 (![X0 : $i, X1 : $i, X2 : $i]:
% 34.10/5.48 (~ (sdtlseqdt0 @ X0 @ X1)
% 34.10/5.48 | ~ (aElement0 @ X1)
% 34.10/5.48 | ~ (aElement0 @ X0)
% 34.10/5.48 | ~ (aElement0 @ X2)
% 34.10/5.48 | (sdtlseqdt0 @ X0 @ X2)
% 34.10/5.48 | ~ (sdtlseqdt0 @ X1 @ X2))),
% 34.10/5.48 inference('cnf', [status(esa)], [mTrans])).
% 34.10/5.48 thf(zip_derived_cl14547, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 (~ (aElement0 @ (sdtlpdtrp0 @ xf @ sk__18))
% 34.10/5.48 | ~ (aElement0 @ (sdtlpdtrp0 @ xf @ xp))
% 34.10/5.48 | ~ (aElement0 @ X0)
% 34.10/5.48 | (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ xp) @ X0)
% 34.10/5.48 | ~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ sk__18) @ X0))),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl14541, zip_derived_cl12])).
% 34.10/5.48 thf(zip_derived_cl8557, plain, ( (aElementOf0 @ sk__18 @ xU)),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl8547, zip_derived_cl101])).
% 34.10/5.48 thf(zip_derived_cl122, plain, (((szDzozmdt0 @ xf) = (xU))),
% 34.10/5.48 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl85])).
% 34.10/5.48 thf(mImgSort, axiom,
% 34.10/5.48 (![W0:$i]:
% 34.10/5.48 ( ( aFunction0 @ W0 ) =>
% 34.10/5.48 ( ![W1:$i]:
% 34.10/5.48 ( ( aElementOf0 @ W1 @ ( szDzozmdt0 @ W0 ) ) =>
% 34.10/5.48 ( aElementOf0 @ ( sdtlpdtrp0 @ W0 @ W1 ) @ ( szRzazndt0 @ W0 ) ) ) ) ))).
% 34.10/5.48 thf(zip_derived_cl44, plain,
% 34.10/5.48 (![X0 : $i, X1 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ (szDzozmdt0 @ X1))
% 34.10/5.48 | (aElementOf0 @ (sdtlpdtrp0 @ X1 @ X0) @ (szRzazndt0 @ X1))
% 34.10/5.48 | ~ (aFunction0 @ X1))),
% 34.10/5.48 inference('cnf', [status(esa)], [mImgSort])).
% 34.10/5.48 thf(zip_derived_cl500, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ xU)
% 34.10/5.48 | (aElementOf0 @ (sdtlpdtrp0 @ xf @ X0) @ (szRzazndt0 @ xf))
% 34.10/5.48 | ~ (aFunction0 @ xf))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl122, zip_derived_cl44])).
% 34.10/5.48 thf(zip_derived_cl85, plain, (((szRzazndt0 @ xf) = (xU))),
% 34.10/5.48 inference('cnf', [status(esa)], [zf_stmt_17])).
% 34.10/5.48 thf(zip_derived_cl81, plain, ( (aFunction0 @ xf)),
% 34.10/5.48 inference('cnf', [status(esa)], [zf_stmt_17])).
% 34.10/5.48 thf(zip_derived_cl506, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ xU)
% 34.10/5.48 | (aElementOf0 @ (sdtlpdtrp0 @ xf @ X0) @ xU))),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl500, zip_derived_cl85, zip_derived_cl81])).
% 34.10/5.48 thf(zip_derived_cl8629, plain,
% 34.10/5.48 ( (aElementOf0 @ (sdtlpdtrp0 @ xf @ sk__18) @ xU)),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl8557, zip_derived_cl506])).
% 34.10/5.48 thf(mEOfElem, axiom,
% 34.10/5.48 (![W0:$i]:
% 34.10/5.48 ( ( aSet0 @ W0 ) =>
% 34.10/5.48 ( ![W1:$i]: ( ( aElementOf0 @ W1 @ W0 ) => ( aElement0 @ W1 ) ) ) ))).
% 34.10/5.48 thf(zip_derived_cl2, plain,
% 34.10/5.48 (![X0 : $i, X1 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ X1) | (aElement0 @ X0) | ~ (aSet0 @ X1))),
% 34.10/5.48 inference('cnf', [status(esa)], [mEOfElem])).
% 34.10/5.48 thf(zip_derived_cl8754, plain,
% 34.10/5.48 (( (aElement0 @ (sdtlpdtrp0 @ xf @ sk__18)) | ~ (aSet0 @ xU))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl8629, zip_derived_cl2])).
% 34.10/5.48 thf(zip_derived_cl78, plain, ( (aSet0 @ xU)),
% 34.10/5.48 inference('cnf', [status(esa)], [zf_stmt_17])).
% 34.10/5.48 thf(zip_derived_cl8774, plain, ( (aElement0 @ (sdtlpdtrp0 @ xf @ sk__18))),
% 34.10/5.48 inference('demod', [status(thm)], [zip_derived_cl8754, zip_derived_cl78])).
% 34.10/5.48 thf(zip_derived_cl111, plain, ( (aElementOf0 @ xp @ xU)),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1261])).
% 34.10/5.48 thf(zip_derived_cl506, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ xU)
% 34.10/5.48 | (aElementOf0 @ (sdtlpdtrp0 @ xf @ X0) @ xU))),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl500, zip_derived_cl85, zip_derived_cl81])).
% 34.10/5.48 thf(zip_derived_cl516, plain, ( (aElementOf0 @ (sdtlpdtrp0 @ xf @ xp) @ xU)),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl111, zip_derived_cl506])).
% 34.10/5.48 thf(zip_derived_cl2, plain,
% 34.10/5.48 (![X0 : $i, X1 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ X1) | (aElement0 @ X0) | ~ (aSet0 @ X1))),
% 34.10/5.48 inference('cnf', [status(esa)], [mEOfElem])).
% 34.10/5.48 thf(zip_derived_cl528, plain,
% 34.10/5.48 (( (aElement0 @ (sdtlpdtrp0 @ xf @ xp)) | ~ (aSet0 @ xU))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl516, zip_derived_cl2])).
% 34.10/5.48 thf(zip_derived_cl78, plain, ( (aSet0 @ xU)),
% 34.10/5.48 inference('cnf', [status(esa)], [zf_stmt_17])).
% 34.10/5.48 thf(zip_derived_cl540, plain, ( (aElement0 @ (sdtlpdtrp0 @ xf @ xp))),
% 34.10/5.48 inference('demod', [status(thm)], [zip_derived_cl528, zip_derived_cl78])).
% 34.10/5.48 thf(zip_derived_cl14550, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 (~ (aElement0 @ X0)
% 34.10/5.48 | (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ xp) @ X0)
% 34.10/5.48 | ~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ sk__18) @ X0))),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl14547, zip_derived_cl8774, zip_derived_cl540])).
% 34.10/5.48 thf(zip_derived_cl16036, plain,
% 34.10/5.48 ((~ (aElement0 @ sk__18)
% 34.10/5.48 | (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ xp) @ sk__18))),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl8558, zip_derived_cl14550])).
% 34.10/5.48 thf(zip_derived_cl8547, plain, ( (aElementOf0 @ sk__18 @ xP)),
% 34.10/5.48 inference('clc', [status(thm)], [zip_derived_cl8523, zip_derived_cl118])).
% 34.10/5.48 thf(zip_derived_cl2, plain,
% 34.10/5.48 (![X0 : $i, X1 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ X1) | (aElement0 @ X0) | ~ (aSet0 @ X1))),
% 34.10/5.48 inference('cnf', [status(esa)], [mEOfElem])).
% 34.10/5.48 thf(zip_derived_cl8548, plain, (( (aElement0 @ sk__18) | ~ (aSet0 @ xP))),
% 34.10/5.48 inference('s_sup-', [status(thm)], [zip_derived_cl8547, zip_derived_cl2])).
% 34.10/5.48 thf(zip_derived_cl97, plain, ( (aSet0 @ xP)),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1244])).
% 34.10/5.48 thf(zip_derived_cl8564, plain, ( (aElement0 @ sk__18)),
% 34.10/5.48 inference('demod', [status(thm)], [zip_derived_cl8548, zip_derived_cl97])).
% 34.10/5.48 thf(zip_derived_cl16042, plain,
% 34.10/5.48 ( (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ xp) @ sk__18)),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl16036, zip_derived_cl8564])).
% 34.10/5.48 thf(zip_derived_cl16045, plain,
% 34.10/5.48 (~ (sdtlseqdt0 @ sk__19 @ (sdtlpdtrp0 @ xf @ xp))),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl121, zip_derived_cl16042])).
% 34.10/5.48 thf(zip_derived_cl111, plain, ( (aElementOf0 @ xp @ xU)),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1261])).
% 34.10/5.48 thf(zip_derived_cl120, plain,
% 34.10/5.48 ((~ (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ xp) @ sk__18)
% 34.10/5.48 | (aElementOf0 @ sk__19 @ xT))),
% 34.10/5.48 inference('cnf', [status(esa)], [zf_stmt_0])).
% 34.10/5.48 thf(zip_derived_cl16042, plain,
% 34.10/5.48 ( (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ xp) @ sk__18)),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl16036, zip_derived_cl8564])).
% 34.10/5.48 thf(zip_derived_cl16044, plain, ( (aElementOf0 @ sk__19 @ xT)),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl120, zip_derived_cl16042])).
% 34.10/5.48 thf(zip_derived_cl95, plain,
% 34.10/5.48 (![X0 : $i]: ( (aElementOf0 @ X0 @ xS) | ~ (aElementOf0 @ X0 @ xT))),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1173])).
% 34.10/5.48 thf(zip_derived_cl16061, plain, ( (aElementOf0 @ sk__19 @ xS)),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl16044, zip_derived_cl95])).
% 34.10/5.48 thf(zip_derived_cl123, plain,
% 34.10/5.48 (![X0 : $i]: ( (aElementOf0 @ X0 @ xU) | ~ (aElementOf0 @ X0 @ xS))),
% 34.10/5.48 inference('demod', [status(thm)], [zip_derived_cl90, zip_derived_cl122])).
% 34.10/5.48 thf(zip_derived_cl16159, plain, ( (aElementOf0 @ sk__19 @ xU)),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl16061, zip_derived_cl123])).
% 34.10/5.48 thf(zip_derived_cl125, plain,
% 34.10/5.48 (![X0 : $i, X1 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ xU)
% 34.10/5.48 | ~ (aElementOf0 @ X1 @ xU)
% 34.10/5.48 | (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ X0) @ (sdtlpdtrp0 @ xf @ X1))
% 34.10/5.48 | ~ (sdtlseqdt0 @ X0 @ X1))),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl82, zip_derived_cl122, zip_derived_cl122])).
% 34.10/5.48 thf(zip_derived_cl16235, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ xU)
% 34.10/5.48 | (sdtlseqdt0 @ (sdtlpdtrp0 @ xf @ sk__19) @ (sdtlpdtrp0 @ xf @ X0))
% 34.10/5.48 | ~ (sdtlseqdt0 @ sk__19 @ X0))),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl16159, zip_derived_cl125])).
% 34.10/5.48 thf(zip_derived_cl16061, plain, ( (aElementOf0 @ sk__19 @ xS)),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl16044, zip_derived_cl95])).
% 34.10/5.48 thf(zip_derived_cl91, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 (((sdtlpdtrp0 @ xf @ X0) = (X0)) | ~ (aElementOf0 @ X0 @ xS))),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1144])).
% 34.10/5.48 thf(zip_derived_cl16157, plain, (((sdtlpdtrp0 @ xf @ sk__19) = (sk__19))),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl16061, zip_derived_cl91])).
% 34.10/5.48 thf(zip_derived_cl16260, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ xU)
% 34.10/5.48 | (sdtlseqdt0 @ sk__19 @ (sdtlpdtrp0 @ xf @ X0))
% 34.10/5.48 | ~ (sdtlseqdt0 @ sk__19 @ X0))),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl16235, zip_derived_cl16157])).
% 34.10/5.48 thf(zip_derived_cl22841, plain,
% 34.10/5.48 (( (sdtlseqdt0 @ sk__19 @ (sdtlpdtrp0 @ xf @ xp))
% 34.10/5.48 | ~ (sdtlseqdt0 @ sk__19 @ xp))),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl111, zip_derived_cl16260])).
% 34.10/5.48 thf(zip_derived_cl16159, plain, ( (aElementOf0 @ sk__19 @ xU)),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl16061, zip_derived_cl123])).
% 34.10/5.48 thf(zip_derived_cl107, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 ( (sdtlseqdt0 @ X0 @ xp)
% 34.10/5.48 | ~ (aElementOf0 @ X0 @ xU)
% 34.10/5.48 | (aElementOf0 @ (sk__17 @ X0) @ xP))),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1261])).
% 34.10/5.48 thf(zip_derived_cl16232, plain,
% 34.10/5.48 (( (sdtlseqdt0 @ sk__19 @ xp) | (aElementOf0 @ (sk__17 @ sk__19) @ xP))),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl16159, zip_derived_cl107])).
% 34.10/5.48 thf(zip_derived_cl16044, plain, ( (aElementOf0 @ sk__19 @ xT)),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl120, zip_derived_cl16042])).
% 34.10/5.48 thf(zip_derived_cl103, plain,
% 34.10/5.48 (![X0 : $i, X1 : $i]:
% 34.10/5.48 (~ (aElementOf0 @ X0 @ xT)
% 34.10/5.48 | (sdtlseqdt0 @ X0 @ X1)
% 34.10/5.48 | ~ (aElementOf0 @ X1 @ xP))),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1244])).
% 34.10/5.48 thf(zip_derived_cl16062, plain,
% 34.10/5.48 (![X0 : $i]: ( (sdtlseqdt0 @ sk__19 @ X0) | ~ (aElementOf0 @ X0 @ xP))),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl16044, zip_derived_cl103])).
% 34.10/5.48 thf(zip_derived_cl17648, plain,
% 34.10/5.48 (( (sdtlseqdt0 @ sk__19 @ xp)
% 34.10/5.48 | (sdtlseqdt0 @ sk__19 @ (sk__17 @ sk__19)))),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl16232, zip_derived_cl16062])).
% 34.10/5.48 thf(zip_derived_cl16159, plain, ( (aElementOf0 @ sk__19 @ xU)),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl16061, zip_derived_cl123])).
% 34.10/5.48 thf(zip_derived_cl108, plain,
% 34.10/5.48 (![X0 : $i]:
% 34.10/5.48 ( (sdtlseqdt0 @ X0 @ xp)
% 34.10/5.48 | ~ (aElementOf0 @ X0 @ xU)
% 34.10/5.48 | ~ (sdtlseqdt0 @ X0 @ (sk__17 @ X0)))),
% 34.10/5.48 inference('cnf', [status(esa)], [m__1261])).
% 34.10/5.48 thf(zip_derived_cl16233, plain,
% 34.10/5.48 (( (sdtlseqdt0 @ sk__19 @ xp)
% 34.10/5.48 | ~ (sdtlseqdt0 @ sk__19 @ (sk__17 @ sk__19)))),
% 34.10/5.48 inference('s_sup-', [status(thm)],
% 34.10/5.48 [zip_derived_cl16159, zip_derived_cl108])).
% 34.10/5.48 thf(zip_derived_cl18452, plain, ( (sdtlseqdt0 @ sk__19 @ xp)),
% 34.10/5.48 inference('clc', [status(thm)],
% 34.10/5.48 [zip_derived_cl17648, zip_derived_cl16233])).
% 34.10/5.48 thf(zip_derived_cl22911, plain,
% 34.10/5.48 ( (sdtlseqdt0 @ sk__19 @ (sdtlpdtrp0 @ xf @ xp))),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl22841, zip_derived_cl18452])).
% 34.10/5.48 thf(zip_derived_cl22930, plain, ($false),
% 34.10/5.48 inference('demod', [status(thm)],
% 34.10/5.48 [zip_derived_cl16045, zip_derived_cl22911])).
% 34.10/5.48
% 34.10/5.48 % SZS output end Refutation
% 34.10/5.48
% 34.10/5.48
% 34.10/5.48 % Terminating...
% 34.70/5.58 % Runner terminated.
% 34.70/5.59 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------