%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : PUZ087^2 : TPTP v9.2.0. Released 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.EkSGoFOhOz true
% Computer : n022.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:49:40 PM UTC 2025
% Result : Theorem 188.19s 24.33s
% Output : Refutation 188.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PUZ087^2 : TPTP v9.2.0. Released v5.2.0.
% 0.14/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.EkSGoFOhOz true
% 0.15/0.35 % Computer : n022.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Wed Oct 1 15:07:38 EDT 2025
% 0.21/0.35 % CPUTime :
% 0.21/0.35 % Running portfolio for 300 s
% 0.21/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.35 % Number of cores: 8
% 0.21/0.35 % Python version: Python 3.6.8
% 0.21/0.36 % Running in HO mode
% 0.57/0.67 % Total configuration time : 828
% 0.57/0.67 % Estimated wc time : 1656
% 0.57/0.67 % Estimated cpu time (8 cpus) : 207.0
% 0.58/0.73 % /export/starexec/sandbox/solver/bin/lams/40_c.s.sh running for 80s
% 0.58/0.73 % /export/starexec/sandbox/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.58/0.73 % /export/starexec/sandbox/solver/bin/lams/40_c_ic.sh running for 80s
% 0.58/0.74 % /export/starexec/sandbox/solver/bin/lams/15_e_short1.sh running for 30s
% 0.59/0.77 % /export/starexec/sandbox/solver/bin/lams/40_noforms.sh running for 90s
% 0.59/0.77 % /export/starexec/sandbox/solver/bin/lams/40_b.comb.sh running for 70s
% 0.59/0.78 % /export/starexec/sandbox/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.59/0.79 % /export/starexec/sandbox/solver/bin/lams/30_sp5.sh running for 60s
% 0.59/0.82 % /export/starexec/sandbox/solver/bin/lams/30_b.l.sh running for 90s
% 17.04/2.82 % /export/starexec/sandbox/solver/bin/lams/35_full_unif.sh running for 56s
% 188.19/24.33 % Solved by lams/30_b.l.sh.
% 188.19/24.33 % done 602 iterations in 23.335s
% 188.19/24.33 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 188.19/24.33 % SZS output start Refutation
% 188.19/24.33 thf(mbox_type, type, mbox: ($i > $i > $o) > ($i > $o) > $i > $o).
% 188.19/24.33 thf(a_type, type, a: $i > $i > $o).
% 188.19/24.33 thf('#sk306_type', type, '#sk306': ($i > $o) > $i > $i).
% 188.19/24.33 thf(ws_type, type, ws: ($i > $i > $o) > $i > $o).
% 188.19/24.33 thf('#sk21_type', type, '#sk21': $i > $i).
% 188.19/24.33 thf(mnot_type, type, mnot: ($i > $o) > $i > $o).
% 188.19/24.33 thf('#sk5_type', type, '#sk5': $i).
% 188.19/24.33 thf(mimplies_type, type, mimplies: ($i > $o) > ($i > $o) > $i > $o).
% 188.19/24.33 thf('#sk6_type', type, '#sk6': $i > $i).
% 188.19/24.33 thf('#sk1_type', type, '#sk1': $i).
% 188.19/24.33 thf('#sk114_type', type, '#sk114': ($i > $o) > $i > $i).
% 188.19/24.33 thf('#sk4_type', type, '#sk4': $i).
% 188.19/24.33 thf(priorG_type, type, priorG: $i > $i > $o).
% 188.19/24.33 thf(b_type, type, b: $i > $i > $o).
% 188.19/24.33 thf(c_type, type, c: $i > $i > $o).
% 188.19/24.33 thf('#sk15_type', type, '#sk15': ($i > $o) > $i > $i).
% 188.19/24.33 thf(fool_type, type, fool: $i > $i > $o).
% 188.19/24.33 thf('#sk3_type', type, '#sk3': $i).
% 188.19/24.33 thf(mor_type, type, mor: ($i > $o) > ($i > $o) > $i > $o).
% 188.19/24.33 thf(mforall_prop_type, type, mforall_prop: (($i > $o) > $i > $o) > $i > $o).
% 188.19/24.33 thf(mvalid_type, type, mvalid: ($i > $o) > $o).
% 188.19/24.33 thf('#sk2_type', type, '#sk2': $i).
% 188.19/24.33 thf(a6_axiom_for_fool_c_a, axiom,
% 188.19/24.33 (mvalid @
% 188.19/24.33 ( mforall_prop @
% 188.19/24.33 ( ^[Phi:( $i > $o )]:
% 188.19/24.33 ( mimplies @
% 188.19/24.33 ( mnot @ ( mbox @ c @ Phi ) ) @
% 188.19/24.33 ( mbox @ a @ ( mnot @ ( mbox @ c @ Phi ) ) ) ) ) ))).
% 188.19/24.33 thf(zip_derived_cl30, plain,
% 188.19/24.33 ( (mvalid @
% 188.19/24.33 (mforall_prop @
% 188.19/24.33 (^[Y0 : $i > $o]:
% 188.19/24.33 (mimplies @ (mnot @ (mbox @ c @ Y0)) @
% 188.19/24.33 (mbox @ a @ (mnot @ (mbox @ c @ Y0)))))))),
% 188.19/24.33 inference('cnf', [status(esa)], [a6_axiom_for_fool_c_a])).
% 188.19/24.33 thf(mvalid, axiom, (mvalid @ X0) =>
% 188.19/24.33 ((((!!) @ (^[Y0 : $i]: (X0 @ Y0)))) = ($true))).
% 188.19/24.33 thf('0', plain,
% 188.19/24.33 (![X0:( $i > $o )]: ( ( mvalid @ X0 ) <=> ( ![X5:$i]: ( X0 @ X5 ) ) )),
% 188.19/24.33 inference('rw.lit', [status(esa)], [mvalid])).
% 188.19/24.33 thf(zip_derived_cl547, plain,
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (mforall_prop @
% 188.19/24.33 (^[Y1 : $i > $o]:
% 188.19/24.33 (mimplies @ (mnot @ (mbox @ c @ Y1)) @
% 188.19/24.33 (mbox @ a @ (mnot @ (mbox @ c @ Y1))))) @
% 188.19/24.33 Y0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl30, '0'])).
% 188.19/24.33 thf(zip_derived_cl548, plain,
% 188.19/24.33 (![X2 : $i]:
% 188.19/24.33 (mforall_prop @
% 188.19/24.33 (^[Y0 : $i > $o]:
% 188.19/24.33 (mimplies @ (mnot @ (mbox @ c @ Y0)) @
% 188.19/24.33 (mbox @ a @ (mnot @ (mbox @ c @ Y0))))) @
% 188.19/24.33 X2)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl547])).
% 188.19/24.33 thf(mforall_prop, axiom, (mforall_prop @ X0 @ X1) =>
% 188.19/24.33 ((((!!) @ (^[Y0 : $i > $o]: (X0 @ Y0 @ X1)))) = ($true))).
% 188.19/24.33 thf('1', plain,
% 188.19/24.33 (![X0:( ( $i > $o ) > $i > $o ),X1:$i]:
% 188.19/24.33 ( ( mforall_prop @ X0 @ X1 ) <=> ( ![X6:( $i > $o )]: ( X0 @ X6 @ X1 ) ) )),
% 188.19/24.33 inference('rw.lit', [status(esa)], [mforall_prop])).
% 188.19/24.33 thf(zip_derived_cl549, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i > $o]:
% 188.19/24.33 ((^[Y1 : $i > $o]:
% 188.19/24.33 (mimplies @ (mnot @ (mbox @ c @ Y1)) @
% 188.19/24.33 (mbox @ a @ (mnot @ (mbox @ c @ Y1))))) @
% 188.19/24.33 Y0 @ X0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl548, '1'])).
% 188.19/24.33 thf(zip_derived_cl550, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i > $o]:
% 188.19/24.33 (mimplies @ (mnot @ (mbox @ c @ Y0)) @
% 188.19/24.33 (mbox @ a @ (mnot @ (mbox @ c @ Y0))) @ X0))))),
% 188.19/24.33 inference('ho_norm', [status(thm)], [zip_derived_cl549])).
% 188.19/24.33 thf(zip_derived_cl551, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i > $o]:
% 188.19/24.33 (mimplies @ (mnot @ (mbox @ c @ X2)) @
% 188.19/24.33 (mbox @ a @ (mnot @ (mbox @ c @ X2))) @ X0)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl550])).
% 188.19/24.33 thf(mimplies, axiom,(( mimplies @ (X0)@ (X1)@ (X2)) =
% 188.19/24.33 ((mor @ (mnot @ X0) @ X1 @ X2)))).
% 188.19/24.33 thf('2', plain,
% 188.19/24.33 (![X2:$i,X1:( $i > $o ),X0:( $i > $o )]:
% 188.19/24.33 ( ( mimplies @ X0 @ X1 @ X2 ) = ( mor @ ( mnot @ X0 ) @ X1 @ X2 ) )),
% 188.19/24.33 define([status(thm)])).
% 188.19/24.33 thf(zip_derived_cl552, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i > $o]:
% 188.19/24.33 (mor @ (mnot @ (mnot @ (mbox @ c @ X2))) @
% 188.19/24.33 (mbox @ a @ (mnot @ (mbox @ c @ X2))) @ X0)),
% 188.19/24.33 inference('rw', [status(thm)], [zip_derived_cl551, '2'])).
% 188.19/24.33 thf(mor, axiom, (mor @ X0 @ X1 @ X2) =>
% 188.19/24.33 ((((X1 @ X2) | (X0 @ X2))) = ($true))).
% 188.19/24.33 thf('3', plain,
% 188.19/24.33 (![X0:( $i > $o ),X1:( $i > $o ),X2:$i]:
% 188.19/24.33 ( ( mor @ X0 @ X1 @ X2 ) <=> ( ( X0 @ X2 ) | ( X1 @ X2 ) ) )),
% 188.19/24.33 inference('rw.lit', [status(esa)], [mor])).
% 188.19/24.33 thf(zip_derived_cl553, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 (((mbox @ a @ (mnot @ (mbox @ c @ X0)) @ X1) | (mnot @
% 188.19/24.33 (mnot @ (mbox @ c @ X0)) @ X1)))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl552, '3'])).
% 188.19/24.33 thf(zip_derived_cl554, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 ( (mbox @ a @ (mnot @ (mbox @ c @ X0)) @ X1)
% 188.19/24.33 | (mnot @ (mnot @ (mbox @ c @ X0)) @ X1))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl553])).
% 188.19/24.33 thf(mbox, axiom, (mbox @ X0 @ X1 @ X2) =>
% 188.19/24.33 ((((!!) @ (^[Y0 : $i]: (((((~) @ (X0 @ X2 @ Y0))) | (X1 @ Y0)))))) =
% 188.19/24.33 ($true))).
% 188.19/24.33 thf('4', plain,
% 188.19/24.33 (![X0:( $i > $i > $o ),X1:( $i > $o ),X2:$i]:
% 188.19/24.33 ( ( mbox @ X0 @ X1 @ X2 ) <=>
% 188.19/24.33 ( ![X7:$i]: ( ( ~( X0 @ X2 @ X7 ) ) | ( X1 @ X7 ) ) ) )),
% 188.19/24.33 inference('rw.lit', [status(esa)], [mbox])).
% 188.19/24.33 thf(zip_derived_cl555, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i > $o]:
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (a @ X0 @ Y0))) | (mnot @ (mbox @ c @ X1) @
% 188.19/24.33 Y0))))))
% 188.19/24.33 | (mnot @ (mnot @ (mbox @ c @ X1)) @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl554, '4'])).
% 188.19/24.33 thf(mnot, axiom, (mnot @ X0 @ X1) => ((X0 @ X1) != ($true))).
% 188.19/24.33 thf('5', plain,
% 188.19/24.33 (![X0:( $i > $o ),X1:$i]: ( ( mnot @ X0 @ X1 ) <=> ( ~( X0 @ X1 ) ) )),
% 188.19/24.33 inference('rw.lit', [status(esa)], [mnot])).
% 188.19/24.33 thf(zip_derived_cl556, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 (~ (mnot @ (mbox @ c @ X0) @ X1)
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (a @ X1 @ Y0))) | (mnot @ (mbox @ c @ X0) @
% 188.19/24.33 Y0)))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl555, '5'])).
% 188.19/24.33 thf(mnot, axiom, ~ (mnot @ X0 @ X1) => ((X0 @ X1) = ($true))).
% 188.19/24.33 thf('6', plain,
% 188.19/24.33 (![X0:( $i > $o ),X1:$i]: ( ( ~( mnot @ X0 @ X1 ) ) <=> ( X0 @ X1 ) )),
% 188.19/24.33 inference('rw.lit', [status(esa)], [mnot])).
% 188.19/24.33 thf(zip_derived_cl557, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 ( (mbox @ c @ X0 @ X1)
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (a @ X1 @ Y0))) | (mnot @ (mbox @ c @ X0) @
% 188.19/24.33 Y0)))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl556, '6'])).
% 188.19/24.33 thf(zip_derived_cl558, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]: (((((~) @ (c @ X1 @ Y0))) | (X0 @ Y0))))))
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (a @ X1 @ Y0))) | (mnot @ (mbox @ c @ X0) @
% 188.19/24.33 Y0)))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl557, '4'])).
% 188.19/24.33 thf(zip_derived_cl559, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i, X3 : $i]:
% 188.19/24.33 ( (((((~) @ (c @ X1 @ X3))) | (X0 @ X3)))
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (a @ X1 @ Y0))) | (mnot @ (mbox @ c @ X0) @
% 188.19/24.33 Y0)))))))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl558])).
% 188.19/24.33 thf(zip_derived_cl560, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i, X3 : $i]:
% 188.19/24.33 (~ (c @ X1 @ X3)
% 188.19/24.33 | (X0 @ X3)
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (a @ X1 @ Y0))) | (mnot @ (mbox @ c @ X0) @
% 188.19/24.33 Y0)))))))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl559])).
% 188.19/24.33 thf(zip_derived_cl561, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i, X3 : $i, X5 : $i]:
% 188.19/24.33 ( (((((~) @ (a @ X1 @ X5))) | (mnot @ (mbox @ c @ X0) @ X5)))
% 188.19/24.33 | (X0 @ X3)
% 188.19/24.33 | ~ (c @ X1 @ X3))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl560])).
% 188.19/24.33 thf(zip_derived_cl562, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i, X3 : $i, X5 : $i]:
% 188.19/24.33 (~ (a @ X1 @ X5)
% 188.19/24.33 | (mnot @ (mbox @ c @ X0) @ X5)
% 188.19/24.33 | ~ (c @ X1 @ X3)
% 188.19/24.33 | (X0 @ X3))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl561])).
% 188.19/24.33 thf(zip_derived_cl563, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i, X2 : $i, X3 : $i]:
% 188.19/24.33 (~ (mbox @ c @ X0 @ X3)
% 188.19/24.33 | (X0 @ X1)
% 188.19/24.33 | ~ (c @ X2 @ X1)
% 188.19/24.33 | ~ (a @ X2 @ X3))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl562, '5'])).
% 188.19/24.33 thf(mbox, axiom, ~ (mbox @ X0 @ X1 @ X2) =>
% 188.19/24.33 ((((!!) @ (^[Y0 : $i]: (((((~) @ (X0 @ X2 @ Y0))) | (X1 @ Y0)))))) !=
% 188.19/24.33 ($true))).
% 188.19/24.33 thf('7', plain,
% 188.19/24.33 (![X0:( $i > $i > $o ),X1:( $i > $o ),X2:$i]:
% 188.19/24.33 ( ( ~( mbox @ X0 @ X1 @ X2 ) ) <=>
% 188.19/24.33 ( ~( ![X7:$i]: ( ( ~( X0 @ X2 @ X7 ) ) | ( X1 @ X7 ) ) ) ) )),
% 188.19/24.33 inference('rw.lit', [status(esa)], [mbox])).
% 188.19/24.33 thf(zip_derived_cl564, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i > $o]:
% 188.19/24.33 (~ (((!!) @ (^[Y0 : $i]: (((((~) @ (c @ X0 @ Y0))) | (X3 @ Y0))))))
% 188.19/24.33 | ~ (a @ X1 @ X0)
% 188.19/24.33 | ~ (c @ X1 @ X2)
% 188.19/24.33 | (X3 @ X2))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl563, '7'])).
% 188.19/24.33 thf(zip_derived_cl565, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i > $o]:
% 188.19/24.33 (~ (((((~) @ (c @ X0 @ ('#sk114' @ X3 @ X0)))) | (X3 @
% 188.19/24.33 ('#sk114' @ X3 @ X0))))
% 188.19/24.33 | (X3 @ X2)
% 188.19/24.33 | ~ (c @ X1 @ X2)
% 188.19/24.33 | ~ (a @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl564])).
% 188.19/24.33 thf(zip_derived_cl567, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i > $o]:
% 188.19/24.33 (~ (X3 @ ('#sk114' @ X3 @ X0))
% 188.19/24.33 | ~ (a @ X1 @ X0)
% 188.19/24.33 | ~ (c @ X1 @ X2)
% 188.19/24.33 | (X3 @ X2))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl565])).
% 188.19/24.33 thf(conj, conjecture,
% 188.19/24.33 (mvalid @
% 188.19/24.33 ( mbox @
% 188.19/24.33 priorG @
% 188.19/24.33 ( mbox @ priorG @ ( mbox @ priorG @ ( mbox @ c @ ( ws @ c ) ) ) ) ))).
% 188.19/24.33 thf(zf_stmt_0, negated_conjecture,
% 188.19/24.33 (~( mvalid @
% 188.19/24.33 ( mbox @
% 188.19/24.33 priorG @
% 188.19/24.33 ( mbox @ priorG @ ( mbox @ priorG @ ( mbox @ c @ ( ws @ c ) ) ) ) ) )),
% 188.19/24.33 inference('cnf.neg', [status(esa)], [conj])).
% 188.19/24.33 thf(zip_derived_cl34, plain,
% 188.19/24.33 (~ (mvalid @
% 188.19/24.33 (mbox @ priorG @
% 188.19/24.33 (mbox @ priorG @ (mbox @ priorG @ (mbox @ c @ (ws @ c))))))),
% 188.19/24.33 inference('cnf', [status(esa)], [zf_stmt_0])).
% 188.19/24.33 thf(mvalid, axiom, ~ (mvalid @ X0) =>
% 188.19/24.33 ((((!!) @ (^[Y0 : $i]: (X0 @ Y0)))) != ($true))).
% 188.19/24.33 thf('8', plain,
% 188.19/24.33 (![X0:( $i > $o )]:
% 188.19/24.33 ( ( ~( mvalid @ X0 ) ) <=> ( ~( ![X5:$i]: ( X0 @ X5 ) ) ) )),
% 188.19/24.33 inference('rw.lit', [status(esa)], [mvalid])).
% 188.19/24.33 thf(zip_derived_cl43, plain,
% 188.19/24.33 (~ (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (mbox @ priorG @
% 188.19/24.33 (mbox @ priorG @ (mbox @ priorG @ (mbox @ c @ (ws @ c)))) @
% 188.19/24.33 Y0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl34, '8'])).
% 188.19/24.33 thf(zip_derived_cl44, plain,
% 188.19/24.33 (~ (mbox @ priorG @
% 188.19/24.33 (mbox @ priorG @ (mbox @ priorG @ (mbox @ c @ (ws @ c)))) @ '#sk1')),
% 188.19/24.33 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl43])).
% 188.19/24.33 thf(zip_derived_cl45, plain,
% 188.19/24.33 (~ (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (priorG @ '#sk1' @ Y0))) | (mbox @ priorG @
% 188.19/24.33 (mbox @ priorG @ (mbox @ c @ (ws @ c))) @ Y0))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl44, '7'])).
% 188.19/24.33 thf(zip_derived_cl46, plain,
% 188.19/24.33 (~ (((((~) @ (priorG @ '#sk1' @ '#sk2'))) | (mbox @ priorG @
% 188.19/24.33 (mbox @ priorG @ (mbox @ c @ (ws @ c))) @ '#sk2')))),
% 188.19/24.33 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl45])).
% 188.19/24.33 thf(zip_derived_cl48, plain,
% 188.19/24.33 (~ (mbox @ priorG @ (mbox @ priorG @ (mbox @ c @ (ws @ c))) @ '#sk2')),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl46])).
% 188.19/24.33 thf(zip_derived_cl49, plain,
% 188.19/24.33 (~ (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (priorG @ '#sk2' @ Y0))) | (mbox @ priorG @
% 188.19/24.33 (mbox @ c @ (ws @ c)) @ Y0))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl48, '7'])).
% 188.19/24.33 thf(zip_derived_cl50, plain,
% 188.19/24.33 (~ (((((~) @ (priorG @ '#sk2' @ '#sk3'))) | (mbox @ priorG @
% 188.19/24.33 (mbox @ c @ (ws @ c)) @ '#sk3')))),
% 188.19/24.33 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl49])).
% 188.19/24.33 thf(zip_derived_cl52, plain,
% 188.19/24.33 (~ (mbox @ priorG @ (mbox @ c @ (ws @ c)) @ '#sk3')),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl50])).
% 188.19/24.33 thf(zip_derived_cl53, plain,
% 188.19/24.33 (~ (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (priorG @ '#sk3' @ Y0))) | (mbox @ c @
% 188.19/24.33 (ws @ c) @ Y0))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl52, '7'])).
% 188.19/24.33 thf(zip_derived_cl54, plain,
% 188.19/24.33 (~ (((((~) @ (priorG @ '#sk3' @ '#sk4'))) | (mbox @ c @ (ws @ c) @
% 188.19/24.33 '#sk4')))),
% 188.19/24.33 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl53])).
% 188.19/24.33 thf(zip_derived_cl56, plain, (~ (mbox @ c @ (ws @ c) @ '#sk4')),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl54])).
% 188.19/24.33 thf(zip_derived_cl57, plain,
% 188.19/24.33 (~ (((!!) @ (^[Y0 : $i]: (((((~) @ (c @ '#sk4' @ Y0))) | (ws @ c @ Y0))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl56, '7'])).
% 188.19/24.33 thf(zip_derived_cl58, plain,
% 188.19/24.33 (~ (((((~) @ (c @ '#sk4' @ '#sk5'))) | (ws @ c @ '#sk5')))),
% 188.19/24.33 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl57])).
% 188.19/24.33 thf(zip_derived_cl59, plain, ( (c @ '#sk4' @ '#sk5')),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl58])).
% 188.19/24.33 thf(zip_derived_cl14721, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 ( (X0 @ '#sk5') | ~ (a @ '#sk4' @ X1) | ~ (X0 @ ('#sk114' @ X0 @ X1)))),
% 188.19/24.33 inference('sup+', [status(thm)], [zip_derived_cl567, zip_derived_cl59])).
% 188.19/24.33 thf(axiom_4, axiom,
% 188.19/24.33 (mvalid @ ( mbox @ priorG @ ( mnot @ ( mbox @ a @ ( ws @ a ) ) ) ))).
% 188.19/24.33 thf(zip_derived_cl32, plain,
% 188.19/24.33 ( (mvalid @ (mbox @ priorG @ (mnot @ (mbox @ a @ (ws @ a)))))),
% 188.19/24.33 inference('cnf', [status(esa)], [axiom_4])).
% 188.19/24.33 thf(zip_derived_cl61, plain,
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (mbox @ priorG @ (mnot @ (mbox @ a @ (ws @ a))) @ Y0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl32, '0'])).
% 188.19/24.33 thf(zip_derived_cl62, plain,
% 188.19/24.33 (![X2 : $i]: (mbox @ priorG @ (mnot @ (mbox @ a @ (ws @ a))) @ X2)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl61])).
% 188.19/24.33 thf(zip_derived_cl63, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (priorG @ X0 @ Y0))) | (mnot @
% 188.19/24.33 (mbox @ a @ (ws @ a)) @ Y0))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl62, '4'])).
% 188.19/24.33 thf(zip_derived_cl64, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (((((~) @ (priorG @ X0 @ X2))) | (mnot @ (mbox @ a @ (ws @ a)) @ X2)))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl63])).
% 188.19/24.33 thf(zip_derived_cl65, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (~ (priorG @ X0 @ X2) | (mnot @ (mbox @ a @ (ws @ a)) @ X2))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl64])).
% 188.19/24.33 thf(zip_derived_cl66, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 (~ (mbox @ a @ (ws @ a) @ X0) | ~ (priorG @ X1 @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl65, '5'])).
% 188.19/24.33 thf(zip_derived_cl67, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 (~ (((!!) @ (^[Y0 : $i]: (((((~) @ (a @ X0 @ Y0))) | (ws @ a @ Y0))))))
% 188.19/24.33 | ~ (priorG @ X1 @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl66, '7'])).
% 188.19/24.33 thf(zip_derived_cl68, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 (~ (((((~) @ (a @ X0 @ ('#sk6' @ X0)))) | (ws @ a @ ('#sk6' @ X0))))
% 188.19/24.33 | ~ (priorG @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl67])).
% 188.19/24.33 thf(zip_derived_cl70, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]: (~ (ws @ a @ ('#sk6' @ X0)) | ~ (priorG @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl68])).
% 188.19/24.33 thf(zip_derived_cl566, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i > $o]:
% 188.19/24.33 ( (c @ X0 @ ('#sk114' @ X3 @ X0))
% 188.19/24.33 | ~ (a @ X1 @ X0)
% 188.19/24.33 | ~ (c @ X1 @ X2)
% 188.19/24.33 | (X3 @ X2))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl565])).
% 188.19/24.33 thf(zip_derived_cl69, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]: ( (a @ X0 @ ('#sk6' @ X0)) | ~ (priorG @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl68])).
% 188.19/24.33 thf(axiom_3_a_c, axiom,
% 188.19/24.33 (mvalid @
% 188.19/24.33 ( mbox @
% 188.19/24.33 fool @
% 188.19/24.33 ( mimplies @
% 188.19/24.33 ( mnot @ ( ws @ a ) ) @ ( mbox @ c @ ( mnot @ ( ws @ a ) ) ) ) ))).
% 188.19/24.33 thf(zip_derived_cl10, plain,
% 188.19/24.33 ( (mvalid @
% 188.19/24.33 (mbox @ fool @
% 188.19/24.33 (mimplies @ (mnot @ (ws @ a)) @ (mbox @ c @ (mnot @ (ws @ a))))))),
% 188.19/24.33 inference('cnf', [status(esa)], [axiom_3_a_c])).
% 188.19/24.33 thf(zip_derived_cl246, plain,
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (mbox @ fool @
% 188.19/24.33 (mimplies @ (mnot @ (ws @ a)) @
% 188.19/24.33 (mbox @ c @ (mnot @ (ws @ a)))) @
% 188.19/24.33 Y0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl10, '0'])).
% 188.19/24.33 thf(zip_derived_cl247, plain,
% 188.19/24.33 (![X2 : $i]:
% 188.19/24.33 (mbox @ fool @
% 188.19/24.33 (mimplies @ (mnot @ (ws @ a)) @ (mbox @ c @ (mnot @ (ws @ a)))) @ X2)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl246])).
% 188.19/24.33 thf(zip_derived_cl248, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (fool @ X0 @ Y0))) | (mimplies @
% 188.19/24.33 (mnot @ (ws @ a)) @ (mbox @ c @ (mnot @ (ws @ a))) @
% 188.19/24.33 Y0))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl247, '4'])).
% 188.19/24.33 thf(zip_derived_cl249, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (((((~) @ (fool @ X0 @ X2))) | (mimplies @ (mnot @ (ws @ a)) @
% 188.19/24.33 (mbox @ c @ (mnot @ (ws @ a))) @ X2)))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl248])).
% 188.19/24.33 thf(zip_derived_cl250, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (((((~) @ (fool @ X0 @ X2))) | (mor @ (mnot @ (mnot @ (ws @ a))) @
% 188.19/24.33 (mbox @ c @ (mnot @ (ws @ a))) @ X2)))),
% 188.19/24.33 inference('rw', [status(thm)], [zip_derived_cl249, '2'])).
% 188.19/24.33 thf(zip_derived_cl251, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (~ (fool @ X0 @ X2)
% 188.19/24.33 | (mor @ (mnot @ (mnot @ (ws @ a))) @
% 188.19/24.33 (mbox @ c @ (mnot @ (ws @ a))) @ X2))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl250])).
% 188.19/24.33 thf(zip_derived_cl252, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (((mbox @ c @ (mnot @ (ws @ a)) @ X0) | (mnot @ (mnot @ (ws @ a)) @
% 188.19/24.33 X0)))
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl251, '3'])).
% 188.19/24.33 thf(zip_derived_cl253, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (mbox @ c @ (mnot @ (ws @ a)) @ X0)
% 188.19/24.33 | (mnot @ (mnot @ (ws @ a)) @ X0)
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl252])).
% 188.19/24.33 thf(zip_derived_cl254, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (c @ X0 @ Y0))) | (mnot @ (ws @ a) @ Y0))))))
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (mnot @ (mnot @ (ws @ a)) @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl253, '4'])).
% 188.19/24.33 thf(zip_derived_cl255, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 (~ (mnot @ (ws @ a) @ X0)
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (c @ X0 @ Y0))) | (mnot @ (ws @ a) @ Y0)))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl254, '5'])).
% 188.19/24.33 thf(zip_derived_cl256, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (ws @ a @ X0)
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (c @ X0 @ Y0))) | (mnot @ (ws @ a) @ Y0))))))
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl255, '6'])).
% 188.19/24.33 thf(zip_derived_cl257, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X3 : $i]:
% 188.19/24.33 ( (((((~) @ (c @ X0 @ X3))) | (mnot @ (ws @ a) @ X3)))
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (ws @ a @ X0))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl256])).
% 188.19/24.33 thf(zip_derived_cl258, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X3 : $i]:
% 188.19/24.33 (~ (c @ X0 @ X3)
% 188.19/24.33 | (mnot @ (ws @ a) @ X3)
% 188.19/24.33 | (ws @ a @ X0)
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl257])).
% 188.19/24.33 thf(zip_derived_cl259, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i]:
% 188.19/24.33 (~ (ws @ a @ X2)
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (ws @ a @ X0)
% 188.19/24.33 | ~ (c @ X0 @ X2))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl258, '5'])).
% 188.19/24.33 thf(axiom_3_a_b, axiom,
% 188.19/24.33 (mvalid @
% 188.19/24.33 ( mbox @
% 188.19/24.33 fool @
% 188.19/24.33 ( mimplies @
% 188.19/24.33 ( mnot @ ( ws @ a ) ) @ ( mbox @ b @ ( mnot @ ( ws @ a ) ) ) ) ))).
% 188.19/24.33 thf(zip_derived_cl9, plain,
% 188.19/24.33 ( (mvalid @
% 188.19/24.33 (mbox @ fool @
% 188.19/24.33 (mimplies @ (mnot @ (ws @ a)) @ (mbox @ b @ (mnot @ (ws @ a))))))),
% 188.19/24.33 inference('cnf', [status(esa)], [axiom_3_a_b])).
% 188.19/24.33 thf(zip_derived_cl232, plain,
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (mbox @ fool @
% 188.19/24.33 (mimplies @ (mnot @ (ws @ a)) @
% 188.19/24.33 (mbox @ b @ (mnot @ (ws @ a)))) @
% 188.19/24.33 Y0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl9, '0'])).
% 188.19/24.33 thf(zip_derived_cl233, plain,
% 188.19/24.33 (![X2 : $i]:
% 188.19/24.33 (mbox @ fool @
% 188.19/24.33 (mimplies @ (mnot @ (ws @ a)) @ (mbox @ b @ (mnot @ (ws @ a)))) @ X2)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl232])).
% 188.19/24.33 thf(zip_derived_cl234, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (fool @ X0 @ Y0))) | (mimplies @
% 188.19/24.33 (mnot @ (ws @ a)) @ (mbox @ b @ (mnot @ (ws @ a))) @
% 188.19/24.33 Y0))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl233, '4'])).
% 188.19/24.33 thf(zip_derived_cl235, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (((((~) @ (fool @ X0 @ X2))) | (mimplies @ (mnot @ (ws @ a)) @
% 188.19/24.33 (mbox @ b @ (mnot @ (ws @ a))) @ X2)))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl234])).
% 188.19/24.33 thf(zip_derived_cl236, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (((((~) @ (fool @ X0 @ X2))) | (mor @ (mnot @ (mnot @ (ws @ a))) @
% 188.19/24.33 (mbox @ b @ (mnot @ (ws @ a))) @ X2)))),
% 188.19/24.33 inference('rw', [status(thm)], [zip_derived_cl235, '2'])).
% 188.19/24.33 thf(zip_derived_cl237, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (~ (fool @ X0 @ X2)
% 188.19/24.33 | (mor @ (mnot @ (mnot @ (ws @ a))) @
% 188.19/24.33 (mbox @ b @ (mnot @ (ws @ a))) @ X2))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl236])).
% 188.19/24.33 thf(zip_derived_cl238, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (((mbox @ b @ (mnot @ (ws @ a)) @ X0) | (mnot @ (mnot @ (ws @ a)) @
% 188.19/24.33 X0)))
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl237, '3'])).
% 188.19/24.33 thf(zip_derived_cl239, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (mbox @ b @ (mnot @ (ws @ a)) @ X0)
% 188.19/24.33 | (mnot @ (mnot @ (ws @ a)) @ X0)
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl238])).
% 188.19/24.33 thf(zip_derived_cl240, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (b @ X0 @ Y0))) | (mnot @ (ws @ a) @ Y0))))))
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (mnot @ (mnot @ (ws @ a)) @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl239, '4'])).
% 188.19/24.33 thf(zip_derived_cl241, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 (~ (mnot @ (ws @ a) @ X0)
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (b @ X0 @ Y0))) | (mnot @ (ws @ a) @ Y0)))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl240, '5'])).
% 188.19/24.33 thf(zip_derived_cl242, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (ws @ a @ X0)
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (b @ X0 @ Y0))) | (mnot @ (ws @ a) @ Y0))))))
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl241, '6'])).
% 188.19/24.33 thf(zip_derived_cl243, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X3 : $i]:
% 188.19/24.33 ( (((((~) @ (b @ X0 @ X3))) | (mnot @ (ws @ a) @ X3)))
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (ws @ a @ X0))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl242])).
% 188.19/24.33 thf(zip_derived_cl244, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X3 : $i]:
% 188.19/24.33 (~ (b @ X0 @ X3)
% 188.19/24.33 | (mnot @ (ws @ a) @ X3)
% 188.19/24.33 | (ws @ a @ X0)
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl243])).
% 188.19/24.33 thf(zip_derived_cl245, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i]:
% 188.19/24.33 (~ (ws @ a @ X2)
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (ws @ a @ X0)
% 188.19/24.33 | ~ (b @ X0 @ X2))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl244, '5'])).
% 188.19/24.33 thf(axiom_2_a_c, axiom,
% 188.19/24.33 (mvalid @
% 188.19/24.33 ( mbox @ fool @ ( mimplies @ ( ws @ a ) @ ( mbox @ c @ ( ws @ a ) ) ) ))).
% 188.19/24.33 thf(zip_derived_cl4, plain,
% 188.19/24.33 ( (mvalid @ (mbox @ fool @ (mimplies @ (ws @ a) @ (mbox @ c @ (ws @ a)))))),
% 188.19/24.33 inference('cnf', [status(esa)], [axiom_2_a_c])).
% 188.19/24.33 thf(zip_derived_cl96, plain,
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (mbox @ fool @
% 188.19/24.33 (mimplies @ (ws @ a) @ (mbox @ c @ (ws @ a))) @ Y0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl4, '0'])).
% 188.19/24.33 thf(zip_derived_cl97, plain,
% 188.19/24.33 (![X2 : $i]:
% 188.19/24.33 (mbox @ fool @ (mimplies @ (ws @ a) @ (mbox @ c @ (ws @ a))) @ X2)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl96])).
% 188.19/24.33 thf(zip_derived_cl98, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (fool @ X0 @ Y0))) | (mimplies @ (ws @ a) @
% 188.19/24.33 (mbox @ c @ (ws @ a)) @ Y0))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl97, '4'])).
% 188.19/24.33 thf(zip_derived_cl99, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (((((~) @ (fool @ X0 @ X2))) | (mimplies @ (ws @ a) @
% 188.19/24.33 (mbox @ c @ (ws @ a)) @ X2)))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl98])).
% 188.19/24.33 thf(zip_derived_cl100, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (((((~) @ (fool @ X0 @ X2))) | (mor @ (mnot @ (ws @ a)) @
% 188.19/24.33 (mbox @ c @ (ws @ a)) @ X2)))),
% 188.19/24.33 inference('rw', [status(thm)], [zip_derived_cl99, '2'])).
% 188.19/24.33 thf(zip_derived_cl101, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (~ (fool @ X0 @ X2)
% 188.19/24.33 | (mor @ (mnot @ (ws @ a)) @ (mbox @ c @ (ws @ a)) @ X2))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl100])).
% 188.19/24.33 thf(zip_derived_cl102, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (((mbox @ c @ (ws @ a) @ X0) | (mnot @ (ws @ a) @ X0)))
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl101, '3'])).
% 188.19/24.33 thf(zip_derived_cl103, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (mbox @ c @ (ws @ a) @ X0)
% 188.19/24.33 | (mnot @ (ws @ a) @ X0)
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl102])).
% 188.19/24.33 thf(zip_derived_cl104, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]: (((((~) @ (c @ X0 @ Y0))) | (ws @ a @ Y0))))))
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (mnot @ (ws @ a) @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl103, '4'])).
% 188.19/24.33 thf(zip_derived_cl105, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 (~ (ws @ a @ X0)
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]: (((((~) @ (c @ X0 @ Y0))) | (ws @ a @ Y0)))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl104, '5'])).
% 188.19/24.33 thf(zip_derived_cl106, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X3 : $i]:
% 188.19/24.33 ( (((((~) @ (c @ X0 @ X3))) | (ws @ a @ X3)))
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | ~ (ws @ a @ X0))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl105])).
% 188.19/24.33 thf(zip_derived_cl107, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X3 : $i]:
% 188.19/24.33 (~ (c @ X0 @ X3)
% 188.19/24.33 | (ws @ a @ X3)
% 188.19/24.33 | ~ (ws @ a @ X0)
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl106])).
% 188.19/24.33 thf(axiom_5, axiom,
% 188.19/24.33 (mvalid @
% 188.19/24.33 ( mbox @ priorG @ ( mbox @ priorG @ ( mnot @ ( mbox @ b @ ( ws @ b ) ) ) ) ))).
% 188.19/24.33 thf(zip_derived_cl33, plain,
% 188.19/24.33 ( (mvalid @
% 188.19/24.33 (mbox @ priorG @ (mbox @ priorG @ (mnot @ (mbox @ b @ (ws @ b))))))),
% 188.19/24.33 inference('cnf', [status(esa)], [axiom_5])).
% 188.19/24.33 thf(zip_derived_cl165, plain,
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (mbox @ priorG @
% 188.19/24.33 (mbox @ priorG @ (mnot @ (mbox @ b @ (ws @ b)))) @ Y0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl33, '0'])).
% 188.19/24.33 thf(zip_derived_cl166, plain,
% 188.19/24.33 (![X2 : $i]:
% 188.19/24.33 (mbox @ priorG @ (mbox @ priorG @ (mnot @ (mbox @ b @ (ws @ b)))) @
% 188.19/24.33 X2)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl165])).
% 188.19/24.33 thf(zip_derived_cl167, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (priorG @ X0 @ Y0))) | (mbox @ priorG @
% 188.19/24.33 (mnot @ (mbox @ b @ (ws @ b))) @ Y0))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl166, '4'])).
% 188.19/24.33 thf(zip_derived_cl168, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (((((~) @ (priorG @ X0 @ X2))) | (mbox @ priorG @
% 188.19/24.33 (mnot @ (mbox @ b @ (ws @ b))) @ X2)))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl167])).
% 188.19/24.33 thf(zip_derived_cl169, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (~ (priorG @ X0 @ X2)
% 188.19/24.33 | (mbox @ priorG @ (mnot @ (mbox @ b @ (ws @ b))) @ X2))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl168])).
% 188.19/24.33 thf(zip_derived_cl170, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (priorG @ X0 @ Y0))) | (mnot @
% 188.19/24.33 (mbox @ b @ (ws @ b)) @ Y0))))))
% 188.19/24.33 | ~ (priorG @ X1 @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl169, '4'])).
% 188.19/24.33 thf(zip_derived_cl171, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X3 : $i]:
% 188.19/24.33 ( (((((~) @ (priorG @ X0 @ X3))) | (mnot @ (mbox @ b @ (ws @ b)) @ X3)))
% 188.19/24.33 | ~ (priorG @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl170])).
% 188.19/24.33 thf(zip_derived_cl172, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X3 : $i]:
% 188.19/24.33 (~ (priorG @ X0 @ X3)
% 188.19/24.33 | (mnot @ (mbox @ b @ (ws @ b)) @ X3)
% 188.19/24.33 | ~ (priorG @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl171])).
% 188.19/24.33 thf(zip_derived_cl173, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i]:
% 188.19/24.33 (~ (mbox @ b @ (ws @ b) @ X2)
% 188.19/24.33 | ~ (priorG @ X1 @ X0)
% 188.19/24.33 | ~ (priorG @ X0 @ X2))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl172, '5'])).
% 188.19/24.33 thf(zip_derived_cl174, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i]:
% 188.19/24.33 (~ (((!!) @ (^[Y0 : $i]: (((((~) @ (b @ X0 @ Y0))) | (ws @ b @ Y0))))))
% 188.19/24.33 | ~ (priorG @ X1 @ X0)
% 188.19/24.33 | ~ (priorG @ X2 @ X1))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl173, '7'])).
% 188.19/24.33 thf(zip_derived_cl175, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i]:
% 188.19/24.33 (~ (((((~) @ (b @ X0 @ ('#sk21' @ X0)))) | (ws @ b @ ('#sk21' @ X0))))
% 188.19/24.33 | ~ (priorG @ X2 @ X1)
% 188.19/24.33 | ~ (priorG @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl174])).
% 188.19/24.33 thf(zip_derived_cl177, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i]:
% 188.19/24.33 (~ (ws @ b @ ('#sk21' @ X0))
% 188.19/24.33 | ~ (priorG @ X1 @ X0)
% 188.19/24.33 | ~ (priorG @ X2 @ X1))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl175])).
% 188.19/24.33 thf(zip_derived_cl60, plain, (~ (ws @ c @ '#sk5')),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl58])).
% 188.19/24.33 thf(i_axiom_for_fool_c, axiom,
% 188.19/24.33 (mvalid @
% 188.19/24.33 ( mforall_prop @
% 188.19/24.33 ( ^[Phi:( $i > $o )]:
% 188.19/24.33 ( mimplies @ ( mbox @ fool @ Phi ) @ ( mbox @ c @ Phi ) ) ) ))).
% 188.19/24.33 thf(zip_derived_cl19, plain,
% 188.19/24.33 ( (mvalid @
% 188.19/24.33 (mforall_prop @
% 188.19/24.33 (^[Y0 : $i > $o]: (mimplies @ (mbox @ fool @ Y0) @ (mbox @ c @ Y0)))))),
% 188.19/24.33 inference('cnf', [status(esa)], [i_axiom_for_fool_c])).
% 188.19/24.33 thf(zip_derived_cl214, plain,
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (mforall_prop @
% 188.19/24.33 (^[Y1 : $i > $o]:
% 188.19/24.33 (mimplies @ (mbox @ fool @ Y1) @ (mbox @ c @ Y1))) @
% 188.19/24.33 Y0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl19, '0'])).
% 188.19/24.33 thf(zip_derived_cl215, plain,
% 188.19/24.33 (![X2 : $i]:
% 188.19/24.33 (mforall_prop @
% 188.19/24.33 (^[Y0 : $i > $o]: (mimplies @ (mbox @ fool @ Y0) @ (mbox @ c @ Y0))) @
% 188.19/24.33 X2)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl214])).
% 188.19/24.33 thf(zip_derived_cl216, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i > $o]:
% 188.19/24.33 ((^[Y1 : $i > $o]:
% 188.19/24.33 (mimplies @ (mbox @ fool @ Y1) @ (mbox @ c @ Y1))) @
% 188.19/24.33 Y0 @ X0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl215, '1'])).
% 188.19/24.33 thf(zip_derived_cl217, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i > $o]:
% 188.19/24.33 (mimplies @ (mbox @ fool @ Y0) @ (mbox @ c @ Y0) @ X0))))),
% 188.19/24.33 inference('ho_norm', [status(thm)], [zip_derived_cl216])).
% 188.19/24.33 thf(zip_derived_cl218, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i > $o]:
% 188.19/24.33 (mimplies @ (mbox @ fool @ X2) @ (mbox @ c @ X2) @ X0)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl217])).
% 188.19/24.33 thf(zip_derived_cl219, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i > $o]:
% 188.19/24.33 (mor @ (mnot @ (mbox @ fool @ X2)) @ (mbox @ c @ X2) @ X0)),
% 188.19/24.33 inference('rw', [status(thm)], [zip_derived_cl218, '2'])).
% 188.19/24.33 thf(zip_derived_cl220, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 (((mbox @ c @ X0 @ X1) | (mnot @ (mbox @ fool @ X0) @ X1)))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl219, '3'])).
% 188.19/24.33 thf(zip_derived_cl221, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 ( (mbox @ c @ X0 @ X1) | (mnot @ (mbox @ fool @ X0) @ X1))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl220])).
% 188.19/24.33 thf(zip_derived_cl222, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i > $o]:
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]: (((((~) @ (c @ X0 @ Y0))) | (X1 @ Y0))))))
% 188.19/24.33 | (mnot @ (mbox @ fool @ X1) @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl221, '4'])).
% 188.19/24.33 thf(zip_derived_cl223, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 (~ (mbox @ fool @ X0 @ X1)
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]: (((((~) @ (c @ X1 @ Y0))) | (X0 @ Y0)))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl222, '5'])).
% 188.19/24.33 thf(zip_derived_cl224, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 (~ (((!!) @ (^[Y0 : $i]: (((((~) @ (fool @ X1 @ Y0))) | (X0 @ Y0))))))
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]: (((((~) @ (c @ X1 @ Y0))) | (X0 @ Y0)))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl223, '7'])).
% 188.19/24.33 thf(zip_derived_cl225, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 (~ (((((~) @ (fool @ X1 @ ('#sk15' @ X0 @ X1)))) | (X0 @
% 188.19/24.33 ('#sk15' @ X0 @ X1))))
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]: (((((~) @ (c @ X1 @ Y0))) | (X0 @ Y0)))))))),
% 188.19/24.33 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl224])).
% 188.19/24.33 thf(zip_derived_cl227, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 (~ (X0 @ ('#sk15' @ X0 @ X1))
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]: (((((~) @ (c @ X1 @ Y0))) | (X0 @ Y0)))))))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl225])).
% 188.19/24.33 thf(zip_derived_cl229, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i, X3 : $i]:
% 188.19/24.33 ( (((((~) @ (c @ X1 @ X3))) | (X0 @ X3)))
% 188.19/24.33 | ~ (X0 @ ('#sk15' @ X0 @ X1)))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl227])).
% 188.19/24.33 thf(zip_derived_cl231, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i, X3 : $i]:
% 188.19/24.33 (~ (c @ X1 @ X3) | (X0 @ X3) | ~ (X0 @ ('#sk15' @ X0 @ X1)))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl229])).
% 188.19/24.33 thf(zip_derived_cl59, plain, ( (c @ '#sk4' @ '#sk5')),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl58])).
% 188.19/24.33 thf(zip_derived_cl3928, plain,
% 188.19/24.33 (![X0 : $i > $o]: (~ (X0 @ ('#sk15' @ X0 @ '#sk4')) | (X0 @ '#sk5'))),
% 188.19/24.33 inference('sup+', [status(thm)], [zip_derived_cl231, zip_derived_cl59])).
% 188.19/24.33 thf(zip_derived_cl55, plain, ( (priorG @ '#sk3' @ '#sk4')),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl54])).
% 188.19/24.33 thf(zip_derived_cl226, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 ( (fool @ X1 @ ('#sk15' @ X0 @ X1))
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]: (((((~) @ (c @ X1 @ Y0))) | (X0 @ Y0)))))))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl225])).
% 188.19/24.33 thf(zip_derived_cl228, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i, X3 : $i]:
% 188.19/24.33 ( (((((~) @ (c @ X1 @ X3))) | (X0 @ X3)))
% 188.19/24.33 | (fool @ X1 @ ('#sk15' @ X0 @ X1)))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl226])).
% 188.19/24.33 thf(zip_derived_cl230, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i, X3 : $i]:
% 188.19/24.33 (~ (c @ X1 @ X3) | (X0 @ X3) | (fool @ X1 @ ('#sk15' @ X0 @ X1)))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl228])).
% 188.19/24.33 thf(zip_derived_cl51, plain, ( (priorG @ '#sk2' @ '#sk3')),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl50])).
% 188.19/24.33 thf(zip_derived_cl59, plain, ( (c @ '#sk4' @ '#sk5')),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl58])).
% 188.19/24.33 thf(axiom_3_c_b, axiom,
% 188.19/24.33 (mvalid @
% 188.19/24.33 ( mbox @
% 188.19/24.33 fool @
% 188.19/24.33 ( mimplies @
% 188.19/24.33 ( mnot @ ( ws @ c ) ) @ ( mbox @ b @ ( mnot @ ( ws @ c ) ) ) ) ))).
% 188.19/24.33 thf(zip_derived_cl14, plain,
% 188.19/24.33 ( (mvalid @
% 188.19/24.33 (mbox @ fool @
% 188.19/24.33 (mimplies @ (mnot @ (ws @ c)) @ (mbox @ b @ (mnot @ (ws @ c))))))),
% 188.19/24.33 inference('cnf', [status(esa)], [axiom_3_c_b])).
% 188.19/24.33 thf(zip_derived_cl350, plain,
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (mbox @ fool @
% 188.19/24.33 (mimplies @ (mnot @ (ws @ c)) @
% 188.19/24.33 (mbox @ b @ (mnot @ (ws @ c)))) @
% 188.19/24.33 Y0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl14, '0'])).
% 188.19/24.33 thf(zip_derived_cl351, plain,
% 188.19/24.33 (![X2 : $i]:
% 188.19/24.33 (mbox @ fool @
% 188.19/24.33 (mimplies @ (mnot @ (ws @ c)) @ (mbox @ b @ (mnot @ (ws @ c)))) @ X2)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl350])).
% 188.19/24.33 thf(zip_derived_cl352, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (fool @ X0 @ Y0))) | (mimplies @
% 188.19/24.33 (mnot @ (ws @ c)) @ (mbox @ b @ (mnot @ (ws @ c))) @
% 188.19/24.33 Y0))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl351, '4'])).
% 188.19/24.33 thf(zip_derived_cl353, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (((((~) @ (fool @ X0 @ X2))) | (mimplies @ (mnot @ (ws @ c)) @
% 188.19/24.33 (mbox @ b @ (mnot @ (ws @ c))) @ X2)))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl352])).
% 188.19/24.33 thf(zip_derived_cl354, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (((((~) @ (fool @ X0 @ X2))) | (mor @ (mnot @ (mnot @ (ws @ c))) @
% 188.19/24.33 (mbox @ b @ (mnot @ (ws @ c))) @ X2)))),
% 188.19/24.33 inference('rw', [status(thm)], [zip_derived_cl353, '2'])).
% 188.19/24.33 thf(zip_derived_cl355, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (~ (fool @ X0 @ X2)
% 188.19/24.33 | (mor @ (mnot @ (mnot @ (ws @ c))) @
% 188.19/24.33 (mbox @ b @ (mnot @ (ws @ c))) @ X2))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl354])).
% 188.19/24.33 thf(zip_derived_cl356, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (((mbox @ b @ (mnot @ (ws @ c)) @ X0) | (mnot @ (mnot @ (ws @ c)) @
% 188.19/24.33 X0)))
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl355, '3'])).
% 188.19/24.33 thf(zip_derived_cl357, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (mbox @ b @ (mnot @ (ws @ c)) @ X0)
% 188.19/24.33 | (mnot @ (mnot @ (ws @ c)) @ X0)
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl356])).
% 188.19/24.33 thf(zip_derived_cl358, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (b @ X0 @ Y0))) | (mnot @ (ws @ c) @ Y0))))))
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (mnot @ (mnot @ (ws @ c)) @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl357, '4'])).
% 188.19/24.33 thf(zip_derived_cl359, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 (~ (mnot @ (ws @ c) @ X0)
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (b @ X0 @ Y0))) | (mnot @ (ws @ c) @ Y0)))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl358, '5'])).
% 188.19/24.33 thf(zip_derived_cl360, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (ws @ c @ X0)
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (b @ X0 @ Y0))) | (mnot @ (ws @ c) @ Y0))))))
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl359, '6'])).
% 188.19/24.33 thf(zip_derived_cl361, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X3 : $i]:
% 188.19/24.33 ( (((((~) @ (b @ X0 @ X3))) | (mnot @ (ws @ c) @ X3)))
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (ws @ c @ X0))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl360])).
% 188.19/24.33 thf(zip_derived_cl362, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X3 : $i]:
% 188.19/24.33 (~ (b @ X0 @ X3)
% 188.19/24.33 | (mnot @ (ws @ c) @ X3)
% 188.19/24.33 | (ws @ c @ X0)
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl361])).
% 188.19/24.33 thf(zip_derived_cl363, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i]:
% 188.19/24.33 (~ (ws @ c @ X2)
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (ws @ c @ X0)
% 188.19/24.33 | ~ (b @ X0 @ X2))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl362, '5'])).
% 188.19/24.33 thf(t_axiom_for_fool, axiom,
% 188.19/24.33 (mvalid @
% 188.19/24.33 ( mforall_prop @
% 188.19/24.33 ( ^[A:( $i > $o )]: ( mimplies @ ( mbox @ fool @ A ) @ A ) ) ))).
% 188.19/24.33 thf(zip_derived_cl15, plain,
% 188.19/24.33 ( (mvalid @
% 188.19/24.33 (mforall_prop @
% 188.19/24.33 (^[Y0 : $i > $o]: (mimplies @ (mbox @ fool @ Y0) @ Y0))))),
% 188.19/24.33 inference('cnf', [status(esa)], [t_axiom_for_fool])).
% 188.19/24.33 thf(zip_derived_cl71, plain,
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (mforall_prop @
% 188.19/24.33 (^[Y1 : $i > $o]: (mimplies @ (mbox @ fool @ Y1) @ Y1)) @
% 188.19/24.33 Y0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl15, '0'])).
% 188.19/24.33 thf(zip_derived_cl72, plain,
% 188.19/24.33 (![X2 : $i]:
% 188.19/24.33 (mforall_prop @
% 188.19/24.33 (^[Y0 : $i > $o]: (mimplies @ (mbox @ fool @ Y0) @ Y0)) @ X2)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl71])).
% 188.19/24.33 thf(zip_derived_cl73, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i > $o]:
% 188.19/24.33 ((^[Y1 : $i > $o]: (mimplies @ (mbox @ fool @ Y1) @ Y1)) @
% 188.19/24.33 Y0 @ X0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl72, '1'])).
% 188.19/24.33 thf(zip_derived_cl74, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i > $o]: (mimplies @ (mbox @ fool @ Y0) @ Y0 @ X0))))),
% 188.19/24.33 inference('ho_norm', [status(thm)], [zip_derived_cl73])).
% 188.19/24.33 thf(zip_derived_cl75, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i > $o]: (mimplies @ (mbox @ fool @ X2) @ X2 @ X0)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl74])).
% 188.19/24.33 thf(zip_derived_cl76, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i > $o]: (mor @ (mnot @ (mbox @ fool @ X2)) @ X2 @ X0)),
% 188.19/24.33 inference('rw', [status(thm)], [zip_derived_cl75, '2'])).
% 188.19/24.33 thf(zip_derived_cl77, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 (((X0 @ X1) | (mnot @ (mbox @ fool @ X0) @ X1)))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl76, '3'])).
% 188.19/24.33 thf(zip_derived_cl78, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 ( (X0 @ X1) | (mnot @ (mbox @ fool @ X0) @ X1))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl77])).
% 188.19/24.33 thf(zip_derived_cl79, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]: (~ (mbox @ fool @ X0 @ X1) | (X0 @ X1))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl78, '5'])).
% 188.19/24.33 thf(zip_derived_cl80, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 (~ (((!!) @ (^[Y0 : $i]: (((((~) @ (fool @ X1 @ Y0))) | (X0 @ Y0))))))
% 188.19/24.33 | (X0 @ X1))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl79, '7'])).
% 188.19/24.33 thf(zip_derived_cl81, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 (~ (((((~) @ (fool @ X1 @ ('#sk15' @ X0 @ X1)))) | (X0 @
% 188.19/24.33 ('#sk15' @ X0 @ X1))))
% 188.19/24.33 | (X0 @ X1))),
% 188.19/24.33 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl80])).
% 188.19/24.33 thf(zip_derived_cl82, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 ( (fool @ X1 @ ('#sk15' @ X0 @ X1)) | (X0 @ X1))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl81])).
% 188.19/24.33 thf(axiom_1, axiom,
% 188.19/24.33 (mvalid @
% 188.19/24.33 ( mbox @ fool @ ( mor @ ( ws @ a ) @ ( mor @ ( ws @ b ) @ ( ws @ c ) ) ) ))).
% 188.19/24.33 thf(zip_derived_cl2, plain,
% 188.19/24.33 ( (mvalid @
% 188.19/24.33 (mbox @ fool @ (mor @ (ws @ a) @ (mor @ (ws @ b) @ (ws @ c)))))),
% 188.19/24.33 inference('cnf', [status(esa)], [axiom_1])).
% 188.19/24.33 thf(zip_derived_cl108, plain,
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (mbox @ fool @
% 188.19/24.33 (mor @ (ws @ a) @ (mor @ (ws @ b) @ (ws @ c))) @ Y0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl2, '0'])).
% 188.19/24.33 thf(zip_derived_cl109, plain,
% 188.19/24.33 (![X2 : $i]:
% 188.19/24.33 (mbox @ fool @ (mor @ (ws @ a) @ (mor @ (ws @ b) @ (ws @ c))) @ X2)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl108])).
% 188.19/24.33 thf(zip_derived_cl110, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (fool @ X0 @ Y0))) | (mor @ (ws @ a) @
% 188.19/24.33 (mor @ (ws @ b) @ (ws @ c)) @ Y0))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl109, '4'])).
% 188.19/24.33 thf(zip_derived_cl111, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (((((~) @ (fool @ X0 @ X2))) | (mor @ (ws @ a) @
% 188.19/24.33 (mor @ (ws @ b) @ (ws @ c)) @ X2)))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl110])).
% 188.19/24.33 thf(zip_derived_cl112, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i]:
% 188.19/24.33 (~ (fool @ X0 @ X2)
% 188.19/24.33 | (mor @ (ws @ a) @ (mor @ (ws @ b) @ (ws @ c)) @ X2))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl111])).
% 188.19/24.33 thf(zip_derived_cl113, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (((mor @ (ws @ b) @ (ws @ c) @ X0) | (ws @ a @ X0)))
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl112, '3'])).
% 188.19/24.33 thf(zip_derived_cl114, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (mor @ (ws @ b) @ (ws @ c) @ X0)
% 188.19/24.33 | (ws @ a @ X0)
% 188.19/24.33 | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl113])).
% 188.19/24.33 thf(zip_derived_cl115, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (((ws @ c @ X0) | (ws @ b @ X0)))
% 188.19/24.33 | ~ (fool @ X1 @ X0)
% 188.19/24.33 | (ws @ a @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl114, '3'])).
% 188.19/24.33 thf(zip_derived_cl116, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i]:
% 188.19/24.33 ( (ws @ c @ X0) | (ws @ b @ X0) | (ws @ a @ X0) | ~ (fool @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl115])).
% 188.19/24.33 thf(a6_axiom_for_fool_b_c, axiom,
% 188.19/24.33 (mvalid @
% 188.19/24.33 ( mforall_prop @
% 188.19/24.33 ( ^[Phi:( $i > $o )]:
% 188.19/24.33 ( mimplies @
% 188.19/24.33 ( mnot @ ( mbox @ b @ Phi ) ) @
% 188.19/24.33 ( mbox @ c @ ( mnot @ ( mbox @ b @ Phi ) ) ) ) ) ))).
% 188.19/24.33 thf(zip_derived_cl29, plain,
% 188.19/24.33 ( (mvalid @
% 188.19/24.33 (mforall_prop @
% 188.19/24.33 (^[Y0 : $i > $o]:
% 188.19/24.33 (mimplies @ (mnot @ (mbox @ b @ Y0)) @
% 188.19/24.33 (mbox @ c @ (mnot @ (mbox @ b @ Y0)))))))),
% 188.19/24.33 inference('cnf', [status(esa)], [a6_axiom_for_fool_b_c])).
% 188.19/24.33 thf(zip_derived_cl589, plain,
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (mforall_prop @
% 188.19/24.33 (^[Y1 : $i > $o]:
% 188.19/24.33 (mimplies @ (mnot @ (mbox @ b @ Y1)) @
% 188.19/24.33 (mbox @ c @ (mnot @ (mbox @ b @ Y1))))) @
% 188.19/24.33 Y0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl29, '0'])).
% 188.19/24.33 thf(zip_derived_cl590, plain,
% 188.19/24.33 (![X2 : $i]:
% 188.19/24.33 (mforall_prop @
% 188.19/24.33 (^[Y0 : $i > $o]:
% 188.19/24.33 (mimplies @ (mnot @ (mbox @ b @ Y0)) @
% 188.19/24.33 (mbox @ c @ (mnot @ (mbox @ b @ Y0))))) @
% 188.19/24.33 X2)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl589])).
% 188.19/24.33 thf(zip_derived_cl591, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i > $o]:
% 188.19/24.33 ((^[Y1 : $i > $o]:
% 188.19/24.33 (mimplies @ (mnot @ (mbox @ b @ Y1)) @
% 188.19/24.33 (mbox @ c @ (mnot @ (mbox @ b @ Y1))))) @
% 188.19/24.33 Y0 @ X0))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl590, '1'])).
% 188.19/24.33 thf(zip_derived_cl592, plain,
% 188.19/24.33 (![X0 : $i]:
% 188.19/24.33 (((!!) @ (^[Y0 : $i > $o]:
% 188.19/24.33 (mimplies @ (mnot @ (mbox @ b @ Y0)) @
% 188.19/24.33 (mbox @ c @ (mnot @ (mbox @ b @ Y0))) @ X0))))),
% 188.19/24.33 inference('ho_norm', [status(thm)], [zip_derived_cl591])).
% 188.19/24.33 thf(zip_derived_cl593, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i > $o]:
% 188.19/24.33 (mimplies @ (mnot @ (mbox @ b @ X2)) @
% 188.19/24.33 (mbox @ c @ (mnot @ (mbox @ b @ X2))) @ X0)),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl592])).
% 188.19/24.33 thf(zip_derived_cl594, plain,
% 188.19/24.33 (![X0 : $i, X2 : $i > $o]:
% 188.19/24.33 (mor @ (mnot @ (mnot @ (mbox @ b @ X2))) @
% 188.19/24.33 (mbox @ c @ (mnot @ (mbox @ b @ X2))) @ X0)),
% 188.19/24.33 inference('rw', [status(thm)], [zip_derived_cl593, '2'])).
% 188.19/24.33 thf(zip_derived_cl595, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 (((mbox @ c @ (mnot @ (mbox @ b @ X0)) @ X1) | (mnot @
% 188.19/24.33 (mnot @ (mbox @ b @ X0)) @ X1)))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl594, '3'])).
% 188.19/24.33 thf(zip_derived_cl596, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 ( (mbox @ c @ (mnot @ (mbox @ b @ X0)) @ X1)
% 188.19/24.33 | (mnot @ (mnot @ (mbox @ b @ X0)) @ X1))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl595])).
% 188.19/24.33 thf(zip_derived_cl597, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i > $o]:
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (c @ X0 @ Y0))) | (mnot @ (mbox @ b @ X1) @
% 188.19/24.33 Y0))))))
% 188.19/24.33 | (mnot @ (mnot @ (mbox @ b @ X1)) @ X0))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl596, '4'])).
% 188.19/24.33 thf(zip_derived_cl598, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 (~ (mnot @ (mbox @ b @ X0) @ X1)
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (c @ X1 @ Y0))) | (mnot @ (mbox @ b @ X0) @
% 188.19/24.33 Y0)))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl597, '5'])).
% 188.19/24.33 thf(zip_derived_cl599, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 ( (mbox @ b @ X0 @ X1)
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (c @ X1 @ Y0))) | (mnot @ (mbox @ b @ X0) @
% 188.19/24.33 Y0)))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl598, '6'])).
% 188.19/24.33 thf(zip_derived_cl600, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 ( (((!!) @ (^[Y0 : $i]: (((((~) @ (b @ X1 @ Y0))) | (X0 @ Y0))))))
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (c @ X1 @ Y0))) | (mnot @ (mbox @ b @ X0) @
% 188.19/24.33 Y0)))))))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl599, '4'])).
% 188.19/24.33 thf(zip_derived_cl601, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i, X3 : $i]:
% 188.19/24.33 ( (((((~) @ (b @ X1 @ X3))) | (X0 @ X3)))
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (c @ X1 @ Y0))) | (mnot @ (mbox @ b @ X0) @
% 188.19/24.33 Y0)))))))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl600])).
% 188.19/24.33 thf(zip_derived_cl602, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i, X3 : $i]:
% 188.19/24.33 (~ (b @ X1 @ X3)
% 188.19/24.33 | (X0 @ X3)
% 188.19/24.33 | (((!!) @ (^[Y0 : $i]:
% 188.19/24.33 (((((~) @ (c @ X1 @ Y0))) | (mnot @ (mbox @ b @ X0) @
% 188.19/24.33 Y0)))))))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl601])).
% 188.19/24.33 thf(zip_derived_cl603, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i, X3 : $i, X5 : $i]:
% 188.19/24.33 ( (((((~) @ (c @ X1 @ X5))) | (mnot @ (mbox @ b @ X0) @ X5)))
% 188.19/24.33 | (X0 @ X3)
% 188.19/24.33 | ~ (b @ X1 @ X3))),
% 188.19/24.33 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl602])).
% 188.19/24.33 thf(zip_derived_cl604, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i, X3 : $i, X5 : $i]:
% 188.19/24.33 (~ (c @ X1 @ X5)
% 188.19/24.33 | (mnot @ (mbox @ b @ X0) @ X5)
% 188.19/24.33 | ~ (b @ X1 @ X3)
% 188.19/24.33 | (X0 @ X3))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl603])).
% 188.19/24.33 thf(zip_derived_cl605, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i, X2 : $i, X3 : $i]:
% 188.19/24.33 (~ (mbox @ b @ X0 @ X3)
% 188.19/24.33 | (X0 @ X1)
% 188.19/24.33 | ~ (b @ X2 @ X1)
% 188.19/24.33 | ~ (c @ X2 @ X3))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl604, '5'])).
% 188.19/24.33 thf(zip_derived_cl606, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i > $o]:
% 188.19/24.33 (~ (((!!) @ (^[Y0 : $i]: (((((~) @ (b @ X0 @ Y0))) | (X3 @ Y0))))))
% 188.19/24.33 | ~ (c @ X1 @ X0)
% 188.19/24.33 | ~ (b @ X1 @ X2)
% 188.19/24.33 | (X3 @ X2))),
% 188.19/24.33 inference('rw_clause', [status(thm)], [zip_derived_cl605, '7'])).
% 188.19/24.33 thf(zip_derived_cl607, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i > $o]:
% 188.19/24.33 (~ (((((~) @ (b @ X0 @ ('#sk306' @ X3 @ X0)))) | (X3 @
% 188.19/24.33 ('#sk306' @ X3 @ X0))))
% 188.19/24.33 | (X3 @ X2)
% 188.19/24.33 | ~ (b @ X1 @ X2)
% 188.19/24.33 | ~ (c @ X1 @ X0))),
% 188.19/24.33 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl606])).
% 188.19/24.33 thf(zip_derived_cl609, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i > $o]:
% 188.19/24.33 (~ (X3 @ ('#sk306' @ X3 @ X0))
% 188.19/24.33 | ~ (c @ X1 @ X0)
% 188.19/24.33 | ~ (b @ X1 @ X2)
% 188.19/24.33 | (X3 @ X2))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl607])).
% 188.19/24.33 thf(zip_derived_cl59, plain, ( (c @ '#sk4' @ '#sk5')),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl58])).
% 188.19/24.33 thf(zip_derived_cl17000, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]:
% 188.19/24.33 ( (X0 @ X1) | ~ (b @ '#sk4' @ X1) | ~ (X0 @ ('#sk306' @ X0 @ '#sk5')))),
% 188.19/24.33 inference('sup+', [status(thm)], [zip_derived_cl609, zip_derived_cl59])).
% 188.19/24.33 thf(zip_derived_cl176, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i]:
% 188.19/24.33 ( (b @ X0 @ ('#sk21' @ X0))
% 188.19/24.33 | ~ (priorG @ X1 @ X0)
% 188.19/24.33 | ~ (priorG @ X2 @ X1))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl175])).
% 188.19/24.33 thf(zip_derived_cl608, plain,
% 188.19/24.33 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i > $o]:
% 188.19/24.33 ( (b @ X0 @ ('#sk306' @ X3 @ X0))
% 188.19/24.33 | ~ (c @ X1 @ X0)
% 188.19/24.33 | ~ (b @ X1 @ X2)
% 188.19/24.33 | (X3 @ X2))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl607])).
% 188.19/24.33 thf(zip_derived_cl83, plain,
% 188.19/24.33 (![X0 : $i > $o, X1 : $i]: (~ (X0 @ ('#sk15' @ X0 @ X1)) | (X0 @ X1))),
% 188.19/24.33 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl81])).
% 188.19/24.33 thf(zip_derived_cl17351, plain, ($false),
% 188.19/24.33 inference('eprover', [status(thm)],
% 188.19/24.33 [zip_derived_cl14721, zip_derived_cl70, zip_derived_cl566,
% 188.19/24.33 zip_derived_cl69, zip_derived_cl259, zip_derived_cl245,
% 188.19/24.33 zip_derived_cl107, zip_derived_cl177, zip_derived_cl60,
% 188.19/24.33 zip_derived_cl3928, zip_derived_cl55, zip_derived_cl230,
% 188.19/24.33 zip_derived_cl51, zip_derived_cl59, zip_derived_cl363,
% 188.19/24.33 zip_derived_cl82, zip_derived_cl116, zip_derived_cl17000,
% 188.19/24.33 zip_derived_cl176, zip_derived_cl608, zip_derived_cl83])).
% 188.19/24.33
% 188.19/24.33 % SZS output end Refutation
% 188.19/24.33
% 188.19/24.33
% 188.19/24.33 % Terminating...
% 188.19/24.46 % Runner terminated.
% 188.19/24.47 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------