%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : ALG268^3 : TPTP v9.2.0. Bugfixed v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.8C9OOP78eI 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 04:28:31 PM UTC 2025
% Result : Theorem 4.59s 1.25s
% Output : Refutation 4.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : ALG268^3 : TPTP v9.2.0. Bugfixed v5.2.0.
% 0.08/0.14 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.8C9OOP78eI true
% 0.14/0.35 % Computer : n019.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Oct 1 17:02:23 EDT 2025
% 0.14/0.35 % CPUTime :
% 0.14/0.35 % Running portfolio for 300 s
% 0.14/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.36 % Number of cores: 8
% 0.14/0.36 % Python version: Python 3.6.8
% 0.14/0.36 % Running in HO mode
% 0.57/0.65 % Total configuration time : 828
% 0.57/0.65 % Estimated wc time : 1656
% 0.57/0.65 % Estimated cpu time (8 cpus) : 207.0
% 0.58/0.76 % /export/starexec/sandbox/solver/bin/lams/40_c.s.sh running for 80s
% 0.58/0.78 % /export/starexec/sandbox/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.58/0.80 % /export/starexec/sandbox/solver/bin/lams/40_c_ic.sh running for 80s
% 0.58/0.81 % /export/starexec/sandbox/solver/bin/lams/15_e_short1.sh running for 30s
% 0.58/0.81 % /export/starexec/sandbox/solver/bin/lams/40_b.comb.sh running for 70s
% 0.58/0.82 % /export/starexec/sandbox/solver/bin/lams/40_noforms.sh running for 90s
% 0.58/0.82 % /export/starexec/sandbox/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.58/0.82 % /export/starexec/sandbox/solver/bin/lams/30_sp5.sh running for 60s
% 0.58/0.85 % /export/starexec/sandbox/solver/bin/lams/30_b.l.sh running for 90s
% 4.59/1.25 % Solved by lams/40_b.comb.sh.
% 4.59/1.25 % done 52 iterations in 0.375s
% 4.59/1.25 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 4.59/1.25 % SZS output start Refutation
% 4.59/1.25 thf(subst_type, type, subst: $tType).
% 4.59/1.25 thf(term_type, type, term: $tType).
% 4.59/1.25 thf(axmap_type, type, axmap: $o).
% 4.59/1.25 thf(axclos_type, type, axclos: $o).
% 4.59/1.25 thf(lam_type, type, lam: term > term).
% 4.59/1.25 thf('#sk3_type', type, '#sk3': term > $o).
% 4.59/1.25 thf('#sk7_type', type, '#sk7': (subst > term > term) > subst).
% 4.59/1.25 thf(push_type, type, push: term > subst > subst).
% 4.59/1.25 thf(hoasinduction_p_and_p_prime_type, type, hoasinduction_p_and_p_prime:
% 4.59/1.25 (subst > term > subst > $o) > (term > $o) > $o).
% 4.59/1.25 thf('#sk4_type', type, '#sk4': term).
% 4.59/1.25 thf(one_type, type, one: term).
% 4.59/1.25 thf(id_type, type, id: subst).
% 4.59/1.25 thf(comp_type, type, comp: subst > subst > subst).
% 4.59/1.25 thf(axvarid_type, type, axvarid: $o).
% 4.59/1.25 thf(axvarshift_type, type, axvarshift: $o).
% 4.59/1.25 thf('#sk8_type', type, '#sk8': (subst > term > term) > term).
% 4.59/1.25 thf(sh_type, type, sh: subst).
% 4.59/1.25 thf(hoasinduction_lem3v2a_lthm_type, type, hoasinduction_lem3v2a_lthm: $o).
% 4.59/1.25 thf('#sk1_type', type, '#sk1': term > subst > term > term).
% 4.59/1.25 thf(sub_type, type, sub: term > subst > term).
% 4.59/1.25 thf('#sk5_type', type, '#sk5': (subst > term > term) > subst).
% 4.59/1.25 thf(hoasinduction_lem3v2a_type, type, hoasinduction_lem3v2a: $o).
% 4.59/1.25 thf('#sk2_type', type, '#sk2': subst > term > subst > $o).
% 4.59/1.25 thf(hoaslam_type, type, hoaslam: subst > (subst > term > term) > term).
% 4.59/1.25 thf(hoasinduction_lem3v2_f_type, type, hoasinduction_lem3v2_f: $o).
% 4.59/1.25 thf('#sk6_type', type, '#sk6': (subst > term > term) > term).
% 4.59/1.25 thf(s_comb_type, type, '#S': !>[A:$tType, B:$tType, C:$tType]: ((A > B > C) > (A > B) > A > C)).
% 4.59/1.25 thf(c_comb_type, type, '#C': !>[A:$tType, B:$tType, C:$tType]: ((A > B > C) > B > A > C)).
% 4.59/1.25 thf(b_comb_type, type, '#B': !>[A:$tType, B:$tType, C:$tType]: ((A > B) > (C > A) > C > B)).
% 4.59/1.25 thf(k_comb_type, type, '#K': !>[A:$tType, B:$tType]: (B > A > B)).
% 4.59/1.25 thf(i_comb_type, type, '#I': !>[A:$tType]: (A > A)).
% 4.59/1.25 thf(thm, conjecture, (hoasinduction_lem3v2a_lthm)).
% 4.59/1.25 thf(zf_stmt_0, negated_conjecture, (~( hoasinduction_lem3v2a_lthm )),
% 4.59/1.25 inference('cnf.neg', [status(esa)], [thm])).
% 4.59/1.25 thf(zip_derived_cl0, plain, (~ (hoasinduction_lem3v2a_lthm)),
% 4.59/1.25 inference('cnf', [status(esa)], [zf_stmt_0])).
% 4.59/1.25 thf(hoasinduction_lem3v2a_lthm, axiom, ~ (hoasinduction_lem3v2a_lthm) =>
% 4.59/1.25 ((((hoasinduction_lem3v2_f) =>
% 4.59/1.25 (((axvarid) =>
% 4.59/1.25 (((axvarshift) =>
% 4.59/1.25 (((axclos) => (((axmap) => (hoasinduction_lem3v2a)))))))))))
% 4.59/1.25 != ($true))).
% 4.59/1.25 thf('0', plain,
% 4.59/1.25 (( ~( hoasinduction_lem3v2a_lthm ) ) <=>
% 4.59/1.25 ( ~( ( hoasinduction_lem3v2_f ) =>
% 4.59/1.25 ( ( axvarid ) =>
% 4.59/1.25 ( ( axvarshift ) =>
% 4.59/1.25 ( ( axclos ) => ( ( axmap ) => ( hoasinduction_lem3v2a ) ) ) ) ) ) )),
% 4.59/1.25 inference('rw.lit', [status(esa)], [hoasinduction_lem3v2a_lthm])).
% 4.59/1.25 thf(zip_derived_cl1, plain,
% 4.59/1.25 (~ (((hoasinduction_lem3v2_f) =>
% 4.59/1.25 (((axvarid) =>
% 4.59/1.25 (((axvarshift) =>
% 4.59/1.25 (((axclos) => (((axmap) => (hoasinduction_lem3v2a)))))))))))),
% 4.59/1.25 inference('rw_clause', [status(thm)], [zip_derived_cl0, '0'])).
% 4.59/1.25 thf(axvarshift, axiom,(( axvarshift ) = ((((push @ one @ sh) = (id)))))).
% 4.59/1.25 thf('1', plain, (( axvarshift ) = ( ( push @ one @ sh ) = ( id ) )),
% 4.59/1.25 define([status(thm)])).
% 4.59/1.25 thf(zip_derived_cl2, plain,
% 4.59/1.25 (~ (((hoasinduction_lem3v2_f) =>
% 4.59/1.25 (((axvarid) =>
% 4.59/1.25 (((((push @ one @ sh) = (id))) =>
% 4.59/1.25 (((axclos) => (((axmap) => (hoasinduction_lem3v2a)))))))))))),
% 4.59/1.25 inference('rw', [status(thm)], [zip_derived_cl1, '1'])).
% 4.59/1.25 thf(zip_derived_cl4, plain,
% 4.59/1.25 (~ (((axvarid) =>
% 4.59/1.25 (((((push @ one @ sh) = (id))) =>
% 4.59/1.25 (((axclos) => (((axmap) => (hoasinduction_lem3v2a)))))))))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl2])).
% 4.59/1.25 thf(zip_derived_cl7, plain,
% 4.59/1.25 (~ (((((push @ one @ sh) = (id))) =>
% 4.59/1.25 (((axclos) => (((axmap) => (hoasinduction_lem3v2a)))))))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl4])).
% 4.59/1.25 thf(zip_derived_cl12, plain,
% 4.59/1.25 (~ (((axclos) => (((axmap) => (hoasinduction_lem3v2a)))))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl7])).
% 4.59/1.25 thf(zip_derived_cl18, plain, (~ (((axmap) => (hoasinduction_lem3v2a)))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl12])).
% 4.59/1.25 thf(zip_derived_cl22, plain, ( (axmap)),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl18])).
% 4.59/1.25 thf(axmap, axiom, (axmap) =>
% 4.59/1.25 ((((!!) @ (^[Y0 : term]:
% 4.59/1.25 (((!!) @ (^[Y1 : subst]:
% 4.59/1.25 (((!!) @ (^[Y2 : subst]:
% 4.59/1.25 (((comp @ (push @ Y0 @ Y1) @ Y2) =
% 4.59/1.25 (push @ (sub @ Y0 @ Y2) @
% 4.59/1.25 (comp @ Y1 @ Y2)))))))))))))
% 4.59/1.25 = ($true))).
% 4.59/1.25 thf('2', plain,
% 4.59/1.25 (( axmap ) <=>
% 4.59/1.25 ( ![X5:term,X7:subst,X9:subst]:
% 4.59/1.25 ( ( comp @ ( push @ X5 @ X7 ) @ X9 ) =
% 4.59/1.25 ( push @ ( sub @ X5 @ X9 ) @ ( comp @ X7 @ X9 ) ) ) )),
% 4.59/1.25 inference('rw.lit', [status(esa)], [axmap])).
% 4.59/1.25 thf(zip_derived_cl27, plain,
% 4.59/1.25 ( (((!!) @ (^[Y0 : term]:
% 4.59/1.25 (((!!) @ (^[Y1 : subst]:
% 4.59/1.25 (((!!) @ (^[Y2 : subst]:
% 4.59/1.25 (((comp @ (push @ Y0 @ Y1) @ Y2) =
% 4.59/1.25 (push @ (sub @ Y0 @ Y2) @
% 4.59/1.25 (comp @ Y1 @ Y2)))))))))))))),
% 4.59/1.25 inference('rw_clause', [status(thm)], [zip_derived_cl22, '2'])).
% 4.59/1.25 thf(zip_derived_cl31, plain,
% 4.59/1.25 ( (((!!) @ ((('#B') @ (!!) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (!!))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ ('#S'))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ ((('#B') @ (=))))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ comp)) @ push)))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#B') @
% 4.59/1.25 ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ push)) @ sub)))))) @
% 4.59/1.25 comp))))))))))),
% 4.59/1.25 inference('comb-normalize', [status(thm)], [zip_derived_cl27])).
% 4.59/1.25 thf(zip_derived_cl32, plain,
% 4.59/1.25 (![X2 : term]:
% 4.59/1.25 (((!!) @ ((('#B') @ (!!) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ (=))) @
% 4.59/1.25 ((('#B') @ comp @ (push @ X2))))))) @
% 4.59/1.25 ((('#B') @ ((('#S') @ ((('#B') @ push @ (sub @ X2))))) @
% 4.59/1.25 comp))))))))),
% 4.59/1.25 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl31])).
% 4.59/1.25 thf(zip_derived_cl36, plain,
% 4.59/1.25 (![X2 : term, X4 : subst]:
% 4.59/1.25 (((!!) @ ((('#S') @ ((('#B') @ (=) @ (comp @ (push @ X2 @ X4)))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ push @ (sub @ X2))) @ (comp @ X4)))))))),
% 4.59/1.25 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl32])).
% 4.59/1.25 thf(zip_derived_cl39, plain,
% 4.59/1.25 (![X2 : term, X4 : subst, X6 : subst]:
% 4.59/1.25 (((comp @ (push @ X2 @ X4) @ X6) = (push @ (sub @ X2 @ X6) @
% 4.59/1.25 (comp @ X4 @ X6))))),
% 4.59/1.25 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl36])).
% 4.59/1.25 thf(zip_derived_cl42, plain,
% 4.59/1.25 (![X2 : term, X4 : subst, X6 : subst]:
% 4.59/1.25 ((comp @ (push @ X2 @ X4) @ X6)
% 4.59/1.25 = (push @ (sub @ X2 @ X6) @ (comp @ X4 @ X6)))),
% 4.59/1.25 inference('simplify nested equalities', [status(thm)], [zip_derived_cl39])).
% 4.59/1.25 thf(zip_derived_cl3, plain, ( (hoasinduction_lem3v2_f)),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl2])).
% 4.59/1.25 thf(hoasinduction_lem3v2_f, axiom, (hoasinduction_lem3v2_f) =>
% 4.59/1.25 ((((!!) @ (^[Y0 : term]:
% 4.59/1.25 (((??) @ (^[Y1 : subst > term > term]:
% 4.59/1.25 (((!!) @ (^[Y2 : term]:
% 4.59/1.25 (((!!) @ (^[Y3 : subst]:
% 4.59/1.25 (((Y1 @ Y3 @ Y2) = (sub @
% 4.59/1.25 Y0 @ (push @ Y2 @ Y3))))))))))))))))
% 4.59/1.25 = ($true))).
% 4.59/1.25 thf('3', plain,
% 4.59/1.25 (( hoasinduction_lem3v2_f ) <=>
% 4.59/1.25 ( ![X5:term]:
% 4.59/1.25 ( ?[X7:( subst > term > term )]:
% 4.59/1.25 ( ![X9:term,X11:subst]:
% 4.59/1.25 ( ( X7 @ X11 @ X9 ) = ( sub @ X5 @ ( push @ X9 @ X11 ) ) ) ) ) )),
% 4.59/1.25 inference('rw.lit', [status(esa)], [hoasinduction_lem3v2_f])).
% 4.59/1.25 thf(zip_derived_cl5, plain,
% 4.59/1.25 ( (((!!) @ (^[Y0 : term]:
% 4.59/1.25 (((??) @ (^[Y1 : subst > term > term]:
% 4.59/1.25 (((!!) @ (^[Y2 : term]:
% 4.59/1.25 (((!!) @ (^[Y3 : subst]:
% 4.59/1.25 (((Y1 @ Y3 @ Y2) =
% 4.59/1.25 (sub @ Y0 @
% 4.59/1.25 (push @ Y2 @ Y3))))))))))))))))),
% 4.59/1.25 inference('rw_clause', [status(thm)], [zip_derived_cl3, '3'])).
% 4.59/1.25 thf(zip_derived_cl8, plain,
% 4.59/1.25 ( (((!!) @ ((('#B') @ (??) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (!!))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ ((('#B') @ (!!))))) @
% 4.59/1.25 ((('#B') @ ((('#C') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ ('#S'))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (
% 4.59/1.25 (('#B') @ (=))))) @
% 4.59/1.25 ('#C'))))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#B') @
% 4.59/1.25 ((('#B') @ ('#B') @ sub)))) @
% 4.59/1.25 push))))))))))))),
% 4.59/1.25 inference('comb-normalize', [status(thm)], [zip_derived_cl5])).
% 4.59/1.25 thf(zip_derived_cl9, plain,
% 4.59/1.25 (![X2 : term]:
% 4.59/1.25 (((??) @ ((('#B') @ (!!) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (!!))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ ('#S'))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ ((('#B') @ (=))))) @
% 4.59/1.25 ('#C'))))))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (sub @ X2))) @ push))))))))))),
% 4.59/1.25 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl8])).
% 4.59/1.25 thf(zip_derived_cl13, plain,
% 4.59/1.25 (![X2 : term]:
% 4.59/1.25 (((!!) @ ((('#B') @ (!!) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ (=))) @
% 4.59/1.25 ((('#C') @ ('#sk1' @ X2))))))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (sub @ X2))) @ push))))))))),
% 4.59/1.25 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl9])).
% 4.59/1.25 thf(zip_derived_cl19, plain,
% 4.59/1.25 (![X2 : term, X4 : term]:
% 4.59/1.25 (((!!) @ ((('#S') @ ((('#B') @ (=) @ ((('#C') @ ('#sk1' @ X2) @ X4)))) @
% 4.59/1.25 ((('#B') @ (sub @ X2) @ (push @ X4)))))))),
% 4.59/1.25 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl13])).
% 4.59/1.25 thf(zip_derived_cl24, plain,
% 4.59/1.25 (![X2 : term, X4 : term, X6 : subst]:
% 4.59/1.25 ((('#sk1' @ X2 @ X6 @ X4) = (sub @ X2 @ (push @ X4 @ X6))))),
% 4.59/1.25 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl19])).
% 4.59/1.25 thf(zip_derived_cl29, plain,
% 4.59/1.25 (![X2 : term, X4 : term, X6 : subst]:
% 4.59/1.25 (('#sk1' @ X2 @ X6 @ X4) = (sub @ X2 @ (push @ X4 @ X6)))),
% 4.59/1.25 inference('simplify nested equalities', [status(thm)], [zip_derived_cl24])).
% 4.59/1.25 thf(zip_derived_cl92, plain,
% 4.59/1.25 (![X0 : subst, X1 : subst, X2 : term, X3 : term]:
% 4.59/1.25 (('#sk1' @ X3 @ (comp @ X1 @ X0) @ (sub @ X2 @ X0))
% 4.59/1.25 = (sub @ X3 @ (comp @ (push @ X2 @ X1) @ X0)))),
% 4.59/1.25 inference('sup+', [status(thm)], [zip_derived_cl42, zip_derived_cl29])).
% 4.59/1.25 thf(zip_derived_cl29, plain,
% 4.59/1.25 (![X2 : term, X4 : term, X6 : subst]:
% 4.59/1.25 (('#sk1' @ X2 @ X6 @ X4) = (sub @ X2 @ (push @ X4 @ X6)))),
% 4.59/1.25 inference('simplify nested equalities', [status(thm)], [zip_derived_cl24])).
% 4.59/1.25 thf(zip_derived_cl17, plain, ( (axclos)),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl12])).
% 4.59/1.25 thf(axclos, axiom, (axclos) =>
% 4.59/1.25 ((((!!) @ (^[Y0 : term]:
% 4.59/1.25 (((!!) @ (^[Y1 : subst]:
% 4.59/1.25 (((!!) @ (^[Y2 : subst]:
% 4.59/1.25 (((sub @ (sub @ Y0 @ Y1) @ Y2) =
% 4.59/1.25 (sub @ Y0 @ (comp @ Y1 @ Y2)))))))))))))
% 4.59/1.25 = ($true))).
% 4.59/1.25 thf('4', plain,
% 4.59/1.25 (( axclos ) <=>
% 4.59/1.25 ( ![X5:term,X7:subst,X9:subst]:
% 4.59/1.25 ( ( sub @ ( sub @ X5 @ X7 ) @ X9 ) = ( sub @ X5 @ ( comp @ X7 @ X9 ) ) ) )),
% 4.59/1.25 inference('rw.lit', [status(esa)], [axclos])).
% 4.59/1.25 thf(zip_derived_cl21, plain,
% 4.59/1.25 ( (((!!) @ (^[Y0 : term]:
% 4.59/1.25 (((!!) @ (^[Y1 : subst]:
% 4.59/1.25 (((!!) @ (^[Y2 : subst]:
% 4.59/1.25 (((sub @ (sub @ Y0 @ Y1) @ Y2) =
% 4.59/1.25 (sub @ Y0 @ (comp @ Y1 @ Y2)))))))))))))),
% 4.59/1.25 inference('rw_clause', [status(thm)], [zip_derived_cl17, '4'])).
% 4.59/1.25 thf(zip_derived_cl25, plain,
% 4.59/1.25 ( (((!!) @ ((('#B') @ (!!) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (!!))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ ('#S'))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ ((('#B') @ (=))))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ sub)) @ sub)))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#B') @ ((('#B') @ ('#B') @ sub)))) @
% 4.59/1.25 comp))))))))))),
% 4.59/1.25 inference('comb-normalize', [status(thm)], [zip_derived_cl21])).
% 4.59/1.25 thf(zip_derived_cl26, plain,
% 4.59/1.25 (![X2 : term]:
% 4.59/1.25 (((!!) @ ((('#B') @ (!!) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ (=))) @
% 4.59/1.25 ((('#B') @ sub @ (sub @ X2))))))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (sub @ X2))) @ comp))))))))),
% 4.59/1.25 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl25])).
% 4.59/1.25 thf(zip_derived_cl30, plain,
% 4.59/1.25 (![X2 : term, X4 : subst]:
% 4.59/1.25 (((!!) @ ((('#S') @ ((('#B') @ (=) @ (sub @ (sub @ X2 @ X4)))) @
% 4.59/1.25 ((('#B') @ (sub @ X2) @ (comp @ X4)))))))),
% 4.59/1.25 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl26])).
% 4.59/1.25 thf(zip_derived_cl35, plain,
% 4.59/1.25 (![X2 : term, X4 : subst, X6 : subst]:
% 4.59/1.25 (((sub @ (sub @ X2 @ X4) @ X6) = (sub @ X2 @ (comp @ X4 @ X6))))),
% 4.59/1.25 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl30])).
% 4.59/1.25 thf(zip_derived_cl38, plain,
% 4.59/1.25 (![X2 : term, X4 : subst, X6 : subst]:
% 4.59/1.25 ((sub @ (sub @ X2 @ X4) @ X6) = (sub @ X2 @ (comp @ X4 @ X6)))),
% 4.59/1.25 inference('simplify nested equalities', [status(thm)], [zip_derived_cl35])).
% 4.59/1.25 thf(zip_derived_cl80, plain,
% 4.59/1.25 (![X0 : term, X1 : subst, X2 : term, X3 : subst]:
% 4.59/1.25 ((sub @ ('#sk1' @ X2 @ X1 @ X0) @ X3)
% 4.59/1.25 = (sub @ X2 @ (comp @ (push @ X0 @ X1) @ X3)))),
% 4.59/1.25 inference('sup+', [status(thm)], [zip_derived_cl29, zip_derived_cl38])).
% 4.59/1.25 thf(zip_derived_cl321, plain,
% 4.59/1.25 (![X0 : subst, X1 : subst, X2 : term, X3 : term]:
% 4.59/1.25 (('#sk1' @ X3 @ (comp @ X1 @ X0) @ (sub @ X2 @ X0))
% 4.59/1.25 = (sub @ ('#sk1' @ X3 @ X1 @ X2) @ X0))),
% 4.59/1.25 inference('demod', [status(thm)], [zip_derived_cl92, zip_derived_cl80])).
% 4.59/1.25 thf(zip_derived_cl23, plain, (~ (hoasinduction_lem3v2a)),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl18])).
% 4.59/1.25 thf(hoasinduction_lem3v2a, axiom, ~ (hoasinduction_lem3v2a) =>
% 4.59/1.25 ((((!!) @ (^[Y0 : subst > term > subst > $o]:
% 4.59/1.25 (((!!) @ (^[Y1 : term > $o]:
% 4.59/1.25 (((((!!) @ (^[Y2 : subst > term > term]:
% 4.59/1.25 (((((!!) @ (^[Y3 : subst]:
% 4.59/1.25 (((!!) @ (^[Y4 : term]:
% 4.59/1.25 ((
% 4.59/1.25 (!!) @ (
% 4.59/1.25 ^[Y5 : subst]:
% 4.59/1.25 ((
% 4.59/1.25 (sub @
% 4.59/1.25 (
% 4.59/1.25 Y2 @
% 4.59/1.25 Y3 @ Y4) @
% 4.59/1.25 Y5) =
% 4.59/1.25 (Y2 @
% 4.59/1.25 (
% 4.59/1.25 comp @
% 4.59/1.25 Y3 @ Y5) @
% 4.59/1.25 (
% 4.59/1.25 sub @
% 4.59/1.25 Y4 @ Y5))))))))))))) =>
% 4.59/1.25 (((((!!) @ (^[Y3 : term]:
% 4.59/1.25 (((Y0 @ id @ Y3 @
% 4.59/1.25 id) => (Y0 @ id @
% 4.59/1.25 (Y2 @ id @ Y3) @
% 4.59/1.25 id)))))) =>
% 4.59/1.25 (Y0 @ id @
% 4.59/1.25 (hoaslam @ id @
% 4.59/1.25 (^[Y3 : subst,Y4 : term]:
% 4.59/1.25 (Y2 @ Y3 @ Y4))) @
% 4.59/1.25 id)))))))) =>
% 4.59/1.25 (((hoasinduction_p_and_p_prime @ Y0 @ Y1) =>
% 4.59/1.25 (((!!) @ (^[Y2 : term]:
% 4.59/1.25 (((((!!) @ (^[Y3 : term]:
% 4.59/1.25 (((Y1 @ Y3) =>
% 4.59/1.25 (Y1 @
% 4.59/1.25 (sub @ Y2 @
% 4.59/1.25 (push @ Y3 @ id)))))))) =>
% 4.59/1.25 (Y1 @ (lam @ Y2)))))))))))))))))
% 4.59/1.25 != ($true))).
% 4.59/1.25 thf('5', plain,
% 4.59/1.25 (( ~( hoasinduction_lem3v2a ) ) <=>
% 4.59/1.25 ( ~( ![X5:( subst > term > subst > $o ),X7:( term > $o )]:
% 4.59/1.25 ( ( ![X9:( subst > term > term )]:
% 4.59/1.25 ( ( ![X11:subst,X13:term,X15:subst]:
% 4.59/1.25 ( ( sub @ ( X9 @ X11 @ X13 ) @ X15 ) =
% 4.59/1.25 ( X9 @ ( comp @ X11 @ X15 ) @ ( sub @ X13 @ X15 ) ) ) ) =>
% 4.59/1.25 ( ( ![X17:term]:
% 4.59/1.25 ( ( X5 @ id @ X17 @ id ) =>
% 4.59/1.25 ( X5 @ id @ ( X9 @ id @ X17 ) @ id ) ) ) =>
% 4.59/1.25 ( X5 @
% 4.59/1.25 id @
% 4.59/1.25 ( hoaslam @
% 4.59/1.25 id @ ( ^[V_1:subst,V_2:term]: ( X9 @ V_1 @ V_2 ) ) ) @
% 4.59/1.25 id ) ) ) ) =>
% 4.59/1.25 ( ( hoasinduction_p_and_p_prime @ X5 @ X7 ) =>
% 4.59/1.25 ( ![X19:term]:
% 4.59/1.25 ( ( ![X21:term]:
% 4.59/1.25 ( ( X7 @ X21 ) =>
% 4.59/1.25 ( X7 @ ( sub @ X19 @ ( push @ X21 @ id ) ) ) ) ) =>
% 4.59/1.25 ( X7 @ ( lam @ X19 ) ) ) ) ) ) ) )),
% 4.59/1.25 inference('rw.lit', [status(esa)], [hoasinduction_lem3v2a])).
% 4.59/1.25 thf(zip_derived_cl28, plain,
% 4.59/1.25 (~ (((!!) @ (^[Y0 : subst > term > subst > $o]:
% 4.59/1.25 (((!!) @ (^[Y1 : term > $o]:
% 4.59/1.25 (((((!!) @ (^[Y2 : subst > term > term]:
% 4.59/1.25 (((((!!) @ (^[Y3 : subst]:
% 4.59/1.25 (((!!) @ (
% 4.59/1.25 ^[Y4 : term]:
% 4.59/1.25 (((!!) @ (
% 4.59/1.25 ^[Y5 : subst]:
% 4.59/1.25 ((
% 4.59/1.25 (sub @
% 4.59/1.25 (
% 4.59/1.25 Y2 @
% 4.59/1.25 Y3 @ Y4) @
% 4.59/1.25 Y5) =
% 4.59/1.25 (Y2 @
% 4.59/1.25 (
% 4.59/1.25 comp @
% 4.59/1.25 Y3 @ Y5) @
% 4.59/1.25 (
% 4.59/1.25 sub @
% 4.59/1.25 Y4 @ Y5))))))))))))) =>
% 4.59/1.25 (((((!!) @ (^[Y3 : term]:
% 4.59/1.25 (((Y0 @ id @
% 4.59/1.25 Y3 @ id) =>
% 4.59/1.25 (Y0 @ id @
% 4.59/1.25 (Y2 @ id @ Y3) @
% 4.59/1.25 id)))))) =>
% 4.59/1.25 (Y0 @ id @
% 4.59/1.25 (hoaslam @ id @
% 4.59/1.25 (^[Y3 : subst,Y4 : term]:
% 4.59/1.25 (Y2 @ Y3 @ Y4))) @
% 4.59/1.25 id)))))))) =>
% 4.59/1.25 (((hoasinduction_p_and_p_prime @ Y0 @ Y1) =>
% 4.59/1.25 (((!!) @ (^[Y2 : term]:
% 4.59/1.25 (((((!!) @ (^[Y3 : term]:
% 4.59/1.25 (((Y1 @ Y3) =>
% 4.59/1.25 (Y1 @
% 4.59/1.25 (sub @ Y2 @
% 4.59/1.25 (push @ Y3 @
% 4.59/1.25 id)))))))) =>
% 4.59/1.25 (Y1 @ (lam @ Y2)))))))))))))))))),
% 4.59/1.25 inference('rw_clause', [status(thm)], [zip_derived_cl23, '5'])).
% 4.59/1.25 thf(zip_derived_cl33, plain,
% 4.59/1.25 (~ (((!!) @ ((('#B') @ (!!) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#B') @
% 4.59/1.25 ((('#B') @ (=>) @
% 4.59/1.25 ((('#B') @ (!!) @
% 4.59/1.25 ((('#B') @ ((('#S') @ ((('#B') @ (
% 4.59/1.25 =>) @
% 4.59/1.25 ((('#B') @ (
% 4.59/1.25 !!) @
% 4.59/1.25 ((('#B') @ (
% 4.59/1.25 (('#B') @ (!!))) @
% 4.59/1.25 ((('#B') @ (
% 4.59/1.25 (('#B') @ (
% 4.59/1.25 (('#B') @ (
% 4.59/1.25 !!))))) @
% 4.59/1.25 ((('#S') @ (
% 4.59/1.25 (('#B') @ (
% 4.59/1.25 '#S') @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#S'))) @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#S'))))) @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 =))))))) @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ sub)))))))))))) @
% 4.59/1.25 ((
% 4.59/1.25 ('#C') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#C') @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#B'))) @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#S'))) @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#C') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#B') @
% 4.59/1.25 (
% 4.59/1.25 '#B'))) @
% 4.59/1.25 comp)))))))) @
% 4.59/1.25 sub)))))))))))))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ (=>))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (
% 4.59/1.25 !!))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ (
% 4.59/1.25 '#B') @
% 4.59/1.25 ((
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#S') @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 =>))) @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#C') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#C') @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#C') @ (
% 4.59/1.25 '#I') @
% 4.59/1.25 id)))) @
% 4.59/1.25 id)))))))) @
% 4.59/1.25 ((('#C') @ ((
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#C') @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#C'))) @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#C') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#B') @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#B') @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#C') @ (
% 4.59/1.25 '#I') @
% 4.59/1.25 id)))))) @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#C') @ (
% 4.59/1.25 '#I') @
% 4.59/1.25 id)))))))) @
% 4.59/1.25 id)))))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#C') @
% 4.59/1.25 ((('#C') @ ((('#B') @ (
% 4.59/1.25 '#B') @
% 4.59/1.25 ((('#C') @ (
% 4.59/1.25 '#I') @ id)))) @
% 4.59/1.25 (hoaslam @ id))))) @
% 4.59/1.25 id)))))))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ (=>))) @
% 4.59/1.25 hoasinduction_p_and_p_prime)))) @
% 4.59/1.25 ((('#B') @ (!!) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ (=>))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (!!))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#B') @
% 4.59/1.25 ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ (=>))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#B') @
% 4.59/1.25 ('#B'))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#B') @
% 4.59/1.25 sub)) @
% 4.59/1.25 ((('#C') @ push @ id)))))))))))))) @
% 4.59/1.25 ((('#C') @ ('#B') @ lam))))))))))))))),
% 4.59/1.25 inference('comb-normalize', [status(thm)], [zip_derived_cl28])).
% 4.59/1.25 thf(zip_derived_cl34, plain,
% 4.59/1.25 (~ (((!!) @ ((('#B') @ (((=>) @ (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#B') @ (
% 4.59/1.25 !!) @
% 4.59/1.25 ((('#B') @ (
% 4.59/1.25 (('#B') @ (!!))) @
% 4.59/1.25 ((('#B') @ (
% 4.59/1.25 (('#B') @ (
% 4.59/1.25 (('#B') @ (
% 4.59/1.25 !!))))) @
% 4.59/1.25 ((('#S') @ (
% 4.59/1.25 (('#B') @ (
% 4.59/1.25 '#S') @
% 4.59/1.25 ((
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#S'))) @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#S'))))) @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 =))))))) @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ sub)))))))))))) @
% 4.59/1.25 ((('#C') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#C') @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#B'))) @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#S'))) @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#C') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#B') @
% 4.59/1.25 (
% 4.59/1.25 '#B'))) @
% 4.59/1.25 comp)))))))) @
% 4.59/1.25 sub)))))))))))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ (
% 4.59/1.25 =>) @
% 4.59/1.25 ((('#B') @ (
% 4.59/1.25 !!) @
% 4.59/1.25 ((('#B') @ (
% 4.59/1.25 (('#S') @ (
% 4.59/1.25 (('#B') @ (
% 4.59/1.25 =>) @
% 4.59/1.25 ((('#C') @ (
% 4.59/1.25 '#sk2' @
% 4.59/1.25 id) @ id)))))) @
% 4.59/1.25 ((('#C') @ (
% 4.59/1.25 (('#B') @ (
% 4.59/1.25 '#C') @
% 4.59/1.25 ((
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#sk2' @
% 4.59/1.25 id))) @
% 4.59/1.25 (
% 4.59/1.25 (
% 4.59/1.25 ('#C') @ (
% 4.59/1.25 '#I') @
% 4.59/1.25 id)))))) @
% 4.59/1.25 id)))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ (
% 4.59/1.25 '#sk2' @ id) @
% 4.59/1.25 (hoaslam @ id))) @
% 4.59/1.25 id)))))))))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 (hoasinduction_p_and_p_prime @ '#sk2'))) @
% 4.59/1.25 ((('#B') @ (!!) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ (=>))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (!!))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#B') @
% 4.59/1.25 ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ (=>))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#B') @
% 4.59/1.25 ('#B'))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#B') @ sub)) @
% 4.59/1.25 ((('#C') @ push @ id)))))))))))))) @
% 4.59/1.25 ((('#C') @ ('#B') @ lam))))))))))))),
% 4.59/1.25 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl33])).
% 4.59/1.25 thf(zip_derived_cl37, plain,
% 4.59/1.25 (~ (((((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#B') @ (!!) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (!!))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ ((('#B') @ (!!))))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ (
% 4.59/1.25 '#S'))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (
% 4.59/1.25 (('#B') @ (
% 4.59/1.25 '#S'))))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (
% 4.59/1.25 (('#B') @ (
% 4.59/1.25 (
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 =))))))) @
% 4.59/1.25 ((('#B') @ ((
% 4.59/1.25 ('#B') @ sub)))))))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#C') @
% 4.59/1.25 ((('#B') @ ((('#B') @ (
% 4.59/1.25 '#B'))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (
% 4.59/1.25 '#S'))) @
% 4.59/1.25 ((('#C') @ ((
% 4.59/1.25 ('#B') @ (
% 4.59/1.25 '#B') @
% 4.59/1.25 (
% 4.59/1.25 '#B'))) @
% 4.59/1.25 comp)))))))) @
% 4.59/1.25 sub)))))))))))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#B') @ (!!) @
% 4.59/1.25 ((('#B') @ ((('#S') @ ((('#B') @ (
% 4.59/1.25 =>) @
% 4.59/1.25 ((('#C') @ (
% 4.59/1.25 '#sk2' @ id) @
% 4.59/1.25 id)))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#C') @
% 4.59/1.25 ((('#B') @ ((('#B') @ (
% 4.59/1.25 '#sk2' @ id))) @
% 4.59/1.25 ((('#C') @ ('#I') @ id)))))) @
% 4.59/1.25 id)))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#sk2' @ id) @ (hoaslam @ id))) @
% 4.59/1.25 id)))))))) =>
% 4.59/1.25 (((hoasinduction_p_and_p_prime @ '#sk2' @ '#sk3') =>
% 4.59/1.25 (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#B') @ (!!) @
% 4.59/1.25 ((('#B') @ ((('#S') @ ((('#B') @ (
% 4.59/1.25 =>) @ '#sk3')))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ '#sk3')) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#B') @ sub)) @
% 4.59/1.25 ((('#C') @ push @ id)))))))))))) @
% 4.59/1.25 ((('#B') @ '#sk3' @ lam))))))))))),
% 4.59/1.25 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl34])).
% 4.59/1.25 thf(zip_derived_cl40, plain,
% 4.59/1.25 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#B') @ (!!) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (!!))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ ((('#B') @ (!!))))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ ('#S'))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (
% 4.59/1.25 (('#B') @ (
% 4.59/1.25 '#S'))))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (
% 4.59/1.25 (('#B') @ (
% 4.59/1.25 (('#B') @ (
% 4.59/1.25 =))))))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ sub)))))))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#C') @
% 4.59/1.25 ((('#B') @ ((('#B') @ ('#B'))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (
% 4.59/1.25 '#S'))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ (
% 4.59/1.25 '#B') @
% 4.59/1.25 ('#B'))) @
% 4.59/1.25 comp)))))))) @
% 4.59/1.25 sub)))))))))))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#B') @ (!!) @
% 4.59/1.25 ((('#B') @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#C') @ ('#sk2' @
% 4.59/1.25 id) @
% 4.59/1.25 id)))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#C') @
% 4.59/1.25 ((('#B') @ ((('#B') @ (
% 4.59/1.25 '#sk2' @ id))) @
% 4.59/1.25 ((('#C') @ ('#I') @ id)))))) @
% 4.59/1.25 id)))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#sk2' @ id) @ (hoaslam @ id))) @
% 4.59/1.25 id))))))))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl37])).
% 4.59/1.25 thf(zip_derived_cl43, plain,
% 4.59/1.25 (![X2 : subst > term > term]:
% 4.59/1.25 (((((!!) @ ((('#B') @ (!!) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (!!))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ ('#S'))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ ((('#B') @ (=))))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ sub)) @ X2)))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#B') @
% 4.59/1.25 ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ X2)) @ comp)))))) @
% 4.59/1.25 sub)))))))))) =>
% 4.59/1.25 (((((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#C') @ ('#sk2' @ id) @ id)))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#sk2' @ id) @ (X2 @ id))) @ id)))))) =>
% 4.59/1.25 ('#sk2' @ id @ (hoaslam @ id @ X2) @ id)))))),
% 4.59/1.25 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl40])).
% 4.59/1.25 thf(hoaslam, axiom,(( hoaslam @ (X1)@ (X0)) = ((lam @ (X0 @ sh @ one))))).
% 4.59/1.25 thf('6', plain,
% 4.59/1.25 (![X1:subst,X0:( subst > term > term )]:
% 4.59/1.25 ( ( hoaslam @ X1 @ X0 ) = ( lam @ ( X0 @ sh @ one ) ) )),
% 4.59/1.25 define([status(thm)])).
% 4.59/1.25 thf(zip_derived_cl46, plain,
% 4.59/1.25 (![X2 : subst > term > term]:
% 4.59/1.25 (((((!!) @ ((('#B') @ (!!) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (!!))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ ('#S'))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ ((('#B') @ (=))))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ sub)) @ X2)))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#B') @
% 4.59/1.25 ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ X2)) @ comp)))))) @
% 4.59/1.25 sub)))))))))) =>
% 4.59/1.25 (((((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#C') @ ('#sk2' @ id) @ id)))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#sk2' @ id) @ (X2 @ id))) @ id)))))) =>
% 4.59/1.25 ('#sk2' @ id @ (lam @ (X2 @ sh @ one)) @ id)))))),
% 4.59/1.25 inference('rw', [status(thm)], [zip_derived_cl43, '6'])).
% 4.59/1.25 thf(zip_derived_cl47, plain,
% 4.59/1.25 (![X2 : subst > term > term]:
% 4.59/1.25 (~ (((!!) @ ((('#B') @ (!!) @
% 4.59/1.25 ((('#B') @ ((('#B') @ (!!))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ ('#S'))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ ((('#B') @ (=))))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ sub)) @ X2)))))))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#B') @
% 4.59/1.25 ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ X2)) @ comp)))))) @
% 4.59/1.25 sub))))))))))
% 4.59/1.25 | (((((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#C') @ ('#sk2' @ id) @ id)))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#sk2' @ id) @ (X2 @ id))) @
% 4.59/1.25 id)))))) =>
% 4.59/1.25 ('#sk2' @ id @ (lam @ (X2 @ sh @ one)) @ id))))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl46])).
% 4.59/1.25 thf(zip_derived_cl50, plain,
% 4.59/1.25 (![X2 : subst > term > term]:
% 4.59/1.25 (~ (((!!) @ ((('#B') @ (!!) @
% 4.59/1.25 ((('#S') @ ((('#B') @ ('#S') @
% 4.59/1.25 ((('#B') @ ((('#B') @ (=))) @
% 4.59/1.25 ((('#B') @ sub @ (X2 @ ('#sk5' @ X2)))))))) @
% 4.59/1.25 ((('#B') @ ((('#S') @ ((('#B') @ X2 @
% 4.59/1.25 (comp @ ('#sk5' @ X2)))))) @
% 4.59/1.25 sub))))))))
% 4.59/1.25 | (((((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#C') @ ('#sk2' @ id) @ id)))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#sk2' @ id) @ (X2 @ id))) @
% 4.59/1.25 id)))))) =>
% 4.59/1.25 ('#sk2' @ id @ (lam @ (X2 @ sh @ one)) @ id))))),
% 4.59/1.25 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl47])).
% 4.59/1.25 thf(zip_derived_cl55, plain,
% 4.59/1.25 (![X2 : subst > term > term]:
% 4.59/1.25 (~ (((!!) @ ((('#S') @ ((('#B') @ (=) @
% 4.59/1.25 (sub @ (X2 @ ('#sk5' @ X2) @ ('#sk6' @ X2))))) @
% 4.59/1.25 ((('#S') @ ((('#B') @ X2 @ (comp @ ('#sk5' @ X2)))) @
% 4.59/1.25 (sub @ ('#sk6' @ X2))))))))
% 4.59/1.25 | (((((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#C') @ ('#sk2' @ id) @ id)))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#sk2' @ id) @ (X2 @ id))) @
% 4.59/1.25 id)))))) =>
% 4.59/1.25 ('#sk2' @ id @ (lam @ (X2 @ sh @ one)) @ id))))),
% 4.59/1.25 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl50])).
% 4.59/1.25 thf(zip_derived_cl58, plain,
% 4.59/1.25 (![X2 : subst > term > term]:
% 4.59/1.25 (~ (((sub @ (X2 @ ('#sk5' @ X2) @ ('#sk6' @ X2)) @ ('#sk7' @ X2)) =
% 4.59/1.25 (X2 @ (comp @ ('#sk5' @ X2) @ ('#sk7' @ X2)) @
% 4.59/1.25 (sub @ ('#sk6' @ X2) @ ('#sk7' @ X2)))))
% 4.59/1.25 | (((((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#C') @ ('#sk2' @ id) @ id)))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#sk2' @ id) @ (X2 @ id))) @
% 4.59/1.25 id)))))) =>
% 4.59/1.25 ('#sk2' @ id @ (lam @ (X2 @ sh @ one)) @ id))))),
% 4.59/1.25 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl55])).
% 4.59/1.25 thf(zip_derived_cl60, plain,
% 4.59/1.25 (![X2 : subst > term > term]:
% 4.59/1.25 (((sub @ (X2 @ ('#sk5' @ X2) @ ('#sk6' @ X2)) @ ('#sk7' @ X2))
% 4.59/1.25 != (X2 @ (comp @ ('#sk5' @ X2) @ ('#sk7' @ X2)) @
% 4.59/1.25 (sub @ ('#sk6' @ X2) @ ('#sk7' @ X2))))
% 4.59/1.25 | (((((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#C') @ ('#sk2' @ id) @ id)))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#sk2' @ id) @ (X2 @ id))) @
% 4.59/1.25 id)))))) =>
% 4.59/1.25 ('#sk2' @ id @ (lam @ (X2 @ sh @ one)) @ id))))),
% 4.59/1.25 inference('simplify nested equalities', [status(thm)], [zip_derived_cl58])).
% 4.59/1.25 thf(zip_derived_cl61, plain,
% 4.59/1.25 (![X2 : subst > term > term]:
% 4.59/1.25 (~ (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#C') @ ('#sk2' @ id) @ id)))) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#sk2' @ id) @ (X2 @ id))) @ id))))))
% 4.59/1.25 | ('#sk2' @ id @ (lam @ (X2 @ sh @ one)) @ id)
% 4.59/1.25 | ((sub @ (X2 @ ('#sk5' @ X2) @ ('#sk6' @ X2)) @ ('#sk7' @ X2))
% 4.59/1.25 != (X2 @ (comp @ ('#sk5' @ X2) @ ('#sk7' @ X2)) @
% 4.59/1.25 (sub @ ('#sk6' @ X2) @ ('#sk7' @ X2)))))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl60])).
% 4.59/1.25 thf(zip_derived_cl62, plain,
% 4.59/1.25 (![X2 : subst > term > term]:
% 4.59/1.25 (~ ((('#sk2' @ id @ ('#sk8' @ X2) @ id) => ('#sk2' @ id @
% 4.59/1.25 (X2 @ id @ ('#sk8' @ X2)) @ id)))
% 4.59/1.25 | ((sub @ (X2 @ ('#sk5' @ X2) @ ('#sk6' @ X2)) @ ('#sk7' @ X2))
% 4.59/1.25 != (X2 @ (comp @ ('#sk5' @ X2) @ ('#sk7' @ X2)) @
% 4.59/1.25 (sub @ ('#sk6' @ X2) @ ('#sk7' @ X2))))
% 4.59/1.25 | ('#sk2' @ id @ (lam @ (X2 @ sh @ one)) @ id))),
% 4.59/1.25 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl61])).
% 4.59/1.25 thf(zip_derived_cl64, plain,
% 4.59/1.25 (![X2 : subst > term > term]:
% 4.59/1.25 (~ ('#sk2' @ id @ (X2 @ id @ ('#sk8' @ X2)) @ id)
% 4.59/1.25 | ('#sk2' @ id @ (lam @ (X2 @ sh @ one)) @ id)
% 4.59/1.25 | ((sub @ (X2 @ ('#sk5' @ X2) @ ('#sk6' @ X2)) @ ('#sk7' @ X2))
% 4.59/1.25 != (X2 @ (comp @ ('#sk5' @ X2) @ ('#sk7' @ X2)) @
% 4.59/1.25 (sub @ ('#sk6' @ X2) @ ('#sk7' @ X2)))))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl62])).
% 4.59/1.25 thf(zip_derived_cl322, plain,
% 4.59/1.25 (![X0 : term]:
% 4.59/1.25 (((sub @
% 4.59/1.25 ('#sk1' @ X0 @ ('#sk5' @ ('#sk1' @ X0)) @ ('#sk6' @ ('#sk1' @ X0))) @
% 4.59/1.25 ('#sk7' @ ('#sk1' @ X0)))
% 4.59/1.25 != (sub @
% 4.59/1.25 ('#sk1' @ X0 @ ('#sk5' @ ('#sk1' @ X0)) @
% 4.59/1.25 ('#sk6' @ ('#sk1' @ X0))) @
% 4.59/1.25 ('#sk7' @ ('#sk1' @ X0))))
% 4.59/1.25 | ('#sk2' @ id @ (lam @ ('#sk1' @ X0 @ sh @ one)) @ id)
% 4.59/1.25 | ~ ('#sk2' @ id @ ('#sk1' @ X0 @ id @ ('#sk8' @ ('#sk1' @ X0))) @ id))),
% 4.59/1.25 inference('sup-', [status(thm)], [zip_derived_cl321, zip_derived_cl64])).
% 4.59/1.25 thf(zip_derived_cl11, plain, ( (((push @ one @ sh) = (id)))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl7])).
% 4.59/1.25 thf(zip_derived_cl16, plain, (((push @ one @ sh) = (id))),
% 4.59/1.25 inference('simplify nested equalities', [status(thm)], [zip_derived_cl11])).
% 4.59/1.25 thf(zip_derived_cl29, plain,
% 4.59/1.25 (![X2 : term, X4 : term, X6 : subst]:
% 4.59/1.25 (('#sk1' @ X2 @ X6 @ X4) = (sub @ X2 @ (push @ X4 @ X6)))),
% 4.59/1.25 inference('simplify nested equalities', [status(thm)], [zip_derived_cl24])).
% 4.59/1.25 thf(zip_derived_cl74, plain,
% 4.59/1.25 (![X0 : term]: (('#sk1' @ X0 @ sh @ one) = (sub @ X0 @ id))),
% 4.59/1.25 inference('sup+', [status(thm)], [zip_derived_cl16, zip_derived_cl29])).
% 4.59/1.25 thf(zip_derived_cl6, plain, ( (axvarid)),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl4])).
% 4.59/1.25 thf(axvarid, axiom, (axvarid) =>
% 4.59/1.25 ((((!!) @ (^[Y0 : term]: (((sub @ Y0 @ id) = (Y0)))))) = ($true))).
% 4.59/1.25 thf('7', plain,
% 4.59/1.25 (( axvarid ) <=> ( ![X5:term]: ( ( sub @ X5 @ id ) = ( X5 ) ) )),
% 4.59/1.25 inference('rw.lit', [status(esa)], [axvarid])).
% 4.59/1.25 thf(zip_derived_cl10, plain,
% 4.59/1.25 ( (((!!) @ (^[Y0 : term]: (((sub @ Y0 @ id) = (Y0))))))),
% 4.59/1.25 inference('rw_clause', [status(thm)], [zip_derived_cl6, '7'])).
% 4.59/1.25 thf(zip_derived_cl14, plain,
% 4.59/1.25 ( (((!!) @ ((('#S') @ ((('#B') @ (=) @ ((('#C') @ sub @ id)))) @ ('#I')))))),
% 4.59/1.25 inference('comb-normalize', [status(thm)], [zip_derived_cl10])).
% 4.59/1.25 thf(zip_derived_cl15, plain, (![X2 : term]: (((sub @ X2 @ id) = (X2)))),
% 4.59/1.25 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl14])).
% 4.59/1.25 thf(zip_derived_cl20, plain, (![X2 : term]: ((sub @ X2 @ id) = (X2))),
% 4.59/1.25 inference('simplify nested equalities', [status(thm)], [zip_derived_cl15])).
% 4.59/1.25 thf(zip_derived_cl75, plain,
% 4.59/1.25 (![X0 : term]: (('#sk1' @ X0 @ sh @ one) = (X0))),
% 4.59/1.25 inference('demod', [status(thm)], [zip_derived_cl74, zip_derived_cl20])).
% 4.59/1.25 thf(zip_derived_cl41, plain,
% 4.59/1.25 (~ (((hoasinduction_p_and_p_prime @ '#sk2' @ '#sk3') =>
% 4.59/1.25 (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#B') @ (!!) @
% 4.59/1.25 ((('#B') @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 '#sk3')))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ '#sk3')) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#B') @ sub)) @
% 4.59/1.25 ((('#C') @ push @ id)))))))))))) @
% 4.59/1.25 ((('#B') @ '#sk3' @ lam))))))))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl37])).
% 4.59/1.25 thf(zip_derived_cl44, plain,
% 4.59/1.25 ( (hoasinduction_p_and_p_prime @ '#sk2' @ '#sk3')),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl41])).
% 4.59/1.25 thf(hoasinduction_p_and_p_prime, axiom,
% 4.59/1.25 (hoasinduction_p_and_p_prime @ X0 @ X1) =>
% 4.59/1.25 ((((!!) @ (^[Y0 : term]: (((X1 @ Y0) <=> (X0 @ id @ Y0 @ id)))))) = ($true))).
% 4.59/1.25 thf('8', plain,
% 4.59/1.25 (![X0:( subst > term > subst > $o ),X1:( term > $o )]:
% 4.59/1.25 ( ( hoasinduction_p_and_p_prime @ X0 @ X1 ) <=>
% 4.59/1.25 ( ![X6:term]: ( ( X1 @ X6 ) <=> ( X0 @ id @ X6 @ id ) ) ) )),
% 4.59/1.25 inference('rw.lit', [status(esa)], [hoasinduction_p_and_p_prime])).
% 4.59/1.25 thf(zip_derived_cl48, plain,
% 4.59/1.25 ( (((!!) @ (^[Y0 : term]: ((('#sk3' @ Y0) <=> ('#sk2' @ id @ Y0 @ id))))))),
% 4.59/1.25 inference('rw_clause', [status(thm)], [zip_derived_cl44, '8'])).
% 4.59/1.25 thf(zip_derived_cl51, plain,
% 4.59/1.25 ( (((!!) @ ((('#S') @ ((('#B') @ (<=>) @ '#sk3')) @
% 4.59/1.25 ((('#C') @ ('#sk2' @ id) @ id))))))),
% 4.59/1.25 inference('comb-normalize', [status(thm)], [zip_derived_cl48])).
% 4.59/1.25 thf(zip_derived_cl52, plain,
% 4.59/1.25 (![X2 : term]: ((('#sk3' @ X2) <=> ('#sk2' @ id @ X2 @ id)))),
% 4.59/1.25 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl51])).
% 4.59/1.25 thf(zip_derived_cl56, plain,
% 4.59/1.25 (![X2 : term]: (('#sk3' @ X2) = ('#sk2' @ id @ X2 @ id))),
% 4.59/1.25 inference('simplify nested equalities', [status(thm)], [zip_derived_cl52])).
% 4.59/1.25 thf(zip_derived_cl56, plain,
% 4.59/1.25 (![X2 : term]: (('#sk3' @ X2) = ('#sk2' @ id @ X2 @ id))),
% 4.59/1.25 inference('simplify nested equalities', [status(thm)], [zip_derived_cl52])).
% 4.59/1.25 thf(zip_derived_cl350, plain,
% 4.59/1.25 (![X0 : term]:
% 4.59/1.25 (((sub @
% 4.59/1.25 ('#sk1' @ X0 @ ('#sk5' @ ('#sk1' @ X0)) @ ('#sk6' @ ('#sk1' @ X0))) @
% 4.59/1.25 ('#sk7' @ ('#sk1' @ X0)))
% 4.59/1.25 != (sub @
% 4.59/1.25 ('#sk1' @ X0 @ ('#sk5' @ ('#sk1' @ X0)) @
% 4.59/1.25 ('#sk6' @ ('#sk1' @ X0))) @
% 4.59/1.25 ('#sk7' @ ('#sk1' @ X0))))
% 4.59/1.25 | ('#sk3' @ (lam @ X0))
% 4.59/1.25 | ~ ('#sk3' @ ('#sk1' @ X0 @ id @ ('#sk8' @ ('#sk1' @ X0)))))),
% 4.59/1.25 inference('demod', [status(thm)],
% 4.59/1.25 [zip_derived_cl322, zip_derived_cl75, zip_derived_cl56,
% 4.59/1.25 zip_derived_cl56])).
% 4.59/1.25 thf(zip_derived_cl351, plain,
% 4.59/1.25 (![X0 : term]:
% 4.59/1.25 (~ ('#sk3' @ ('#sk1' @ X0 @ id @ ('#sk8' @ ('#sk1' @ X0))))
% 4.59/1.25 | ('#sk3' @ (lam @ X0)))),
% 4.59/1.25 inference('simplify', [status(thm)], [zip_derived_cl350])).
% 4.59/1.25 thf(zip_derived_cl45, plain,
% 4.59/1.25 (~ (((!!) @ ((('#S') @ ((('#B') @ (=>) @
% 4.59/1.25 ((('#B') @ (!!) @
% 4.59/1.25 ((('#B') @ ((('#S') @ ((('#B') @ (=>) @ '#sk3')))) @
% 4.59/1.25 ((('#B') @ ((('#B') @ '#sk3')) @
% 4.59/1.25 ((('#C') @ ((('#B') @ ('#B') @ sub)) @
% 4.59/1.25 ((('#C') @ push @ id)))))))))))) @
% 4.59/1.25 ((('#B') @ '#sk3' @ lam))))))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl41])).
% 4.59/1.25 thf(zip_derived_cl49, plain,
% 4.59/1.25 (~ (((((!!) @ ((('#S') @ ((('#B') @ (=>) @ '#sk3')) @
% 4.59/1.25 ((('#B') @ '#sk3' @
% 4.59/1.25 ((('#B') @ (sub @ '#sk4') @ ((('#C') @ push @ id)))))))))) =>
% 4.59/1.25 ('#sk3' @ (lam @ '#sk4'))))),
% 4.59/1.25 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl45])).
% 4.59/1.25 thf(zip_derived_cl53, plain,
% 4.59/1.25 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @ '#sk3')) @
% 4.59/1.25 ((('#B') @ '#sk3' @
% 4.59/1.25 ((('#B') @ (sub @ '#sk4') @ ((('#C') @ push @ id))))))))))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl49])).
% 4.59/1.25 thf(zip_derived_cl57, plain,
% 4.59/1.25 (![X2 : term]:
% 4.59/1.25 ((('#sk3' @ X2) => ('#sk3' @ (sub @ '#sk4' @ (push @ X2 @ id)))))),
% 4.59/1.25 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl53])).
% 4.59/1.25 thf(zip_derived_cl59, plain,
% 4.59/1.25 (![X2 : term]:
% 4.59/1.25 (~ ('#sk3' @ X2) | ('#sk3' @ (sub @ '#sk4' @ (push @ X2 @ id))))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl57])).
% 4.59/1.25 thf(zip_derived_cl29, plain,
% 4.59/1.25 (![X2 : term, X4 : term, X6 : subst]:
% 4.59/1.25 (('#sk1' @ X2 @ X6 @ X4) = (sub @ X2 @ (push @ X4 @ X6)))),
% 4.59/1.25 inference('simplify nested equalities', [status(thm)], [zip_derived_cl24])).
% 4.59/1.25 thf(zip_derived_cl65, plain,
% 4.59/1.25 (![X2 : term]:
% 4.59/1.25 (~ ('#sk3' @ X2) | ('#sk3' @ ('#sk1' @ '#sk4' @ id @ X2)))),
% 4.59/1.25 inference('demod', [status(thm)], [zip_derived_cl59, zip_derived_cl29])).
% 4.59/1.25 thf(zip_derived_cl355, plain,
% 4.59/1.25 (( ('#sk3' @ (lam @ '#sk4')) | ~ ('#sk3' @ ('#sk8' @ ('#sk1' @ '#sk4'))))),
% 4.59/1.25 inference('sup+', [status(thm)], [zip_derived_cl351, zip_derived_cl65])).
% 4.59/1.25 thf(zip_derived_cl54, plain, (~ ('#sk3' @ (lam @ '#sk4'))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl49])).
% 4.59/1.25 thf(zip_derived_cl357, plain, (~ ('#sk3' @ ('#sk8' @ ('#sk1' @ '#sk4')))),
% 4.59/1.25 inference('clc', [status(thm)], [zip_derived_cl355, zip_derived_cl54])).
% 4.59/1.25 thf(zip_derived_cl321, plain,
% 4.59/1.25 (![X0 : subst, X1 : subst, X2 : term, X3 : term]:
% 4.59/1.25 (('#sk1' @ X3 @ (comp @ X1 @ X0) @ (sub @ X2 @ X0))
% 4.59/1.25 = (sub @ ('#sk1' @ X3 @ X1 @ X2) @ X0))),
% 4.59/1.25 inference('demod', [status(thm)], [zip_derived_cl92, zip_derived_cl80])).
% 4.59/1.25 thf(zip_derived_cl63, plain,
% 4.59/1.25 (![X2 : subst > term > term]:
% 4.59/1.25 ( ('#sk2' @ id @ ('#sk8' @ X2) @ id)
% 4.59/1.25 | ('#sk2' @ id @ (lam @ (X2 @ sh @ one)) @ id)
% 4.59/1.25 | ((sub @ (X2 @ ('#sk5' @ X2) @ ('#sk6' @ X2)) @ ('#sk7' @ X2))
% 4.59/1.25 != (X2 @ (comp @ ('#sk5' @ X2) @ ('#sk7' @ X2)) @
% 4.59/1.25 (sub @ ('#sk6' @ X2) @ ('#sk7' @ X2)))))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl62])).
% 4.59/1.25 thf(zip_derived_cl56, plain,
% 4.59/1.25 (![X2 : term]: (('#sk3' @ X2) = ('#sk2' @ id @ X2 @ id))),
% 4.59/1.25 inference('simplify nested equalities', [status(thm)], [zip_derived_cl52])).
% 4.59/1.25 thf(zip_derived_cl66, plain,
% 4.59/1.25 (![X2 : subst > term > term]:
% 4.59/1.25 ( ('#sk3' @ ('#sk8' @ X2))
% 4.59/1.25 | ('#sk2' @ id @ (lam @ (X2 @ sh @ one)) @ id)
% 4.59/1.25 | ((sub @ (X2 @ ('#sk5' @ X2) @ ('#sk6' @ X2)) @ ('#sk7' @ X2))
% 4.59/1.25 != (X2 @ (comp @ ('#sk5' @ X2) @ ('#sk7' @ X2)) @
% 4.59/1.25 (sub @ ('#sk6' @ X2) @ ('#sk7' @ X2)))))),
% 4.59/1.25 inference('demod', [status(thm)], [zip_derived_cl63, zip_derived_cl56])).
% 4.59/1.25 thf(zip_derived_cl323, plain,
% 4.59/1.25 (![X0 : term]:
% 4.59/1.25 (((sub @
% 4.59/1.25 ('#sk1' @ X0 @ ('#sk5' @ ('#sk1' @ X0)) @ ('#sk6' @ ('#sk1' @ X0))) @
% 4.59/1.25 ('#sk7' @ ('#sk1' @ X0)))
% 4.59/1.25 != (sub @
% 4.59/1.25 ('#sk1' @ X0 @ ('#sk5' @ ('#sk1' @ X0)) @
% 4.59/1.25 ('#sk6' @ ('#sk1' @ X0))) @
% 4.59/1.25 ('#sk7' @ ('#sk1' @ X0))))
% 4.59/1.25 | ('#sk2' @ id @ (lam @ ('#sk1' @ X0 @ sh @ one)) @ id)
% 4.59/1.25 | ('#sk3' @ ('#sk8' @ ('#sk1' @ X0))))),
% 4.59/1.25 inference('sup-', [status(thm)], [zip_derived_cl321, zip_derived_cl66])).
% 4.59/1.25 thf(zip_derived_cl75, plain,
% 4.59/1.25 (![X0 : term]: (('#sk1' @ X0 @ sh @ one) = (X0))),
% 4.59/1.25 inference('demod', [status(thm)], [zip_derived_cl74, zip_derived_cl20])).
% 4.59/1.25 thf(zip_derived_cl56, plain,
% 4.59/1.25 (![X2 : term]: (('#sk3' @ X2) = ('#sk2' @ id @ X2 @ id))),
% 4.59/1.25 inference('simplify nested equalities', [status(thm)], [zip_derived_cl52])).
% 4.59/1.25 thf(zip_derived_cl352, plain,
% 4.59/1.25 (![X0 : term]:
% 4.59/1.25 (((sub @
% 4.59/1.25 ('#sk1' @ X0 @ ('#sk5' @ ('#sk1' @ X0)) @ ('#sk6' @ ('#sk1' @ X0))) @
% 4.59/1.25 ('#sk7' @ ('#sk1' @ X0)))
% 4.59/1.25 != (sub @
% 4.59/1.25 ('#sk1' @ X0 @ ('#sk5' @ ('#sk1' @ X0)) @
% 4.59/1.25 ('#sk6' @ ('#sk1' @ X0))) @
% 4.59/1.25 ('#sk7' @ ('#sk1' @ X0))))
% 4.59/1.25 | ('#sk3' @ (lam @ X0))
% 4.59/1.25 | ('#sk3' @ ('#sk8' @ ('#sk1' @ X0))))),
% 4.59/1.25 inference('demod', [status(thm)],
% 4.59/1.25 [zip_derived_cl323, zip_derived_cl75, zip_derived_cl56])).
% 4.59/1.25 thf(zip_derived_cl353, plain,
% 4.59/1.25 (![X0 : term]:
% 4.59/1.25 ( ('#sk3' @ ('#sk8' @ ('#sk1' @ X0))) | ('#sk3' @ (lam @ X0)))),
% 4.59/1.25 inference('simplify', [status(thm)], [zip_derived_cl352])).
% 4.59/1.25 thf(zip_derived_cl54, plain, (~ ('#sk3' @ (lam @ '#sk4'))),
% 4.59/1.25 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl49])).
% 4.59/1.25 thf(zip_derived_cl450, plain, ( ('#sk3' @ ('#sk8' @ ('#sk1' @ '#sk4')))),
% 4.59/1.25 inference('sup-', [status(thm)], [zip_derived_cl353, zip_derived_cl54])).
% 4.59/1.25 thf(zip_derived_cl452, plain, ($false),
% 4.59/1.25 inference('demod', [status(thm)], [zip_derived_cl357, zip_derived_cl450])).
% 4.59/1.25
% 4.59/1.25 % SZS output end Refutation
% 4.59/1.25
% 4.59/1.25
% 4.59/1.25 % Terminating...
% 5.02/1.37 % Runner terminated.
% 5.02/1.39 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------