diff -r dca8d06ecbba -r 8cecd655eef4 src/HOL/SMT_Examples/VCC_Max.certs2 --- a/src/HOL/SMT_Examples/VCC_Max.certs2 Thu Jun 12 01:00:49 2014 +0200 +++ b/src/HOL/SMT_Examples/VCC_Max.certs2 Thu Jun 12 01:00:49 2014 +0200 @@ -1,4 +1,4 @@ -57921b560a136ca1a710a5f3b5e4e77c40b33980 2972 0 +05a761f33f246f0fee720bec6f015ca5aba01c4d 2972 0 unsat ((set-logic ) (declare-fun ?v0!14 () Int) @@ -114,10 +114,10 @@ (let (($x19992 (or $x15590 $x15599 $x19474 $x19501 $x19989))) (let (($x19995 (not $x19992))) (let ((?x23404 (b_S_ref$ ?x10320))) -(let ((?x23225 (b_S_ptr$ b_T_T_u1$ ?x23404))) -(let ((?x24099 (b_S_typ$ ?x23225))) -(let ((?x24100 (b_S_kind_n_of$ ?x24099))) -(let (($x23805 (= ?x24100 b_S_kind_n_primitive$))) +(let ((?x23228 (b_S_ptr$ b_T_T_u1$ ?x23404))) +(let ((?x23728 (b_S_typ$ ?x23228))) +(let ((?x23730 (b_S_kind_n_of$ ?x23728))) +(let (($x24098 (= ?x23730 b_S_kind_n_primitive$))) (let ((?x21472 (b_S_kind_n_of$ b_T_T_u1$))) (let (($x21473 (= ?x21472 b_S_kind_n_primitive$))) (let (($x9768 (b_S_is_n_primitive$ b_T_T_u1$))) @@ -221,7 +221,7 @@ (let ((@x24344 (unit-resolution (unit-resolution @x24337 (unit-resolution @x23870 @x19833 $x23270) $x23889) @x24343 false))) (let ((@x24345 (lemma @x24344 $x10321))) (let ((@x25031 (unit-resolution (def-axiom (or (not $x23270) $x15590 $x23242)) @x24345 (or (not $x23270) $x23242)))) -(let (($x23227 (= ?x10320 ?x23225))) +(let (($x23306 (= ?x10320 ?x23228))) (let (($x9607 (forall ((?v0 B_S_ptr$) (?v1 B_S_ctype$) )(!(or (not (b_S_is$ ?v0 ?v1)) (= ?v0 (b_S_ptr$ ?v1 (b_S_ref$ ?v0)))) :pattern ( (b_S_is$ ?v0 ?v1) ))) )) (let (($x9604 (or (not $x9596) (= ?1 (b_S_ptr$ ?0 (b_S_ref$ ?1)))))) @@ -231,24 +231,24 @@ (let ((@x9606 (rewrite (= (=> $x9596 (= ?1 (b_S_ptr$ ?0 (b_S_ref$ ?1)))) $x9604)))) (let ((@x15336 (mp~ (mp (asserted $x9601) (quant-intro @x9606 (= $x9601 $x9607)) $x9607) (nnf-pos (refl (~ $x9604 $x9604)) (~ $x9607 $x9607)) $x9607))) (let (($x21994 (not $x9607))) -(let (($x24289 (or $x21994 $x15590 $x23227))) -(let ((@x24294 (mp ((_ quant-inst (b_S_idx$ ?x10078 v_b_L_H_p_G_0$ b_T_T_u1$) b_T_T_u1$) (or $x21994 (or $x15590 $x23227))) (rewrite (= (or $x21994 (or $x15590 $x23227)) $x24289)) $x24289))) -(let ((@x25262 (symm (unit-resolution @x24294 @x15336 @x24345 $x23227) (= ?x23225 ?x10320)))) -(let ((@x24694 (trans (monotonicity @x25262 (= ?x24099 ?x23241)) (unit-resolution @x25031 (unit-resolution @x23870 @x19833 $x23270) $x23242) (= ?x24099 b_T_T_u1$)))) -(let ((@x24696 (trans (monotonicity @x24694 (= ?x24100 ?x21472)) (unit-resolution @x23544 (unit-resolution @x21484 @x15456 $x21480) $x21473) $x23805))) +(let (($x24294 (or $x21994 $x15590 $x23306))) +(let ((@x24335 (mp ((_ quant-inst (b_S_idx$ ?x10078 v_b_L_H_p_G_0$ b_T_T_u1$) b_T_T_u1$) (or $x21994 (or $x15590 $x23306))) (rewrite (= (or $x21994 (or $x15590 $x23306)) $x24294)) $x24294))) +(let ((@x25262 (symm (unit-resolution @x24335 @x15336 @x24345 $x23306) (= ?x23228 ?x10320)))) +(let ((@x24694 (trans (monotonicity @x25262 (= ?x23728 ?x23241)) (unit-resolution @x25031 (unit-resolution @x23870 @x19833 $x23270) $x23242) (= ?x23728 b_T_T_u1$)))) +(let ((@x24696 (trans (monotonicity @x24694 (= ?x23730 ?x21472)) (unit-resolution @x23544 (unit-resolution @x21484 @x15456 $x21480) $x21473) $x24098))) (let ((?x10272 (b_S_typemap$ v_b_S_s$))) -(let ((?x24217 (b_S_select_o_tm$ ?x10272 ?x23225))) +(let ((?x24217 (b_S_select_o_tm$ ?x10272 ?x23228))) (let ((?x24218 (b_S_ts_n_emb$ ?x24217))) -(let (($x23797 (b_S_closed$ v_b_S_s$ ?x24218))) -(let (($x23803 (not $x23797))) -(let (($x23775 (b_S_ts_n_is_n_volatile$ ?x24217))) +(let (($x23775 (b_S_closed$ v_b_S_s$ ?x24218))) (let (($x23784 (not $x23775))) -(let (($x23804 (or $x23784 $x23803))) -(let ((@x24686 (monotonicity (monotonicity @x25262 (= ?x24217 (b_S_select_o_tm$ ?x10272 ?x10320))) (= $x23775 (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320)))))) -(let ((@x24702 (symm @x24686 (= (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320)) $x23775)))) -(let ((@x24701 (monotonicity @x24702 (= (not (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320))) $x23784)))) -(let ((?x23101 (b_S_select_o_tm$ ?x10272 ?x10320))) -(let (($x23361 (b_S_ts_n_is_n_volatile$ ?x23101))) +(let (($x23805 (b_S_ts_n_is_n_volatile$ ?x24217))) +(let (($x23770 (not $x23805))) +(let (($x23797 (or $x23770 $x23784))) +(let ((@x24686 (monotonicity (monotonicity @x25262 (= ?x24217 (b_S_select_o_tm$ ?x10272 ?x10320))) (= $x23805 (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320)))))) +(let ((@x24702 (symm @x24686 (= (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320)) $x23805)))) +(let ((@x24701 (monotonicity @x24702 (= (not (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320))) $x23770)))) +(let ((?x23124 (b_S_select_o_tm$ ?x10272 ?x10320))) +(let (($x23361 (b_S_ts_n_is_n_volatile$ ?x23124))) (let (($x23297 (not $x23361))) (let (($x23362 (or $x15593 $x23361))) (let (($x23363 (not $x23362))) @@ -399,7 +399,7 @@ (let (($x19313 (or $x19297 $x19298 $x15525 $x15533))) (let (($x20589 (not $x15533))) (let (($x19318 (not $x19313))) -(let ((@x24016 (hypothesis $x19318))) +(let ((@x23991 (hypothesis $x19318))) (let (($x10141 (b_S_thread_n_local$ v_b_S_s$ ?x10137))) (let ((?x21175 (b_S_typ$ ?x10078))) (let ((?x22803 (b_S_kind_n_of$ ?x21175))) @@ -439,7 +439,7 @@ (let ((@x22576 (trans (monotonicity @x22567 (= (or $x22568 $x22543) $x22569)) (rewrite (= $x22569 $x22569)) (= (or $x22568 $x22543) $x22569)))) (let ((@x22577 (mp ((_ quant-inst (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) 0 b_T_T_u1$) (or $x22568 $x22543)) @x22576 $x22569))) (let ((@x22581 (def-axiom (or $x22562 $x22556)))) -(let ((@x24124 (unit-resolution @x22581 (lemma (unit-resolution @x22577 @x18183 (hypothesis $x22562) false) $x22565) $x22556))) +(let ((@x24189 (unit-resolution @x22581 (lemma (unit-resolution @x22577 @x18183 (hypothesis $x22562) false) $x22565) $x22556))) (let (($x21179 (= ?x10079 v_b_P_H_arr$))) (let (($x19835 (forall ((?v0 B_S_ctype$) (?v1 Int) )(!(= (b_S_ref$ (b_S_ptr$ ?v0 ?v1)) ?v1) :pattern ( (b_S_ptr$ ?v0 ?v1) ))) )) @@ -453,12 +453,12 @@ (let ((@x21185 ((_ quant-inst b_T_T_u1$ v_b_P_H_arr$) $x21184))) (let ((@x24511 (unit-resolution @x21185 @x19840 $x21179))) (let ((@x22852 (monotonicity @x24511 (= ?x22553 ?x10078)))) -(let ((@x24070 (monotonicity (trans (hypothesis $x22556) @x22852 (= ?x10137 ?x10078)) (= ?x22485 ?x10079)))) -(let ((@x22338 (symm (monotonicity (trans @x24070 @x24511 (= ?x22485 v_b_P_H_arr$)) (= ?x22505 ?x10078)) (= ?x10078 ?x22505)))) +(let ((@x24073 (monotonicity (trans (hypothesis $x22556) @x22852 (= ?x10137 ?x10078)) (= ?x22485 ?x10079)))) +(let ((@x22338 (symm (monotonicity (trans @x24073 @x24511 (= ?x22485 v_b_P_H_arr$)) (= ?x22505 ?x10078)) (= ?x10078 ?x22505)))) (let ((@x22340 (unit-resolution (hypothesis (not $x22506)) (trans (trans (hypothesis $x22556) @x22852 (= ?x10137 ?x10078)) @x22338 $x22506) false))) -(let ((@x23350 (unit-resolution (lemma @x22340 (or $x22559 $x22506)) @x24124 $x22506))) -(let ((@x23663 (trans (symm @x22852 (= ?x10078 ?x22553)) (symm @x24124 (= ?x22553 ?x10137)) (= ?x10078 ?x10137)))) -(let ((@x22940 (trans (monotonicity (trans @x23663 @x23350 (= ?x10078 ?x22505)) (= ?x22818 ?x22655)) (symm (monotonicity @x23350 (= ?x22478 ?x22655)) (= ?x22655 ?x22478)) (= ?x22818 ?x22478)))) +(let ((@x23667 (unit-resolution (lemma @x22340 (or $x22559 $x22506)) @x24189 $x22506))) +(let ((@x23699 (trans (symm @x22852 (= ?x10078 ?x22553)) (symm @x24189 (= ?x22553 ?x10137)) (= ?x10078 ?x10137)))) +(let ((@x22940 (trans (monotonicity (trans @x23699 @x23667 (= ?x10078 ?x22505)) (= ?x22818 ?x22655)) (symm (monotonicity @x23667 (= ?x22478 ?x22655)) (= ?x22655 ?x22478)) (= ?x22818 ?x22478)))) (let ((@x23082 (symm (monotonicity @x22940 (= $x22902 (b_S_ts_n_is_n_volatile$ ?x22478))) (= (b_S_ts_n_is_n_volatile$ ?x22478) $x22902)))) (let (($x22602 (b_S_ts_n_is_n_volatile$ ?x22478))) (let (($x22641 (not $x22602))) @@ -1364,7 +1364,7 @@ (let ((@x22613 ((_ quant-inst v_b_S_s$ (b_S_ptr$ ?x10076 ?x21014) (b_S_ptr$ ?x10076 ?x21014) b_l_H_public$) $x22612))) (let (($x35 (= b_S_kind_n_primitive$ b_S_kind_n_array$))) (let (($x36 (not $x35))) -(let (($x22500 (= $x36 (not (= (b_S_kind_n_of$ (b_S_typ$ ?x21983)) b_S_kind_n_primitive$))))) +(let (($x22488 (= $x36 (not (= (b_S_kind_n_of$ (b_S_typ$ ?x21983)) b_S_kind_n_primitive$))))) (let ((?x22234 (b_S_typ$ ?x21983))) (let ((?x22387 (b_S_kind_n_of$ ?x22234))) (let (($x22388 (= ?x22387 b_S_kind_n_primitive$))) @@ -1404,7 +1404,7 @@ (let ((@x22414 (trans (monotonicity @x24520 (= ?x22234 ?x21180)) (unit-resolution @x21189 @x19846 $x21183) (= ?x22234 ?x10076)))) (let ((@x22418 (trans (monotonicity @x22414 (= ?x22387 ?x10086)) (unit-resolution @x22406 (unit-resolution @x22160 @x15446 $x22149) $x22148) (= ?x22387 b_S_kind_n_array$)))) (let ((@x22857 (monotonicity @x22418 (= $x22388 (= b_S_kind_n_array$ b_S_kind_n_primitive$))))) -(let ((@x22934 (trans @x22857 (commutativity (= (= b_S_kind_n_array$ b_S_kind_n_primitive$) $x35)) (= $x22388 $x35)))) +(let ((@x22500 (trans @x22857 (commutativity (= (= b_S_kind_n_array$ b_S_kind_n_primitive$) $x35)) (= $x22388 $x35)))) (let (($x41 (= b_S_kind_n_thread$ b_S_kind_n_array$))) (let (($x42 (not $x41))) (let (($x39 (= b_S_kind_n_composite$ b_S_kind_n_array$))) @@ -1431,10 +1431,10 @@ (let ((@x22935 (monotonicity (symm (monotonicity @x24520 @x24520 (= $x22317 $x10136)) (= $x10136 $x22317)) (= $x11221 $x22336)))) (let ((@x22938 (unit-resolution (def-axiom (or (not $x22326) $x22317 $x22333)) (mp (hypothesis $x11221) @x22935 $x22336) (unit-resolution @x22613 @x15021 $x22326) $x22333))) (let (($x22368 (b_S_is$ ?x21983 ?x22234))) -(let ((@x22898 (mp @x12044 (symm (monotonicity @x24520 @x22414 (= $x22368 $x10084)) (= $x10084 $x22368)) $x22368))) +(let ((@x22885 (mp @x12044 (symm (monotonicity @x24520 @x22414 (= $x22368 $x10084)) (= $x10084 $x22368)) $x22368))) (let (($x22385 (b_S_typed$ v_b_S_s$ ?x21983))) (let ((@x12045 (and-elim @x12033 $x10085))) -(let ((@x22886 (mp @x12045 (symm (monotonicity @x24520 (= $x22385 $x10085)) (= $x10085 $x22385)) $x22385))) +(let ((@x22517 (mp @x12045 (symm (monotonicity @x24520 (= $x22385 $x10085)) (= $x10085 $x22385)) $x22385))) (let ((?x22243 (b_S_owner$ v_b_S_s$ ?x21983))) (let (($x22259 (= ?x22243 b_S_me$))) (let ((@x12043 (and-elim @x12033 $x10083))) @@ -1540,11 +1540,11 @@ (let (($x22386 (not $x22385))) (let (($x22384 (not $x22368))) (let (($x24309 (or (not $x18905) $x19677 $x22272 (not $x22259) $x22384 $x22386 $x22388 $x22242 $x22318))) -(let (($x24492 (= (or (not $x18905) (or $x19677 $x22272 (not $x22259) $x22384 $x22386 $x22388 $x22242 $x22318)) $x24309))) +(let (($x22614 (= (or (not $x18905) (or $x19677 $x22272 (not $x22259) $x22384 $x22386 $x22388 $x22242 $x22318)) $x24309))) (let ((@x24028 ((_ quant-inst v_b_S_s$ (b_S_ptr$ ?x10076 ?x21014)) (or (not $x18905) (or $x19677 $x22272 (not $x22259) $x22384 $x22386 $x22388 $x22242 $x22318))))) -(let ((@x24084 (mp @x24028 (rewrite $x24492) $x24309))) -(let ((@x22410 (unit-resolution @x24084 @x18908 @x12050 @x22409 @x22429 (trans (monotonicity @x24520 (= ?x22243 ?x10082)) @x12043 $x22259) (or $x22384 $x22386 $x22388 $x22318)))) -(let ((@x22411 (unit-resolution @x22410 @x22886 @x22898 @x22938 (mp @x75 (monotonicity (symm @x22934 (= $x35 $x22388)) $x22500) (not $x22388)) false))) +(let ((@x24070 (mp @x24028 (rewrite $x22614) $x24309))) +(let ((@x22410 (unit-resolution @x24070 @x18908 @x12050 @x22409 @x22429 (trans (monotonicity @x24520 (= ?x22243 ?x10082)) @x12043 $x22259) (or $x22384 $x22386 $x22388 $x22318)))) +(let ((@x22411 (unit-resolution @x22410 @x22517 @x22885 @x22938 (mp @x75 (monotonicity (symm @x22500 (= $x35 $x22388)) $x22488) (not $x22388)) false))) (let ((@x22434 (lemma @x22411 $x10136))) (let ((@x22687 (mp @x22434 (symm (monotonicity @x24520 @x24520 (= $x22317 $x10136)) (= $x10136 $x22317)) $x22317))) (let ((@x22688 (unit-resolution (def-axiom (or (not $x22326) $x22336 $x22318)) @x22687 (unit-resolution @x22613 @x15021 $x22326) $x22318))) @@ -1894,10 +1894,10 @@ (let (($x23521 (or (not $x19072) $x22944))) (let ((@x23524 ((_ quant-inst v_b_S_s$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$)) $x23521))) (let (($x23055 (not $x22801))) -(let ((@x23295 (monotonicity (symm (monotonicity @x23663 (= $x22801 $x10141)) (= $x10141 $x22801)) (= (not $x10141) $x23055)))) +(let ((@x23295 (monotonicity (symm (monotonicity @x23699 (= $x22801 $x10141)) (= $x10141 $x22801)) (= (not $x10141) $x23055)))) (let ((@x23090 (unit-resolution (def-axiom (or (not $x22944) $x22801 $x22939)) (mp (hypothesis (not $x10141)) @x23295 $x23055) (unit-resolution @x23524 @x19075 $x22944) $x22939))) -(let ((@x23670 (mp (unit-resolution (def-axiom (or $x22603 $x10139)) @x22760 $x10139) (symm (monotonicity @x23663 (= $x22799 $x10139)) (= $x10139 $x22799)) $x22799))) -(let ((@x23233 (unit-resolution (def-axiom (or $x22921 $x22900)) (unit-resolution (def-axiom (or $x22943 $x22802 $x22923)) @x23670 @x23090 $x22923) $x22900))) +(let ((@x23706 (mp (unit-resolution (def-axiom (or $x22603 $x10139)) @x22760 $x10139) (symm (monotonicity @x23699 (= $x22799 $x10139)) (= $x10139 $x22799)) $x22799))) +(let ((@x23222 (unit-resolution (def-axiom (or $x22921 $x22900)) (unit-resolution (def-axiom (or $x22943 $x22802 $x22923)) @x23706 @x23090 $x22923) $x22900))) (let ((?x24419 (b_S_ref$ ?x21983))) (let ((?x24433 (b_S_ptr$ b_T_T_u1$ ?x24419))) (let ((?x24410 (b_S_idx$ ?x21983 0 b_T_T_u1$))) @@ -2016,13 +2016,13 @@ (let ((@x14355 (mp~ (mp (asserted $x6917) @x6947 $x6943) (nnf-pos (refl (~ $x6940 $x6940)) (~ $x6943 $x6943)) $x6943))) (let ((@x17967 (mp @x14355 @x17966 $x17964))) (let (($x24241 (not $x24240))) -(let (($x23110 (not $x17964))) -(let (($x24183 (or $x23110 $x24241 $x11259 $x23791))) +(let (($x23252 (not $x17964))) +(let (($x23749 (or $x23252 $x24241 $x11259 $x23791))) (let (($x23792 (or $x24241 $x22599 $x22601 $x23791))) -(let (($x24184 (or $x23110 $x23792))) -(let ((@x23271 (trans (monotonicity @x22715 @x22724 (= $x23792 (or $x24241 false $x11259 $x23791))) (rewrite (= (or $x24241 false $x11259 $x23791) (or $x24241 $x11259 $x23791))) (= $x23792 (or $x24241 $x11259 $x23791))))) -(let ((@x23705 (trans (monotonicity @x23271 (= $x24184 (or $x23110 (or $x24241 $x11259 $x23791)))) (rewrite (= (or $x23110 (or $x24241 $x11259 $x23791)) $x24183)) (= $x24184 $x24183)))) -(let ((@x23755 (unit-resolution (mp ((_ quant-inst v_b_S_s$ v_b_P_H_arr$ b_T_T_u1$ v_b_P_H_len$ 0) $x24184) @x23705 $x24183) @x17967 @x12041 @x24355 (hypothesis $x23737) false))) +(let (($x23750 (or $x23252 $x23792))) +(let ((@x23251 (trans (monotonicity @x22715 @x22724 (= $x23792 (or $x24241 false $x11259 $x23791))) (rewrite (= (or $x24241 false $x11259 $x23791) (or $x24241 $x11259 $x23791))) (= $x23792 (or $x24241 $x11259 $x23791))))) +(let ((@x23352 (trans (monotonicity @x23251 (= $x23750 (or $x23252 (or $x24241 $x11259 $x23791)))) (rewrite (= (or $x23252 (or $x24241 $x11259 $x23791)) $x23749)) (= $x23750 $x23749)))) +(let ((@x23658 (unit-resolution (mp ((_ quant-inst v_b_S_s$ v_b_P_H_arr$ b_T_T_u1$ v_b_P_H_len$ 0) $x23750) @x23352 $x23749) @x17967 @x12041 @x24355 (hypothesis $x23737) false))) (let (($x21186 (= ?x21014 ?x10079))) (let (($x21191 (or $x21152 $x21186))) (let ((@x21192 ((_ quant-inst (b_S_array$ b_T_T_u1$ v_b_P_H_len$) (b_S_ref$ ?x10078)) $x21191))) @@ -2030,19 +2030,19 @@ (let ((@x24532 (trans @x24530 (unit-resolution @x22000 @x15336 @x12044 $x21990) (= ?x22595 ?x21983)))) (let ((@x23632 (trans (monotonicity @x24532 (= ?x24245 ?x24410)) (hypothesis $x24436) (= ?x24245 ?x24433)))) (let ((@x23628 (trans @x23632 (monotonicity (trans @x24524 @x24511 (= ?x24419 v_b_P_H_arr$)) (= ?x24433 ?x10078)) (= ?x24245 ?x10078)))) -(let ((@x23622 (trans (trans @x23628 (symm @x22852 (= ?x10078 ?x22553)) (= ?x24245 ?x22553)) (symm @x24124 (= ?x22553 ?x10137)) (= ?x24245 ?x10137)))) -(let ((@x23636 (symm (monotonicity (trans @x23622 @x23350 (= ?x24245 ?x22505)) (= ?x24246 ?x22655)) (= ?x22655 ?x24246)))) -(let ((@x23256 (monotonicity (monotonicity (trans @x23663 @x23350 (= ?x10078 ?x22505)) (= ?x22818 ?x22655)) (= ?x22903 (b_S_ts_n_emb$ ?x22655))))) -(let ((@x23678 (trans @x23256 (monotonicity @x23636 (= (b_S_ts_n_emb$ ?x22655) ?x24247)) (= ?x22903 ?x24247)))) -(let ((@x23865 (trans @x23678 (unit-resolution (def-axiom (or $x23737 $x24248)) (lemma @x23755 $x23791) $x24248) (= ?x22903 ?x22595)))) -(let ((@x23912 (trans (monotonicity (trans @x23865 @x24530 (= ?x22903 ?x10080)) (= ?x22893 ?x10082)) @x12043 $x22888))) +(let ((@x23622 (trans (trans @x23628 (symm @x22852 (= ?x10078 ?x22553)) (= ?x24245 ?x22553)) (symm @x24189 (= ?x22553 ?x10137)) (= ?x24245 ?x10137)))) +(let ((@x23636 (symm (monotonicity (trans @x23622 @x23667 (= ?x24245 ?x22505)) (= ?x24246 ?x22655)) (= ?x22655 ?x24246)))) +(let ((@x23746 (monotonicity (monotonicity (trans @x23699 @x23667 (= ?x10078 ?x22505)) (= ?x22818 ?x22655)) (= ?x22903 (b_S_ts_n_emb$ ?x22655))))) +(let ((@x23678 (trans @x23746 (monotonicity @x23636 (= (b_S_ts_n_emb$ ?x22655) ?x24247)) (= ?x22903 ?x24247)))) +(let ((@x23867 (trans @x23678 (unit-resolution (def-axiom (or $x23737 $x24248)) (lemma @x23658 $x23791) $x24248) (= ?x22903 ?x22595)))) +(let ((@x23912 (trans (monotonicity (trans @x23867 @x24530 (= ?x22903 ?x10080)) (= ?x22893 ?x10082)) @x12043 $x22888))) (let ((@x24132 (lemma (unit-resolution (hypothesis (not $x22888)) @x23912 false) (or $x24439 $x22888)))) (let ((@x23115 (unit-resolution @x24132 (unit-resolution @x24460 (lemma @x24133 $x24445) $x24436) $x22888))) (let ((?x22658 (b_S_ts_n_emb$ ?x22655))) (let ((?x22663 (b_S_typ$ ?x22658))) (let ((?x22664 (b_S_kind_n_of$ ?x22663))) (let (($x22665 (= ?x22664 b_S_kind_n_primitive$))) -(let ((@x23071 (monotonicity (monotonicity (symm @x23256 (= ?x22658 ?x22903)) (= ?x22663 ?x22890)) (= ?x22664 ?x22891)))) +(let ((@x23071 (monotonicity (monotonicity (symm @x23746 (= ?x22658 ?x22903)) (= ?x22663 ?x22890)) (= ?x22664 ?x22891)))) (let (($x22946 (b_S_is_n_non_n_primitive$ ?x22663))) (let (($x23237 (not $x22946))) (let (($x23503 (or $x22665 $x23237))) @@ -2063,8 +2063,8 @@ (let ((@x23058 ((_ quant-inst (b_S_select_o_tm$ ?x10272 ?x22505)) $x23057))) (let ((@x23584 (unit-resolution (def-axiom (or $x23503 (not $x22665))) (unit-resolution @x23058 @x19237 $x23504) (not $x22665)))) (let ((@x23060 (lemma (unit-resolution @x23584 (trans @x23071 (hypothesis $x22892) $x22665) false) (not $x22892)))) -(let ((@x23231 (unit-resolution (def-axiom (or $x22901 $x22817 $x22889 $x22892 $x22896)) @x23060 (unit-resolution (def-axiom (or $x22895 (not $x22888))) @x23115 $x22895) (or $x22901 $x22817 $x22889)))) -(let ((@x23406 (unit-resolution @x23231 @x23233 (unit-resolution (def-axiom (or $x22906 $x22902)) @x23294 $x22906) @x23076 false))) +(let ((@x23221 (unit-resolution (def-axiom (or $x22901 $x22817 $x22889 $x22892 $x22896)) @x23060 (unit-resolution (def-axiom (or $x22895 (not $x22888))) @x23115 $x22895) (or $x22901 $x22817 $x22889)))) +(let ((@x23406 (unit-resolution @x23221 @x23222 (unit-resolution (def-axiom (or $x22906 $x22902)) @x23294 $x22906) @x23076 false))) (let ((@x23403 (lemma @x23406 $x10141))) (let (($x20092 (or $x19318 $x20089))) (let (($x20095 (not $x20092))) @@ -2618,19 +2618,19 @@ (let ((@x13510 (monotonicity (monotonicity @x13504 (= $x12021 (and $x10136 $x13502))) (= (not $x12021) $x13508)))) (let ((@x13511 (mp (not-or-elim (mp (asserted $x10434) @x12031 $x12027) (not $x12021)) @x13510 $x13508))) (let ((@x20143 (mp (mp (mp (mp~ @x13511 @x15835 $x15833) @x16117 $x16115) @x19763 $x19761) (monotonicity @x20139 (= $x19761 $x20140)) $x20140))) -(let ((@x24002 (unit-resolution (def-axiom (or $x20134 $x20128)) (unit-resolution @x20143 @x22434 $x20137) $x20128))) +(let ((@x24008 (unit-resolution (def-axiom (or $x20134 $x20128)) (unit-resolution @x20143 @x22434 $x20137) $x20128))) (let ((?x22514 (b_S_typ$ ?x10137))) (let (($x22515 (= ?x22514 b_T_T_u1$))) (let ((@x22856 (trans (unit-resolution @x22581 (unit-resolution @x22577 @x18183 $x22565) $x22556) @x22852 (= ?x10137 ?x10078)))) (let ((@x22875 (trans (monotonicity @x22856 (= ?x22514 ?x21175)) (unit-resolution @x21182 @x19846 $x21176) $x22515))) -(let (($x22507 (not $x22515))) +(let (($x22932 (not $x22515))) (let (($x22522 (= $x10138 $x22515))) -(let (($x22949 (or $x22002 $x22522))) -(let ((@x22487 ((_ quant-inst (b_S_idx$ ?x10078 0 b_T_T_u1$) b_T_T_u1$) $x22949))) -(let ((@x22509 (unit-resolution (def-axiom (or (not $x22522) $x10138 $x22507)) (hypothesis $x15502) (or (not $x22522) $x22507)))) -(let ((@x22873 (unit-resolution (unit-resolution @x22509 (unit-resolution @x22487 @x19833 $x22522) $x22507) @x22875 false))) +(let (($x22487 (or $x22002 $x22522))) +(let ((@x22492 ((_ quant-inst (b_S_idx$ ?x10078 0 b_T_T_u1$) b_T_T_u1$) $x22487))) +(let ((@x22511 (unit-resolution (def-axiom (or (not $x22522) $x10138 $x22932)) (hypothesis $x15502) (or (not $x22522) $x22932)))) +(let ((@x22873 (unit-resolution (unit-resolution @x22511 (unit-resolution @x22492 @x19833 $x22522) $x22932) @x22875 false))) (let ((@x22876 (lemma @x22873 $x10138))) -(let ((@x23964 (unit-resolution (def-axiom (or $x20131 $x15502 $x15505 $x20125)) (unit-resolution (def-axiom (or $x22603 $x10139)) @x22760 $x10139) @x22876 @x24002 $x20125))) +(let ((@x24016 (unit-resolution (def-axiom (or $x20131 $x15502 $x15505 $x20125)) (unit-resolution (def-axiom (or $x22603 $x10139)) @x22760 $x10139) @x22876 @x24008 $x20125))) (let ((?x22963 (* (- 1) ?x10144))) (let ((?x22964 (+ v_b_L_H_max_G_0$ ?x22963))) (let (($x22965 (>= ?x22964 0))) @@ -2652,9 +2652,9 @@ (let ((@x23011 (symm (unit-resolution @x22447 @x15336 (hypothesis $x10138) $x22506) (= ?x22505 ?x10137)))) (let ((@x23020 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x22834) $x22839)) (symm (monotonicity @x23011 (= ?x22685 ?x10144)) $x22834) $x22839))) (let ((@x23023 (lemma ((_ th-lemma arith farkas 1 -1 -1 1) @x23020 @x23010 (hypothesis $x20589) @x23016 false) (or $x15502 $x15533 $x19297 $x15525 $x15511 $x20119)))) -(let ((@x24012 (unit-resolution @x23023 @x22876 (unit-resolution (def-axiom (or $x20122 $x20116)) @x23964 $x20116) (or $x15533 $x19297 $x15525 $x15511)))) -(let ((@x24203 (unit-resolution (unit-resolution @x24012 @x23403 (or $x15533 $x19297 $x15525)) (unit-resolution (def-axiom (or $x19313 (not $x15525))) @x24016 (not $x15525)) (unit-resolution (def-axiom (or $x19313 $x15523)) @x24016 $x15523) (unit-resolution (def-axiom (or $x19313 $x20589)) @x24016 $x20589) false))) -(let ((@x24417 (unit-resolution @x20962 @x22876 (unit-resolution (def-axiom (or $x20122 $x20116)) @x23964 $x20116) (or $x15511 $x20113)))) +(let ((@x24012 (unit-resolution @x23023 @x22876 (unit-resolution (def-axiom (or $x20122 $x20116)) @x24016 $x20116) (or $x15533 $x19297 $x15525 $x15511)))) +(let ((@x24203 (unit-resolution (unit-resolution @x24012 @x23403 (or $x15533 $x19297 $x15525)) (unit-resolution (def-axiom (or $x19313 (not $x15525))) @x23991 (not $x15525)) (unit-resolution (def-axiom (or $x19313 $x15523)) @x23991 $x15523) (unit-resolution (def-axiom (or $x19313 $x20589)) @x23991 $x20589) false))) +(let ((@x24417 (unit-resolution @x20962 @x22876 (unit-resolution (def-axiom (or $x20122 $x20116)) @x24016 $x20116) (or $x15511 $x20113)))) (let ((@x24506 (unit-resolution (def-axiom (or $x20110 $x20104)) (unit-resolution @x24417 @x23403 $x20113) $x20104))) (let ((@x24507 (unit-resolution (def-axiom (or $x20107 $x11385 $x20101)) (lemma ((_ th-lemma arith farkas 1 1) @x12041 (hypothesis $x11385) false) $x11382) @x24506 $x20101))) (let ((@x24462 (unit-resolution (def-axiom (or $x20095 $x19318 $x20089)) (unit-resolution (def-axiom (or $x20098 $x20092)) @x24507 $x20092) $x20092))) @@ -2710,8 +2710,8 @@ (let ((@x23338 ((_ th-lemma arith farkas -1 1 1) (unit-resolution (def-axiom (or $x19575 $x16014)) @x23328 $x16014) (unit-resolution @x23335 @x23330 $x23168) (unit-resolution (def-axiom (or $x20062 $x11486)) (hypothesis $x20065) $x11486) false))) (let ((@x24500 (unit-resolution (lemma @x23338 (or $x20062 $x19903 $x11867 $x19501 $x19674 $x19669)) @x24499 @x24415 (unit-resolution (def-axiom (or $x20074 $x11432)) @x24583 $x11432) @x24314 (unit-resolution (def-axiom (or $x20074 $x13315)) @x24583 $x13315) $x20062))) (let ((@x24502 (unit-resolution (def-axiom (or $x20071 $x20019 $x20065)) (unit-resolution (def-axiom (or $x20074 $x20068)) @x24583 $x20068) @x24500 $x20019))) -(let ((@x24684 (unit-resolution (def-axiom (or $x20016 $x11487)) @x24502 $x11487))) -(let ((@x24741 (mp @x22691 (symm (monotonicity @x24532 (= $x22596 $x22344)) (= $x22344 $x22596)) $x22596))) +(let ((@x24656 (unit-resolution (def-axiom (or $x20016 $x11487)) @x24502 $x11487))) +(let ((@x24896 (mp @x22691 (symm (monotonicity @x24532 (= $x22596 $x22344)) (= $x22344 $x22596)) $x22596))) (let ((@x23420 (hypothesis $x11487))) (let (($x23378 (or $x22629 $x19677 $x21489 $x22597 $x19670 $x11486 $x23363))) (let (($x23360 (>= (+ v_b_L_H_p_G_0$ (* (- 1) v_b_P_H_len$)) 0))) @@ -2725,42 +2725,42 @@ (let ((@x23387 (trans @x23383 (rewrite (= (or $x22629 (or $x19677 $x21489 $x22597 $x19670 $x11486 $x23363)) $x23378)) (= $x23379 $x23378)))) (let ((@x23388 (mp ((_ quant-inst v_b_S_s$ v_b_P_H_arr$ (b_S_ptr$ ?x10076 ?x21014) v_b_P_H_len$ v_b_L_H_p_G_0$ b_T_T_u1$) $x23379) @x23387 $x23378))) (let ((@x23422 (unit-resolution @x23388 @x18670 @x9769 @x12050 (hypothesis $x11901) @x23420 (hypothesis $x22596) (hypothesis $x23362) false))) -(let ((@x24788 (unit-resolution (lemma @x23422 (or $x23363 $x19670 $x11486 $x22597)) @x24741 (or $x23363 $x19670 $x11486)))) -(let ((@x24697 (unit-resolution (def-axiom (or $x23362 $x23297)) (unit-resolution @x24788 @x24684 @x24576 $x23363) $x23297))) +(let ((@x24759 (unit-resolution (lemma @x23422 (or $x23363 $x19670 $x11486 $x22597)) @x24896 (or $x23363 $x19670 $x11486)))) +(let ((@x24697 (unit-resolution (def-axiom (or $x23362 $x23297)) (unit-resolution @x24759 @x24656 @x24576 $x23363) $x23297))) (let (($x23782 (b_S_in_n_wrapped_n_domain$ v_b_S_s$ ?x24218))) (let ((?x23727 (b_S_owner$ v_b_S_s$ ?x24218))) (let (($x23776 (= ?x23727 b_S_me$))) (let (($x23785 (or $x23776 $x23782))) (let (($x24475 (not $x23785))) -(let ((?x23730 (b_S_typ$ ?x24218))) -(let ((?x23768 (b_S_kind_n_of$ ?x23730))) +(let ((?x23804 (b_S_typ$ ?x24218))) +(let ((?x23768 (b_S_kind_n_of$ ?x23804))) (let (($x23769 (= ?x23768 b_S_kind_n_primitive$))) -(let (($x23728 (not $x23804))) -(let (($x23770 (not $x23805))) -(let (($x24476 (or $x23770 $x23728 $x23769 $x24475))) -(let (($x24627 (b_S_in_n_wrapped_n_domain$ v_b_S_s$ ?x23225))) -(let (($x24478 (= (b_S_owner$ v_b_S_s$ ?x23225) b_S_me$))) -(let (($x24943 (or $x24478 $x24627))) -(let (($x25004 (not $x24943))) -(let (($x24820 (or $x23805 $x25004))) -(let (($x24623 (not $x24820))) +(let (($x23803 (not $x23797))) +(let (($x24099 (not $x24098))) +(let (($x24476 (or $x24099 $x23803 $x23769 $x24475))) +(let (($x24604 (b_S_in_n_wrapped_n_domain$ v_b_S_s$ ?x23228))) +(let (($x24478 (= (b_S_owner$ v_b_S_s$ ?x23228) b_S_me$))) +(let (($x24602 (or $x24478 $x24604))) +(let (($x24797 (not $x24602))) +(let (($x24820 (or $x24098 $x24797))) +(let (($x24655 (not $x24820))) (let (($x24474 (not $x24476))) -(let (($x24809 (or $x24474 $x24623))) -(let (($x24810 (not $x24809))) -(let (($x24209 (b_S_typed$ v_b_S_s$ ?x23225))) +(let (($x24912 (or $x24474 $x24655))) +(let (($x24913 (not $x24912))) +(let (($x24209 (b_S_typed$ v_b_S_s$ ?x23228))) (let (($x24210 (not $x24209))) -(let (($x24817 (or $x24210 $x24810))) -(let (($x24818 (not $x24817))) -(let (($x23783 (b_S_thread_n_local$ v_b_S_s$ ?x23225))) -(let (($x24819 (= $x23783 $x24818))) -(let (($x24622 (or (not $x19072) $x24819))) -(let ((@x24633 ((_ quant-inst v_b_S_s$ (b_S_ptr$ b_T_T_u1$ ?x23404)) $x24622))) +(let (($x24931 (or $x24210 $x24913))) +(let (($x24932 (not $x24931))) +(let (($x23783 (b_S_thread_n_local$ v_b_S_s$ ?x23228))) +(let (($x24934 (= $x23783 $x24932))) +(let (($x24622 (or (not $x19072) $x24934))) +(let ((@x24172 ((_ quant-inst v_b_S_s$ (b_S_ptr$ b_T_T_u1$ ?x23404)) $x24622))) (let (($x24628 (not $x23783))) (let ((@x24670 (monotonicity (symm (monotonicity @x25262 (= $x23783 $x10324)) (= $x10324 $x23783)) (= $x15599 $x24628)))) -(let ((@x24708 (unit-resolution (def-axiom (or (not $x24819) $x23783 $x24817)) (mp (hypothesis $x15599) @x24670 $x24628) (unit-resolution @x24633 @x19075 $x24819) $x24817))) -(let ((@x24998 (unit-resolution (def-axiom (or $x23362 $x10322)) (unit-resolution @x24788 @x24684 @x24576 $x23363) $x10322))) -(let ((@x24710 (mp @x24998 (symm (monotonicity @x25262 (= $x24209 $x10322)) (= $x10322 $x24209)) $x24209))) -(let ((@x24724 (unit-resolution (def-axiom (or $x24809 $x24476)) (unit-resolution (def-axiom (or $x24818 $x24210 $x24810)) @x24710 @x24708 $x24810) $x24476))) +(let ((@x24708 (unit-resolution (def-axiom (or (not $x24934) $x23783 $x24931)) (mp (hypothesis $x15599) @x24670 $x24628) (unit-resolution @x24172 @x19075 $x24934) $x24931))) +(let ((@x24785 (unit-resolution (def-axiom (or $x23362 $x10322)) (unit-resolution @x24759 @x24656 @x24576 $x23363) $x10322))) +(let ((@x24710 (mp @x24785 (symm (monotonicity @x25262 (= $x24209 $x10322)) (= $x10322 $x24209)) $x24209))) +(let ((@x24724 (unit-resolution (def-axiom (or $x24912 $x24476)) (unit-resolution (def-axiom (or $x24932 $x24210 $x24913)) @x24710 @x24708 $x24913) $x24476))) (let ((?x24320 (b_S_idx$ ?x22595 v_b_L_H_p_G_0$ b_T_T_u1$))) (let ((?x24321 (b_S_select_o_tm$ ?x10272 ?x24320))) (let ((?x24322 (b_S_ts_n_emb$ ?x24321))) @@ -2771,12 +2771,12 @@ (let (($x24324 (not $x24323))) (let (($x24330 (or $x24324 $x24325 (not (b_S_ts_n_is_n_array_n_elt$ ?x24321)) $x24329))) (let (($x24331 (not $x24330))) -(let (($x25071 (or $x23110 $x24241 $x19670 $x11486 $x24331))) +(let (($x25071 (or $x23252 $x24241 $x19670 $x11486 $x24331))) (let (($x24332 (or $x24241 $x19670 $x23360 $x24331))) -(let (($x25072 (or $x23110 $x24332))) +(let (($x25072 (or $x23252 $x24332))) (let ((@x25070 (monotonicity (trans @x23370 @x23372 (= $x23360 $x11486)) (= $x24332 (or $x24241 $x19670 $x11486 $x24331))))) -(let ((@x25080 (trans (monotonicity @x25070 (= $x25072 (or $x23110 (or $x24241 $x19670 $x11486 $x24331)))) (rewrite (= (or $x23110 (or $x24241 $x19670 $x11486 $x24331)) $x25071)) (= $x25072 $x25071)))) -(let ((@x25137 (unit-resolution (mp ((_ quant-inst v_b_S_s$ v_b_P_H_arr$ b_T_T_u1$ v_b_P_H_len$ v_b_L_H_p_G_0$) $x25072) @x25080 $x25071) @x17967 @x24576 @x24684 @x24355 (hypothesis $x24330) false))) +(let ((@x25080 (trans (monotonicity @x25070 (= $x25072 (or $x23252 (or $x24241 $x19670 $x11486 $x24331)))) (rewrite (= (or $x23252 (or $x24241 $x19670 $x11486 $x24331)) $x25071)) (= $x25072 $x25071)))) +(let ((@x25137 (unit-resolution (mp ((_ quant-inst v_b_S_s$ v_b_P_H_arr$ b_T_T_u1$ v_b_P_H_len$ v_b_L_H_p_G_0$) $x25072) @x25080 $x25071) @x17967 @x24576 @x24656 @x24355 (hypothesis $x24330) false))) (let ((@x25083 (def-axiom (or $x24330 $x24323)))) (let ((?x24315 (b_S_ref$ ?x24198))) (let ((?x24367 (* (- 1) ?x24315))) @@ -2795,15 +2795,15 @@ (let ((?x25227 (* (- 1) ?x24925))) (let ((?x25228 (+ ?x24174 ?x25227))) (let (($x25229 (<= ?x25228 0))) -(let ((?x23747 (* (- 1) ?x21014))) -(let ((?x23641 (+ ?x10079 ?x23747))) -(let (($x24296 (<= ?x23641 0))) -(let ((@x25085 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x10079 ?x21014)) $x24296)) (symm (unit-resolution @x21192 @x19840 $x21186) (= ?x10079 ?x21014)) $x24296))) +(let ((?x24127 (* (- 1) ?x21014))) +(let ((?x23641 (+ ?x10079 ?x24127))) +(let (($x24104 (<= ?x23641 0))) +(let ((@x25085 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x10079 ?x21014)) $x24104)) (symm (unit-resolution @x21192 @x19840 $x21186) (= ?x10079 ?x21014)) $x24104))) (let ((?x25173 (* (- 1) ?x24419))) (let ((?x25174 (+ ?x21014 ?x25173))) (let (($x25175 (<= ?x25174 0))) (let ((@x25090 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x21014 ?x24419)) $x25175)) (symm (monotonicity @x24520 (= ?x24419 ?x21014)) (= ?x21014 ?x24419)) $x25175))) -(let ((@x25103 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x25229 (not $x24296) (not $x25175))) @x25090 @x25085 $x25229))) +(let ((@x25103 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x25229 (not $x24104) (not $x25175))) @x25090 @x25085 $x25229))) (let (($x25230 (>= ?x25228 0))) (let (($x23809 (>= ?x23641 0))) (let ((@x25106 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x10079 ?x21014)) $x23809)) (symm (unit-resolution @x21192 @x19840 $x21186) (= ?x10079 ?x21014)) $x23809))) @@ -2829,54 +2829,54 @@ (let ((@x25162 (monotonicity (monotonicity @x25154 (= $x24471 $x25155)) (= (or $x22568 $x24471) $x25158)))) (let ((@x25166 (mp ((_ quant-inst (b_S_ptr$ ?x10076 ?x21014) v_b_L_H_p_G_0$ b_T_T_u1$) (or $x22568 $x24471)) (trans @x25162 (rewrite (= $x25158 $x25158)) (= (or $x22568 $x24471) $x25158)) $x25158))) (let ((@x25257 (unit-resolution (def-axiom (or $x25152 $x25146)) (unit-resolution @x25166 @x18183 $x25155) $x25146))) -(let ((@x25185 (trans (trans (monotonicity @x24532 (= ?x24320 ?x24463)) @x25257 (= ?x24320 ?x24930)) (monotonicity @x25183 (= ?x24930 ?x23225)) (= ?x24320 ?x23225)))) -(let ((@x25217 (symm (monotonicity (trans @x25185 @x25262 (= ?x24320 ?x10320)) (= ?x24321 ?x23101)) (= ?x23101 ?x24321)))) -(let ((@x25274 (monotonicity (monotonicity @x25262 (= ?x24217 ?x23101)) (= ?x24218 (b_S_ts_n_emb$ ?x23101))))) -(let ((@x25219 (trans @x25274 (monotonicity @x25217 (= (b_S_ts_n_emb$ ?x23101) ?x24322)) (= ?x24218 ?x24322)))) +(let ((@x25185 (trans (trans (monotonicity @x24532 (= ?x24320 ?x24463)) @x25257 (= ?x24320 ?x24930)) (monotonicity @x25183 (= ?x24930 ?x23228)) (= ?x24320 ?x23228)))) +(let ((@x25217 (symm (monotonicity (trans @x25185 @x25262 (= ?x24320 ?x10320)) (= ?x24321 ?x23124)) (= ?x23124 ?x24321)))) +(let ((@x25274 (monotonicity (monotonicity @x25262 (= ?x24217 ?x23124)) (= ?x24218 (b_S_ts_n_emb$ ?x23124))))) +(let ((@x25219 (trans @x25274 (monotonicity @x25217 (= (b_S_ts_n_emb$ ?x23124) ?x24322)) (= ?x24218 ?x24322)))) (let ((@x25221 (trans (trans @x25219 (hypothesis $x24323) (= ?x24218 ?x22595)) @x24530 (= ?x24218 ?x10080)))) (let ((@x25293 (unit-resolution (hypothesis (not $x23776)) (trans (monotonicity @x25221 (= ?x23727 ?x10082)) @x12043 $x23776) false))) -(let ((@x23976 (unit-resolution (lemma @x25293 (or $x24324 $x23776)) (unit-resolution @x25083 (lemma @x25137 $x24331) $x24323) $x23776))) -(let ((?x23443 (b_S_ts_n_emb$ ?x23101))) +(let ((@x24057 (unit-resolution (lemma @x25293 (or $x24324 $x23776)) (unit-resolution @x25083 (lemma @x25137 $x24331) $x24323) $x23776))) +(let ((?x23443 (b_S_ts_n_emb$ ?x23124))) (let ((?x23448 (b_S_typ$ ?x23443))) (let ((?x23449 (b_S_kind_n_of$ ?x23448))) (let (($x23450 (= ?x23449 b_S_kind_n_primitive$))) -(let ((@x24651 (monotonicity (monotonicity (symm @x25274 (= ?x23443 ?x24218)) (= ?x23448 ?x23730)) (= ?x23449 ?x23768)))) +(let ((@x24651 (monotonicity (monotonicity (symm @x25274 (= ?x23443 ?x24218)) (= ?x23448 ?x23804)) (= ?x23449 ?x23768)))) (let (($x23598 (b_S_is_n_non_n_primitive$ ?x23448))) (let (($x23599 (not $x23598))) (let (($x23602 (or $x23450 $x23599))) (let (($x23603 (not $x23602))) (let (($x24666 (or (not $x19234) $x23603))) -(let ((@x24631 ((_ quant-inst (b_S_select_o_tm$ ?x10272 ?x10320)) $x24666))) -(let ((@x24965 (unit-resolution (def-axiom (or $x23602 (not $x23450))) (unit-resolution @x24631 @x19237 $x23603) (not $x23450)))) +(let ((@x24626 ((_ quant-inst (b_S_select_o_tm$ ?x10272 ?x10320)) $x24666))) +(let ((@x24965 (unit-resolution (def-axiom (or $x23602 (not $x23450))) (unit-resolution @x24626 @x19237 $x23603) (not $x23450)))) (let ((@x24645 (lemma (unit-resolution @x24965 (trans @x24651 (hypothesis $x23769) $x23450) false) (not $x23769)))) -(let ((@x24718 (unit-resolution (def-axiom (or $x24474 $x23770 $x23728 $x23769 $x24475)) @x24645 (unit-resolution (def-axiom (or $x23785 (not $x23776))) @x23976 $x23785) (or $x24474 $x23770 $x23728)))) -(let ((@x24717 (unit-resolution @x24718 @x24724 (unit-resolution (def-axiom (or $x23804 $x23775)) (mp @x24697 @x24701 $x23784) $x23804) @x24696 false))) +(let ((@x24718 (unit-resolution (def-axiom (or $x24474 $x24099 $x23803 $x23769 $x24475)) @x24645 (unit-resolution (def-axiom (or $x23785 (not $x23776))) @x24057 $x23785) (or $x24474 $x24099 $x23803)))) +(let ((@x24717 (unit-resolution @x24718 @x24724 (unit-resolution (def-axiom (or $x23797 $x23805)) (mp @x24697 @x24701 $x23770) $x23797) @x24696 false))) (let ((@x20784 (def-axiom (or $x20013 $x15590 $x15593 $x20007)))) -(let ((@x24650 (unit-resolution (unit-resolution @x20784 @x24345 (or $x20013 $x15593 $x20007)) @x24998 (unit-resolution (def-axiom (or $x20016 $x20010)) @x24502 $x20010) $x20007))) +(let ((@x24630 (unit-resolution (unit-resolution @x20784 @x24345 (or $x20013 $x15593 $x20007)) @x24785 (unit-resolution (def-axiom (or $x20016 $x20010)) @x24502 $x20010) $x20007))) (let ((@x20774 (def-axiom (or $x20004 $x19998)))) (let ((@x20768 (def-axiom (or $x20001 $x15590 $x15599 $x19995)))) -(let ((@x25020 (unit-resolution (unit-resolution @x20768 @x24345 (or $x20001 $x15599 $x19995)) (unit-resolution @x20774 @x24650 $x19998) (or $x15599 $x19995)))) +(let ((@x25020 (unit-resolution (unit-resolution @x20768 @x24345 (or $x20001 $x15599 $x19995)) (unit-resolution @x20774 @x24630 $x19998) (or $x15599 $x19995)))) (let ((@x23989 (hypothesis $x19980))) -(let ((@x24787 (unit-resolution (def-axiom (or $x19959 $x15590 $x15599 $x19953)) @x24345 (or $x19959 $x15599 $x19953)))) -(let ((@x24655 (unit-resolution @x24787 (unit-resolution (def-axiom (or $x19992 $x10324)) (hypothesis $x19995) $x10324) (hypothesis $x19950) $x19959))) +(let ((@x25004 (unit-resolution (def-axiom (or $x19959 $x15590 $x15599 $x19953)) @x24345 (or $x19959 $x15599 $x19953)))) +(let ((@x24684 (unit-resolution @x25004 (unit-resolution (def-axiom (or $x19992 $x10324)) (hypothesis $x19995) $x10324) (hypothesis $x19950) $x19959))) (let ((@x20748 (def-axiom (or $x19989 $x19977 $x19983)))) -(let ((@x24904 (unit-resolution @x20748 (unit-resolution (def-axiom (or $x19992 $x19986)) (hypothesis $x19995) $x19986) @x23989 $x19977))) +(let ((@x24916 (unit-resolution @x20748 (unit-resolution (def-axiom (or $x19992 $x19986)) (hypothesis $x19995) $x19986) @x23989 $x19977))) (let ((@x20716 (def-axiom (or $x19974 $x19968)))) -(let ((@x24602 (unit-resolution (def-axiom (or $x19971 $x15590 $x15593 $x19965)) @x24345 (or $x19971 $x15593 $x19965)))) -(let ((@x24657 (unit-resolution @x24602 (unit-resolution @x20716 @x24904 $x19968) (unit-resolution (def-axiom (or $x19962 $x19956)) @x24655 $x19962) @x24998 false))) -(let ((@x24972 (unit-resolution (lemma @x24657 (or $x19992 $x19983 $x19953)) @x23989 (unit-resolution @x25020 (lemma @x24717 $x10324) $x19995) $x19953))) +(let ((@x24762 (unit-resolution (def-axiom (or $x19971 $x15590 $x15593 $x19965)) @x24345 (or $x19971 $x15593 $x19965)))) +(let ((@x24920 (unit-resolution @x24762 (unit-resolution @x20716 @x24916 $x19968) (unit-resolution (def-axiom (or $x19962 $x19956)) @x24684 $x19962) @x24785 false))) +(let ((@x24972 (unit-resolution (lemma @x24920 (or $x19992 $x19983 $x19953)) @x23989 (unit-resolution @x25020 (lemma @x24717 $x10324) $x19995) $x19953))) (let (($x13277 (<= v_b_P_H_len$ 4294967295))) (let (($x13272 (= (+ b_S_max_o_u4$ (* (- 1) v_b_P_H_len$)) (+ 4294967295 (* (- 1) v_b_P_H_len$))))) (let ((@x13276 (monotonicity (monotonicity @x6446 $x13272) (= $x11245 (>= (+ 4294967295 (* (- 1) v_b_P_H_len$)) 0))))) (let ((@x13281 (trans @x13276 (rewrite (= (>= (+ 4294967295 (* (- 1) v_b_P_H_len$)) 0) $x13277)) (= $x11245 $x13277)))) (let ((@x13282 (mp (and-elim @x12033 $x11245) @x13281 $x13277))) (let ((@x25068 (unit-resolution ((_ th-lemma arith assign-bounds 1 -1) (or $x13353 (not $x13277) $x11486)) @x13282 (or $x13353 $x11486)))) -(let ((@x25023 (unit-resolution (def-axiom (or $x19947 $x15611 $x15614 $x19941)) (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x19670 $x11570)) @x24576 $x11570) (unit-resolution @x25068 @x24684 $x13353) (or $x19947 $x19941)))) +(let ((@x25023 (unit-resolution (def-axiom (or $x19947 $x15611 $x15614 $x19941)) (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x19670 $x11570)) @x24576 $x11570) (unit-resolution @x25068 @x24656 $x13353) (or $x19947 $x19941)))) (let ((@x25021 (unit-resolution @x25023 (unit-resolution (def-axiom (or $x19950 $x19944)) @x24972 $x19944) $x19941))) (let ((@x20652 (def-axiom (or $x19938 $x19932)))) (let (($x20596 (>= ?x11582 (- 1)))) (let ((@x25129 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x19452 $x20596)) (unit-resolution (def-axiom (or $x19938 $x11580)) @x25021 $x11580) $x20596))) -(let ((@x25134 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x11608 $x11486 (not $x20596))) @x24684 (or $x11608 (not $x20596))))) +(let ((@x25134 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x11608 $x11486 (not $x20596))) @x24656 (or $x11608 (not $x20596))))) (let ((@x20638 (def-axiom (or $x19935 $x11612 $x19929)))) (let ((@x25133 (unit-resolution @x20638 (unit-resolution @x25134 @x25129 $x11608) (unit-resolution @x20652 @x25021 $x19932) $x19929))) (let ((@x20630 (def-axiom (or $x19926 $x19920)))) @@ -2888,12 +2888,12 @@ (let ((@x25188 (symm (unit-resolution (def-axiom (or $x19950 $x10340)) @x24972 $x10340) (= v_b_L_H_p_G_0$ v_b_SL_H_witness_G_1$)))) (let ((@x25200 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= v_b_L_H_p_G_0$ v_b_SL_H_witness_G_1$)) $x24861)) @x25188 $x24861))) (let ((@x20614 (def-axiom (or $x19413 $x11647 (not $x10374))))) -(let ((@x25206 (unit-resolution @x20614 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x11648 (not $x24861) $x11486)) @x25200 @x24684 $x11648) (trans @x25190 @x25121 $x10374) $x19413))) +(let ((@x25206 (unit-resolution @x20614 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x11648 (not $x24861) $x11486)) @x25200 @x24656 $x11648) (trans @x25190 @x25121 $x10374) $x19413))) (let ((@x20618 (def-axiom (or $x19914 $x19412)))) (let ((@x20626 (def-axiom (or $x19923 $x19386 $x19917)))) (let ((@x25210 (unit-resolution @x20626 (unit-resolution @x20618 @x25206 $x19914) (unit-resolution @x20630 @x25133 $x19920) $x19386))) -(let (($x24182 (>= (+ v_b_L_H_max_G_1$ ?x15891) 0))) -(let (($x24206 (not $x24182))) +(let (($x24195 (>= (+ v_b_L_H_max_G_1$ ?x15891) 0))) +(let (($x24206 (not $x24195))) (let ((?x11631 (* (- 1) v_b_L_H_max_G_3$))) (let ((?x20720 (+ v_b_L_H_max_G_1$ ?x11631))) (let (($x20721 (<= ?x20720 0))) @@ -2905,30 +2905,30 @@ (let ((@x24170 (hypothesis $x20721))) (let (($x20603 (not $x15893))) (let ((@x24171 (hypothesis $x20603))) -(let ((@x24211 (lemma ((_ th-lemma arith farkas -1 1 1) (hypothesis $x24182) @x24171 @x24170 false) (or $x24206 $x15893 (not $x20721))))) +(let ((@x24211 (lemma ((_ th-lemma arith farkas -1 1 1) (hypothesis $x24195) @x24171 @x24170 false) (or $x24206 $x15893 (not $x20721))))) (let ((@x25131 (unit-resolution @x24211 (unit-resolution (def-axiom (or $x19381 $x20603)) @x25210 $x20603) (unit-resolution ((_ th-lemma arith assign-bounds 1 1) (or $x20721 (not $x24870) $x11516)) @x25214 @x25195 $x20721) $x24206))) (let ((?x15869 (* (- 1) ?v0!14))) (let ((?x23656 (+ v_b_L_H_p_G_0$ ?x15869))) -(let (($x24586 (>= ?x23656 0))) +(let (($x24926 (>= ?x23656 0))) (let ((@x24735 (hypothesis $x20596))) -(let ((@x24001 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x24586 $x15871 (not $x20596))) (hypothesis $x15876) @x24735 $x24586))) +(let ((@x24918 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x24926 $x15871 (not $x20596))) (hypothesis $x15876) @x24735 $x24926))) (let (($x23657 (<= ?x23656 0))) -(let (($x24913 (or $x19903 $x19365 $x19366 $x23657 $x24182))) +(let (($x24882 (or $x19903 $x19365 $x19366 $x23657 $x24195))) (let (($x23648 (<= (+ ?x15634 (* (- 1) v_b_L_H_max_G_1$)) 0))) (let (($x23640 (>= (+ ?v0!14 ?x11484) 0))) (let (($x23649 (or $x19365 $x19366 $x23640 $x23648))) -(let (($x24853 (or $x19903 $x23649))) -(let (($x24880 (= (+ ?x15634 (* (- 1) v_b_L_H_max_G_1$)) (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634)))) -(let ((@x24024 (monotonicity (rewrite $x24880) (= $x23648 (<= (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634) 0))))) -(let ((@x24867 (trans @x24024 (rewrite (= (<= (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634) 0) $x24182)) (= $x23648 $x24182)))) -(let ((@x24020 (monotonicity (rewrite (= (+ ?v0!14 ?x11484) (+ ?x11484 ?v0!14))) (= $x23640 (>= (+ ?x11484 ?v0!14) 0))))) -(let ((@x24881 (trans @x24020 (rewrite (= (>= (+ ?x11484 ?v0!14) 0) $x23657)) (= $x23640 $x23657)))) -(let ((@x24935 (monotonicity (monotonicity @x24881 @x24867 (= $x23649 (or $x19365 $x19366 $x23657 $x24182))) (= $x24853 (or $x19903 (or $x19365 $x19366 $x23657 $x24182)))))) -(let ((@x24917 (trans @x24935 (rewrite (= (or $x19903 (or $x19365 $x19366 $x23657 $x24182)) $x24913)) (= $x24853 $x24913)))) -(let ((@x24941 (unit-resolution (mp ((_ quant-inst ?v0!14) $x24853) @x24917 $x24913) @x23333 (unit-resolution (def-axiom (or $x19381 $x15626)) (hypothesis $x19386) $x15626) (unit-resolution (def-axiom (or $x19381 $x15627)) (hypothesis $x19386) $x15627) (hypothesis $x24206) $x23657))) -(let ((@x24757 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x25035 (not $x23657) (not $x24586))) @x24941 @x24001 (hypothesis (not $x25035)) false))) -(let ((@x24761 (lemma @x24757 (or $x19381 $x25035 $x19903 $x24182 $x15871 (not $x20596))))) -(let ((@x25179 (unit-resolution (unit-resolution @x24761 @x24499 (or $x19381 $x25035 $x24182 $x15871 (not $x20596))) @x25131 @x25129 (unit-resolution (def-axiom (or $x19381 $x15876)) @x25210 $x15876) @x25210 $x25035))) +(let (($x24880 (or $x19903 $x23649))) +(let (($x24587 (= (+ ?x15634 (* (- 1) v_b_L_H_max_G_1$)) (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634)))) +(let ((@x24936 (monotonicity (rewrite $x24587) (= $x23648 (<= (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634) 0))))) +(let ((@x24841 (trans @x24936 (rewrite (= (<= (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634) 0) $x24195)) (= $x23648 $x24195)))) +(let ((@x24943 (monotonicity (rewrite (= (+ ?v0!14 ?x11484) (+ ?x11484 ?v0!14))) (= $x23640 (>= (+ ?x11484 ?v0!14) 0))))) +(let ((@x24623 (trans @x24943 (rewrite (= (>= (+ ?x11484 ?v0!14) 0) $x23657)) (= $x23640 $x23657)))) +(let ((@x24818 (monotonicity (monotonicity @x24623 @x24841 (= $x23649 (or $x19365 $x19366 $x23657 $x24195))) (= $x24880 (or $x19903 (or $x19365 $x19366 $x23657 $x24195)))))) +(let ((@x24597 (trans @x24818 (rewrite (= (or $x19903 (or $x19365 $x19366 $x23657 $x24195)) $x24882)) (= $x24880 $x24882)))) +(let ((@x24900 (unit-resolution (mp ((_ quant-inst ?v0!14) $x24880) @x24597 $x24882) @x23333 (unit-resolution (def-axiom (or $x19381 $x15626)) (hypothesis $x19386) $x15626) (unit-resolution (def-axiom (or $x19381 $x15627)) (hypothesis $x19386) $x15627) (hypothesis $x24206) $x23657))) +(let ((@x24984 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x25035 (not $x23657) (not $x24926))) @x24900 @x24918 (hypothesis (not $x25035)) false))) +(let ((@x24787 (lemma @x24984 (or $x19381 $x25035 $x19903 $x24195 $x15871 (not $x20596))))) +(let ((@x25179 (unit-resolution (unit-resolution @x24787 @x24499 (or $x19381 $x25035 $x24195 $x15871 (not $x20596))) @x25131 @x25129 (unit-resolution (def-axiom (or $x19381 $x15876)) @x25210 $x15876) @x25210 $x25035))) (let ((@x25060 (monotonicity (symm (hypothesis $x25035) (= ?v0!14 v_b_L_H_p_G_0$)) (= ?x15633 ?x10320)))) (let ((@x25064 (unit-resolution (hypothesis (not $x25038)) (symm (monotonicity @x25060 (= ?x15634 ?x10327)) $x25038) false))) (let ((@x25067 (lemma @x25064 (or (not $x25035) $x25038)))) @@ -2944,30 +2944,30 @@ (let (($x25044 (not $x25038))) (let (($x25049 (not $x25041))) (let ((@x25051 (lemma ((_ th-lemma arith farkas 1 -1 -1 1) (hypothesis $x25041) @x24170 @x24171 (hypothesis $x11516) false) (or $x25049 (not $x20721) $x15893 $x11515)))) -(let ((@x24891 (unit-resolution @x25051 (unit-resolution (def-axiom (or $x19980 $x11516)) (hypothesis $x19983) $x11516) @x24171 @x24170 $x25049))) -(let ((@x24597 (unit-resolution @x20638 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x11608 $x11486 (not $x20596))) @x24735 @x23420 $x11608) (hypothesis $x19932) $x19929))) -(let ((@x24892 (symm (unit-resolution (def-axiom (or $x19980 $x10391)) (hypothesis $x19983) $x10391) $x20719))) -(let ((@x24061 (monotonicity (unit-resolution (def-axiom (or $x19980 $x10392)) (hypothesis $x19983) $x10392) (= ?x10372 ?x10190)))) -(let ((@x24887 (trans (monotonicity @x24061 (= ?x10373 ?x10191)) @x23175 (= ?x10373 v_b_L_H_max_G_1$)))) +(let ((@x24047 (unit-resolution @x25051 (unit-resolution (def-axiom (or $x19980 $x11516)) (hypothesis $x19983) $x11516) @x24171 @x24170 $x25049))) +(let ((@x24884 (unit-resolution @x20638 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x11608 $x11486 (not $x20596))) @x24735 @x23420 $x11608) (hypothesis $x19932) $x19929))) +(let ((@x24887 (symm (unit-resolution (def-axiom (or $x19980 $x10391)) (hypothesis $x19983) $x10391) $x20719))) +(let ((@x24982 (monotonicity (unit-resolution (def-axiom (or $x19980 $x10392)) (hypothesis $x19983) $x10392) (= ?x10372 ?x10190)))) +(let ((@x24897 (trans (monotonicity @x24982 (= ?x10373 ?x10191)) @x23175 (= ?x10373 v_b_L_H_max_G_1$)))) (let ((?x11645 (* (- 1) v_b_SL_H_witness_G_1$))) (let ((?x20724 (+ v_b_SL_H_witness_G_0$ ?x11645))) (let (($x20726 (>= ?x20724 0))) (let (($x20723 (= v_b_SL_H_witness_G_0$ v_b_SL_H_witness_G_1$))) -(let ((@x24982 (mp (unit-resolution (def-axiom (or $x19980 $x10392)) (hypothesis $x19983) $x10392) (symm (commutativity (= $x20723 $x10392)) (= $x10392 $x20723)) $x20723))) -(let ((@x24888 (lemma ((_ th-lemma arith farkas 1 -1 1) (hypothesis $x20726) (hypothesis $x11647) @x23180 false) (or $x11648 (not $x20726) $x11867)))) -(let ((@x24648 (unit-resolution @x24888 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x20723) $x20726)) @x24982 $x20726) @x23180 $x11648))) -(let ((@x24798 (unit-resolution @x20618 (unit-resolution @x20614 @x24648 (trans @x24887 @x24892 $x10374) $x19413) $x19914))) +(let ((@x24788 (mp (unit-resolution (def-axiom (or $x19980 $x10392)) (hypothesis $x19983) $x10392) (symm (commutativity (= $x20723 $x10392)) (= $x10392 $x20723)) $x20723))) +(let ((@x24909 (lemma ((_ th-lemma arith farkas 1 -1 1) (hypothesis $x20726) (hypothesis $x11647) @x23180 false) (or $x11648 (not $x20726) $x11867)))) +(let ((@x24673 (unit-resolution @x24909 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x20723) $x20726)) @x24788 $x20726) @x23180 $x11648))) +(let ((@x24789 (unit-resolution @x20618 (unit-resolution @x20614 @x24673 (trans @x24897 @x24887 $x10374) $x19413) $x19914))) (let ((@x20602 (def-axiom (or $x19381 $x15876)))) -(let ((@x25013 (unit-resolution @x20602 (unit-resolution @x20626 @x24798 (unit-resolution @x20630 @x24597 $x19920) $x19386) $x15876))) -(let ((@x25017 (unit-resolution @x24761 @x25013 (unit-resolution @x20626 @x24798 (unit-resolution @x20630 @x24597 $x19920) $x19386) @x23333 (unit-resolution @x24211 @x24171 @x24170 $x24206) (unit-resolution @x25067 (unit-resolution @x25052 @x24891 $x25044) $x25065) @x24735 false))) -(let ((@x24056 (lemma @x25017 (or $x19980 $x19903 (not $x20596) $x11867 $x15893 (not $x20721) $x19935 $x11486 $x19674)))) -(let ((@x24843 (unit-resolution @x24056 @x24499 @x24415 @x24684 @x24314 (or $x19980 (not $x20596) $x15893 (not $x20721) $x19935)))) +(let ((@x24914 (unit-resolution @x20602 (unit-resolution @x20626 @x24789 (unit-resolution @x20630 @x24884 $x19920) $x19386) $x15876))) +(let ((@x24915 (unit-resolution @x24787 @x24914 (unit-resolution @x20626 @x24789 (unit-resolution @x20630 @x24884 $x19920) $x19386) @x23333 (unit-resolution @x24211 @x24171 @x24170 $x24206) (unit-resolution @x25067 (unit-resolution @x25052 @x24047 $x25044) $x25065) @x24735 false))) +(let ((@x24889 (lemma @x24915 (or $x19980 $x19903 (not $x20596) $x11867 $x15893 (not $x20721) $x19935 $x11486 $x19674)))) +(let ((@x24843 (unit-resolution @x24889 @x24499 @x24415 @x24656 @x24314 (or $x19980 (not $x20596) $x15893 (not $x20721) $x19935)))) (let ((@x24844 (unit-resolution @x24843 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x20719) $x20721)) @x25006 $x20721) @x25299 @x24947 (unit-resolution @x20652 @x24908 $x19932) $x15893))) (let ((@x20605 (def-axiom (or $x19381 $x20603)))) (let ((@x25302 (monotonicity (unit-resolution (def-axiom (or $x19980 $x10392)) @x25299 $x10392) (= ?x10372 ?x10190)))) (let ((@x25305 (trans (monotonicity @x25302 (= ?x10373 ?x10191)) @x24314 (= ?x10373 v_b_L_H_max_G_1$)))) (let ((@x25306 (trans @x25305 (symm (unit-resolution (def-axiom (or $x19980 $x10391)) @x25299 $x10391) $x20719) $x10374))) (let ((@x25307 (mp (unit-resolution (def-axiom (or $x19980 $x10392)) @x25299 $x10392) (symm (commutativity (= $x20723 $x10392)) (= $x10392 $x20723)) $x20723))) -(let ((@x25311 (unit-resolution (unit-resolution @x24888 @x24415 (or $x11648 (not $x20726))) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x20723) $x20726)) @x25307 $x20726) $x11648))) +(let ((@x25311 (unit-resolution (unit-resolution @x24909 @x24415 (or $x11648 (not $x20726))) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x20723) $x20726)) @x25307 $x20726) $x11648))) (unit-resolution @x20626 (unit-resolution @x20618 (unit-resolution @x20614 @x25311 @x25306 $x19413) $x19914) (unit-resolution @x20605 @x24844 $x19381) (unit-resolution @x20630 @x24954 $x19920) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))