%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SYO672-1 : TPTP v9.2.0. Released v7.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.jRBWXrHxjh 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:08:07 PM UTC 2025
% Result : Unsatisfiable 6.72s 1.54s
% Output : Refutation 6.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYO672-1 : TPTP v9.2.0. Released v7.3.0.
% 0.03/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.jRBWXrHxjh true
% 0.13/0.34 % Computer : n019.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 1 18:05:53 EDT 2025
% 0.13/0.35 % CPUTime :
% 0.13/0.35 % Running portfolio for 300 s
% 0.13/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.35 % Number of cores: 8
% 0.13/0.35 % Python version: Python 3.6.8
% 0.13/0.35 % Running in FO mode
% 0.57/0.64 % Total configuration time : 435
% 0.57/0.64 % Estimated wc time : 1092
% 0.57/0.64 % Estimated cpu time (7 cpus) : 156.0
% 0.57/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.57/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.57/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.57/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.57/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.58/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.58/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 0.58/0.78 % /export/starexec/sandbox2/solver/bin/fo/fo17_bce.sh running for 50s
% 0.58/0.81 % /export/starexec/sandbox2/solver/bin/fo/fo8.sh running for 50s
% 6.72/1.54 % Solved by fo/fo5.sh.
% 6.72/1.54 % done 390 iterations in 0.742s
% 6.72/1.54 % SZS status Unsatisfiable for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 6.72/1.54 % SZS output start Refutation
% 6.72/1.54 thf(f_type, type, f: $i > $i).
% 6.72/1.54 thf(0_type, type, 0: $i).
% 6.72/1.54 thf(suc_type, type, suc: $i > $i).
% 6.72/1.54 thf(z_type, type, z: $i).
% 6.72/1.54 thf(s_type, type, s: $i > $i).
% 6.72/1.54 thf(E_type, type, E: $i > $i > $o).
% 6.72/1.54 thf(iLEQ_type, type, iLEQ: $i > $i > $o).
% 6.72/1.54 thf(LE_type, type, LE: $i > $i > $o).
% 6.72/1.54 thf(clause_1160, axiom, (~( LE @ ( f @ z ) @ 0 ))).
% 6.72/1.54 thf(zip_derived_cl64, plain, (~ (LE @ (f @ z) @ 0)),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_1160])).
% 6.72/1.54 thf(clause_994, axiom,
% 6.72/1.54 (( ~( LE @ ( f @ ( suc @ ( suc @ ( suc @ B_35 ) ) ) ) @ ( s @ 0 ) ) ) |
% 6.72/1.54 ( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ B_35 ) ) ) ) ) |
% 6.72/1.54 ( LE @ ( f @ B_35 ) @ 0 ))).
% 6.72/1.54 thf(zip_derived_cl49, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (LE @ (f @ (suc @ (suc @ (suc @ X0)))) @ (s @ 0))
% 6.72/1.54 | (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | (LE @ (f @ X0) @ 0))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_994])).
% 6.72/1.54 thf(clause_1642, axiom,
% 6.72/1.54 (( ~( LE @ ( f @ ( suc @ ( suc @ ( suc @ B_28 ) ) ) ) @ ( s @ ( s @ 0 ) ) ) ) |
% 6.72/1.54 ( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ ( suc @ B_28 ) ) ) ) ) |
% 6.72/1.54 ( LE @ ( f @ B_28 ) @ ( s @ 0 ) ))).
% 6.72/1.54 thf(zip_derived_cl77, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (LE @ (f @ (suc @ (suc @ (suc @ X0)))) @ (s @ (s @ 0)))
% 6.72/1.54 | (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ 0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_1642])).
% 6.72/1.54 thf(clause_921, axiom,
% 6.72/1.54 (( ~( LE @
% 6.72/1.54 ( f @ ( suc @ ( suc @ ( suc @ B_16 ) ) ) ) @
% 6.72/1.54 ( s @ ( s @ ( s @ 0 ) ) ) ) ) |
% 6.72/1.54 ( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ ( suc @ B_16 ) ) ) ) ) |
% 6.72/1.54 ( LE @ ( f @ B_16 ) @ ( s @ ( s @ 0 ) ) ))).
% 6.72/1.54 thf(zip_derived_cl45, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (LE @ (f @ (suc @ (suc @ (suc @ X0)))) @ (s @ (s @ (s @ 0))))
% 6.72/1.54 | (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_921])).
% 6.72/1.54 thf(clause_2366, axiom, (LE @ ( f @ A ) @ ( s @ ( s @ ( s @ 0 ) ) ))).
% 6.72/1.54 thf(zip_derived_cl91, plain,
% 6.72/1.54 (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ (s @ 0))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_2366])).
% 6.72/1.54 thf(zip_derived_cl119, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 6.72/1.54 inference('demod', [status(thm)], [zip_derived_cl45, zip_derived_cl91])).
% 6.72/1.54 thf(clause_2086, axiom,
% 6.72/1.54 (( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ A_1 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ B_17 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ B_17 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ B_18 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ B_17 ) @ ( suc @ B_18 ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_17 ) @ ( f @ ( suc @ ( suc @ B_17 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ B_18 ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_18 ) @ ( f @ ( suc @ B_18 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_18 ) @ ( f @ ( suc @ ( suc @ B_18 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ ( suc @ B_18 ) ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ ( suc @ B_17 ) ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_17 ) @ ( f @ ( suc @ B_17 ) ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ A_1 ) @ ( suc @ B_17 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ B_18 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ B_17 ) ) ) ) ))).
% 6.72/1.54 thf(zip_derived_cl71, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i, X2 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X1))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X2))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X2))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X2))
% 6.72/1.54 | ~ (E @ (f @ X2) @ (f @ (suc @ X2)))
% 6.72/1.54 | ~ (E @ (f @ X2) @ (f @ (suc @ (suc @ X2))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X2)))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X2)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X1)))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_2086])).
% 6.72/1.54 thf(zip_derived_cl862, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X1))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0)))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl71])).
% 6.72/1.54 thf(zip_derived_cl864, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X1))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X1)))))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl862])).
% 6.72/1.54 thf(zip_derived_cl1348, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl864])).
% 6.72/1.54 thf(zip_derived_cl1349, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl1348])).
% 6.72/1.54 thf(clause_1941, axiom,
% 6.72/1.54 (( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ A_1 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ B_17 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ B_17 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ B_18 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ B_17 ) @ ( suc @ B_18 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ B_18 ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_18 ) @ ( f @ ( suc @ B_18 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_17 ) @ ( f @ ( suc @ B_17 ) ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ A_1 ) @ ( suc @ B_17 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ B_18 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ B_17 ) ) ) ) ) |
% 6.72/1.54 ( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) |
% 6.72/1.54 ( E @ ( f @ B_17 ) @ ( f @ ( suc @ ( suc @ B_17 ) ) ) ) |
% 6.72/1.54 ( E @ ( f @ B_18 ) @ ( f @ ( suc @ ( suc @ B_18 ) ) ) ))).
% 6.72/1.54 thf(zip_derived_cl57, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i, X2 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X1))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X2))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X2))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X2))
% 6.72/1.54 | ~ (E @ (f @ X2) @ (f @ (suc @ X2)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X2)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | (E @ (f @ X2) @ (f @ (suc @ (suc @ X2)))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_1941])).
% 6.72/1.54 thf(zip_derived_cl751, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X1))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0)))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl57])).
% 6.72/1.54 thf(zip_derived_cl753, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X1))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl751])).
% 6.72/1.54 thf(zip_derived_cl1262, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl753])).
% 6.72/1.54 thf(zip_derived_cl1263, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl1262])).
% 6.72/1.54 thf(clause_1761, axiom,
% 6.72/1.54 (( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ A_1 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ B_17 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ B_17 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ B_17 ) @ ( suc @ B_18 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ B_18 ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ A_1 ) @ ( suc @ B_17 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ B_18 ) ) ) ) |
% 6.72/1.54 ( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) |
% 6.72/1.54 ( E @ ( f @ B_17 ) @ ( f @ ( suc @ B_17 ) ) ) |
% 6.72/1.54 ( E @ ( f @ B_18 ) @ ( f @ ( suc @ B_18 ) ) ))).
% 6.72/1.54 thf(zip_derived_cl61, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i, X2 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X1))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X2))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X2))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X2)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | (E @ (f @ X2) @ (f @ (suc @ X2))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_1761])).
% 6.72/1.54 thf(zip_derived_cl211, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 ( (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X1))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0)))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl61])).
% 6.72/1.54 thf(zip_derived_cl213, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X1))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X1)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ X1))))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl211])).
% 6.72/1.54 thf(clause_179, axiom,
% 6.72/1.54 (( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ A_1 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 6.72/1.54 ( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) |
% 6.72/1.54 ( iLEQ @ ( suc @ A_1 ) @ ( suc @ A_1 ) ))).
% 6.72/1.54 thf(zip_derived_cl90, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_179])).
% 6.72/1.54 thf(zip_derived_cl359, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 ( (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X1))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl213, zip_derived_cl90])).
% 6.72/1.54 thf(zip_derived_cl364, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl359])).
% 6.72/1.54 thf(zip_derived_cl365, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0)))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl364])).
% 6.72/1.54 thf(zip_derived_cl90, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_179])).
% 6.72/1.54 thf(zip_derived_cl366, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl365, zip_derived_cl90])).
% 6.72/1.54 thf(zip_derived_cl1264, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1263, zip_derived_cl366])).
% 6.72/1.54 thf(clause_2026, axiom,
% 6.72/1.54 (( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ A_1 ) ) ) |
% 6.72/1.54 ( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) |
% 6.72/1.54 ( iLEQ @ ( suc @ A_1 ) @ ( suc @ A_1 ) ))).
% 6.72/1.54 thf(zip_derived_cl68, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_2026])).
% 6.72/1.54 thf(zip_derived_cl90, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_179])).
% 6.72/1.54 thf(zip_derived_cl156, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl68, zip_derived_cl90])).
% 6.72/1.54 thf(zip_derived_cl1265, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1264, zip_derived_cl156])).
% 6.72/1.54 thf(zip_derived_cl1350, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1349, zip_derived_cl1265])).
% 6.72/1.54 thf(clause_2162, axiom,
% 6.72/1.54 (( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ A_1 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 6.72/1.54 ( iLEQ @ ( suc @ A_1 ) @ ( suc @ A_1 ) ))).
% 6.72/1.54 thf(zip_derived_cl14, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_2162])).
% 6.72/1.54 thf(zip_derived_cl156, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl68, zip_derived_cl90])).
% 6.72/1.54 thf(zip_derived_cl163, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl14, zip_derived_cl156])).
% 6.72/1.54 thf(zip_derived_cl90, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_179])).
% 6.72/1.54 thf(zip_derived_cl164, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl163, zip_derived_cl90])).
% 6.72/1.54 thf(zip_derived_cl1351, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1350, zip_derived_cl164])).
% 6.72/1.54 thf(zip_derived_cl366, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl365, zip_derived_cl90])).
% 6.72/1.54 thf(zip_derived_cl1352, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1351, zip_derived_cl366])).
% 6.72/1.54 thf(zip_derived_cl1356, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (LE @ (f @ X0) @ (s @ (s @ 0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('sup-', [status(thm)], [zip_derived_cl119, zip_derived_cl1352])).
% 6.72/1.54 thf(clause_1449, axiom,
% 6.72/1.54 (( ~( LE @ ( f @ B_16 ) @ ( s @ ( s @ ( s @ 0 ) ) ) ) ) |
% 6.72/1.54 ( E @ ( s @ ( s @ 0 ) ) @ ( f @ B_16 ) ) |
% 6.72/1.54 ( LE @ ( f @ B_16 ) @ ( s @ ( s @ 0 ) ) ))).
% 6.72/1.54 thf(zip_derived_cl36, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (LE @ (f @ X0) @ (s @ (s @ (s @ 0))))
% 6.72/1.54 | (E @ (s @ (s @ 0)) @ (f @ X0))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_1449])).
% 6.72/1.54 thf(zip_derived_cl91, plain,
% 6.72/1.54 (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ (s @ 0))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_2366])).
% 6.72/1.54 thf(zip_derived_cl104, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (s @ (s @ 0)) @ (f @ X0)) | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 6.72/1.54 inference('demod', [status(thm)], [zip_derived_cl36, zip_derived_cl91])).
% 6.72/1.54 thf(zip_derived_cl1357, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1356, zip_derived_cl104])).
% 6.72/1.54 thf(clause_1175, axiom,
% 6.72/1.54 (( ~( LE @ ( f @ ( suc @ ( suc @ B_16 ) ) ) @ ( s @ ( s @ ( s @ 0 ) ) ) ) ) |
% 6.72/1.54 ( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ B_16 ) ) ) ) |
% 6.72/1.54 ( LE @ ( f @ B_16 ) @ ( s @ ( s @ 0 ) ) ))).
% 6.72/1.54 thf(zip_derived_cl25, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (LE @ (f @ (suc @ (suc @ X0))) @ (s @ (s @ (s @ 0))))
% 6.72/1.54 | (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_1175])).
% 6.72/1.54 thf(zip_derived_cl91, plain,
% 6.72/1.54 (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ (s @ 0))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_2366])).
% 6.72/1.54 thf(zip_derived_cl116, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 6.72/1.54 inference('demod', [status(thm)], [zip_derived_cl25, zip_derived_cl91])).
% 6.72/1.54 thf(zip_derived_cl1358, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (LE @ (f @ X0) @ (s @ (s @ 0)))
% 6.72/1.54 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1357, zip_derived_cl116])).
% 6.72/1.54 thf(clause_1030, axiom,
% 6.72/1.54 (( ~( LE @ ( f @ ( suc @ B_16 ) ) @ ( s @ ( s @ ( s @ 0 ) ) ) ) ) |
% 6.72/1.54 ( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ B_16 ) ) ) |
% 6.72/1.54 ( LE @ ( f @ B_16 ) @ ( s @ ( s @ 0 ) ) ))).
% 6.72/1.54 thf(zip_derived_cl100, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (LE @ (f @ (suc @ X0)) @ (s @ (s @ (s @ 0))))
% 6.72/1.54 | (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_1030])).
% 6.72/1.54 thf(zip_derived_cl91, plain,
% 6.72/1.54 (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ (s @ 0))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_2366])).
% 6.72/1.54 thf(zip_derived_cl113, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 6.72/1.54 inference('demod', [status(thm)], [zip_derived_cl100, zip_derived_cl91])).
% 6.72/1.54 thf(zip_derived_cl1359, plain,
% 6.72/1.54 (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ 0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1358, zip_derived_cl113])).
% 6.72/1.54 thf(zip_derived_cl1362, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ 0)))),
% 6.72/1.54 inference('demod', [status(thm)], [zip_derived_cl77, zip_derived_cl1359])).
% 6.72/1.54 thf(clause_299, axiom,
% 6.72/1.54 (( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ ( suc @ B_29 ) ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ B_30 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ B_30 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_30 ) @ ( f @ ( suc @ ( suc @ B_30 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_29 ) @ ( f @ ( suc @ ( suc @ B_29 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ ( suc @ B_30 ) ) ) ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ A_2 ) @ ( suc @ B_29 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ B_29 ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ B_29 ) @ ( suc @ B_30 ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_29 ) @ ( f @ ( suc @ B_29 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ B_29 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ B_29 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_2 ) ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_30 ) @ ( f @ ( suc @ B_30 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ A_2 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ B_30 ) ) ) ) ))).
% 6.72/1.54 thf(zip_derived_cl46, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i, X2 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X1))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (f @ X2) @ (f @ (suc @ (suc @ X2))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X2)))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X2) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X2))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X2)))))
% 6.72/1.54 | ~ (E @ (f @ X2) @ (f @ (suc @ X2)))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X2))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X1)))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_299])).
% 6.72/1.54 thf(zip_derived_cl777, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X1))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0)))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl46])).
% 6.72/1.54 thf(zip_derived_cl779, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 (~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X1))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl777])).
% 6.72/1.54 thf(zip_derived_cl1057, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl779])).
% 6.72/1.54 thf(zip_derived_cl1058, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl1057])).
% 6.72/1.54 thf(clause_939, axiom,
% 6.72/1.54 (( ~( E @ ( s @ 0 ) @ ( f @ B_30 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ B_30 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ A_2 ) @ ( suc @ B_29 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ B_29 ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ B_29 ) @ ( suc @ B_30 ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_29 ) @ ( f @ ( suc @ B_29 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ B_29 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ B_29 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_30 ) @ ( f @ ( suc @ B_30 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ A_2 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ B_30 ) ) ) ) ) |
% 6.72/1.54 ( E @ ( f @ A_2 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) |
% 6.72/1.54 ( E @ ( f @ B_29 ) @ ( f @ ( suc @ ( suc @ B_29 ) ) ) ) |
% 6.72/1.54 ( E @ ( f @ B_30 ) @ ( f @ ( suc @ ( suc @ B_30 ) ) ) ))).
% 6.72/1.54 thf(zip_derived_cl28, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i, X2 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X2))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X2))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X2) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (f @ X2) @ (f @ (suc @ X2)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X2))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X2)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X1))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | (E @ (f @ X2) @ (f @ (suc @ (suc @ X2))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_939])).
% 6.72/1.54 thf(zip_derived_cl693, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 ( (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X1)))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl28])).
% 6.72/1.54 thf(zip_derived_cl695, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ X1))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ (suc @ X1)))))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl693])).
% 6.72/1.54 thf(zip_derived_cl930, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0)))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl695])).
% 6.72/1.54 thf(zip_derived_cl931, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl930])).
% 6.72/1.54 thf(clause_593, axiom,
% 6.72/1.54 (( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ A_2 ) ) ) |
% 6.72/1.54 ( E @ ( f @ A_2 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) |
% 6.72/1.54 ( iLEQ @ ( suc @ A_2 ) @ ( suc @ A_2 ) ))).
% 6.72/1.54 thf(zip_derived_cl72, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_593])).
% 6.72/1.54 thf(clause_362, axiom,
% 6.72/1.54 (( ~( E @ ( s @ 0 ) @ ( f @ A_2 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 6.72/1.54 ( E @ ( f @ A_2 ) @ ( f @ ( suc @ A_2 ) ) ) |
% 6.72/1.54 ( iLEQ @ ( suc @ A_2 ) @ ( suc @ A_2 ) ))).
% 6.72/1.54 thf(zip_derived_cl51, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_362])).
% 6.72/1.54 thf(zip_derived_cl123, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl72, zip_derived_cl51])).
% 6.72/1.54 thf(zip_derived_cl932, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl931, zip_derived_cl123])).
% 6.72/1.54 thf(clause_1935, axiom,
% 6.72/1.54 (( ~( E @ ( s @ 0 ) @ ( f @ B_30 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ B_30 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ A_2 ) @ ( suc @ B_29 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ B_29 ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ B_29 ) @ ( suc @ B_30 ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ B_29 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ A_2 ) ) ) |
% 6.72/1.54 ( E @ ( f @ A_2 ) @ ( f @ ( suc @ A_2 ) ) ) |
% 6.72/1.54 ( E @ ( f @ B_29 ) @ ( f @ ( suc @ B_29 ) ) ) |
% 6.72/1.54 ( E @ ( f @ B_30 ) @ ( f @ ( suc @ B_30 ) ) ))).
% 6.72/1.54 thf(zip_derived_cl4, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i, X2 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X2))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X2))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X2) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X2)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X1))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | (E @ (f @ X2) @ (f @ (suc @ X2)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_1935])).
% 6.72/1.54 thf(zip_derived_cl173, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 ( (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X1))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0)))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl4])).
% 6.72/1.54 thf(zip_derived_cl175, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X1))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl173])).
% 6.72/1.54 thf(zip_derived_cl306, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl175])).
% 6.72/1.54 thf(zip_derived_cl307, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl306])).
% 6.72/1.54 thf(zip_derived_cl51, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_362])).
% 6.72/1.54 thf(zip_derived_cl308, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl307, zip_derived_cl51])).
% 6.72/1.54 thf(zip_derived_cl933, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl932, zip_derived_cl308])).
% 6.72/1.54 thf(zip_derived_cl1059, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1058, zip_derived_cl933])).
% 6.72/1.54 thf(zip_derived_cl308, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl307, zip_derived_cl51])).
% 6.72/1.54 thf(zip_derived_cl1060, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1059, zip_derived_cl308])).
% 6.72/1.54 thf(clause_2111, axiom,
% 6.72/1.54 (( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_2 ) ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( s @ 0 ) @ ( f @ A_2 ) ) ) |
% 6.72/1.54 ( iLEQ @ ( suc @ A_2 ) @ ( suc @ A_2 ) ))).
% 6.72/1.54 thf(zip_derived_cl98, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_2111])).
% 6.72/1.54 thf(zip_derived_cl123, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl72, zip_derived_cl51])).
% 6.72/1.54 thf(zip_derived_cl161, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl98, zip_derived_cl123])).
% 6.72/1.54 thf(zip_derived_cl51, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_362])).
% 6.72/1.54 thf(zip_derived_cl162, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl161, zip_derived_cl51])).
% 6.72/1.54 thf(zip_derived_cl1061, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1060, zip_derived_cl162])).
% 6.72/1.54 thf(zip_derived_cl1375, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (LE @ (f @ X0) @ (s @ 0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('sup-', [status(thm)], [zip_derived_cl1362, zip_derived_cl1061])).
% 6.72/1.54 thf(clause_783, axiom,
% 6.72/1.54 (( ~( LE @ ( f @ ( suc @ B_28 ) ) @ ( s @ ( s @ 0 ) ) ) ) |
% 6.72/1.54 ( E @ ( s @ 0 ) @ ( f @ ( suc @ B_28 ) ) ) |
% 6.72/1.54 ( LE @ ( f @ B_28 ) @ ( s @ 0 ) ))).
% 6.72/1.54 thf(zip_derived_cl84, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (LE @ (f @ (suc @ X0)) @ (s @ (s @ 0)))
% 6.72/1.54 | (E @ (s @ 0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ 0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_783])).
% 6.72/1.54 thf(zip_derived_cl1359, plain,
% 6.72/1.54 (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ 0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1358, zip_derived_cl113])).
% 6.72/1.54 thf(zip_derived_cl1363, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (s @ 0) @ (f @ (suc @ X0))) | (LE @ (f @ X0) @ (s @ 0)))),
% 6.72/1.54 inference('demod', [status(thm)], [zip_derived_cl84, zip_derived_cl1359])).
% 6.72/1.54 thf(zip_derived_cl1382, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ 0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1375, zip_derived_cl1363])).
% 6.72/1.54 thf(clause_101, axiom,
% 6.72/1.54 (( ~( LE @ ( f @ ( suc @ ( suc @ B_28 ) ) ) @ ( s @ ( s @ 0 ) ) ) ) |
% 6.72/1.54 ( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ B_28 ) ) ) ) |
% 6.72/1.54 ( LE @ ( f @ B_28 ) @ ( s @ 0 ) ))).
% 6.72/1.54 thf(zip_derived_cl58, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (LE @ (f @ (suc @ (suc @ X0))) @ (s @ (s @ 0)))
% 6.72/1.54 | (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ 0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_101])).
% 6.72/1.54 thf(zip_derived_cl1359, plain,
% 6.72/1.54 (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ 0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1358, zip_derived_cl113])).
% 6.72/1.54 thf(zip_derived_cl1361, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ 0)))),
% 6.72/1.54 inference('demod', [status(thm)], [zip_derived_cl58, zip_derived_cl1359])).
% 6.72/1.54 thf(zip_derived_cl1383, plain,
% 6.72/1.54 (![X0 : $i]: ( (LE @ (f @ X0) @ (s @ 0)) | ~ (E @ (s @ 0) @ (f @ X0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1382, zip_derived_cl1361])).
% 6.72/1.54 thf(clause_1841, axiom,
% 6.72/1.54 (( ~( LE @ ( f @ B_28 ) @ ( s @ ( s @ 0 ) ) ) ) |
% 6.72/1.54 ( E @ ( s @ 0 ) @ ( f @ B_28 ) ) | ( LE @ ( f @ B_28 ) @ ( s @ 0 ) ))).
% 6.72/1.54 thf(zip_derived_cl40, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (LE @ (f @ X0) @ (s @ (s @ 0)))
% 6.72/1.54 | (E @ (s @ 0) @ (f @ X0))
% 6.72/1.54 | (LE @ (f @ X0) @ (s @ 0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_1841])).
% 6.72/1.54 thf(zip_derived_cl1359, plain,
% 6.72/1.54 (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ 0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1358, zip_derived_cl113])).
% 6.72/1.54 thf(zip_derived_cl1360, plain,
% 6.72/1.54 (![X0 : $i]: ( (E @ (s @ 0) @ (f @ X0)) | (LE @ (f @ X0) @ (s @ 0)))),
% 6.72/1.54 inference('demod', [status(thm)], [zip_derived_cl40, zip_derived_cl1359])).
% 6.72/1.54 thf(zip_derived_cl1384, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1383, zip_derived_cl1360])).
% 6.72/1.54 thf(zip_derived_cl1385, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0))))) | (LE @ (f @ X0) @ 0))),
% 6.72/1.54 inference('demod', [status(thm)], [zip_derived_cl49, zip_derived_cl1384])).
% 6.72/1.54 thf(clause_848, axiom,
% 6.72/1.54 (( ~( E @ 0 @ ( f @ B_36 ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ B_36 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_37 ) @ ( f @ ( suc @ ( suc @ B_37 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ B_37 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ B_36 ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ A_3 ) ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ A_3 ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_36 ) @ ( f @ ( suc @ ( suc @ B_36 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_36 ) @ ( f @ ( suc @ B_36 ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ A_3 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ A_3 ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ B_37 ) ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ B_37 ) ) ) ) | ( ~( E @ 0 @ ( f @ B_37 ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_37 ) @ ( f @ ( suc @ B_37 ) ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ A_3 ) @ ( suc @ B_36 ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ B_36 ) ) ) ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ B_36 ) @ ( suc @ B_37 ) ) ))).
% 6.72/1.54 thf(zip_derived_cl59, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i, X2 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ (f @ X2) @ (f @ (suc @ (suc @ X2))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X2))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X1)))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X1))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X2)))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X2)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X2))
% 6.72/1.54 | ~ (E @ (f @ X2) @ (f @ (suc @ X2)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X2)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_848])).
% 6.72/1.54 thf(zip_derived_cl733, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 (~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X1)))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X1)))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl59])).
% 6.72/1.54 thf(zip_derived_cl735, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ X1))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X1)))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0)))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl733])).
% 6.72/1.54 thf(zip_derived_cl811, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0)))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl735])).
% 6.72/1.54 thf(zip_derived_cl812, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl811])).
% 6.72/1.54 thf(clause_717, axiom,
% 6.72/1.54 (( ~( E @ 0 @ ( f @ B_36 ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ B_36 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ B_37 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ B_36 ) ) ) ) | ( ~( E @ 0 @ ( f @ A_3 ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_36 ) @ ( f @ ( suc @ B_36 ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ A_3 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ A_3 ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ B_37 ) ) ) ) | ( ~( E @ 0 @ ( f @ B_37 ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ B_37 ) @ ( f @ ( suc @ B_37 ) ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ A_3 ) @ ( suc @ B_36 ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ B_36 ) @ ( suc @ B_37 ) ) ) |
% 6.72/1.54 ( E @ ( f @ A_3 ) @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) |
% 6.72/1.54 ( E @ ( f @ B_36 ) @ ( f @ ( suc @ ( suc @ B_36 ) ) ) ) |
% 6.72/1.54 ( E @ ( f @ B_37 ) @ ( f @ ( suc @ ( suc @ B_37 ) ) ) ))).
% 6.72/1.54 thf(zip_derived_cl95, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i, X2 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X2))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X2))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X2)))
% 6.72/1.54 | ~ (E @ (f @ X2) @ (f @ (suc @ X2)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X1))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X2) @ (suc @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | (E @ (f @ X2) @ (f @ (suc @ (suc @ X2))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ (suc @ X1)))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_717])).
% 6.72/1.54 thf(zip_derived_cl555, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X1))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0)))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl95])).
% 6.72/1.54 thf(zip_derived_cl557, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X1))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl555])).
% 6.72/1.54 thf(zip_derived_cl714, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0)))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl557])).
% 6.72/1.54 thf(zip_derived_cl715, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl714])).
% 6.72/1.54 thf(clause_85, axiom,
% 6.72/1.54 (( ~( E @ 0 @ ( f @ B_36 ) ) ) | ( ~( E @ 0 @ ( f @ ( suc @ B_36 ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ A_3 ) ) ) | ( ~( E @ 0 @ ( f @ ( suc @ A_3 ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ B_37 ) ) ) ) | ( ~( E @ 0 @ ( f @ B_37 ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ A_3 ) @ ( suc @ B_36 ) ) ) |
% 6.72/1.54 ( ~( iLEQ @ ( suc @ B_36 ) @ ( suc @ B_37 ) ) ) |
% 6.72/1.54 ( E @ ( f @ A_3 ) @ ( f @ ( suc @ A_3 ) ) ) |
% 6.72/1.54 ( E @ ( f @ B_36 ) @ ( f @ ( suc @ B_36 ) ) ) |
% 6.72/1.54 ( E @ ( f @ B_37 ) @ ( f @ ( suc @ B_37 ) ) ))).
% 6.72/1.54 thf(zip_derived_cl74, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i, X2 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X1))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X2)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X2))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X2))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X2) @ (f @ (suc @ X2))))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_85])).
% 6.72/1.54 thf(zip_derived_cl169, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 ( (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X1))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0)))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl74])).
% 6.72/1.54 thf(zip_derived_cl171, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X1))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X1) @ (f @ (suc @ X1))))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl169])).
% 6.72/1.54 thf(clause_528, axiom,
% 6.72/1.54 (( ~( E @ 0 @ ( f @ A_3 ) ) ) | ( ~( E @ 0 @ ( f @ ( suc @ A_3 ) ) ) ) |
% 6.72/1.54 ( E @ ( f @ A_3 ) @ ( f @ ( suc @ A_3 ) ) ) |
% 6.72/1.54 ( iLEQ @ ( suc @ A_3 ) @ ( suc @ A_3 ) ))).
% 6.72/1.54 thf(zip_derived_cl67, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_528])).
% 6.72/1.54 thf(zip_derived_cl237, plain,
% 6.72/1.54 (![X0 : $i, X1 : $i]:
% 6.72/1.54 ( (E @ (f @ X1) @ (f @ (suc @ X1)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X1))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl171, zip_derived_cl67])).
% 6.72/1.54 thf(zip_derived_cl238, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('eq_fact', [status(thm)], [zip_derived_cl237])).
% 6.72/1.54 thf(zip_derived_cl239, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0)))),
% 6.72/1.54 inference('simplify', [status(thm)], [zip_derived_cl238])).
% 6.72/1.54 thf(zip_derived_cl67, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_528])).
% 6.72/1.54 thf(zip_derived_cl240, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl239, zip_derived_cl67])).
% 6.72/1.54 thf(zip_derived_cl716, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl715, zip_derived_cl240])).
% 6.72/1.54 thf(clause_1108, axiom,
% 6.72/1.54 (( ~( E @ 0 @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ A_3 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ A_3 ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ A_3 ) ) ) |
% 6.72/1.54 ( E @ ( f @ A_3 ) @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) |
% 6.72/1.54 ( iLEQ @ ( suc @ A_3 ) @ ( suc @ A_3 ) ))).
% 6.72/1.54 thf(zip_derived_cl8, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_1108])).
% 6.72/1.54 thf(zip_derived_cl67, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_528])).
% 6.72/1.54 thf(zip_derived_cl122, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl8, zip_derived_cl67])).
% 6.72/1.54 thf(zip_derived_cl717, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl716, zip_derived_cl122])).
% 6.72/1.54 thf(zip_derived_cl813, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl812, zip_derived_cl717])).
% 6.72/1.54 thf(clause_2357, axiom,
% 6.72/1.54 (( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ A_3 ) ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ A_3 ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) ) |
% 6.72/1.54 ( ~( E @ 0 @ ( f @ ( suc @ A_3 ) ) ) ) |
% 6.72/1.54 ( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ A_3 ) ) ) ) |
% 6.72/1.54 ( iLEQ @ ( suc @ A_3 ) @ ( suc @ A_3 ) ))).
% 6.72/1.54 thf(zip_derived_cl32, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_2357])).
% 6.72/1.54 thf(zip_derived_cl122, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl8, zip_derived_cl67])).
% 6.72/1.54 thf(zip_derived_cl154, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl32, zip_derived_cl122])).
% 6.72/1.54 thf(zip_derived_cl67, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_528])).
% 6.72/1.54 thf(zip_derived_cl155, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl154, zip_derived_cl67])).
% 6.72/1.54 thf(zip_derived_cl814, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl813, zip_derived_cl155])).
% 6.72/1.54 thf(zip_derived_cl240, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl239, zip_derived_cl67])).
% 6.72/1.54 thf(zip_derived_cl815, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0)))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl814, zip_derived_cl240])).
% 6.72/1.54 thf(zip_derived_cl1400, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 ( (LE @ (f @ X0) @ 0)
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | ~ (E @ 0 @ (f @ X0)))),
% 6.72/1.54 inference('sup-', [status(thm)], [zip_derived_cl1385, zip_derived_cl815])).
% 6.72/1.54 thf(clause_415, axiom,
% 6.72/1.54 (( ~( LE @ ( f @ ( suc @ ( suc @ B_35 ) ) ) @ ( s @ 0 ) ) ) |
% 6.72/1.54 ( E @ 0 @ ( f @ ( suc @ ( suc @ B_35 ) ) ) ) | ( LE @ ( f @ B_35 ) @ 0 ))).
% 6.72/1.54 thf(zip_derived_cl65, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (LE @ (f @ (suc @ (suc @ X0))) @ (s @ 0))
% 6.72/1.54 | (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 6.72/1.54 | (LE @ (f @ X0) @ 0))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_415])).
% 6.72/1.54 thf(zip_derived_cl1384, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1383, zip_derived_cl1360])).
% 6.72/1.54 thf(zip_derived_cl1386, plain,
% 6.72/1.54 (![X0 : $i]: ( (E @ 0 @ (f @ (suc @ (suc @ X0)))) | (LE @ (f @ X0) @ 0))),
% 6.72/1.54 inference('demod', [status(thm)], [zip_derived_cl65, zip_derived_cl1384])).
% 6.72/1.54 thf(zip_derived_cl1408, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (E @ 0 @ (f @ X0))
% 6.72/1.54 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | (LE @ (f @ X0) @ 0))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1400, zip_derived_cl1386])).
% 6.72/1.54 thf(clause_1753, axiom,
% 6.72/1.54 (( ~( LE @ ( f @ B_35 ) @ ( s @ 0 ) ) ) | ( E @ 0 @ ( f @ B_35 ) ) |
% 6.72/1.54 ( LE @ ( f @ B_35 ) @ 0 ))).
% 6.72/1.54 thf(zip_derived_cl102, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (LE @ (f @ X0) @ (s @ 0))
% 6.72/1.54 | (E @ 0 @ (f @ X0))
% 6.72/1.54 | (LE @ (f @ X0) @ 0))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_1753])).
% 6.72/1.54 thf(zip_derived_cl1384, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1383, zip_derived_cl1360])).
% 6.72/1.54 thf(zip_derived_cl1388, plain,
% 6.72/1.54 (![X0 : $i]: ( (E @ 0 @ (f @ X0)) | (LE @ (f @ X0) @ 0))),
% 6.72/1.54 inference('demod', [status(thm)], [zip_derived_cl102, zip_derived_cl1384])).
% 6.72/1.54 thf(zip_derived_cl1409, plain,
% 6.72/1.54 (![X0 : $i]: ( (LE @ (f @ X0) @ 0) | ~ (E @ 0 @ (f @ (suc @ X0))))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1408, zip_derived_cl1388])).
% 6.72/1.54 thf(clause_2008, axiom,
% 6.72/1.54 (( ~( LE @ ( f @ ( suc @ B_35 ) ) @ ( s @ 0 ) ) ) |
% 6.72/1.54 ( E @ 0 @ ( f @ ( suc @ B_35 ) ) ) | ( LE @ ( f @ B_35 ) @ 0 ))).
% 6.72/1.54 thf(zip_derived_cl89, plain,
% 6.72/1.54 (![X0 : $i]:
% 6.72/1.54 (~ (LE @ (f @ (suc @ X0)) @ (s @ 0))
% 6.72/1.54 | (E @ 0 @ (f @ (suc @ X0)))
% 6.72/1.54 | (LE @ (f @ X0) @ 0))),
% 6.72/1.54 inference('cnf', [status(esa)], [clause_2008])).
% 6.72/1.54 thf(zip_derived_cl1384, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1383, zip_derived_cl1360])).
% 6.72/1.54 thf(zip_derived_cl1387, plain,
% 6.72/1.54 (![X0 : $i]: ( (E @ 0 @ (f @ (suc @ X0))) | (LE @ (f @ X0) @ 0))),
% 6.72/1.54 inference('demod', [status(thm)], [zip_derived_cl89, zip_derived_cl1384])).
% 6.72/1.54 thf(zip_derived_cl1410, plain, (![X0 : $i]: (LE @ (f @ X0) @ 0)),
% 6.72/1.54 inference('clc', [status(thm)], [zip_derived_cl1409, zip_derived_cl1387])).
% 6.72/1.54 thf(zip_derived_cl1411, plain, ($false),
% 6.72/1.54 inference('demod', [status(thm)], [zip_derived_cl64, zip_derived_cl1410])).
% 6.72/1.54
% 6.72/1.54 % SZS output end Refutation
% 6.72/1.54
% 6.72/1.54
% 6.72/1.54 % Terminating...
% 7.36/1.65 % Runner terminated.
% 7.36/1.67 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------