%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : NUM630+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.UnfGxbp6d1 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 20.82s 3.55s
% Output : Refutation 20.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM630+3 : TPTP v9.2.0. Released v4.0.0.
% 0.03/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.UnfGxbp6d1 true
% 0.13/0.33 % Computer : n006.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed Oct 1 16:19:53 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % Running portfolio for 300 s
% 0.13/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.34 % Number of cores: 8
% 0.13/0.34 % Python version: Python 3.6.8
% 0.13/0.34 % Running in FO mode
% 0.52/0.63 % Total configuration time : 435
% 0.52/0.63 % Estimated wc time : 1092
% 0.52/0.63 % Estimated cpu time (7 cpus) : 156.0
% 0.52/0.67 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.52/0.70 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.52/0.71 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.52/0.71 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.52/0.71 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.52/0.72 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.53/0.73 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 20.82/3.55 % Solved by fo/fo5.sh.
% 20.82/3.55 % done 3214 iterations in 2.803s
% 20.82/3.55 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 20.82/3.55 % SZS output start Refutation
% 20.82/3.55 thf(zip_tseitin_48_type, type, zip_tseitin_48: $i > $i > $i > $o).
% 20.82/3.55 thf(szDzizrdt0_type, type, szDzizrdt0: $i > $i).
% 20.82/3.55 thf(aSet0_type, type, aSet0: $i > $o).
% 20.82/3.55 thf(szDzozmdt0_type, type, szDzozmdt0: $i > $i).
% 20.82/3.55 thf(aFunction0_type, type, aFunction0: $i > $o).
% 20.82/3.55 thf(slbdtsldtrb0_type, type, slbdtsldtrb0: $i > $i > $i).
% 20.82/3.55 thf(xe_type, type, xe: $i).
% 20.82/3.55 thf(xO_type, type, xO: $i).
% 20.82/3.55 thf(zip_tseitin_45_type, type, zip_tseitin_45: $i > $i > $o).
% 20.82/3.55 thf(zip_tseitin_41_type, type, zip_tseitin_41: $i > $i > $i > $o).
% 20.82/3.55 thf(zip_tseitin_46_type, type, zip_tseitin_46: $i > $i > $i > $o).
% 20.82/3.55 thf(sdtlpdtrp0_type, type, sdtlpdtrp0: $i > $i > $i).
% 20.82/3.55 thf(zip_tseitin_42_type, type, zip_tseitin_42: $i > $i > $o).
% 20.82/3.55 thf(xc_type, type, xc: $i).
% 20.82/3.55 thf(sdtlbdtrb0_type, type, sdtlbdtrb0: $i > $i > $i).
% 20.82/3.55 thf(aElement0_type, type, aElement0: $i > $o).
% 20.82/3.55 thf(zip_tseitin_66_type, type, zip_tseitin_66: $i > $o).
% 20.82/3.55 thf(sbrdtbr0_type, type, sbrdtbr0: $i > $i).
% 20.82/3.55 thf(zip_tseitin_39_type, type, zip_tseitin_39: $i > $i > $o).
% 20.82/3.55 thf(zip_tseitin_43_type, type, zip_tseitin_43: $i > $i > $o).
% 20.82/3.55 thf(zip_tseitin_47_type, type, zip_tseitin_47: $i > $i > $i > $o).
% 20.82/3.55 thf(sdtlseqdt0_type, type, sdtlseqdt0: $i > $i > $o).
% 20.82/3.55 thf(zip_tseitin_49_type, type, zip_tseitin_49: $i > $i > $o).
% 20.82/3.55 thf(sdtmndt0_type, type, sdtmndt0: $i > $i > $i).
% 20.82/3.55 thf(szmzizndt0_type, type, szmzizndt0: $i > $i).
% 20.82/3.55 thf(aSubsetOf0_type, type, aSubsetOf0: $i > $i > $o).
% 20.82/3.55 thf(xC_type, type, xC: $i).
% 20.82/3.55 thf(xQ_type, type, xQ: $i).
% 20.82/3.55 thf(sdtpldt0_type, type, sdtpldt0: $i > $i > $i).
% 20.82/3.55 thf(xp_type, type, xp: $i).
% 20.82/3.55 thf(xP_type, type, xP: $i).
% 20.82/3.55 thf(xd_type, type, xd: $i).
% 20.82/3.55 thf(zip_tseitin_38_type, type, zip_tseitin_38: $i > $i > $o).
% 20.82/3.55 thf(zip_tseitin_40_type, type, zip_tseitin_40: $i > $o).
% 20.82/3.55 thf(xk_type, type, xk: $i).
% 20.82/3.55 thf(xK_type, type, xK: $i).
% 20.82/3.55 thf(szNzAzT0_type, type, szNzAzT0: $i).
% 20.82/3.55 thf(xN_type, type, xN: $i).
% 20.82/3.55 thf(zip_tseitin_44_type, type, zip_tseitin_44: $i > $i > $o).
% 20.82/3.55 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 20.82/3.55 thf(zip_tseitin_37_type, type, zip_tseitin_37: $i > $o).
% 20.82/3.55 thf(xD_type, type, xD: $i).
% 20.82/3.55 thf(xn_type, type, xn: $i).
% 20.82/3.55 thf(m__5599, axiom,
% 20.82/3.55 (( aElementOf0 @ xP @ ( slbdtsldtrb0 @ xD @ xk ) ) &
% 20.82/3.55 ( aSubsetOf0 @ xP @ xD ) &
% 20.82/3.55 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xP ) => ( aElementOf0 @ W0 @ xD ) ) ))).
% 20.82/3.55 thf(zip_derived_cl488, plain, ( (aSubsetOf0 @ xP @ xD)),
% 20.82/3.55 inference('cnf', [status(esa)], [m__5599])).
% 20.82/3.55 thf(m__5309, axiom,
% 20.82/3.55 (( ( sdtlpdtrp0 @ xe @ xn ) = ( xp ) ) & ( aElementOf0 @ xn @ szNzAzT0 ) &
% 20.82/3.55 ( aElementOf0 @ xn @ ( sdtlbdtrb0 @ xd @ ( szDzizrdt0 @ xd ) ) ) &
% 20.82/3.55 ( ( sdtlpdtrp0 @ xd @ xn ) = ( szDzizrdt0 @ xd ) ) &
% 20.82/3.55 ( aElementOf0 @ xn @ ( szDzozmdt0 @ xd ) ))).
% 20.82/3.55 thf(zip_derived_cl473, plain, ( (aElementOf0 @ xn @ szNzAzT0)),
% 20.82/3.55 inference('cnf', [status(esa)], [m__5309])).
% 20.82/3.55 thf(m__4660, axiom,
% 20.82/3.55 (( ![W0:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W0 @ szNzAzT0 ) =>
% 20.82/3.55 ( ( aElementOf0 @ ( sdtlpdtrp0 @ xe @ W0 ) @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 20.82/3.55 ( ![W1:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 20.82/3.55 ( sdtlseqdt0 @ ( sdtlpdtrp0 @ xe @ W0 ) @ W1 ) ) ) &
% 20.82/3.55 ( ( sdtlpdtrp0 @ xe @ W0 ) =
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) &
% 20.82/3.55 ( ( szDzozmdt0 @ xe ) = ( szNzAzT0 ) ) & ( aFunction0 @ xe ))).
% 20.82/3.55 thf(zip_derived_cl401, plain,
% 20.82/3.55 (![X0 : $i]:
% 20.82/3.55 (((sdtlpdtrp0 @ xe @ X0) = (szmzizndt0 @ (sdtlpdtrp0 @ xN @ X0)))
% 20.82/3.55 | ~ (aElementOf0 @ X0 @ szNzAzT0))),
% 20.82/3.55 inference('cnf', [status(esa)], [m__4660])).
% 20.82/3.55 thf(zip_derived_cl1716, plain,
% 20.82/3.55 (((sdtlpdtrp0 @ xe @ xn) = (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn)))),
% 20.82/3.55 inference('sup-', [status(thm)], [zip_derived_cl473, zip_derived_cl401])).
% 20.82/3.55 thf(zip_derived_cl472, plain, (((sdtlpdtrp0 @ xe @ xn) = (xp))),
% 20.82/3.55 inference('cnf', [status(esa)], [m__5309])).
% 20.82/3.55 thf(zip_derived_cl1723, plain,
% 20.82/3.55 (((xp) = (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn)))),
% 20.82/3.55 inference('demod', [status(thm)], [zip_derived_cl1716, zip_derived_cl472])).
% 20.82/3.55 thf(m__4151, axiom,
% 20.82/3.55 (( aFunction0 @ xC ) & ( ( szDzozmdt0 @ xC ) = ( szNzAzT0 ) ) &
% 20.82/3.55 ( ![W0:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W0 @ szNzAzT0 ) =>
% 20.82/3.55 ( ( ![W1:$i]:
% 20.82/3.55 ( ( ( ( ( ![W2:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W2 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 20.82/3.55 ( sdtlseqdt0 @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ W2 ) ) ) &
% 20.82/3.55 ( aElementOf0 @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) ) ) =>
% 20.82/3.55 ( ( ( ![W2:$i]:
% 20.82/3.55 ( ( aElementOf0 @
% 20.82/3.55 W2 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) <=>
% 20.82/3.55 ( ( ( W2 ) !=
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) &
% 20.82/3.55 ( aElementOf0 @ W2 @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 20.82/3.55 ( aElement0 @ W2 ) ) ) ) &
% 20.82/3.55 ( aSet0 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) =>
% 20.82/3.55 ( ( aElementOf0 @
% 20.82/3.55 W1 @
% 20.82/3.55 ( slbdtsldtrb0 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) @
% 20.82/3.55 xk ) ) |
% 20.82/3.55 ( ( ( sbrdtbr0 @ W1 ) = ( xk ) ) &
% 20.82/3.55 ( ( aSubsetOf0 @
% 20.82/3.55 W1 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) |
% 20.82/3.55 ( ![W2:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W2 @ W1 ) =>
% 20.82/3.55 ( aElementOf0 @
% 20.82/3.55 W2 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) ) ) ) ) ) &
% 20.82/3.55 ( aSet0 @ W1 ) ) =>
% 20.82/3.55 ( ( ( sdtlpdtrp0 @ ( sdtlpdtrp0 @ xC @ W0 ) @ W1 ) =
% 20.82/3.55 ( sdtlpdtrp0 @
% 20.82/3.55 xc @
% 20.82/3.55 ( sdtpldt0 @
% 20.82/3.55 W1 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) &
% 20.82/3.55 ( ![W2:$i]:
% 20.82/3.55 ( ( aElementOf0 @
% 20.82/3.55 W2 @
% 20.82/3.55 ( sdtpldt0 @
% 20.82/3.55 W1 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) <=>
% 20.82/3.55 ( ( ( ( W2 ) = ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) |
% 20.82/3.55 ( aElementOf0 @ W2 @ W1 ) ) &
% 20.82/3.55 ( aElement0 @ W2 ) ) ) ) &
% 20.82/3.55 ( ![W2:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W2 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 20.82/3.55 ( sdtlseqdt0 @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ W2 ) ) ) &
% 20.82/3.55 ( aElementOf0 @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) &
% 20.82/3.55 ( ( szDzozmdt0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) =
% 20.82/3.55 ( slbdtsldtrb0 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) @
% 20.82/3.55 xk ) ) &
% 20.82/3.55 ( ![W1:$i]:
% 20.82/3.55 ( ( ( aElementOf0 @ W1 @ ( szDzozmdt0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) ) =>
% 20.82/3.55 ( ( ( sbrdtbr0 @ W1 ) = ( xk ) ) &
% 20.82/3.55 ( aSubsetOf0 @
% 20.82/3.55 W1 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 20.82/3.55 ( ![W2:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W2 @ W1 ) =>
% 20.82/3.55 ( aElementOf0 @
% 20.82/3.55 W2 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) &
% 20.82/3.55 ( aSet0 @ W1 ) ) ) &
% 20.82/3.55 ( ( ( ( sbrdtbr0 @ W1 ) = ( xk ) ) &
% 20.82/3.55 ( ( aSubsetOf0 @
% 20.82/3.55 W1 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) |
% 20.82/3.55 ( ( ![W2:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W2 @ W1 ) =>
% 20.82/3.55 ( aElementOf0 @
% 20.82/3.55 W2 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) &
% 20.82/3.55 ( aSet0 @ W1 ) ) ) ) =>
% 20.82/3.55 ( aElementOf0 @ W1 @ ( szDzozmdt0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) ) ) ) ) &
% 20.82/3.55 ( ![W1:$i]:
% 20.82/3.55 ( ( aElementOf0 @
% 20.82/3.55 W1 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) <=>
% 20.82/3.55 ( ( ( W1 ) != ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) &
% 20.82/3.55 ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 20.82/3.55 ( aElement0 @ W1 ) ) ) ) &
% 20.82/3.55 ( aSet0 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 20.82/3.55 ( ![W1:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 20.82/3.55 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ W1 ) ) ) &
% 20.82/3.55 ( aElementOf0 @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 20.82/3.55 ( aFunction0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) ) ) ))).
% 20.82/3.55 thf(zf_stmt_0, axiom,
% 20.82/3.55 (![W1:$i,W0:$i]:
% 20.82/3.55 ( ( ( ![W2:$i]: ( zip_tseitin_41 @ W2 @ W1 @ W0 ) ) |
% 20.82/3.55 ( aSubsetOf0 @
% 20.82/3.55 W1 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) =>
% 20.82/3.55 ( zip_tseitin_42 @ W1 @ W0 ) ))).
% 20.82/3.55 thf(zip_derived_cl294, plain,
% 20.82/3.55 (![X0 : $i, X1 : $i]:
% 20.82/3.55 ( (zip_tseitin_42 @ X0 @ X1)
% 20.82/3.55 | ~ (aSubsetOf0 @ X0 @
% 20.82/3.55 (sdtmndt0 @ (sdtlpdtrp0 @ xN @ X1) @
% 20.82/3.55 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ X1)))))),
% 20.82/3.55 inference('cnf', [status(esa)], [zf_stmt_0])).
% 20.82/3.55 thf(zip_derived_cl12954, plain,
% 20.82/3.55 (![X0 : $i]:
% 20.82/3.55 (~ (aSubsetOf0 @ X0 @ (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xn) @ xp))
% 20.82/3.55 | (zip_tseitin_42 @ X0 @ xn))),
% 20.82/3.55 inference('sup-', [status(thm)], [zip_derived_cl1723, zip_derived_cl294])).
% 20.82/3.55 thf(m__5585, axiom,
% 20.82/3.55 (( ( xD ) =
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ xn ) @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) ) &
% 20.82/3.55 ( ![W0:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W0 @ xD ) <=>
% 20.82/3.55 ( ( aElement0 @ W0 ) &
% 20.82/3.55 ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xn ) ) &
% 20.82/3.55 ( ( W0 ) != ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) ) ) ) &
% 20.82/3.55 ( aSet0 @ xD ) &
% 20.82/3.55 ( ![W0:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xn ) ) =>
% 20.82/3.55 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) @ W0 ) ) ))).
% 20.82/3.55 thf(zip_derived_cl486, plain,
% 20.82/3.55 (((xD)
% 20.82/3.55 = (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xn) @
% 20.82/3.55 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn))))),
% 20.82/3.55 inference('cnf', [status(esa)], [m__5585])).
% 20.82/3.55 thf(zip_derived_cl1723, plain,
% 20.82/3.55 (((xp) = (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn)))),
% 20.82/3.55 inference('demod', [status(thm)], [zip_derived_cl1716, zip_derived_cl472])).
% 20.82/3.55 thf(zip_derived_cl4773, plain,
% 20.82/3.55 (((xD) = (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xn) @ xp))),
% 20.82/3.55 inference('demod', [status(thm)], [zip_derived_cl486, zip_derived_cl1723])).
% 20.82/3.55 thf(zip_derived_cl12960, plain,
% 20.82/3.55 (![X0 : $i]: (~ (aSubsetOf0 @ X0 @ xD) | (zip_tseitin_42 @ X0 @ xn))),
% 20.82/3.55 inference('demod', [status(thm)],
% 20.82/3.55 [zip_derived_cl12954, zip_derived_cl4773])).
% 20.82/3.55 thf(zip_derived_cl12969, plain, ( (zip_tseitin_42 @ xP @ xn)),
% 20.82/3.55 inference('sup-', [status(thm)], [zip_derived_cl488, zip_derived_cl12960])).
% 20.82/3.55 thf(m__5217, axiom, (( sbrdtbr0 @ xP ) = ( xk ))).
% 20.82/3.55 thf(zip_derived_cl470, plain, (((sbrdtbr0 @ xP) = (xk))),
% 20.82/3.55 inference('cnf', [status(esa)], [m__5217])).
% 20.82/3.55 thf(zf_stmt_1, axiom,
% 20.82/3.55 (![W1:$i,W0:$i]:
% 20.82/3.55 ( ( ( ( zip_tseitin_42 @ W1 @ W0 ) & ( ( sbrdtbr0 @ W1 ) = ( xk ) ) ) |
% 20.82/3.55 ( aElementOf0 @
% 20.82/3.55 W1 @
% 20.82/3.55 ( slbdtsldtrb0 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) @
% 20.82/3.55 xk ) ) ) =>
% 20.82/3.55 ( zip_tseitin_43 @ W1 @ W0 ) ))).
% 20.82/3.55 thf(zip_derived_cl295, plain,
% 20.82/3.55 (![X0 : $i, X1 : $i]:
% 20.82/3.55 ( (zip_tseitin_43 @ X0 @ X1)
% 20.82/3.55 | ~ (zip_tseitin_42 @ X0 @ X1)
% 20.82/3.55 | ((sbrdtbr0 @ X0) != (xk)))),
% 20.82/3.55 inference('cnf', [status(esa)], [zf_stmt_1])).
% 20.82/3.55 thf(zip_derived_cl4886, plain,
% 20.82/3.55 (![X0 : $i]:
% 20.82/3.55 (((xk) != (xk))
% 20.82/3.55 | ~ (zip_tseitin_42 @ xP @ X0)
% 20.82/3.55 | (zip_tseitin_43 @ xP @ X0))),
% 20.82/3.55 inference('sup-', [status(thm)], [zip_derived_cl470, zip_derived_cl295])).
% 20.82/3.55 thf(zip_derived_cl4888, plain,
% 20.82/3.55 (![X0 : $i]: ( (zip_tseitin_43 @ xP @ X0) | ~ (zip_tseitin_42 @ xP @ X0))),
% 20.82/3.55 inference('simplify', [status(thm)], [zip_derived_cl4886])).
% 20.82/3.55 thf(zip_derived_cl12972, plain, ( (zip_tseitin_43 @ xP @ xn)),
% 20.82/3.55 inference('sup-', [status(thm)],
% 20.82/3.55 [zip_derived_cl12969, zip_derived_cl4888])).
% 20.82/3.55 thf(zf_stmt_2, axiom,
% 20.82/3.55 (![W1:$i,W0:$i]:
% 20.82/3.55 ( ( ( zip_tseitin_40 @ W0 ) => ( zip_tseitin_43 @ W1 @ W0 ) ) =>
% 20.82/3.55 ( zip_tseitin_44 @ W1 @ W0 ) ))).
% 20.82/3.55 thf(zip_derived_cl297, plain,
% 20.82/3.55 (![X0 : $i, X1 : $i]:
% 20.82/3.55 ( (zip_tseitin_44 @ X0 @ X1) | ~ (zip_tseitin_43 @ X0 @ X1))),
% 20.82/3.55 inference('cnf', [status(esa)], [zf_stmt_2])).
% 20.82/3.55 thf(zip_derived_cl12973, plain, ( (zip_tseitin_44 @ xP @ xn)),
% 20.82/3.55 inference('sup-', [status(thm)], [zip_derived_cl12972, zip_derived_cl297])).
% 20.82/3.55 thf(zf_stmt_3, axiom,
% 20.82/3.55 (![W1:$i,W0:$i]:
% 20.82/3.55 ( ( ( zip_tseitin_37 @ W0 ) => ( zip_tseitin_44 @ W1 @ W0 ) ) =>
% 20.82/3.55 ( zip_tseitin_45 @ W1 @ W0 ) ))).
% 20.82/3.55 thf(zip_derived_cl299, plain,
% 20.82/3.55 (![X0 : $i, X1 : $i]:
% 20.82/3.55 ( (zip_tseitin_45 @ X0 @ X1) | ~ (zip_tseitin_44 @ X0 @ X1))),
% 20.82/3.55 inference('cnf', [status(esa)], [zf_stmt_3])).
% 20.82/3.55 thf(zip_derived_cl12974, plain, ( (zip_tseitin_45 @ xP @ xn)),
% 20.82/3.55 inference('sup-', [status(thm)], [zip_derived_cl12973, zip_derived_cl299])).
% 20.82/3.55 thf(zip_derived_cl473, plain, ( (aElementOf0 @ xn @ szNzAzT0)),
% 20.82/3.55 inference('cnf', [status(esa)], [m__5309])).
% 20.82/3.55 thf(zf_stmt_4, type, zip_tseitin_49 : $i > $i > $o).
% 20.82/3.55 thf(zf_stmt_5, axiom,
% 20.82/3.55 (![W1:$i,W0:$i]:
% 20.82/3.55 ( ( zip_tseitin_49 @ W1 @ W0 ) =>
% 20.82/3.55 ( ( aElementOf0 @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 20.82/3.55 ( ![W2:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W2 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 20.82/3.55 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ W2 ) ) ) &
% 20.82/3.55 ( ![W2:$i]: ( zip_tseitin_48 @ W2 @ W1 @ W0 ) ) &
% 20.82/3.55 ( ( sdtlpdtrp0 @ ( sdtlpdtrp0 @ xC @ W0 ) @ W1 ) =
% 20.82/3.55 ( sdtlpdtrp0 @
% 20.82/3.55 xc @ ( sdtpldt0 @ W1 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) ))).
% 20.82/3.55 thf(zf_stmt_6, type, zip_tseitin_48 : $i > $i > $i > $o).
% 20.82/3.55 thf(zf_stmt_7, axiom,
% 20.82/3.55 (![W2:$i,W1:$i,W0:$i]:
% 20.82/3.55 ( ( zip_tseitin_48 @ W2 @ W1 @ W0 ) =>
% 20.82/3.55 ( ( aElementOf0 @
% 20.82/3.55 W2 @ ( sdtpldt0 @ W1 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) <=>
% 20.82/3.55 ( zip_tseitin_47 @ W2 @ W1 @ W0 ) ) ))).
% 20.82/3.55 thf(zf_stmt_8, type, zip_tseitin_47 : $i > $i > $i > $o).
% 20.82/3.55 thf(zf_stmt_9, axiom,
% 20.82/3.55 (![W2:$i,W1:$i,W0:$i]:
% 20.82/3.55 ( ( zip_tseitin_47 @ W2 @ W1 @ W0 ) <=>
% 20.82/3.55 ( ( aElement0 @ W2 ) & ( zip_tseitin_46 @ W2 @ W1 @ W0 ) ) ))).
% 20.82/3.55 thf(zf_stmt_10, type, zip_tseitin_46 : $i > $i > $i > $o).
% 20.82/3.55 thf(zf_stmt_11, axiom,
% 20.82/3.55 (![W2:$i,W1:$i,W0:$i]:
% 20.82/3.55 ( ( zip_tseitin_46 @ W2 @ W1 @ W0 ) <=>
% 20.82/3.55 ( ( aElementOf0 @ W2 @ W1 ) |
% 20.82/3.55 ( ( W2 ) = ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ))).
% 20.82/3.55 thf(zf_stmt_12, type, zip_tseitin_45 : $i > $i > $o).
% 20.82/3.55 thf(zf_stmt_13, type, zip_tseitin_44 : $i > $i > $o).
% 20.82/3.55 thf(zf_stmt_14, type, zip_tseitin_43 : $i > $i > $o).
% 20.82/3.55 thf(zf_stmt_15, type, zip_tseitin_42 : $i > $i > $o).
% 20.82/3.55 thf(zf_stmt_16, type, zip_tseitin_41 : $i > $i > $i > $o).
% 20.82/3.55 thf(zf_stmt_17, axiom,
% 20.82/3.55 (![W2:$i,W1:$i,W0:$i]:
% 20.82/3.55 ( ( ( aElementOf0 @ W2 @ W1 ) =>
% 20.82/3.55 ( aElementOf0 @
% 20.82/3.55 W2 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) =>
% 20.82/3.55 ( zip_tseitin_41 @ W2 @ W1 @ W0 ) ))).
% 20.82/3.55 thf(zf_stmt_18, type, zip_tseitin_40 : $i > $o).
% 20.82/3.55 thf(zf_stmt_19, axiom,
% 20.82/3.55 (![W0:$i]:
% 20.82/3.55 ( ( zip_tseitin_40 @ W0 ) =>
% 20.82/3.55 ( ( aSet0 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 20.82/3.55 ( ![W2:$i]: ( zip_tseitin_39 @ W2 @ W0 ) ) ) ))).
% 20.82/3.55 thf(zf_stmt_20, type, zip_tseitin_39 : $i > $i > $o).
% 20.82/3.55 thf(zf_stmt_21, axiom,
% 20.82/3.55 (![W2:$i,W0:$i]:
% 20.82/3.55 ( ( zip_tseitin_39 @ W2 @ W0 ) =>
% 20.82/3.55 ( ( aElementOf0 @
% 20.82/3.55 W2 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) <=>
% 20.82/3.55 ( zip_tseitin_38 @ W2 @ W0 ) ) ))).
% 20.82/3.55 thf(zf_stmt_22, type, zip_tseitin_38 : $i > $i > $o).
% 20.82/3.55 thf(zf_stmt_23, axiom,
% 20.82/3.55 (![W2:$i,W0:$i]:
% 20.82/3.55 ( ( zip_tseitin_38 @ W2 @ W0 ) <=>
% 20.82/3.55 ( ( aElement0 @ W2 ) &
% 20.82/3.55 ( aElementOf0 @ W2 @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 20.82/3.55 ( ( W2 ) != ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ))).
% 20.82/3.55 thf(zf_stmt_24, type, zip_tseitin_37 : $i > $o).
% 20.82/3.55 thf(zf_stmt_25, axiom,
% 20.82/3.55 (![W0:$i]:
% 20.82/3.55 ( ( zip_tseitin_37 @ W0 ) =>
% 20.82/3.55 ( ( aElementOf0 @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 20.82/3.55 ( ![W2:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W2 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 20.82/3.55 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ W2 ) ) ) ) ))).
% 20.82/3.55 thf(zf_stmt_26, axiom,
% 20.82/3.55 (( ![W0:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W0 @ szNzAzT0 ) =>
% 20.82/3.55 ( ( aFunction0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) &
% 20.82/3.55 ( aElementOf0 @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 20.82/3.55 ( ![W1:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 20.82/3.55 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ W1 ) ) ) &
% 20.82/3.55 ( aSet0 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 20.82/3.55 ( ![W1:$i]:
% 20.82/3.55 ( ( aElementOf0 @
% 20.82/3.55 W1 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) <=>
% 20.82/3.55 ( ( aElement0 @ W1 ) &
% 20.82/3.55 ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 20.82/3.55 ( ( W1 ) != ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) &
% 20.82/3.55 ( ![W1:$i]:
% 20.82/3.55 ( ( ( ( ( ( aSet0 @ W1 ) &
% 20.82/3.55 ( ![W2:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W2 @ W1 ) =>
% 20.82/3.55 ( aElementOf0 @
% 20.82/3.55 W2 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) ) |
% 20.82/3.55 ( aSubsetOf0 @
% 20.82/3.55 W1 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) &
% 20.82/3.55 ( ( sbrdtbr0 @ W1 ) = ( xk ) ) ) =>
% 20.82/3.55 ( aElementOf0 @ W1 @ ( szDzozmdt0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) ) ) &
% 20.82/3.55 ( ( aElementOf0 @ W1 @ ( szDzozmdt0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) ) =>
% 20.82/3.55 ( ( aSet0 @ W1 ) &
% 20.82/3.55 ( ![W2:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W2 @ W1 ) =>
% 20.82/3.55 ( aElementOf0 @
% 20.82/3.55 W2 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) &
% 20.82/3.55 ( aSubsetOf0 @
% 20.82/3.55 W1 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 20.82/3.55 ( ( sbrdtbr0 @ W1 ) = ( xk ) ) ) ) ) ) &
% 20.82/3.55 ( ( szDzozmdt0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) =
% 20.82/3.55 ( slbdtsldtrb0 @
% 20.82/3.55 ( sdtmndt0 @
% 20.82/3.55 ( sdtlpdtrp0 @ xN @ W0 ) @
% 20.82/3.55 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) @
% 20.82/3.55 xk ) ) &
% 20.82/3.55 ( ![W1:$i]:
% 20.82/3.55 ( ( ( aSet0 @ W1 ) & ( zip_tseitin_45 @ W1 @ W0 ) ) =>
% 20.82/3.55 ( zip_tseitin_49 @ W1 @ W0 ) ) ) ) ) ) &
% 20.82/3.55 ( ( szDzozmdt0 @ xC ) = ( szNzAzT0 ) ) & ( aFunction0 @ xC ))).
% 20.82/3.55 thf(zip_derived_cl331, plain,
% 20.82/3.55 (![X0 : $i, X1 : $i]:
% 20.82/3.55 (~ (aSet0 @ X0)
% 20.82/3.55 | ~ (zip_tseitin_45 @ X0 @ X1)
% 20.82/3.55 | (zip_tseitin_49 @ X0 @ X1)
% 20.82/3.55 | ~ (aElementOf0 @ X1 @ szNzAzT0))),
% 20.82/3.55 inference('cnf', [status(esa)], [zf_stmt_26])).
% 20.82/3.55 thf(zip_derived_cl6034, plain,
% 20.82/3.55 (![X0 : $i]:
% 20.82/3.55 ( (zip_tseitin_49 @ X0 @ xn)
% 20.82/3.55 | ~ (zip_tseitin_45 @ X0 @ xn)
% 20.82/3.55 | ~ (aSet0 @ X0))),
% 20.82/3.55 inference('sup-', [status(thm)], [zip_derived_cl473, zip_derived_cl331])).
% 20.82/3.55 thf(zip_derived_cl12976, plain,
% 20.82/3.55 ((~ (aSet0 @ xP) | (zip_tseitin_49 @ xP @ xn))),
% 20.82/3.55 inference('sup-', [status(thm)],
% 20.82/3.55 [zip_derived_cl12974, zip_derived_cl6034])).
% 20.82/3.55 thf(m__5164, axiom,
% 20.82/3.55 (( ( xP ) = ( sdtmndt0 @ xQ @ ( szmzizndt0 @ xQ ) ) ) &
% 20.82/3.55 ( ![W0:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W0 @ xP ) <=>
% 20.82/3.55 ( ( aElement0 @ W0 ) & ( aElementOf0 @ W0 @ xQ ) &
% 20.82/3.55 ( ( W0 ) != ( szmzizndt0 @ xQ ) ) ) ) ) &
% 20.82/3.55 ( ![W0:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W0 @ xQ ) => ( sdtlseqdt0 @ ( szmzizndt0 @ xQ ) @ W0 ) ) ) &
% 20.82/3.55 ( aSet0 @ xP ))).
% 20.82/3.55 thf(zip_derived_cl456, plain, ( (aSet0 @ xP)),
% 20.82/3.55 inference('cnf', [status(esa)], [m__5164])).
% 20.82/3.55 thf(zip_derived_cl12978, plain, ( (zip_tseitin_49 @ xP @ xn)),
% 20.82/3.55 inference('demod', [status(thm)],
% 20.82/3.55 [zip_derived_cl12976, zip_derived_cl456])).
% 20.82/3.55 thf(zip_derived_cl312, plain,
% 20.82/3.55 (![X0 : $i, X1 : $i]:
% 20.82/3.55 (((sdtlpdtrp0 @ (sdtlpdtrp0 @ xC @ X1) @ X0)
% 20.82/3.55 = (sdtlpdtrp0 @ xc @
% 20.82/3.55 (sdtpldt0 @ X0 @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ X1)))))
% 20.82/3.55 | ~ (zip_tseitin_49 @ X0 @ X1))),
% 20.82/3.55 inference('cnf', [status(esa)], [zf_stmt_5])).
% 20.82/3.55 thf(zip_derived_cl13307, plain,
% 20.82/3.55 (((sdtlpdtrp0 @ (sdtlpdtrp0 @ xC @ xn) @ xP)
% 20.82/3.55 = (sdtlpdtrp0 @ xc @
% 20.82/3.55 (sdtpldt0 @ xP @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn)))))),
% 20.82/3.55 inference('sup-', [status(thm)], [zip_derived_cl12978, zip_derived_cl312])).
% 20.82/3.55 thf(zip_derived_cl1723, plain,
% 20.82/3.55 (((xp) = (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn)))),
% 20.82/3.55 inference('demod', [status(thm)], [zip_derived_cl1716, zip_derived_cl472])).
% 20.82/3.55 thf(m__5147, axiom,
% 20.82/3.55 (( ( xp ) = ( szmzizndt0 @ xQ ) ) &
% 20.82/3.55 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xQ ) => ( sdtlseqdt0 @ xp @ W0 ) ) ) &
% 20.82/3.55 ( aElementOf0 @ xp @ xQ ))).
% 20.82/3.55 thf(zip_derived_cl453, plain, ( (aElementOf0 @ xp @ xQ)),
% 20.82/3.55 inference('cnf', [status(esa)], [m__5147])).
% 20.82/3.55 thf(mConsDiff, axiom,
% 20.82/3.55 (![W0:$i]:
% 20.82/3.55 ( ( aSet0 @ W0 ) =>
% 20.82/3.55 ( ![W1:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W1 @ W0 ) =>
% 20.82/3.55 ( ( sdtpldt0 @ ( sdtmndt0 @ W0 @ W1 ) @ W1 ) = ( W0 ) ) ) ) ))).
% 20.82/3.55 thf(zip_derived_cl37, plain,
% 20.82/3.55 (![X0 : $i, X1 : $i]:
% 20.82/3.55 (~ (aElementOf0 @ X0 @ X1)
% 20.82/3.55 | ((sdtpldt0 @ (sdtmndt0 @ X1 @ X0) @ X0) = (X1))
% 20.82/3.55 | ~ (aSet0 @ X1))),
% 20.82/3.55 inference('cnf', [status(esa)], [mConsDiff])).
% 20.82/3.55 thf(zip_derived_cl1828, plain,
% 20.82/3.55 ((~ (aSet0 @ xQ) | ((sdtpldt0 @ (sdtmndt0 @ xQ @ xp) @ xp) = (xQ)))),
% 20.82/3.55 inference('sup-', [status(thm)], [zip_derived_cl453, zip_derived_cl37])).
% 20.82/3.55 thf(m__5078, axiom,
% 20.82/3.55 (( aElementOf0 @ xQ @ ( slbdtsldtrb0 @ xO @ xK ) ) &
% 20.82/3.55 ( ( sbrdtbr0 @ xQ ) = ( xK ) ) & ( aSubsetOf0 @ xQ @ xO ) &
% 20.82/3.55 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xQ ) => ( aElementOf0 @ W0 @ xO ) ) ) &
% 20.82/3.55 ( aSet0 @ xQ ))).
% 20.82/3.55 thf(zip_derived_cl439, plain, ( (aSet0 @ xQ)),
% 20.82/3.55 inference('cnf', [status(esa)], [m__5078])).
% 20.82/3.55 thf(zip_derived_cl462, plain, (((xP) = (sdtmndt0 @ xQ @ (szmzizndt0 @ xQ)))),
% 20.82/3.55 inference('cnf', [status(esa)], [m__5164])).
% 20.82/3.55 thf(zip_derived_cl455, plain, (((xp) = (szmzizndt0 @ xQ))),
% 20.82/3.55 inference('cnf', [status(esa)], [m__5147])).
% 20.82/3.55 thf(zip_derived_cl958, plain, (((xP) = (sdtmndt0 @ xQ @ xp))),
% 20.82/3.55 inference('demod', [status(thm)], [zip_derived_cl462, zip_derived_cl455])).
% 20.82/3.55 thf(zip_derived_cl1852, plain, (((sdtpldt0 @ xP @ xp) = (xQ))),
% 20.82/3.55 inference('demod', [status(thm)],
% 20.82/3.55 [zip_derived_cl1828, zip_derived_cl439, zip_derived_cl958])).
% 20.82/3.55 thf(zip_derived_cl13310, plain,
% 20.82/3.55 (((sdtlpdtrp0 @ (sdtlpdtrp0 @ xC @ xn) @ xP) = (sdtlpdtrp0 @ xc @ xQ))),
% 20.82/3.55 inference('demod', [status(thm)],
% 20.82/3.55 [zip_derived_cl13307, zip_derived_cl1723, zip_derived_cl1852])).
% 20.82/3.55 thf(m__, conjecture,
% 20.82/3.55 (( ![W0:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xn ) ) =>
% 20.82/3.55 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) @ W0 ) ) ) =>
% 20.82/3.55 ( ( ( ![W0:$i]:
% 20.82/3.55 ( ( aElementOf0 @
% 20.82/3.55 W0 @
% 20.82/3.55 ( sdtpldt0 @ xP @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) ) <=>
% 20.82/3.55 ( ( ( ( W0 ) = ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) |
% 20.82/3.55 ( aElementOf0 @ W0 @ xP ) ) &
% 20.82/3.55 ( aElement0 @ W0 ) ) ) ) &
% 20.82/3.55 ( aSet0 @
% 20.82/3.55 ( sdtpldt0 @ xP @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) ) ) =>
% 20.82/3.55 ( ( sdtlpdtrp0 @
% 20.82/3.55 xc @ ( sdtpldt0 @ xP @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) ) =
% 20.82/3.55 ( sdtlpdtrp0 @ ( sdtlpdtrp0 @ xC @ xn ) @ xP ) ) ))).
% 20.82/3.55 thf(zf_stmt_27, type, zip_tseitin_66 : $i > $o).
% 20.82/3.55 thf(zf_stmt_28, axiom,
% 20.82/3.55 (![W0:$i]:
% 20.82/3.55 ( ( zip_tseitin_66 @ W0 ) <=>
% 20.82/3.55 ( ( aElement0 @ W0 ) &
% 20.82/3.55 ( ( aElementOf0 @ W0 @ xP ) |
% 20.82/3.55 ( ( W0 ) = ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) ) ) ))).
% 20.82/3.55 thf(zf_stmt_29, conjecture,
% 20.82/3.55 (( ![W0:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xn ) ) =>
% 20.82/3.55 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) @ W0 ) ) ) =>
% 20.82/3.55 ( ( ( aSet0 @
% 20.82/3.55 ( sdtpldt0 @ xP @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) ) &
% 20.82/3.55 ( ![W0:$i]:
% 20.82/3.55 ( ( aElementOf0 @
% 20.82/3.55 W0 @
% 20.82/3.55 ( sdtpldt0 @ xP @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) ) <=>
% 20.82/3.55 ( zip_tseitin_66 @ W0 ) ) ) ) =>
% 20.82/3.55 ( ( sdtlpdtrp0 @
% 20.82/3.55 xc @ ( sdtpldt0 @ xP @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) ) =
% 20.82/3.55 ( sdtlpdtrp0 @ ( sdtlpdtrp0 @ xC @ xn ) @ xP ) ) ))).
% 20.82/3.55 thf(zf_stmt_30, negated_conjecture,
% 20.82/3.55 (~( ( ![W0:$i]:
% 20.82/3.55 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xn ) ) =>
% 20.82/3.55 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) @ W0 ) ) ) =>
% 20.82/3.55 ( ( ( aSet0 @
% 20.82/3.55 ( sdtpldt0 @ xP @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) ) &
% 20.82/3.55 ( ![W0:$i]:
% 20.82/3.55 ( ( aElementOf0 @
% 20.82/3.55 W0 @
% 20.82/3.55 ( sdtpldt0 @ xP @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) ) <=>
% 20.82/3.55 ( zip_tseitin_66 @ W0 ) ) ) ) =>
% 20.82/3.55 ( ( sdtlpdtrp0 @
% 20.82/3.55 xc @
% 20.82/3.55 ( sdtpldt0 @ xP @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xn ) ) ) ) =
% 20.82/3.55 ( sdtlpdtrp0 @ ( sdtlpdtrp0 @ xC @ xn ) @ xP ) ) ) )),
% 20.82/3.55 inference('cnf.neg', [status(esa)], [zf_stmt_29])).
% 20.82/3.55 thf(zip_derived_cl495, plain,
% 20.82/3.55 (((sdtlpdtrp0 @ xc @
% 20.82/3.55 (sdtpldt0 @ xP @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn))))
% 20.82/3.55 != (sdtlpdtrp0 @ (sdtlpdtrp0 @ xC @ xn) @ xP))),
% 20.82/3.55 inference('cnf', [status(esa)], [zf_stmt_30])).
% 20.82/3.55 thf(zip_derived_cl1723, plain,
% 20.82/3.55 (((xp) = (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xn)))),
% 20.82/3.55 inference('demod', [status(thm)], [zip_derived_cl1716, zip_derived_cl472])).
% 20.82/3.55 thf(zip_derived_cl1789, plain,
% 20.82/3.55 (((sdtlpdtrp0 @ xc @ (sdtpldt0 @ xP @ xp))
% 20.82/3.55 != (sdtlpdtrp0 @ (sdtlpdtrp0 @ xC @ xn) @ xP))),
% 20.82/3.55 inference('demod', [status(thm)], [zip_derived_cl495, zip_derived_cl1723])).
% 20.82/3.55 thf(zip_derived_cl1852, plain, (((sdtpldt0 @ xP @ xp) = (xQ))),
% 20.82/3.55 inference('demod', [status(thm)],
% 20.82/3.55 [zip_derived_cl1828, zip_derived_cl439, zip_derived_cl958])).
% 20.82/3.55 thf(zip_derived_cl1970, plain,
% 20.82/3.55 (((sdtlpdtrp0 @ xc @ xQ) != (sdtlpdtrp0 @ (sdtlpdtrp0 @ xC @ xn) @ xP))),
% 20.82/3.55 inference('demod', [status(thm)],
% 20.82/3.55 [zip_derived_cl1789, zip_derived_cl1852])).
% 20.82/3.55 thf(zip_derived_cl13311, plain, ($false),
% 20.82/3.55 inference('simplify_reflect-', [status(thm)],
% 20.82/3.55 [zip_derived_cl13310, zip_derived_cl1970])).
% 20.82/3.55
% 20.82/3.55 % SZS output end Refutation
% 20.82/3.55
% 20.82/3.55
% 20.82/3.55 % Terminating...
% 20.98/3.65 % Runner terminated.
% 20.98/3.65 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------