%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEU272+1 : TPTP v9.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.hEXcAz2PhW true
% Computer : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 04:54:05 PM UTC 2025
% Result : Theorem 25.72s 4.30s
% Output : Refutation 25.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SEU272+1 : TPTP v9.2.0. Released v3.3.0.
% 0.07/0.14 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.hEXcAz2PhW true
% 0.13/0.35 % Computer : n021.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Oct 1 16:03:23 EDT 2025
% 0.13/0.35 % CPUTime :
% 0.13/0.35 % Running portfolio for 300 s
% 0.13/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.35 % Number of cores: 8
% 0.13/0.35 % Python version: Python 3.6.8
% 0.13/0.36 % Running in FO mode
% 0.40/0.59 % Total configuration time : 435
% 0.40/0.59 % Estimated wc time : 1092
% 0.40/0.59 % Estimated cpu time (7 cpus) : 156.0
% 0.47/0.67 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.48/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.48/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.48/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.48/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.48/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.48/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 25.72/4.29 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 25.72/4.30 % Solved by fo/fo7.sh.
% 25.72/4.30 % done 1847 iterations in 3.533s
% 25.72/4.30 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 25.72/4.30 % SZS output start Refutation
% 25.72/4.30 thf(sk__2_type, type, sk__2: $i > $i).
% 25.72/4.30 thf(sk__12_type, type, sk__12: $i > $i).
% 25.72/4.30 thf(epsilon_transitive_type, type, epsilon_transitive: $i > $o).
% 25.72/4.30 thf(sk__10_type, type, sk__10: $i > $i > $i).
% 25.72/4.30 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $i > $i > $i > $o).
% 25.72/4.30 thf(sk__14_type, type, sk__14: $i > $i).
% 25.72/4.30 thf(sk__1_type, type, sk__1: $i).
% 25.72/4.30 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $i > $o).
% 25.72/4.30 thf(ordinal_type, type, ordinal: $i > $o).
% 25.72/4.30 thf(sk__11_type, type, sk__11: $i > $i > $i > $i).
% 25.72/4.30 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $i > $o).
% 25.72/4.30 thf(sk__15_type, type, sk__15: $i > $i > $i).
% 25.72/4.30 thf(zip_tseitin_5_type, type, zip_tseitin_5: $i > $i > $i > $i > $o).
% 25.72/4.30 thf(sk__13_type, type, sk__13: $i > $i).
% 25.72/4.30 thf(sk__type, type, sk_: $i).
% 25.72/4.30 thf(sk__3_type, type, sk__3: $i > $i).
% 25.72/4.30 thf(zip_tseitin_6_type, type, zip_tseitin_6: $i > $i > $i > $i > $o).
% 25.72/4.30 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $i > $i > $o).
% 25.72/4.30 thf(zip_tseitin_4_type, type, zip_tseitin_4: $i > $i > $i > $o).
% 25.72/4.30 thf(succ_type, type, succ: $i > $i).
% 25.72/4.30 thf(epsilon_connected_type, type, epsilon_connected: $i > $o).
% 25.72/4.30 thf(in_type, type, in: $i > $i > $o).
% 25.72/4.30 thf(s1_xboole_0__e8_6__wellord2__1, conjecture,
% 25.72/4.30 (![A:$i,B:$i]:
% 25.72/4.30 ( ( ordinal @ B ) =>
% 25.72/4.30 ( ?[C:$i]:
% 25.72/4.30 ( ![D:$i]:
% 25.72/4.30 ( ( in @ D @ C ) <=>
% 25.72/4.30 ( ( in @ D @ ( succ @ B ) ) &
% 25.72/4.30 ( ?[E:$i]:
% 25.72/4.30 ( ( in @ E @ A ) & ( ( D ) = ( E ) ) & ( ordinal @ E ) ) ) ) ) ) ) ))).
% 25.72/4.30 thf(zf_stmt_0, negated_conjecture,
% 25.72/4.30 (~( ![A:$i,B:$i]:
% 25.72/4.30 ( ( ordinal @ B ) =>
% 25.72/4.30 ( ?[C:$i]:
% 25.72/4.30 ( ![D:$i]:
% 25.72/4.30 ( ( in @ D @ C ) <=>
% 25.72/4.30 ( ( in @ D @ ( succ @ B ) ) &
% 25.72/4.30 ( ?[E:$i]:
% 25.72/4.30 ( ( in @ E @ A ) & ( ( D ) = ( E ) ) & ( ordinal @ E ) ) ) ) ) ) ) ) )),
% 25.72/4.30 inference('cnf.neg', [status(esa)], [s1_xboole_0__e8_6__wellord2__1])).
% 25.72/4.30 thf(zip_derived_cl4, plain,
% 25.72/4.30 (![X1 : $i]: (((sk__2 @ X1) = (sk__3 @ X1)) | (in @ (sk__2 @ X1) @ X1))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_0])).
% 25.72/4.30 thf(s1_tarski__e8_6__wellord2__1, axiom,
% 25.72/4.30 (![A:$i,B:$i]:
% 25.72/4.30 ( ( ordinal @ B ) =>
% 25.72/4.30 ( ( ![C:$i,D:$i,E:$i]:
% 25.72/4.30 ( ( ( ?[G:$i]:
% 25.72/4.30 ( ( ordinal @ G ) & ( ( E ) = ( G ) ) & ( in @ G @ A ) ) ) &
% 25.72/4.30 ( ( C ) = ( E ) ) &
% 25.72/4.30 ( ?[F:$i]:
% 25.72/4.30 ( ( ordinal @ F ) & ( ( D ) = ( F ) ) & ( in @ F @ A ) ) ) &
% 25.72/4.30 ( ( C ) = ( D ) ) ) =>
% 25.72/4.30 ( ( D ) = ( E ) ) ) ) =>
% 25.72/4.30 ( ?[C:$i]:
% 25.72/4.30 ( ![D:$i]:
% 25.72/4.30 ( ( in @ D @ C ) <=>
% 25.72/4.30 ( ?[E:$i]:
% 25.72/4.30 ( ( in @ E @ ( succ @ B ) ) & ( ( E ) = ( D ) ) &
% 25.72/4.30 ( ?[H:$i]:
% 25.72/4.30 ( ( ordinal @ H ) & ( ( D ) = ( H ) ) & ( in @ H @ A ) ) ) ) ) ) ) ) ) ))).
% 25.72/4.30 thf(zf_stmt_1, axiom,
% 25.72/4.30 (![E:$i,D:$i,C:$i,A:$i]:
% 25.72/4.30 ( ( ( zip_tseitin_2 @ E @ D @ C @ A ) => ( ( D ) = ( E ) ) ) =>
% 25.72/4.30 ( zip_tseitin_3 @ E @ D @ C @ A ) ))).
% 25.72/4.30 thf(zip_derived_cl40, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 ( (zip_tseitin_3 @ X0 @ X1 @ X2 @ X3)
% 25.72/4.30 | (zip_tseitin_2 @ X0 @ X1 @ X2 @ X3))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_1])).
% 25.72/4.30 thf(zf_stmt_2, type, zip_tseitin_6 : $i > $i > $i > $i > $o).
% 25.72/4.30 thf(zf_stmt_3, axiom,
% 25.72/4.30 (![D:$i,C:$i,B:$i,A:$i]:
% 25.72/4.30 ( ( zip_tseitin_6 @ D @ C @ B @ A ) =>
% 25.72/4.30 ( ( in @ D @ C ) <=> ( ?[E:$i]: ( zip_tseitin_5 @ E @ D @ B @ A ) ) ) ))).
% 25.72/4.30 thf(zf_stmt_4, type, zip_tseitin_5 : $i > $i > $i > $i > $o).
% 25.72/4.30 thf(zf_stmt_5, axiom,
% 25.72/4.30 (![E:$i,D:$i,B:$i,A:$i]:
% 25.72/4.30 ( ( zip_tseitin_5 @ E @ D @ B @ A ) <=>
% 25.72/4.30 ( ( ?[H:$i]: ( zip_tseitin_4 @ H @ D @ A ) ) & ( ( E ) = ( D ) ) &
% 25.72/4.30 ( in @ E @ ( succ @ B ) ) ) ))).
% 25.72/4.30 thf(zf_stmt_6, type, zip_tseitin_4 : $i > $i > $i > $o).
% 25.72/4.30 thf(zf_stmt_7, axiom,
% 25.72/4.30 (![H:$i,D:$i,A:$i]:
% 25.72/4.30 ( ( zip_tseitin_4 @ H @ D @ A ) <=>
% 25.72/4.30 ( ( in @ H @ A ) & ( ( D ) = ( H ) ) & ( ordinal @ H ) ) ))).
% 25.72/4.30 thf(zf_stmt_8, type, zip_tseitin_3 : $i > $i > $i > $i > $o).
% 25.72/4.30 thf(zf_stmt_9, type, zip_tseitin_2 : $i > $i > $i > $i > $o).
% 25.72/4.30 thf(zf_stmt_10, axiom,
% 25.72/4.30 (![E:$i,D:$i,C:$i,A:$i]:
% 25.72/4.30 ( ( zip_tseitin_2 @ E @ D @ C @ A ) =>
% 25.72/4.30 ( ( ( C ) = ( D ) ) & ( ?[F:$i]: ( zip_tseitin_1 @ F @ D @ A ) ) &
% 25.72/4.30 ( ( C ) = ( E ) ) & ( ?[G:$i]: ( zip_tseitin_0 @ G @ E @ A ) ) ) ))).
% 25.72/4.30 thf(zf_stmt_11, type, zip_tseitin_1 : $i > $i > $i > $o).
% 25.72/4.30 thf(zf_stmt_12, axiom,
% 25.72/4.30 (![F:$i,D:$i,A:$i]:
% 25.72/4.30 ( ( zip_tseitin_1 @ F @ D @ A ) =>
% 25.72/4.30 ( ( in @ F @ A ) & ( ( D ) = ( F ) ) & ( ordinal @ F ) ) ))).
% 25.72/4.30 thf(zf_stmt_13, type, zip_tseitin_0 : $i > $i > $i > $o).
% 25.72/4.30 thf(zf_stmt_14, axiom,
% 25.72/4.30 (![G:$i,E:$i,A:$i]:
% 25.72/4.30 ( ( zip_tseitin_0 @ G @ E @ A ) =>
% 25.72/4.30 ( ( in @ G @ A ) & ( ( E ) = ( G ) ) & ( ordinal @ G ) ) ))).
% 25.72/4.30 thf(zf_stmt_15, axiom,
% 25.72/4.30 (![A:$i,B:$i]:
% 25.72/4.30 ( ( ordinal @ B ) =>
% 25.72/4.30 ( ( ![C:$i,D:$i,E:$i]: ( zip_tseitin_3 @ E @ D @ C @ A ) ) =>
% 25.72/4.30 ( ?[C:$i]: ( ![D:$i]: ( zip_tseitin_6 @ D @ C @ B @ A ) ) ) ) ))).
% 25.72/4.30 thf(zip_derived_cl51, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 (~ (zip_tseitin_3 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | ~ (ordinal @ X1)
% 25.72/4.30 | (zip_tseitin_6 @ X2 @ (sk__15 @ X1 @ X0) @ X1 @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_15])).
% 25.72/4.30 thf(zip_derived_cl177, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_6 @ X2 @ (sk__15 @ X1 @ X0) @ X1 @ X0)
% 25.72/4.30 | ~ (ordinal @ X1))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl40, zip_derived_cl51])).
% 25.72/4.30 thf(cc2_ordinal1, axiom,
% 25.72/4.30 (![A:$i]:
% 25.72/4.30 ( ( ( epsilon_transitive @ A ) & ( epsilon_connected @ A ) ) =>
% 25.72/4.30 ( ordinal @ A ) ))).
% 25.72/4.30 thf(zip_derived_cl7, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (ordinal @ X0)
% 25.72/4.30 | ~ (epsilon_connected @ X0)
% 25.72/4.30 | ~ (epsilon_transitive @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [cc2_ordinal1])).
% 25.72/4.30 thf(zip_derived_cl238, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 ( (zip_tseitin_6 @ X2 @ (sk__15 @ X0 @ X1) @ X0 @ X1)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X1) @ (sk__13 @ X1) @ (sk__12 @ X1) @
% 25.72/4.30 X1)
% 25.72/4.30 | ~ (epsilon_transitive @ X0)
% 25.72/4.30 | ~ (epsilon_connected @ X0))),
% 25.72/4.30 inference('sup+', [status(thm)], [zip_derived_cl177, zip_derived_cl7])).
% 25.72/4.30 thf(zip_derived_cl7, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (ordinal @ X0)
% 25.72/4.30 | ~ (epsilon_connected @ X0)
% 25.72/4.30 | ~ (epsilon_transitive @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [cc2_ordinal1])).
% 25.72/4.30 thf(zip_derived_cl7, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (ordinal @ X0)
% 25.72/4.30 | ~ (epsilon_connected @ X0)
% 25.72/4.30 | ~ (epsilon_transitive @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [cc2_ordinal1])).
% 25.72/4.30 thf(zip_derived_cl4, plain,
% 25.72/4.30 (![X1 : $i]: (((sk__2 @ X1) = (sk__3 @ X1)) | (in @ (sk__2 @ X1) @ X1))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_0])).
% 25.72/4.30 thf(zip_derived_cl44, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 ( (zip_tseitin_4 @ X0 @ X1 @ X2)
% 25.72/4.30 | ~ (ordinal @ X0)
% 25.72/4.30 | ((X1) != (X0))
% 25.72/4.30 | ~ (in @ X0 @ X2))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.30 thf(zip_derived_cl81, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i]:
% 25.72/4.30 (~ (in @ X1 @ X0) | ~ (ordinal @ X1) | (zip_tseitin_4 @ X1 @ X1 @ X0))),
% 25.72/4.30 inference('eq_res', [status(thm)], [zip_derived_cl44])).
% 25.72/4.30 thf(zip_derived_cl83, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (((sk__2 @ X0) = (sk__3 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ~ (ordinal @ (sk__2 @ X0)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl4, zip_derived_cl81])).
% 25.72/4.30 thf(zip_derived_cl117, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ((sk__2 @ X0) = (sk__3 @ X0)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl7, zip_derived_cl83])).
% 25.72/4.30 thf(zip_derived_cl7, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (ordinal @ X0)
% 25.72/4.30 | ~ (epsilon_connected @ X0)
% 25.72/4.30 | ~ (epsilon_transitive @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [cc2_ordinal1])).
% 25.72/4.30 thf(zip_derived_cl5, plain,
% 25.72/4.30 (![X1 : $i]: ( (in @ (sk__3 @ X1) @ sk_) | (in @ (sk__2 @ X1) @ X1))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_0])).
% 25.72/4.30 thf(zip_derived_cl81, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i]:
% 25.72/4.30 (~ (in @ X1 @ X0) | ~ (ordinal @ X1) | (zip_tseitin_4 @ X1 @ X1 @ X0))),
% 25.72/4.30 inference('eq_res', [status(thm)], [zip_derived_cl44])).
% 25.72/4.30 thf(zip_derived_cl84, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (in @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_4 @ (sk__3 @ X0) @ (sk__3 @ X0) @ sk_)
% 25.72/4.30 | ~ (ordinal @ (sk__3 @ X0)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl81])).
% 25.72/4.30 thf(zip_derived_cl3, plain,
% 25.72/4.30 (![X1 : $i]: ( (ordinal @ (sk__3 @ X1)) | (in @ (sk__2 @ X1) @ X1))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_0])).
% 25.72/4.30 thf(zip_derived_cl119, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_4 @ (sk__3 @ X0) @ (sk__3 @ X0) @ sk_)
% 25.72/4.30 | (in @ (sk__2 @ X0) @ X0))),
% 25.72/4.30 inference('clc', [status(thm)], [zip_derived_cl84, zip_derived_cl3])).
% 25.72/4.30 thf(zip_derived_cl81, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i]:
% 25.72/4.30 (~ (in @ X1 @ X0) | ~ (ordinal @ X1) | (zip_tseitin_4 @ X1 @ X1 @ X0))),
% 25.72/4.30 inference('eq_res', [status(thm)], [zip_derived_cl44])).
% 25.72/4.30 thf(zip_derived_cl121, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_4 @ (sk__3 @ X0) @ (sk__3 @ X0) @ sk_)
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ~ (ordinal @ (sk__2 @ X0)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl119, zip_derived_cl81])).
% 25.72/4.30 thf(zip_derived_cl164, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_4 @ (sk__3 @ X0) @ (sk__3 @ X0) @ sk_))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl7, zip_derived_cl121])).
% 25.72/4.30 thf(zip_derived_cl274, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_4 @ (sk__3 @ X0) @ (sk__2 @ X0) @ sk_)
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ X0)))),
% 25.72/4.30 inference('sup+', [status(thm)], [zip_derived_cl117, zip_derived_cl164])).
% 25.72/4.30 thf(zip_derived_cl278, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_4 @ (sk__3 @ X0) @ (sk__2 @ X0) @ sk_))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl274])).
% 25.72/4.30 thf(zip_derived_cl2, plain,
% 25.72/4.30 (![X1 : $i]:
% 25.72/4.30 ( (in @ (sk__2 @ X1) @ (succ @ sk__1)) | (in @ (sk__2 @ X1) @ X1))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_0])).
% 25.72/4.30 thf(zip_derived_cl48, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 25.72/4.30 ( (zip_tseitin_5 @ X0 @ X1 @ X2 @ X3)
% 25.72/4.30 | ~ (in @ X0 @ (succ @ X2))
% 25.72/4.30 | ((X0) != (X1))
% 25.72/4.30 | ~ (zip_tseitin_4 @ X4 @ X1 @ X3))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.30 thf(zip_derived_cl101, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 (~ (zip_tseitin_4 @ X2 @ X1 @ X0)
% 25.72/4.30 | ~ (in @ X1 @ (succ @ X3))
% 25.72/4.30 | (zip_tseitin_5 @ X1 @ X1 @ X3 @ X0))),
% 25.72/4.30 inference('eq_res', [status(thm)], [zip_derived_cl48])).
% 25.72/4.30 thf(zip_derived_cl106, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 ( (in @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ X0) @ (sk__2 @ X0) @ sk__1 @ X1)
% 25.72/4.30 | ~ (zip_tseitin_4 @ X2 @ (sk__2 @ X0) @ X1))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl2, zip_derived_cl101])).
% 25.72/4.30 thf(zip_derived_cl333, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ X0) @ (sk__2 @ X0) @ sk__1 @ sk_)
% 25.72/4.30 | (in @ (sk__2 @ X0) @ X0))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl278, zip_derived_cl106])).
% 25.72/4.30 thf(zip_derived_cl41, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 ( (in @ X0 @ X1) | ~ (zip_tseitin_4 @ X0 @ X2 @ X1))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.30 thf(zip_derived_cl538, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (in @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ X0) @ (sk__2 @ X0) @ sk__1 @ sk_)
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0)))),
% 25.72/4.30 inference('clc', [status(thm)], [zip_derived_cl333, zip_derived_cl41])).
% 25.72/4.30 thf(zip_derived_cl81, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i]:
% 25.72/4.30 (~ (in @ X1 @ X0) | ~ (ordinal @ X1) | (zip_tseitin_4 @ X1 @ X1 @ X0))),
% 25.72/4.30 inference('eq_res', [status(thm)], [zip_derived_cl44])).
% 25.72/4.30 thf(zip_derived_cl540, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ X0) @ (sk__2 @ X0) @ sk__1 @ sk_)
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ~ (ordinal @ (sk__2 @ X0)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl538, zip_derived_cl81])).
% 25.72/4.30 thf(cc1_ordinal1, axiom,
% 25.72/4.30 (![A:$i]:
% 25.72/4.30 ( ( ordinal @ A ) =>
% 25.72/4.30 ( ( epsilon_transitive @ A ) & ( epsilon_connected @ A ) ) ))).
% 25.72/4.30 thf(zip_derived_cl24, plain,
% 25.72/4.30 (![X0 : $i]: ( (epsilon_connected @ X0) | ~ (ordinal @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [cc1_ordinal1])).
% 25.72/4.30 thf(zip_derived_cl550, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (ordinal @ (sk__2 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ X0) @ (sk__2 @ X0) @ sk__1 @ sk_)
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ X0)))),
% 25.72/4.30 inference('clc', [status(thm)], [zip_derived_cl540, zip_derived_cl24])).
% 25.72/4.30 thf(zip_derived_cl23, plain,
% 25.72/4.30 (![X0 : $i]: ( (epsilon_transitive @ X0) | ~ (ordinal @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [cc1_ordinal1])).
% 25.72/4.30 thf(zip_derived_cl551, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_5 @ (sk__2 @ X0) @ (sk__2 @ X0) @ sk__1 @ sk_)
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ~ (ordinal @ (sk__2 @ X0)))),
% 25.72/4.30 inference('clc', [status(thm)], [zip_derived_cl550, zip_derived_cl23])).
% 25.72/4.30 thf(zip_derived_cl552, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ X0) @ (sk__2 @ X0) @ sk__1 @ sk_))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl7, zip_derived_cl551])).
% 25.72/4.30 thf(zip_derived_cl49, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 25.72/4.30 (~ (zip_tseitin_5 @ X0 @ X1 @ X2 @ X3)
% 25.72/4.30 | (in @ X1 @ X4)
% 25.72/4.30 | ~ (zip_tseitin_6 @ X1 @ X4 @ X2 @ X3))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_3])).
% 25.72/4.30 thf(zip_derived_cl561, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i]:
% 25.72/4.30 ( (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | ~ (zip_tseitin_6 @ (sk__2 @ X0) @ X1 @ sk__1 @ sk_)
% 25.72/4.30 | (in @ (sk__2 @ X0) @ X1))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl552, zip_derived_cl49])).
% 25.72/4.30 thf(zip_derived_cl552, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ X0) @ (sk__2 @ X0) @ sk__1 @ sk_))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl7, zip_derived_cl551])).
% 25.72/4.30 thf(zip_derived_cl47, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 ( (in @ X0 @ (succ @ X1)) | ~ (zip_tseitin_5 @ X0 @ X2 @ X1 @ X3))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.30 thf(zip_derived_cl560, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | (in @ (sk__2 @ X0) @ (succ @ sk__1)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl552, zip_derived_cl47])).
% 25.72/4.30 thf(zip_derived_cl117, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ((sk__2 @ X0) = (sk__3 @ X0)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl7, zip_derived_cl83])).
% 25.72/4.30 thf(zip_derived_cl164, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_4 @ (sk__3 @ X0) @ (sk__3 @ X0) @ sk_))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl7, zip_derived_cl121])).
% 25.72/4.30 thf(zip_derived_cl41, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 ( (in @ X0 @ X1) | ~ (zip_tseitin_4 @ X0 @ X2 @ X1))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.30 thf(zip_derived_cl271, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | (in @ (sk__3 @ X0) @ sk_))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl164, zip_derived_cl41])).
% 25.72/4.30 thf(zip_derived_cl294, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (in @ (sk__2 @ X0) @ sk_)
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0))),
% 25.72/4.30 inference('sup+', [status(thm)], [zip_derived_cl117, zip_derived_cl271])).
% 25.72/4.30 thf(zip_derived_cl296, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | (in @ (sk__2 @ X0) @ sk_))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl294])).
% 25.72/4.30 thf(zip_derived_cl4, plain,
% 25.72/4.30 (![X1 : $i]: (((sk__2 @ X1) = (sk__3 @ X1)) | (in @ (sk__2 @ X1) @ X1))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_0])).
% 25.72/4.30 thf(zip_derived_cl177, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_6 @ X2 @ (sk__15 @ X1 @ X0) @ X1 @ X0)
% 25.72/4.30 | ~ (ordinal @ X1))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl40, zip_derived_cl51])).
% 25.72/4.30 thf(zip_derived_cl0, plain, ( (ordinal @ sk__1)),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_0])).
% 25.72/4.30 thf(zip_derived_cl241, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i]:
% 25.72/4.30 ( (zip_tseitin_6 @ X1 @ (sk__15 @ sk__1 @ X0) @ sk__1 @ X0)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0))),
% 25.72/4.30 inference('sup+', [status(thm)], [zip_derived_cl177, zip_derived_cl0])).
% 25.72/4.30 thf(zip_derived_cl50, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 (~ (in @ X0 @ X1)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__11 @ X2 @ X3 @ X0) @ X0 @ X3 @ X2)
% 25.72/4.30 | ~ (zip_tseitin_6 @ X0 @ X1 @ X3 @ X2))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_3])).
% 25.72/4.30 thf(zip_derived_cl254, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__11 @ X0 @ sk__1 @ X1) @ X1 @ sk__1 @ X0)
% 25.72/4.30 | ~ (in @ X1 @ (sk__15 @ sk__1 @ X0)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl241, zip_derived_cl50])).
% 25.72/4.30 thf(zip_derived_cl414, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (((sk__2 @ (sk__15 @ sk__1 @ X0)) = (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_5 @
% 25.72/4.30 (sk__11 @ X0 @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ X0))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl4, zip_derived_cl254])).
% 25.72/4.30 thf(zip_derived_cl46, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 (((X1) = (X0)) | ~ (zip_tseitin_5 @ X1 @ X0 @ X2 @ X3))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.30 thf(zip_derived_cl2805, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | ((sk__2 @ (sk__15 @ sk__1 @ X0)) = (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | ((sk__11 @ X0 @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 = (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl414, zip_derived_cl46])).
% 25.72/4.30 thf(zip_derived_cl414, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (((sk__2 @ (sk__15 @ sk__1 @ X0)) = (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_5 @
% 25.72/4.30 (sk__11 @ X0 @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ X0))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl4, zip_derived_cl254])).
% 25.72/4.30 thf(zip_derived_cl2812, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | ((sk__2 @ (sk__15 @ sk__1 @ X0)) = (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | ((sk__2 @ (sk__15 @ sk__1 @ X0)) = (sk__3 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('sup+', [status(thm)], [zip_derived_cl2805, zip_derived_cl414])).
% 25.72/4.30 thf(zip_derived_cl2819, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | ((sk__2 @ (sk__15 @ sk__1 @ X0)) = (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl2812])).
% 25.72/4.30 thf(zip_derived_cl3, plain,
% 25.72/4.30 (![X1 : $i]: ( (ordinal @ (sk__3 @ X1)) | (in @ (sk__2 @ X1) @ X1))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_0])).
% 25.72/4.30 thf(zip_derived_cl254, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__11 @ X0 @ sk__1 @ X1) @ X1 @ sk__1 @ X0)
% 25.72/4.30 | ~ (in @ X1 @ (sk__15 @ sk__1 @ X0)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl241, zip_derived_cl50])).
% 25.72/4.30 thf(zip_derived_cl413, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (ordinal @ (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_5 @
% 25.72/4.30 (sk__11 @ X0 @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ X0))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl3, zip_derived_cl254])).
% 25.72/4.30 thf(zip_derived_cl24, plain,
% 25.72/4.30 (![X0 : $i]: ( (epsilon_connected @ X0) | ~ (ordinal @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [cc1_ordinal1])).
% 25.72/4.30 thf(zip_derived_cl489, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_5 @
% 25.72/4.30 (sk__11 @ X0 @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ X0))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (epsilon_connected @ (sk__3 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl413, zip_derived_cl24])).
% 25.72/4.30 thf(zip_derived_cl46, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 (((X1) = (X0)) | ~ (zip_tseitin_5 @ X1 @ X0 @ X2 @ X3))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.30 thf(zip_derived_cl987, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (epsilon_connected @ (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | ((sk__11 @ X0 @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 = (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl489, zip_derived_cl46])).
% 25.72/4.30 thf(zip_derived_cl489, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_5 @
% 25.72/4.30 (sk__11 @ X0 @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ X0))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (epsilon_connected @ (sk__3 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl413, zip_derived_cl24])).
% 25.72/4.30 thf(zip_derived_cl1000, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (epsilon_connected @ (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (epsilon_connected @ (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0))),
% 25.72/4.30 inference('sup+', [status(thm)], [zip_derived_cl987, zip_derived_cl489])).
% 25.72/4.30 thf(zip_derived_cl1006, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (epsilon_connected @ (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl1000])).
% 25.72/4.30 thf(zip_derived_cl2859, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0))),
% 25.72/4.30 inference('sup+', [status(thm)], [zip_derived_cl2819, zip_derived_cl1006])).
% 25.72/4.30 thf(zip_derived_cl2885, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl2859])).
% 25.72/4.30 thf(zip_derived_cl45, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 ( (zip_tseitin_4 @ (sk__10 @ X0 @ X1) @ X1 @ X0)
% 25.72/4.30 | ~ (zip_tseitin_5 @ X2 @ X1 @ X3 @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.30 thf(zip_derived_cl3457, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (zip_tseitin_4 @
% 25.72/4.30 (sk__10 @ X0 @ (sk__2 @ (sk__15 @ sk__1 @ X0))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ X0))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl2885, zip_derived_cl45])).
% 25.72/4.30 thf(zip_derived_cl42, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 (((X1) = (X0)) | ~ (zip_tseitin_4 @ X0 @ X1 @ X2))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.30 thf(zip_derived_cl3810, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | ((sk__2 @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 = (sk__10 @ X0 @ (sk__2 @ (sk__15 @ sk__1 @ X0)))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl3457, zip_derived_cl42])).
% 25.72/4.30 thf(zip_derived_cl3457, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (zip_tseitin_4 @
% 25.72/4.30 (sk__10 @ X0 @ (sk__2 @ (sk__15 @ sk__1 @ X0))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ X0))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl2885, zip_derived_cl45])).
% 25.72/4.30 thf(zip_derived_cl43, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 ( (ordinal @ X0) | ~ (zip_tseitin_4 @ X0 @ X1 @ X2))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.30 thf(zip_derived_cl3811, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (ordinal @ (sk__10 @ X0 @ (sk__2 @ (sk__15 @ sk__1 @ X0)))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl3457, zip_derived_cl43])).
% 25.72/4.30 thf(zip_derived_cl24, plain,
% 25.72/4.30 (![X0 : $i]: ( (epsilon_connected @ X0) | ~ (ordinal @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [cc1_ordinal1])).
% 25.72/4.30 thf(zip_derived_cl3820, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (epsilon_connected @
% 25.72/4.30 (sk__10 @ X0 @ (sk__2 @ (sk__15 @ sk__1 @ X0)))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl3811, zip_derived_cl24])).
% 25.72/4.30 thf(zip_derived_cl3942, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('sup+', [status(thm)], [zip_derived_cl3810, zip_derived_cl3820])).
% 25.72/4.30 thf(zip_derived_cl3975, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl3942])).
% 25.72/4.30 thf(zip_derived_cl2819, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | ((sk__2 @ (sk__15 @ sk__1 @ X0)) = (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl2812])).
% 25.72/4.30 thf(zip_derived_cl413, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (ordinal @ (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_5 @
% 25.72/4.30 (sk__11 @ X0 @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ X0))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl3, zip_derived_cl254])).
% 25.72/4.30 thf(zip_derived_cl23, plain,
% 25.72/4.30 (![X0 : $i]: ( (epsilon_transitive @ X0) | ~ (ordinal @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [cc1_ordinal1])).
% 25.72/4.30 thf(zip_derived_cl488, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_5 @
% 25.72/4.30 (sk__11 @ X0 @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ X0))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (epsilon_transitive @ (sk__3 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl413, zip_derived_cl23])).
% 25.72/4.30 thf(zip_derived_cl46, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 (((X1) = (X0)) | ~ (zip_tseitin_5 @ X1 @ X0 @ X2 @ X3))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.30 thf(zip_derived_cl708, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (epsilon_transitive @ (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | ((sk__11 @ X0 @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 = (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl488, zip_derived_cl46])).
% 25.72/4.30 thf(zip_derived_cl488, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_5 @
% 25.72/4.30 (sk__11 @ X0 @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ X0))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (epsilon_transitive @ (sk__3 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl413, zip_derived_cl23])).
% 25.72/4.30 thf(zip_derived_cl714, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (epsilon_transitive @ (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (epsilon_transitive @ (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0))),
% 25.72/4.30 inference('sup+', [status(thm)], [zip_derived_cl708, zip_derived_cl488])).
% 25.72/4.30 thf(zip_derived_cl716, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (epsilon_transitive @ (sk__3 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl714])).
% 25.72/4.30 thf(zip_derived_cl2854, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0))),
% 25.72/4.30 inference('sup+', [status(thm)], [zip_derived_cl2819, zip_derived_cl716])).
% 25.72/4.30 thf(zip_derived_cl2880, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk__1 @ X0)
% 25.72/4.30 | (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl2854])).
% 25.72/4.30 thf(zip_derived_cl45, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 ( (zip_tseitin_4 @ (sk__10 @ X0 @ X1) @ X1 @ X0)
% 25.72/4.30 | ~ (zip_tseitin_5 @ X2 @ X1 @ X3 @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.30 thf(zip_derived_cl3352, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (zip_tseitin_4 @
% 25.72/4.30 (sk__10 @ X0 @ (sk__2 @ (sk__15 @ sk__1 @ X0))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ X0))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl2880, zip_derived_cl45])).
% 25.72/4.30 thf(zip_derived_cl42, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 (((X1) = (X0)) | ~ (zip_tseitin_4 @ X0 @ X1 @ X2))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.30 thf(zip_derived_cl3576, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | ((sk__2 @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 = (sk__10 @ X0 @ (sk__2 @ (sk__15 @ sk__1 @ X0)))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl3352, zip_derived_cl42])).
% 25.72/4.30 thf(zip_derived_cl3352, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (zip_tseitin_4 @
% 25.72/4.30 (sk__10 @ X0 @ (sk__2 @ (sk__15 @ sk__1 @ X0))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ X0))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl2880, zip_derived_cl45])).
% 25.72/4.30 thf(zip_derived_cl43, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 ( (ordinal @ X0) | ~ (zip_tseitin_4 @ X0 @ X1 @ X2))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.30 thf(zip_derived_cl3577, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (ordinal @ (sk__10 @ X0 @ (sk__2 @ (sk__15 @ sk__1 @ X0)))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl3352, zip_derived_cl43])).
% 25.72/4.30 thf(zip_derived_cl23, plain,
% 25.72/4.30 (![X0 : $i]: ( (epsilon_transitive @ X0) | ~ (ordinal @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [cc1_ordinal1])).
% 25.72/4.30 thf(zip_derived_cl3585, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (epsilon_transitive @
% 25.72/4.30 (sk__10 @ X0 @ (sk__2 @ (sk__15 @ sk__1 @ X0)))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl3577, zip_derived_cl23])).
% 25.72/4.30 thf(zip_derived_cl3656, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('sup+', [status(thm)], [zip_derived_cl3576, zip_derived_cl3585])).
% 25.72/4.30 thf(zip_derived_cl3689, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl3656])).
% 25.72/4.30 thf(zip_derived_cl7, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (ordinal @ X0)
% 25.72/4.30 | ~ (epsilon_connected @ X0)
% 25.72/4.30 | ~ (epsilon_transitive @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [cc2_ordinal1])).
% 25.72/4.30 thf(zip_derived_cl1, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i]:
% 25.72/4.30 (~ (ordinal @ X0)
% 25.72/4.30 | ((sk__2 @ X1) != (X0))
% 25.72/4.30 | ~ (in @ X0 @ sk_)
% 25.72/4.30 | ~ (in @ (sk__2 @ X1) @ (succ @ sk__1))
% 25.72/4.30 | ~ (in @ (sk__2 @ X1) @ X1))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_0])).
% 25.72/4.30 thf(zip_derived_cl66, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (in @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ~ (in @ (sk__2 @ X0) @ (succ @ sk__1))
% 25.72/4.30 | ~ (in @ (sk__2 @ X0) @ sk_)
% 25.72/4.30 | ~ (ordinal @ (sk__2 @ X0)))),
% 25.72/4.30 inference('eq_res', [status(thm)], [zip_derived_cl1])).
% 25.72/4.30 thf(zip_derived_cl78, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.30 | ~ (in @ (sk__2 @ X0) @ sk_)
% 25.72/4.30 | ~ (in @ (sk__2 @ X0) @ (succ @ sk__1))
% 25.72/4.30 | ~ (in @ (sk__2 @ X0) @ X0))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl7, zip_derived_cl66])).
% 25.72/4.30 thf(zip_derived_cl3694, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (succ @ sk__1))
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk_)
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl3689, zip_derived_cl78])).
% 25.72/4.30 thf(zip_derived_cl3986, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk_)
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (succ @ sk__1))
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl3975, zip_derived_cl3694])).
% 25.72/4.30 thf(zip_derived_cl3991, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (succ @ sk__1))
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ sk_)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl3986])).
% 25.72/4.30 thf(zip_derived_cl4021, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (succ @ sk__1))
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl296, zip_derived_cl3991])).
% 25.72/4.30 thf(zip_derived_cl3975, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl3942])).
% 25.72/4.30 thf(zip_derived_cl4835, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (succ @ sk__1))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0)))),
% 25.72/4.30 inference('clc', [status(thm)], [zip_derived_cl4021, zip_derived_cl3975])).
% 25.72/4.30 thf(zip_derived_cl3689, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl3656])).
% 25.72/4.30 thf(zip_derived_cl4836, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (succ @ sk__1))
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0)))),
% 25.72/4.30 inference('clc', [status(thm)], [zip_derived_cl4835, zip_derived_cl3689])).
% 25.72/4.30 thf(zip_derived_cl4848, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl560, zip_derived_cl4836])).
% 25.72/4.30 thf(zip_derived_cl4862, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl4848])).
% 25.72/4.30 thf(zip_derived_cl3975, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl3942])).
% 25.72/4.30 thf(zip_derived_cl4902, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0))),
% 25.72/4.30 inference('clc', [status(thm)], [zip_derived_cl4862, zip_derived_cl3975])).
% 25.72/4.30 thf(zip_derived_cl3689, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl3656])).
% 25.72/4.30 thf(zip_derived_cl4903, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0)))),
% 25.72/4.30 inference('clc', [status(thm)], [zip_derived_cl4902, zip_derived_cl3689])).
% 25.72/4.30 thf(zip_derived_cl4912, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (zip_tseitin_6 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__15 @ sk__1 @ X0) @ sk__1 @ sk_)
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl561, zip_derived_cl4903])).
% 25.72/4.30 thf(zip_derived_cl4918, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | ~ (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | ~ (zip_tseitin_6 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__15 @ sk__1 @ X0) @ sk__1 @ sk_))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl4912])).
% 25.72/4.30 thf(zip_derived_cl3975, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl3942])).
% 25.72/4.30 thf(zip_derived_cl4923, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (zip_tseitin_6 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__15 @ sk__1 @ X0) @ sk__1 @ sk_)
% 25.72/4.30 | ~ (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0)))
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0))),
% 25.72/4.30 inference('clc', [status(thm)], [zip_derived_cl4918, zip_derived_cl3975])).
% 25.72/4.30 thf(zip_derived_cl3689, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ X0))))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl3656])).
% 25.72/4.30 thf(zip_derived_cl4924, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ X0)) @ (sk__15 @ sk__1 @ X0))
% 25.72/4.30 | ~ (zip_tseitin_6 @ (sk__2 @ (sk__15 @ sk__1 @ X0)) @
% 25.72/4.30 (sk__15 @ sk__1 @ X0) @ sk__1 @ sk_))),
% 25.72/4.30 inference('clc', [status(thm)], [zip_derived_cl4923, zip_derived_cl3689])).
% 25.72/4.30 thf(zip_derived_cl4925, plain,
% 25.72/4.30 ((~ (epsilon_connected @ sk__1)
% 25.72/4.30 | ~ (epsilon_transitive @ sk__1)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl238, zip_derived_cl4924])).
% 25.72/4.30 thf(zip_derived_cl0, plain, ( (ordinal @ sk__1)),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_0])).
% 25.72/4.30 thf(zip_derived_cl24, plain,
% 25.72/4.30 (![X0 : $i]: ( (epsilon_connected @ X0) | ~ (ordinal @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [cc1_ordinal1])).
% 25.72/4.30 thf(zip_derived_cl55, plain, ( (epsilon_connected @ sk__1)),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl0, zip_derived_cl24])).
% 25.72/4.30 thf(zip_derived_cl0, plain, ( (ordinal @ sk__1)),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_0])).
% 25.72/4.30 thf(zip_derived_cl23, plain,
% 25.72/4.30 (![X0 : $i]: ( (epsilon_transitive @ X0) | ~ (ordinal @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [cc1_ordinal1])).
% 25.72/4.30 thf(zip_derived_cl54, plain, ( (epsilon_transitive @ sk__1)),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl0, zip_derived_cl23])).
% 25.72/4.30 thf(zip_derived_cl4928, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_))),
% 25.72/4.30 inference('demod', [status(thm)],
% 25.72/4.30 [zip_derived_cl4925, zip_derived_cl55, zip_derived_cl54])).
% 25.72/4.30 thf(zip_derived_cl4929, plain,
% 25.72/4.30 (( (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl4928])).
% 25.72/4.30 thf(zip_derived_cl41, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 ( (in @ X0 @ X1) | ~ (zip_tseitin_4 @ X0 @ X2 @ X1))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.30 thf(zip_derived_cl4943, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl4929, zip_derived_cl41])).
% 25.72/4.30 thf(zip_derived_cl177, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | (zip_tseitin_6 @ X2 @ (sk__15 @ X1 @ X0) @ X1 @ X0)
% 25.72/4.30 | ~ (ordinal @ X1))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl40, zip_derived_cl51])).
% 25.72/4.30 thf(zip_derived_cl50, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 (~ (in @ X0 @ X1)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__11 @ X2 @ X3 @ X0) @ X0 @ X3 @ X2)
% 25.72/4.30 | ~ (zip_tseitin_6 @ X0 @ X1 @ X3 @ X2))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_3])).
% 25.72/4.30 thf(zip_derived_cl237, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 (~ (ordinal @ X1)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @
% 25.72/4.30 X0)
% 25.72/4.30 | (zip_tseitin_5 @ (sk__11 @ X0 @ X1 @ X2) @ X2 @ X1 @ X0)
% 25.72/4.30 | ~ (in @ X2 @ (sk__15 @ X1 @ X0)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl177, zip_derived_cl50])).
% 25.72/4.30 thf(zip_derived_cl4976, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (zip_tseitin_5 @
% 25.72/4.30 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | ~ (ordinal @ sk__1))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl4943, zip_derived_cl237])).
% 25.72/4.30 thf(zip_derived_cl0, plain, ( (ordinal @ sk__1)),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_0])).
% 25.72/4.30 thf(zip_derived_cl4981, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (zip_tseitin_5 @
% 25.72/4.30 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_))),
% 25.72/4.30 inference('demod', [status(thm)], [zip_derived_cl4976, zip_derived_cl0])).
% 25.72/4.30 thf(zip_derived_cl4982, plain,
% 25.72/4.30 (( (zip_tseitin_5 @
% 25.72/4.30 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl4981])).
% 25.72/4.30 thf(zip_derived_cl45, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 ( (zip_tseitin_4 @ (sk__10 @ X0 @ X1) @ X1 @ X0)
% 25.72/4.30 | ~ (zip_tseitin_5 @ X2 @ X1 @ X3 @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.30 thf(zip_derived_cl5033, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (zip_tseitin_4 @
% 25.72/4.30 (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl4982, zip_derived_cl45])).
% 25.72/4.30 thf(zip_derived_cl42, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 (((X1) = (X0)) | ~ (zip_tseitin_4 @ X0 @ X1 @ X2))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.30 thf(zip_derived_cl5183, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | ((sk__2 @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.30 = (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl5033, zip_derived_cl42])).
% 25.72/4.30 thf(zip_derived_cl5033, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (zip_tseitin_4 @
% 25.72/4.30 (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl4982, zip_derived_cl45])).
% 25.72/4.30 thf(zip_derived_cl41, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 ( (in @ X0 @ X1) | ~ (zip_tseitin_4 @ X0 @ X2 @ X1))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.30 thf(zip_derived_cl5182, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (in @ (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @ sk_))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl5033, zip_derived_cl41])).
% 25.72/4.30 thf(zip_derived_cl5257, plain,
% 25.72/4.30 (( (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_))),
% 25.72/4.30 inference('sup+', [status(thm)], [zip_derived_cl5183, zip_derived_cl5182])).
% 25.72/4.30 thf(zip_derived_cl5275, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl5257])).
% 25.72/4.30 thf(zip_derived_cl4929, plain,
% 25.72/4.30 (( (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl4928])).
% 25.72/4.30 thf(zip_derived_cl43, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 ( (ordinal @ X0) | ~ (zip_tseitin_4 @ X0 @ X1 @ X2))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.30 thf(zip_derived_cl4945, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (ordinal @ (sk__2 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl4929, zip_derived_cl43])).
% 25.72/4.30 thf(zip_derived_cl66, plain,
% 25.72/4.30 (![X0 : $i]:
% 25.72/4.30 (~ (in @ (sk__2 @ X0) @ X0)
% 25.72/4.30 | ~ (in @ (sk__2 @ X0) @ (succ @ sk__1))
% 25.72/4.30 | ~ (in @ (sk__2 @ X0) @ sk_)
% 25.72/4.30 | ~ (ordinal @ (sk__2 @ X0)))),
% 25.72/4.30 inference('eq_res', [status(thm)], [zip_derived_cl1])).
% 25.72/4.30 thf(zip_derived_cl4954, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_)
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (succ @ sk__1))
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl4945, zip_derived_cl66])).
% 25.72/4.30 thf(zip_derived_cl4943, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl4929, zip_derived_cl41])).
% 25.72/4.30 thf(zip_derived_cl5006, plain,
% 25.72/4.30 ((~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (succ @ sk__1))
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_))),
% 25.72/4.30 inference('clc', [status(thm)], [zip_derived_cl4954, zip_derived_cl4943])).
% 25.72/4.30 thf(zip_derived_cl5296, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (succ @ sk__1)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl5275, zip_derived_cl5006])).
% 25.72/4.30 thf(zip_derived_cl5300, plain,
% 25.72/4.30 ((~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (succ @ sk__1))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl5296])).
% 25.72/4.30 thf(zip_derived_cl4982, plain,
% 25.72/4.30 (( (zip_tseitin_5 @
% 25.72/4.30 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl4981])).
% 25.72/4.30 thf(zip_derived_cl46, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 (((X1) = (X0)) | ~ (zip_tseitin_5 @ X1 @ X0 @ X2 @ X3))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.30 thf(zip_derived_cl5034, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | ((sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.30 = (sk__2 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl4982, zip_derived_cl46])).
% 25.72/4.30 thf(zip_derived_cl4982, plain,
% 25.72/4.30 (( (zip_tseitin_5 @
% 25.72/4.30 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.30 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl4981])).
% 25.72/4.30 thf(zip_derived_cl47, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 ( (in @ X0 @ (succ @ X1)) | ~ (zip_tseitin_5 @ X0 @ X2 @ X1 @ X3))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.30 thf(zip_derived_cl5035, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (in @ (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.30 (succ @ sk__1)))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl4982, zip_derived_cl47])).
% 25.72/4.30 thf(zip_derived_cl5070, plain,
% 25.72/4.30 (( (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (succ @ sk__1))
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_))),
% 25.72/4.30 inference('sup+', [status(thm)], [zip_derived_cl5034, zip_derived_cl5035])).
% 25.72/4.30 thf(zip_derived_cl5074, plain,
% 25.72/4.30 (( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 sk_)
% 25.72/4.30 | (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (succ @ sk__1)))),
% 25.72/4.30 inference('simplify', [status(thm)], [zip_derived_cl5070])).
% 25.72/4.30 thf(zip_derived_cl5304, plain,
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @ sk_)),
% 25.72/4.30 inference('clc', [status(thm)], [zip_derived_cl5300, zip_derived_cl5074])).
% 25.72/4.30 thf(zip_derived_cl35, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 (((X1) = (X0)) | ~ (zip_tseitin_2 @ X2 @ X0 @ X1 @ X3))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_10])).
% 25.72/4.30 thf(zip_derived_cl5305, plain, (((sk__12 @ sk_) = (sk__13 @ sk_))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl5304, zip_derived_cl35])).
% 25.72/4.30 thf(zip_derived_cl51, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.30 (~ (zip_tseitin_3 @ (sk__14 @ X0) @ (sk__13 @ X0) @ (sk__12 @ X0) @ X0)
% 25.72/4.30 | ~ (ordinal @ X1)
% 25.72/4.30 | (zip_tseitin_6 @ X2 @ (sk__15 @ X1 @ X0) @ X1 @ X0))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_15])).
% 25.72/4.30 thf(zip_derived_cl5310, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i]:
% 25.72/4.30 (~ (zip_tseitin_3 @ (sk__14 @ sk_) @ (sk__12 @ sk_) @
% 25.72/4.30 (sk__12 @ sk_) @ sk_)
% 25.72/4.30 | (zip_tseitin_6 @ X1 @ (sk__15 @ X0 @ sk_) @ X0 @ sk_)
% 25.72/4.30 | ~ (ordinal @ X0))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl5305, zip_derived_cl51])).
% 25.72/4.30 thf(zip_derived_cl5304, plain,
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__13 @ sk_) @ (sk__12 @ sk_) @ sk_)),
% 25.72/4.30 inference('clc', [status(thm)], [zip_derived_cl5300, zip_derived_cl5074])).
% 25.72/4.30 thf(zip_derived_cl5305, plain, (((sk__12 @ sk_) = (sk__13 @ sk_))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl5304, zip_derived_cl35])).
% 25.72/4.30 thf(zip_derived_cl5309, plain,
% 25.72/4.30 ( (zip_tseitin_2 @ (sk__14 @ sk_) @ (sk__12 @ sk_) @ (sk__12 @ sk_) @ sk_)),
% 25.72/4.30 inference('demod', [status(thm)],
% 25.72/4.30 [zip_derived_cl5304, zip_derived_cl5305])).
% 25.72/4.30 thf(zip_derived_cl37, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 (((X1) = (X0)) | ~ (zip_tseitin_2 @ X0 @ X2 @ X1 @ X3))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_10])).
% 25.72/4.30 thf(zip_derived_cl5313, plain, (((sk__12 @ sk_) = (sk__14 @ sk_))),
% 25.72/4.30 inference('sup-', [status(thm)], [zip_derived_cl5309, zip_derived_cl37])).
% 25.72/4.30 thf(zip_derived_cl39, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.30 ( (zip_tseitin_3 @ X0 @ X1 @ X2 @ X3) | ((X1) != (X0)))),
% 25.72/4.30 inference('cnf', [status(esa)], [zf_stmt_1])).
% 25.72/4.30 thf(zip_derived_cl75, plain,
% 25.72/4.30 (![X0 : $i, X1 : $i, X2 : $i]: (zip_tseitin_3 @ X2 @ X2 @ X1 @ X0)),
% 25.72/4.31 inference('eq_res', [status(thm)], [zip_derived_cl39])).
% 25.72/4.31 thf(zip_derived_cl5339, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i]:
% 25.72/4.31 ( (zip_tseitin_6 @ X1 @ (sk__15 @ X0 @ sk_) @ X0 @ sk_)
% 25.72/4.31 | ~ (ordinal @ X0))),
% 25.72/4.31 inference('demod', [status(thm)],
% 25.72/4.31 [zip_derived_cl5310, zip_derived_cl5313, zip_derived_cl75])).
% 25.72/4.31 thf(zip_derived_cl0, plain, ( (ordinal @ sk__1)),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_0])).
% 25.72/4.31 thf(zip_derived_cl5344, plain,
% 25.72/4.31 (![X0 : $i]: (zip_tseitin_6 @ X0 @ (sk__15 @ sk__1 @ sk_) @ sk__1 @ sk_)),
% 25.72/4.31 inference('sup+', [status(thm)], [zip_derived_cl5339, zip_derived_cl0])).
% 25.72/4.31 thf(zip_derived_cl50, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.31 (~ (in @ X0 @ X1)
% 25.72/4.31 | (zip_tseitin_5 @ (sk__11 @ X2 @ X3 @ X0) @ X0 @ X3 @ X2)
% 25.72/4.31 | ~ (zip_tseitin_6 @ X0 @ X1 @ X3 @ X2))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_3])).
% 25.72/4.31 thf(zip_derived_cl5504, plain,
% 25.72/4.31 (![X0 : $i]:
% 25.72/4.31 ( (zip_tseitin_5 @ (sk__11 @ sk_ @ sk__1 @ X0) @ X0 @ sk__1 @ sk_)
% 25.72/4.31 | ~ (in @ X0 @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl5344, zip_derived_cl50])).
% 25.72/4.31 thf(zip_derived_cl5522, plain,
% 25.72/4.31 ((((sk__2 @ (sk__15 @ sk__1 @ sk_)) = (sk__3 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_5 @
% 25.72/4.31 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl4, zip_derived_cl5504])).
% 25.72/4.31 thf(zip_derived_cl46, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.31 (((X1) = (X0)) | ~ (zip_tseitin_5 @ X1 @ X0 @ X2 @ X3))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.31 thf(zip_derived_cl5846, plain,
% 25.72/4.31 ((((sk__2 @ (sk__15 @ sk__1 @ sk_)) = (sk__3 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | ((sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 = (sk__2 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl5522, zip_derived_cl46])).
% 25.72/4.31 thf(zip_derived_cl5522, plain,
% 25.72/4.31 ((((sk__2 @ (sk__15 @ sk__1 @ sk_)) = (sk__3 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_5 @
% 25.72/4.31 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl4, zip_derived_cl5504])).
% 25.72/4.31 thf(zip_derived_cl5865, plain,
% 25.72/4.31 (( (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.31 | ((sk__2 @ (sk__15 @ sk__1 @ sk_)) = (sk__3 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | ((sk__2 @ (sk__15 @ sk__1 @ sk_)) = (sk__3 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('sup+', [status(thm)], [zip_derived_cl5846, zip_derived_cl5522])).
% 25.72/4.31 thf(zip_derived_cl5878, plain,
% 25.72/4.31 ((((sk__2 @ (sk__15 @ sk__1 @ sk_)) = (sk__3 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl5865])).
% 25.72/4.31 thf(zip_derived_cl3, plain,
% 25.72/4.31 (![X1 : $i]: ( (ordinal @ (sk__3 @ X1)) | (in @ (sk__2 @ X1) @ X1))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_0])).
% 25.72/4.31 thf(zip_derived_cl5504, plain,
% 25.72/4.31 (![X0 : $i]:
% 25.72/4.31 ( (zip_tseitin_5 @ (sk__11 @ sk_ @ sk__1 @ X0) @ X0 @ sk__1 @ sk_)
% 25.72/4.31 | ~ (in @ X0 @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl5344, zip_derived_cl50])).
% 25.72/4.31 thf(zip_derived_cl5521, plain,
% 25.72/4.31 (( (ordinal @ (sk__3 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_5 @
% 25.72/4.31 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl3, zip_derived_cl5504])).
% 25.72/4.31 thf(zip_derived_cl23, plain,
% 25.72/4.31 (![X0 : $i]: ( (epsilon_transitive @ X0) | ~ (ordinal @ X0))),
% 25.72/4.31 inference('cnf', [status(esa)], [cc1_ordinal1])).
% 25.72/4.31 thf(zip_derived_cl5770, plain,
% 25.72/4.31 (( (zip_tseitin_5 @
% 25.72/4.31 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.31 | (epsilon_transitive @ (sk__3 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl5521, zip_derived_cl23])).
% 25.72/4.31 thf(zip_derived_cl46, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.31 (((X1) = (X0)) | ~ (zip_tseitin_5 @ X1 @ X0 @ X2 @ X3))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.31 thf(zip_derived_cl5972, plain,
% 25.72/4.31 (( (epsilon_transitive @ (sk__3 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | ((sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 = (sk__2 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl5770, zip_derived_cl46])).
% 25.72/4.31 thf(zip_derived_cl5770, plain,
% 25.72/4.31 (( (zip_tseitin_5 @
% 25.72/4.31 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.31 | (epsilon_transitive @ (sk__3 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl5521, zip_derived_cl23])).
% 25.72/4.31 thf(zip_derived_cl5993, plain,
% 25.72/4.31 (( (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.31 | (epsilon_transitive @ (sk__3 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (epsilon_transitive @ (sk__3 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('sup+', [status(thm)], [zip_derived_cl5972, zip_derived_cl5770])).
% 25.72/4.31 thf(zip_derived_cl6008, plain,
% 25.72/4.31 (( (epsilon_transitive @ (sk__3 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl5993])).
% 25.72/4.31 thf(zip_derived_cl6014, plain,
% 25.72/4.31 (( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.31 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_))),
% 25.72/4.31 inference('sup+', [status(thm)], [zip_derived_cl5878, zip_derived_cl6008])).
% 25.72/4.31 thf(zip_derived_cl6019, plain,
% 25.72/4.31 (( (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.31 | (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl6014])).
% 25.72/4.31 thf(zip_derived_cl45, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.31 ( (zip_tseitin_4 @ (sk__10 @ X0 @ X1) @ X1 @ X0)
% 25.72/4.31 | ~ (zip_tseitin_5 @ X2 @ X1 @ X3 @ X0))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.31 thf(zip_derived_cl6493, plain,
% 25.72/4.31 (( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_4 @
% 25.72/4.31 (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl6019, zip_derived_cl45])).
% 25.72/4.31 thf(zip_derived_cl42, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.31 (((X1) = (X0)) | ~ (zip_tseitin_4 @ X0 @ X1 @ X2))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.31 thf(zip_derived_cl6605, plain,
% 25.72/4.31 (( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | ((sk__2 @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 = (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl6493, zip_derived_cl42])).
% 25.72/4.31 thf(zip_derived_cl6493, plain,
% 25.72/4.31 (( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_4 @
% 25.72/4.31 (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl6019, zip_derived_cl45])).
% 25.72/4.31 thf(zip_derived_cl43, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.31 ( (ordinal @ X0) | ~ (zip_tseitin_4 @ X0 @ X1 @ X2))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.31 thf(zip_derived_cl6606, plain,
% 25.72/4.31 (( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (ordinal @ (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl6493, zip_derived_cl43])).
% 25.72/4.31 thf(zip_derived_cl23, plain,
% 25.72/4.31 (![X0 : $i]: ( (epsilon_transitive @ X0) | ~ (ordinal @ X0))),
% 25.72/4.31 inference('cnf', [status(esa)], [cc1_ordinal1])).
% 25.72/4.31 thf(zip_derived_cl6618, plain,
% 25.72/4.31 (( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (epsilon_transitive @
% 25.72/4.31 (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl6606, zip_derived_cl23])).
% 25.72/4.31 thf(zip_derived_cl6701, plain,
% 25.72/4.31 (( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('sup+', [status(thm)], [zip_derived_cl6605, zip_derived_cl6618])).
% 25.72/4.31 thf(zip_derived_cl6727, plain,
% 25.72/4.31 ( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl6701])).
% 25.72/4.31 thf(zip_derived_cl78, plain,
% 25.72/4.31 (![X0 : $i]:
% 25.72/4.31 (~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.31 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.31 | ~ (in @ (sk__2 @ X0) @ sk_)
% 25.72/4.31 | ~ (in @ (sk__2 @ X0) @ (succ @ sk__1))
% 25.72/4.31 | ~ (in @ (sk__2 @ X0) @ X0))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl7, zip_derived_cl66])).
% 25.72/4.31 thf(zip_derived_cl6731, plain,
% 25.72/4.31 ((~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (succ @ sk__1))
% 25.72/4.31 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_)
% 25.72/4.31 | ~ (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl6727, zip_derived_cl78])).
% 25.72/4.31 thf(zip_derived_cl5878, plain,
% 25.72/4.31 ((((sk__2 @ (sk__15 @ sk__1 @ sk_)) = (sk__3 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl5865])).
% 25.72/4.31 thf(zip_derived_cl5521, plain,
% 25.72/4.31 (( (ordinal @ (sk__3 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_5 @
% 25.72/4.31 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl3, zip_derived_cl5504])).
% 25.72/4.31 thf(zip_derived_cl24, plain,
% 25.72/4.31 (![X0 : $i]: ( (epsilon_connected @ X0) | ~ (ordinal @ X0))),
% 25.72/4.31 inference('cnf', [status(esa)], [cc1_ordinal1])).
% 25.72/4.31 thf(zip_derived_cl5771, plain,
% 25.72/4.31 (( (zip_tseitin_5 @
% 25.72/4.31 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.31 | (epsilon_connected @ (sk__3 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl5521, zip_derived_cl24])).
% 25.72/4.31 thf(zip_derived_cl46, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.31 (((X1) = (X0)) | ~ (zip_tseitin_5 @ X1 @ X0 @ X2 @ X3))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.31 thf(zip_derived_cl6774, plain,
% 25.72/4.31 (( (epsilon_connected @ (sk__3 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | ((sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 = (sk__2 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl5771, zip_derived_cl46])).
% 25.72/4.31 thf(zip_derived_cl5771, plain,
% 25.72/4.31 (( (zip_tseitin_5 @
% 25.72/4.31 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.31 | (epsilon_connected @ (sk__3 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl5521, zip_derived_cl24])).
% 25.72/4.31 thf(zip_derived_cl6811, plain,
% 25.72/4.31 (( (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.31 | (epsilon_connected @ (sk__3 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (epsilon_connected @ (sk__3 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('sup+', [status(thm)], [zip_derived_cl6774, zip_derived_cl5771])).
% 25.72/4.31 thf(zip_derived_cl6830, plain,
% 25.72/4.31 (( (epsilon_connected @ (sk__3 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl6811])).
% 25.72/4.31 thf(zip_derived_cl6840, plain,
% 25.72/4.31 (( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.31 | (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_))),
% 25.72/4.31 inference('sup+', [status(thm)], [zip_derived_cl5878, zip_derived_cl6830])).
% 25.72/4.31 thf(zip_derived_cl6846, plain,
% 25.72/4.31 (( (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)
% 25.72/4.31 | (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl6840])).
% 25.72/4.31 thf(zip_derived_cl45, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.31 ( (zip_tseitin_4 @ (sk__10 @ X0 @ X1) @ X1 @ X0)
% 25.72/4.31 | ~ (zip_tseitin_5 @ X2 @ X1 @ X3 @ X0))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.31 thf(zip_derived_cl7322, plain,
% 25.72/4.31 (( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_4 @
% 25.72/4.31 (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl6846, zip_derived_cl45])).
% 25.72/4.31 thf(zip_derived_cl42, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.31 (((X1) = (X0)) | ~ (zip_tseitin_4 @ X0 @ X1 @ X2))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.31 thf(zip_derived_cl7383, plain,
% 25.72/4.31 (( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | ((sk__2 @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 = (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl7322, zip_derived_cl42])).
% 25.72/4.31 thf(zip_derived_cl7322, plain,
% 25.72/4.31 (( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_4 @
% 25.72/4.31 (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl6846, zip_derived_cl45])).
% 25.72/4.31 thf(zip_derived_cl43, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.31 ( (ordinal @ X0) | ~ (zip_tseitin_4 @ X0 @ X1 @ X2))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.31 thf(zip_derived_cl7384, plain,
% 25.72/4.31 (( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (ordinal @ (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl7322, zip_derived_cl43])).
% 25.72/4.31 thf(zip_derived_cl24, plain,
% 25.72/4.31 (![X0 : $i]: ( (epsilon_connected @ X0) | ~ (ordinal @ X0))),
% 25.72/4.31 inference('cnf', [status(esa)], [cc1_ordinal1])).
% 25.72/4.31 thf(zip_derived_cl7402, plain,
% 25.72/4.31 (( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (epsilon_connected @
% 25.72/4.31 (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl7384, zip_derived_cl24])).
% 25.72/4.31 thf(zip_derived_cl7482, plain,
% 25.72/4.31 (( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('sup+', [status(thm)], [zip_derived_cl7383, zip_derived_cl7402])).
% 25.72/4.31 thf(zip_derived_cl7524, plain,
% 25.72/4.31 ( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl7482])).
% 25.72/4.31 thf(zip_derived_cl7526, plain,
% 25.72/4.31 ((~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (succ @ sk__1))
% 25.72/4.31 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_))),
% 25.72/4.31 inference('demod', [status(thm)],
% 25.72/4.31 [zip_derived_cl6731, zip_derived_cl7524])).
% 25.72/4.31 thf(zip_derived_cl561, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i]:
% 25.72/4.31 ( (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.31 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.31 | ~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.31 | ~ (zip_tseitin_6 @ (sk__2 @ X0) @ X1 @ sk__1 @ sk_)
% 25.72/4.31 | (in @ (sk__2 @ X0) @ X1))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl552, zip_derived_cl49])).
% 25.72/4.31 thf(zip_derived_cl560, plain,
% 25.72/4.31 (![X0 : $i]:
% 25.72/4.31 ( (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.31 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.31 | ~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.31 | (in @ (sk__2 @ X0) @ (succ @ sk__1)))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl552, zip_derived_cl47])).
% 25.72/4.31 thf(zip_derived_cl296, plain,
% 25.72/4.31 (![X0 : $i]:
% 25.72/4.31 (~ (epsilon_transitive @ (sk__2 @ X0))
% 25.72/4.31 | ~ (epsilon_connected @ (sk__2 @ X0))
% 25.72/4.31 | (zip_tseitin_4 @ (sk__2 @ X0) @ (sk__2 @ X0) @ X0)
% 25.72/4.31 | (in @ (sk__2 @ X0) @ sk_))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl294])).
% 25.72/4.31 thf(zip_derived_cl7526, plain,
% 25.72/4.31 ((~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (succ @ sk__1))
% 25.72/4.31 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_))),
% 25.72/4.31 inference('demod', [status(thm)],
% 25.72/4.31 [zip_derived_cl6731, zip_derived_cl7524])).
% 25.72/4.31 thf(zip_derived_cl7594, plain,
% 25.72/4.31 (( (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 | ~ (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | ~ (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (succ @ sk__1))
% 25.72/4.31 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl296, zip_derived_cl7526])).
% 25.72/4.31 thf(zip_derived_cl7524, plain,
% 25.72/4.31 ( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl7482])).
% 25.72/4.31 thf(zip_derived_cl6727, plain,
% 25.72/4.31 ( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl6701])).
% 25.72/4.31 thf(zip_derived_cl7605, plain,
% 25.72/4.31 (( (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (succ @ sk__1))
% 25.72/4.31 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('demod', [status(thm)],
% 25.72/4.31 [zip_derived_cl7594, zip_derived_cl7524, zip_derived_cl6727])).
% 25.72/4.31 thf(zip_derived_cl7775, plain,
% 25.72/4.31 ((~ (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | ~ (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl560, zip_derived_cl7605])).
% 25.72/4.31 thf(zip_derived_cl6727, plain,
% 25.72/4.31 ( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl6701])).
% 25.72/4.31 thf(zip_derived_cl7524, plain,
% 25.72/4.31 ( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl7482])).
% 25.72/4.31 thf(zip_derived_cl7790, plain,
% 25.72/4.31 (( (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('demod', [status(thm)],
% 25.72/4.31 [zip_derived_cl7775, zip_derived_cl6727, zip_derived_cl7524])).
% 25.72/4.31 thf(zip_derived_cl7791, plain,
% 25.72/4.31 ((~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl7790])).
% 25.72/4.31 thf(zip_derived_cl7805, plain,
% 25.72/4.31 ((~ (zip_tseitin_6 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__15 @ sk__1 @ sk_) @ sk__1 @ sk_)
% 25.72/4.31 | ~ (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | ~ (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl561, zip_derived_cl7791])).
% 25.72/4.31 thf(zip_derived_cl5344, plain,
% 25.72/4.31 (![X0 : $i]: (zip_tseitin_6 @ X0 @ (sk__15 @ sk__1 @ sk_) @ sk__1 @ sk_)),
% 25.72/4.31 inference('sup+', [status(thm)], [zip_derived_cl5339, zip_derived_cl0])).
% 25.72/4.31 thf(zip_derived_cl6727, plain,
% 25.72/4.31 ( (epsilon_transitive @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl6701])).
% 25.72/4.31 thf(zip_derived_cl7524, plain,
% 25.72/4.31 ( (epsilon_connected @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl7482])).
% 25.72/4.31 thf(zip_derived_cl7816, plain,
% 25.72/4.31 (( (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 | (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('demod', [status(thm)],
% 25.72/4.31 [zip_derived_cl7805, zip_derived_cl5344, zip_derived_cl6727,
% 25.72/4.31 zip_derived_cl7524])).
% 25.72/4.31 thf(zip_derived_cl7817, plain,
% 25.72/4.31 ( (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))),
% 25.72/4.31 inference('simplify', [status(thm)], [zip_derived_cl7816])).
% 25.72/4.31 thf(zip_derived_cl41, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.31 ( (in @ X0 @ X1) | ~ (zip_tseitin_4 @ X0 @ X2 @ X1))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.31 thf(zip_derived_cl7825, plain,
% 25.72/4.31 ( (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl7817, zip_derived_cl41])).
% 25.72/4.31 thf(zip_derived_cl7875, plain,
% 25.72/4.31 ((~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (succ @ sk__1))
% 25.72/4.31 | ~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_))),
% 25.72/4.31 inference('demod', [status(thm)],
% 25.72/4.31 [zip_derived_cl7526, zip_derived_cl7825])).
% 25.72/4.31 thf(zip_derived_cl7825, plain,
% 25.72/4.31 ( (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (sk__15 @ sk__1 @ sk_))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl7817, zip_derived_cl41])).
% 25.72/4.31 thf(zip_derived_cl5504, plain,
% 25.72/4.31 (![X0 : $i]:
% 25.72/4.31 ( (zip_tseitin_5 @ (sk__11 @ sk_ @ sk__1 @ X0) @ X0 @ sk__1 @ sk_)
% 25.72/4.31 | ~ (in @ X0 @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl5344, zip_derived_cl50])).
% 25.72/4.31 thf(zip_derived_cl7885, plain,
% 25.72/4.31 ( (zip_tseitin_5 @
% 25.72/4.31 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl7825, zip_derived_cl5504])).
% 25.72/4.31 thf(zip_derived_cl7885, plain,
% 25.72/4.31 ( (zip_tseitin_5 @
% 25.72/4.31 (sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl7825, zip_derived_cl5504])).
% 25.72/4.31 thf(zip_derived_cl46, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.31 (((X1) = (X0)) | ~ (zip_tseitin_5 @ X1 @ X0 @ X2 @ X3))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.31 thf(zip_derived_cl8070, plain,
% 25.72/4.31 (((sk__11 @ sk_ @ sk__1 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)))
% 25.72/4.31 = (sk__2 @ (sk__15 @ sk__1 @ sk_)))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl7885, zip_derived_cl46])).
% 25.72/4.31 thf(zip_derived_cl8081, plain,
% 25.72/4.31 ( (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)),
% 25.72/4.31 inference('demod', [status(thm)],
% 25.72/4.31 [zip_derived_cl7885, zip_derived_cl8070])).
% 25.72/4.31 thf(zip_derived_cl47, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.31 ( (in @ X0 @ (succ @ X1)) | ~ (zip_tseitin_5 @ X0 @ X2 @ X1 @ X3))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.31 thf(zip_derived_cl8108, plain,
% 25.72/4.31 ( (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ (succ @ sk__1))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl8081, zip_derived_cl47])).
% 25.72/4.31 thf(zip_derived_cl8110, plain,
% 25.72/4.31 (~ (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_)),
% 25.72/4.31 inference('demod', [status(thm)],
% 25.72/4.31 [zip_derived_cl7875, zip_derived_cl8108])).
% 25.72/4.31 thf(zip_derived_cl8081, plain,
% 25.72/4.31 ( (zip_tseitin_5 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk__1 @ sk_)),
% 25.72/4.31 inference('demod', [status(thm)],
% 25.72/4.31 [zip_derived_cl7885, zip_derived_cl8070])).
% 25.72/4.31 thf(zip_derived_cl45, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 25.72/4.31 ( (zip_tseitin_4 @ (sk__10 @ X0 @ X1) @ X1 @ X0)
% 25.72/4.31 | ~ (zip_tseitin_5 @ X2 @ X1 @ X3 @ X0))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_5])).
% 25.72/4.31 thf(zip_derived_cl8106, plain,
% 25.72/4.31 ( (zip_tseitin_4 @ (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_)),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl8081, zip_derived_cl45])).
% 25.72/4.31 thf(zip_derived_cl8106, plain,
% 25.72/4.31 ( (zip_tseitin_4 @ (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_))) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_)),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl8081, zip_derived_cl45])).
% 25.72/4.31 thf(zip_derived_cl42, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.31 (((X1) = (X0)) | ~ (zip_tseitin_4 @ X0 @ X1 @ X2))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.31 thf(zip_derived_cl8148, plain,
% 25.72/4.31 (((sk__2 @ (sk__15 @ sk__1 @ sk_))
% 25.72/4.31 = (sk__10 @ sk_ @ (sk__2 @ (sk__15 @ sk__1 @ sk_))))),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl8106, zip_derived_cl42])).
% 25.72/4.31 thf(zip_derived_cl8337, plain,
% 25.72/4.31 ( (zip_tseitin_4 @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @
% 25.72/4.31 (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_)),
% 25.72/4.31 inference('demod', [status(thm)],
% 25.72/4.31 [zip_derived_cl8106, zip_derived_cl8148])).
% 25.72/4.31 thf(zip_derived_cl41, plain,
% 25.72/4.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 25.72/4.31 ( (in @ X0 @ X1) | ~ (zip_tseitin_4 @ X0 @ X2 @ X1))),
% 25.72/4.31 inference('cnf', [status(esa)], [zf_stmt_7])).
% 25.72/4.31 thf(zip_derived_cl8410, plain,
% 25.72/4.31 ( (in @ (sk__2 @ (sk__15 @ sk__1 @ sk_)) @ sk_)),
% 25.72/4.31 inference('sup-', [status(thm)], [zip_derived_cl8337, zip_derived_cl41])).
% 25.72/4.31 thf(zip_derived_cl8423, plain, ($false),
% 25.72/4.31 inference('demod', [status(thm)],
% 25.72/4.31 [zip_derived_cl8110, zip_derived_cl8410])).
% 25.72/4.31
% 25.72/4.31 % SZS output end Refutation
% 25.72/4.31
% 25.72/4.31
% 25.72/4.31 % Terminating...
% 26.39/4.43 % Runner terminated.
% 26.39/4.44 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------