%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : NUM580+3 : 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.49QHeEoDSQ 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:47:31 PM UTC 2025
% Result : Theorem 3.82s 1.23s
% Output : Refutation 3.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.26 % Problem : NUM580+3 : TPTP v9.2.0. Released v4.0.0.
% 0.11/0.27 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.49QHeEoDSQ true
% 0.13/0.49 % Computer : n024.cluster.edu
% 0.13/0.49 % Model : x86_64 x86_64
% 0.13/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.49 % Memory : 8042.1875MB
% 0.13/0.49 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.49 % CPULimit : 300
% 0.13/0.49 % WCLimit : 300
% 0.13/0.49 % DateTime : Wed Oct 1 16:41:53 EDT 2025
% 0.13/0.49 % CPUTime :
% 0.13/0.49 % Running portfolio for 300 s
% 0.13/0.49 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.49 % Number of cores: 8
% 0.13/0.49 % Python version: Python 3.6.8
% 0.13/0.49 % Running in FO mode
% 0.51/0.72 % Total configuration time : 435
% 0.51/0.72 % Estimated wc time : 1092
% 0.51/0.72 % Estimated cpu time (7 cpus) : 156.0
% 0.51/0.80 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.51/0.83 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.51/0.83 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.51/0.83 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.51/0.84 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.51/0.84 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.51/0.85 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 3.82/1.23 % Solved by fo/fo5.sh.
% 3.82/1.23 % done 598 iterations in 0.369s
% 3.82/1.23 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 3.82/1.23 % SZS output start Refutation
% 3.82/1.23 thf(aSet0_type, type, aSet0: $i > $o).
% 3.82/1.23 thf(slbdtsldtrb0_type, type, slbdtsldtrb0: $i > $i > $i).
% 3.82/1.23 thf(xi_type, type, xi: $i).
% 3.82/1.23 thf(szszuzczcdt0_type, type, szszuzczcdt0: $i > $i).
% 3.82/1.23 thf(sdtlpdtrp0_type, type, sdtlpdtrp0: $i > $i > $i).
% 3.82/1.23 thf(isCountable0_type, type, isCountable0: $i > $o).
% 3.82/1.23 thf(aElement0_type, type, aElement0: $i > $o).
% 3.82/1.23 thf(sbrdtbr0_type, type, sbrdtbr0: $i > $i).
% 3.82/1.23 thf(sdtlseqdt0_type, type, sdtlseqdt0: $i > $i > $o).
% 3.82/1.23 thf(sdtmndt0_type, type, sdtmndt0: $i > $i > $i).
% 3.82/1.23 thf(szmzizndt0_type, type, szmzizndt0: $i > $i).
% 3.82/1.23 thf(aSubsetOf0_type, type, aSubsetOf0: $i > $i > $o).
% 3.82/1.23 thf(isFinite0_type, type, isFinite0: $i > $o).
% 3.82/1.23 thf(sdtpldt0_type, type, sdtpldt0: $i > $i > $i).
% 3.82/1.23 thf(xk_type, type, xk: $i).
% 3.82/1.23 thf(xK_type, type, xK: $i).
% 3.82/1.23 thf(szNzAzT0_type, type, szNzAzT0: $i).
% 3.82/1.23 thf(xN_type, type, xN: $i).
% 3.82/1.23 thf(zip_tseitin_24_type, type, zip_tseitin_24: $i > $o).
% 3.82/1.23 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 3.82/1.23 thf(xQ_type, type, xQ: $i).
% 3.82/1.23 thf(mCardCons, axiom,
% 3.82/1.23 (![W0:$i]:
% 3.82/1.23 ( ( ( aSet0 @ W0 ) & ( isFinite0 @ W0 ) ) =>
% 3.82/1.23 ( ![W1:$i]:
% 3.82/1.23 ( ( aElement0 @ W1 ) =>
% 3.82/1.23 ( ( ~( aElementOf0 @ W1 @ W0 ) ) =>
% 3.82/1.23 ( ( sbrdtbr0 @ ( sdtpldt0 @ W0 @ W1 ) ) =
% 3.82/1.23 ( szszuzczcdt0 @ ( sbrdtbr0 @ W0 ) ) ) ) ) ) ))).
% 3.82/1.23 thf(zip_derived_cl69, plain,
% 3.82/1.23 (![X0 : $i, X1 : $i]:
% 3.82/1.23 (~ (aElement0 @ X0)
% 3.82/1.23 | ((sbrdtbr0 @ (sdtpldt0 @ X1 @ X0))
% 3.82/1.23 = (szszuzczcdt0 @ (sbrdtbr0 @ X1)))
% 3.82/1.23 | (aElementOf0 @ X0 @ X1)
% 3.82/1.23 | ~ (isFinite0 @ X1)
% 3.82/1.23 | ~ (aSet0 @ X1))),
% 3.82/1.23 inference('cnf', [status(esa)], [mCardCons])).
% 3.82/1.23 thf(m__, conjecture,
% 3.82/1.23 (( ( ![W0:$i]:
% 3.82/1.23 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) =>
% 3.82/1.23 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ W0 ) ) ) &
% 3.82/1.23 ( aElementOf0 @
% 3.82/1.23 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ ( sdtlpdtrp0 @ xN @ xi ) ) ) =>
% 3.82/1.23 ( ( ( ![W0:$i]:
% 3.82/1.23 ( ( aElementOf0 @
% 3.82/1.23 W0 @
% 3.82/1.23 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) <=>
% 3.82/1.23 ( ( ( ( W0 ) = ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) |
% 3.82/1.23 ( aElementOf0 @ W0 @ xQ ) ) &
% 3.82/1.23 ( aElement0 @ W0 ) ) ) ) &
% 3.82/1.23 ( aSet0 @
% 3.82/1.23 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) ) =>
% 3.82/1.23 ( ( sbrdtbr0 @
% 3.82/1.23 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) =
% 3.82/1.23 ( xK ) ) ))).thf(zf_stmt_0, type, zip_tseitin_24 : $i > $o).
% 3.82/1.23 thf(zf_stmt_1, axiom,
% 3.82/1.23 (![W0:$i]:
% 3.82/1.23 ( ( zip_tseitin_24 @ W0 ) <=>
% 3.82/1.23 ( ( aElement0 @ W0 ) &
% 3.82/1.23 ( ( aElementOf0 @ W0 @ xQ ) |
% 3.82/1.23 ( ( W0 ) = ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) ) ))).
% 3.82/1.23 thf(zf_stmt_2, conjecture,
% 3.82/1.23 (( ( aElementOf0 @
% 3.82/1.23 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ ( sdtlpdtrp0 @ xN @ xi ) ) &
% 3.82/1.23 ( ![W0:$i]:
% 3.82/1.23 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) =>
% 3.82/1.23 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ W0 ) ) ) ) =>
% 3.82/1.23 ( ( ( aSet0 @
% 3.82/1.23 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) &
% 3.82/1.23 ( ![W0:$i]:
% 3.82/1.23 ( ( aElementOf0 @
% 3.82/1.23 W0 @
% 3.82/1.23 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) <=>
% 3.82/1.23 ( zip_tseitin_24 @ W0 ) ) ) ) =>
% 3.82/1.23 ( ( sbrdtbr0 @
% 3.82/1.23 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) =
% 3.82/1.23 ( xK ) ) ))).
% 3.82/1.23 thf(zf_stmt_3, negated_conjecture,
% 3.82/1.23 (~( ( ( aElementOf0 @
% 3.82/1.23 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @
% 3.82/1.23 ( sdtlpdtrp0 @ xN @ xi ) ) &
% 3.82/1.23 ( ![W0:$i]:
% 3.82/1.23 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) =>
% 3.82/1.23 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ W0 ) ) ) ) =>
% 3.82/1.23 ( ( ( aSet0 @
% 3.82/1.23 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) &
% 3.82/1.23 ( ![W0:$i]:
% 3.82/1.23 ( ( aElementOf0 @
% 3.82/1.23 W0 @
% 3.82/1.23 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) <=>
% 3.82/1.23 ( zip_tseitin_24 @ W0 ) ) ) ) =>
% 3.82/1.23 ( ( sbrdtbr0 @
% 3.82/1.23 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) =
% 3.82/1.23 ( xK ) ) ) )),
% 3.82/1.23 inference('cnf.neg', [status(esa)], [zf_stmt_2])).
% 3.82/1.23 thf(zip_derived_cl263, plain,
% 3.82/1.23 (((sbrdtbr0 @ (sdtpldt0 @ xQ @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi))))
% 3.82/1.23 != (xK))),
% 3.82/1.23 inference('cnf', [status(esa)], [zf_stmt_3])).
% 3.82/1.23 thf(zip_derived_cl2065, plain,
% 3.82/1.23 ((((szszuzczcdt0 @ (sbrdtbr0 @ xQ)) != (xK))
% 3.82/1.23 | ~ (aSet0 @ xQ)
% 3.82/1.23 | ~ (isFinite0 @ xQ)
% 3.82/1.23 | (aElementOf0 @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)) @ xQ)
% 3.82/1.23 | ~ (aElement0 @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi))))),
% 3.82/1.23 inference('sup-', [status(thm)], [zip_derived_cl69, zip_derived_cl263])).
% 3.82/1.23 thf(m__3989_02, axiom,
% 3.82/1.23 (( aElementOf0 @
% 3.82/1.23 xQ @
% 3.82/1.23 ( slbdtsldtrb0 @
% 3.82/1.23 ( sdtmndt0 @
% 3.82/1.23 ( sdtlpdtrp0 @ xN @ xi ) @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) @
% 3.82/1.23 xk ) ) &
% 3.82/1.23 ( ( sbrdtbr0 @ xQ ) = ( xk ) ) &
% 3.82/1.23 ( aSubsetOf0 @
% 3.82/1.23 xQ @
% 3.82/1.23 ( sdtmndt0 @
% 3.82/1.23 ( sdtlpdtrp0 @ xN @ xi ) @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) &
% 3.82/1.23 ( ![W0:$i]:
% 3.82/1.23 ( ( aElementOf0 @ W0 @ xQ ) =>
% 3.82/1.23 ( aElementOf0 @
% 3.82/1.23 W0 @
% 3.82/1.23 ( sdtmndt0 @
% 3.82/1.23 ( sdtlpdtrp0 @ xN @ xi ) @
% 3.82/1.23 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) ) ) &
% 3.82/1.23 ( aSet0 @ xQ ) &
% 3.82/1.23 ( ![W0:$i]:
% 3.82/1.23 ( ( aElementOf0 @
% 3.82/1.23 W0 @
% 3.82/1.23 ( sdtmndt0 @
% 3.82/1.23 ( sdtlpdtrp0 @ xN @ xi ) @
% 3.82/1.23 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) <=>
% 3.82/1.23 ( ( aElement0 @ W0 ) &
% 3.82/1.23 ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) &
% 3.82/1.23 ( ( W0 ) != ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) ) ) &
% 3.82/1.23 ( aSet0 @
% 3.82/1.23 ( sdtmndt0 @
% 3.82/1.23 ( sdtlpdtrp0 @ xN @ xi ) @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) &
% 3.82/1.23 ( ![W0:$i]:
% 3.82/1.23 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) =>
% 3.82/1.23 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ W0 ) ) ) &
% 3.82/1.23 ( aElementOf0 @
% 3.82/1.23 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ ( sdtlpdtrp0 @ xN @ xi ) ))).
% 3.82/1.23 thf(zip_derived_cl255, plain, (((sbrdtbr0 @ xQ) = (xk))),
% 3.82/1.23 inference('cnf', [status(esa)], [m__3989_02])).
% 3.82/1.23 thf(m__3533, axiom,
% 3.82/1.23 (( ( szszuzczcdt0 @ xk ) = ( xK ) ) & ( aElementOf0 @ xk @ szNzAzT0 ))).
% 3.82/1.23 thf(zip_derived_cl209, plain, (((szszuzczcdt0 @ xk) = (xK))),
% 3.82/1.23 inference('cnf', [status(esa)], [m__3533])).
% 3.82/1.23 thf(zip_derived_cl252, plain, ( (aSet0 @ xQ)),
% 3.82/1.23 inference('cnf', [status(esa)], [m__3989_02])).
% 3.82/1.23 thf(zip_derived_cl255, plain, (((sbrdtbr0 @ xQ) = (xk))),
% 3.82/1.23 inference('cnf', [status(esa)], [m__3989_02])).
% 3.82/1.23 thf(mCardNum, axiom,
% 3.82/1.23 (![W0:$i]:
% 3.82/1.23 ( ( aSet0 @ W0 ) =>
% 3.82/1.23 ( ( aElementOf0 @ ( sbrdtbr0 @ W0 ) @ szNzAzT0 ) <=> ( isFinite0 @ W0 ) ) ))).
% 3.82/1.23 thf(zip_derived_cl66, plain,
% 3.82/1.23 (![X0 : $i]:
% 3.82/1.23 (~ (aElementOf0 @ (sbrdtbr0 @ X0) @ szNzAzT0)
% 3.82/1.23 | (isFinite0 @ X0)
% 3.82/1.23 | ~ (aSet0 @ X0))),
% 3.82/1.23 inference('cnf', [status(esa)], [mCardNum])).
% 3.82/1.23 thf(zip_derived_cl481, plain,
% 3.82/1.23 ((~ (aElementOf0 @ xk @ szNzAzT0) | ~ (aSet0 @ xQ) | (isFinite0 @ xQ))),
% 3.82/1.23 inference('sup-', [status(thm)], [zip_derived_cl255, zip_derived_cl66])).
% 3.82/1.23 thf(zip_derived_cl210, plain, ( (aElementOf0 @ xk @ szNzAzT0)),
% 3.82/1.23 inference('cnf', [status(esa)], [m__3533])).
% 3.82/1.23 thf(zip_derived_cl252, plain, ( (aSet0 @ xQ)),
% 3.82/1.23 inference('cnf', [status(esa)], [m__3989_02])).
% 3.82/1.23 thf(zip_derived_cl483, plain, ( (isFinite0 @ xQ)),
% 3.82/1.23 inference('demod', [status(thm)],
% 3.82/1.23 [zip_derived_cl481, zip_derived_cl210, zip_derived_cl252])).
% 3.82/1.23 thf(zip_derived_cl245, plain,
% 3.82/1.23 ( (aElementOf0 @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)) @
% 3.82/1.23 (sdtlpdtrp0 @ xN @ xi))),
% 3.82/1.23 inference('cnf', [status(esa)], [m__3989_02])).
% 3.82/1.23 thf(mEOfElem, axiom,
% 3.82/1.23 (![W0:$i]:
% 3.82/1.23 ( ( aSet0 @ W0 ) =>
% 3.82/1.23 ( ![W1:$i]: ( ( aElementOf0 @ W1 @ W0 ) => ( aElement0 @ W1 ) ) ) ))).
% 3.82/1.23 thf(zip_derived_cl2, plain,
% 3.82/1.23 (![X0 : $i, X1 : $i]:
% 3.82/1.23 (~ (aElementOf0 @ X0 @ X1) | (aElement0 @ X0) | ~ (aSet0 @ X1))),
% 3.82/1.23 inference('cnf', [status(esa)], [mEOfElem])).
% 3.82/1.23 thf(zip_derived_cl460, plain,
% 3.82/1.23 ((~ (aSet0 @ (sdtlpdtrp0 @ xN @ xi))
% 3.82/1.23 | (aElement0 @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi))))),
% 3.82/1.23 inference('sup-', [status(thm)], [zip_derived_cl245, zip_derived_cl2])).
% 3.82/1.23 thf(m__3989, axiom, (aElementOf0 @ xi @ szNzAzT0)).
% 3.82/1.23 thf(zip_derived_cl244, plain, ( (aElementOf0 @ xi @ szNzAzT0)),
% 3.82/1.23 inference('cnf', [status(esa)], [m__3989])).
% 3.82/1.23 thf(m__3671, axiom,
% 3.82/1.23 (![W0:$i]:
% 3.82/1.23 ( ( aElementOf0 @ W0 @ szNzAzT0 ) =>
% 3.82/1.23 ( ( aSet0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 3.82/1.23 ( ![W1:$i]:
% 3.82/1.23 ( ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 3.82/1.23 ( aElementOf0 @ W1 @ szNzAzT0 ) ) ) &
% 3.82/1.23 ( aSubsetOf0 @ ( sdtlpdtrp0 @ xN @ W0 ) @ szNzAzT0 ) &
% 3.82/1.23 ( isCountable0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ))).
% 3.82/1.23 thf(zip_derived_cl233, plain,
% 3.82/1.23 (![X0 : $i]:
% 3.82/1.23 ( (aSet0 @ (sdtlpdtrp0 @ xN @ X0)) | ~ (aElementOf0 @ X0 @ szNzAzT0))),
% 3.82/1.23 inference('cnf', [status(esa)], [m__3671])).
% 3.82/1.23 thf(zip_derived_cl337, plain, ( (aSet0 @ (sdtlpdtrp0 @ xN @ xi))),
% 3.82/1.23 inference('sup-', [status(thm)], [zip_derived_cl244, zip_derived_cl233])).
% 3.82/1.23 thf(zip_derived_cl461, plain,
% 3.82/1.23 ( (aElement0 @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)))),
% 3.82/1.23 inference('demod', [status(thm)], [zip_derived_cl460, zip_derived_cl337])).
% 3.82/1.23 thf(zip_derived_cl2088, plain,
% 3.82/1.23 ((((xK) != (xK))
% 3.82/1.23 | (aElementOf0 @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)) @ xQ))),
% 3.82/1.23 inference('demod', [status(thm)],
% 3.82/1.23 [zip_derived_cl2065, zip_derived_cl255, zip_derived_cl209,
% 3.82/1.23 zip_derived_cl252, zip_derived_cl483, zip_derived_cl461])).
% 3.82/1.23 thf(zip_derived_cl2089, plain,
% 3.82/1.23 ( (aElementOf0 @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)) @ xQ)),
% 3.82/1.23 inference('simplify', [status(thm)], [zip_derived_cl2088])).
% 3.82/1.23 thf(zip_derived_cl253, plain,
% 3.82/1.23 (![X0 : $i]:
% 3.82/1.23 ( (aElementOf0 @ X0 @
% 3.82/1.23 (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xi) @
% 3.82/1.23 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi))))
% 3.82/1.23 | ~ (aElementOf0 @ X0 @ xQ))),
% 3.82/1.23 inference('cnf', [status(esa)], [m__3989_02])).
% 3.82/1.23 thf(zip_derived_cl2096, plain,
% 3.82/1.23 ( (aElementOf0 @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)) @
% 3.82/1.23 (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xi) @
% 3.82/1.23 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi))))),
% 3.82/1.23 inference('sup-', [status(thm)], [zip_derived_cl2089, zip_derived_cl253])).
% 3.82/1.23 thf(zip_derived_cl251, plain,
% 3.82/1.23 (![X0 : $i]:
% 3.82/1.23 (((X0) != (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)))
% 3.82/1.23 | ~ (aElementOf0 @ X0 @
% 3.82/1.23 (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xi) @
% 3.82/1.23 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)))))),
% 3.82/1.23 inference('cnf', [status(esa)], [m__3989_02])).
% 3.82/1.23 thf(zip_derived_cl2495, plain,
% 3.82/1.23 (((szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi))
% 3.82/1.23 != (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)))),
% 3.82/1.23 inference('sup-', [status(thm)], [zip_derived_cl2096, zip_derived_cl251])).
% 3.82/1.23 thf(zip_derived_cl2501, plain, ($false),
% 3.82/1.23 inference('simplify', [status(thm)], [zip_derived_cl2495])).
% 3.82/1.23
% 3.82/1.23 % SZS output end Refutation
% 3.82/1.23
% 3.82/1.23
% 3.82/1.23 % Terminating...
% 4.42/1.34 % Runner terminated.
% 4.42/1.35 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------