%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEU277+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.AcsP14aqPj true
% Computer : n013.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 13.30s 2.56s
% Output : Refutation 13.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SEU277+1 : TPTP v9.2.0. Released v3.3.0.
% 0.04/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.AcsP14aqPj true
% 0.12/0.33 % Computer : n013.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Oct 1 16:14:38 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.34 % Running portfolio for 300 s
% 0.12/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.34 % Number of cores: 8
% 0.12/0.34 % Python version: Python 3.6.8
% 0.12/0.34 % Running in FO mode
% 0.57/0.66 % Total configuration time : 435
% 0.57/0.66 % Estimated wc time : 1092
% 0.57/0.66 % Estimated cpu time (7 cpus) : 156.0
% 0.59/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.59/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.59/0.78 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.59/0.78 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.59/0.78 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.59/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.59/0.81 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 13.30/2.56 % Solved by fo/fo6_bce.sh.
% 13.30/2.56 % BCE start: 66
% 13.30/2.56 % BCE eliminated: 3
% 13.30/2.56 % PE start: 63
% 13.30/2.56 logic: eq
% 13.30/2.56 % PE eliminated: 17
% 13.30/2.56 % done 918 iterations in 1.767s
% 13.30/2.56 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 13.30/2.56 % SZS output start Refutation
% 13.30/2.56 thf(cartesian_product2_type, type, cartesian_product2: $i > $i > $i).
% 13.30/2.56 thf(sk__21_type, type, sk__21: $i > $i > $i).
% 13.30/2.56 thf(sk__3_type, type, sk__3: $i > $i).
% 13.30/2.56 thf(sk__24_type, type, sk__24: $i > $i > $i > $i).
% 13.30/2.56 thf(sk__4_type, type, sk__4: $i > $i).
% 13.30/2.56 thf(sk__2_type, type, sk__2: $i).
% 13.30/2.56 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $i > $i > $i > $o).
% 13.30/2.56 thf(function_type, type, function: $i > $o).
% 13.30/2.56 thf(relation_type, type, relation: $i > $o).
% 13.30/2.56 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $i > $i > $i > $o).
% 13.30/2.56 thf(zip_tseitin_5_type, type, zip_tseitin_5: $i > $i > $i > $i > $i > $o).
% 13.30/2.56 thf(sk__19_type, type, sk__19: $i > $i > $i > $i).
% 13.30/2.56 thf(sk__type, type, sk_: $i).
% 13.30/2.56 thf(in_type, type, in: $i > $i > $o).
% 13.30/2.56 thf(sk__22_type, type, sk__22: $i > $i > $i).
% 13.30/2.56 thf(sk__1_type, type, sk__1: $i).
% 13.30/2.56 thf(zip_tseitin_6_type, type, zip_tseitin_6: $i > $i > $i > $i > $i > $o).
% 13.30/2.56 thf(sk__20_type, type, sk__20: $i > $i > $i > $i > $i).
% 13.30/2.56 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $i > $i > $i > $o).
% 13.30/2.56 thf(sk__18_type, type, sk__18: $i > $i > $i > $i).
% 13.30/2.56 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $i > $i > $i > $i > $o).
% 13.30/2.56 thf(zip_tseitin_4_type, type, zip_tseitin_4: $i > $i > $i > $i > $i > $o).
% 13.30/2.56 thf(sk__5_type, type, sk__5: $i > $i).
% 13.30/2.56 thf(sk__23_type, type, sk__23: $i > $i > $i).
% 13.30/2.56 thf(apply_type, type, apply: $i > $i > $i).
% 13.30/2.56 thf(ordered_pair_type, type, ordered_pair: $i > $i > $i).
% 13.30/2.56 thf(s1_xboole_0__e6_21__wellord2__1, conjecture,
% 13.30/2.56 (![A:$i,B:$i,C:$i]:
% 13.30/2.56 ( ( ( relation @ B ) & ( relation @ C ) & ( function @ C ) ) =>
% 13.30/2.56 ( ?[D:$i]:
% 13.30/2.56 ( ![E:$i]:
% 13.30/2.56 ( ( in @ E @ D ) <=>
% 13.30/2.56 ( ( in @ E @ ( cartesian_product2 @ A @ A ) ) &
% 13.30/2.56 ( ?[F:$i,G:$i]:
% 13.30/2.56 ( ( in @
% 13.30/2.56 ( ordered_pair @ ( apply @ C @ F ) @ ( apply @ C @ G ) ) @
% 13.30/2.56 B ) &
% 13.30/2.56 ( ( E ) = ( ordered_pair @ F @ G ) ) ) ) ) ) ) ) ))).
% 13.30/2.56 thf(zf_stmt_0, negated_conjecture,
% 13.30/2.56 (~( ![A:$i,B:$i,C:$i]:
% 13.30/2.56 ( ( ( relation @ B ) & ( relation @ C ) & ( function @ C ) ) =>
% 13.30/2.56 ( ?[D:$i]:
% 13.30/2.56 ( ![E:$i]:
% 13.30/2.56 ( ( in @ E @ D ) <=>
% 13.30/2.56 ( ( in @ E @ ( cartesian_product2 @ A @ A ) ) &
% 13.30/2.56 ( ?[F:$i,G:$i]:
% 13.30/2.56 ( ( in @
% 13.30/2.56 ( ordered_pair @ ( apply @ C @ F ) @ ( apply @ C @ G ) ) @
% 13.30/2.56 B ) &
% 13.30/2.56 ( ( E ) = ( ordered_pair @ F @ G ) ) ) ) ) ) ) ) ) )),
% 13.30/2.56 inference('cnf.neg', [status(esa)], [s1_xboole_0__e6_21__wellord2__1])).
% 13.30/2.56 thf(zip_derived_cl2, plain,
% 13.30/2.56 (![X0 : $i]:
% 13.30/2.56 ( (in @
% 13.30/2.56 (ordered_pair @ (apply @ sk__2 @ (sk__4 @ X0)) @
% 13.30/2.56 (apply @ sk__2 @ (sk__5 @ X0))) @
% 13.30/2.56 sk__1)
% 13.30/2.56 | (in @ (sk__3 @ X0) @ X0))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl0, plain,
% 13.30/2.56 (![X0 : $i]:
% 13.30/2.56 ( (in @ (sk__3 @ X0) @ (cartesian_product2 @ sk_ @ sk_))
% 13.30/2.56 | (in @ (sk__3 @ X0) @ X0))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl1, plain,
% 13.30/2.56 (![X0 : $i]:
% 13.30/2.56 (((sk__3 @ X0) = (ordered_pair @ (sk__4 @ X0) @ (sk__5 @ X0)))
% 13.30/2.56 | (in @ (sk__3 @ X0) @ X0))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(s1_tarski__e6_21__wellord2__1, axiom,
% 13.30/2.56 (![A:$i,B:$i,C:$i]:
% 13.30/2.56 ( ( ( function @ C ) & ( relation @ C ) & ( relation @ B ) ) =>
% 13.30/2.56 ( ( ![D:$i,E:$i,F:$i]:
% 13.30/2.56 ( ( ( ?[I:$i,J:$i]:
% 13.30/2.56 ( ( ( F ) = ( ordered_pair @ I @ J ) ) &
% 13.30/2.56 ( in @
% 13.30/2.56 ( ordered_pair @ ( apply @ C @ I ) @ ( apply @ C @ J ) ) @
% 13.30/2.56 B ) ) ) &
% 13.30/2.56 ( ( D ) = ( F ) ) &
% 13.30/2.56 ( ?[G:$i,H:$i]:
% 13.30/2.56 ( ( ( E ) = ( ordered_pair @ G @ H ) ) &
% 13.30/2.56 ( in @
% 13.30/2.56 ( ordered_pair @ ( apply @ C @ G ) @ ( apply @ C @ H ) ) @
% 13.30/2.56 B ) ) ) &
% 13.30/2.56 ( ( D ) = ( E ) ) ) =>
% 13.30/2.56 ( ( E ) = ( F ) ) ) ) =>
% 13.30/2.56 ( ?[D:$i]:
% 13.30/2.56 ( ![E:$i]:
% 13.30/2.56 ( ( in @ E @ D ) <=>
% 13.30/2.56 ( ?[F:$i]:
% 13.30/2.56 ( ( in @ F @ ( cartesian_product2 @ A @ A ) ) &
% 13.30/2.56 ( ( F ) = ( E ) ) &
% 13.30/2.56 ( ?[K:$i,L:$i]:
% 13.30/2.56 ( ( ( E ) = ( ordered_pair @ K @ L ) ) &
% 13.30/2.56 ( in @
% 13.30/2.56 ( ordered_pair @ ( apply @ C @ K ) @ ( apply @ C @ L ) ) @
% 13.30/2.56 B ) ) ) ) ) ) ) ) ) ))).
% 13.30/2.56 thf(zf_stmt_1, axiom,
% 13.30/2.56 (![L:$i,K:$i,E:$i,C:$i,B:$i]:
% 13.30/2.56 ( ( zip_tseitin_4 @ L @ K @ E @ C @ B ) <=>
% 13.30/2.56 ( ( in @ ( ordered_pair @ ( apply @ C @ K ) @ ( apply @ C @ L ) ) @ B ) &
% 13.30/2.56 ( ( E ) = ( ordered_pair @ K @ L ) ) ) ))).
% 13.30/2.56 thf(zip_derived_cl58, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 ( (zip_tseitin_4 @ X0 @ X1 @ X2 @ X3 @ X4)
% 13.30/2.56 | ((X2) != (ordered_pair @ X1 @ X0))
% 13.30/2.56 | ~ (in @ (ordered_pair @ (apply @ X3 @ X1) @ (apply @ X3 @ X0)) @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_1])).
% 13.30/2.56 thf(zf_stmt_2, axiom,
% 13.30/2.56 (![F:$i,E:$i,C:$i,B:$i,A:$i]:
% 13.30/2.56 ( ( zip_tseitin_5 @ F @ E @ C @ B @ A ) <=>
% 13.30/2.56 ( ( ?[K:$i,L:$i]: ( zip_tseitin_4 @ L @ K @ E @ C @ B ) ) &
% 13.30/2.56 ( ( F ) = ( E ) ) & ( in @ F @ ( cartesian_product2 @ A @ A ) ) ) ))).
% 13.30/2.56 thf(zip_derived_cl62, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i]:
% 13.30/2.56 ( (zip_tseitin_5 @ X0 @ X1 @ X2 @ X3 @ X4)
% 13.30/2.56 | ~ (in @ X0 @ (cartesian_product2 @ X4 @ X4))
% 13.30/2.56 | ((X0) != (X1))
% 13.30/2.56 | ~ (zip_tseitin_4 @ X5 @ X6 @ X1 @ X2 @ X3))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_2])).
% 13.30/2.56 thf(zip_derived_cl282, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i]:
% 13.30/2.56 (~ (in @ (ordered_pair @ (apply @ X1 @ X3) @ (apply @ X1 @ X4)) @ X0)
% 13.30/2.56 | ((X2) != (ordered_pair @ X3 @ X4))
% 13.30/2.56 | ((X6) != (X2))
% 13.30/2.56 | ~ (in @ X6 @ (cartesian_product2 @ X5 @ X5))
% 13.30/2.56 | (zip_tseitin_5 @ X6 @ X2 @ X1 @ X0 @ X5))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl58, zip_derived_cl62])).
% 13.30/2.56 thf(zip_derived_cl419, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 13.30/2.56 ( (zip_tseitin_5 @ X3 @ X3 @ X2 @ X1 @ X0)
% 13.30/2.56 | ~ (in @ X3 @ (cartesian_product2 @ X0 @ X0))
% 13.30/2.56 | ((X3) != (ordered_pair @ X5 @ X4))
% 13.30/2.56 | ~ (in @ (ordered_pair @ (apply @ X2 @ X5) @ (apply @ X2 @ X4)) @ X1))),
% 13.30/2.56 inference('eq_res', [status(thm)], [zip_derived_cl282])).
% 13.30/2.56 thf(zip_derived_cl421, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (~ (in @ (ordered_pair @ (apply @ X2 @ X3) @ (apply @ X2 @ X1)) @ X0)
% 13.30/2.56 | ~ (in @ (ordered_pair @ X3 @ X1) @ (cartesian_product2 @ X4 @ X4))
% 13.30/2.56 | (zip_tseitin_5 @ (ordered_pair @ X3 @ X1) @
% 13.30/2.56 (ordered_pair @ X3 @ X1) @ X2 @ X0 @ X4))),
% 13.30/2.56 inference('eq_res', [status(thm)], [zip_derived_cl419])).
% 13.30/2.56 thf(zip_derived_cl422, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 ( (in @ (sk__3 @ X0) @ X0)
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @ (apply @ X3 @ (sk__4 @ X0)) @
% 13.30/2.56 (apply @ X3 @ (sk__5 @ X0))) @
% 13.30/2.56 X2)
% 13.30/2.56 | ~ (in @ (sk__3 @ X0) @ (cartesian_product2 @ X1 @ X1))
% 13.30/2.56 | (zip_tseitin_5 @ (sk__3 @ X0) @ (sk__3 @ X0) @ X3 @ X2 @ X1))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl421])).
% 13.30/2.56 thf(zip_derived_cl435, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i]:
% 13.30/2.56 ( (in @ (sk__3 @ X0) @ X0)
% 13.30/2.56 | (in @ (sk__3 @ X0) @ X0)
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @ (apply @ X2 @ (sk__4 @ X0)) @
% 13.30/2.56 (apply @ X2 @ (sk__5 @ X0))) @
% 13.30/2.56 X1)
% 13.30/2.56 | (zip_tseitin_5 @ (sk__3 @ X0) @ (sk__3 @ X0) @ X2 @ X1 @ sk_))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl0, zip_derived_cl422])).
% 13.30/2.56 thf(zip_derived_cl437, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i]:
% 13.30/2.56 ( (zip_tseitin_5 @ (sk__3 @ X0) @ (sk__3 @ X0) @ X2 @ X1 @ sk_)
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @ (apply @ X2 @ (sk__4 @ X0)) @
% 13.30/2.56 (apply @ X2 @ (sk__5 @ X0))) @
% 13.30/2.56 X1)
% 13.30/2.56 | (in @ (sk__3 @ X0) @ X0))),
% 13.30/2.56 inference('simplify', [status(thm)], [zip_derived_cl435])).
% 13.30/2.56 thf(zip_derived_cl442, plain,
% 13.30/2.56 (![X0 : $i]:
% 13.30/2.56 ( (in @ (sk__3 @ X0) @ X0)
% 13.30/2.56 | (zip_tseitin_5 @ (sk__3 @ X0) @ (sk__3 @ X0) @ sk__2 @ sk__1 @ sk_)
% 13.30/2.56 | (in @ (sk__3 @ X0) @ X0))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl2, zip_derived_cl437])).
% 13.30/2.56 thf(zip_derived_cl443, plain,
% 13.30/2.56 (![X0 : $i]:
% 13.30/2.56 ( (zip_tseitin_5 @ (sk__3 @ X0) @ (sk__3 @ X0) @ sk__2 @ sk__1 @ sk_)
% 13.30/2.56 | (in @ (sk__3 @ X0) @ X0))),
% 13.30/2.56 inference('simplify', [status(thm)], [zip_derived_cl442])).
% 13.30/2.56 thf(zip_derived_cl443, plain,
% 13.30/2.56 (![X0 : $i]:
% 13.30/2.56 ( (zip_tseitin_5 @ (sk__3 @ X0) @ (sk__3 @ X0) @ sk__2 @ sk__1 @ sk_)
% 13.30/2.56 | (in @ (sk__3 @ X0) @ X0))),
% 13.30/2.56 inference('simplify', [status(thm)], [zip_derived_cl442])).
% 13.30/2.56 thf(zf_stmt_3, axiom,
% 13.30/2.56 (![F:$i,E:$i,D:$i,C:$i,B:$i]:
% 13.30/2.56 ( ( ( zip_tseitin_2 @ F @ E @ D @ C @ B ) => ( ( E ) = ( F ) ) ) =>
% 13.30/2.56 ( zip_tseitin_3 @ F @ E @ D @ C @ B ) ))).
% 13.30/2.56 thf(zip_derived_cl55, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 ( (zip_tseitin_3 @ X0 @ X1 @ X2 @ X3 @ X4)
% 13.30/2.56 | (zip_tseitin_2 @ X0 @ X1 @ X2 @ X3 @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_3])).
% 13.30/2.56 thf(zf_stmt_4, type, zip_tseitin_6 : $i > $i > $i > $i > $i > $o).
% 13.30/2.56 thf(zf_stmt_5, axiom,
% 13.30/2.56 (![E:$i,D:$i,C:$i,B:$i,A:$i]:
% 13.30/2.56 ( ( zip_tseitin_6 @ E @ D @ C @ B @ A ) =>
% 13.30/2.56 ( ( in @ E @ D ) <=> ( ?[F:$i]: ( zip_tseitin_5 @ F @ E @ C @ B @ A ) ) ) ))).
% 13.30/2.56 thf(zf_stmt_6, type, zip_tseitin_5 : $i > $i > $i > $i > $i > $o).
% 13.30/2.56 thf(zf_stmt_7, type, zip_tseitin_4 : $i > $i > $i > $i > $i > $o).
% 13.30/2.56 thf(zf_stmt_8, type, zip_tseitin_3 : $i > $i > $i > $i > $i > $o).
% 13.30/2.56 thf(zf_stmt_9, type, zip_tseitin_2 : $i > $i > $i > $i > $i > $o).
% 13.30/2.56 thf(zf_stmt_10, axiom,
% 13.30/2.56 (![F:$i,E:$i,D:$i,C:$i,B:$i]:
% 13.30/2.56 ( ( zip_tseitin_2 @ F @ E @ D @ C @ B ) =>
% 13.30/2.56 ( ( ( D ) = ( E ) ) &
% 13.30/2.56 ( ?[G:$i,H:$i]: ( zip_tseitin_1 @ H @ G @ E @ C @ B ) ) &
% 13.30/2.56 ( ( D ) = ( F ) ) &
% 13.30/2.56 ( ?[I:$i,J:$i]: ( zip_tseitin_0 @ J @ I @ F @ C @ B ) ) ) ))).
% 13.30/2.56 thf(zf_stmt_11, type, zip_tseitin_1 : $i > $i > $i > $i > $i > $o).
% 13.30/2.56 thf(zf_stmt_12, axiom,
% 13.30/2.56 (![H:$i,G:$i,E:$i,C:$i,B:$i]:
% 13.30/2.56 ( ( zip_tseitin_1 @ H @ G @ E @ C @ B ) =>
% 13.30/2.56 ( ( in @ ( ordered_pair @ ( apply @ C @ G ) @ ( apply @ C @ H ) ) @ B ) &
% 13.30/2.56 ( ( E ) = ( ordered_pair @ G @ H ) ) ) ))).
% 13.30/2.56 thf(zf_stmt_13, type, zip_tseitin_0 : $i > $i > $i > $i > $i > $o).
% 13.30/2.56 thf(zf_stmt_14, axiom,
% 13.30/2.56 (![J:$i,I:$i,F:$i,C:$i,B:$i]:
% 13.30/2.56 ( ( zip_tseitin_0 @ J @ I @ F @ C @ B ) =>
% 13.30/2.56 ( ( in @ ( ordered_pair @ ( apply @ C @ I ) @ ( apply @ C @ J ) ) @ B ) &
% 13.30/2.56 ( ( F ) = ( ordered_pair @ I @ J ) ) ) ))).
% 13.30/2.56 thf(zf_stmt_15, axiom,
% 13.30/2.56 (![A:$i,B:$i,C:$i]:
% 13.30/2.56 ( ( ( relation @ B ) & ( relation @ C ) & ( function @ C ) ) =>
% 13.30/2.56 ( ( ![D:$i,E:$i,F:$i]: ( zip_tseitin_3 @ F @ E @ D @ C @ B ) ) =>
% 13.30/2.56 ( ?[D:$i]: ( ![E:$i]: ( zip_tseitin_6 @ E @ D @ C @ B @ A ) ) ) ) ))).
% 13.30/2.56 thf(zip_derived_cl65, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (~ (relation @ X0)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | (zip_tseitin_6 @ X2 @ (sk__24 @ X1 @ X0 @ X3) @ X1 @ X0 @ X3)
% 13.30/2.56 | ~ (zip_tseitin_3 @ (sk__23 @ X1 @ X0) @ (sk__22 @ X1 @ X0) @
% 13.30/2.56 (sk__21 @ X1 @ X0) @ X1 @ X0))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_15])).
% 13.30/2.56 thf(zip_derived_cl275, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 ( (zip_tseitin_2 @ (sk__23 @ X1 @ X0) @ (sk__22 @ X1 @ X0) @
% 13.30/2.56 (sk__21 @ X1 @ X0) @ X1 @ X0)
% 13.30/2.56 | (zip_tseitin_6 @ X3 @ (sk__24 @ X1 @ X0 @ X2) @ X1 @ X0 @ X2)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (relation @ X0))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl55, zip_derived_cl65])).
% 13.30/2.56 thf(zip_derived_cl63, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 13.30/2.56 (~ (zip_tseitin_5 @ X0 @ X1 @ X2 @ X3 @ X4)
% 13.30/2.56 | (in @ X1 @ X5)
% 13.30/2.56 | ~ (zip_tseitin_6 @ X1 @ X5 @ X2 @ X3 @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_5])).
% 13.30/2.56 thf(zip_derived_cl278, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (~ (relation @ X0)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | (zip_tseitin_2 @ (sk__23 @ X1 @ X0) @ (sk__22 @ X1 @ X0) @
% 13.30/2.56 (sk__21 @ X1 @ X0) @ X1 @ X0)
% 13.30/2.56 | (in @ X3 @ (sk__24 @ X1 @ X0 @ X2))
% 13.30/2.56 | ~ (zip_tseitin_5 @ X4 @ X3 @ X1 @ X0 @ X2))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl275, zip_derived_cl63])).
% 13.30/2.56 thf(zip_derived_cl446, plain,
% 13.30/2.56 (![X0 : $i]:
% 13.30/2.56 ( (in @ (sk__3 @ X0) @ X0)
% 13.30/2.56 | ~ (relation @ sk__1)
% 13.30/2.56 | ~ (relation @ sk__2)
% 13.30/2.56 | ~ (function @ sk__2)
% 13.30/2.56 | (zip_tseitin_2 @ (sk__23 @ sk__2 @ sk__1) @
% 13.30/2.56 (sk__22 @ sk__2 @ sk__1) @ (sk__21 @ sk__2 @ sk__1) @ sk__2 @
% 13.30/2.56 sk__1)
% 13.30/2.56 | (in @ (sk__3 @ X0) @ (sk__24 @ sk__2 @ sk__1 @ sk_)))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl443, zip_derived_cl278])).
% 13.30/2.56 thf(zip_derived_cl6, plain, ( (relation @ sk__1)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl5, plain, ( (relation @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl4, plain, ( (function @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl449, plain,
% 13.30/2.56 (![X0 : $i]:
% 13.30/2.56 ( (in @ (sk__3 @ X0) @ X0)
% 13.30/2.56 | (zip_tseitin_2 @ (sk__23 @ sk__2 @ sk__1) @
% 13.30/2.56 (sk__22 @ sk__2 @ sk__1) @ (sk__21 @ sk__2 @ sk__1) @ sk__2 @
% 13.30/2.56 sk__1)
% 13.30/2.56 | (in @ (sk__3 @ X0) @ (sk__24 @ sk__2 @ sk__1 @ sk_)))),
% 13.30/2.56 inference('demod', [status(thm)],
% 13.30/2.56 [zip_derived_cl446, zip_derived_cl6, zip_derived_cl5,
% 13.30/2.56 zip_derived_cl4])).
% 13.30/2.56 thf(zip_derived_cl52, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (((X1) = (X0)) | ~ (zip_tseitin_2 @ X0 @ X2 @ X1 @ X3 @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_10])).
% 13.30/2.56 thf(zip_derived_cl488, plain,
% 13.30/2.56 (![X0 : $i]:
% 13.30/2.56 ( (in @ (sk__3 @ X0) @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 | (in @ (sk__3 @ X0) @ X0)
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl449, zip_derived_cl52])).
% 13.30/2.56 thf(zip_derived_cl550, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (sk__24 @ sk__2 @ sk__1 @ sk_)))),
% 13.30/2.56 inference('eq_fact', [status(thm)], [zip_derived_cl488])).
% 13.30/2.56 thf(zip_derived_cl275, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 ( (zip_tseitin_2 @ (sk__23 @ X1 @ X0) @ (sk__22 @ X1 @ X0) @
% 13.30/2.56 (sk__21 @ X1 @ X0) @ X1 @ X0)
% 13.30/2.56 | (zip_tseitin_6 @ X3 @ (sk__24 @ X1 @ X0 @ X2) @ X1 @ X0 @ X2)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (relation @ X0))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl55, zip_derived_cl65])).
% 13.30/2.56 thf(zip_derived_cl64, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (~ (in @ X0 @ X1)
% 13.30/2.56 | (zip_tseitin_5 @ (sk__20 @ X2 @ X3 @ X4 @ X0) @ X0 @ X4 @ X3 @ X2)
% 13.30/2.56 | ~ (zip_tseitin_6 @ X0 @ X1 @ X4 @ X3 @ X2))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_5])).
% 13.30/2.56 thf(zip_derived_cl279, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (~ (relation @ X0)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | (zip_tseitin_2 @ (sk__23 @ X1 @ X0) @ (sk__22 @ X1 @ X0) @
% 13.30/2.56 (sk__21 @ X1 @ X0) @ X1 @ X0)
% 13.30/2.56 | (zip_tseitin_5 @ (sk__20 @ X2 @ X0 @ X1 @ X3) @ X3 @ X1 @ X0 @ X2)
% 13.30/2.56 | ~ (in @ X3 @ (sk__24 @ X1 @ X0 @ X2)))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl275, zip_derived_cl64])).
% 13.30/2.56 thf(zip_derived_cl554, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | ~ (relation @ sk__1)
% 13.30/2.56 | ~ (relation @ sk__2)
% 13.30/2.56 | ~ (function @ sk__2)
% 13.30/2.56 | (zip_tseitin_2 @ (sk__23 @ sk__2 @ sk__1) @
% 13.30/2.56 (sk__22 @ sk__2 @ sk__1) @ (sk__21 @ sk__2 @ sk__1) @ sk__2 @ sk__1)
% 13.30/2.56 | (zip_tseitin_5 @
% 13.30/2.56 (sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @ sk__2 @ sk__1 @ sk_))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl550, zip_derived_cl279])).
% 13.30/2.56 thf(zip_derived_cl6, plain, ( (relation @ sk__1)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl5, plain, ( (relation @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl4, plain, ( (function @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl556, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | (zip_tseitin_2 @ (sk__23 @ sk__2 @ sk__1) @
% 13.30/2.56 (sk__22 @ sk__2 @ sk__1) @ (sk__21 @ sk__2 @ sk__1) @ sk__2 @ sk__1)
% 13.30/2.56 | (zip_tseitin_5 @
% 13.30/2.56 (sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @ sk__2 @ sk__1 @ sk_))),
% 13.30/2.56 inference('demod', [status(thm)],
% 13.30/2.56 [zip_derived_cl554, zip_derived_cl6, zip_derived_cl5,
% 13.30/2.56 zip_derived_cl4])).
% 13.30/2.56 thf(zip_derived_cl52, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (((X1) = (X0)) | ~ (zip_tseitin_2 @ X0 @ X2 @ X1 @ X3 @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_10])).
% 13.30/2.56 thf(zip_derived_cl1443, plain,
% 13.30/2.56 (( (zip_tseitin_5 @
% 13.30/2.56 (sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @ sk__2 @ sk__1 @ sk_)
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl556, zip_derived_cl52])).
% 13.30/2.56 thf(zip_derived_cl59, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 ( (zip_tseitin_4 @ (sk__19 @ X0 @ X1 @ X2) @
% 13.30/2.56 (sk__18 @ X0 @ X1 @ X2) @ X2 @ X1 @ X0)
% 13.30/2.56 | ~ (zip_tseitin_5 @ X3 @ X2 @ X1 @ X0 @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_2])).
% 13.30/2.56 thf(zip_derived_cl56, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 ( (in @ (ordered_pair @ (apply @ X0 @ X1) @ (apply @ X0 @ X2)) @ X3)
% 13.30/2.56 | ~ (zip_tseitin_4 @ X2 @ X1 @ X4 @ X0 @ X3))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_1])).
% 13.30/2.56 thf(zip_derived_cl280, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (~ (zip_tseitin_5 @ X4 @ X2 @ X1 @ X0 @ X3)
% 13.30/2.56 | (in @
% 13.30/2.56 (ordered_pair @ (apply @ X1 @ (sk__18 @ X0 @ X1 @ X2)) @
% 13.30/2.56 (apply @ X1 @ (sk__19 @ X0 @ X1 @ X2))) @
% 13.30/2.56 X0))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl59, zip_derived_cl56])).
% 13.30/2.56 thf(zip_derived_cl1447, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @
% 13.30/2.56 (ordered_pair @
% 13.30/2.56 (apply @ sk__2 @
% 13.30/2.56 (sk__18 @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))) @
% 13.30/2.56 (apply @ sk__2 @
% 13.30/2.56 (sk__19 @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))))) @
% 13.30/2.56 sk__1))),
% 13.30/2.56 inference('s_sup-', [status(thm)],
% 13.30/2.56 [zip_derived_cl1443, zip_derived_cl280])).
% 13.30/2.56 thf(zip_derived_cl1443, plain,
% 13.30/2.56 (( (zip_tseitin_5 @
% 13.30/2.56 (sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @ sk__2 @ sk__1 @ sk_)
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl556, zip_derived_cl52])).
% 13.30/2.56 thf(zip_derived_cl59, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 ( (zip_tseitin_4 @ (sk__19 @ X0 @ X1 @ X2) @
% 13.30/2.56 (sk__18 @ X0 @ X1 @ X2) @ X2 @ X1 @ X0)
% 13.30/2.56 | ~ (zip_tseitin_5 @ X3 @ X2 @ X1 @ X0 @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_2])).
% 13.30/2.56 thf(zip_derived_cl57, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (((X2) = (ordered_pair @ X0 @ X1))
% 13.30/2.56 | ~ (zip_tseitin_4 @ X1 @ X0 @ X2 @ X3 @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_1])).
% 13.30/2.56 thf(zip_derived_cl281, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (~ (zip_tseitin_5 @ X4 @ X2 @ X1 @ X0 @ X3)
% 13.30/2.56 | ((X2)
% 13.30/2.56 = (ordered_pair @ (sk__18 @ X0 @ X1 @ X2) @
% 13.30/2.56 (sk__19 @ X0 @ X1 @ X2))))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl59, zip_derived_cl57])).
% 13.30/2.56 thf(zip_derived_cl1448, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | ((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 = (ordered_pair @
% 13.30/2.56 (sk__18 @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (sk__19 @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))))))),
% 13.30/2.56 inference('s_sup-', [status(thm)],
% 13.30/2.56 [zip_derived_cl1443, zip_derived_cl281])).
% 13.30/2.56 thf(zip_derived_cl0, plain,
% 13.30/2.56 (![X0 : $i]:
% 13.30/2.56 ( (in @ (sk__3 @ X0) @ (cartesian_product2 @ sk_ @ sk_))
% 13.30/2.56 | (in @ (sk__3 @ X0) @ X0))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl279, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (~ (relation @ X0)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | (zip_tseitin_2 @ (sk__23 @ X1 @ X0) @ (sk__22 @ X1 @ X0) @
% 13.30/2.56 (sk__21 @ X1 @ X0) @ X1 @ X0)
% 13.30/2.56 | (zip_tseitin_5 @ (sk__20 @ X2 @ X0 @ X1 @ X3) @ X3 @ X1 @ X0 @ X2)
% 13.30/2.56 | ~ (in @ X3 @ (sk__24 @ X1 @ X0 @ X2)))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl275, zip_derived_cl64])).
% 13.30/2.56 thf(zip_derived_cl438, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i]:
% 13.30/2.56 ( (in @ (sk__3 @ (sk__24 @ X2 @ X1 @ X0)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_))
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (relation @ X2)
% 13.30/2.56 | ~ (function @ X2)
% 13.30/2.56 | (zip_tseitin_2 @ (sk__23 @ X2 @ X1) @ (sk__22 @ X2 @ X1) @
% 13.30/2.56 (sk__21 @ X2 @ X1) @ X2 @ X1)
% 13.30/2.56 | (zip_tseitin_5 @
% 13.30/2.56 (sk__20 @ X0 @ X1 @ X2 @ (sk__3 @ (sk__24 @ X2 @ X1 @ X0))) @
% 13.30/2.56 (sk__3 @ (sk__24 @ X2 @ X1 @ X0)) @ X2 @ X1 @ X0))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl0, zip_derived_cl279])).
% 13.30/2.56 thf(zip_derived_cl60, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (((X1) = (X0)) | ~ (zip_tseitin_5 @ X1 @ X0 @ X2 @ X3 @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_2])).
% 13.30/2.56 thf(zip_derived_cl456, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i]:
% 13.30/2.56 ( (zip_tseitin_2 @ (sk__23 @ X2 @ X1) @ (sk__22 @ X2 @ X1) @
% 13.30/2.56 (sk__21 @ X2 @ X1) @ X2 @ X1)
% 13.30/2.56 | ~ (function @ X2)
% 13.30/2.56 | ~ (relation @ X2)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | (in @ (sk__3 @ (sk__24 @ X2 @ X1 @ X0)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_))
% 13.30/2.56 | ((sk__20 @ X0 @ X1 @ X2 @ (sk__3 @ (sk__24 @ X2 @ X1 @ X0)))
% 13.30/2.56 = (sk__3 @ (sk__24 @ X2 @ X1 @ X0))))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl438, zip_derived_cl60])).
% 13.30/2.56 thf(zip_derived_cl52, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (((X1) = (X0)) | ~ (zip_tseitin_2 @ X0 @ X2 @ X1 @ X3 @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_10])).
% 13.30/2.56 thf(zip_derived_cl525, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i]:
% 13.30/2.56 (((sk__20 @ X2 @ X0 @ X1 @ (sk__3 @ (sk__24 @ X1 @ X0 @ X2)))
% 13.30/2.56 = (sk__3 @ (sk__24 @ X1 @ X0 @ X2)))
% 13.30/2.56 | (in @ (sk__3 @ (sk__24 @ X1 @ X0 @ X2)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_))
% 13.30/2.56 | ~ (relation @ X0)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | ((sk__21 @ X1 @ X0) = (sk__23 @ X1 @ X0)))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl456, zip_derived_cl52])).
% 13.30/2.56 thf(zip_derived_cl1443, plain,
% 13.30/2.56 (( (zip_tseitin_5 @
% 13.30/2.56 (sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @ sk__2 @ sk__1 @ sk_)
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl556, zip_derived_cl52])).
% 13.30/2.56 thf(zip_derived_cl61, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 ( (in @ X0 @ (cartesian_product2 @ X1 @ X1))
% 13.30/2.56 | ~ (zip_tseitin_5 @ X0 @ X2 @ X3 @ X4 @ X1))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_2])).
% 13.30/2.56 thf(zip_derived_cl1445, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @
% 13.30/2.56 (sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_)))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl1443, zip_derived_cl61])).
% 13.30/2.56 thf(zip_derived_cl1470, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | ~ (function @ sk__2)
% 13.30/2.56 | ~ (relation @ sk__2)
% 13.30/2.56 | ~ (relation @ sk__1)
% 13.30/2.56 | (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_))
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_)))),
% 13.30/2.56 inference('s_sup+', [status(thm)],
% 13.30/2.56 [zip_derived_cl525, zip_derived_cl1445])).
% 13.30/2.56 thf(zip_derived_cl4, plain, ( (function @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl5, plain, ( (relation @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl6, plain, ( (relation @ sk__1)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl1480, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_))
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_)))),
% 13.30/2.56 inference('demod', [status(thm)],
% 13.30/2.56 [zip_derived_cl1470, zip_derived_cl4, zip_derived_cl5,
% 13.30/2.56 zip_derived_cl6])).
% 13.30/2.56 thf(zip_derived_cl1481, plain,
% 13.30/2.56 (( (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_))
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('simplify', [status(thm)], [zip_derived_cl1480])).
% 13.30/2.56 thf(zip_derived_cl550, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (sk__24 @ sk__2 @ sk__1 @ sk_)))),
% 13.30/2.56 inference('eq_fact', [status(thm)], [zip_derived_cl488])).
% 13.30/2.56 thf(zip_derived_cl3, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i]:
% 13.30/2.56 (((sk__3 @ X0) != (ordered_pair @ X1 @ X2))
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @ (apply @ sk__2 @ X1) @ (apply @ sk__2 @ X2)) @
% 13.30/2.56 sk__1)
% 13.30/2.56 | ~ (in @ (sk__3 @ X0) @ (cartesian_product2 @ sk_ @ sk_))
% 13.30/2.56 | ~ (in @ (sk__3 @ X0) @ X0))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl555, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | ((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 != (ordered_pair @ X1 @ X0))
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @ (apply @ sk__2 @ X1) @ (apply @ sk__2 @ X0)) @
% 13.30/2.56 sk__1)
% 13.30/2.56 | ~ (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_)))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl550, zip_derived_cl3])).
% 13.30/2.56 thf(zip_derived_cl1527, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | ((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 != (ordered_pair @ X1 @ X0))
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @ (apply @ sk__2 @ X1) @ (apply @ sk__2 @ X0)) @
% 13.30/2.56 sk__1))),
% 13.30/2.56 inference('s_sup-', [status(thm)],
% 13.30/2.56 [zip_derived_cl1481, zip_derived_cl555])).
% 13.30/2.56 thf(zip_derived_cl1528, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (~ (in @
% 13.30/2.56 (ordered_pair @ (apply @ sk__2 @ X1) @ (apply @ sk__2 @ X0)) @
% 13.30/2.56 sk__1)
% 13.30/2.56 | ((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 != (ordered_pair @ X1 @ X0))
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('simplify', [status(thm)], [zip_derived_cl1527])).
% 13.30/2.56 thf(zip_derived_cl3070, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @
% 13.30/2.56 (apply @ sk__2 @
% 13.30/2.56 (sk__18 @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))) @
% 13.30/2.56 (apply @ sk__2 @
% 13.30/2.56 (sk__19 @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))))) @
% 13.30/2.56 sk__1)
% 13.30/2.56 | ((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 != (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('s_sup-', [status(thm)],
% 13.30/2.56 [zip_derived_cl1448, zip_derived_cl1528])).
% 13.30/2.56 thf(zip_derived_cl3081, plain,
% 13.30/2.56 ((~ (in @
% 13.30/2.56 (ordered_pair @
% 13.30/2.56 (apply @ sk__2 @
% 13.30/2.56 (sk__18 @ sk__1 @ sk__2 @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))) @
% 13.30/2.56 (apply @ sk__2 @
% 13.30/2.56 (sk__19 @ sk__1 @ sk__2 @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))))) @
% 13.30/2.56 sk__1)
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('simplify', [status(thm)], [zip_derived_cl3070])).
% 13.30/2.56 thf(zip_derived_cl3159, plain,
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl1447, zip_derived_cl3081])).
% 13.30/2.56 thf(zip_derived_cl54, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 ( (zip_tseitin_3 @ X0 @ X1 @ X2 @ X3 @ X4) | ((X1) != (X0)))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_3])).
% 13.30/2.56 thf(zip_derived_cl65, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (~ (relation @ X0)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | (zip_tseitin_6 @ X2 @ (sk__24 @ X1 @ X0 @ X3) @ X1 @ X0 @ X3)
% 13.30/2.56 | ~ (zip_tseitin_3 @ (sk__23 @ X1 @ X0) @ (sk__22 @ X1 @ X0) @
% 13.30/2.56 (sk__21 @ X1 @ X0) @ X1 @ X0))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_15])).
% 13.30/2.56 thf(zip_derived_cl274, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (((sk__22 @ X1 @ X0) != (sk__23 @ X1 @ X0))
% 13.30/2.56 | (zip_tseitin_6 @ X3 @ (sk__24 @ X1 @ X0 @ X2) @ X1 @ X0 @ X2)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (relation @ X0))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl54, zip_derived_cl65])).
% 13.30/2.56 thf(zip_derived_cl63, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 13.30/2.56 (~ (zip_tseitin_5 @ X0 @ X1 @ X2 @ X3 @ X4)
% 13.30/2.56 | (in @ X1 @ X5)
% 13.30/2.56 | ~ (zip_tseitin_6 @ X1 @ X5 @ X2 @ X3 @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_5])).
% 13.30/2.56 thf(zip_derived_cl276, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (~ (relation @ X0)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | ((sk__22 @ X1 @ X0) != (sk__23 @ X1 @ X0))
% 13.30/2.56 | (in @ X3 @ (sk__24 @ X1 @ X0 @ X2))
% 13.30/2.56 | ~ (zip_tseitin_5 @ X4 @ X3 @ X1 @ X0 @ X2))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl274, zip_derived_cl63])).
% 13.30/2.56 thf(zip_derived_cl3190, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i]:
% 13.30/2.56 (~ (relation @ sk__1)
% 13.30/2.56 | ~ (relation @ sk__2)
% 13.30/2.56 | ~ (function @ sk__2)
% 13.30/2.56 | ((sk__22 @ sk__2 @ sk__1) != (sk__21 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @ X1 @ (sk__24 @ sk__2 @ sk__1 @ X0))
% 13.30/2.56 | ~ (zip_tseitin_5 @ X2 @ X1 @ sk__2 @ sk__1 @ X0))),
% 13.30/2.56 inference('s_sup-', [status(thm)],
% 13.30/2.56 [zip_derived_cl3159, zip_derived_cl276])).
% 13.30/2.56 thf(zip_derived_cl6, plain, ( (relation @ sk__1)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl5, plain, ( (relation @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl4, plain, ( (function @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl449, plain,
% 13.30/2.56 (![X0 : $i]:
% 13.30/2.56 ( (in @ (sk__3 @ X0) @ X0)
% 13.30/2.56 | (zip_tseitin_2 @ (sk__23 @ sk__2 @ sk__1) @
% 13.30/2.56 (sk__22 @ sk__2 @ sk__1) @ (sk__21 @ sk__2 @ sk__1) @ sk__2 @
% 13.30/2.56 sk__1)
% 13.30/2.56 | (in @ (sk__3 @ X0) @ (sk__24 @ sk__2 @ sk__1 @ sk_)))),
% 13.30/2.56 inference('demod', [status(thm)],
% 13.30/2.56 [zip_derived_cl446, zip_derived_cl6, zip_derived_cl5,
% 13.30/2.56 zip_derived_cl4])).
% 13.30/2.56 thf(zip_derived_cl50, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (((X1) = (X0)) | ~ (zip_tseitin_2 @ X2 @ X0 @ X1 @ X3 @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_10])).
% 13.30/2.56 thf(zip_derived_cl487, plain,
% 13.30/2.56 (![X0 : $i]:
% 13.30/2.56 ( (in @ (sk__3 @ X0) @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 | (in @ (sk__3 @ X0) @ X0)
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl449, zip_derived_cl50])).
% 13.30/2.56 thf(zip_derived_cl511, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (sk__24 @ sk__2 @ sk__1 @ sk_)))),
% 13.30/2.56 inference('eq_fact', [status(thm)], [zip_derived_cl487])).
% 13.30/2.56 thf(zip_derived_cl279, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (~ (relation @ X0)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | (zip_tseitin_2 @ (sk__23 @ X1 @ X0) @ (sk__22 @ X1 @ X0) @
% 13.30/2.56 (sk__21 @ X1 @ X0) @ X1 @ X0)
% 13.30/2.56 | (zip_tseitin_5 @ (sk__20 @ X2 @ X0 @ X1 @ X3) @ X3 @ X1 @ X0 @ X2)
% 13.30/2.56 | ~ (in @ X3 @ (sk__24 @ X1 @ X0 @ X2)))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl275, zip_derived_cl64])).
% 13.30/2.56 thf(zip_derived_cl515, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))
% 13.30/2.56 | ~ (relation @ sk__1)
% 13.30/2.56 | ~ (relation @ sk__2)
% 13.30/2.56 | ~ (function @ sk__2)
% 13.30/2.56 | (zip_tseitin_2 @ (sk__23 @ sk__2 @ sk__1) @
% 13.30/2.56 (sk__22 @ sk__2 @ sk__1) @ (sk__21 @ sk__2 @ sk__1) @ sk__2 @ sk__1)
% 13.30/2.56 | (zip_tseitin_5 @
% 13.30/2.56 (sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @ sk__2 @ sk__1 @ sk_))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl511, zip_derived_cl279])).
% 13.30/2.56 thf(zip_derived_cl6, plain, ( (relation @ sk__1)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl5, plain, ( (relation @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl4, plain, ( (function @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl517, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))
% 13.30/2.56 | (zip_tseitin_2 @ (sk__23 @ sk__2 @ sk__1) @
% 13.30/2.56 (sk__22 @ sk__2 @ sk__1) @ (sk__21 @ sk__2 @ sk__1) @ sk__2 @ sk__1)
% 13.30/2.56 | (zip_tseitin_5 @
% 13.30/2.56 (sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @ sk__2 @ sk__1 @ sk_))),
% 13.30/2.56 inference('demod', [status(thm)],
% 13.30/2.56 [zip_derived_cl515, zip_derived_cl6, zip_derived_cl5,
% 13.30/2.56 zip_derived_cl4])).
% 13.30/2.56 thf(zip_derived_cl50, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (((X1) = (X0)) | ~ (zip_tseitin_2 @ X2 @ X0 @ X1 @ X3 @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_10])).
% 13.30/2.56 thf(zip_derived_cl581, plain,
% 13.30/2.56 (( (zip_tseitin_5 @
% 13.30/2.56 (sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @ sk__2 @ sk__1 @ sk_)
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl517, zip_derived_cl50])).
% 13.30/2.56 thf(zip_derived_cl281, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (~ (zip_tseitin_5 @ X4 @ X2 @ X1 @ X0 @ X3)
% 13.30/2.56 | ((X2)
% 13.30/2.56 = (ordered_pair @ (sk__18 @ X0 @ X1 @ X2) @
% 13.30/2.56 (sk__19 @ X0 @ X1 @ X2))))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl59, zip_derived_cl57])).
% 13.30/2.56 thf(zip_derived_cl586, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))
% 13.30/2.56 | ((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 = (ordered_pair @
% 13.30/2.56 (sk__18 @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (sk__19 @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))))))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl581, zip_derived_cl281])).
% 13.30/2.56 thf(zip_derived_cl581, plain,
% 13.30/2.56 (( (zip_tseitin_5 @
% 13.30/2.56 (sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @ sk__2 @ sk__1 @ sk_)
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl517, zip_derived_cl50])).
% 13.30/2.56 thf(zip_derived_cl60, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (((X1) = (X0)) | ~ (zip_tseitin_5 @ X1 @ X0 @ X2 @ X3 @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_2])).
% 13.30/2.56 thf(zip_derived_cl582, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))
% 13.30/2.56 | ((sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))
% 13.30/2.56 = (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl581, zip_derived_cl60])).
% 13.30/2.56 thf(zip_derived_cl581, plain,
% 13.30/2.56 (( (zip_tseitin_5 @
% 13.30/2.56 (sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @ sk__2 @ sk__1 @ sk_)
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl517, zip_derived_cl50])).
% 13.30/2.56 thf(zip_derived_cl61, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 ( (in @ X0 @ (cartesian_product2 @ X1 @ X1))
% 13.30/2.56 | ~ (zip_tseitin_5 @ X0 @ X2 @ X3 @ X4 @ X1))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_2])).
% 13.30/2.56 thf(zip_derived_cl583, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @
% 13.30/2.56 (sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_)))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl581, zip_derived_cl61])).
% 13.30/2.56 thf(zip_derived_cl600, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_)))),
% 13.30/2.56 inference('s_sup+', [status(thm)], [zip_derived_cl582, zip_derived_cl583])).
% 13.30/2.56 thf(zip_derived_cl609, plain,
% 13.30/2.56 (( (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_))
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('simplify', [status(thm)], [zip_derived_cl600])).
% 13.30/2.56 thf(zip_derived_cl511, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (sk__24 @ sk__2 @ sk__1 @ sk_)))),
% 13.30/2.56 inference('eq_fact', [status(thm)], [zip_derived_cl487])).
% 13.30/2.56 thf(zip_derived_cl3, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i]:
% 13.30/2.56 (((sk__3 @ X0) != (ordered_pair @ X1 @ X2))
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @ (apply @ sk__2 @ X1) @ (apply @ sk__2 @ X2)) @
% 13.30/2.56 sk__1)
% 13.30/2.56 | ~ (in @ (sk__3 @ X0) @ (cartesian_product2 @ sk_ @ sk_))
% 13.30/2.56 | ~ (in @ (sk__3 @ X0) @ X0))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl516, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))
% 13.30/2.56 | ((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 != (ordered_pair @ X1 @ X0))
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @ (apply @ sk__2 @ X1) @ (apply @ sk__2 @ X0)) @
% 13.30/2.56 sk__1)
% 13.30/2.56 | ~ (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_)))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl511, zip_derived_cl3])).
% 13.30/2.56 thf(zip_derived_cl614, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))
% 13.30/2.56 | ((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 != (ordered_pair @ X1 @ X0))
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @ (apply @ sk__2 @ X1) @ (apply @ sk__2 @ X0)) @
% 13.30/2.56 sk__1))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl609, zip_derived_cl516])).
% 13.30/2.56 thf(zip_derived_cl616, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (~ (in @
% 13.30/2.56 (ordered_pair @ (apply @ sk__2 @ X1) @ (apply @ sk__2 @ X0)) @
% 13.30/2.56 sk__1)
% 13.30/2.56 | ((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 != (ordered_pair @ X1 @ X0))
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('simplify', [status(thm)], [zip_derived_cl614])).
% 13.30/2.56 thf(zip_derived_cl2020, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @
% 13.30/2.56 (apply @ sk__2 @
% 13.30/2.56 (sk__18 @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))) @
% 13.30/2.56 (apply @ sk__2 @
% 13.30/2.56 (sk__19 @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))))) @
% 13.30/2.56 sk__1)
% 13.30/2.56 | ((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 != (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl586, zip_derived_cl616])).
% 13.30/2.56 thf(zip_derived_cl2031, plain,
% 13.30/2.56 ((~ (in @
% 13.30/2.56 (ordered_pair @
% 13.30/2.56 (apply @ sk__2 @
% 13.30/2.56 (sk__18 @ sk__1 @ sk__2 @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))) @
% 13.30/2.56 (apply @ sk__2 @
% 13.30/2.56 (sk__19 @ sk__1 @ sk__2 @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))))) @
% 13.30/2.56 sk__1)
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('simplify', [status(thm)], [zip_derived_cl2020])).
% 13.30/2.56 thf(zip_derived_cl581, plain,
% 13.30/2.56 (( (zip_tseitin_5 @
% 13.30/2.56 (sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @ sk__2 @ sk__1 @ sk_)
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1)))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl517, zip_derived_cl50])).
% 13.30/2.56 thf(zip_derived_cl280, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (~ (zip_tseitin_5 @ X4 @ X2 @ X1 @ X0 @ X3)
% 13.30/2.56 | (in @
% 13.30/2.56 (ordered_pair @ (apply @ X1 @ (sk__18 @ X0 @ X1 @ X2)) @
% 13.30/2.56 (apply @ X1 @ (sk__19 @ X0 @ X1 @ X2))) @
% 13.30/2.56 X0))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl59, zip_derived_cl56])).
% 13.30/2.56 thf(zip_derived_cl585, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @
% 13.30/2.56 (ordered_pair @
% 13.30/2.56 (apply @ sk__2 @
% 13.30/2.56 (sk__18 @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))) @
% 13.30/2.56 (apply @ sk__2 @
% 13.30/2.56 (sk__19 @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))))) @
% 13.30/2.56 sk__1))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl581, zip_derived_cl280])).
% 13.30/2.56 thf(zip_derived_cl2038, plain,
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl2031, zip_derived_cl585])).
% 13.30/2.56 thf(zip_derived_cl3225, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i]:
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) != (sk__21 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @ X1 @ (sk__24 @ sk__2 @ sk__1 @ X0))
% 13.30/2.56 | ~ (zip_tseitin_5 @ X2 @ X1 @ sk__2 @ sk__1 @ X0))),
% 13.30/2.56 inference('demod', [status(thm)],
% 13.30/2.56 [zip_derived_cl3190, zip_derived_cl6, zip_derived_cl5,
% 13.30/2.56 zip_derived_cl4, zip_derived_cl2038])).
% 13.30/2.56 thf(zip_derived_cl3226, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i]:
% 13.30/2.56 (~ (zip_tseitin_5 @ X2 @ X1 @ sk__2 @ sk__1 @ X0)
% 13.30/2.56 | (in @ X1 @ (sk__24 @ sk__2 @ sk__1 @ X0)))),
% 13.30/2.56 inference('simplify', [status(thm)], [zip_derived_cl3225])).
% 13.30/2.56 thf(zip_derived_cl3312, plain,
% 13.30/2.56 (![X0 : $i]:
% 13.30/2.56 ( (in @ (sk__3 @ X0) @ X0)
% 13.30/2.56 | (in @ (sk__3 @ X0) @ (sk__24 @ sk__2 @ sk__1 @ sk_)))),
% 13.30/2.56 inference('s_sup-', [status(thm)],
% 13.30/2.56 [zip_derived_cl443, zip_derived_cl3226])).
% 13.30/2.56 thf(zip_derived_cl3360, plain,
% 13.30/2.56 ( (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (sk__24 @ sk__2 @ sk__1 @ sk_))),
% 13.30/2.56 inference('eq_fact', [status(thm)], [zip_derived_cl3312])).
% 13.30/2.56 thf(zip_derived_cl3159, plain,
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl1447, zip_derived_cl3081])).
% 13.30/2.56 thf(zip_derived_cl274, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (((sk__22 @ X1 @ X0) != (sk__23 @ X1 @ X0))
% 13.30/2.56 | (zip_tseitin_6 @ X3 @ (sk__24 @ X1 @ X0 @ X2) @ X1 @ X0 @ X2)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (relation @ X0))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl54, zip_derived_cl65])).
% 13.30/2.56 thf(zip_derived_cl64, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (~ (in @ X0 @ X1)
% 13.30/2.56 | (zip_tseitin_5 @ (sk__20 @ X2 @ X3 @ X4 @ X0) @ X0 @ X4 @ X3 @ X2)
% 13.30/2.56 | ~ (zip_tseitin_6 @ X0 @ X1 @ X4 @ X3 @ X2))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_5])).
% 13.30/2.56 thf(zip_derived_cl277, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (~ (relation @ X0)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | ((sk__22 @ X1 @ X0) != (sk__23 @ X1 @ X0))
% 13.30/2.56 | (zip_tseitin_5 @ (sk__20 @ X2 @ X0 @ X1 @ X3) @ X3 @ X1 @ X0 @ X2)
% 13.30/2.56 | ~ (in @ X3 @ (sk__24 @ X1 @ X0 @ X2)))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl274, zip_derived_cl64])).
% 13.30/2.56 thf(zip_derived_cl281, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (~ (zip_tseitin_5 @ X4 @ X2 @ X1 @ X0 @ X3)
% 13.30/2.56 | ((X2)
% 13.30/2.56 = (ordered_pair @ (sk__18 @ X0 @ X1 @ X2) @
% 13.30/2.56 (sk__19 @ X0 @ X1 @ X2))))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl59, zip_derived_cl57])).
% 13.30/2.56 thf(zip_derived_cl426, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (~ (in @ X3 @ (sk__24 @ X2 @ X1 @ X0))
% 13.30/2.56 | ((sk__22 @ X2 @ X1) != (sk__23 @ X2 @ X1))
% 13.30/2.56 | ~ (function @ X2)
% 13.30/2.56 | ~ (relation @ X2)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ((X3)
% 13.30/2.56 = (ordered_pair @ (sk__18 @ X1 @ X2 @ X3) @
% 13.30/2.56 (sk__19 @ X1 @ X2 @ X3))))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl277, zip_derived_cl281])).
% 13.30/2.56 thf(zip_derived_cl3208, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (~ (in @ X1 @ (sk__24 @ sk__2 @ sk__1 @ X0))
% 13.30/2.56 | ((sk__22 @ sk__2 @ sk__1) != (sk__21 @ sk__2 @ sk__1))
% 13.30/2.56 | ~ (function @ sk__2)
% 13.30/2.56 | ~ (relation @ sk__2)
% 13.30/2.56 | ~ (relation @ sk__1)
% 13.30/2.56 | ((X1)
% 13.30/2.56 = (ordered_pair @ (sk__18 @ sk__1 @ sk__2 @ X1) @
% 13.30/2.56 (sk__19 @ sk__1 @ sk__2 @ X1))))),
% 13.30/2.56 inference('s_sup-', [status(thm)],
% 13.30/2.56 [zip_derived_cl3159, zip_derived_cl426])).
% 13.30/2.56 thf(zip_derived_cl2038, plain,
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl2031, zip_derived_cl585])).
% 13.30/2.56 thf(zip_derived_cl4, plain, ( (function @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl5, plain, ( (relation @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl6, plain, ( (relation @ sk__1)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl3245, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (~ (in @ X1 @ (sk__24 @ sk__2 @ sk__1 @ X0))
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) != (sk__21 @ sk__2 @ sk__1))
% 13.30/2.56 | ((X1)
% 13.30/2.56 = (ordered_pair @ (sk__18 @ sk__1 @ sk__2 @ X1) @
% 13.30/2.56 (sk__19 @ sk__1 @ sk__2 @ X1))))),
% 13.30/2.56 inference('demod', [status(thm)],
% 13.30/2.56 [zip_derived_cl3208, zip_derived_cl2038, zip_derived_cl4,
% 13.30/2.56 zip_derived_cl5, zip_derived_cl6])).
% 13.30/2.56 thf(zip_derived_cl3246, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (((X1)
% 13.30/2.56 = (ordered_pair @ (sk__18 @ sk__1 @ sk__2 @ X1) @
% 13.30/2.56 (sk__19 @ sk__1 @ sk__2 @ X1)))
% 13.30/2.56 | ~ (in @ X1 @ (sk__24 @ sk__2 @ sk__1 @ X0)))),
% 13.30/2.56 inference('simplify', [status(thm)], [zip_derived_cl3245])).
% 13.30/2.56 thf(zip_derived_cl3470, plain,
% 13.30/2.56 (((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 = (ordered_pair @
% 13.30/2.56 (sk__18 @ sk__1 @ sk__2 @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))) @
% 13.30/2.56 (sk__19 @ sk__1 @ sk__2 @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))))),
% 13.30/2.56 inference('s_sup-', [status(thm)],
% 13.30/2.56 [zip_derived_cl3360, zip_derived_cl3246])).
% 13.30/2.56 thf(zip_derived_cl3360, plain,
% 13.30/2.56 ( (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (sk__24 @ sk__2 @ sk__1 @ sk_))),
% 13.30/2.56 inference('eq_fact', [status(thm)], [zip_derived_cl3312])).
% 13.30/2.56 thf(zip_derived_cl3, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i]:
% 13.30/2.56 (((sk__3 @ X0) != (ordered_pair @ X1 @ X2))
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @ (apply @ sk__2 @ X1) @ (apply @ sk__2 @ X2)) @
% 13.30/2.56 sk__1)
% 13.30/2.56 | ~ (in @ (sk__3 @ X0) @ (cartesian_product2 @ sk_ @ sk_))
% 13.30/2.56 | ~ (in @ (sk__3 @ X0) @ X0))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl3367, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) != (ordered_pair @ X1 @ X0))
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @ (apply @ sk__2 @ X1) @ (apply @ sk__2 @ X0)) @
% 13.30/2.56 sk__1)
% 13.30/2.56 | ~ (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_)))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl3360, zip_derived_cl3])).
% 13.30/2.56 thf(zip_derived_cl3360, plain,
% 13.30/2.56 ( (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (sk__24 @ sk__2 @ sk__1 @ sk_))),
% 13.30/2.56 inference('eq_fact', [status(thm)], [zip_derived_cl3312])).
% 13.30/2.56 thf(zip_derived_cl3159, plain,
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl1447, zip_derived_cl3081])).
% 13.30/2.56 thf(zip_derived_cl277, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (~ (relation @ X0)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | ((sk__22 @ X1 @ X0) != (sk__23 @ X1 @ X0))
% 13.30/2.56 | (zip_tseitin_5 @ (sk__20 @ X2 @ X0 @ X1 @ X3) @ X3 @ X1 @ X0 @ X2)
% 13.30/2.56 | ~ (in @ X3 @ (sk__24 @ X1 @ X0 @ X2)))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl274, zip_derived_cl64])).
% 13.30/2.56 thf(zip_derived_cl60, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (((X1) = (X0)) | ~ (zip_tseitin_5 @ X1 @ X0 @ X2 @ X3 @ X4))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_2])).
% 13.30/2.56 thf(zip_derived_cl424, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (~ (in @ X3 @ (sk__24 @ X2 @ X1 @ X0))
% 13.30/2.56 | ((sk__22 @ X2 @ X1) != (sk__23 @ X2 @ X1))
% 13.30/2.56 | ~ (function @ X2)
% 13.30/2.56 | ~ (relation @ X2)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ((sk__20 @ X0 @ X1 @ X2 @ X3) = (X3)))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl277, zip_derived_cl60])).
% 13.30/2.56 thf(zip_derived_cl3207, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (~ (in @ X1 @ (sk__24 @ sk__2 @ sk__1 @ X0))
% 13.30/2.56 | ((sk__22 @ sk__2 @ sk__1) != (sk__21 @ sk__2 @ sk__1))
% 13.30/2.56 | ~ (function @ sk__2)
% 13.30/2.56 | ~ (relation @ sk__2)
% 13.30/2.56 | ~ (relation @ sk__1)
% 13.30/2.56 | ((sk__20 @ X0 @ sk__1 @ sk__2 @ X1) = (X1)))),
% 13.30/2.56 inference('s_sup-', [status(thm)],
% 13.30/2.56 [zip_derived_cl3159, zip_derived_cl424])).
% 13.30/2.56 thf(zip_derived_cl2038, plain,
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl2031, zip_derived_cl585])).
% 13.30/2.56 thf(zip_derived_cl4, plain, ( (function @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl5, plain, ( (relation @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl6, plain, ( (relation @ sk__1)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl3243, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (~ (in @ X1 @ (sk__24 @ sk__2 @ sk__1 @ X0))
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) != (sk__21 @ sk__2 @ sk__1))
% 13.30/2.56 | ((sk__20 @ X0 @ sk__1 @ sk__2 @ X1) = (X1)))),
% 13.30/2.56 inference('demod', [status(thm)],
% 13.30/2.56 [zip_derived_cl3207, zip_derived_cl2038, zip_derived_cl4,
% 13.30/2.56 zip_derived_cl5, zip_derived_cl6])).
% 13.30/2.56 thf(zip_derived_cl3244, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (((sk__20 @ X0 @ sk__1 @ sk__2 @ X1) = (X1))
% 13.30/2.56 | ~ (in @ X1 @ (sk__24 @ sk__2 @ sk__1 @ X0)))),
% 13.30/2.56 inference('simplify', [status(thm)], [zip_derived_cl3243])).
% 13.30/2.56 thf(zip_derived_cl3365, plain,
% 13.30/2.56 (((sk__20 @ sk_ @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))
% 13.30/2.56 = (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))),
% 13.30/2.56 inference('s_sup-', [status(thm)],
% 13.30/2.56 [zip_derived_cl3360, zip_derived_cl3244])).
% 13.30/2.56 thf(zip_derived_cl277, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (~ (relation @ X0)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | ((sk__22 @ X1 @ X0) != (sk__23 @ X1 @ X0))
% 13.30/2.56 | (zip_tseitin_5 @ (sk__20 @ X2 @ X0 @ X1 @ X3) @ X3 @ X1 @ X0 @ X2)
% 13.30/2.56 | ~ (in @ X3 @ (sk__24 @ X1 @ X0 @ X2)))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl274, zip_derived_cl64])).
% 13.30/2.56 thf(zip_derived_cl61, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 ( (in @ X0 @ (cartesian_product2 @ X1 @ X1))
% 13.30/2.56 | ~ (zip_tseitin_5 @ X0 @ X2 @ X3 @ X4 @ X1))),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_2])).
% 13.30/2.56 thf(zip_derived_cl425, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (~ (in @ X3 @ (sk__24 @ X2 @ X1 @ X0))
% 13.30/2.56 | ((sk__22 @ X2 @ X1) != (sk__23 @ X2 @ X1))
% 13.30/2.56 | ~ (function @ X2)
% 13.30/2.56 | ~ (relation @ X2)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | (in @ (sk__20 @ X0 @ X1 @ X2 @ X3) @
% 13.30/2.56 (cartesian_product2 @ X0 @ X0)))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl277, zip_derived_cl61])).
% 13.30/2.56 thf(zip_derived_cl3477, plain,
% 13.30/2.56 ((~ (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 | ((sk__22 @ sk__2 @ sk__1) != (sk__23 @ sk__2 @ sk__1))
% 13.30/2.56 | ~ (function @ sk__2)
% 13.30/2.56 | ~ (relation @ sk__2)
% 13.30/2.56 | ~ (relation @ sk__1)
% 13.30/2.56 | (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_)))),
% 13.30/2.56 inference('s_sup+', [status(thm)],
% 13.30/2.56 [zip_derived_cl3365, zip_derived_cl425])).
% 13.30/2.56 thf(zip_derived_cl3360, plain,
% 13.30/2.56 ( (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (sk__24 @ sk__2 @ sk__1 @ sk_))),
% 13.30/2.56 inference('eq_fact', [status(thm)], [zip_derived_cl3312])).
% 13.30/2.56 thf(zip_derived_cl2038, plain,
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl2031, zip_derived_cl585])).
% 13.30/2.56 thf(zip_derived_cl3159, plain,
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl1447, zip_derived_cl3081])).
% 13.30/2.56 thf(zip_derived_cl4, plain, ( (function @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl5, plain, ( (relation @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl6, plain, ( (relation @ sk__1)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl3496, plain,
% 13.30/2.56 ((((sk__21 @ sk__2 @ sk__1) != (sk__21 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_)))),
% 13.30/2.56 inference('demod', [status(thm)],
% 13.30/2.56 [zip_derived_cl3477, zip_derived_cl3360, zip_derived_cl2038,
% 13.30/2.56 zip_derived_cl3159, zip_derived_cl4, zip_derived_cl5,
% 13.30/2.56 zip_derived_cl6])).
% 13.30/2.56 thf(zip_derived_cl3497, plain,
% 13.30/2.56 ( (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (cartesian_product2 @ sk_ @ sk_))),
% 13.30/2.56 inference('simplify', [status(thm)], [zip_derived_cl3496])).
% 13.30/2.56 thf(zip_derived_cl3523, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) != (ordered_pair @ X1 @ X0))
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @ (apply @ sk__2 @ X1) @ (apply @ sk__2 @ X0)) @
% 13.30/2.56 sk__1))),
% 13.30/2.56 inference('demod', [status(thm)],
% 13.30/2.56 [zip_derived_cl3367, zip_derived_cl3497])).
% 13.30/2.56 thf(zip_derived_cl4258, plain,
% 13.30/2.56 ((((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.56 != (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))
% 13.30/2.56 | ~ (in @
% 13.30/2.56 (ordered_pair @
% 13.30/2.56 (apply @ sk__2 @
% 13.30/2.56 (sk__18 @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))) @
% 13.30/2.56 (apply @ sk__2 @
% 13.30/2.56 (sk__19 @ sk__1 @ sk__2 @
% 13.30/2.56 (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))))) @
% 13.30/2.56 sk__1))),
% 13.30/2.56 inference('s_sup-', [status(thm)],
% 13.30/2.56 [zip_derived_cl3470, zip_derived_cl3523])).
% 13.30/2.56 thf(zip_derived_cl3360, plain,
% 13.30/2.56 ( (in @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)) @
% 13.30/2.56 (sk__24 @ sk__2 @ sk__1 @ sk_))),
% 13.30/2.56 inference('eq_fact', [status(thm)], [zip_derived_cl3312])).
% 13.30/2.56 thf(zip_derived_cl3159, plain,
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) = (sk__23 @ sk__2 @ sk__1))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl1447, zip_derived_cl3081])).
% 13.30/2.56 thf(zip_derived_cl277, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (~ (relation @ X0)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | ~ (function @ X1)
% 13.30/2.56 | ((sk__22 @ X1 @ X0) != (sk__23 @ X1 @ X0))
% 13.30/2.56 | (zip_tseitin_5 @ (sk__20 @ X2 @ X0 @ X1 @ X3) @ X3 @ X1 @ X0 @ X2)
% 13.30/2.56 | ~ (in @ X3 @ (sk__24 @ X1 @ X0 @ X2)))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl274, zip_derived_cl64])).
% 13.30/2.56 thf(zip_derived_cl280, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 13.30/2.56 (~ (zip_tseitin_5 @ X4 @ X2 @ X1 @ X0 @ X3)
% 13.30/2.56 | (in @
% 13.30/2.56 (ordered_pair @ (apply @ X1 @ (sk__18 @ X0 @ X1 @ X2)) @
% 13.30/2.56 (apply @ X1 @ (sk__19 @ X0 @ X1 @ X2))) @
% 13.30/2.56 X0))),
% 13.30/2.56 inference('dp-resolution', [status(thm)],
% 13.30/2.56 [zip_derived_cl59, zip_derived_cl56])).
% 13.30/2.56 thf(zip_derived_cl427, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.30/2.56 (~ (in @ X3 @ (sk__24 @ X2 @ X1 @ X0))
% 13.30/2.56 | ((sk__22 @ X2 @ X1) != (sk__23 @ X2 @ X1))
% 13.30/2.56 | ~ (function @ X2)
% 13.30/2.56 | ~ (relation @ X2)
% 13.30/2.56 | ~ (relation @ X1)
% 13.30/2.56 | (in @
% 13.30/2.56 (ordered_pair @ (apply @ X2 @ (sk__18 @ X1 @ X2 @ X3)) @
% 13.30/2.56 (apply @ X2 @ (sk__19 @ X1 @ X2 @ X3))) @
% 13.30/2.56 X1))),
% 13.30/2.56 inference('s_sup-', [status(thm)], [zip_derived_cl277, zip_derived_cl280])).
% 13.30/2.56 thf(zip_derived_cl3209, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (~ (in @ X1 @ (sk__24 @ sk__2 @ sk__1 @ X0))
% 13.30/2.56 | ((sk__22 @ sk__2 @ sk__1) != (sk__21 @ sk__2 @ sk__1))
% 13.30/2.56 | ~ (function @ sk__2)
% 13.30/2.56 | ~ (relation @ sk__2)
% 13.30/2.56 | ~ (relation @ sk__1)
% 13.30/2.56 | (in @
% 13.30/2.56 (ordered_pair @
% 13.30/2.56 (apply @ sk__2 @ (sk__18 @ sk__1 @ sk__2 @ X1)) @
% 13.30/2.56 (apply @ sk__2 @ (sk__19 @ sk__1 @ sk__2 @ X1))) @
% 13.30/2.56 sk__1))),
% 13.30/2.56 inference('s_sup-', [status(thm)],
% 13.30/2.56 [zip_derived_cl3159, zip_derived_cl427])).
% 13.30/2.56 thf(zip_derived_cl2038, plain,
% 13.30/2.56 (((sk__21 @ sk__2 @ sk__1) = (sk__22 @ sk__2 @ sk__1))),
% 13.30/2.56 inference('clc', [status(thm)], [zip_derived_cl2031, zip_derived_cl585])).
% 13.30/2.56 thf(zip_derived_cl4, plain, ( (function @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl5, plain, ( (relation @ sk__2)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl6, plain, ( (relation @ sk__1)),
% 13.30/2.56 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.30/2.56 thf(zip_derived_cl3247, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 (~ (in @ X1 @ (sk__24 @ sk__2 @ sk__1 @ X0))
% 13.30/2.56 | ((sk__21 @ sk__2 @ sk__1) != (sk__21 @ sk__2 @ sk__1))
% 13.30/2.56 | (in @
% 13.30/2.56 (ordered_pair @
% 13.30/2.56 (apply @ sk__2 @ (sk__18 @ sk__1 @ sk__2 @ X1)) @
% 13.30/2.56 (apply @ sk__2 @ (sk__19 @ sk__1 @ sk__2 @ X1))) @
% 13.30/2.56 sk__1))),
% 13.30/2.56 inference('demod', [status(thm)],
% 13.30/2.56 [zip_derived_cl3209, zip_derived_cl2038, zip_derived_cl4,
% 13.30/2.56 zip_derived_cl5, zip_derived_cl6])).
% 13.30/2.56 thf(zip_derived_cl3248, plain,
% 13.30/2.56 (![X0 : $i, X1 : $i]:
% 13.30/2.56 ( (in @
% 13.30/2.56 (ordered_pair @ (apply @ sk__2 @ (sk__18 @ sk__1 @ sk__2 @ X1)) @
% 13.30/2.57 (apply @ sk__2 @ (sk__19 @ sk__1 @ sk__2 @ X1))) @
% 13.30/2.57 sk__1)
% 13.30/2.57 | ~ (in @ X1 @ (sk__24 @ sk__2 @ sk__1 @ X0)))),
% 13.30/2.57 inference('simplify', [status(thm)], [zip_derived_cl3247])).
% 13.30/2.57 thf(zip_derived_cl3715, plain,
% 13.30/2.57 ( (in @
% 13.30/2.57 (ordered_pair @
% 13.30/2.57 (apply @ sk__2 @
% 13.30/2.57 (sk__18 @ sk__1 @ sk__2 @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))) @
% 13.30/2.57 (apply @ sk__2 @
% 13.30/2.57 (sk__19 @ sk__1 @ sk__2 @ (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))))) @
% 13.30/2.57 sk__1)),
% 13.30/2.57 inference('s_sup-', [status(thm)],
% 13.30/2.57 [zip_derived_cl3360, zip_derived_cl3248])).
% 13.30/2.57 thf(zip_derived_cl4264, plain,
% 13.30/2.57 (((sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_))
% 13.30/2.57 != (sk__3 @ (sk__24 @ sk__2 @ sk__1 @ sk_)))),
% 13.30/2.57 inference('demod', [status(thm)],
% 13.30/2.57 [zip_derived_cl4258, zip_derived_cl3715])).
% 13.30/2.57 thf(zip_derived_cl4265, plain, ($false),
% 13.30/2.57 inference('simplify', [status(thm)], [zip_derived_cl4264])).
% 13.30/2.57
% 13.30/2.57 % SZS output end Refutation
% 13.30/2.57
% 13.30/2.57
% 13.30/2.57 % Terminating...
% 14.13/2.70 % Runner terminated.
% 14.13/2.72 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------