%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : NUM629+1 : 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.ciiJ1wfjDh true
% Computer : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 04:47:42 PM UTC 2025
% Result : Theorem 50.67s 7.87s
% Output : Refutation 50.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.16 % Problem : NUM629+1 : TPTP v9.2.0. Released v4.0.0.
% 0.11/0.17 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.ciiJ1wfjDh true
% 0.14/0.39 % Computer : n021.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8042.1875MB
% 0.14/0.39 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Wed Oct 1 16:46:23 EDT 2025
% 0.14/0.39 % CPUTime :
% 0.14/0.39 % Running portfolio for 300 s
% 0.14/0.39 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.40 % Number of cores: 8
% 0.14/0.40 % Python version: Python 3.6.8
% 0.14/0.40 % Running in FO mode
% 0.54/0.71 % Total configuration time : 435
% 0.54/0.71 % Estimated wc time : 1092
% 0.54/0.71 % Estimated cpu time (7 cpus) : 156.0
% 0.59/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.59/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.59/0.81 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.59/0.82 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.59/0.82 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.59/0.82 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.59/0.82 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 50.67/7.87 % Solved by fo/fo6_bce.sh.
% 50.67/7.87 % BCE start: 221
% 50.67/7.87 % BCE eliminated: 0
% 50.67/7.87 % PE start: 221
% 50.67/7.87 logic: eq
% 50.67/7.87 % PE eliminated: 1
% 50.67/7.87 % done 2760 iterations in 7.072s
% 50.67/7.87 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 50.67/7.87 % SZS output start Refutation
% 50.67/7.87 thf(xD_type, type, xD: $i).
% 50.67/7.87 thf(szDzizrdt0_type, type, szDzizrdt0: $i > $i).
% 50.67/7.87 thf(aSet0_type, type, aSet0: $i > $o).
% 50.67/7.87 thf(szDzozmdt0_type, type, szDzozmdt0: $i > $i).
% 50.67/7.87 thf(aFunction0_type, type, aFunction0: $i > $o).
% 50.67/7.87 thf(slbdtsldtrb0_type, type, slbdtsldtrb0: $i > $i > $i).
% 50.67/7.87 thf(sz00_type, type, sz00: $i).
% 50.67/7.87 thf(xQ_type, type, xQ: $i).
% 50.67/7.87 thf(szszuzczcdt0_type, type, szszuzczcdt0: $i > $i).
% 50.67/7.87 thf(xP_type, type, xP: $i).
% 50.67/7.87 thf(sdtlpdtrp0_type, type, sdtlpdtrp0: $i > $i > $i).
% 50.67/7.87 thf(isCountable0_type, type, isCountable0: $i > $o).
% 50.67/7.87 thf(xN_type, type, xN: $i).
% 50.67/7.87 thf(sdtlbdtrb0_type, type, sdtlbdtrb0: $i > $i > $i).
% 50.67/7.87 thf(aElement0_type, type, aElement0: $i > $o).
% 50.67/7.87 thf(sbrdtbr0_type, type, sbrdtbr0: $i > $i).
% 50.67/7.87 thf(xS_type, type, xS: $i).
% 50.67/7.87 thf(xe_type, type, xe: $i).
% 50.67/7.87 thf(sk__1_type, type, sk__1: $i > $i > $i).
% 50.67/7.87 thf(sdtmndt0_type, type, sdtmndt0: $i > $i > $i).
% 50.67/7.87 thf(szmzizndt0_type, type, szmzizndt0: $i > $i).
% 50.67/7.87 thf(xd_type, type, xd: $i).
% 50.67/7.87 thf(aSubsetOf0_type, type, aSubsetOf0: $i > $i > $o).
% 50.67/7.87 thf(xO_type, type, xO: $i).
% 50.67/7.87 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $i > $o).
% 50.67/7.87 thf(xK_type, type, xK: $i).
% 50.67/7.87 thf(xp_type, type, xp: $i).
% 50.67/7.87 thf(szNzAzT0_type, type, szNzAzT0: $i).
% 50.67/7.87 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 50.67/7.87 thf(xn_type, type, xn: $i).
% 50.67/7.87 thf(xk_type, type, xk: $i).
% 50.67/7.87 thf(sdtlcdtrc0_type, type, sdtlcdtrc0: $i > $i > $i).
% 50.67/7.87 thf(m__, conjecture, (aElementOf0 @ xP @ ( slbdtsldtrb0 @ xD @ xk ))).
% 50.67/7.87 thf(zf_stmt_0, negated_conjecture,
% 50.67/7.87 (~( aElementOf0 @ xP @ ( slbdtsldtrb0 @ xD @ xk ) )),
% 50.67/7.87 inference('cnf.neg', [status(esa)], [m__])).
% 50.67/7.87 thf(zip_derived_cl220, plain,
% 50.67/7.87 (~ (aElementOf0 @ xP @ (slbdtsldtrb0 @ xD @ xk))),
% 50.67/7.87 inference('cnf', [status(esa)], [zf_stmt_0])).
% 50.67/7.87 thf(mDefSub, axiom,
% 50.67/7.87 (![W0:$i]:
% 50.67/7.87 ( ( aSet0 @ W0 ) =>
% 50.67/7.87 ( ![W1:$i]:
% 50.67/7.87 ( ( aSubsetOf0 @ W1 @ W0 ) <=>
% 50.67/7.87 ( ( aSet0 @ W1 ) &
% 50.67/7.87 ( ![W2:$i]:
% 50.67/7.87 ( ( aElementOf0 @ W2 @ W1 ) => ( aElementOf0 @ W2 @ W0 ) ) ) ) ) ) ))).
% 50.67/7.87 thf(zip_derived_cl12, plain,
% 50.67/7.87 (![X0 : $i, X1 : $i]:
% 50.67/7.87 (~ (aSet0 @ X0)
% 50.67/7.87 | (aElementOf0 @ (sk__1 @ X0 @ X1) @ X0)
% 50.67/7.87 | (aSubsetOf0 @ X0 @ X1)
% 50.67/7.87 | ~ (aSet0 @ X1))),
% 50.67/7.87 inference('cnf', [status(esa)], [mDefSub])).
% 50.67/7.87 thf(m__5334, axiom,
% 50.67/7.87 (aSubsetOf0 @ xP @ ( sdtlpdtrp0 @ xN @ ( szszuzczcdt0 @ xn ) ))).
% 50.67/7.87 thf(zip_derived_cl218, plain,
% 50.67/7.87 ( (aSubsetOf0 @ xP @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ xn)))),
% 50.67/7.87 inference('cnf', [status(esa)], [m__5334])).
% 50.67/7.87 thf(zip_derived_cl13, plain,
% 50.67/7.87 (![X0 : $i, X1 : $i, X2 : $i]:
% 50.67/7.87 (~ (aSubsetOf0 @ X0 @ X1)
% 50.67/7.87 | (aElementOf0 @ X2 @ X1)
% 50.67/7.87 | ~ (aElementOf0 @ X2 @ X0)
% 50.67/7.87 | ~ (aSet0 @ X1))),
% 50.67/7.87 inference('cnf', [status(esa)], [mDefSub])).
% 50.67/7.87 thf(zip_derived_cl2633, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 ( (aElementOf0 @ X0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ xn)))
% 50.67/7.87 | ~ (aElementOf0 @ X0 @ xP)
% 50.67/7.87 | ~ (aSet0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ xn))))),
% 50.67/7.87 inference('s_sup-', [status(thm)], [zip_derived_cl218, zip_derived_cl13])).
% 50.67/7.87 thf(m__5585, axiom,
% 50.67/7.87 (( xD ) =
% 50.67/7.87 ( sdtmndt0 @
% 50.67/7.87 ( sdtlpdtrp0 @ xN @ xn ) @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ))).
% 50.67/7.87 thf(zip_derived_cl219, plain,
% 50.67/7.87 (((xD)
% 50.67/7.87 = (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xn) @
% 50.67/7.87 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn))))),
% 50.67/7.87 inference('cnf', [status(esa)], [m__5585])).
% 50.67/7.87 thf(m__3623, axiom,
% 50.67/7.87 (( ![W0:$i]:
% 50.67/7.87 ( ( aElementOf0 @ W0 @ szNzAzT0 ) =>
% 50.67/7.87 ( ( ( aSubsetOf0 @ ( sdtlpdtrp0 @ xN @ W0 ) @ szNzAzT0 ) &
% 50.67/7.87 ( isCountable0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) =>
% 50.67/7.87 ( ( aSubsetOf0 @
% 50.67/7.87 ( sdtlpdtrp0 @ xN @ ( szszuzczcdt0 @ W0 ) ) @
% 50.67/7.87 ( sdtmndt0 @
% 50.67/7.87 ( sdtlpdtrp0 @ xN @ W0 ) @
% 50.67/7.87 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 50.67/7.87 ( isCountable0 @ ( sdtlpdtrp0 @ xN @ ( szszuzczcdt0 @ W0 ) ) ) ) ) ) ) &
% 50.67/7.87 ( ( sdtlpdtrp0 @ xN @ sz00 ) = ( xS ) ) &
% 50.67/7.87 ( ( szDzozmdt0 @ xN ) = ( szNzAzT0 ) ) & ( aFunction0 @ xN ))).
% 50.67/7.87 thf(zip_derived_cl163, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 (~ (aSubsetOf0 @ (sdtlpdtrp0 @ xN @ X0) @ szNzAzT0)
% 50.67/7.87 | ~ (isCountable0 @ (sdtlpdtrp0 @ xN @ X0))
% 50.67/7.87 | (aSubsetOf0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ X0)) @
% 50.67/7.87 (sdtmndt0 @ (sdtlpdtrp0 @ xN @ X0) @
% 50.67/7.87 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ X0))))
% 50.67/7.87 | ~ (aElementOf0 @ X0 @ szNzAzT0))),
% 50.67/7.87 inference('cnf', [status(esa)], [m__3623])).
% 50.67/7.87 thf(m__3671, axiom,
% 50.67/7.87 (![W0:$i]:
% 50.67/7.87 ( ( aElementOf0 @ W0 @ szNzAzT0 ) =>
% 50.67/7.87 ( ( aSubsetOf0 @ ( sdtlpdtrp0 @ xN @ W0 ) @ szNzAzT0 ) &
% 50.67/7.87 ( isCountable0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ))).
% 50.67/7.87 thf(zip_derived_cl165, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 ( (aSubsetOf0 @ (sdtlpdtrp0 @ xN @ X0) @ szNzAzT0)
% 50.67/7.87 | ~ (aElementOf0 @ X0 @ szNzAzT0))),
% 50.67/7.87 inference('cnf', [status(esa)], [m__3671])).
% 50.67/7.87 thf(zip_derived_cl3403, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 (~ (aElementOf0 @ X0 @ szNzAzT0)
% 50.67/7.87 | (aSubsetOf0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ X0)) @
% 50.67/7.87 (sdtmndt0 @ (sdtlpdtrp0 @ xN @ X0) @
% 50.67/7.87 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ X0))))
% 50.67/7.87 | ~ (isCountable0 @ (sdtlpdtrp0 @ xN @ X0)))),
% 50.67/7.87 inference('clc', [status(thm)], [zip_derived_cl163, zip_derived_cl165])).
% 50.67/7.87 thf(zip_derived_cl166, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 ( (isCountable0 @ (sdtlpdtrp0 @ xN @ X0))
% 50.67/7.87 | ~ (aElementOf0 @ X0 @ szNzAzT0))),
% 50.67/7.87 inference('cnf', [status(esa)], [m__3671])).
% 50.67/7.87 thf(zip_derived_cl3404, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 ( (aSubsetOf0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ X0)) @
% 50.67/7.87 (sdtmndt0 @ (sdtlpdtrp0 @ xN @ X0) @
% 50.67/7.87 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ X0))))
% 50.67/7.87 | ~ (aElementOf0 @ X0 @ szNzAzT0))),
% 50.67/7.87 inference('clc', [status(thm)], [zip_derived_cl3403, zip_derived_cl166])).
% 50.67/7.87 thf(zip_derived_cl3410, plain,
% 50.67/7.87 (( (aSubsetOf0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ xn)) @ xD)
% 50.67/7.87 | ~ (aElementOf0 @ xn @ szNzAzT0))),
% 50.67/7.87 inference('s_sup+', [status(thm)],
% 50.67/7.87 [zip_derived_cl219, zip_derived_cl3404])).
% 50.67/7.87 thf(m__5309, axiom,
% 50.67/7.87 (( ( sdtlpdtrp0 @ xe @ xn ) = ( xp ) ) & ( aElementOf0 @ xn @ szNzAzT0 ) &
% 50.67/7.87 ( aElementOf0 @ xn @ ( sdtlbdtrb0 @ xd @ ( szDzizrdt0 @ xd ) ) ))).
% 50.67/7.87 thf(zip_derived_cl215, plain, ( (aElementOf0 @ xn @ szNzAzT0)),
% 50.67/7.87 inference('cnf', [status(esa)], [m__5309])).
% 50.67/7.87 thf(zip_derived_cl3419, plain,
% 50.67/7.87 ( (aSubsetOf0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ xn)) @ xD)),
% 50.67/7.87 inference('demod', [status(thm)], [zip_derived_cl3410, zip_derived_cl215])).
% 50.67/7.87 thf(zip_derived_cl14, plain,
% 50.67/7.87 (![X0 : $i, X1 : $i]:
% 50.67/7.87 (~ (aSubsetOf0 @ X0 @ X1) | (aSet0 @ X0) | ~ (aSet0 @ X1))),
% 50.67/7.87 inference('cnf', [status(esa)], [mDefSub])).
% 50.67/7.87 thf(zip_derived_cl4862, plain,
% 50.67/7.87 (( (aSet0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ xn))) | ~ (aSet0 @ xD))),
% 50.67/7.87 inference('s_sup-', [status(thm)], [zip_derived_cl3419, zip_derived_cl14])).
% 50.67/7.87 thf(zip_derived_cl165, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 ( (aSubsetOf0 @ (sdtlpdtrp0 @ xN @ X0) @ szNzAzT0)
% 50.67/7.87 | ~ (aElementOf0 @ X0 @ szNzAzT0))),
% 50.67/7.87 inference('cnf', [status(esa)], [m__3671])).
% 50.67/7.87 thf(zip_derived_cl14, plain,
% 50.67/7.87 (![X0 : $i, X1 : $i]:
% 50.67/7.87 (~ (aSubsetOf0 @ X0 @ X1) | (aSet0 @ X0) | ~ (aSet0 @ X1))),
% 50.67/7.87 inference('cnf', [status(esa)], [mDefSub])).
% 50.67/7.87 thf(zip_derived_cl2333, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 (~ (aElementOf0 @ X0 @ szNzAzT0)
% 50.67/7.87 | (aSet0 @ (sdtlpdtrp0 @ xN @ X0))
% 50.67/7.87 | ~ (aSet0 @ szNzAzT0))),
% 50.67/7.87 inference('s_sup-', [status(thm)], [zip_derived_cl165, zip_derived_cl14])).
% 50.67/7.87 thf(mNATSet, axiom, (( isCountable0 @ szNzAzT0 ) & ( aSet0 @ szNzAzT0 ))).
% 50.67/7.87 thf(zip_derived_cl44, plain, ( (aSet0 @ szNzAzT0)),
% 50.67/7.87 inference('cnf', [status(esa)], [mNATSet])).
% 50.67/7.87 thf(zip_derived_cl2343, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 (~ (aElementOf0 @ X0 @ szNzAzT0) | (aSet0 @ (sdtlpdtrp0 @ xN @ X0)))),
% 50.67/7.87 inference('demod', [status(thm)], [zip_derived_cl2333, zip_derived_cl44])).
% 50.67/7.87 thf(m__4660, axiom,
% 50.67/7.87 (( ![W0:$i]:
% 50.67/7.87 ( ( aElementOf0 @ W0 @ szNzAzT0 ) =>
% 50.67/7.87 ( ( sdtlpdtrp0 @ xe @ W0 ) = ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) &
% 50.67/7.87 ( ( szDzozmdt0 @ xe ) = ( szNzAzT0 ) ) & ( aFunction0 @ xe ))).
% 50.67/7.87 thf(zip_derived_cl185, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 (((sdtlpdtrp0 @ xe @ X0) = (szmzizndt0 @ (sdtlpdtrp0 @ xN @ X0)))
% 50.67/7.87 | ~ (aElementOf0 @ X0 @ szNzAzT0))),
% 50.67/7.87 inference('cnf', [status(esa)], [m__4660])).
% 50.67/7.87 thf(zip_derived_cl219, plain,
% 50.67/7.87 (((xD)
% 50.67/7.87 = (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xn) @
% 50.67/7.87 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn))))),
% 50.67/7.87 inference('cnf', [status(esa)], [m__5585])).
% 50.67/7.87 thf(zip_derived_cl3152, plain,
% 50.67/7.87 ((~ (aElementOf0 @ xn @ szNzAzT0)
% 50.67/7.87 | ((xD) = (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xn) @ (sdtlpdtrp0 @ xe @ xn))))),
% 50.67/7.87 inference('s_sup+', [status(thm)], [zip_derived_cl185, zip_derived_cl219])).
% 50.67/7.87 thf(zip_derived_cl215, plain, ( (aElementOf0 @ xn @ szNzAzT0)),
% 50.67/7.87 inference('cnf', [status(esa)], [m__5309])).
% 50.67/7.87 thf(zip_derived_cl214, plain, (((sdtlpdtrp0 @ xe @ xn) = (xp))),
% 50.67/7.87 inference('cnf', [status(esa)], [m__5309])).
% 50.67/7.87 thf(zip_derived_cl3153, plain,
% 50.67/7.87 (((xD) = (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xn) @ xp))),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl3152, zip_derived_cl215, zip_derived_cl214])).
% 50.67/7.87 thf(mDefDiff, axiom,
% 50.67/7.87 (![W0:$i,W1:$i]:
% 50.67/7.87 ( ( ( aElement0 @ W1 ) & ( aSet0 @ W0 ) ) =>
% 50.67/7.87 ( ![W2:$i]:
% 50.67/7.87 ( ( ( W2 ) = ( sdtmndt0 @ W0 @ W1 ) ) <=>
% 50.67/7.87 ( ( ![W3:$i]:
% 50.67/7.87 ( ( aElementOf0 @ W3 @ W2 ) <=>
% 50.67/7.87 ( ( ( W3 ) != ( W1 ) ) & ( aElementOf0 @ W3 @ W0 ) &
% 50.67/7.87 ( aElement0 @ W3 ) ) ) ) &
% 50.67/7.87 ( aSet0 @ W2 ) ) ) ) ))).
% 50.67/7.87 thf(zf_stmt_1, type, zip_tseitin_1 : $i > $i > $i > $o).
% 50.67/7.87 thf(zf_stmt_2, axiom,
% 50.67/7.87 (![W3:$i,W1:$i,W0:$i]:
% 50.67/7.87 ( ( zip_tseitin_1 @ W3 @ W1 @ W0 ) <=>
% 50.67/7.87 ( ( aElement0 @ W3 ) & ( aElementOf0 @ W3 @ W0 ) & ( ( W3 ) != ( W1 ) ) ) ))).
% 50.67/7.87 thf(zf_stmt_3, axiom,
% 50.67/7.87 (![W0:$i,W1:$i]:
% 50.67/7.87 ( ( ( aSet0 @ W0 ) & ( aElement0 @ W1 ) ) =>
% 50.67/7.87 ( ![W2:$i]:
% 50.67/7.87 ( ( ( W2 ) = ( sdtmndt0 @ W0 @ W1 ) ) <=>
% 50.67/7.87 ( ( aSet0 @ W2 ) &
% 50.67/7.87 ( ![W3:$i]:
% 50.67/7.87 ( ( aElementOf0 @ W3 @ W2 ) <=> ( zip_tseitin_1 @ W3 @ W1 @ W0 ) ) ) ) ) ) ))).
% 50.67/7.87 thf(zip_derived_cl32, plain,
% 50.67/7.87 (![X0 : $i, X1 : $i, X2 : $i]:
% 50.67/7.87 (~ (aSet0 @ X0)
% 50.67/7.87 | ~ (aElement0 @ X1)
% 50.67/7.87 | (aSet0 @ X2)
% 50.67/7.87 | ((X2) != (sdtmndt0 @ X0 @ X1)))),
% 50.67/7.87 inference('cnf', [status(esa)], [zf_stmt_3])).
% 50.67/7.87 thf(zip_derived_cl1725, plain,
% 50.67/7.87 (![X0 : $i, X1 : $i]:
% 50.67/7.87 ( (aSet0 @ (sdtmndt0 @ X1 @ X0)) | ~ (aElement0 @ X0) | ~ (aSet0 @ X1))),
% 50.67/7.87 inference('eq_res', [status(thm)], [zip_derived_cl32])).
% 50.67/7.87 thf(zip_derived_cl4288, plain,
% 50.67/7.87 (( (aSet0 @ xD) | ~ (aElement0 @ xp) | ~ (aSet0 @ (sdtlpdtrp0 @ xN @ xn)))),
% 50.67/7.87 inference('s_sup+', [status(thm)],
% 50.67/7.87 [zip_derived_cl3153, zip_derived_cl1725])).
% 50.67/7.87 thf(m__5182, axiom, (aElementOf0 @ xp @ xO)).
% 50.67/7.87 thf(zip_derived_cl209, plain, ( (aElementOf0 @ xp @ xO)),
% 50.67/7.87 inference('cnf', [status(esa)], [m__5182])).
% 50.67/7.87 thf(mEOfElem, axiom,
% 50.67/7.87 (![W0:$i]:
% 50.67/7.87 ( ( aSet0 @ W0 ) =>
% 50.67/7.87 ( ![W1:$i]: ( ( aElementOf0 @ W1 @ W0 ) => ( aElement0 @ W1 ) ) ) ))).
% 50.67/7.87 thf(zip_derived_cl2, plain,
% 50.67/7.87 (![X0 : $i, X1 : $i]:
% 50.67/7.87 (~ (aElementOf0 @ X0 @ X1) | (aElement0 @ X0) | ~ (aSet0 @ X1))),
% 50.67/7.87 inference('cnf', [status(esa)], [mEOfElem])).
% 50.67/7.87 thf(zip_derived_cl1626, plain, (( (aElement0 @ xp) | ~ (aSet0 @ xO))),
% 50.67/7.87 inference('s_sup-', [status(thm)], [zip_derived_cl209, zip_derived_cl2])).
% 50.67/7.87 thf(m__4891, axiom,
% 50.67/7.87 (( ( xO ) = ( sdtlcdtrc0 @ xe @ ( sdtlbdtrb0 @ xd @ ( szDzizrdt0 @ xd ) ) ) ) &
% 50.67/7.87 ( aSet0 @ xO ))).
% 50.67/7.87 thf(zip_derived_cl193, plain, ( (aSet0 @ xO)),
% 50.67/7.87 inference('cnf', [status(esa)], [m__4891])).
% 50.67/7.87 thf(zip_derived_cl1627, plain, ( (aElement0 @ xp)),
% 50.67/7.87 inference('demod', [status(thm)], [zip_derived_cl1626, zip_derived_cl193])).
% 50.67/7.87 thf(zip_derived_cl4291, plain,
% 50.67/7.87 (( (aSet0 @ xD) | ~ (aSet0 @ (sdtlpdtrp0 @ xN @ xn)))),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl4288, zip_derived_cl1627])).
% 50.67/7.87 thf(zip_derived_cl12653, plain,
% 50.67/7.87 ((~ (aElementOf0 @ xn @ szNzAzT0) | (aSet0 @ xD))),
% 50.67/7.87 inference('s_sup-', [status(thm)],
% 50.67/7.87 [zip_derived_cl2343, zip_derived_cl4291])).
% 50.67/7.87 thf(zip_derived_cl215, plain, ( (aElementOf0 @ xn @ szNzAzT0)),
% 50.67/7.87 inference('cnf', [status(esa)], [m__5309])).
% 50.67/7.87 thf(zip_derived_cl12658, plain, ( (aSet0 @ xD)),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl12653, zip_derived_cl215])).
% 50.67/7.87 thf(zip_derived_cl12665, plain,
% 50.67/7.87 ( (aSet0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ xn)))),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl4862, zip_derived_cl12658])).
% 50.67/7.87 thf(zip_derived_cl28255, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 ( (aElementOf0 @ X0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ xn)))
% 50.67/7.87 | ~ (aElementOf0 @ X0 @ xP))),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl2633, zip_derived_cl12665])).
% 50.67/7.87 thf(zip_derived_cl3419, plain,
% 50.67/7.87 ( (aSubsetOf0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ xn)) @ xD)),
% 50.67/7.87 inference('demod', [status(thm)], [zip_derived_cl3410, zip_derived_cl215])).
% 50.67/7.87 thf(zip_derived_cl13, plain,
% 50.67/7.87 (![X0 : $i, X1 : $i, X2 : $i]:
% 50.67/7.87 (~ (aSubsetOf0 @ X0 @ X1)
% 50.67/7.87 | (aElementOf0 @ X2 @ X1)
% 50.67/7.87 | ~ (aElementOf0 @ X2 @ X0)
% 50.67/7.87 | ~ (aSet0 @ X1))),
% 50.67/7.87 inference('cnf', [status(esa)], [mDefSub])).
% 50.67/7.87 thf(zip_derived_cl4861, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 ( (aElementOf0 @ X0 @ xD)
% 50.67/7.87 | ~ (aElementOf0 @ X0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ xn)))
% 50.67/7.87 | ~ (aSet0 @ xD))),
% 50.67/7.87 inference('s_sup-', [status(thm)], [zip_derived_cl3419, zip_derived_cl13])).
% 50.67/7.87 thf(zip_derived_cl12658, plain, ( (aSet0 @ xD)),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl12653, zip_derived_cl215])).
% 50.67/7.87 thf(zip_derived_cl12664, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 ( (aElementOf0 @ X0 @ xD)
% 50.67/7.87 | ~ (aElementOf0 @ X0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ xn))))),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl4861, zip_derived_cl12658])).
% 50.67/7.87 thf(zip_derived_cl28258, plain,
% 50.67/7.87 (![X0 : $i]: (~ (aElementOf0 @ X0 @ xP) | (aElementOf0 @ X0 @ xD))),
% 50.67/7.87 inference('s_sup-', [status(thm)],
% 50.67/7.87 [zip_derived_cl28255, zip_derived_cl12664])).
% 50.67/7.87 thf(zip_derived_cl11, plain,
% 50.67/7.87 (![X0 : $i, X1 : $i]:
% 50.67/7.87 (~ (aSet0 @ X0)
% 50.67/7.87 | ~ (aElementOf0 @ (sk__1 @ X0 @ X1) @ X1)
% 50.67/7.87 | (aSubsetOf0 @ X0 @ X1)
% 50.67/7.87 | ~ (aSet0 @ X1))),
% 50.67/7.87 inference('cnf', [status(esa)], [mDefSub])).
% 50.67/7.87 thf(zip_derived_cl28272, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 (~ (aElementOf0 @ (sk__1 @ X0 @ xD) @ xP)
% 50.67/7.87 | ~ (aSet0 @ X0)
% 50.67/7.87 | (aSubsetOf0 @ X0 @ xD)
% 50.67/7.87 | ~ (aSet0 @ xD))),
% 50.67/7.87 inference('s_sup-', [status(thm)],
% 50.67/7.87 [zip_derived_cl28258, zip_derived_cl11])).
% 50.67/7.87 thf(zip_derived_cl12658, plain, ( (aSet0 @ xD)),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl12653, zip_derived_cl215])).
% 50.67/7.87 thf(zip_derived_cl28279, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 (~ (aElementOf0 @ (sk__1 @ X0 @ xD) @ xP)
% 50.67/7.87 | ~ (aSet0 @ X0)
% 50.67/7.87 | (aSubsetOf0 @ X0 @ xD))),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl28272, zip_derived_cl12658])).
% 50.67/7.87 thf(zip_derived_cl36166, plain,
% 50.67/7.87 ((~ (aSet0 @ xD)
% 50.67/7.87 | (aSubsetOf0 @ xP @ xD)
% 50.67/7.87 | ~ (aSet0 @ xP)
% 50.67/7.87 | ~ (aSet0 @ xP)
% 50.67/7.87 | (aSubsetOf0 @ xP @ xD))),
% 50.67/7.87 inference('s_sup-', [status(thm)],
% 50.67/7.87 [zip_derived_cl12, zip_derived_cl28279])).
% 50.67/7.87 thf(zip_derived_cl12658, plain, ( (aSet0 @ xD)),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl12653, zip_derived_cl215])).
% 50.67/7.87 thf(m__5164, axiom,
% 50.67/7.87 (( ( xP ) = ( sdtmndt0 @ xQ @ ( szmzizndt0 @ xQ ) ) ) & ( aSet0 @ xP ))).
% 50.67/7.87 thf(zip_derived_cl207, plain, ( (aSet0 @ xP)),
% 50.67/7.87 inference('cnf', [status(esa)], [m__5164])).
% 50.67/7.87 thf(zip_derived_cl207, plain, ( (aSet0 @ xP)),
% 50.67/7.87 inference('cnf', [status(esa)], [m__5164])).
% 50.67/7.87 thf(zip_derived_cl36167, plain,
% 50.67/7.87 (( (aSubsetOf0 @ xP @ xD) | (aSubsetOf0 @ xP @ xD))),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl36166, zip_derived_cl12658, zip_derived_cl207,
% 50.67/7.87 zip_derived_cl207])).
% 50.67/7.87 thf(zip_derived_cl36168, plain, ( (aSubsetOf0 @ xP @ xD)),
% 50.67/7.87 inference('simplify', [status(thm)], [zip_derived_cl36167])).
% 50.67/7.87 thf(m__5217, axiom, (( sbrdtbr0 @ xP ) = ( xk ))).
% 50.67/7.87 thf(zip_derived_cl212, plain, (((sbrdtbr0 @ xP) = (xk))),
% 50.67/7.87 inference('cnf', [status(esa)], [m__5217])).
% 50.67/7.87 thf(mDefSel, axiom,
% 50.67/7.87 (![W0:$i,W1:$i]:
% 50.67/7.87 ( ( ( aSet0 @ W0 ) & ( aElementOf0 @ W1 @ szNzAzT0 ) ) =>
% 50.67/7.87 ( ![W2:$i]:
% 50.67/7.87 ( ( ( W2 ) = ( slbdtsldtrb0 @ W0 @ W1 ) ) <=>
% 50.67/7.87 ( ( aSet0 @ W2 ) &
% 50.67/7.87 ( ![W3:$i]:
% 50.67/7.87 ( ( aElementOf0 @ W3 @ W2 ) <=>
% 50.67/7.87 ( ( aSubsetOf0 @ W3 @ W0 ) & ( ( sbrdtbr0 @ W3 ) = ( W1 ) ) ) ) ) ) ) ) ))).
% 50.67/7.87 thf(zip_derived_cl103, plain,
% 50.67/7.87 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 50.67/7.87 (~ (aSet0 @ X0)
% 50.67/7.87 | ~ (aElementOf0 @ X1 @ szNzAzT0)
% 50.67/7.87 | ~ (aSubsetOf0 @ X2 @ X0)
% 50.67/7.87 | ((sbrdtbr0 @ X2) != (X1))
% 50.67/7.87 | (aElementOf0 @ X2 @ X3)
% 50.67/7.87 | ((X3) != (slbdtsldtrb0 @ X0 @ X1)))),
% 50.67/7.87 inference('cnf', [status(esa)], [mDefSel])).
% 50.67/7.87 thf(zip_derived_cl2688, plain,
% 50.67/7.87 (![X0 : $i, X1 : $i, X2 : $i]:
% 50.67/7.87 (~ (aSet0 @ X1)
% 50.67/7.87 | ~ (aElementOf0 @ X0 @ szNzAzT0)
% 50.67/7.87 | ~ (aSubsetOf0 @ xP @ X1)
% 50.67/7.87 | ((xk) != (X0))
% 50.67/7.87 | (aElementOf0 @ xP @ X2)
% 50.67/7.87 | ((X2) != (slbdtsldtrb0 @ X1 @ X0)))),
% 50.67/7.87 inference('s_sup-', [status(thm)], [zip_derived_cl212, zip_derived_cl103])).
% 50.67/7.87 thf(zip_derived_cl32125, plain,
% 50.67/7.87 (![X0 : $i, X1 : $i]:
% 50.67/7.87 (((X0) != (slbdtsldtrb0 @ X1 @ xk))
% 50.67/7.87 | (aElementOf0 @ xP @ X0)
% 50.67/7.87 | ~ (aSubsetOf0 @ xP @ X1)
% 50.67/7.87 | ~ (aElementOf0 @ xk @ szNzAzT0)
% 50.67/7.87 | ~ (aSet0 @ X1))),
% 50.67/7.87 inference('eq_res', [status(thm)], [zip_derived_cl2688])).
% 50.67/7.87 thf(m__3533, axiom,
% 50.67/7.87 (( ( szszuzczcdt0 @ xk ) = ( xK ) ) & ( aElementOf0 @ xk @ szNzAzT0 ))).
% 50.67/7.87 thf(zip_derived_cl159, plain, ( (aElementOf0 @ xk @ szNzAzT0)),
% 50.67/7.87 inference('cnf', [status(esa)], [m__3533])).
% 50.67/7.87 thf(zip_derived_cl32126, plain,
% 50.67/7.87 (![X0 : $i, X1 : $i]:
% 50.67/7.87 (((X0) != (slbdtsldtrb0 @ X1 @ xk))
% 50.67/7.87 | (aElementOf0 @ xP @ X0)
% 50.67/7.87 | ~ (aSubsetOf0 @ xP @ X1)
% 50.67/7.87 | ~ (aSet0 @ X1))),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl32125, zip_derived_cl159])).
% 50.67/7.87 thf(zip_derived_cl36174, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 (((X0) != (slbdtsldtrb0 @ xD @ xk))
% 50.67/7.87 | (aElementOf0 @ xP @ X0)
% 50.67/7.87 | ~ (aSet0 @ xD))),
% 50.67/7.87 inference('s_sup-', [status(thm)],
% 50.67/7.87 [zip_derived_cl36168, zip_derived_cl32126])).
% 50.67/7.87 thf(zip_derived_cl12658, plain, ( (aSet0 @ xD)),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl12653, zip_derived_cl215])).
% 50.67/7.87 thf(zip_derived_cl36180, plain,
% 50.67/7.87 (![X0 : $i]:
% 50.67/7.87 (((X0) != (slbdtsldtrb0 @ xD @ xk)) | (aElementOf0 @ xP @ X0))),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl36174, zip_derived_cl12658])).
% 50.67/7.87 thf(zip_derived_cl36434, plain,
% 50.67/7.87 ( (aElementOf0 @ xP @ (slbdtsldtrb0 @ xD @ xk))),
% 50.67/7.87 inference('eq_res', [status(thm)], [zip_derived_cl36180])).
% 50.67/7.87 thf(zip_derived_cl36435, plain, ($false),
% 50.67/7.87 inference('demod', [status(thm)],
% 50.67/7.87 [zip_derived_cl220, zip_derived_cl36434])).
% 50.67/7.87
% 50.67/7.87 % SZS output end Refutation
% 50.67/7.87
% 50.67/7.87
% 50.67/7.87 % Terminating...
% 50.67/7.93 % Runner terminated.
% 50.67/7.94 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------