%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : NUM629+3 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.zsphnGpOZy true
% Computer : n006.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 31.44s 5.72s
% Output : Refutation 31.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.14 % Problem : NUM629+3 : TPTP v9.2.0. Released v4.0.0.
% 0.07/0.15 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.zsphnGpOZy true
% 0.13/0.36 % Computer : n006.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Wed Oct 1 16:27:23 EDT 2025
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Running portfolio for 300 s
% 0.13/0.36 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.36 % Number of cores: 8
% 0.13/0.37 % Python version: Python 3.6.8
% 0.13/0.37 % Running in FO mode
% 0.53/0.67 % Total configuration time : 435
% 0.53/0.67 % Estimated wc time : 1092
% 0.53/0.67 % Estimated cpu time (7 cpus) : 156.0
% 0.54/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.54/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.54/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.55/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 31.44/5.72 % Solved by fo/fo5.sh.
% 31.44/5.72 % done 4916 iterations in 4.905s
% 31.44/5.72 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 31.44/5.72 % SZS output start Refutation
% 31.44/5.72 thf(zip_tseitin_19_type, type, zip_tseitin_19: $i > $i > $o).
% 31.44/5.72 thf(szDzizrdt0_type, type, szDzizrdt0: $i > $i).
% 31.44/5.72 thf(aSet0_type, type, aSet0: $i > $o).
% 31.44/5.72 thf(szDzozmdt0_type, type, szDzozmdt0: $i > $i).
% 31.44/5.72 thf(sk__47_type, type, sk__47: $i).
% 31.44/5.72 thf(aFunction0_type, type, aFunction0: $i > $o).
% 31.44/5.72 thf(slbdtsldtrb0_type, type, slbdtsldtrb0: $i > $i > $i).
% 31.44/5.72 thf(sz00_type, type, sz00: $i).
% 31.44/5.72 thf(xe_type, type, xe: $i).
% 31.44/5.72 thf(xO_type, type, xO: $i).
% 31.44/5.72 thf(szszuzczcdt0_type, type, szszuzczcdt0: $i > $i).
% 31.44/5.72 thf(sdtlpdtrp0_type, type, sdtlpdtrp0: $i > $i > $i).
% 31.44/5.72 thf(isCountable0_type, type, isCountable0: $i > $o).
% 31.44/5.72 thf(sdtlbdtrb0_type, type, sdtlbdtrb0: $i > $i > $i).
% 31.44/5.72 thf(aElement0_type, type, aElement0: $i > $o).
% 31.44/5.72 thf(sbrdtbr0_type, type, sbrdtbr0: $i > $i).
% 31.44/5.72 thf(xS_type, type, xS: $i).
% 31.44/5.72 thf(sdtlseqdt0_type, type, sdtlseqdt0: $i > $i > $o).
% 31.44/5.72 thf(zip_tseitin_23_type, type, zip_tseitin_23: $i > $o).
% 31.44/5.72 thf(sdtmndt0_type, type, sdtmndt0: $i > $i > $i).
% 31.44/5.72 thf(szmzizndt0_type, type, szmzizndt0: $i > $i).
% 31.44/5.72 thf(aSubsetOf0_type, type, aSubsetOf0: $i > $i > $o).
% 31.44/5.72 thf(xQ_type, type, xQ: $i).
% 31.44/5.72 thf(sdtpldt0_type, type, sdtpldt0: $i > $i > $i).
% 31.44/5.72 thf(xp_type, type, xp: $i).
% 31.44/5.72 thf(xP_type, type, xP: $i).
% 31.44/5.72 thf(xd_type, type, xd: $i).
% 31.44/5.72 thf(zip_tseitin_21_type, type, zip_tseitin_21: $i > $i > $o).
% 31.44/5.72 thf(xk_type, type, xk: $i).
% 31.44/5.72 thf(xK_type, type, xK: $i).
% 31.44/5.72 thf(szNzAzT0_type, type, szNzAzT0: $i).
% 31.44/5.72 thf(xN_type, type, xN: $i).
% 31.44/5.72 thf(zip_tseitin_22_type, type, zip_tseitin_22: $i > $i > $o).
% 31.44/5.72 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 31.44/5.72 thf(zip_tseitin_20_type, type, zip_tseitin_20: $i > $o).
% 31.44/5.72 thf(xD_type, type, xD: $i).
% 31.44/5.72 thf(xn_type, type, xn: $i).
% 31.44/5.72 thf(m__, conjecture,
% 31.44/5.72 (( aElementOf0 @ xP @ ( slbdtsldtrb0 @ xD @ xk ) ) |
% 31.44/5.72 ( aSubsetOf0 @ xP @ xD ) |
% 31.44/5.72 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xP ) => ( aElementOf0 @ W0 @ xD ) ) ))).
% 31.44/5.72 thf(zf_stmt_0, negated_conjecture,
% 31.44/5.72 (~( ( aElementOf0 @ xP @ ( slbdtsldtrb0 @ xD @ xk ) ) |
% 31.44/5.72 ( aSubsetOf0 @ xP @ xD ) |
% 31.44/5.72 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xP ) => ( aElementOf0 @ W0 @ xD ) ) ) )),
% 31.44/5.72 inference('cnf.neg', [status(esa)], [m__])).
% 31.44/5.72 thf(zip_derived_cl487, plain, (~ (aElementOf0 @ sk__47 @ xD)),
% 31.44/5.72 inference('cnf', [status(esa)], [zf_stmt_0])).
% 31.44/5.72 thf(mDiffCons, axiom,
% 31.44/5.72 (![W0:$i,W1:$i]:
% 31.44/5.72 ( ( ( aElement0 @ W0 ) & ( aSet0 @ W1 ) ) =>
% 31.44/5.72 ( ( ~( aElementOf0 @ W0 @ W1 ) ) =>
% 31.44/5.72 ( ( sdtmndt0 @ ( sdtpldt0 @ W1 @ W0 ) @ W0 ) = ( W1 ) ) ) ))).
% 31.44/5.72 thf(zip_derived_cl38, plain,
% 31.44/5.72 (![X0 : $i, X1 : $i]:
% 31.44/5.72 (~ (aElement0 @ X0)
% 31.44/5.72 | ~ (aSet0 @ X1)
% 31.44/5.72 | ((sdtmndt0 @ (sdtpldt0 @ X1 @ X0) @ X0) = (X1))
% 31.44/5.72 | (aElementOf0 @ X0 @ X1))),
% 31.44/5.72 inference('cnf', [status(esa)], [mDiffCons])).
% 31.44/5.72 thf(zip_derived_cl488, plain, ( (aElementOf0 @ sk__47 @ xP)),
% 31.44/5.72 inference('cnf', [status(esa)], [zf_stmt_0])).
% 31.44/5.72 thf(m__5334, axiom,
% 31.44/5.72 (( aSubsetOf0 @ xP @ ( sdtlpdtrp0 @ xN @ ( szszuzczcdt0 @ xn ) ) ) &
% 31.44/5.72 ( ![W0:$i]:
% 31.44/5.72 ( ( aElementOf0 @ W0 @ xP ) =>
% 31.44/5.72 ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ ( szszuzczcdt0 @ xn ) ) ) ) ))).
% 31.44/5.72 thf(zip_derived_cl478, plain,
% 31.44/5.72 (![X0 : $i]:
% 31.44/5.72 ( (aElementOf0 @ X0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ xn)))
% 31.44/5.72 | ~ (aElementOf0 @ X0 @ xP))),
% 31.44/5.72 inference('cnf', [status(esa)], [m__5334])).
% 31.44/5.72 thf(zip_derived_cl3258, plain,
% 31.44/5.72 ( (aElementOf0 @ sk__47 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ xn)))),
% 31.44/5.72 inference('sup-', [status(thm)], [zip_derived_cl488, zip_derived_cl478])).
% 31.44/5.72 thf(m__3623, axiom,
% 31.44/5.72 (( aFunction0 @ xN ) & ( ( szDzozmdt0 @ xN ) = ( szNzAzT0 ) ) &
% 31.44/5.72 ( ( sdtlpdtrp0 @ xN @ sz00 ) = ( xS ) ) &
% 31.44/5.72 ( ![W0:$i]:
% 31.44/5.72 ( ( aElementOf0 @ W0 @ szNzAzT0 ) =>
% 31.44/5.72 ( ( ( isCountable0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 31.44/5.72 ( ( aSubsetOf0 @ ( sdtlpdtrp0 @ xN @ W0 ) @ szNzAzT0 ) |
% 31.44/5.72 ( ( ![W1:$i]:
% 31.44/5.72 ( ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 31.44/5.72 ( aElementOf0 @ W1 @ szNzAzT0 ) ) ) &
% 31.44/5.72 ( aSet0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) =>
% 31.44/5.72 ( ( isCountable0 @ ( sdtlpdtrp0 @ xN @ ( szszuzczcdt0 @ W0 ) ) ) &
% 31.44/5.72 ( aSubsetOf0 @
% 31.44/5.72 ( sdtlpdtrp0 @ xN @ ( szszuzczcdt0 @ W0 ) ) @
% 31.44/5.72 ( sdtmndt0 @
% 31.44/5.72 ( sdtlpdtrp0 @ xN @ W0 ) @
% 31.44/5.72 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 31.44/5.72 ( ![W1:$i]:
% 31.44/5.72 ( ( aElementOf0 @
% 31.44/5.72 W1 @ ( sdtlpdtrp0 @ xN @ ( szszuzczcdt0 @ W0 ) ) ) =>
% 31.44/5.72 ( aElementOf0 @
% 31.44/5.72 W1 @
% 31.44/5.72 ( sdtmndt0 @
% 31.44/5.72 ( sdtlpdtrp0 @ xN @ W0 ) @
% 31.44/5.72 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) &
% 31.44/5.72 ( aSet0 @ ( sdtlpdtrp0 @ xN @ ( szszuzczcdt0 @ W0 ) ) ) &
% 31.44/5.72 ( ![W1:$i]:
% 31.44/5.72 ( ( aElementOf0 @
% 31.44/5.72 W1 @
% 31.44/5.72 ( sdtmndt0 @
% 31.44/5.72 ( sdtlpdtrp0 @ xN @ W0 ) @
% 31.44/5.72 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) <=>
% 31.44/5.72 ( ( ( W1 ) != ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) &
% 31.44/5.72 ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 31.44/5.72 ( aElement0 @ W1 ) ) ) ) &
% 31.44/5.72 ( aSet0 @
% 31.44/5.72 ( sdtmndt0 @
% 31.44/5.72 ( sdtlpdtrp0 @ xN @ W0 ) @
% 31.44/5.72 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 31.44/5.72 ( ![W1:$i]:
% 31.44/5.72 ( ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 31.44/5.72 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ W1 ) ) ) &
% 31.44/5.72 ( aElementOf0 @
% 31.44/5.72 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @
% 31.44/5.72 ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ))).
% 31.44/5.72 thf(zf_stmt_1, axiom,
% 31.44/5.72 (![W0:$i]:
% 31.44/5.72 ( ( zip_tseitin_23 @ W0 ) =>
% 31.44/5.72 ( ( aElementOf0 @
% 31.44/5.72 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 31.44/5.72 ( ![W1:$i]:
% 31.44/5.72 ( ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 31.44/5.72 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ W1 ) ) ) &
% 31.44/5.72 ( aSet0 @
% 31.44/5.72 ( sdtmndt0 @
% 31.44/5.72 ( sdtlpdtrp0 @ xN @ W0 ) @
% 31.44/5.72 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 31.44/5.72 ( ![W1:$i]: ( zip_tseitin_22 @ W1 @ W0 ) ) &
% 31.44/5.72 ( aSet0 @ ( sdtlpdtrp0 @ xN @ ( szszuzczcdt0 @ W0 ) ) ) &
% 31.44/5.72 ( ![W1:$i]:
% 31.44/5.72 ( ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ ( szszuzczcdt0 @ W0 ) ) ) =>
% 31.44/5.72 ( aElementOf0 @
% 31.44/5.72 W1 @
% 31.44/5.72 ( sdtmndt0 @
% 31.44/5.72 ( sdtlpdtrp0 @ xN @ W0 ) @
% 31.44/5.72 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) &
% 31.44/5.72 ( aSubsetOf0 @
% 31.44/5.72 ( sdtlpdtrp0 @ xN @ ( szszuzczcdt0 @ W0 ) ) @
% 31.44/5.72 ( sdtmndt0 @
% 31.44/5.72 ( sdtlpdtrp0 @ xN @ W0 ) @
% 31.44/5.72 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 31.44/5.72 ( isCountable0 @ ( sdtlpdtrp0 @ xN @ ( szszuzczcdt0 @ W0 ) ) ) ) ))).
% 31.44/5.72 thf(zip_derived_cl226, plain,
% 31.44/5.72 (![X0 : $i, X1 : $i]:
% 31.44/5.72 (~ (aElementOf0 @ X0 @ (sdtlpdtrp0 @ xN @ (szszuzczcdt0 @ X1)))
% 31.44/5.72 | (aElementOf0 @ X0 @
% 31.44/5.72 (sdtmndt0 @ (sdtlpdtrp0 @ xN @ X1) @
% 31.44/5.72 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ X1))))
% 31.44/5.72 | ~ (zip_tseitin_23 @ X1))),
% 31.44/5.72 inference('cnf', [status(esa)], [zf_stmt_1])).
% 31.44/5.72 thf(zip_derived_cl9603, plain,
% 31.44/5.72 ((~ (zip_tseitin_23 @ xn)
% 31.44/5.72 | (aElementOf0 @ sk__47 @
% 31.44/5.72 (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xn) @
% 31.44/5.72 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn)))))),
% 31.44/5.72 inference('sup-', [status(thm)], [zip_derived_cl3258, zip_derived_cl226])).
% 31.44/5.72 thf(m__5309, axiom,
% 31.44/5.72 (( ( sdtlpdtrp0 @ xe @ xn ) = ( xp ) ) & ( aElementOf0 @ xn @ szNzAzT0 ) &
% 31.44/5.72 ( aElementOf0 @ xn @ ( sdtlbdtrb0 @ xd @ ( szDzizrdt0 @ xd ) ) ) &
% 31.44/5.72 ( ( sdtlpdtrp0 @ xd @ xn ) = ( szDzizrdt0 @ xd ) ) &
% 31.44/5.72 ( aElementOf0 @ xn @ ( szDzozmdt0 @ xd ) ))).
% 31.44/5.72 thf(zip_derived_cl473, plain, ( (aElementOf0 @ xn @ szNzAzT0)),
% 31.44/5.72 inference('cnf', [status(esa)], [m__5309])).
% 31.44/5.72 thf(m__4660, axiom,
% 31.44/5.72 (( ![W0:$i]:
% 31.44/5.72 ( ( aElementOf0 @ W0 @ szNzAzT0 ) =>
% 31.44/5.72 ( ( aElementOf0 @ ( sdtlpdtrp0 @ xe @ W0 ) @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 31.44/5.72 ( ![W1:$i]:
% 31.44/5.72 ( ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 31.44/5.72 ( sdtlseqdt0 @ ( sdtlpdtrp0 @ xe @ W0 ) @ W1 ) ) ) &
% 31.44/5.72 ( ( sdtlpdtrp0 @ xe @ W0 ) =
% 31.44/5.72 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) &
% 31.44/5.72 ( ( szDzozmdt0 @ xe ) = ( szNzAzT0 ) ) & ( aFunction0 @ xe ))).
% 31.44/5.72 thf(zip_derived_cl401, plain,
% 31.44/5.72 (![X0 : $i]:
% 31.44/5.72 (((sdtlpdtrp0 @ xe @ X0) = (szmzizndt0 @ (sdtlpdtrp0 @ xN @ X0)))
% 31.44/5.72 | ~ (aElementOf0 @ X0 @ szNzAzT0))),
% 31.44/5.72 inference('cnf', [status(esa)], [m__4660])).
% 31.44/5.72 thf(zip_derived_cl8467, plain,
% 31.44/5.72 (((sdtlpdtrp0 @ xe @ xn) = (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn)))),
% 31.44/5.72 inference('sup-', [status(thm)], [zip_derived_cl473, zip_derived_cl401])).
% 31.44/5.72 thf(zip_derived_cl472, plain, (((sdtlpdtrp0 @ xe @ xn) = (xp))),
% 31.44/5.72 inference('cnf', [status(esa)], [m__5309])).
% 31.44/5.72 thf(zip_derived_cl8487, plain,
% 31.44/5.72 (((xp) = (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn)))),
% 31.44/5.72 inference('demod', [status(thm)], [zip_derived_cl8467, zip_derived_cl472])).
% 31.44/5.72 thf(zip_derived_cl9614, plain,
% 31.44/5.72 ((~ (zip_tseitin_23 @ xn)
% 31.44/5.72 | (aElementOf0 @ sk__47 @ (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xn) @ xp)))),
% 31.44/5.72 inference('demod', [status(thm)],
% 31.44/5.72 [zip_derived_cl9603, zip_derived_cl8487])).
% 31.44/5.72 thf(zip_derived_cl473, plain, ( (aElementOf0 @ xn @ szNzAzT0)),
% 31.44/5.72 inference('cnf', [status(esa)], [m__5309])).
% 31.44/5.72 thf(zf_stmt_2, type, zip_tseitin_23 : $i > $o).
% 31.44/5.72 thf(zf_stmt_3, type, zip_tseitin_22 : $i > $i > $o).
% 31.44/5.72 thf(zf_stmt_4, axiom,
% 31.44/5.72 (![W1:$i,W0:$i]:
% 31.44/5.72 ( ( zip_tseitin_22 @ W1 @ W0 ) =>
% 31.44/5.72 ( ( aElementOf0 @
% 31.44/5.72 W1 @
% 31.44/5.72 ( sdtmndt0 @
% 31.44/5.72 ( sdtlpdtrp0 @ xN @ W0 ) @
% 31.44/5.72 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) <=>
% 31.44/5.72 ( zip_tseitin_21 @ W1 @ W0 ) ) ))).
% 31.44/5.72 thf(zf_stmt_5, type, zip_tseitin_21 : $i > $i > $o).
% 31.44/5.72 thf(zf_stmt_6, axiom,
% 31.44/5.72 (![W1:$i,W0:$i]:
% 31.44/5.72 ( ( zip_tseitin_21 @ W1 @ W0 ) <=>
% 31.44/5.72 ( ( aElement0 @ W1 ) &
% 31.44/5.72 ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 31.44/5.72 ( ( W1 ) != ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ))).
% 31.44/5.72 thf(zf_stmt_7, type, zip_tseitin_20 : $i > $o).
% 31.44/5.72 thf(zf_stmt_8, axiom,
% 31.44/5.72 (![W0:$i]:
% 31.44/5.72 ( ( ( ( aSet0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 31.44/5.72 ( ![W1:$i]: ( zip_tseitin_19 @ W1 @ W0 ) ) ) |
% 31.44/5.72 ( aSubsetOf0 @ ( sdtlpdtrp0 @ xN @ W0 ) @ szNzAzT0 ) ) =>
% 31.44/5.72 ( zip_tseitin_20 @ W0 ) ))).
% 31.44/5.72 thf(zf_stmt_9, type, zip_tseitin_19 : $i > $i > $o).
% 31.44/5.72 thf(zf_stmt_10, axiom,
% 31.44/5.72 (![W1:$i,W0:$i]:
% 31.44/5.72 ( ( ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 31.44/5.72 ( aElementOf0 @ W1 @ szNzAzT0 ) ) =>
% 31.44/5.72 ( zip_tseitin_19 @ W1 @ W0 ) ))).
% 31.44/5.72 thf(zf_stmt_11, axiom,
% 31.44/5.72 (( ![W0:$i]:
% 31.44/5.72 ( ( aElementOf0 @ W0 @ szNzAzT0 ) =>
% 31.44/5.72 ( ( ( zip_tseitin_20 @ W0 ) &
% 31.44/5.72 ( isCountable0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) =>
% 31.44/5.72 ( zip_tseitin_23 @ W0 ) ) ) ) &
% 31.44/5.72 ( ( sdtlpdtrp0 @ xN @ sz00 ) = ( xS ) ) &
% 31.44/5.72 ( ( szDzozmdt0 @ xN ) = ( szNzAzT0 ) ) & ( aFunction0 @ xN ))).
% 31.44/5.72 thf(zip_derived_cl232, plain,
% 31.44/5.72 (![X0 : $i]:
% 31.44/5.72 (~ (zip_tseitin_20 @ X0)
% 31.44/5.72 | ~ (isCountable0 @ (sdtlpdtrp0 @ xN @ X0))
% 31.44/5.72 | (zip_tseitin_23 @ X0)
% 31.44/5.72 | ~ (aElementOf0 @ X0 @ szNzAzT0))),
% 31.44/5.72 inference('cnf', [status(esa)], [zf_stmt_11])).
% 31.44/5.72 thf(m__3671, axiom,
% 31.44/5.72 (![W0:$i]:
% 31.44/5.72 ( ( aElementOf0 @ W0 @ szNzAzT0 ) =>
% 31.44/5.72 ( ( aSet0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 31.44/5.72 ( ![W1:$i]:
% 31.44/5.72 ( ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 31.44/5.72 ( aElementOf0 @ W1 @ szNzAzT0 ) ) ) &
% 31.44/5.72 ( aSubsetOf0 @ ( sdtlpdtrp0 @ xN @ W0 ) @ szNzAzT0 ) &
% 31.44/5.72 ( isCountable0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ))).
% 31.44/5.72 thf(zip_derived_cl236, plain,
% 31.44/5.72 (![X0 : $i]:
% 31.44/5.72 ( (isCountable0 @ (sdtlpdtrp0 @ xN @ X0))
% 31.44/5.72 | ~ (aElementOf0 @ X0 @ szNzAzT0))),
% 31.44/5.72 inference('cnf', [status(esa)], [m__3671])).
% 31.44/5.72 thf(zip_derived_cl7001, plain,
% 31.44/5.72 (![X0 : $i]:
% 31.44/5.72 (~ (aElementOf0 @ X0 @ szNzAzT0)
% 31.44/5.72 | (zip_tseitin_23 @ X0)
% 31.44/5.72 | ~ (zip_tseitin_20 @ X0))),
% 31.44/5.72 inference('clc', [status(thm)], [zip_derived_cl232, zip_derived_cl236])).
% 31.44/5.72 thf(zip_derived_cl7021, plain,
% 31.44/5.72 ((~ (zip_tseitin_20 @ xn) | (zip_tseitin_23 @ xn))),
% 31.44/5.72 inference('sup-', [status(thm)], [zip_derived_cl473, zip_derived_cl7001])).
% 31.44/5.72 thf(zip_derived_cl473, plain, ( (aElementOf0 @ xn @ szNzAzT0)),
% 31.44/5.72 inference('cnf', [status(esa)], [m__5309])).
% 31.44/5.72 thf(zip_derived_cl235, plain,
% 31.44/5.72 (![X0 : $i]:
% 31.44/5.72 ( (aSubsetOf0 @ (sdtlpdtrp0 @ xN @ X0) @ szNzAzT0)
% 31.44/5.72 | ~ (aElementOf0 @ X0 @ szNzAzT0))),
% 31.44/5.72 inference('cnf', [status(esa)], [m__3671])).
% 31.44/5.72 thf(zip_derived_cl2192, plain,
% 31.44/5.72 ( (aSubsetOf0 @ (sdtlpdtrp0 @ xN @ xn) @ szNzAzT0)),
% 31.44/5.72 inference('sup-', [status(thm)], [zip_derived_cl473, zip_derived_cl235])).
% 31.44/5.72 thf(zip_derived_cl214, plain,
% 31.44/5.72 (![X0 : $i]:
% 31.44/5.72 ( (zip_tseitin_20 @ X0)
% 31.44/5.72 | ~ (aSubsetOf0 @ (sdtlpdtrp0 @ xN @ X0) @ szNzAzT0))),
% 31.44/5.72 inference('cnf', [status(esa)], [zf_stmt_8])).
% 31.44/5.72 thf(zip_derived_cl12023, plain, ( (zip_tseitin_20 @ xn)),
% 31.44/5.72 inference('sup-', [status(thm)], [zip_derived_cl2192, zip_derived_cl214])).
% 31.44/5.72 thf(zip_derived_cl12045, plain, ( (zip_tseitin_23 @ xn)),
% 31.44/5.72 inference('demod', [status(thm)],
% 31.44/5.72 [zip_derived_cl7021, zip_derived_cl12023])).
% 31.44/5.72 thf(zip_derived_cl12047, plain,
% 31.44/5.72 ( (aElementOf0 @ sk__47 @ (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xn) @ xp))),
% 31.44/5.72 inference('demod', [status(thm)],
% 31.44/5.72 [zip_derived_cl9614, zip_derived_cl12045])).
% 31.44/5.72 thf(zip_derived_cl473, plain, ( (aElementOf0 @ xn @ szNzAzT0)),
% 31.44/5.72 inference('cnf', [status(esa)], [m__5309])).
% 31.44/5.72 thf(zip_derived_cl399, plain,
% 31.44/5.72 (![X0 : $i]:
% 31.44/5.72 ( (aElementOf0 @ (sdtlpdtrp0 @ xe @ X0) @ (sdtlpdtrp0 @ xN @ X0))
% 31.44/5.72 | ~ (aElementOf0 @ X0 @ szNzAzT0))),
% 31.44/5.72 inference('cnf', [status(esa)], [m__4660])).
% 31.44/5.72 thf(zip_derived_cl7092, plain,
% 31.44/5.72 ( (aElementOf0 @ (sdtlpdtrp0 @ xe @ xn) @ (sdtlpdtrp0 @ xN @ xn))),
% 31.44/5.72 inference('sup-', [status(thm)], [zip_derived_cl473, zip_derived_cl399])).
% 31.44/5.72 thf(zip_derived_cl472, plain, (((sdtlpdtrp0 @ xe @ xn) = (xp))),
% 31.44/5.72 inference('cnf', [status(esa)], [m__5309])).
% 31.44/5.72 thf(zip_derived_cl7109, plain,
% 31.44/5.72 ( (aElementOf0 @ xp @ (sdtlpdtrp0 @ xN @ xn))),
% 31.44/5.72 inference('demod', [status(thm)], [zip_derived_cl7092, zip_derived_cl472])).
% 31.44/5.72 thf(mConsDiff, axiom,
% 31.44/5.72 (![W0:$i]:
% 31.44/5.72 ( ( aSet0 @ W0 ) =>
% 31.44/5.72 ( ![W1:$i]:
% 31.44/5.72 ( ( aElementOf0 @ W1 @ W0 ) =>
% 31.44/5.72 ( ( sdtpldt0 @ ( sdtmndt0 @ W0 @ W1 ) @ W1 ) = ( W0 ) ) ) ) ))).
% 31.44/5.72 thf(zip_derived_cl37, plain,
% 31.44/5.72 (![X0 : $i, X1 : $i]:
% 31.44/5.72 (~ (aElementOf0 @ X0 @ X1)
% 31.44/5.72 | ((sdtpldt0 @ (sdtmndt0 @ X1 @ X0) @ X0) = (X1))
% 31.44/5.72 | ~ (aSet0 @ X1))),
% 31.44/5.72 inference('cnf', [status(esa)], [mConsDiff])).
% 31.44/5.72 thf(zip_derived_cl22912, plain,
% 31.44/5.72 ((~ (aSet0 @ (sdtlpdtrp0 @ xN @ xn))
% 31.44/5.72 | ((sdtpldt0 @ (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xn) @ xp) @ xp)
% 31.44/5.72 = (sdtlpdtrp0 @ xN @ xn)))),
% 31.44/5.72 inference('sup-', [status(thm)], [zip_derived_cl7109, zip_derived_cl37])).
% 31.44/5.72 thf(zip_derived_cl473, plain, ( (aElementOf0 @ xn @ szNzAzT0)),
% 31.44/5.72 inference('cnf', [status(esa)], [m__5309])).
% 31.44/5.72 thf(zip_derived_cl233, plain,
% 31.44/5.72 (![X0 : $i]:
% 31.44/5.72 ( (aSet0 @ (sdtlpdtrp0 @ xN @ X0)) | ~ (aElementOf0 @ X0 @ szNzAzT0))),
% 31.44/5.72 inference('cnf', [status(esa)], [m__3671])).
% 31.44/5.72 thf(zip_derived_cl1408, plain, ( (aSet0 @ (sdtlpdtrp0 @ xN @ xn))),
% 31.44/5.72 inference('sup-', [status(thm)], [zip_derived_cl473, zip_derived_cl233])).
% 31.44/5.72 thf(m__5585, axiom,
% 31.44/5.72 (( ( xD ) =
% 31.44/5.72 ( sdtmndt0 @
% 31.44/5.72 ( sdtlpdtrp0 @ xN @ xn ) @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) ) &
% 31.44/5.72 ( ![W0:$i]:
% 31.44/5.72 ( ( aElementOf0 @ W0 @ xD ) <=>
% 31.44/5.72 ( ( aElement0 @ W0 ) &
% 31.44/5.72 ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xn ) ) &
% 31.44/5.72 ( ( W0 ) != ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) ) ) ) &
% 31.44/5.72 ( aSet0 @ xD ) &
% 31.44/5.72 ( ![W0:$i]:
% 31.44/5.72 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xn ) ) =>
% 31.44/5.72 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) @ W0 ) ) ))).
% 31.44/5.72 thf(zip_derived_cl486, plain,
% 31.44/5.72 (((xD)
% 31.44/5.72 = (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xn) @
% 31.44/5.72 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn))))),
% 31.44/5.72 inference('cnf', [status(esa)], [m__5585])).
% 31.44/5.72 thf(zip_derived_cl8487, plain,
% 31.44/5.72 (((xp) = (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn)))),
% 31.44/5.72 inference('demod', [status(thm)], [zip_derived_cl8467, zip_derived_cl472])).
% 31.44/5.72 thf(zip_derived_cl22681, plain,
% 31.44/5.72 (((xD) = (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xn) @ xp))),
% 31.44/5.72 inference('demod', [status(thm)], [zip_derived_cl486, zip_derived_cl8487])).
% 31.44/5.72 thf(zip_derived_cl22941, plain,
% 31.44/5.72 (((sdtpldt0 @ xD @ xp) = (sdtlpdtrp0 @ xN @ xn))),
% 31.44/5.72 inference('demod', [status(thm)],
% 31.44/5.72 [zip_derived_cl22912, zip_derived_cl1408, zip_derived_cl22681])).
% 31.44/5.72 thf(zip_derived_cl24167, plain,
% 31.44/5.72 ( (aElementOf0 @ sk__47 @ (sdtmndt0 @ (sdtpldt0 @ xD @ xp) @ xp))),
% 31.44/5.72 inference('demod', [status(thm)],
% 31.44/5.72 [zip_derived_cl12047, zip_derived_cl22941])).
% 31.44/5.72 thf(zip_derived_cl24177, plain,
% 31.44/5.72 (( (aElementOf0 @ sk__47 @ xD)
% 31.44/5.72 | (aElementOf0 @ xp @ xD)
% 31.44/5.72 | ~ (aSet0 @ xD)
% 31.44/5.72 | ~ (aElement0 @ xp))),
% 31.44/5.72 inference('sup+', [status(thm)], [zip_derived_cl38, zip_derived_cl24167])).
% 31.44/5.72 thf(zip_derived_cl485, plain,
% 31.44/5.72 (![X0 : $i]:
% 31.44/5.72 (((X0) != (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn)))
% 31.44/5.72 | ~ (aElementOf0 @ X0 @ xD))),
% 31.44/5.72 inference('cnf', [status(esa)], [m__5585])).
% 31.44/5.72 thf(zip_derived_cl1339, plain,
% 31.44/5.72 (~ (aElementOf0 @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn)) @ xD)),
% 31.44/5.72 inference('eq_res', [status(thm)], [zip_derived_cl485])).
% 31.44/5.72 thf(zip_derived_cl8487, plain,
% 31.44/5.72 (((xp) = (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn)))),
% 31.44/5.72 inference('demod', [status(thm)], [zip_derived_cl8467, zip_derived_cl472])).
% 31.44/5.72 thf(zip_derived_cl8545, plain, (~ (aElementOf0 @ xp @ xD)),
% 31.44/5.72 inference('demod', [status(thm)],
% 31.44/5.72 [zip_derived_cl1339, zip_derived_cl8487])).
% 31.44/5.72 thf(zip_derived_cl481, plain, ( (aSet0 @ xD)),
% 31.44/5.72 inference('cnf', [status(esa)], [m__5585])).
% 31.44/5.72 thf(m__5147, axiom,
% 31.44/5.72 (( ( xp ) = ( szmzizndt0 @ xQ ) ) &
% 31.44/5.72 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xQ ) => ( sdtlseqdt0 @ xp @ W0 ) ) ) &
% 31.44/5.72 ( aElementOf0 @ xp @ xQ ))).
% 31.44/5.72 thf(zip_derived_cl453, plain, ( (aElementOf0 @ xp @ xQ)),
% 31.44/5.72 inference('cnf', [status(esa)], [m__5147])).
% 31.44/5.72 thf(mEOfElem, axiom,
% 31.44/5.72 (![W0:$i]:
% 31.44/5.72 ( ( aSet0 @ W0 ) =>
% 31.44/5.72 ( ![W1:$i]: ( ( aElementOf0 @ W1 @ W0 ) => ( aElement0 @ W1 ) ) ) ))).
% 31.44/5.72 thf(zip_derived_cl2, plain,
% 31.44/5.72 (![X0 : $i, X1 : $i]:
% 31.44/5.72 (~ (aElementOf0 @ X0 @ X1) | (aElement0 @ X0) | ~ (aSet0 @ X1))),
% 31.44/5.72 inference('cnf', [status(esa)], [mEOfElem])).
% 31.44/5.72 thf(zip_derived_cl543, plain, ((~ (aSet0 @ xQ) | (aElement0 @ xp))),
% 31.44/5.72 inference('sup-', [status(thm)], [zip_derived_cl453, zip_derived_cl2])).
% 31.44/5.72 thf(m__5078, axiom,
% 31.44/5.72 (( aElementOf0 @ xQ @ ( slbdtsldtrb0 @ xO @ xK ) ) &
% 31.44/5.72 ( ( sbrdtbr0 @ xQ ) = ( xK ) ) & ( aSubsetOf0 @ xQ @ xO ) &
% 31.44/5.72 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xQ ) => ( aElementOf0 @ W0 @ xO ) ) ) &
% 31.44/5.72 ( aSet0 @ xQ ))).
% 31.44/5.72 thf(zip_derived_cl439, plain, ( (aSet0 @ xQ)),
% 31.44/5.72 inference('cnf', [status(esa)], [m__5078])).
% 31.44/5.72 thf(zip_derived_cl544, plain, ( (aElement0 @ xp)),
% 31.44/5.72 inference('demod', [status(thm)], [zip_derived_cl543, zip_derived_cl439])).
% 31.44/5.72 thf(zip_derived_cl24178, plain, ( (aElementOf0 @ sk__47 @ xD)),
% 31.44/5.72 inference('demod', [status(thm)],
% 31.44/5.72 [zip_derived_cl24177, zip_derived_cl8545, zip_derived_cl481,
% 31.44/5.72 zip_derived_cl544])).
% 31.44/5.72 thf(zip_derived_cl24182, plain, ($false),
% 31.44/5.72 inference('demod', [status(thm)],
% 31.44/5.72 [zip_derived_cl487, zip_derived_cl24178])).
% 31.44/5.72
% 31.44/5.72 % SZS output end Refutation
% 31.44/5.72
% 31.44/5.72
% 31.44/5.72 % Terminating...
% 32.03/5.87 % Runner terminated.
% 32.03/5.88 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------