%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEU280+2 : TPTP v9.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.gw8x5vqQJH true
% Computer : n011.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:54:06 PM UTC 2025
% Result : Theorem 77.37s 11.59s
% Output : Refutation 77.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.10 % Problem : SEU280+2 : TPTP v9.2.0. Released v3.3.0.
% 0.06/0.11 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.gw8x5vqQJH true
% 0.11/0.32 % Computer : n011.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Wed Oct 1 16:03:23 EDT 2025
% 0.11/0.32 % CPUTime :
% 0.11/0.32 % Running portfolio for 300 s
% 0.11/0.32 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.32 % Number of cores: 8
% 0.11/0.32 % Python version: Python 3.6.8
% 0.11/0.33 % Running in FO mode
% 0.17/0.53 % Total configuration time : 435
% 0.17/0.53 % Estimated wc time : 1092
% 0.17/0.53 % Estimated cpu time (7 cpus) : 156.0
% 0.78/0.56 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.78/0.56 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.78/0.57 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.78/0.60 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.78/0.60 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.78/0.60 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.78/0.61 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 77.37/11.59 % Solved by fo/fo4.sh.
% 77.37/11.59 % done 6116 iterations in 10.942s
% 77.37/11.59 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 77.37/11.59 % SZS output start Refutation
% 77.37/11.59 thf(sk__type, type, sk_: $i > $i > $i).
% 77.37/11.59 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $i > $i > $o).
% 77.37/11.59 thf(sk__4_type, type, sk__4: $i > $i).
% 77.37/11.59 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $i > $o).
% 77.37/11.59 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $i > $o).
% 77.37/11.59 thf(in_type, type, in: $i > $i > $o).
% 77.37/11.59 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $i > $o).
% 77.37/11.59 thf(sk__1_type, type, sk__1: $i).
% 77.37/11.59 thf(sk__3_type, type, sk__3: $i).
% 77.37/11.59 thf(ordinal_type, type, ordinal: $i > $o).
% 77.37/11.59 thf(sk__9_type, type, sk__9: $i > $i).
% 77.37/11.59 thf(sk__2_type, type, sk__2: $i).
% 77.37/11.59 thf(sk__8_type, type, sk__8: $i).
% 77.37/11.59 thf(s1_tarski__e6_22__wellord2__1, axiom,
% 77.37/11.59 (![A:$i]:
% 77.37/11.59 ( ( ![B:$i,C:$i,D:$i]:
% 77.37/11.59 ( ( ( ordinal @ D ) & ( ( B ) = ( D ) ) & ( ordinal @ C ) &
% 77.37/11.59 ( ( B ) = ( C ) ) ) =>
% 77.37/11.59 ( ( C ) = ( D ) ) ) ) =>
% 77.37/11.59 ( ?[B:$i]:
% 77.37/11.59 ( ![C:$i]:
% 77.37/11.59 ( ( in @ C @ B ) <=>
% 77.37/11.59 ( ?[D:$i]:
% 77.37/11.59 ( ( in @ D @ A ) & ( ( D ) = ( C ) ) & ( ordinal @ C ) ) ) ) ) ) ))).
% 77.37/11.59 thf(zf_stmt_0, axiom,
% 77.37/11.59 (![D:$i,C:$i,B:$i]:
% 77.37/11.59 ( ( ( zip_tseitin_0 @ D @ C @ B ) => ( ( C ) = ( D ) ) ) =>
% 77.37/11.59 ( zip_tseitin_1 @ D @ C @ B ) ))).
% 77.37/11.59 thf(zip_derived_cl6, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (zip_tseitin_1 @ X0 @ X1 @ X2) | (zip_tseitin_0 @ X0 @ X1 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_0])).
% 77.37/11.59 thf(zf_stmt_1, type, zip_tseitin_3 : $i > $i > $i > $o).
% 77.37/11.59 thf(zf_stmt_2, axiom,
% 77.37/11.59 (![C:$i,B:$i,A:$i]:
% 77.37/11.59 ( ( zip_tseitin_3 @ C @ B @ A ) =>
% 77.37/11.59 ( ( in @ C @ B ) <=> ( ?[D:$i]: ( zip_tseitin_2 @ D @ C @ A ) ) ) ))).
% 77.37/11.59 thf(zf_stmt_3, type, zip_tseitin_2 : $i > $i > $i > $o).
% 77.37/11.59 thf(zf_stmt_4, axiom,
% 77.37/11.59 (![D:$i,C:$i,A:$i]:
% 77.37/11.59 ( ( zip_tseitin_2 @ D @ C @ A ) <=>
% 77.37/11.59 ( ( ordinal @ C ) & ( ( D ) = ( C ) ) & ( in @ D @ A ) ) ))).
% 77.37/11.59 thf(zf_stmt_5, type, zip_tseitin_1 : $i > $i > $i > $o).
% 77.37/11.59 thf(zf_stmt_6, type, zip_tseitin_0 : $i > $i > $i > $o).
% 77.37/11.59 thf(zf_stmt_7, axiom,
% 77.37/11.59 (![D:$i,C:$i,B:$i]:
% 77.37/11.59 ( ( zip_tseitin_0 @ D @ C @ B ) =>
% 77.37/11.59 ( ( ( B ) = ( C ) ) & ( ordinal @ C ) & ( ( B ) = ( D ) ) &
% 77.37/11.59 ( ordinal @ D ) ) ))).
% 77.37/11.59 thf(zf_stmt_8, axiom,
% 77.37/11.59 (![A:$i]:
% 77.37/11.59 ( ( ![B:$i,C:$i,D:$i]: ( zip_tseitin_1 @ D @ C @ B ) ) =>
% 77.37/11.59 ( ?[B:$i]: ( ![C:$i]: ( zip_tseitin_3 @ C @ B @ A ) ) ) ))).
% 77.37/11.59 thf(zip_derived_cl13, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (zip_tseitin_3 @ X0 @ (sk__4 @ X1) @ X1))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_8])).
% 77.37/11.59 thf(zip_derived_cl54, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (zip_tseitin_0 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (zip_tseitin_3 @ X1 @ (sk__4 @ X0) @ X0))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl6, zip_derived_cl13])).
% 77.37/11.59 thf(zip_derived_cl3, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 (((X1) = (X0)) | ~ (zip_tseitin_0 @ X0 @ X2 @ X1))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_7])).
% 77.37/11.59 thf(zip_derived_cl360, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (zip_tseitin_3 @ X1 @ (sk__4 @ X0) @ X0) | ((sk__1) = (sk__3)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl54, zip_derived_cl3])).
% 77.37/11.59 thf(zip_derived_cl10, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (zip_tseitin_2 @ X0 @ X1 @ X2)
% 77.37/11.59 | ~ (in @ X0 @ X2)
% 77.37/11.59 | ((X0) != (X1))
% 77.37/11.59 | ~ (ordinal @ X1))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_4])).
% 77.37/11.59 thf(zip_derived_cl11, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 77.37/11.59 (~ (zip_tseitin_2 @ X0 @ X1 @ X2)
% 77.37/11.59 | (in @ X1 @ X3)
% 77.37/11.59 | ~ (zip_tseitin_3 @ X1 @ X3 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_2])).
% 77.37/11.59 thf(zip_derived_cl96, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 77.37/11.59 (~ (ordinal @ X1)
% 77.37/11.59 | ((X2) != (X1))
% 77.37/11.59 | ~ (in @ X2 @ X0)
% 77.37/11.59 | ~ (zip_tseitin_3 @ X1 @ X3 @ X0)
% 77.37/11.59 | (in @ X1 @ X3))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl10, zip_derived_cl11])).
% 77.37/11.59 thf(zip_derived_cl161, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (in @ X1 @ X0)
% 77.37/11.59 | ~ (zip_tseitin_3 @ X1 @ X0 @ X2)
% 77.37/11.59 | ~ (in @ X1 @ X2)
% 77.37/11.59 | ~ (ordinal @ X1))),
% 77.37/11.59 inference('eq_res', [status(thm)], [zip_derived_cl96])).
% 77.37/11.59 thf(zip_derived_cl543, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__1) = (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl360, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl6, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (zip_tseitin_1 @ X0 @ X1 @ X2) | (zip_tseitin_0 @ X0 @ X1 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_0])).
% 77.37/11.59 thf(s1_xboole_0__e6_22__wellord2, conjecture,
% 77.37/11.59 (![A:$i]:
% 77.37/11.59 ( ?[B:$i]:
% 77.37/11.59 ( ![C:$i]: ( ( in @ C @ B ) <=> ( ( in @ C @ A ) & ( ordinal @ C ) ) ) ) ))).
% 77.37/11.59 thf(zf_stmt_9, negated_conjecture,
% 77.37/11.59 (~( ![A:$i]:
% 77.37/11.59 ( ?[B:$i]:
% 77.37/11.59 ( ![C:$i]:
% 77.37/11.59 ( ( in @ C @ B ) <=> ( ( in @ C @ A ) & ( ordinal @ C ) ) ) ) ) )),
% 77.37/11.59 inference('cnf.neg', [status(esa)], [s1_xboole_0__e6_22__wellord2])).
% 77.37/11.59 thf(zip_derived_cl23, plain,
% 77.37/11.59 (![X0 : $i]: ( (in @ (sk__9 @ X0) @ sk__8) | (in @ (sk__9 @ X0) @ X0))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_9])).
% 77.37/11.59 thf(zip_derived_cl54, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (zip_tseitin_0 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (zip_tseitin_3 @ X1 @ (sk__4 @ X0) @ X0))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl6, zip_derived_cl13])).
% 77.37/11.59 thf(zip_derived_cl1, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 (((X1) = (X0)) | ~ (zip_tseitin_0 @ X2 @ X0 @ X1))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_7])).
% 77.37/11.59 thf(zip_derived_cl358, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (zip_tseitin_3 @ X1 @ (sk__4 @ X0) @ X0) | ((sk__1) = (sk__2)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl54, zip_derived_cl1])).
% 77.37/11.59 thf(zip_derived_cl161, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (in @ X1 @ X0)
% 77.37/11.59 | ~ (zip_tseitin_3 @ X1 @ X0 @ X2)
% 77.37/11.59 | ~ (in @ X1 @ X2)
% 77.37/11.59 | ~ (ordinal @ X1))),
% 77.37/11.59 inference('eq_res', [status(thm)], [zip_derived_cl96])).
% 77.37/11.59 thf(zip_derived_cl524, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__1) = (sk__2))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl358, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl537, plain,
% 77.37/11.59 (![X0 : $i]:
% 77.37/11.59 ( (in @ (sk__9 @ X0) @ X0)
% 77.37/11.59 | (in @ (sk__9 @ X0) @ (sk__4 @ sk__8))
% 77.37/11.59 | ~ (ordinal @ (sk__9 @ X0))
% 77.37/11.59 | ((sk__1) = (sk__2)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl23, zip_derived_cl524])).
% 77.37/11.59 thf(zip_derived_cl24, plain,
% 77.37/11.59 (![X0 : $i]: ( (ordinal @ (sk__9 @ X0)) | (in @ (sk__9 @ X0) @ X0))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_9])).
% 77.37/11.59 thf(zip_derived_cl22991, plain,
% 77.37/11.59 (![X0 : $i]:
% 77.37/11.59 (((sk__1) = (sk__2))
% 77.37/11.59 | (in @ (sk__9 @ X0) @ (sk__4 @ sk__8))
% 77.37/11.59 | (in @ (sk__9 @ X0) @ X0))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl537, zip_derived_cl24])).
% 77.37/11.59 thf(zip_derived_cl23138, plain,
% 77.37/11.59 (( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))
% 77.37/11.59 | ((sk__1) = (sk__2)))),
% 77.37/11.59 inference('eq_fact', [status(thm)], [zip_derived_cl22991])).
% 77.37/11.59 thf(zip_derived_cl13, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (zip_tseitin_3 @ X0 @ (sk__4 @ X1) @ X1))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_8])).
% 77.37/11.59 thf(zip_derived_cl12, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 (~ (in @ X0 @ X1)
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X2 @ X0) @ X0 @ X2)
% 77.37/11.59 | ~ (zip_tseitin_3 @ X0 @ X1 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_2])).
% 77.37/11.59 thf(zip_derived_cl51, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X0 @ X1) @ X1 @ X0)
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl13, zip_derived_cl12])).
% 77.37/11.59 thf(zip_derived_cl8, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 (((X1) = (X0)) | ~ (zip_tseitin_2 @ X1 @ X0 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_4])).
% 77.37/11.59 thf(zip_derived_cl302, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | ((sk_ @ X0 @ X1) = (X1)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl51, zip_derived_cl8])).
% 77.37/11.59 thf(zip_derived_cl6, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (zip_tseitin_1 @ X0 @ X1 @ X2) | (zip_tseitin_0 @ X0 @ X1 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_0])).
% 77.37/11.59 thf(zip_derived_cl573, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ X1 @ X0) = (X0))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ X1))
% 77.37/11.59 | (zip_tseitin_0 @ sk__3 @ sk__2 @ sk__1))),
% 77.37/11.59 inference('sup+', [status(thm)], [zip_derived_cl302, zip_derived_cl6])).
% 77.37/11.59 thf(zip_derived_cl23179, plain,
% 77.37/11.59 ((((sk__1) = (sk__2))
% 77.37/11.59 | (zip_tseitin_0 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | ((sk_ @ sk__8 @ (sk__9 @ (sk__4 @ sk__8)))
% 77.37/11.59 = (sk__9 @ (sk__4 @ sk__8))))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl23138, zip_derived_cl573])).
% 77.37/11.59 thf(zip_derived_cl1, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 (((X1) = (X0)) | ~ (zip_tseitin_0 @ X2 @ X0 @ X1))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_7])).
% 77.37/11.59 thf(zip_derived_cl28604, plain,
% 77.37/11.59 ((((sk_ @ sk__8 @ (sk__9 @ (sk__4 @ sk__8))) = (sk__9 @ (sk__4 @ sk__8)))
% 77.37/11.59 | ((sk__1) = (sk__2)))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl23179, zip_derived_cl1])).
% 77.37/11.59 thf(zip_derived_cl51, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X0 @ X1) @ X1 @ X0)
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl13, zip_derived_cl12])).
% 77.37/11.59 thf(zip_derived_cl9, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (in @ X0 @ X1) | ~ (zip_tseitin_2 @ X0 @ X2 @ X1))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_4])).
% 77.37/11.59 thf(zip_derived_cl303, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (in @ (sk_ @ X0 @ X1) @ X0))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl51, zip_derived_cl9])).
% 77.37/11.59 thf(zip_derived_cl28609, plain,
% 77.37/11.59 (( (in @ (sk__9 @ (sk__4 @ sk__8)) @ sk__8)
% 77.37/11.59 | ((sk__1) = (sk__2))
% 77.37/11.59 | ~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | ~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8)))),
% 77.37/11.59 inference('sup+', [status(thm)], [zip_derived_cl28604, zip_derived_cl303])).
% 77.37/11.59 thf(zip_derived_cl23138, plain,
% 77.37/11.59 (( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))
% 77.37/11.59 | ((sk__1) = (sk__2)))),
% 77.37/11.59 inference('eq_fact', [status(thm)], [zip_derived_cl22991])).
% 77.37/11.59 thf(zip_derived_cl28639, plain,
% 77.37/11.59 ((~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | ((sk__1) = (sk__2))
% 77.37/11.59 | (in @ (sk__9 @ (sk__4 @ sk__8)) @ sk__8))),
% 77.37/11.59 inference('clc', [status(thm)],
% 77.37/11.59 [zip_derived_cl28609, zip_derived_cl23138])).
% 77.37/11.59 thf(zip_derived_cl28641, plain,
% 77.37/11.59 (( (zip_tseitin_0 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (in @ (sk__9 @ (sk__4 @ sk__8)) @ sk__8)
% 77.37/11.59 | ((sk__1) = (sk__2)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl6, zip_derived_cl28639])).
% 77.37/11.59 thf(zip_derived_cl1, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 (((X1) = (X0)) | ~ (zip_tseitin_0 @ X2 @ X0 @ X1))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_7])).
% 77.37/11.59 thf(zip_derived_cl28642, plain,
% 77.37/11.59 ((((sk__1) = (sk__2)) | (in @ (sk__9 @ (sk__4 @ sk__8)) @ sk__8))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl28641, zip_derived_cl1])).
% 77.37/11.59 thf(zip_derived_cl25, plain,
% 77.37/11.59 (![X0 : $i]:
% 77.37/11.59 (~ (ordinal @ (sk__9 @ X0))
% 77.37/11.59 | ~ (in @ (sk__9 @ X0) @ sk__8)
% 77.37/11.59 | ~ (in @ (sk__9 @ X0) @ X0))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_9])).
% 77.37/11.59 thf(zip_derived_cl28664, plain,
% 77.37/11.59 ((((sk__1) = (sk__2))
% 77.37/11.59 | ~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))
% 77.37/11.59 | ~ (ordinal @ (sk__9 @ (sk__4 @ sk__8))))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl28642, zip_derived_cl25])).
% 77.37/11.59 thf(zip_derived_cl23138, plain,
% 77.37/11.59 (( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))
% 77.37/11.59 | ((sk__1) = (sk__2)))),
% 77.37/11.59 inference('eq_fact', [status(thm)], [zip_derived_cl22991])).
% 77.37/11.59 thf(zip_derived_cl28672, plain,
% 77.37/11.59 ((~ (ordinal @ (sk__9 @ (sk__4 @ sk__8))) | ((sk__1) = (sk__2)))),
% 77.37/11.59 inference('clc', [status(thm)],
% 77.37/11.59 [zip_derived_cl28664, zip_derived_cl23138])).
% 77.37/11.59 thf(zip_derived_cl24, plain,
% 77.37/11.59 (![X0 : $i]: ( (ordinal @ (sk__9 @ X0)) | (in @ (sk__9 @ X0) @ X0))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_9])).
% 77.37/11.59 thf(zip_derived_cl6, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (zip_tseitin_1 @ X0 @ X1 @ X2) | (zip_tseitin_0 @ X0 @ X1 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_0])).
% 77.37/11.59 thf(zip_derived_cl51, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X0 @ X1) @ X1 @ X0)
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl13, zip_derived_cl12])).
% 77.37/11.59 thf(zip_derived_cl7, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (ordinal @ X0) | ~ (zip_tseitin_2 @ X1 @ X0 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_4])).
% 77.37/11.59 thf(zip_derived_cl301, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (ordinal @ X1))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl51, zip_derived_cl7])).
% 77.37/11.59 thf(zip_derived_cl327, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (zip_tseitin_0 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (ordinal @ X0)
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ X1)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl6, zip_derived_cl301])).
% 77.37/11.59 thf(zip_derived_cl336, plain,
% 77.37/11.59 (![X0 : $i]:
% 77.37/11.59 ( (ordinal @ (sk__9 @ (sk__4 @ X0)))
% 77.37/11.59 | (ordinal @ (sk__9 @ (sk__4 @ X0)))
% 77.37/11.59 | (zip_tseitin_0 @ sk__3 @ sk__2 @ sk__1))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl24, zip_derived_cl327])).
% 77.37/11.59 thf(zip_derived_cl337, plain,
% 77.37/11.59 (![X0 : $i]:
% 77.37/11.59 ( (zip_tseitin_0 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (ordinal @ (sk__9 @ (sk__4 @ X0))))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl336])).
% 77.37/11.59 thf(zip_derived_cl1, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 (((X1) = (X0)) | ~ (zip_tseitin_0 @ X2 @ X0 @ X1))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_7])).
% 77.37/11.59 thf(zip_derived_cl494, plain,
% 77.37/11.59 (![X0 : $i]: ( (ordinal @ (sk__9 @ (sk__4 @ X0))) | ((sk__1) = (sk__2)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl337, zip_derived_cl1])).
% 77.37/11.59 thf(zip_derived_cl28673, plain, (((sk__1) = (sk__2))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl28672, zip_derived_cl494])).
% 77.37/11.59 thf(zip_derived_cl28704, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) = (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('demod', [status(thm)],
% 77.37/11.59 [zip_derived_cl543, zip_derived_cl28673])).
% 77.37/11.59 thf(zip_derived_cl13, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (zip_tseitin_3 @ X0 @ (sk__4 @ X1) @ X1))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_8])).
% 77.37/11.59 thf(zip_derived_cl5, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (zip_tseitin_1 @ X0 @ X1 @ X2) | ((X1) != (X0)))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_0])).
% 77.37/11.59 thf(zip_derived_cl50, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (zip_tseitin_3 @ X1 @ (sk__4 @ X0) @ X0) | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('sup+', [status(thm)], [zip_derived_cl13, zip_derived_cl5])).
% 77.37/11.59 thf(zip_derived_cl161, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (in @ X1 @ X0)
% 77.37/11.59 | ~ (zip_tseitin_3 @ X1 @ X0 @ X2)
% 77.37/11.59 | ~ (in @ X1 @ X2)
% 77.37/11.59 | ~ (ordinal @ X1))),
% 77.37/11.59 inference('eq_res', [status(thm)], [zip_derived_cl96])).
% 77.37/11.59 thf(zip_derived_cl163, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl31347, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ X1 @ (sk__4 @ X0)) | ~ (in @ X1 @ X0) | ~ (ordinal @ X1))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl28704, zip_derived_cl163])).
% 77.37/11.59 thf(zip_derived_cl360, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (zip_tseitin_3 @ X1 @ (sk__4 @ X0) @ X0) | ((sk__1) = (sk__3)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl54, zip_derived_cl3])).
% 77.37/11.59 thf(zip_derived_cl12, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 (~ (in @ X0 @ X1)
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X2 @ X0) @ X0 @ X2)
% 77.37/11.59 | ~ (zip_tseitin_3 @ X0 @ X1 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_2])).
% 77.37/11.59 thf(zip_derived_cl542, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__1) = (sk__3))
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X0 @ X1) @ X1 @ X0)
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl360, zip_derived_cl12])).
% 77.37/11.59 thf(zip_derived_cl28673, plain, (((sk__1) = (sk__2))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl28672, zip_derived_cl494])).
% 77.37/11.59 thf(zip_derived_cl28703, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) = (sk__3))
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X0 @ X1) @ X1 @ X0)
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('demod', [status(thm)],
% 77.37/11.59 [zip_derived_cl542, zip_derived_cl28673])).
% 77.37/11.59 thf(zip_derived_cl50, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (zip_tseitin_3 @ X1 @ (sk__4 @ X0) @ X0) | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('sup+', [status(thm)], [zip_derived_cl13, zip_derived_cl5])).
% 77.37/11.59 thf(zip_derived_cl12, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 (~ (in @ X0 @ X1)
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X2 @ X0) @ X0 @ X2)
% 77.37/11.59 | ~ (zip_tseitin_3 @ X0 @ X1 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_2])).
% 77.37/11.59 thf(zip_derived_cl53, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X0 @ X1) @ X1 @ X0)
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl12])).
% 77.37/11.59 thf(zip_derived_cl36427, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X0 @ X1) @ X1 @ X0))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl28703, zip_derived_cl53])).
% 77.37/11.59 thf(zip_derived_cl8, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 (((X1) = (X0)) | ~ (zip_tseitin_2 @ X1 @ X0 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_4])).
% 77.37/11.59 thf(zip_derived_cl36429, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0)) | ((sk_ @ X0 @ X1) = (X1)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl36427, zip_derived_cl8])).
% 77.37/11.59 thf(zip_derived_cl23, plain,
% 77.37/11.59 (![X0 : $i]: ( (in @ (sk__9 @ X0) @ sk__8) | (in @ (sk__9 @ X0) @ X0))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_9])).
% 77.37/11.59 thf(zip_derived_cl54, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (zip_tseitin_0 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (zip_tseitin_3 @ X1 @ (sk__4 @ X0) @ X0))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl6, zip_derived_cl13])).
% 77.37/11.59 thf(zip_derived_cl4, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (ordinal @ X0) | ~ (zip_tseitin_0 @ X0 @ X1 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_7])).
% 77.37/11.59 thf(zip_derived_cl361, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (zip_tseitin_3 @ X1 @ (sk__4 @ X0) @ X0) | (ordinal @ sk__3))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl54, zip_derived_cl4])).
% 77.37/11.59 thf(zip_derived_cl161, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (in @ X1 @ X0)
% 77.37/11.59 | ~ (zip_tseitin_3 @ X1 @ X0 @ X2)
% 77.37/11.59 | ~ (in @ X1 @ X2)
% 77.37/11.59 | ~ (ordinal @ X1))),
% 77.37/11.59 inference('eq_res', [status(thm)], [zip_derived_cl96])).
% 77.37/11.59 thf(zip_derived_cl390, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (ordinal @ sk__3)
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl361, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl401, plain,
% 77.37/11.59 (![X0 : $i]:
% 77.37/11.59 ( (in @ (sk__9 @ X0) @ X0)
% 77.37/11.59 | (in @ (sk__9 @ X0) @ (sk__4 @ sk__8))
% 77.37/11.59 | ~ (ordinal @ (sk__9 @ X0))
% 77.37/11.59 | (ordinal @ sk__3))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl23, zip_derived_cl390])).
% 77.37/11.59 thf(zip_derived_cl24, plain,
% 77.37/11.59 (![X0 : $i]: ( (ordinal @ (sk__9 @ X0)) | (in @ (sk__9 @ X0) @ X0))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_9])).
% 77.37/11.59 thf(zip_derived_cl14214, plain,
% 77.37/11.59 (![X0 : $i]:
% 77.37/11.59 ( (ordinal @ sk__3)
% 77.37/11.59 | (in @ (sk__9 @ X0) @ (sk__4 @ sk__8))
% 77.37/11.59 | (in @ (sk__9 @ X0) @ X0))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl401, zip_derived_cl24])).
% 77.37/11.59 thf(zip_derived_cl14354, plain,
% 77.37/11.59 (( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))
% 77.37/11.59 | (ordinal @ sk__3))),
% 77.37/11.59 inference('eq_fact', [status(thm)], [zip_derived_cl14214])).
% 77.37/11.59 thf(zip_derived_cl390, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (ordinal @ sk__3)
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl361, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl14373, plain,
% 77.37/11.59 (( (ordinal @ sk__3)
% 77.37/11.59 | (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ (sk__4 @ sk__8)))
% 77.37/11.59 | ~ (ordinal @ (sk__9 @ (sk__4 @ sk__8)))
% 77.37/11.59 | (ordinal @ sk__3))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl14354, zip_derived_cl390])).
% 77.37/11.59 thf(zip_derived_cl14404, plain,
% 77.37/11.59 ((~ (ordinal @ (sk__9 @ (sk__4 @ sk__8)))
% 77.37/11.59 | (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ (sk__4 @ sk__8)))
% 77.37/11.59 | (ordinal @ sk__3))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl14373])).
% 77.37/11.59 thf(zip_derived_cl337, plain,
% 77.37/11.59 (![X0 : $i]:
% 77.37/11.59 ( (zip_tseitin_0 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (ordinal @ (sk__9 @ (sk__4 @ X0))))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl336])).
% 77.37/11.59 thf(zip_derived_cl4, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (ordinal @ X0) | ~ (zip_tseitin_0 @ X0 @ X1 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_7])).
% 77.37/11.59 thf(zip_derived_cl497, plain,
% 77.37/11.59 (![X0 : $i]: ( (ordinal @ (sk__9 @ (sk__4 @ X0))) | (ordinal @ sk__3))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl337, zip_derived_cl4])).
% 77.37/11.59 thf(zip_derived_cl14630, plain,
% 77.37/11.59 (( (ordinal @ sk__3)
% 77.37/11.59 | (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ (sk__4 @ sk__8))))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl14404, zip_derived_cl497])).
% 77.37/11.59 thf(zip_derived_cl37005, plain,
% 77.37/11.59 ((((sk_ @ (sk__4 @ sk__8) @ (sk__9 @ (sk__4 @ sk__8)))
% 77.37/11.59 = (sk__9 @ (sk__4 @ sk__8)))
% 77.37/11.59 | (ordinal @ sk__3))),
% 77.37/11.59 inference('sup+', [status(thm)],
% 77.37/11.59 [zip_derived_cl36429, zip_derived_cl14630])).
% 77.37/11.59 thf(zip_derived_cl163, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl163, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl53, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X0 @ X1) @ X1 @ X0)
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl12])).
% 77.37/11.59 thf(zip_derived_cl8, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 (((X1) = (X0)) | ~ (zip_tseitin_2 @ X1 @ X0 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_4])).
% 77.37/11.59 thf(zip_derived_cl72, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk_ @ X0 @ X1) = (X1)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl8])).
% 77.37/11.59 thf(zip_derived_cl163, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl176, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ X0 @ X1) = (X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('sup+', [status(thm)], [zip_derived_cl72, zip_derived_cl163])).
% 77.37/11.59 thf(zip_derived_cl183, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk_ @ X0 @ X1) = (X1)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl176])).
% 77.37/11.59 thf(zip_derived_cl206, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ X0)
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk_ @ (sk__4 @ X0) @ X1) = (X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl163, zip_derived_cl183])).
% 77.37/11.59 thf(zip_derived_cl214, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ (sk__4 @ X0) @ X1) = (X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl206])).
% 77.37/11.59 thf(zip_derived_cl72, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk_ @ X0 @ X1) = (X1)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl8])).
% 77.37/11.59 thf(zip_derived_cl53, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X0 @ X1) @ X1 @ X0)
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl12])).
% 77.37/11.59 thf(zip_derived_cl9, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (in @ X0 @ X1) | ~ (zip_tseitin_2 @ X0 @ X2 @ X1))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_4])).
% 77.37/11.59 thf(zip_derived_cl73, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | (in @ (sk_ @ X0 @ X1) @ X0))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl9])).
% 77.37/11.59 thf(zip_derived_cl90, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ X0 @ (sk_ @ (sk__4 @ X0) @ X1)) = (sk_ @ (sk__4 @ X0) @ X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ (sk__4 @ X0))))),
% 77.37/11.59 inference('sup+', [status(thm)], [zip_derived_cl72, zip_derived_cl73])).
% 77.37/11.59 thf(zip_derived_cl91, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ (sk__4 @ X0)))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk_ @ X0 @ (sk_ @ (sk__4 @ X0) @ X1)) = (sk_ @ (sk__4 @ X0) @ X1)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl90])).
% 77.37/11.59 thf(zip_derived_cl1119, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ X1 @ X0) = (sk_ @ (sk__4 @ X1) @ X0))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ (sk__4 @ X1))))),
% 77.37/11.59 inference('sup+', [status(thm)], [zip_derived_cl214, zip_derived_cl91])).
% 77.37/11.59 thf(zip_derived_cl1121, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X0 @ (sk__4 @ (sk__4 @ X1)))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ((sk_ @ X1 @ X0) = (sk_ @ (sk__4 @ X1) @ X0)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl1119])).
% 77.37/11.59 thf(zip_derived_cl53, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X0 @ X1) @ X1 @ X0)
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl12])).
% 77.37/11.59 thf(zip_derived_cl7, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (ordinal @ X0) | ~ (zip_tseitin_2 @ X1 @ X0 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_4])).
% 77.37/11.59 thf(zip_derived_cl71, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0)) | ((sk__2) != (sk__3)) | (ordinal @ X1))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl7])).
% 77.37/11.59 thf(zip_derived_cl5501, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ X1 @ X0) = (sk_ @ (sk__4 @ X1) @ X0))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ (sk__4 @ X1))))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl1121, zip_derived_cl71])).
% 77.37/11.59 thf(zip_derived_cl5530, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | ((sk_ @ X0 @ X1) = (sk_ @ (sk__4 @ X0) @ X1)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl163, zip_derived_cl5501])).
% 77.37/11.59 thf(zip_derived_cl5560, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ X0 @ X1) = (sk_ @ (sk__4 @ X0) @ X1))
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl5530])).
% 77.37/11.59 thf(zip_derived_cl71, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0)) | ((sk__2) != (sk__3)) | (ordinal @ X1))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl7])).
% 77.37/11.59 thf(zip_derived_cl5574, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | ((sk_ @ X0 @ X1) = (sk_ @ (sk__4 @ X0) @ X1)))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl5560, zip_derived_cl71])).
% 77.37/11.59 thf(zip_derived_cl214, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ (sk__4 @ X0) @ X1) = (X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl206])).
% 77.37/11.59 thf(zip_derived_cl163, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl5574, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | ((sk_ @ X0 @ X1) = (sk_ @ (sk__4 @ X0) @ X1)))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl5560, zip_derived_cl71])).
% 77.37/11.59 thf(zip_derived_cl5603, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ X0)
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk_ @ X0 @ X1) = (sk_ @ (sk__4 @ X0) @ X1))
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl163, zip_derived_cl5574])).
% 77.37/11.59 thf(zip_derived_cl5632, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ X0 @ X1) = (sk_ @ (sk__4 @ X0) @ X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl5603])).
% 77.37/11.59 thf(zip_derived_cl13, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (zip_tseitin_3 @ X0 @ (sk__4 @ X1) @ X1))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_8])).
% 77.37/11.59 thf(zip_derived_cl161, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (in @ X1 @ X0)
% 77.37/11.59 | ~ (zip_tseitin_3 @ X1 @ X0 @ X2)
% 77.37/11.59 | ~ (in @ X1 @ X2)
% 77.37/11.59 | ~ (ordinal @ X1))),
% 77.37/11.59 inference('eq_res', [status(thm)], [zip_derived_cl96])).
% 77.37/11.59 thf(zip_derived_cl162, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl13, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl5632, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ X0 @ X1) = (sk_ @ (sk__4 @ X0) @ X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl5603])).
% 77.37/11.59 thf(zip_derived_cl91, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ (sk__4 @ X0)))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk_ @ X0 @ (sk_ @ (sk__4 @ X0) @ X1)) = (sk_ @ (sk__4 @ X0) @ X1)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl90])).
% 77.37/11.59 thf(zip_derived_cl73, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | (in @ (sk_ @ X0 @ X1) @ X0))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl9])).
% 77.37/11.59 thf(zip_derived_cl1115, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ (sk__4 @ X1) @ X0) @ X1)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ (sk__4 @ X1)))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ (sk_ @ (sk__4 @ X1) @ X0) @ (sk__4 @ X1)))),
% 77.37/11.59 inference('sup+', [status(thm)], [zip_derived_cl91, zip_derived_cl73])).
% 77.37/11.59 thf(zip_derived_cl1123, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ (sk_ @ (sk__4 @ X1) @ X0) @ (sk__4 @ X1))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ (sk__4 @ X1)))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | (in @ (sk_ @ (sk__4 @ X1) @ X0) @ X1))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl1115])).
% 77.37/11.59 thf(zip_derived_cl73, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | (in @ (sk_ @ X0 @ X1) @ X0))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl9])).
% 77.37/11.59 thf(zip_derived_cl7380, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ (sk__4 @ X1) @ X0) @ X1)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ (sk__4 @ X1))))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl1123, zip_derived_cl73])).
% 77.37/11.59 thf(zip_derived_cl7462, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ X1 @ X0) @ X1)
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ (sk__4 @ X1)))
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('sup+', [status(thm)], [zip_derived_cl5632, zip_derived_cl7380])).
% 77.37/11.59 thf(zip_derived_cl7485, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X0 @ (sk__4 @ (sk__4 @ X1)))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | (in @ (sk_ @ X1 @ X0) @ X1))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl7462])).
% 77.37/11.59 thf(zip_derived_cl71, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0)) | ((sk__2) != (sk__3)) | (ordinal @ X1))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl7])).
% 77.37/11.59 thf(zip_derived_cl7566, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ X1 @ X0) @ X1)
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ (sk__4 @ X1))))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl7485, zip_derived_cl71])).
% 77.37/11.59 thf(zip_derived_cl7686, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ (sk_ @ X0 @ X1) @ X0))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl162, zip_derived_cl7566])).
% 77.37/11.59 thf(zip_derived_cl163, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl10661, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ X0 @ X1) @ X0)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (zip_tseitin_1 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | ~ (ordinal @ X1))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl7686, zip_derived_cl163])).
% 77.37/11.59 thf(zip_derived_cl5, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (zip_tseitin_1 @ X0 @ X1 @ X2) | ((X1) != (X0)))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_0])).
% 77.37/11.59 thf(zip_derived_cl10662, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (ordinal @ X1)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ (sk_ @ X0 @ X1) @ X0))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl10661, zip_derived_cl5])).
% 77.37/11.59 thf(zip_derived_cl10756, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ X1 @ X0) @ (sk__4 @ X1))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X0))),
% 77.37/11.59 inference('sup+', [status(thm)],
% 77.37/11.59 [zip_derived_cl5632, zip_derived_cl10662])).
% 77.37/11.59 thf(zip_derived_cl10784, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X0 @ (sk__4 @ X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | (in @ (sk_ @ X1 @ X0) @ (sk__4 @ X1)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl10756])).
% 77.37/11.59 thf(zip_derived_cl163, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl11066, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ X1 @ X0) @ (sk__4 @ X1))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl10784, zip_derived_cl163])).
% 77.37/11.59 thf(zip_derived_cl11132, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ X0 @ (sk__4 @ (sk__4 @ X1)))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ X1)))),
% 77.37/11.59 inference('sup+', [status(thm)], [zip_derived_cl214, zip_derived_cl11066])).
% 77.37/11.59 thf(zip_derived_cl11160, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X0 @ (sk__4 @ X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | (in @ X0 @ (sk__4 @ (sk__4 @ X1))))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl11132])).
% 77.37/11.59 thf(zip_derived_cl163, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl11334, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ X0 @ (sk__4 @ (sk__4 @ X1)))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl11160, zip_derived_cl163])).
% 77.37/11.59 thf(zip_derived_cl214, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ (sk__4 @ X0) @ X1) = (X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl206])).
% 77.37/11.59 thf(zip_derived_cl5632, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ X0 @ X1) = (sk_ @ (sk__4 @ X0) @ X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl5603])).
% 77.37/11.59 thf(zip_derived_cl73, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | (in @ (sk_ @ X0 @ X1) @ X0))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl9])).
% 77.37/11.59 thf(zip_derived_cl5960, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ X1 @ X0) @ (sk__4 @ X1))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ (sk__4 @ X1))))),
% 77.37/11.59 inference('sup+', [status(thm)], [zip_derived_cl5632, zip_derived_cl73])).
% 77.37/11.59 thf(zip_derived_cl5983, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X0 @ (sk__4 @ (sk__4 @ X1)))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | (in @ (sk_ @ X1 @ X0) @ (sk__4 @ X1)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl5960])).
% 77.37/11.59 thf(zip_derived_cl71, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0)) | ((sk__2) != (sk__3)) | (ordinal @ X1))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl7])).
% 77.37/11.59 thf(zip_derived_cl6164, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ X1 @ X0) @ (sk__4 @ X1))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ (sk__4 @ X1))))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl5983, zip_derived_cl71])).
% 77.37/11.59 thf(zip_derived_cl6216, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ X0 @ (sk__4 @ (sk__4 @ X1)))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ (sk__4 @ (sk__4 @ X1))))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ X1)))),
% 77.37/11.59 inference('sup+', [status(thm)], [zip_derived_cl214, zip_derived_cl6164])).
% 77.37/11.59 thf(zip_derived_cl6239, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X0 @ (sk__4 @ X1))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ (sk__4 @ (sk__4 @ X1))))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | (in @ X0 @ (sk__4 @ (sk__4 @ X1))))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl6216])).
% 77.37/11.59 thf(zip_derived_cl163, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl6613, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ X0 @ (sk__4 @ (sk__4 @ X1)))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ (sk__4 @ (sk__4 @ X1)))))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl6239, zip_derived_cl163])).
% 77.37/11.59 thf(zip_derived_cl71, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0)) | ((sk__2) != (sk__3)) | (ordinal @ X1))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl7])).
% 77.37/11.59 thf(zip_derived_cl6614, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X0 @ (sk__4 @ (sk__4 @ (sk__4 @ X1))))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | (in @ X0 @ (sk__4 @ (sk__4 @ X1))))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl6613, zip_derived_cl71])).
% 77.37/11.59 thf(zip_derived_cl11373, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | (in @ X1 @ (sk__4 @ (sk__4 @ X0)))
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('sup-', [status(thm)],
% 77.37/11.59 [zip_derived_cl11334, zip_derived_cl6614])).
% 77.37/11.59 thf(zip_derived_cl11536, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ (sk__4 @ X0)))
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl11373])).
% 77.37/11.59 thf(zip_derived_cl163, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl11847, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | (in @ X1 @ (sk__4 @ (sk__4 @ X0))))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl11536, zip_derived_cl163])).
% 77.37/11.59 thf(zip_derived_cl71, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0)) | ((sk__2) != (sk__3)) | (ordinal @ X1))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl7])).
% 77.37/11.59 thf(zip_derived_cl11848, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ X1 @ (sk__4 @ (sk__4 @ X0)))
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl11847, zip_derived_cl71])).
% 77.37/11.59 thf(zip_derived_cl11958, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ (sk__4 @ X0) @ X1) = (sk_ @ (sk__4 @ (sk__4 @ X0)) @ X1))
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup+', [status(thm)],
% 77.37/11.59 [zip_derived_cl5574, zip_derived_cl11848])).
% 77.37/11.59 thf(zip_derived_cl12000, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ((sk_ @ (sk__4 @ X0) @ X1) = (sk_ @ (sk__4 @ (sk__4 @ X0)) @ X1)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl11958])).
% 77.37/11.59 thf(zip_derived_cl214, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ (sk__4 @ X0) @ X1) = (X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl206])).
% 77.37/11.59 thf(zip_derived_cl7566, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ X1 @ X0) @ X1)
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ (sk__4 @ X1))))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl7485, zip_derived_cl71])).
% 77.37/11.59 thf(zip_derived_cl5632, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk_ @ X0 @ X1) = (sk_ @ (sk__4 @ X0) @ X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl5603])).
% 77.37/11.59 thf(zip_derived_cl11066, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ X1 @ X0) @ (sk__4 @ X1))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl10784, zip_derived_cl163])).
% 77.37/11.59 thf(zip_derived_cl11134, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ X1 @ X0) @ (sk__4 @ (sk__4 @ X1)))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ X1)))),
% 77.37/11.59 inference('sup+', [status(thm)],
% 77.37/11.59 [zip_derived_cl5632, zip_derived_cl11066])).
% 77.37/11.59 thf(zip_derived_cl11162, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X0 @ (sk__4 @ X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | (in @ (sk_ @ X1 @ X0) @ (sk__4 @ (sk__4 @ X1))))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl11134])).
% 77.37/11.59 thf(zip_derived_cl163, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl18943, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ X1 @ X0) @ (sk__4 @ (sk__4 @ X1)))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl11162, zip_derived_cl163])).
% 77.37/11.59 thf(zip_derived_cl18993, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ (sk_ @ X0 @ X1) @ X0)
% 77.37/11.59 | (in @ (sk_ @ X0 @ (sk_ @ X0 @ X1)) @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0))),
% 77.37/11.59 inference('sup+', [status(thm)],
% 77.37/11.59 [zip_derived_cl7566, zip_derived_cl18943])).
% 77.37/11.59 thf(zip_derived_cl19045, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ X0)
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | (in @ (sk_ @ X0 @ (sk_ @ X0 @ X1)) @ X0)
% 77.37/11.59 | ~ (in @ (sk_ @ X0 @ X1) @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl18993])).
% 77.37/11.59 thf(zip_derived_cl10662, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (ordinal @ X1)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ (sk_ @ X0 @ X1) @ X0))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl10661, zip_derived_cl5])).
% 77.37/11.59 thf(zip_derived_cl19538, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | (in @ (sk_ @ X0 @ (sk_ @ X0 @ X1)) @ X0)
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0))),
% 77.37/11.59 inference('clc', [status(thm)],
% 77.37/11.59 [zip_derived_cl19045, zip_derived_cl10662])).
% 77.37/11.59 thf(zip_derived_cl19646, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ (sk__4 @ X1) @ X0) @ (sk__4 @ X1))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ X1))
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('sup+', [status(thm)], [zip_derived_cl214, zip_derived_cl19538])).
% 77.37/11.59 thf(zip_derived_cl19698, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X0 @ (sk__4 @ X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | (in @ (sk_ @ (sk__4 @ X1) @ X0) @ (sk__4 @ X1)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl19646])).
% 77.37/11.59 thf(zip_derived_cl163, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl22635, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ (sk__4 @ X1) @ X0) @ (sk__4 @ X1))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl19698, zip_derived_cl163])).
% 77.37/11.59 thf(zip_derived_cl22708, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ (sk__4 @ X1) @ X0) @ (sk__4 @ (sk__4 @ X1)))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ X1))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ X1)))),
% 77.37/11.59 inference('sup+', [status(thm)],
% 77.37/11.59 [zip_derived_cl12000, zip_derived_cl22635])).
% 77.37/11.59 thf(zip_derived_cl22753, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ X1))
% 77.37/11.59 | (in @ (sk_ @ (sk__4 @ X1) @ X0) @ (sk__4 @ (sk__4 @ X1))))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl22708])).
% 77.37/11.59 thf(zip_derived_cl71, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0)) | ((sk__2) != (sk__3)) | (ordinal @ X1))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl7])).
% 77.37/11.59 thf(zip_derived_cl32834, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ (sk__4 @ X1) @ X0) @ (sk__4 @ (sk__4 @ X1)))
% 77.37/11.59 | ~ (in @ X0 @ (sk__4 @ X1))
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl22753, zip_derived_cl71])).
% 77.37/11.59 thf(zip_derived_cl41812, plain,
% 77.37/11.59 (( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ (sk__4 @ sk__8)))
% 77.37/11.59 | (ordinal @ sk__3)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8)))),
% 77.37/11.59 inference('sup+', [status(thm)],
% 77.37/11.59 [zip_derived_cl37005, zip_derived_cl32834])).
% 77.37/11.59 thf(zip_derived_cl11848, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ X1 @ (sk__4 @ (sk__4 @ X0)))
% 77.37/11.59 | ~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl11847, zip_derived_cl71])).
% 77.37/11.59 thf(zip_derived_cl45967, plain,
% 77.37/11.59 ((~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ (sk__4 @ sk__8))))),
% 77.37/11.59 inference('clc', [status(thm)],
% 77.37/11.59 [zip_derived_cl41812, zip_derived_cl11848])).
% 77.37/11.59 thf(zip_derived_cl23, plain,
% 77.37/11.59 (![X0 : $i]: ( (in @ (sk__9 @ X0) @ sk__8) | (in @ (sk__9 @ X0) @ X0))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_9])).
% 77.37/11.59 thf(zip_derived_cl543, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__1) = (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl360, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl556, plain,
% 77.37/11.59 (![X0 : $i]:
% 77.37/11.59 ( (in @ (sk__9 @ X0) @ X0)
% 77.37/11.59 | (in @ (sk__9 @ X0) @ (sk__4 @ sk__8))
% 77.37/11.59 | ~ (ordinal @ (sk__9 @ X0))
% 77.37/11.59 | ((sk__1) = (sk__3)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl23, zip_derived_cl543])).
% 77.37/11.59 thf(zip_derived_cl24, plain,
% 77.37/11.59 (![X0 : $i]: ( (ordinal @ (sk__9 @ X0)) | (in @ (sk__9 @ X0) @ X0))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_9])).
% 77.37/11.59 thf(zip_derived_cl24240, plain,
% 77.37/11.59 (![X0 : $i]:
% 77.37/11.59 (((sk__1) = (sk__3))
% 77.37/11.59 | (in @ (sk__9 @ X0) @ (sk__4 @ sk__8))
% 77.37/11.59 | (in @ (sk__9 @ X0) @ X0))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl556, zip_derived_cl24])).
% 77.37/11.59 thf(zip_derived_cl24391, plain,
% 77.37/11.59 (( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))
% 77.37/11.59 | ((sk__1) = (sk__3)))),
% 77.37/11.59 inference('eq_fact', [status(thm)], [zip_derived_cl24240])).
% 77.37/11.59 thf(zip_derived_cl543, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (((sk__1) = (sk__3))
% 77.37/11.59 | ~ (ordinal @ X1)
% 77.37/11.59 | ~ (in @ X1 @ X0)
% 77.37/11.59 | (in @ X1 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl360, zip_derived_cl161])).
% 77.37/11.59 thf(zip_derived_cl24414, plain,
% 77.37/11.59 ((((sk__1) = (sk__3))
% 77.37/11.59 | (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ (sk__4 @ sk__8)))
% 77.37/11.59 | ~ (ordinal @ (sk__9 @ (sk__4 @ sk__8)))
% 77.37/11.59 | ((sk__1) = (sk__3)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl24391, zip_derived_cl543])).
% 77.37/11.59 thf(zip_derived_cl24445, plain,
% 77.37/11.59 ((~ (ordinal @ (sk__9 @ (sk__4 @ sk__8)))
% 77.37/11.59 | (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ (sk__4 @ sk__8)))
% 77.37/11.59 | ((sk__1) = (sk__3)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl24414])).
% 77.37/11.59 thf(zip_derived_cl337, plain,
% 77.37/11.59 (![X0 : $i]:
% 77.37/11.59 ( (zip_tseitin_0 @ sk__3 @ sk__2 @ sk__1)
% 77.37/11.59 | (ordinal @ (sk__9 @ (sk__4 @ X0))))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl336])).
% 77.37/11.59 thf(zip_derived_cl3, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 (((X1) = (X0)) | ~ (zip_tseitin_0 @ X0 @ X2 @ X1))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_7])).
% 77.37/11.59 thf(zip_derived_cl496, plain,
% 77.37/11.59 (![X0 : $i]: ( (ordinal @ (sk__9 @ (sk__4 @ X0))) | ((sk__1) = (sk__3)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl337, zip_derived_cl3])).
% 77.37/11.59 thf(zip_derived_cl24679, plain,
% 77.37/11.59 ((((sk__1) = (sk__3))
% 77.37/11.59 | (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ (sk__4 @ sk__8))))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl24445, zip_derived_cl496])).
% 77.37/11.59 thf(zip_derived_cl28673, plain, (((sk__1) = (sk__2))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl28672, zip_derived_cl494])).
% 77.37/11.59 thf(zip_derived_cl29034, plain,
% 77.37/11.59 ((((sk__2) = (sk__3))
% 77.37/11.59 | (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ (sk__4 @ sk__8))))),
% 77.37/11.59 inference('demod', [status(thm)],
% 77.37/11.59 [zip_derived_cl24679, zip_derived_cl28673])).
% 77.37/11.59 thf(zip_derived_cl45968, plain,
% 77.37/11.59 (( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ (sk__4 @ sk__8)))
% 77.37/11.59 | ~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8)))),
% 77.37/11.59 inference('clc', [status(thm)],
% 77.37/11.59 [zip_derived_cl45967, zip_derived_cl29034])).
% 77.37/11.59 thf(zip_derived_cl36429, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0)) | ((sk_ @ X0 @ X1) = (X1)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl36427, zip_derived_cl8])).
% 77.37/11.59 thf(zip_derived_cl45982, plain,
% 77.37/11.59 ((~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))
% 77.37/11.59 | ((sk_ @ (sk__4 @ sk__8) @ (sk__9 @ (sk__4 @ sk__8)))
% 77.37/11.59 = (sk__9 @ (sk__4 @ sk__8))))),
% 77.37/11.59 inference('sup-', [status(thm)],
% 77.37/11.59 [zip_derived_cl45968, zip_derived_cl36429])).
% 77.37/11.59 thf(zip_derived_cl51081, plain,
% 77.37/11.59 ((~ (ordinal @ (sk__9 @ (sk__4 @ sk__8)))
% 77.37/11.59 | ~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ sk__8)
% 77.37/11.59 | ((sk_ @ (sk__4 @ sk__8) @ (sk__9 @ (sk__4 @ sk__8)))
% 77.37/11.59 = (sk__9 @ (sk__4 @ sk__8))))),
% 77.37/11.59 inference('sup-', [status(thm)],
% 77.37/11.59 [zip_derived_cl31347, zip_derived_cl45982])).
% 77.37/11.59 thf(zip_derived_cl24, plain,
% 77.37/11.59 (![X0 : $i]: ( (ordinal @ (sk__9 @ X0)) | (in @ (sk__9 @ X0) @ X0))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_9])).
% 77.37/11.59 thf(zip_derived_cl36427, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X0 @ X1) @ X1 @ X0))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl28703, zip_derived_cl53])).
% 77.37/11.59 thf(zip_derived_cl7, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (ordinal @ X0) | ~ (zip_tseitin_2 @ X1 @ X0 @ X2))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_4])).
% 77.37/11.59 thf(zip_derived_cl36428, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]: (~ (in @ X1 @ (sk__4 @ X0)) | (ordinal @ X1))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl36427, zip_derived_cl7])).
% 77.37/11.59 thf(zip_derived_cl36564, plain,
% 77.37/11.59 (![X0 : $i]:
% 77.37/11.59 ( (ordinal @ (sk__9 @ (sk__4 @ X0)))
% 77.37/11.59 | (ordinal @ (sk__9 @ (sk__4 @ X0))))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl24, zip_derived_cl36428])).
% 77.37/11.59 thf(zip_derived_cl36597, plain,
% 77.37/11.59 (![X0 : $i]: (ordinal @ (sk__9 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl36564])).
% 77.37/11.59 thf(zip_derived_cl51096, plain,
% 77.37/11.59 ((~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ sk__8)
% 77.37/11.59 | ((sk_ @ (sk__4 @ sk__8) @ (sk__9 @ (sk__4 @ sk__8)))
% 77.37/11.59 = (sk__9 @ (sk__4 @ sk__8))))),
% 77.37/11.59 inference('demod', [status(thm)],
% 77.37/11.59 [zip_derived_cl51081, zip_derived_cl36597])).
% 77.37/11.59 thf(zip_derived_cl22635, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 ( (in @ (sk_ @ (sk__4 @ X1) @ X0) @ (sk__4 @ X1))
% 77.37/11.59 | ~ (in @ X0 @ X1)
% 77.37/11.59 | ~ (ordinal @ X0)
% 77.37/11.59 | ((sk__2) != (sk__3)))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl19698, zip_derived_cl163])).
% 77.37/11.59 thf(zip_derived_cl51309, plain,
% 77.37/11.59 (( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))
% 77.37/11.59 | ~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ sk__8)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (ordinal @ (sk__9 @ (sk__4 @ sk__8)))
% 77.37/11.59 | ~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ sk__8))),
% 77.37/11.59 inference('sup+', [status(thm)],
% 77.37/11.59 [zip_derived_cl51096, zip_derived_cl22635])).
% 77.37/11.59 thf(zip_derived_cl36597, plain,
% 77.37/11.59 (![X0 : $i]: (ordinal @ (sk__9 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl36564])).
% 77.37/11.59 thf(zip_derived_cl51351, plain,
% 77.37/11.59 (( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))
% 77.37/11.59 | ~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ sk__8)
% 77.37/11.59 | ((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ sk__8))),
% 77.37/11.59 inference('demod', [status(thm)],
% 77.37/11.59 [zip_derived_cl51309, zip_derived_cl36597])).
% 77.37/11.59 thf(zip_derived_cl51352, plain,
% 77.37/11.59 ((((sk__2) != (sk__3))
% 77.37/11.59 | ~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ sk__8)
% 77.37/11.59 | (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl51351])).
% 77.37/11.59 thf(zip_derived_cl24391, plain,
% 77.37/11.59 (( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))
% 77.37/11.59 | ((sk__1) = (sk__3)))),
% 77.37/11.59 inference('eq_fact', [status(thm)], [zip_derived_cl24240])).
% 77.37/11.59 thf(zip_derived_cl28673, plain, (((sk__1) = (sk__2))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl28672, zip_derived_cl494])).
% 77.37/11.59 thf(zip_derived_cl28981, plain,
% 77.37/11.59 (( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))
% 77.37/11.59 | ((sk__2) = (sk__3)))),
% 77.37/11.59 inference('demod', [status(thm)],
% 77.37/11.59 [zip_derived_cl24391, zip_derived_cl28673])).
% 77.37/11.59 thf(zip_derived_cl51520, plain,
% 77.37/11.59 (( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))
% 77.37/11.59 | ~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ sk__8))),
% 77.37/11.59 inference('clc', [status(thm)],
% 77.37/11.59 [zip_derived_cl51352, zip_derived_cl28981])).
% 77.37/11.59 thf(zip_derived_cl23, plain,
% 77.37/11.59 (![X0 : $i]: ( (in @ (sk__9 @ X0) @ sk__8) | (in @ (sk__9 @ X0) @ X0))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_9])).
% 77.37/11.59 thf(zip_derived_cl51521, plain,
% 77.37/11.59 ( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl51520, zip_derived_cl23])).
% 77.37/11.59 thf(zip_derived_cl36429, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0)) | ((sk_ @ X0 @ X1) = (X1)))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl36427, zip_derived_cl8])).
% 77.37/11.59 thf(zip_derived_cl51538, plain,
% 77.37/11.59 (((sk_ @ sk__8 @ (sk__9 @ (sk__4 @ sk__8))) = (sk__9 @ (sk__4 @ sk__8)))),
% 77.37/11.59 inference('sup-', [status(thm)],
% 77.37/11.59 [zip_derived_cl51521, zip_derived_cl36429])).
% 77.37/11.59 thf(zip_derived_cl36427, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i]:
% 77.37/11.59 (~ (in @ X1 @ (sk__4 @ X0))
% 77.37/11.59 | (zip_tseitin_2 @ (sk_ @ X0 @ X1) @ X1 @ X0))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl28703, zip_derived_cl53])).
% 77.37/11.59 thf(zip_derived_cl51901, plain,
% 77.37/11.59 (( (zip_tseitin_2 @ (sk__9 @ (sk__4 @ sk__8)) @
% 77.37/11.59 (sk__9 @ (sk__4 @ sk__8)) @ sk__8)
% 77.37/11.59 | ~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8)))),
% 77.37/11.59 inference('sup+', [status(thm)],
% 77.37/11.59 [zip_derived_cl51538, zip_derived_cl36427])).
% 77.37/11.59 thf(zip_derived_cl51521, plain,
% 77.37/11.59 ( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl51520, zip_derived_cl23])).
% 77.37/11.59 thf(zip_derived_cl51938, plain,
% 77.37/11.59 ( (zip_tseitin_2 @ (sk__9 @ (sk__4 @ sk__8)) @
% 77.37/11.59 (sk__9 @ (sk__4 @ sk__8)) @ sk__8)),
% 77.37/11.59 inference('demod', [status(thm)],
% 77.37/11.59 [zip_derived_cl51901, zip_derived_cl51521])).
% 77.37/11.59 thf(zip_derived_cl9, plain,
% 77.37/11.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 77.37/11.59 ( (in @ X0 @ X1) | ~ (zip_tseitin_2 @ X0 @ X2 @ X1))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_4])).
% 77.37/11.59 thf(zip_derived_cl52865, plain, ( (in @ (sk__9 @ (sk__4 @ sk__8)) @ sk__8)),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl51938, zip_derived_cl9])).
% 77.37/11.59 thf(zip_derived_cl25, plain,
% 77.37/11.59 (![X0 : $i]:
% 77.37/11.59 (~ (ordinal @ (sk__9 @ X0))
% 77.37/11.59 | ~ (in @ (sk__9 @ X0) @ sk__8)
% 77.37/11.59 | ~ (in @ (sk__9 @ X0) @ X0))),
% 77.37/11.59 inference('cnf', [status(esa)], [zf_stmt_9])).
% 77.37/11.59 thf(zip_derived_cl52879, plain,
% 77.37/11.59 ((~ (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))
% 77.37/11.59 | ~ (ordinal @ (sk__9 @ (sk__4 @ sk__8))))),
% 77.37/11.59 inference('sup-', [status(thm)], [zip_derived_cl52865, zip_derived_cl25])).
% 77.37/11.59 thf(zip_derived_cl51521, plain,
% 77.37/11.59 ( (in @ (sk__9 @ (sk__4 @ sk__8)) @ (sk__4 @ sk__8))),
% 77.37/11.59 inference('clc', [status(thm)], [zip_derived_cl51520, zip_derived_cl23])).
% 77.37/11.59 thf(zip_derived_cl36597, plain,
% 77.37/11.59 (![X0 : $i]: (ordinal @ (sk__9 @ (sk__4 @ X0)))),
% 77.37/11.59 inference('simplify', [status(thm)], [zip_derived_cl36564])).
% 77.37/11.59 thf(zip_derived_cl52891, plain, ($false),
% 77.37/11.59 inference('demod', [status(thm)],
% 77.37/11.59 [zip_derived_cl52879, zip_derived_cl51521, zip_derived_cl36597])).
% 77.37/11.59
% 77.37/11.59 % SZS output end Refutation
% 77.37/11.59
% 77.37/11.59
% 77.37/11.59 % Terminating...
% 77.37/11.66 % Runner terminated.
% 77.37/11.66 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------