%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWX033+1 : TPTP v9.2.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.yGJ21U6lc3 true
% Computer : n019.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 05:03:35 PM UTC 2025
% Result : Theorem 183.04s 26.91s
% Output : Refutation 183.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWX033+1 : TPTP v9.2.0. Released v9.1.0.
% 0.06/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.yGJ21U6lc3 true
% 0.12/0.36 % Computer : n019.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8042.1875MB
% 0.12/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Wed Oct 1 10:41:38 EDT 2025
% 0.12/0.36 % CPUTime :
% 0.12/0.36 % Running portfolio for 300 s
% 0.12/0.36 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.36 % Number of cores: 8
% 0.12/0.36 % Python version: Python 3.6.8
% 0.12/0.37 % Running in FO mode
% 0.54/0.68 % Total configuration time : 435
% 0.54/0.68 % Estimated wc time : 1092
% 0.54/0.68 % Estimated cpu time (7 cpus) : 156.0
% 0.61/0.77 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.61/0.79 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.62/0.80 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.62/0.81 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.62/0.81 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.62/0.82 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.62/0.82 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 183.04/26.91 % Solved by fo/fo3_bce.sh.
% 183.04/26.91 % BCE start: 151
% 183.04/26.91 % BCE eliminated: 1
% 183.04/26.91 % PE start: 150
% 183.04/26.91 logic: eq
% 183.04/26.91 % PE eliminated: 11
% 183.04/26.91 % done 15810 iterations in 26.087s
% 183.04/26.91 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 183.04/26.91 % SZS output start Refutation
% 183.04/26.91 thf('@+_type', type, '@+': $i > $i > $i).
% 183.04/26.91 thf(sk__31_type, type, sk__31: $i).
% 183.04/26.91 thf(sk__27_type, type, sk__27: $i > $i).
% 183.04/26.91 thf(sk__35_type, type, sk__35: $i).
% 183.04/26.91 thf(sk__36_type, type, sk__36: $i).
% 183.04/26.91 thf(s_type, type, s: $i > $i).
% 183.04/26.91 thf(zip_tseitin_5_type, type, zip_tseitin_5: $i > $i > $i > $i > $i > $o).
% 183.04/26.91 thf(nat_terminates_type, type, nat_terminates: $i > $o).
% 183.04/26.91 thf(sk__37_type, type, sk__37: $i).
% 183.04/26.91 thf(plus_succeeds_type, type, plus_succeeds: $i > $i > $i > $o).
% 183.04/26.91 thf(0_type, type, 0: $i).
% 183.04/26.91 thf(nat_fails_type, type, nat_fails: $i > $o).
% 183.04/26.91 thf(nat_succeeds_type, type, nat_succeeds: $i > $o).
% 183.04/26.91 thf(zip_tseitin_4_type, type, zip_tseitin_4: $i > $i > $i > $o).
% 183.04/26.91 thf(sk__28_type, type, sk__28: $i > $i).
% 183.04/26.91 thf(sk__29_type, type, sk__29: $i > $i).
% 183.04/26.91 thf(sk__34_type, type, sk__34: $i).
% 183.04/26.91 thf(sk__32_type, type, sk__32: $i).
% 183.04/26.91 thf(sk__33_type, type, sk__33: $i).
% 183.04/26.91 thf('lemma-(plus:injective:second)', conjecture,
% 183.04/26.91 (![Xx:$i,Xy:$i,Xz:$i]:
% 183.04/26.91 ( ( ( nat_succeeds @ Xx ) & ( ( '@+' @ Xx @ Xy ) = ( '@+' @ Xx @ Xz ) ) ) =>
% 183.04/26.91 ( ( Xy ) = ( Xz ) ) ))).
% 183.04/26.91 thf(zf_stmt_0, negated_conjecture,
% 183.04/26.91 (~( ![Xx:$i,Xy:$i,Xz:$i]:
% 183.04/26.91 ( ( ( nat_succeeds @ Xx ) & ( ( '@+' @ Xx @ Xy ) = ( '@+' @ Xx @ Xz ) ) ) =>
% 183.04/26.91 ( ( Xy ) = ( Xz ) ) ) )),
% 183.04/26.91 inference('cnf.neg', [status(esa)], [lemma-(plus:injective:second)])).
% 183.04/26.91 thf(zip_derived_cl149, plain,
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) = ('@+' @ sk__35 @ sk__37))),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(induction, axiom,
% 183.04/26.91 (( ![Xx:$i]:
% 183.04/26.91 ( ( ( ?[Xx2:$i]:
% 183.04/26.91 ( ( ![Xy:$i,Xz:$i]:
% 183.04/26.91 ( ( ( '@+' @ Xx2 @ Xy ) = ( '@+' @ Xx2 @ Xz ) ) =>
% 183.04/26.91 ( ( Xy ) = ( Xz ) ) ) ) &
% 183.04/26.91 ( nat_succeeds @ Xx2 ) & ( ( Xx ) = ( s @ Xx2 ) ) ) ) |
% 183.04/26.91 ( ( Xx ) = ( 0 ) ) ) =>
% 183.04/26.91 ( ![Xy:$i,Xz:$i]:
% 183.04/26.91 ( ( ( '@+' @ Xx @ Xy ) = ( '@+' @ Xx @ Xz ) ) => ( ( Xy ) = ( Xz ) ) ) ) ) ) =>
% 183.04/26.91 ( ![Xx:$i]:
% 183.04/26.91 ( ( nat_succeeds @ Xx ) =>
% 183.04/26.91 ( ![Xy:$i,Xz:$i]:
% 183.04/26.91 ( ( ( '@+' @ Xx @ Xy ) = ( '@+' @ Xx @ Xz ) ) => ( ( Xy ) = ( Xz ) ) ) ) ) ))).
% 183.04/26.91 thf(zip_derived_cl145, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 (~ (nat_succeeds @ X0)
% 183.04/26.91 | ((X2) = (X1))
% 183.04/26.91 | (('@+' @ X0 @ X2) != ('@+' @ X0 @ X1))
% 183.04/26.91 | ((sk__31) = (s @ sk__34))
% 183.04/26.91 | ((sk__31) = (0)))),
% 183.04/26.91 inference('cnf', [status(esa)], [induction])).
% 183.04/26.91 thf(zip_derived_cl2121, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) != ('@+' @ sk__35 @ X0))
% 183.04/26.91 | ((sk__31) = (0))
% 183.04/26.91 | ((sk__31) = (s @ sk__34))
% 183.04/26.91 | ((sk__37) = (X0))
% 183.04/26.91 | ~ (nat_succeeds @ sk__35))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl149, zip_derived_cl145])).
% 183.04/26.91 thf(zip_derived_cl150, plain, ( (nat_succeeds @ sk__35)),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(zip_derived_cl2136, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) != ('@+' @ sk__35 @ X0))
% 183.04/26.91 | ((sk__31) = (0))
% 183.04/26.91 | ((sk__31) = (s @ sk__34))
% 183.04/26.91 | ((sk__37) = (X0)))),
% 183.04/26.91 inference('demod', [status(thm)], [zip_derived_cl2121, zip_derived_cl150])).
% 183.04/26.91 thf(zip_derived_cl149, plain,
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) = ('@+' @ sk__35 @ sk__37))),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(zip_derived_cl143, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 (~ (nat_succeeds @ X0)
% 183.04/26.91 | ((X2) = (X1))
% 183.04/26.91 | (('@+' @ X0 @ X2) != ('@+' @ X0 @ X1))
% 183.04/26.91 | (('@+' @ sk__31 @ sk__32) = ('@+' @ sk__31 @ sk__33)))),
% 183.04/26.91 inference('cnf', [status(esa)], [induction])).
% 183.04/26.91 thf(zip_derived_cl2033, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) != ('@+' @ sk__35 @ X0))
% 183.04/26.91 | (('@+' @ sk__31 @ sk__32) = ('@+' @ sk__31 @ sk__33))
% 183.04/26.91 | ((sk__37) = (X0))
% 183.04/26.91 | ~ (nat_succeeds @ sk__35))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl149, zip_derived_cl143])).
% 183.04/26.91 thf(zip_derived_cl150, plain, ( (nat_succeeds @ sk__35)),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(zip_derived_cl2048, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) != ('@+' @ sk__35 @ X0))
% 183.04/26.91 | (('@+' @ sk__31 @ sk__32) = ('@+' @ sk__31 @ sk__33))
% 183.04/26.91 | ((sk__37) = (X0)))),
% 183.04/26.91 inference('demod', [status(thm)], [zip_derived_cl2033, zip_derived_cl150])).
% 183.04/26.91 thf(zip_derived_cl37727, plain,
% 183.04/26.91 ((((sk__37) = (sk__36))
% 183.04/26.91 | (('@+' @ sk__31 @ sk__32) = ('@+' @ sk__31 @ sk__33)))),
% 183.04/26.91 inference('eq_res', [status(thm)], [zip_derived_cl2048])).
% 183.04/26.91 thf(zip_derived_cl148, plain, (((sk__36) != (sk__37))),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(zip_derived_cl37728, plain,
% 183.04/26.91 ((('@+' @ sk__31 @ sk__32) = ('@+' @ sk__31 @ sk__33))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl37727, zip_derived_cl148])).
% 183.04/26.91 thf(id18, axiom,
% 183.04/26.91 (![Xx1:$i,Xx2:$i,Xx3:$i]:
% 183.04/26.91 ( ( plus_succeeds @ Xx1 @ Xx2 @ Xx3 ) <=>
% 183.04/26.91 ( ( ( ( Xx3 ) = ( Xx2 ) ) & ( ( Xx1 ) = ( 0 ) ) ) |
% 183.04/26.91 ( ?[Xx4:$i,Xx5:$i]:
% 183.04/26.91 ( ( ( Xx1 ) = ( s @ Xx4 ) ) & ( ( Xx3 ) = ( s @ Xx5 ) ) &
% 183.04/26.91 ( plus_succeeds @ Xx4 @ Xx2 @ Xx5 ) ) ) ) ))).
% 183.04/26.91 thf(zf_stmt_1, axiom,
% 183.04/26.91 (![Xx3:$i,Xx2:$i,Xx1:$i]:
% 183.04/26.91 ( ( zip_tseitin_4 @ Xx3 @ Xx2 @ Xx1 ) <=>
% 183.04/26.91 ( ( ( Xx1 ) = ( 0 ) ) & ( ( Xx3 ) = ( Xx2 ) ) ) ))).
% 183.04/26.91 thf(zip_derived_cl42, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 ( (zip_tseitin_4 @ X0 @ X1 @ X2) | ((X0) != (X1)) | ((X2) != (0)))),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_1])).
% 183.04/26.91 thf(zf_stmt_2, type, zip_tseitin_5 : $i > $i > $i > $i > $i > $o).
% 183.04/26.91 thf(zf_stmt_3, axiom,
% 183.04/26.91 (![Xx5:$i,Xx4:$i,Xx3:$i,Xx2:$i,Xx1:$i]:
% 183.04/26.91 ( ( zip_tseitin_5 @ Xx5 @ Xx4 @ Xx3 @ Xx2 @ Xx1 ) <=>
% 183.04/26.91 ( ( plus_succeeds @ Xx4 @ Xx2 @ Xx5 ) & ( ( Xx3 ) = ( s @ Xx5 ) ) &
% 183.04/26.91 ( ( Xx1 ) = ( s @ Xx4 ) ) ) ))).
% 183.04/26.91 thf(zf_stmt_4, type, zip_tseitin_4 : $i > $i > $i > $o).
% 183.04/26.91 thf(zf_stmt_5, axiom,
% 183.04/26.91 (![Xx1:$i,Xx2:$i,Xx3:$i]:
% 183.04/26.91 ( ( plus_succeeds @ Xx1 @ Xx2 @ Xx3 ) <=>
% 183.04/26.91 ( ( ?[Xx4:$i,Xx5:$i]: ( zip_tseitin_5 @ Xx5 @ Xx4 @ Xx3 @ Xx2 @ Xx1 ) ) |
% 183.04/26.91 ( zip_tseitin_4 @ Xx3 @ Xx2 @ Xx1 ) ) ))).
% 183.04/26.91 thf(zip_derived_cl49, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 ( (plus_succeeds @ X0 @ X1 @ X2) | ~ (zip_tseitin_4 @ X2 @ X1 @ X0))),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_5])).
% 183.04/26.91 thf(zip_derived_cl807, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 (((X0) != (0)) | ((X2) != (X1)) | (plus_succeeds @ X0 @ X1 @ X2))),
% 183.04/26.91 inference('dp-resolution', [status(thm)],
% 183.04/26.91 [zip_derived_cl42, zip_derived_cl49])).
% 183.04/26.91 thf('(@+)/2', axiom,
% 183.04/26.91 (![Xx:$i,Xy:$i,Xz:$i]:
% 183.04/26.91 ( ( nat_succeeds @ Xx ) =>
% 183.04/26.91 ( ( ( '@+' @ Xx @ Xy ) = ( Xz ) ) <=> ( plus_succeeds @ Xx @ Xy @ Xz ) ) ))).
% 183.04/26.91 thf(zip_derived_cl119, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 (~ (nat_succeeds @ X0)
% 183.04/26.91 | (('@+' @ X0 @ X2) = (X1))
% 183.04/26.91 | ~ (plus_succeeds @ X0 @ X2 @ X1))),
% 183.04/26.91 inference('cnf', [status(esa)], [(@+)/2])).
% 183.04/26.91 thf('lemma-(plus:types:1)', axiom,
% 183.04/26.91 (![Xx:$i,Xy:$i,Xz:$i]:
% 183.04/26.91 ( ( plus_succeeds @ Xx @ Xy @ Xz ) => ( nat_succeeds @ Xx ) ))).
% 183.04/26.91 thf(zip_derived_cl127, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 ( (nat_succeeds @ X0) | ~ (plus_succeeds @ X0 @ X1 @ X2))),
% 183.04/26.91 inference('cnf', [status(esa)], [lemma-(plus:types:1)])).
% 183.04/26.91 thf(zip_derived_cl1339, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 (~ (plus_succeeds @ X0 @ X2 @ X1) | (('@+' @ X0 @ X2) = (X1)))),
% 183.04/26.91 inference('clc', [status(thm)], [zip_derived_cl119, zip_derived_cl127])).
% 183.04/26.91 thf(zip_derived_cl1343, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 (((X0) != (X1)) | ((X2) != (0)) | (('@+' @ X2 @ X1) = (X0)))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl807, zip_derived_cl1339])).
% 183.04/26.91 thf(zip_derived_cl1385, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]: ((('@+' @ X1 @ X0) = (X0)) | ((X1) != (0)))),
% 183.04/26.91 inference('eq_res', [status(thm)], [zip_derived_cl1343])).
% 183.04/26.91 thf(zip_derived_cl37751, plain,
% 183.04/26.91 (((('@+' @ sk__31 @ sk__32) = (sk__33)) | ((sk__31) != (0)))),
% 183.04/26.91 inference('sup+', [status(thm)],
% 183.04/26.91 [zip_derived_cl37728, zip_derived_cl1385])).
% 183.04/26.91 thf(zip_derived_cl37777, plain,
% 183.04/26.91 (((('@+' @ 0 @ sk__32) = (sk__33)) | ((sk__31) != (0)))),
% 183.04/26.91 inference('local_rewriting', [status(thm)], [zip_derived_cl37751])).
% 183.04/26.91 thf('corollary-(plus:zero)', axiom,
% 183.04/26.91 (![Xy:$i]: ( ( '@+' @ 0 @ Xy ) = ( Xy ) ))).
% 183.04/26.91 thf(zip_derived_cl136, plain, (![X0 : $i]: (('@+' @ 0 @ X0) = (X0))),
% 183.04/26.91 inference('cnf', [status(esa)], [corollary-(plus:zero)])).
% 183.04/26.91 thf(zip_derived_cl37789, plain,
% 183.04/26.91 ((((sk__32) = (sk__33)) | ((sk__31) != (0)))),
% 183.04/26.91 inference('demod', [status(thm)],
% 183.04/26.91 [zip_derived_cl37777, zip_derived_cl136])).
% 183.04/26.91 thf(zip_derived_cl149, plain,
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) = ('@+' @ sk__35 @ sk__37))),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(zip_derived_cl144, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 (~ (nat_succeeds @ X0)
% 183.04/26.91 | ((X2) = (X1))
% 183.04/26.91 | (('@+' @ X0 @ X2) != ('@+' @ X0 @ X1))
% 183.04/26.91 | ((sk__32) != (sk__33)))),
% 183.04/26.91 inference('cnf', [status(esa)], [induction])).
% 183.04/26.91 thf(zip_derived_cl955, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) != ('@+' @ sk__35 @ X0))
% 183.04/26.91 | ((sk__32) != (sk__33))
% 183.04/26.91 | ((sk__37) = (X0))
% 183.04/26.91 | ~ (nat_succeeds @ sk__35))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl149, zip_derived_cl144])).
% 183.04/26.91 thf(zip_derived_cl150, plain, ( (nat_succeeds @ sk__35)),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(zip_derived_cl962, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) != ('@+' @ sk__35 @ X0))
% 183.04/26.91 | ((sk__32) != (sk__33))
% 183.04/26.91 | ((sk__37) = (X0)))),
% 183.04/26.91 inference('demod', [status(thm)], [zip_derived_cl955, zip_derived_cl150])).
% 183.04/26.91 thf(zip_derived_cl967, plain,
% 183.04/26.91 ((((sk__37) = (sk__36)) | ((sk__32) != (sk__33)))),
% 183.04/26.91 inference('eq_res', [status(thm)], [zip_derived_cl962])).
% 183.04/26.91 thf(zip_derived_cl148, plain, (((sk__36) != (sk__37))),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(zip_derived_cl968, plain, (((sk__32) != (sk__33))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl967, zip_derived_cl148])).
% 183.04/26.91 thf(zip_derived_cl37790, plain, (((sk__31) != (0))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl37789, zip_derived_cl968])).
% 183.04/26.91 thf(zip_derived_cl120122, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) != ('@+' @ sk__35 @ X0))
% 183.04/26.91 | ((sk__31) = (s @ sk__34))
% 183.04/26.91 | ((sk__37) = (X0)))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl2136, zip_derived_cl37790])).
% 183.04/26.91 thf(zip_derived_cl120141, plain,
% 183.04/26.91 ((((sk__37) = (sk__36)) | ((sk__31) = (s @ sk__34)))),
% 183.04/26.91 inference('eq_res', [status(thm)], [zip_derived_cl120122])).
% 183.04/26.91 thf(zip_derived_cl148, plain, (((sk__36) != (sk__37))),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(zip_derived_cl120142, plain, (((sk__31) = (s @ sk__34))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl120141, zip_derived_cl148])).
% 183.04/26.91 thf(id27, axiom,
% 183.04/26.91 (![Xx1:$i]:
% 183.04/26.91 ( ( nat_succeeds @ Xx1 ) <=>
% 183.04/26.91 ( ( ?[Xx2:$i]: ( ( nat_succeeds @ Xx2 ) & ( ( Xx1 ) = ( s @ Xx2 ) ) ) ) |
% 183.04/26.91 ( ( Xx1 ) = ( 0 ) ) ) ))).
% 183.04/26.91 thf(zip_derived_cl108, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((X0) = (0)) | ((X0) = (s @ (sk__27 @ X0))) | ~ (nat_succeeds @ X0))),
% 183.04/26.91 inference('cnf', [status(esa)], [id27])).
% 183.04/26.91 thf(id2, axiom,
% 183.04/26.91 (![Xx4:$i,Xx5:$i]:
% 183.04/26.91 ( ( ( s @ Xx4 ) = ( s @ Xx5 ) ) => ( ( Xx4 ) = ( Xx5 ) ) ))).
% 183.04/26.91 thf(zip_derived_cl1, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]: (((X1) = (X0)) | ((s @ X1) != (s @ X0)))),
% 183.04/26.91 inference('cnf', [status(esa)], [id2])).
% 183.04/26.91 thf(zip_derived_cl1356, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (((s @ X1) != (X0))
% 183.04/26.91 | ~ (nat_succeeds @ X0)
% 183.04/26.91 | ((X0) = (0))
% 183.04/26.91 | ((X1) = (sk__27 @ X0)))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl108, zip_derived_cl1])).
% 183.04/26.91 thf(zip_derived_cl1530, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((X0) = (sk__27 @ (s @ X0)))
% 183.04/26.91 | ((s @ X0) = (0))
% 183.04/26.91 | ~ (nat_succeeds @ (s @ X0)))),
% 183.04/26.91 inference('eq_res', [status(thm)], [zip_derived_cl1356])).
% 183.04/26.91 thf(id1, axiom, (![Xx3:$i]: ( ( 0 ) != ( s @ Xx3 ) ))).
% 183.04/26.91 thf(zip_derived_cl0, plain, (![X0 : $i]: ((0) != (s @ X0))),
% 183.04/26.91 inference('cnf', [status(esa)], [id1])).
% 183.04/26.91 thf(zip_derived_cl1531, plain,
% 183.04/26.91 (![X0 : $i]: (((X0) = (sk__27 @ (s @ X0))) | ~ (nat_succeeds @ (s @ X0)))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl1530, zip_derived_cl0])).
% 183.04/26.91 thf(zip_derived_cl120352, plain,
% 183.04/26.91 ((((sk__34) = (sk__27 @ sk__31)) | ~ (nat_succeeds @ (s @ sk__34)))),
% 183.04/26.91 inference('sup+', [status(thm)],
% 183.04/26.91 [zip_derived_cl120142, zip_derived_cl1531])).
% 183.04/26.91 thf(zip_derived_cl120142, plain, (((sk__31) = (s @ sk__34))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl120141, zip_derived_cl148])).
% 183.04/26.91 thf(zip_derived_cl120576, plain,
% 183.04/26.91 ((((sk__34) = (sk__27 @ sk__31)) | ~ (nat_succeeds @ sk__31))),
% 183.04/26.91 inference('demod', [status(thm)],
% 183.04/26.91 [zip_derived_cl120352, zip_derived_cl120142])).
% 183.04/26.91 thf(zip_derived_cl120142, plain, (((sk__31) = (s @ sk__34))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl120141, zip_derived_cl148])).
% 183.04/26.91 thf(zip_derived_cl136, plain, (![X0 : $i]: (('@+' @ 0 @ X0) = (X0))),
% 183.04/26.91 inference('cnf', [status(esa)], [corollary-(plus:zero)])).
% 183.04/26.91 thf(zip_derived_cl120, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 (~ (nat_succeeds @ X0)
% 183.04/26.91 | (plus_succeeds @ X0 @ X1 @ X2)
% 183.04/26.91 | (('@+' @ X0 @ X1) != (X2)))),
% 183.04/26.91 inference('cnf', [status(esa)], [(@+)/2])).
% 183.04/26.91 thf('lemma-(plus:types:3)', axiom,
% 183.04/26.91 (![Xx:$i,Xy:$i,Xz:$i]:
% 183.04/26.91 ( ( ( plus_succeeds @ Xx @ Xy @ Xz ) & ( nat_succeeds @ Xz ) ) =>
% 183.04/26.91 ( nat_succeeds @ Xy ) ))).
% 183.04/26.91 thf(zip_derived_cl129, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 ( (nat_succeeds @ X0)
% 183.04/26.91 | ~ (plus_succeeds @ X1 @ X0 @ X2)
% 183.04/26.91 | ~ (nat_succeeds @ X2))),
% 183.04/26.91 inference('cnf', [status(esa)], [lemma-(plus:types:3)])).
% 183.04/26.91 thf(zip_derived_cl1698, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 ((('@+' @ X2 @ X1) != (X0))
% 183.04/26.91 | ~ (nat_succeeds @ X2)
% 183.04/26.91 | ~ (nat_succeeds @ X0)
% 183.04/26.91 | (nat_succeeds @ X1))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl120, zip_derived_cl129])).
% 183.04/26.91 thf(zip_derived_cl2065, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 ( (nat_succeeds @ X0)
% 183.04/26.91 | ~ (nat_succeeds @ ('@+' @ X1 @ X0))
% 183.04/26.91 | ~ (nat_succeeds @ X1))),
% 183.04/26.91 inference('eq_res', [status(thm)], [zip_derived_cl1698])).
% 183.04/26.91 thf(zip_derived_cl149, plain,
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) = ('@+' @ sk__35 @ sk__37))),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(zip_derived_cl146, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 (~ (nat_succeeds @ X0)
% 183.04/26.91 | ((X2) = (X1))
% 183.04/26.91 | (('@+' @ X0 @ X2) != ('@+' @ X0 @ X1))
% 183.04/26.91 | (nat_succeeds @ sk__34)
% 183.04/26.91 | ((sk__31) = (0)))),
% 183.04/26.91 inference('cnf', [status(esa)], [induction])).
% 183.04/26.91 thf(zip_derived_cl2199, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) != ('@+' @ sk__35 @ X0))
% 183.04/26.91 | ((sk__31) = (0))
% 183.04/26.91 | (nat_succeeds @ sk__34)
% 183.04/26.91 | ((sk__37) = (X0))
% 183.04/26.91 | ~ (nat_succeeds @ sk__35))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl149, zip_derived_cl146])).
% 183.04/26.91 thf(zip_derived_cl150, plain, ( (nat_succeeds @ sk__35)),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(zip_derived_cl2214, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) != ('@+' @ sk__35 @ X0))
% 183.04/26.91 | ((sk__31) = (0))
% 183.04/26.91 | (nat_succeeds @ sk__34)
% 183.04/26.91 | ((sk__37) = (X0)))),
% 183.04/26.91 inference('demod', [status(thm)], [zip_derived_cl2199, zip_derived_cl150])).
% 183.04/26.91 thf(zip_derived_cl35369, plain,
% 183.04/26.91 ((((sk__37) = (sk__36)) | (nat_succeeds @ sk__34) | ((sk__31) = (0)))),
% 183.04/26.91 inference('eq_res', [status(thm)], [zip_derived_cl2214])).
% 183.04/26.91 thf(zip_derived_cl148, plain, (((sk__36) != (sk__37))),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(zip_derived_cl35370, plain,
% 183.04/26.91 (( (nat_succeeds @ sk__34) | ((sk__31) = (0)))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl35369, zip_derived_cl148])).
% 183.04/26.91 thf(zip_derived_cl110, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 ( (nat_succeeds @ X0) | ~ (nat_succeeds @ X1) | ((X0) != (s @ X1)))),
% 183.04/26.91 inference('cnf', [status(esa)], [id27])).
% 183.04/26.91 thf(zip_derived_cl35387, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((sk__31) = (0)) | ((X0) != (s @ sk__34)) | (nat_succeeds @ X0))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl35370, zip_derived_cl110])).
% 183.04/26.91 thf(zip_derived_cl110, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 ( (nat_succeeds @ X0) | ~ (nat_succeeds @ X1) | ((X0) != (s @ X1)))),
% 183.04/26.91 inference('cnf', [status(esa)], [id27])).
% 183.04/26.91 thf(zip_derived_cl35415, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (((X0) != (s @ sk__34))
% 183.04/26.91 | ((sk__31) = (0))
% 183.04/26.91 | ((X1) != (s @ X0))
% 183.04/26.91 | (nat_succeeds @ X1))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl35387, zip_derived_cl110])).
% 183.04/26.91 thf(zip_derived_cl35660, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ( (nat_succeeds @ X0)
% 183.04/26.91 | ((X0) != (s @ (s @ sk__34)))
% 183.04/26.91 | ((sk__31) = (0)))),
% 183.04/26.91 inference('eq_res', [status(thm)], [zip_derived_cl35415])).
% 183.04/26.91 thf(id29, axiom,
% 183.04/26.91 (![Xx1:$i]:
% 183.04/26.91 ( ( nat_terminates @ Xx1 ) <=>
% 183.04/26.91 ( ![Xx2:$i]: ( ( nat_terminates @ Xx2 ) | ( ( Xx1 ) != ( s @ Xx2 ) ) ) ) ))).
% 183.04/26.91 thf(zip_derived_cl118, plain,
% 183.04/26.91 (![X0 : $i]: ( (nat_terminates @ X0) | ((X0) = (s @ (sk__29 @ X0))))),
% 183.04/26.91 inference('cnf', [status(esa)], [id29])).
% 183.04/26.91 thf(zip_derived_cl35370, plain,
% 183.04/26.91 (( (nat_succeeds @ sk__34) | ((sk__31) = (0)))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl35369, zip_derived_cl148])).
% 183.04/26.91 thf('lemma-(nat:termination)', axiom,
% 183.04/26.91 (![Xx:$i]: ( ( nat_succeeds @ Xx ) => ( nat_terminates @ Xx ) ))).
% 183.04/26.91 thf(zip_derived_cl123, plain,
% 183.04/26.91 (![X0 : $i]: ( (nat_terminates @ X0) | ~ (nat_succeeds @ X0))),
% 183.04/26.91 inference('cnf', [status(esa)], [lemma-(nat:termination)])).
% 183.04/26.91 thf(zip_derived_cl116, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (((X1) != (s @ X0)) | (nat_terminates @ X0) | ~ (nat_terminates @ X1))),
% 183.04/26.91 inference('cnf', [status(esa)], [id29])).
% 183.04/26.91 thf(zip_derived_cl894, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (~ (nat_succeeds @ X0) | (nat_terminates @ X1) | ((X0) != (s @ X1)))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl123, zip_derived_cl116])).
% 183.04/26.91 thf(zip_derived_cl35381, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((sk__31) = (0)) | ((sk__34) != (s @ X0)) | (nat_terminates @ X0))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl35370, zip_derived_cl894])).
% 183.04/26.91 thf(zip_derived_cl117, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ( (nat_terminates @ X0) | ~ (nat_terminates @ (sk__29 @ X0)))),
% 183.04/26.91 inference('cnf', [status(esa)], [id29])).
% 183.04/26.91 thf(zip_derived_cl35404, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((sk__34) != (s @ (sk__29 @ X0)))
% 183.04/26.91 | ((sk__31) = (0))
% 183.04/26.91 | (nat_terminates @ X0))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl35381, zip_derived_cl117])).
% 183.04/26.91 thf(zip_derived_cl35569, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((sk__34) != (X0))
% 183.04/26.91 | (nat_terminates @ X0)
% 183.04/26.91 | (nat_terminates @ X0)
% 183.04/26.91 | ((sk__31) = (0)))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl118, zip_derived_cl35404])).
% 183.04/26.91 thf(zip_derived_cl35571, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((sk__31) = (0)) | (nat_terminates @ X0) | ((sk__34) != (X0)))),
% 183.04/26.91 inference('simplify', [status(thm)], [zip_derived_cl35569])).
% 183.04/26.91 thf(id14, axiom,
% 183.04/26.91 (![Xx17:$i]:
% 183.04/26.91 ( ( nat_terminates @ Xx17 ) =>
% 183.04/26.91 ( ( nat_succeeds @ Xx17 ) | ( nat_fails @ Xx17 ) ) ))).
% 183.04/26.91 thf(zip_derived_cl14, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ( (nat_fails @ X0) | (nat_succeeds @ X0) | ~ (nat_terminates @ X0))),
% 183.04/26.91 inference('cnf', [status(esa)], [id14])).
% 183.04/26.91 thf(zip_derived_cl35574, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((sk__34) != (X0))
% 183.04/26.91 | ((sk__31) = (0))
% 183.04/26.91 | (nat_succeeds @ X0)
% 183.04/26.91 | (nat_fails @ X0))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl35571, zip_derived_cl14])).
% 183.04/26.91 thf(zip_derived_cl37790, plain, (((sk__31) != (0))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl37789, zip_derived_cl968])).
% 183.04/26.91 thf(zip_derived_cl91412, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((sk__34) != (X0)) | (nat_succeeds @ X0) | (nat_fails @ X0))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl35574, zip_derived_cl37790])).
% 183.04/26.91 thf(id28, axiom,
% 183.04/26.91 (![Xx1:$i]:
% 183.04/26.91 ( ( nat_fails @ Xx1 ) <=>
% 183.04/26.91 ( ( ![Xx2:$i]: ( ( nat_fails @ Xx2 ) | ( ( Xx1 ) != ( s @ Xx2 ) ) ) ) &
% 183.04/26.91 ( ( Xx1 ) != ( 0 ) ) ) ))).
% 183.04/26.91 thf(zip_derived_cl114, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ( (nat_fails @ X0) | ((X0) = (0)) | ((X0) = (s @ (sk__28 @ X0))))),
% 183.04/26.91 inference('cnf', [status(esa)], [id28])).
% 183.04/26.91 thf(zip_derived_cl1, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]: (((X1) = (X0)) | ((s @ X1) != (s @ X0)))),
% 183.04/26.91 inference('cnf', [status(esa)], [id2])).
% 183.04/26.91 thf(zip_derived_cl1540, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (((s @ X1) != (X0))
% 183.04/26.91 | ((X0) = (0))
% 183.04/26.91 | (nat_fails @ X0)
% 183.04/26.91 | ((X1) = (sk__28 @ X0)))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl114, zip_derived_cl1])).
% 183.04/26.91 thf(zip_derived_cl8128, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((X0) = (sk__28 @ (s @ X0)))
% 183.04/26.91 | (nat_fails @ (s @ X0))
% 183.04/26.91 | ((s @ X0) = (0)))),
% 183.04/26.91 inference('eq_res', [status(thm)], [zip_derived_cl1540])).
% 183.04/26.91 thf(zip_derived_cl0, plain, (![X0 : $i]: ((0) != (s @ X0))),
% 183.04/26.91 inference('cnf', [status(esa)], [id1])).
% 183.04/26.91 thf(zip_derived_cl8129, plain,
% 183.04/26.91 (![X0 : $i]: (((X0) = (sk__28 @ (s @ X0))) | (nat_fails @ (s @ X0)))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl8128, zip_derived_cl0])).
% 183.04/26.91 thf(zip_derived_cl115, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ( (nat_fails @ X0) | ((X0) = (0)) | ~ (nat_fails @ (sk__28 @ X0)))),
% 183.04/26.91 inference('cnf', [status(esa)], [id28])).
% 183.04/26.91 thf(zip_derived_cl11945, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (~ (nat_fails @ X0)
% 183.04/26.91 | (nat_fails @ (s @ X0))
% 183.04/26.91 | ((s @ X0) = (0))
% 183.04/26.91 | (nat_fails @ (s @ X0)))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl8129, zip_derived_cl115])).
% 183.04/26.91 thf(zip_derived_cl11982, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((s @ X0) = (0)) | (nat_fails @ (s @ X0)) | ~ (nat_fails @ X0))),
% 183.04/26.91 inference('simplify', [status(thm)], [zip_derived_cl11945])).
% 183.04/26.91 thf(zip_derived_cl0, plain, (![X0 : $i]: ((0) != (s @ X0))),
% 183.04/26.91 inference('cnf', [status(esa)], [id1])).
% 183.04/26.91 thf(zip_derived_cl11983, plain,
% 183.04/26.91 (![X0 : $i]: ( (nat_fails @ (s @ X0)) | ~ (nat_fails @ X0))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl11982, zip_derived_cl0])).
% 183.04/26.91 thf(id13, axiom,
% 183.04/26.91 (![Xx17:$i]: ( ~( ( nat_succeeds @ Xx17 ) & ( nat_fails @ Xx17 ) ) ))).
% 183.04/26.91 thf(zip_derived_cl13, plain,
% 183.04/26.91 (![X0 : $i]: (~ (nat_succeeds @ X0) | ~ (nat_fails @ X0))),
% 183.04/26.91 inference('cnf', [status(esa)], [id13])).
% 183.04/26.91 thf(zip_derived_cl11994, plain,
% 183.04/26.91 (![X0 : $i]: (~ (nat_fails @ X0) | ~ (nat_succeeds @ (s @ X0)))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl11983, zip_derived_cl13])).
% 183.04/26.91 thf(zip_derived_cl11983, plain,
% 183.04/26.91 (![X0 : $i]: ( (nat_fails @ (s @ X0)) | ~ (nat_fails @ X0))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl11982, zip_derived_cl0])).
% 183.04/26.91 thf(zip_derived_cl12044, plain,
% 183.04/26.91 (![X0 : $i]: (~ (nat_succeeds @ (s @ (s @ X0))) | ~ (nat_fails @ X0))),
% 183.04/26.91 inference('sup+', [status(thm)],
% 183.04/26.91 [zip_derived_cl11994, zip_derived_cl11983])).
% 183.04/26.91 thf(zip_derived_cl91417, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ( (nat_succeeds @ X0)
% 183.04/26.91 | ((sk__34) != (X0))
% 183.04/26.91 | ~ (nat_succeeds @ (s @ (s @ X0))))),
% 183.04/26.91 inference('sup-', [status(thm)],
% 183.04/26.91 [zip_derived_cl91412, zip_derived_cl12044])).
% 183.04/26.91 thf(zip_derived_cl91971, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((sk__31) = (0))
% 183.04/26.91 | ((s @ (s @ X0)) != (s @ (s @ sk__34)))
% 183.04/26.91 | ((sk__34) != (X0))
% 183.04/26.91 | (nat_succeeds @ X0))),
% 183.04/26.91 inference('sup-', [status(thm)],
% 183.04/26.91 [zip_derived_cl35660, zip_derived_cl91417])).
% 183.04/26.91 thf(zip_derived_cl37790, plain, (((sk__31) != (0))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl37789, zip_derived_cl968])).
% 183.04/26.91 thf(zip_derived_cl92047, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((s @ (s @ X0)) != (s @ (s @ sk__34)))
% 183.04/26.91 | ((sk__34) != (X0))
% 183.04/26.91 | (nat_succeeds @ X0))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl91971, zip_derived_cl37790])).
% 183.04/26.91 thf(zip_derived_cl92745, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (~ (nat_succeeds @ X1)
% 183.04/26.91 | (nat_succeeds @ X0)
% 183.04/26.91 | ((sk__34) != ('@+' @ X1 @ X0))
% 183.04/26.91 | ((s @ (s @ ('@+' @ X1 @ X0))) != (s @ (s @ sk__34))))),
% 183.04/26.91 inference('sup+', [status(thm)],
% 183.04/26.91 [zip_derived_cl2065, zip_derived_cl92047])).
% 183.04/26.91 thf(zip_derived_cl92844, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (~ (nat_succeeds @ X1)
% 183.04/26.91 | (nat_succeeds @ X0)
% 183.04/26.91 | ((sk__34) != ('@+' @ X1 @ X0))
% 183.04/26.91 | ((s @ (s @ sk__34)) != (s @ (s @ sk__34))))),
% 183.04/26.91 inference('local_rewriting', [status(thm)], [zip_derived_cl92745])).
% 183.04/26.91 thf(zip_derived_cl92845, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (((sk__34) != ('@+' @ X1 @ X0))
% 183.04/26.91 | (nat_succeeds @ X0)
% 183.04/26.91 | ~ (nat_succeeds @ X1))),
% 183.04/26.91 inference('simplify', [status(thm)], [zip_derived_cl92844])).
% 183.04/26.91 thf(zip_derived_cl99011, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((sk__34) != (X0)) | ~ (nat_succeeds @ 0) | (nat_succeeds @ X0))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl136, zip_derived_cl92845])).
% 183.04/26.91 thf(zip_derived_cl150, plain, ( (nat_succeeds @ sk__35)),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf('lemma-(plus:zero)', axiom,
% 183.04/26.91 (![Xx:$i]: ( ( nat_succeeds @ Xx ) => ( ( '@+' @ Xx @ 0 ) = ( Xx ) ) ))).
% 183.04/26.91 thf(zip_derived_cl140, plain,
% 183.04/26.91 (![X0 : $i]: ((('@+' @ X0 @ 0) = (X0)) | ~ (nat_succeeds @ X0))),
% 183.04/26.91 inference('cnf', [status(esa)], [lemma-(plus:zero)])).
% 183.04/26.91 thf(zip_derived_cl1698, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 ((('@+' @ X2 @ X1) != (X0))
% 183.04/26.91 | ~ (nat_succeeds @ X2)
% 183.04/26.91 | ~ (nat_succeeds @ X0)
% 183.04/26.91 | (nat_succeeds @ X1))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl120, zip_derived_cl129])).
% 183.04/26.91 thf(zip_derived_cl2059, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (((X0) != (X1))
% 183.04/26.91 | ~ (nat_succeeds @ X0)
% 183.04/26.91 | (nat_succeeds @ 0)
% 183.04/26.91 | ~ (nat_succeeds @ X1)
% 183.04/26.91 | ~ (nat_succeeds @ X0))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl140, zip_derived_cl1698])).
% 183.04/26.91 thf(zip_derived_cl2068, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (~ (nat_succeeds @ X1)
% 183.04/26.91 | (nat_succeeds @ 0)
% 183.04/26.91 | ~ (nat_succeeds @ X0)
% 183.04/26.91 | ((X0) != (X1)))),
% 183.04/26.91 inference('simplify', [status(thm)], [zip_derived_cl2059])).
% 183.04/26.91 thf(zip_derived_cl2247, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (~ (nat_succeeds @ X0) | (nat_succeeds @ 0) | ~ (nat_succeeds @ X0))),
% 183.04/26.91 inference('eq_res', [status(thm)], [zip_derived_cl2068])).
% 183.04/26.91 thf(zip_derived_cl2248, plain,
% 183.04/26.91 (![X0 : $i]: ( (nat_succeeds @ 0) | ~ (nat_succeeds @ X0))),
% 183.04/26.91 inference('simplify', [status(thm)], [zip_derived_cl2247])).
% 183.04/26.91 thf(zip_derived_cl2300, plain, ( (nat_succeeds @ 0)),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl150, zip_derived_cl2248])).
% 183.04/26.91 thf(zip_derived_cl99034, plain,
% 183.04/26.91 (![X0 : $i]: (((sk__34) != (X0)) | (nat_succeeds @ X0))),
% 183.04/26.91 inference('demod', [status(thm)],
% 183.04/26.91 [zip_derived_cl99011, zip_derived_cl2300])).
% 183.04/26.91 thf(zip_derived_cl110, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 ( (nat_succeeds @ X0) | ~ (nat_succeeds @ X1) | ((X0) != (s @ X1)))),
% 183.04/26.91 inference('cnf', [status(esa)], [id27])).
% 183.04/26.91 thf(zip_derived_cl99048, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (((sk__34) != (X0)) | ((X1) != (s @ X0)) | (nat_succeeds @ X1))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl99034, zip_derived_cl110])).
% 183.04/26.91 thf(zip_derived_cl99326, plain,
% 183.04/26.91 (![X0 : $i]: ( (nat_succeeds @ (s @ X0)) | ((sk__34) != (X0)))),
% 183.04/26.91 inference('eq_res', [status(thm)], [zip_derived_cl99048])).
% 183.04/26.91 thf(zip_derived_cl120487, plain,
% 183.04/26.91 (( (nat_succeeds @ sk__31) | ((sk__34) != (sk__34)))),
% 183.04/26.91 inference('sup+', [status(thm)],
% 183.04/26.91 [zip_derived_cl120142, zip_derived_cl99326])).
% 183.04/26.91 thf(zip_derived_cl120618, plain, ( (nat_succeeds @ sk__31)),
% 183.04/26.91 inference('simplify', [status(thm)], [zip_derived_cl120487])).
% 183.04/26.91 thf(zip_derived_cl125083, plain, (((sk__34) = (sk__27 @ sk__31))),
% 183.04/26.91 inference('demod', [status(thm)],
% 183.04/26.91 [zip_derived_cl120576, zip_derived_cl120618])).
% 183.04/26.91 thf(zip_derived_cl108, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((X0) = (0)) | ((X0) = (s @ (sk__27 @ X0))) | ~ (nat_succeeds @ X0))),
% 183.04/26.91 inference('cnf', [status(esa)], [id27])).
% 183.04/26.91 thf('corollary-(plus:successor)', axiom,
% 183.04/26.91 (![Xx:$i,Xy:$i]:
% 183.04/26.91 ( ( nat_succeeds @ Xx ) =>
% 183.04/26.91 ( ( '@+' @ ( s @ Xx ) @ Xy ) = ( s @ ( '@+' @ Xx @ Xy ) ) ) ))).
% 183.04/26.91 thf(zip_derived_cl137, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (~ (nat_succeeds @ X0)
% 183.04/26.91 | (('@+' @ (s @ X0) @ X1) = (s @ ('@+' @ X0 @ X1))))),
% 183.04/26.91 inference('cnf', [status(esa)], [corollary-(plus:successor)])).
% 183.04/26.91 thf(zip_derived_cl1889, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 ((('@+' @ X0 @ X1) = (s @ ('@+' @ (sk__27 @ X0) @ X1)))
% 183.04/26.91 | ~ (nat_succeeds @ X0)
% 183.04/26.91 | ((X0) = (0))
% 183.04/26.91 | ~ (nat_succeeds @ (sk__27 @ X0)))),
% 183.04/26.91 inference('sup+', [status(thm)], [zip_derived_cl108, zip_derived_cl137])).
% 183.04/26.91 thf(zip_derived_cl109, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((X0) = (0))
% 183.04/26.91 | (nat_succeeds @ (sk__27 @ X0))
% 183.04/26.91 | ~ (nat_succeeds @ X0))),
% 183.04/26.91 inference('cnf', [status(esa)], [id27])).
% 183.04/26.91 thf(zip_derived_cl90055, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (((X0) = (0))
% 183.04/26.91 | ~ (nat_succeeds @ X0)
% 183.04/26.91 | (('@+' @ X0 @ X1) = (s @ ('@+' @ (sk__27 @ X0) @ X1))))),
% 183.04/26.91 inference('clc', [status(thm)], [zip_derived_cl1889, zip_derived_cl109])).
% 183.04/26.91 thf(zip_derived_cl125092, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ((('@+' @ sk__31 @ X0) = (s @ ('@+' @ sk__34 @ X0)))
% 183.04/26.91 | ~ (nat_succeeds @ sk__31)
% 183.04/26.91 | ((sk__31) = (0)))),
% 183.04/26.91 inference('sup+', [status(thm)],
% 183.04/26.91 [zip_derived_cl125083, zip_derived_cl90055])).
% 183.04/26.91 thf(zip_derived_cl120618, plain, ( (nat_succeeds @ sk__31)),
% 183.04/26.91 inference('simplify', [status(thm)], [zip_derived_cl120487])).
% 183.04/26.91 thf(zip_derived_cl125108, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ((('@+' @ sk__31 @ X0) = (s @ ('@+' @ sk__34 @ X0)))
% 183.04/26.91 | ((sk__31) = (0)))),
% 183.04/26.91 inference('demod', [status(thm)],
% 183.04/26.91 [zip_derived_cl125092, zip_derived_cl120618])).
% 183.04/26.91 thf(zip_derived_cl37790, plain, (((sk__31) != (0))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl37789, zip_derived_cl968])).
% 183.04/26.91 thf(zip_derived_cl125109, plain,
% 183.04/26.91 (![X0 : $i]: (('@+' @ sk__31 @ X0) = (s @ ('@+' @ sk__34 @ X0)))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl125108, zip_derived_cl37790])).
% 183.04/26.91 thf(zip_derived_cl37728, plain,
% 183.04/26.91 ((('@+' @ sk__31 @ sk__32) = ('@+' @ sk__31 @ sk__33))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl37727, zip_derived_cl148])).
% 183.04/26.91 thf(zip_derived_cl125109, plain,
% 183.04/26.91 (![X0 : $i]: (('@+' @ sk__31 @ X0) = (s @ ('@+' @ sk__34 @ X0)))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl125108, zip_derived_cl37790])).
% 183.04/26.91 thf(zip_derived_cl1, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]: (((X1) = (X0)) | ((s @ X1) != (s @ X0)))),
% 183.04/26.91 inference('cnf', [status(esa)], [id2])).
% 183.04/26.91 thf(zip_derived_cl143576, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (((s @ X1) != ('@+' @ sk__31 @ X0)) | ((X1) = ('@+' @ sk__34 @ X0)))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl125109, zip_derived_cl1])).
% 183.04/26.91 thf(zip_derived_cl145825, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((s @ X0) != ('@+' @ sk__31 @ sk__32))
% 183.04/26.91 | ((X0) = ('@+' @ sk__34 @ sk__33)))),
% 183.04/26.91 inference('sup-', [status(thm)],
% 183.04/26.91 [zip_derived_cl37728, zip_derived_cl143576])).
% 183.04/26.91 thf(zip_derived_cl146642, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 ((('@+' @ sk__31 @ X0) != ('@+' @ sk__31 @ sk__32))
% 183.04/26.91 | (('@+' @ sk__34 @ X0) = ('@+' @ sk__34 @ sk__33)))),
% 183.04/26.91 inference('sup-', [status(thm)],
% 183.04/26.91 [zip_derived_cl125109, zip_derived_cl145825])).
% 183.04/26.91 thf(zip_derived_cl149, plain,
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) = ('@+' @ sk__35 @ sk__37))),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(zip_derived_cl147, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 183.04/26.91 (~ (nat_succeeds @ X0)
% 183.04/26.91 | ((X2) = (X1))
% 183.04/26.91 | (('@+' @ X0 @ X2) != ('@+' @ X0 @ X1))
% 183.04/26.91 | (('@+' @ sk__34 @ X4) != ('@+' @ sk__34 @ X3))
% 183.04/26.91 | ((X4) = (X3))
% 183.04/26.91 | ((sk__31) = (0)))),
% 183.04/26.91 inference('cnf', [status(esa)], [induction])).
% 183.04/26.91 thf(zip_derived_cl2257, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) != ('@+' @ sk__35 @ X0))
% 183.04/26.91 | ((sk__31) = (0))
% 183.04/26.91 | ((X1) = (X2))
% 183.04/26.91 | (('@+' @ sk__34 @ X1) != ('@+' @ sk__34 @ X2))
% 183.04/26.91 | ((sk__37) = (X0))
% 183.04/26.91 | ~ (nat_succeeds @ sk__35))),
% 183.04/26.91 inference('sup-', [status(thm)], [zip_derived_cl149, zip_derived_cl147])).
% 183.04/26.91 thf(zip_derived_cl150, plain, ( (nat_succeeds @ sk__35)),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(zip_derived_cl2272, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) != ('@+' @ sk__35 @ X0))
% 183.04/26.91 | ((sk__31) = (0))
% 183.04/26.91 | ((X1) = (X2))
% 183.04/26.91 | (('@+' @ sk__34 @ X1) != ('@+' @ sk__34 @ X2))
% 183.04/26.91 | ((sk__37) = (X0)))),
% 183.04/26.91 inference('demod', [status(thm)], [zip_derived_cl2257, zip_derived_cl150])).
% 183.04/26.91 thf(zip_derived_cl37790, plain, (((sk__31) != (0))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl37789, zip_derived_cl968])).
% 183.04/26.91 thf(zip_derived_cl125770, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 183.04/26.91 ((('@+' @ sk__35 @ sk__36) != ('@+' @ sk__35 @ X0))
% 183.04/26.91 | ((X1) = (X2))
% 183.04/26.91 | (('@+' @ sk__34 @ X1) != ('@+' @ sk__34 @ X2))
% 183.04/26.91 | ((sk__37) = (X0)))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl2272, zip_derived_cl37790])).
% 183.04/26.91 thf(zip_derived_cl125789, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 (((sk__37) = (sk__36))
% 183.04/26.91 | (('@+' @ sk__34 @ X0) != ('@+' @ sk__34 @ X1))
% 183.04/26.91 | ((X0) = (X1)))),
% 183.04/26.91 inference('eq_res', [status(thm)], [zip_derived_cl125770])).
% 183.04/26.91 thf(zip_derived_cl148, plain, (((sk__36) != (sk__37))),
% 183.04/26.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 183.04/26.91 thf(zip_derived_cl125790, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 ((('@+' @ sk__34 @ X0) != ('@+' @ sk__34 @ X1)) | ((X0) = (X1)))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl125789, zip_derived_cl148])).
% 183.04/26.91 thf(zip_derived_cl215249, plain,
% 183.04/26.91 (![X0 : $i, X1 : $i]:
% 183.04/26.91 ((('@+' @ sk__34 @ X1) != ('@+' @ sk__34 @ X0))
% 183.04/26.91 | (('@+' @ sk__31 @ X0) != ('@+' @ sk__31 @ sk__32))
% 183.04/26.91 | ((X1) = (sk__33)))),
% 183.04/26.91 inference('sup-', [status(thm)],
% 183.04/26.91 [zip_derived_cl146642, zip_derived_cl125790])).
% 183.04/26.91 thf(zip_derived_cl225967, plain,
% 183.04/26.91 (![X0 : $i]:
% 183.04/26.91 (((X0) = (sk__33))
% 183.04/26.91 | (('@+' @ sk__31 @ X0) != ('@+' @ sk__31 @ sk__32)))),
% 183.04/26.91 inference('eq_res', [status(thm)], [zip_derived_cl215249])).
% 183.04/26.91 thf(zip_derived_cl226030, plain, (((sk__32) = (sk__33))),
% 183.04/26.91 inference('eq_res', [status(thm)], [zip_derived_cl225967])).
% 183.04/26.91 thf(zip_derived_cl968, plain, (((sk__32) != (sk__33))),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl967, zip_derived_cl148])).
% 183.04/26.91 thf(zip_derived_cl226031, plain, ($false),
% 183.04/26.91 inference('simplify_reflect-', [status(thm)],
% 183.04/26.91 [zip_derived_cl226030, zip_derived_cl968])).
% 183.04/26.91
% 183.04/26.91 % SZS output end Refutation
% 183.04/26.91
% 183.04/26.91
% 183.04/26.91 % Terminating...
% 183.04/26.97 % Runner terminated.
% 183.04/26.98 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------