src/HOL/SMT_Examples/Boogie_Max.certs2
author haftmann
Sat Jul 05 11:01:53 2014 +0200 (2014-07-05)
changeset 57514 bdc2c6b40bf2
parent 57204 7c36ce8e45f6
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
blanchet@57204
     1
9c420ec314a920506e90cf4b4e40b4ee3ab35dec 779 0
blanchet@57170
     2
unsat
blanchet@57170
     3
((set-logic AUFLIA)
blanchet@57170
     4
(declare-fun ?v0!3 () Int)
blanchet@57170
     5
(declare-fun ?v0!2 () Int)
blanchet@57170
     6
(declare-fun ?v0!1 () Int)
blanchet@57170
     7
(declare-fun ?v0!0 () Int)
blanchet@57170
     8
(proof
blanchet@57170
     9
(let (($x109 (= v_b_max_G_3$ v_b_max_G_2$)))
blanchet@57170
    10
(let ((?x135 (v_b_array$ v_b_k_G_1$)))
blanchet@57170
    11
(let (($x136 (= ?x135 v_b_max_G_3$)))
blanchet@57170
    12
(let (($x1878 (forall ((?v0 Int) )(!(let (($x746 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
blanchet@57170
    13
(let (($x733 (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))
blanchet@57170
    14
(let (($x521 (>= ?v0 0)))
blanchet@57170
    15
(let (($x1157 (not $x521)))
blanchet@57170
    16
(or $x1157 $x733 $x746))))) :pattern ( (v_b_array$ ?v0) )))
blanchet@57170
    17
))
blanchet@57170
    18
(let (($x1883 (not $x1878)))
blanchet@57170
    19
(let (($x1886 (or $x1883 $x136)))
blanchet@57170
    20
(let (($x1889 (not $x1886)))
blanchet@57170
    21
(let (($x1070 (>= (+ v_b_max_G_3$ (* (- 1) (v_b_array$ ?v0!3))) 0)))
blanchet@57170
    22
(let (($x1048 (<= (+ v_b_p_G_1$ (* (- 1) ?v0!3)) 0)))
blanchet@57170
    23
(let (($x931 (>= ?v0!3 0)))
blanchet@57170
    24
(let (($x1298 (not $x931)))
blanchet@57170
    25
(let (($x1313 (or $x1298 $x1048 $x1070)))
blanchet@57170
    26
(let (($x1318 (not $x1313)))
blanchet@57170
    27
(let (($x1892 (or $x1318 $x1889)))
blanchet@57170
    28
(let (($x1895 (not $x1892)))
blanchet@57170
    29
(let (($x682 (>= v_b_p_G_1$ 2)))
blanchet@57170
    30
(let (($x1364 (not $x682)))
blanchet@57170
    31
(let (($x679 (>= v_b_k_G_1$ 0)))
blanchet@57170
    32
(let (($x1363 (not $x679)))
blanchet@57170
    33
(let ((?x685 (* (- 1) v_b_p_G_1$)))
blanchet@57170
    34
(let ((?x686 (+ v_b_p_G_0$ ?x685)))
blanchet@57170
    35
(let (($x684 (= ?x686 (- 1))))
blanchet@57170
    36
(let (($x1362 (not $x684)))
blanchet@57170
    37
(let (($x573 (>= v_b_p_G_0$ 1)))
blanchet@57170
    38
(let (($x1287 (not $x573)))
blanchet@57170
    39
(let (($x1361 (not $x109)))
blanchet@57170
    40
(let (($x107 (= v_b_k_G_1$ v_b_p_G_0$)))
blanchet@57170
    41
(let (($x1360 (not $x107)))
blanchet@57170
    42
(let ((?x101 (v_b_array$ v_b_p_G_0$)))
blanchet@57170
    43
(let (($x104 (= v_b_max_G_2$ ?x101)))
blanchet@57170
    44
(let (($x1359 (not $x104)))
blanchet@57170
    45
(let (($x689 (>= (+ v_b_max_G_1$ (* (- 1) ?x101)) 0)))
blanchet@57170
    46
(let (($x571 (>= v_b_k_G_0$ 0)))
blanchet@57170
    47
(let (($x1286 (not $x571)))
blanchet@57170
    48
(let (($x1898 (or $x1286 $x689 $x1359 $x1360 $x1361 $x1287 $x1362 $x1363 $x1364 $x1895)))
blanchet@57170
    49
(let (($x1901 (not $x1898)))
blanchet@57170
    50
(let (($x145 (= v_b_max_G_3$ v_b_max_G_1$)))
blanchet@57170
    51
(let (($x1376 (not $x145)))
blanchet@57170
    52
(let (($x144 (= v_b_k_G_1$ v_b_k_G_0$)))
blanchet@57170
    53
(let (($x1375 (not $x144)))
blanchet@57170
    54
(let (($x692 (not $x689)))
blanchet@57170
    55
(let (($x1904 (or $x692 $x1286 $x1375 $x1376 $x1287 $x1362 $x1363 $x1364 $x1895)))
blanchet@57170
    56
(let ((?x937 (v_b_array$ ?v0!3)))
blanchet@57170
    57
(let (($x1559 (= ?x101 ?x937)))
blanchet@57170
    58
(let (($x1563 (not $x1559)))
blanchet@57170
    59
(let ((?x1068 (* (- 1) ?x937)))
blanchet@57170
    60
(let ((?x1461 (+ ?x101 ?x1068)))
blanchet@57170
    61
(let (($x1445 (>= ?x1461 0)))
blanchet@57170
    62
(let (($x1453 (not $x1445)))
blanchet@57170
    63
(let (($x1907 (not $x1904)))
blanchet@57170
    64
(let ((@x2149 (hypothesis $x1907)))
blanchet@57170
    65
(let ((?x744 (* (- 1) v_b_max_G_3$)))
blanchet@57170
    66
(let ((?x1781 (+ v_b_max_G_1$ ?x744)))
blanchet@57170
    67
(let (($x1782 (<= ?x1781 0)))
blanchet@57170
    68
(let (($x1780 (= v_b_max_G_1$ v_b_max_G_3$)))
blanchet@57170
    69
(let ((@x2162 (mp (unit-resolution (def-axiom (or $x1904 $x145)) @x2149 $x145) (symm (commutativity (= $x1780 $x145)) (= $x145 $x1780)) $x1780)))
blanchet@57170
    70
(let (($x1436 (not $x1070)))
blanchet@57170
    71
(let ((?x62 (v_b_array$ v_b_k_G_0$)))
blanchet@57170
    72
(let (($x63 (= ?x62 v_b_max_G_1$)))
blanchet@57170
    73
(let (($x1910 (or $x1901 $x1907)))
blanchet@57170
    74
(let (($x1913 (not $x1910)))
blanchet@57170
    75
(let ((?x549 (* (- 1) v_b_p_G_0$)))
blanchet@57170
    76
(let ((?x599 (+ v_b_length$ ?x549)))
blanchet@57170
    77
(let (($x600 (<= ?x599 0)))
blanchet@57170
    78
(let (($x1916 (or $x600 $x1286 $x1287 $x1913)))
blanchet@57170
    79
(let (($x1919 (not $x1916)))
blanchet@57170
    80
(let (($x1011 (>= (+ v_b_max_G_4$ (* (- 1) (v_b_array$ ?v0!2))) 0)))
blanchet@57170
    81
(let (($x900 (<= (+ v_b_length$ (* (- 1) ?v0!2)) 0)))
blanchet@57170
    82
(let (($x897 (>= ?v0!2 0)))
blanchet@57170
    83
(let (($x1247 (not $x897)))
blanchet@57170
    84
(let (($x889 (= (v_b_array$ ?v0!1) v_b_max_G_4$)))
blanchet@57170
    85
(let (($x884 (<= (+ v_b_length$ (* (- 1) ?v0!1)) 0)))
blanchet@57170
    86
(let (($x881 (>= ?v0!1 0)))
blanchet@57170
    87
(let (($x1227 (not $x881)))
blanchet@57170
    88
(let (($x1242 (or $x1227 $x884 $x889)))
blanchet@57170
    89
(let (($x1273 (not $x1242)))
blanchet@57170
    90
(let (($x1274 (or $x1273 $x1247 $x900 $x1011)))
blanchet@57170
    91
(let (($x1275 (not $x1274)))
blanchet@57170
    92
(let (($x1861 (forall ((?v0 Int) )(!(let ((?x46 (v_b_array$ ?v0)))
blanchet@57170
    93
(let (($x86 (= ?x46 v_b_max_G_4$)))
blanchet@57170
    94
(let (($x622 (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))
blanchet@57170
    95
(let (($x521 (>= ?v0 0)))
blanchet@57170
    96
(let (($x1157 (not $x521)))
blanchet@57170
    97
(let (($x1216 (or $x1157 $x622 $x86)))
blanchet@57170
    98
(not $x1216))))))) :pattern ( (v_b_array$ ?v0) )))
blanchet@57170
    99
))
blanchet@57170
   100
(let (($x1866 (or $x1861 $x1275)))
blanchet@57170
   101
(let (($x1869 (not $x1866)))
blanchet@57170
   102
(let (($x75 (= v_b_p_G_2$ v_b_p_G_0$)))
blanchet@57170
   103
(let (($x1290 (not $x75)))
blanchet@57170
   104
(let (($x73 (= v_b_max_G_4$ v_b_max_G_1$)))
blanchet@57170
   105
(let (($x1289 (not $x73)))
blanchet@57170
   106
(let (($x71 (= v_b_k_G_2$ v_b_k_G_0$)))
blanchet@57170
   107
(let (($x1288 (not $x71)))
blanchet@57170
   108
(let (($x661 (not $x600)))
blanchet@57170
   109
(let (($x1872 (or $x661 $x1286 $x1287 $x1288 $x1289 $x1290 $x1869)))
blanchet@57170
   110
(let (($x1875 (not $x1872)))
blanchet@57170
   111
(let (($x1922 (or $x1875 $x1919)))
blanchet@57170
   112
(let (($x1925 (not $x1922)))
blanchet@57170
   113
(let (($x1403 (not $x63)))
blanchet@57170
   114
(let (($x1853 (forall ((?v0 Int) )(!(let (($x561 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
blanchet@57170
   115
(let (($x548 (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))
blanchet@57170
   116
(let (($x521 (>= ?v0 0)))
blanchet@57170
   117
(let (($x1157 (not $x521)))
blanchet@57170
   118
(or $x1157 $x548 $x561))))) :pattern ( (v_b_array$ ?v0) )))
blanchet@57170
   119
))
blanchet@57170
   120
(let (($x1858 (not $x1853)))
blanchet@57170
   121
(let ((?x30 (v_b_array$ 0)))
blanchet@57170
   122
(let (($x50 (= ?x30 v_b_max_G_0$)))
blanchet@57170
   123
(let (($x851 (not $x50)))
blanchet@57170
   124
(let (($x1928 (or $x851 $x1858 $x1403 $x1286 $x1287 $x1925)))
blanchet@57170
   125
(let (($x1931 (not $x1928)))
blanchet@57170
   126
(let (($x1934 (or $x851 $x1931)))
blanchet@57170
   127
(let (($x1937 (not $x1934)))
blanchet@57170
   128
(let (($x1845 (forall ((?v0 Int) )(!(let (($x534 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
blanchet@57170
   129
(let (($x524 (>= ?v0 1)))
blanchet@57170
   130
(let (($x521 (>= ?v0 0)))
blanchet@57170
   131
(let (($x1157 (not $x521)))
blanchet@57170
   132
(or $x1157 $x524 $x534))))) :pattern ( (v_b_array$ ?v0) )))
blanchet@57170
   133
))
blanchet@57170
   134
(let (($x1850 (not $x1845)))
blanchet@57170
   135
(let (($x1940 (or $x1850 $x1937)))
blanchet@57170
   136
(let (($x1943 (not $x1940)))
blanchet@57170
   137
(let (($x839 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0!0))) 0)))
blanchet@57170
   138
(let (($x832 (>= ?v0!0 1)))
blanchet@57170
   139
(let (($x835 (>= ?v0!0 0)))
blanchet@57170
   140
(let (($x1134 (not $x835)))
blanchet@57170
   141
(let (($x1149 (or $x1134 $x832 $x839)))
blanchet@57170
   142
(let (($x833 (not $x832)))
blanchet@57170
   143
(let (($x1154 (not $x1149)))
blanchet@57170
   144
(let ((@x1726 (hypothesis $x1154)))
blanchet@57170
   145
(let ((@x1711 ((_ th-lemma arith eq-propagate 0 0) (unit-resolution (def-axiom (or $x1149 $x835)) @x1726 $x835) (unit-resolution (def-axiom (or $x1149 $x833)) @x1726 $x833) (= ?v0!0 0))))
blanchet@57170
   146
(let ((@x1715 (symm (monotonicity @x1711 (= (v_b_array$ ?v0!0) ?x30)) (= ?x30 (v_b_array$ ?v0!0)))))
blanchet@57170
   147
(let (($x31 (= v_b_max_G_0$ ?x30)))
blanchet@57170
   148
(let (($x495 (<= v_b_length$ 0)))
blanchet@57170
   149
(let (($x496 (not $x495)))
blanchet@57170
   150
(let (($x511 (and $x496 $x31)))
blanchet@57170
   151
(let (($x752 (forall ((?v0 Int) )(let (($x746 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
blanchet@57170
   152
(let (($x521 (>= ?v0 0)))
blanchet@57170
   153
(let (($x738 (and $x521 (not (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))))
blanchet@57170
   154
(let (($x741 (not $x738)))
blanchet@57170
   155
(or $x741 $x746))))))
blanchet@57170
   156
))
blanchet@57170
   157
(let (($x755 (not $x752)))
blanchet@57170
   158
(let (($x758 (or $x755 $x136)))
blanchet@57170
   159
(let (($x761 (and $x752 $x758)))
blanchet@57170
   160
(let (($x784 (and $x689 $x571 $x144 $x145 $x573 $x684 $x679 $x682)))
blanchet@57170
   161
(let (($x789 (not $x784)))
blanchet@57170
   162
(let (($x792 (or $x789 $x761)))
blanchet@57170
   163
(let (($x725 (and $x571 $x692 $x104 $x107 $x109 $x573 $x684 $x679 $x682)))
blanchet@57170
   164
(let (($x730 (not $x725)))
blanchet@57170
   165
(let (($x764 (or $x730 $x761)))
blanchet@57170
   166
(let (($x795 (and $x764 $x792)))
blanchet@57170
   167
(let (($x670 (and $x661 $x571 $x573)))
blanchet@57170
   168
(let (($x675 (not $x670)))
blanchet@57170
   169
(let (($x798 (or $x675 $x795)))
blanchet@57170
   170
(let (($x649 (forall ((?v0 Int) )(let (($x521 (>= ?v0 0)))
blanchet@57170
   171
(let (($x626 (and $x521 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
blanchet@57170
   172
(let (($x629 (not $x626)))
blanchet@57170
   173
(or $x629 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_4$)) 0))))))
blanchet@57170
   174
))
blanchet@57170
   175
(let (($x635 (exists ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
blanchet@57170
   176
(let (($x86 (= ?x46 v_b_max_G_4$)))
blanchet@57170
   177
(let (($x521 (>= ?v0 0)))
blanchet@57170
   178
(let (($x626 (and $x521 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
blanchet@57170
   179
(let (($x629 (not $x626)))
blanchet@57170
   180
(or $x629 $x86)))))))
blanchet@57170
   181
))
blanchet@57170
   182
(let (($x638 (not $x635)))
blanchet@57170
   183
(let (($x652 (or $x638 $x649)))
blanchet@57170
   184
(let (($x655 (and $x635 $x652)))
blanchet@57170
   185
(let (($x612 (and $x600 $x571 $x573 $x71 $x73 $x75)))
blanchet@57170
   186
(let (($x617 (not $x612)))
blanchet@57170
   187
(let (($x658 (or $x617 $x655)))
blanchet@57170
   188
(let (($x801 (and $x658 $x798)))
blanchet@57170
   189
(let (($x567 (forall ((?v0 Int) )(let (($x561 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
blanchet@57170
   190
(let (($x521 (>= ?v0 0)))
blanchet@57170
   191
(let (($x553 (and $x521 (not (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))))
blanchet@57170
   192
(let (($x556 (not $x553)))
blanchet@57170
   193
(or $x556 $x561))))))
blanchet@57170
   194
))
blanchet@57170
   195
(let (($x591 (and $x50 $x567 $x63 $x571 $x573)))
blanchet@57170
   196
(let (($x596 (not $x591)))
blanchet@57170
   197
(let (($x804 (or $x596 $x801)))
blanchet@57170
   198
(let (($x807 (and $x50 $x804)))
blanchet@57170
   199
(let (($x541 (forall ((?v0 Int) )(let (($x534 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
blanchet@57170
   200
(let (($x521 (>= ?v0 0)))
blanchet@57170
   201
(let (($x526 (and $x521 (not (>= ?v0 1)))))
blanchet@57170
   202
(let (($x529 (not $x526)))
blanchet@57170
   203
(or $x529 $x534))))))
blanchet@57170
   204
))
blanchet@57170
   205
(let (($x544 (not $x541)))
blanchet@57170
   206
(let (($x810 (or $x544 $x807)))
blanchet@57170
   207
(let (($x813 (and $x541 $x810)))
blanchet@57170
   208
(let (($x819 (not (or (not $x511) $x813))))
blanchet@57170
   209
(let (($x138 (=> (and $x136 false) true)))
blanchet@57170
   210
(let (($x139 (and $x136 $x138)))
blanchet@57170
   211
(let (($x134 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
blanchet@57170
   212
(let (($x132 (<= ?x46 v_b_max_G_3$)))
blanchet@57170
   213
(let (($x43 (<= 0 ?v0)))
blanchet@57170
   214
(let (($x131 (and $x43 (< ?v0 v_b_p_G_1$))))
blanchet@57170
   215
(=> $x131 $x132))))))
blanchet@57170
   216
))
blanchet@57170
   217
(let (($x140 (=> $x134 $x139)))
blanchet@57170
   218
(let (($x141 (and $x134 $x140)))
blanchet@57170
   219
(let (($x119 (and (= v_b_p_G_1$ (+ v_b_p_G_0$ 1)) (and (and (<= 0 v_b_k_G_1$) (<= 2 v_b_p_G_1$)) true))))
blanchet@57170
   220
(let (($x54 (<= 1 v_b_p_G_0$)))
blanchet@57170
   221
(let (($x110 (<= 0 v_b_k_G_1$)))
blanchet@57170
   222
(let (($x111 (and $x110 $x54)))
blanchet@57170
   223
(let (($x121 (and true (and $x111 $x119))))
blanchet@57170
   224
(let (($x148 (and true (and $x144 (and $x145 $x121)))))
blanchet@57170
   225
(let (($x55 (and (<= 0 v_b_k_G_0$) $x54)))
blanchet@57170
   226
(let (($x143 (<= ?x101 v_b_max_G_1$)))
blanchet@57170
   227
(let (($x152 (and true (and $x55 (and $x143 (and $x55 $x148))))))
blanchet@57170
   228
(let (($x153 (=> $x152 $x141)))
blanchet@57170
   229
(let (($x126 (and $x104 (and (and $x54 $x54) (and true (and $x107 (and $x109 $x121)))))))
blanchet@57170
   230
(let (($x102 (< v_b_max_G_1$ ?x101)))
blanchet@57170
   231
(let (($x129 (and true (and $x55 (and $x102 $x126)))))
blanchet@57170
   232
(let (($x142 (=> $x129 $x141)))
blanchet@57170
   233
(let (($x155 (=> (and true (and $x55 (and (< v_b_p_G_0$ v_b_length$) $x55))) (and $x142 $x153))))
blanchet@57170
   234
(let (($x91 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
blanchet@57170
   235
(let (($x89 (<= ?x46 v_b_max_G_4$)))
blanchet@57170
   236
(let (($x43 (<= 0 ?v0)))
blanchet@57170
   237
(let (($x85 (and $x43 (< ?v0 v_b_length$))))
blanchet@57170
   238
(=> $x85 $x89))))))
blanchet@57170
   239
))
blanchet@57170
   240
(let (($x92 (=> $x91 true)))
blanchet@57170
   241
(let (($x93 (and $x91 $x92)))
blanchet@57170
   242
(let (($x88 (exists ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
blanchet@57170
   243
(let (($x86 (= ?x46 v_b_max_G_4$)))
blanchet@57170
   244
(let (($x43 (<= 0 ?v0)))
blanchet@57170
   245
(let (($x85 (and $x43 (< ?v0 v_b_length$))))
blanchet@57170
   246
(=> $x85 $x86))))))
blanchet@57170
   247
))
blanchet@57170
   248
(let (($x94 (=> $x88 $x93)))
blanchet@57170
   249
(let (($x69 (<= v_b_length$ v_b_p_G_0$)))
blanchet@57170
   250
(let (($x81 (and $x69 (and $x55 (and true (and $x71 (and $x73 (and $x75 true))))))))
blanchet@57170
   251
(let (($x83 (and true (and $x55 $x81))))
blanchet@57170
   252
(let (($x96 (=> $x83 (and $x88 $x94))))
blanchet@57170
   253
(let (($x64 (and $x63 $x55)))
blanchet@57170
   254
(let (($x61 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
blanchet@57170
   255
(let (($x59 (<= ?x46 v_b_max_G_1$)))
blanchet@57170
   256
(let (($x43 (<= 0 ?v0)))
blanchet@57170
   257
(let (($x57 (and $x43 (< ?v0 v_b_p_G_0$))))
blanchet@57170
   258
(=> $x57 $x59))))))
blanchet@57170
   259
))
blanchet@57170
   260
(let (($x67 (and true (and $x55 (and $x61 $x64)))))
blanchet@57170
   261
(let (($x157 (=> (and $x50 $x67) (and $x96 $x155))))
blanchet@57170
   262
(let (($x49 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
blanchet@57170
   263
(let (($x47 (<= ?x46 v_b_max_G_0$)))
blanchet@57170
   264
(let (($x43 (<= 0 ?v0)))
blanchet@57170
   265
(let (($x45 (and $x43 (< ?v0 1))))
blanchet@57170
   266
(=> $x45 $x47))))))
blanchet@57170
   267
))
blanchet@57170
   268
(let (($x159 (=> $x49 (and $x50 $x157))))
blanchet@57170
   269
(let (($x32 (<= 0 0)))
blanchet@57170
   270
(let (($x38 (and $x31 (and $x32 (and $x32 (and (<= 1 1) (<= 1 1)))))))
blanchet@57170
   271
(let (($x39 (and true $x38)))
blanchet@57170
   272
(let (($x28 (< 0 v_b_length$)))
blanchet@57170
   273
(let (($x41 (and true (and $x28 $x39))))
blanchet@57170
   274
(let (($x161 (=> $x41 (and $x49 $x159))))
blanchet@57170
   275
(let (($x162 (not $x161)))
blanchet@57170
   276
(let (($x362 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
blanchet@57170
   277
(let (($x132 (<= ?x46 v_b_max_G_3$)))
blanchet@57170
   278
(or (not (and (<= 0 ?v0) (< ?v0 v_b_p_G_1$))) $x132))))
blanchet@57170
   279
))
blanchet@57170
   280
(let (($x385 (or (not $x362) $x136)))
blanchet@57170
   281
(let (($x390 (and $x362 $x385)))
blanchet@57170
   282
(let (($x117 (and $x110 (<= 2 v_b_p_G_1$))))
blanchet@57170
   283
(let (($x308 (= v_b_p_G_1$ (+ 1 v_b_p_G_0$))))
blanchet@57170
   284
(let (($x313 (and $x308 $x117)))
blanchet@57170
   285
(let (($x316 (and $x111 $x313)))
blanchet@57170
   286
(let (($x402 (and $x145 $x316)))
blanchet@57170
   287
(let (($x405 (and $x144 $x402)))
blanchet@57170
   288
(let (($x415 (and $x55 $x405)))
blanchet@57170
   289
(let (($x418 (and $x143 $x415)))
blanchet@57170
   290
(let (($x421 (and $x55 $x418)))
blanchet@57170
   291
(let (($x435 (or (not $x421) $x390)))
blanchet@57170
   292
(let (($x326 (and $x109 $x316)))
blanchet@57170
   293
(let (($x329 (and $x107 $x326)))
blanchet@57170
   294
(let (($x339 (and $x54 $x329)))
blanchet@57170
   295
(let (($x342 (and $x104 $x339)))
blanchet@57170
   296
(let (($x345 (and $x102 $x342)))
blanchet@57170
   297
(let (($x348 (and $x55 $x345)))
blanchet@57170
   298
(let (($x397 (or (not $x348) $x390)))
blanchet@57170
   299
(let (($x440 (and $x397 $x435)))
blanchet@57170
   300
(let (($x447 (or (not (and $x55 (and (< v_b_p_G_0$ v_b_length$) $x55))) $x440)))
blanchet@57170
   301
(let (($x263 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
blanchet@57170
   302
(let (($x89 (<= ?x46 v_b_max_G_4$)))
blanchet@57170
   303
(let (($x43 (<= 0 ?v0)))
blanchet@57170
   304
(let (($x85 (and $x43 (< ?v0 v_b_length$))))
blanchet@57170
   305
(let (($x253 (not $x85)))
blanchet@57170
   306
(or $x253 $x89)))))))
blanchet@57170
   307
))
blanchet@57170
   308
(let (($x257 (exists ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
blanchet@57170
   309
(let (($x86 (= ?x46 v_b_max_G_4$)))
blanchet@57170
   310
(let (($x43 (<= 0 ?v0)))
blanchet@57170
   311
(let (($x85 (and $x43 (< ?v0 v_b_length$))))
blanchet@57170
   312
(let (($x253 (not $x85)))
blanchet@57170
   313
(or $x253 $x86)))))))
blanchet@57170
   314
))
blanchet@57170
   315
(let (($x284 (or (not $x257) $x263)))
blanchet@57170
   316
(let (($x289 (and $x257 $x284)))
blanchet@57170
   317
(let (($x296 (or (not (and $x55 (and $x69 (and $x55 (and $x71 (and $x73 $x75)))))) $x289)))
blanchet@57170
   318
(let (($x452 (and $x296 $x447)))
blanchet@57170
   319
(let (($x203 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
blanchet@57170
   320
(let (($x59 (<= ?x46 v_b_max_G_1$)))
blanchet@57170
   321
(or (not (and (<= 0 ?v0) (< ?v0 v_b_p_G_0$))) $x59))))
blanchet@57170
   322
))
blanchet@57170
   323
(let (($x206 (and $x203 $x64)))
blanchet@57170
   324
(let (($x209 (and $x55 $x206)))
blanchet@57170
   325
(let (($x219 (and $x50 $x209)))
blanchet@57170
   326
(let (($x459 (or (not $x219) $x452)))
blanchet@57170
   327
(let (($x464 (and $x50 $x459)))
blanchet@57170
   328
(let (($x196 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
blanchet@57170
   329
(let (($x47 (<= ?x46 v_b_max_G_0$)))
blanchet@57170
   330
(or (not (and (<= 0 ?v0) (< ?v0 1))) $x47))))
blanchet@57170
   331
))
blanchet@57170
   332
(let (($x471 (or (not $x196) $x464)))
blanchet@57170
   333
(let (($x476 (and $x196 $x471)))
blanchet@57170
   334
(let (($x483 (or (not (and $x28 (and $x31 (and $x32 (and $x32 (<= 1 1)))))) $x476)))
blanchet@57170
   335
(let (($x746 (<= (+ (v_b_array$ ?0) ?x744) 0)))
blanchet@57170
   336
(let (($x521 (>= ?0 0)))
blanchet@57170
   337
(let (($x738 (and $x521 (not (>= (+ ?0 ?x685) 0)))))
blanchet@57170
   338
(let (($x741 (not $x738)))
blanchet@57170
   339
(let (($x749 (or $x741 $x746)))
blanchet@57170
   340
(let ((?x46 (v_b_array$ ?0)))
blanchet@57170
   341
(let (($x132 (<= ?x46 v_b_max_G_3$)))
blanchet@57170
   342
(let (($x359 (or (not (and (<= 0 ?0) (< ?0 v_b_p_G_1$))) $x132)))
blanchet@57170
   343
(let ((@x520 (rewrite (= (<= 0 ?0) $x521))))
blanchet@57170
   344
(let ((@x740 (monotonicity @x520 (rewrite (= (< ?0 v_b_p_G_1$) (not (>= (+ ?0 ?x685) 0)))) (= (and (<= 0 ?0) (< ?0 v_b_p_G_1$)) $x738))))
blanchet@57170
   345
(let ((@x743 (monotonicity @x740 (= (not (and (<= 0 ?0) (< ?0 v_b_p_G_1$))) $x741))))
blanchet@57170
   346
(let ((@x754 (quant-intro (monotonicity @x743 (rewrite (= $x132 $x746)) (= $x359 $x749)) (= $x362 $x752))))
blanchet@57170
   347
(let ((@x760 (monotonicity (monotonicity @x754 (= (not $x362) $x755)) (= $x385 $x758))))
blanchet@57170
   348
(let (($x772 (and $x144 (and $x145 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
blanchet@57170
   349
(let (($x576 (and $x571 $x573)))
blanchet@57170
   350
(let (($x770 (= $x402 (and $x145 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
blanchet@57170
   351
(let ((@x697 (monotonicity (rewrite (= $x110 $x679)) (rewrite (= (<= 2 v_b_p_G_1$) $x682)) (= $x117 (and $x679 $x682)))))
blanchet@57170
   352
(let ((@x700 (monotonicity (rewrite (= $x308 $x684)) @x697 (= $x313 (and $x684 (and $x679 $x682))))))
blanchet@57170
   353
(let ((@x575 (rewrite (= $x54 $x573))))
blanchet@57170
   354
(let ((@x703 (monotonicity (rewrite (= $x110 $x679)) @x575 (= $x111 (and $x679 $x573)))))
blanchet@57170
   355
(let ((@x706 (monotonicity @x703 @x700 (= $x316 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
blanchet@57170
   356
(let ((@x578 (monotonicity (rewrite (= (<= 0 v_b_k_G_0$) $x571)) @x575 (= $x55 $x576))))
blanchet@57170
   357
(let ((@x777 (monotonicity @x578 (monotonicity (monotonicity @x706 $x770) (= $x405 $x772)) (= $x415 (and $x576 $x772)))))
blanchet@57170
   358
(let ((@x780 (monotonicity (rewrite (= $x143 $x689)) @x777 (= $x418 (and $x689 (and $x576 $x772))))))
blanchet@57170
   359
(let ((@x783 (monotonicity @x578 @x780 (= $x421 (and $x576 (and $x689 (and $x576 $x772)))))))
blanchet@57170
   360
(let ((@x788 (trans @x783 (rewrite (= (and $x576 (and $x689 (and $x576 $x772))) $x784)) (= $x421 $x784))))
blanchet@57170
   361
(let ((@x794 (monotonicity (monotonicity @x788 (= (not $x421) $x789)) (monotonicity @x754 @x760 (= $x390 $x761)) (= $x435 $x792))))
blanchet@57170
   362
(let (($x710 (and $x107 (and $x109 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
blanchet@57170
   363
(let ((@x727 (rewrite (= (and $x576 (and $x692 (and $x104 (and $x573 $x710)))) $x725))))
blanchet@57170
   364
(let (($x708 (= $x326 (and $x109 (and (and $x679 $x573) (and $x684 (and $x679 $x682)))))))
blanchet@57170
   365
(let ((@x715 (monotonicity @x575 (monotonicity (monotonicity @x706 $x708) (= $x329 $x710)) (= $x339 (and $x573 $x710)))))
blanchet@57170
   366
(let ((@x721 (monotonicity (rewrite (= $x102 $x692)) (monotonicity @x715 (= $x342 (and $x104 (and $x573 $x710)))) (= $x345 (and $x692 (and $x104 (and $x573 $x710)))))))
blanchet@57170
   367
(let ((@x724 (monotonicity @x578 @x721 (= $x348 (and $x576 (and $x692 (and $x104 (and $x573 $x710))))))))
blanchet@57170
   368
(let ((@x732 (monotonicity (trans @x724 @x727 (= $x348 $x725)) (= (not $x348) $x730))))
blanchet@57170
   369
(let ((@x766 (monotonicity @x732 (monotonicity @x754 @x760 (= $x390 $x761)) (= $x397 $x764))))
blanchet@57170
   370
(let (($x99 (and $x55 (and (< v_b_p_G_0$ v_b_length$) $x55))))
blanchet@57170
   371
(let ((@x666 (monotonicity (rewrite (= (< v_b_p_G_0$ v_b_length$) $x661)) @x578 (= (and (< v_b_p_G_0$ v_b_length$) $x55) (and $x661 $x576)))))
blanchet@57170
   372
(let ((@x674 (trans (monotonicity @x578 @x666 (= $x99 (and $x576 (and $x661 $x576)))) (rewrite (= (and $x576 (and $x661 $x576)) $x670)) (= $x99 $x670))))
blanchet@57170
   373
(let ((@x800 (monotonicity (monotonicity @x674 (= (not $x99) $x675)) (monotonicity @x766 @x794 (= $x440 $x795)) (= $x447 $x798))))
blanchet@57170
   374
(let (($x626 (and $x521 (not (<= (+ v_b_length$ (* (- 1) ?0)) 0)))))
blanchet@57170
   375
(let (($x629 (not $x626)))
blanchet@57170
   376
(let (($x89 (<= ?x46 v_b_max_G_4$)))
blanchet@57170
   377
(let (($x43 (<= 0 ?0)))
blanchet@57170
   378
(let (($x85 (and $x43 (< ?0 v_b_length$))))
blanchet@57170
   379
(let (($x253 (not $x85)))
blanchet@57170
   380
(let (($x260 (or $x253 $x89)))
blanchet@57170
   381
(let (($x624 (= (< ?0 v_b_length$) (not (<= (+ v_b_length$ (* (- 1) ?0)) 0)))))
blanchet@57170
   382
(let ((@x631 (monotonicity (monotonicity @x520 (rewrite $x624) (= $x85 $x626)) (= $x253 $x629))))
blanchet@57170
   383
(let ((@x648 (monotonicity @x631 (rewrite (= $x89 (<= (+ ?x46 (* (- 1) v_b_max_G_4$)) 0))) (= $x260 (or $x629 (<= (+ ?x46 (* (- 1) v_b_max_G_4$)) 0))))))
blanchet@57170
   384
(let (($x86 (= ?x46 v_b_max_G_4$)))
blanchet@57170
   385
(let (($x632 (or $x629 $x86)))
blanchet@57170
   386
(let (($x254 (or $x253 $x86)))
blanchet@57170
   387
(let ((@x640 (monotonicity (quant-intro (monotonicity @x631 (= $x254 $x632)) (= $x257 $x635)) (= (not $x257) $x638))))
blanchet@57170
   388
(let ((@x657 (monotonicity (quant-intro (monotonicity @x631 (= $x254 $x632)) (= $x257 $x635)) (monotonicity @x640 (quant-intro @x648 (= $x263 $x649)) (= $x284 $x652)) (= $x289 $x655))))
blanchet@57170
   389
(let (($x618 (= (not (and $x55 (and $x69 (and $x55 (and $x71 (and $x73 $x75)))))) $x617)))
blanchet@57170
   390
(let (($x227 (and $x71 (and $x73 $x75))))
blanchet@57170
   391
(let (($x237 (and $x55 $x227)))
blanchet@57170
   392
(let (($x240 (and $x69 $x237)))
blanchet@57170
   393
(let (($x243 (and $x55 $x240)))
blanchet@57170
   394
(let ((@x608 (monotonicity (rewrite (= $x69 $x600)) (monotonicity @x578 (= $x237 (and $x576 $x227))) (= $x240 (and $x600 (and $x576 $x227))))))
blanchet@57170
   395
(let ((@x611 (monotonicity @x578 @x608 (= $x243 (and $x576 (and $x600 (and $x576 $x227)))))))
blanchet@57170
   396
(let ((@x616 (trans @x611 (rewrite (= (and $x576 (and $x600 (and $x576 $x227))) $x612)) (= $x243 $x612))))
blanchet@57170
   397
(let ((@x803 (monotonicity (monotonicity (monotonicity @x616 $x618) @x657 (= $x296 $x658)) @x800 (= $x452 $x801))))
blanchet@57170
   398
(let ((@x593 (rewrite (= (and $x50 (and $x576 (and $x567 (and $x63 $x576)))) $x591))))
blanchet@57170
   399
(let (($x561 (<= (+ ?x46 (* (- 1) v_b_max_G_1$)) 0)))
blanchet@57170
   400
(let (($x553 (and $x521 (not (>= (+ ?0 ?x549) 0)))))
blanchet@57170
   401
(let (($x556 (not $x553)))
blanchet@57170
   402
(let (($x564 (or $x556 $x561)))
blanchet@57170
   403
(let (($x59 (<= ?x46 v_b_max_G_1$)))
blanchet@57170
   404
(let (($x200 (or (not (and $x43 (< ?0 v_b_p_G_0$))) $x59)))
blanchet@57170
   405
(let ((@x555 (monotonicity @x520 (rewrite (= (< ?0 v_b_p_G_0$) (not (>= (+ ?0 ?x549) 0)))) (= (and $x43 (< ?0 v_b_p_G_0$)) $x553))))
blanchet@57170
   406
(let ((@x566 (monotonicity (monotonicity @x555 (= (not (and $x43 (< ?0 v_b_p_G_0$))) $x556)) (rewrite (= $x59 $x561)) (= $x200 $x564))))
blanchet@57170
   407
(let ((@x584 (monotonicity (quant-intro @x566 (= $x203 $x567)) (monotonicity @x578 (= $x64 (and $x63 $x576))) (= $x206 (and $x567 (and $x63 $x576))))))
blanchet@57170
   408
(let ((@x587 (monotonicity @x578 @x584 (= $x209 (and $x576 (and $x567 (and $x63 $x576)))))))
blanchet@57170
   409
(let ((@x590 (monotonicity @x587 (= $x219 (and $x50 (and $x576 (and $x567 (and $x63 $x576))))))))
blanchet@57170
   410
(let ((@x598 (monotonicity (trans @x590 @x593 (= $x219 $x591)) (= (not $x219) $x596))))
blanchet@57170
   411
(let ((@x809 (monotonicity (monotonicity @x598 @x803 (= $x459 $x804)) (= $x464 $x807))))
blanchet@57170
   412
(let (($x534 (>= (+ v_b_max_G_0$ (* (- 1) ?x46)) 0)))
blanchet@57170
   413
(let (($x526 (and $x521 (not (>= ?0 1)))))
blanchet@57170
   414
(let (($x529 (not $x526)))
blanchet@57170
   415
(let (($x538 (or $x529 $x534)))
blanchet@57170
   416
(let (($x47 (<= ?x46 v_b_max_G_0$)))
blanchet@57170
   417
(let (($x193 (or (not (and $x43 (< ?0 1))) $x47)))
blanchet@57170
   418
(let ((@x528 (monotonicity @x520 (rewrite (= (< ?0 1) (not (>= ?0 1)))) (= (and $x43 (< ?0 1)) $x526))))
blanchet@57170
   419
(let ((@x540 (monotonicity (monotonicity @x528 (= (not (and $x43 (< ?0 1))) $x529)) (rewrite (= $x47 $x534)) (= $x193 $x538))))
blanchet@57170
   420
(let ((@x546 (monotonicity (quant-intro @x540 (= $x196 $x541)) (= (not $x196) $x544))))
blanchet@57170
   421
(let ((@x815 (monotonicity (quant-intro @x540 (= $x196 $x541)) (monotonicity @x546 @x809 (= $x471 $x810)) (= $x476 $x813))))
blanchet@57170
   422
(let (($x517 (= (not (and $x28 (and $x31 (and $x32 (and $x32 (<= 1 1)))))) (not $x511))))
blanchet@57170
   423
(let (($x34 (<= 1 1)))
blanchet@57170
   424
(let (($x166 (and $x32 $x34)))
blanchet@57170
   425
(let (($x169 (and $x32 $x166)))
blanchet@57170
   426
(let (($x172 (and $x31 $x169)))
blanchet@57170
   427
(let (($x182 (and $x28 $x172)))
blanchet@57170
   428
(let ((@x513 (rewrite (= (and $x496 (and $x31 (and true (and true true)))) $x511))))
blanchet@57170
   429
(let ((@x501 (monotonicity (rewrite (= $x32 true)) (rewrite (= $x34 true)) (= $x166 (and true true)))))
blanchet@57170
   430
(let ((@x504 (monotonicity (rewrite (= $x32 true)) @x501 (= $x169 (and true (and true true))))))
blanchet@57170
   431
(let ((@x507 (monotonicity @x504 (= $x172 (and $x31 (and true (and true true)))))))
blanchet@57170
   432
(let ((@x510 (monotonicity (rewrite (= $x28 $x496)) @x507 (= $x182 (and $x496 (and $x31 (and true (and true true))))))))
blanchet@57170
   433
(let ((@x818 (monotonicity (monotonicity (trans @x510 @x513 (= $x182 $x511)) $x517) @x815 (= $x483 (or (not $x511) $x813)))))
blanchet@57170
   434
(let ((@x369 (monotonicity (rewrite (= (and $x136 false) false)) (= $x138 (=> false true)))))
blanchet@57170
   435
(let ((@x373 (trans @x369 (rewrite (= (=> false true) true)) (= $x138 true))))
blanchet@57170
   436
(let ((@x380 (trans (monotonicity @x373 (= $x139 (and $x136 true))) (rewrite (= (and $x136 true) $x136)) (= $x139 $x136))))
blanchet@57170
   437
(let ((@x364 (quant-intro (rewrite (= (=> (and $x43 (< ?0 v_b_p_G_1$)) $x132) $x359)) (= $x134 $x362))))
blanchet@57170
   438
(let ((@x389 (trans (monotonicity @x364 @x380 (= $x140 (=> $x362 $x136))) (rewrite (= (=> $x362 $x136) $x385)) (= $x140 $x385))))
blanchet@57170
   439
(let ((@x310 (monotonicity (rewrite (= (+ v_b_p_G_0$ 1) (+ 1 v_b_p_G_0$))) (= (= v_b_p_G_1$ (+ v_b_p_G_0$ 1)) $x308))))
blanchet@57170
   440
(let ((@x315 (monotonicity @x310 (rewrite (= (and $x117 true) $x117)) (= $x119 $x313))))
blanchet@57170
   441
(let ((@x321 (monotonicity (monotonicity @x315 (= (and $x111 $x119) $x316)) (= $x121 (and true $x316)))))
blanchet@57170
   442
(let ((@x404 (monotonicity (trans @x321 (rewrite (= (and true $x316) $x316)) (= $x121 $x316)) (= (and $x145 $x121) $x402))))
blanchet@57170
   443
(let ((@x410 (monotonicity (monotonicity @x404 (= (and $x144 (and $x145 $x121)) $x405)) (= $x148 (and true $x405)))))
blanchet@57170
   444
(let ((@x417 (monotonicity (trans @x410 (rewrite (= (and true $x405) $x405)) (= $x148 $x405)) (= (and $x55 $x148) $x415))))
blanchet@57170
   445
(let ((@x423 (monotonicity (monotonicity @x417 (= (and $x143 (and $x55 $x148)) $x418)) (= (and $x55 (and $x143 (and $x55 $x148))) $x421))))
blanchet@57170
   446
(let ((@x430 (trans (monotonicity @x423 (= $x152 (and true $x421))) (rewrite (= (and true $x421) $x421)) (= $x152 $x421))))
blanchet@57170
   447
(let ((@x433 (monotonicity @x430 (monotonicity @x364 @x389 (= $x141 $x390)) (= $x153 (=> $x421 $x390)))))
blanchet@57170
   448
(let (($x340 (= (and (and $x54 $x54) (and true (and $x107 (and $x109 $x121)))) $x339)))
blanchet@57170
   449
(let ((@x328 (monotonicity (trans @x321 (rewrite (= (and true $x316) $x316)) (= $x121 $x316)) (= (and $x109 $x121) $x326))))
blanchet@57170
   450
(let ((@x334 (monotonicity (monotonicity @x328 (= (and $x107 (and $x109 $x121)) $x329)) (= (and true (and $x107 (and $x109 $x121))) (and true $x329)))))
blanchet@57170
   451
(let ((@x338 (trans @x334 (rewrite (= (and true $x329) $x329)) (= (and true (and $x107 (and $x109 $x121))) $x329))))
blanchet@57170
   452
(let ((@x344 (monotonicity (monotonicity (rewrite (= (and $x54 $x54) $x54)) @x338 $x340) (= $x126 $x342))))
blanchet@57170
   453
(let ((@x350 (monotonicity (monotonicity @x344 (= (and $x102 $x126) $x345)) (= (and $x55 (and $x102 $x126)) $x348))))
blanchet@57170
   454
(let ((@x357 (trans (monotonicity @x350 (= $x129 (and true $x348))) (rewrite (= (and true $x348) $x348)) (= $x129 $x348))))
blanchet@57170
   455
(let ((@x395 (monotonicity @x357 (monotonicity @x364 @x389 (= $x141 $x390)) (= $x142 (=> $x348 $x390)))))
blanchet@57170
   456
(let ((@x442 (monotonicity (trans @x395 (rewrite (= (=> $x348 $x390) $x397)) (= $x142 $x397)) (trans @x433 (rewrite (= (=> $x421 $x390) $x435)) (= $x153 $x435)) (= (and $x142 $x153) $x440))))
blanchet@57170
   457
(let ((@x445 (monotonicity (rewrite (= (and true $x99) $x99)) @x442 (= $x155 (=> $x99 $x440)))))
blanchet@57170
   458
(let ((@x268 (monotonicity (quant-intro (rewrite (= (=> $x85 $x89) $x260)) (= $x91 $x263)) (= $x92 (=> $x263 true)))))
blanchet@57170
   459
(let ((@x272 (trans @x268 (rewrite (= (=> $x263 true) true)) (= $x92 true))))
blanchet@57170
   460
(let ((@x275 (monotonicity (quant-intro (rewrite (= (=> $x85 $x89) $x260)) (= $x91 $x263)) @x272 (= $x93 (and $x263 true)))))
blanchet@57170
   461
(let ((@x282 (monotonicity (quant-intro (rewrite (= (=> $x85 $x86) $x254)) (= $x88 $x257)) (trans @x275 (rewrite (= (and $x263 true) $x263)) (= $x93 $x263)) (= $x94 (=> $x257 $x263)))))
blanchet@57170
   462
(let ((@x291 (monotonicity (quant-intro (rewrite (= (=> $x85 $x86) $x254)) (= $x88 $x257)) (trans @x282 (rewrite (= (=> $x257 $x263) $x284)) (= $x94 $x284)) (= (and $x88 $x94) $x289))))
blanchet@57170
   463
(let (($x238 (= (and $x55 (and true (and $x71 (and $x73 (and $x75 true))))) $x237)))
blanchet@57170
   464
(let (($x79 (and true (and $x71 (and $x73 (and $x75 true))))))
blanchet@57170
   465
(let ((@x226 (monotonicity (rewrite (= (and $x75 true) $x75)) (= (and $x73 (and $x75 true)) (and $x73 $x75)))))
blanchet@57170
   466
(let ((@x229 (monotonicity @x226 (= (and $x71 (and $x73 (and $x75 true))) $x227))))
blanchet@57170
   467
(let ((@x236 (trans (monotonicity @x229 (= $x79 (and true $x227))) (rewrite (= (and true $x227) $x227)) (= $x79 $x227))))
blanchet@57170
   468
(let ((@x245 (monotonicity (monotonicity (monotonicity @x236 $x238) (= $x81 $x240)) (= (and $x55 $x81) $x243))))
blanchet@57170
   469
(let ((@x252 (trans (monotonicity @x245 (= $x83 (and true $x243))) (rewrite (= (and true $x243) $x243)) (= $x83 $x243))))
blanchet@57170
   470
(let ((@x300 (trans (monotonicity @x252 @x291 (= $x96 (=> $x243 $x289))) (rewrite (= (=> $x243 $x289) $x296)) (= $x96 $x296))))
blanchet@57170
   471
(let ((@x454 (monotonicity @x300 (trans @x445 (rewrite (= (=> $x99 $x440) $x447)) (= $x155 $x447)) (= (and $x96 $x155) $x452))))
blanchet@57170
   472
(let ((@x205 (quant-intro (rewrite (= (=> (and $x43 (< ?0 v_b_p_G_0$)) $x59) $x200)) (= $x61 $x203))))
blanchet@57170
   473
(let ((@x211 (monotonicity (monotonicity @x205 (= (and $x61 $x64) $x206)) (= (and $x55 (and $x61 $x64)) $x209))))
blanchet@57170
   474
(let ((@x218 (trans (monotonicity @x211 (= $x67 (and true $x209))) (rewrite (= (and true $x209) $x209)) (= $x67 $x209))))
blanchet@57170
   475
(let ((@x457 (monotonicity (monotonicity @x218 (= (and $x50 $x67) $x219)) @x454 (= $x157 (=> $x219 $x452)))))
blanchet@57170
   476
(let ((@x466 (monotonicity (trans @x457 (rewrite (= (=> $x219 $x452) $x459)) (= $x157 $x459)) (= (and $x50 $x157) $x464))))
blanchet@57170
   477
(let ((@x198 (quant-intro (rewrite (= (=> (and $x43 (< ?0 1)) $x47) $x193)) (= $x49 $x196))))
blanchet@57170
   478
(let ((@x475 (trans (monotonicity @x198 @x466 (= $x159 (=> $x196 $x464))) (rewrite (= (=> $x196 $x464) $x471)) (= $x159 $x471))))
blanchet@57170
   479
(let ((@x168 (monotonicity (rewrite (= (and $x34 $x34) $x34)) (= (and $x32 (and $x34 $x34)) $x166))))
blanchet@57170
   480
(let ((@x174 (monotonicity (monotonicity @x168 (= (and $x32 (and $x32 (and $x34 $x34))) $x169)) (= $x38 $x172))))
blanchet@57170
   481
(let ((@x181 (trans (monotonicity @x174 (= $x39 (and true $x172))) (rewrite (= (and true $x172) $x172)) (= $x39 $x172))))
blanchet@57170
   482
(let ((@x187 (monotonicity (monotonicity @x181 (= (and $x28 $x39) $x182)) (= $x41 (and true $x182)))))
blanchet@57170
   483
(let ((@x481 (monotonicity (trans @x187 (rewrite (= (and true $x182) $x182)) (= $x41 $x182)) (monotonicity @x198 @x475 (= (and $x49 $x159) $x476)) (= $x161 (=> $x182 $x476)))))
blanchet@57170
   484
(let ((@x490 (monotonicity (trans @x481 (rewrite (= (=> $x182 $x476) $x483)) (= $x161 $x483)) (= $x162 (not $x483)))))
blanchet@57170
   485
(let ((@x823 (trans @x490 (monotonicity @x818 (= (not $x483) $x819)) (= $x162 $x819))))
blanchet@57170
   486
(let ((@x827 (and-elim (not-or-elim (mp (asserted $x162) @x823 $x819) $x511) $x31)))
blanchet@57170
   487
(let ((@x1690 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= v_b_max_G_0$ (v_b_array$ ?v0!0))) $x839)) (unit-resolution (def-axiom (or $x1149 (not $x839))) @x1726 (not $x839)) (trans @x827 @x1715 (= v_b_max_G_0$ (v_b_array$ ?v0!0))) false)))
blanchet@57170
   488
(let (($x1946 (or $x1154 $x1943)))
blanchet@57170
   489
(let (($x1340 (forall ((?v0 Int) )(let (($x746 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_3$)) 0)))
blanchet@57170
   490
(let (($x733 (>= (+ ?v0 (* (- 1) v_b_p_G_1$)) 0)))
blanchet@57170
   491
(let (($x521 (>= ?v0 0)))
blanchet@57170
   492
(let (($x1157 (not $x521)))
blanchet@57170
   493
(or $x1157 $x733 $x746))))))
blanchet@57170
   494
))
blanchet@57170
   495
(let (($x1348 (not (or (not $x1340) $x136))))
blanchet@57170
   496
(let (($x1353 (or $x1318 $x1348)))
blanchet@57170
   497
(let (($x1365 (not $x1353)))
blanchet@57170
   498
(let (($x1378 (not (or $x692 $x1286 $x1375 $x1376 $x1287 $x1362 $x1363 $x1364 $x1365))))
blanchet@57170
   499
(let (($x1367 (not (or $x1286 $x689 $x1359 $x1360 $x1361 $x1287 $x1362 $x1363 $x1364 $x1365))))
blanchet@57170
   500
(let (($x1383 (or $x1367 $x1378)))
blanchet@57170
   501
(let (($x1391 (not (or $x600 $x1286 $x1287 (not $x1383)))))
blanchet@57170
   502
(let (($x1224 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
blanchet@57170
   503
(let (($x86 (= ?x46 v_b_max_G_4$)))
blanchet@57170
   504
(let (($x622 (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))
blanchet@57170
   505
(let (($x521 (>= ?v0 0)))
blanchet@57170
   506
(let (($x1157 (not $x521)))
blanchet@57170
   507
(let (($x1216 (or $x1157 $x622 $x86)))
blanchet@57170
   508
(not $x1216))))))))
blanchet@57170
   509
))
blanchet@57170
   510
(let (($x1280 (or $x1224 $x1275)))
blanchet@57170
   511
(let (($x1293 (not (or $x661 $x1286 $x1287 $x1288 $x1289 $x1290 (not $x1280)))))
blanchet@57170
   512
(let (($x1396 (or $x1293 $x1391)))
blanchet@57170
   513
(let (($x1199 (forall ((?v0 Int) )(let (($x561 (<= (+ (v_b_array$ ?v0) (* (- 1) v_b_max_G_1$)) 0)))
blanchet@57170
   514
(let (($x548 (>= (+ ?v0 (* (- 1) v_b_p_G_0$)) 0)))
blanchet@57170
   515
(let (($x521 (>= ?v0 0)))
blanchet@57170
   516
(let (($x1157 (not $x521)))
blanchet@57170
   517
(or $x1157 $x548 $x561))))))
blanchet@57170
   518
))
blanchet@57170
   519
(let (($x1406 (not (or $x851 (not $x1199) $x1403 $x1286 $x1287 (not $x1396)))))
blanchet@57170
   520
(let (($x1411 (or $x851 $x1406)))
blanchet@57170
   521
(let (($x1177 (forall ((?v0 Int) )(let (($x534 (>= (+ v_b_max_G_0$ (* (- 1) (v_b_array$ ?v0))) 0)))
blanchet@57170
   522
(let (($x524 (>= ?v0 1)))
blanchet@57170
   523
(let (($x521 (>= ?v0 0)))
blanchet@57170
   524
(let (($x1157 (not $x521)))
blanchet@57170
   525
(or $x1157 $x524 $x534))))))
blanchet@57170
   526
))
blanchet@57170
   527
(let (($x1420 (not (or (not $x1177) (not $x1411)))))
blanchet@57170
   528
(let (($x1425 (or $x1154 $x1420)))
blanchet@57170
   529
(let (($x733 (>= (+ ?0 ?x685) 0)))
blanchet@57170
   530
(let (($x1157 (not $x521)))
blanchet@57170
   531
(let (($x1335 (or $x1157 $x733 $x746)))
blanchet@57170
   532
(let ((@x1885 (monotonicity (quant-intro (refl (= $x1335 $x1335)) (= $x1340 $x1878)) (= (not $x1340) $x1883))))
blanchet@57170
   533
(let ((@x1891 (monotonicity (monotonicity @x1885 (= (or (not $x1340) $x136) $x1886)) (= $x1348 $x1889))))
blanchet@57170
   534
(let ((@x1906 (monotonicity (monotonicity (monotonicity @x1891 (= $x1353 $x1892)) (= $x1365 $x1895)) (= (or $x692 $x1286 $x1375 $x1376 $x1287 $x1362 $x1363 $x1364 $x1365) $x1904))))
blanchet@57170
   535
(let ((@x1900 (monotonicity (monotonicity (monotonicity @x1891 (= $x1353 $x1892)) (= $x1365 $x1895)) (= (or $x1286 $x689 $x1359 $x1360 $x1361 $x1287 $x1362 $x1363 $x1364 $x1365) $x1898))))
blanchet@57170
   536
(let ((@x1912 (monotonicity (monotonicity @x1900 (= $x1367 $x1901)) (monotonicity @x1906 (= $x1378 $x1907)) (= $x1383 $x1910))))
blanchet@57170
   537
(let ((@x1918 (monotonicity (monotonicity @x1912 (= (not $x1383) $x1913)) (= (or $x600 $x1286 $x1287 (not $x1383)) $x1916))))
blanchet@57170
   538
(let (($x622 (<= (+ v_b_length$ (* (- 1) ?0)) 0)))
blanchet@57170
   539
(let (($x1216 (or $x1157 $x622 $x86)))
blanchet@57170
   540
(let (($x1221 (not $x1216)))
blanchet@57170
   541
(let ((@x1868 (monotonicity (quant-intro (refl (= $x1221 $x1221)) (= $x1224 $x1861)) (= $x1280 $x1866))))
blanchet@57170
   542
(let ((@x1874 (monotonicity (monotonicity @x1868 (= (not $x1280) $x1869)) (= (or $x661 $x1286 $x1287 $x1288 $x1289 $x1290 (not $x1280)) $x1872))))
blanchet@57170
   543
(let ((@x1924 (monotonicity (monotonicity @x1874 (= $x1293 $x1875)) (monotonicity @x1918 (= $x1391 $x1919)) (= $x1396 $x1922))))
blanchet@57170
   544
(let (($x548 (>= (+ ?0 ?x549) 0)))
blanchet@57170
   545
(let (($x1194 (or $x1157 $x548 $x561)))
blanchet@57170
   546
(let ((@x1860 (monotonicity (quant-intro (refl (= $x1194 $x1194)) (= $x1199 $x1853)) (= (not $x1199) $x1858))))
blanchet@57170
   547
(let ((@x1930 (monotonicity @x1860 (monotonicity @x1924 (= (not $x1396) $x1925)) (= (or $x851 (not $x1199) $x1403 $x1286 $x1287 (not $x1396)) $x1928))))
blanchet@57170
   548
(let ((@x1939 (monotonicity (monotonicity (monotonicity @x1930 (= $x1406 $x1931)) (= $x1411 $x1934)) (= (not $x1411) $x1937))))
blanchet@57170
   549
(let ((@x1847 (refl (= (or $x1157 (>= ?0 1) $x534) (or $x1157 (>= ?0 1) $x534)))))
blanchet@57170
   550
(let ((@x1852 (monotonicity (quant-intro @x1847 (= $x1177 $x1845)) (= (not $x1177) $x1850))))
blanchet@57170
   551
(let ((@x1945 (monotonicity (monotonicity @x1852 @x1939 (= (or (not $x1177) (not $x1411)) $x1940)) (= $x1420 $x1943))))
blanchet@57170
   552
(let (($x951 (not $x136)))
blanchet@57170
   553
(let (($x954 (and $x752 $x951)))
blanchet@57170
   554
(let (($x1053 (not $x1048)))
blanchet@57170
   555
(let (($x1056 (and $x931 $x1053)))
blanchet@57170
   556
(let (($x1059 (not $x1056)))
blanchet@57170
   557
(let (($x1075 (or $x1059 $x1070)))
blanchet@57170
   558
(let (($x1078 (not $x1075)))
blanchet@57170
   559
(let (($x1081 (or $x1078 $x954)))
blanchet@57170
   560
(let (($x1097 (and $x689 $x571 $x144 $x145 $x573 $x684 $x679 $x682 $x1081)))
blanchet@57170
   561
(let (($x1087 (and $x571 $x692 $x104 $x107 $x109 $x573 $x684 $x679 $x682 $x1081)))
blanchet@57170
   562
(let (($x1102 (or $x1087 $x1097)))
blanchet@57170
   563
(let (($x1108 (and $x661 $x571 $x573 $x1102)))
blanchet@57170
   564
(let (($x903 (not (and $x897 (not $x900)))))
blanchet@57170
   565
(let (($x1016 (or $x903 $x1011)))
blanchet@57170
   566
(let (($x1019 (not $x1016)))
blanchet@57170
   567
(let (($x887 (not (and $x881 (not $x884)))))
blanchet@57170
   568
(let (($x890 (or $x887 $x889)))
blanchet@57170
   569
(let (($x1022 (and $x890 $x1019)))
blanchet@57170
   570
(let (($x877 (forall ((?v0 Int) )(let ((?x46 (v_b_array$ ?v0)))
blanchet@57170
   571
(let (($x86 (= ?x46 v_b_max_G_4$)))
blanchet@57170
   572
(let (($x521 (>= ?v0 0)))
blanchet@57170
   573
(let (($x626 (and $x521 (not (<= (+ v_b_length$ (* (- 1) ?v0)) 0)))))
blanchet@57170
   574
(let (($x629 (not $x626)))
blanchet@57170
   575
(let (($x632 (or $x629 $x86)))
blanchet@57170
   576
(not $x632))))))))
blanchet@57170
   577
))
blanchet@57170
   578
(let (($x1025 (or $x877 $x1022)))
blanchet@57170
   579
(let (($x1031 (and $x600 $x571 $x573 $x71 $x73 $x75 $x1025)))
blanchet@57170
   580
(let (($x1113 (or $x1031 $x1108)))
blanchet@57170
   581
(let (($x1119 (and $x50 $x567 $x63 $x571 $x573 $x1113)))
blanchet@57170
   582
(let (($x1124 (or $x851 $x1119)))
blanchet@57170
   583
(let (($x1127 (and $x541 $x1124)))
blanchet@57170
   584
(let (($x831 (not (and $x835 $x833))))
blanchet@57170
   585
(let (($x840 (or $x831 $x839)))
blanchet@57170
   586
(let (($x841 (not $x840)))
blanchet@57170
   587
(let (($x1130 (or $x841 $x1127)))
blanchet@57170
   588
(let ((@x1380 (rewrite (= (and $x689 $x571 $x144 $x145 $x573 $x684 $x679 $x682 $x1353) $x1378))))
blanchet@57170
   589
(let ((@x1327 (monotonicity (rewrite (= $x738 (not (or $x1157 $x733)))) (= $x741 (not (not (or $x1157 $x733)))))))
blanchet@57170
   590
(let ((@x1331 (trans @x1327 (rewrite (= (not (not (or $x1157 $x733))) (or $x1157 $x733))) (= $x741 (or $x1157 $x733)))))
blanchet@57170
   591
(let ((@x1339 (trans (monotonicity @x1331 (= $x749 (or (or $x1157 $x733) $x746))) (rewrite (= (or (or $x1157 $x733) $x746) $x1335)) (= $x749 $x1335))))
blanchet@57170
   592
(let ((@x1345 (monotonicity (quant-intro @x1339 (= $x752 $x1340)) (= $x954 (and $x1340 $x951)))))
blanchet@57170
   593
(let ((@x1305 (monotonicity (rewrite (= $x1056 (not (or $x1298 $x1048)))) (= $x1059 (not (not (or $x1298 $x1048)))))))
blanchet@57170
   594
(let ((@x1309 (trans @x1305 (rewrite (= (not (not (or $x1298 $x1048))) (or $x1298 $x1048))) (= $x1059 (or $x1298 $x1048)))))
blanchet@57170
   595
(let ((@x1317 (trans (monotonicity @x1309 (= $x1075 (or (or $x1298 $x1048) $x1070))) (rewrite (= (or (or $x1298 $x1048) $x1070) $x1313)) (= $x1075 $x1313))))
blanchet@57170
   596
(let ((@x1355 (monotonicity (monotonicity @x1317 (= $x1078 $x1318)) (trans @x1345 (rewrite (= (and $x1340 $x951) $x1348)) (= $x954 $x1348)) (= $x1081 $x1353))))
blanchet@57170
   597
(let ((@x1374 (monotonicity @x1355 (= $x1097 (and $x689 $x571 $x144 $x145 $x573 $x684 $x679 $x682 $x1353)))))
blanchet@57170
   598
(let ((@x1369 (rewrite (= (and $x571 $x692 $x104 $x107 $x109 $x573 $x684 $x679 $x682 $x1353) $x1367))))
blanchet@57170
   599
(let ((@x1358 (monotonicity @x1355 (= $x1087 (and $x571 $x692 $x104 $x107 $x109 $x573 $x684 $x679 $x682 $x1353)))))
blanchet@57170
   600
(let ((@x1385 (monotonicity (trans @x1358 @x1369 (= $x1087 $x1367)) (trans @x1374 @x1380 (= $x1097 $x1378)) (= $x1102 $x1383))))
blanchet@57170
   601
(let ((@x1395 (trans (monotonicity @x1385 (= $x1108 (and $x661 $x571 $x573 $x1383))) (rewrite (= (and $x661 $x571 $x573 $x1383) $x1391)) (= $x1108 $x1391))))
blanchet@57170
   602
(let ((@x1254 (monotonicity (rewrite (= (and $x897 (not $x900)) (not (or $x1247 $x900)))) (= $x903 (not (not (or $x1247 $x900)))))))
blanchet@57170
   603
(let ((@x1258 (trans @x1254 (rewrite (= (not (not (or $x1247 $x900))) (or $x1247 $x900))) (= $x903 (or $x1247 $x900)))))
blanchet@57170
   604
(let ((@x1266 (trans (monotonicity @x1258 (= $x1016 (or (or $x1247 $x900) $x1011))) (rewrite (= (or (or $x1247 $x900) $x1011) (or $x1247 $x900 $x1011))) (= $x1016 (or $x1247 $x900 $x1011)))))
blanchet@57170
   605
(let ((@x1234 (monotonicity (rewrite (= (and $x881 (not $x884)) (not (or $x1227 $x884)))) (= $x887 (not (not (or $x1227 $x884)))))))
blanchet@57170
   606
(let ((@x1238 (trans @x1234 (rewrite (= (not (not (or $x1227 $x884))) (or $x1227 $x884))) (= $x887 (or $x1227 $x884)))))
blanchet@57170
   607
(let ((@x1246 (trans (monotonicity @x1238 (= $x890 (or (or $x1227 $x884) $x889))) (rewrite (= (or (or $x1227 $x884) $x889) $x1242)) (= $x890 $x1242))))
blanchet@57170
   608
(let ((@x1272 (monotonicity @x1246 (monotonicity @x1266 (= $x1019 (not (or $x1247 $x900 $x1011)))) (= $x1022 (and $x1242 (not (or $x1247 $x900 $x1011)))))))
blanchet@57170
   609
(let ((@x1279 (trans @x1272 (rewrite (= (and $x1242 (not (or $x1247 $x900 $x1011))) $x1275)) (= $x1022 $x1275))))
blanchet@57170
   610
(let ((@x1208 (monotonicity (rewrite (= $x626 (not (or $x1157 $x622)))) (= $x629 (not (not (or $x1157 $x622)))))))
blanchet@57170
   611
(let ((@x1212 (trans @x1208 (rewrite (= (not (not (or $x1157 $x622))) (or $x1157 $x622))) (= $x629 (or $x1157 $x622)))))
blanchet@57170
   612
(let ((@x1220 (trans (monotonicity @x1212 (= $x632 (or (or $x1157 $x622) $x86))) (rewrite (= (or (or $x1157 $x622) $x86) $x1216)) (= $x632 $x1216))))
blanchet@57170
   613
(let ((@x1226 (quant-intro (monotonicity @x1220 (= (not $x632) $x1221)) (= $x877 $x1224))))
blanchet@57170
   614
(let ((@x1285 (monotonicity (monotonicity @x1226 @x1279 (= $x1025 $x1280)) (= $x1031 (and $x600 $x571 $x573 $x71 $x73 $x75 $x1280)))))
blanchet@57170
   615
(let ((@x1297 (trans @x1285 (rewrite (= (and $x600 $x571 $x573 $x71 $x73 $x75 $x1280) $x1293)) (= $x1031 $x1293))))
blanchet@57170
   616
(let ((@x1186 (monotonicity (rewrite (= $x553 (not (or $x1157 $x548)))) (= $x556 (not (not (or $x1157 $x548)))))))
blanchet@57170
   617
(let ((@x1190 (trans @x1186 (rewrite (= (not (not (or $x1157 $x548))) (or $x1157 $x548))) (= $x556 (or $x1157 $x548)))))
blanchet@57170
   618
(let ((@x1198 (trans (monotonicity @x1190 (= $x564 (or (or $x1157 $x548) $x561))) (rewrite (= (or (or $x1157 $x548) $x561) $x1194)) (= $x564 $x1194))))
blanchet@57170
   619
(let ((@x1401 (monotonicity (quant-intro @x1198 (= $x567 $x1199)) (monotonicity @x1297 @x1395 (= $x1113 $x1396)) (= $x1119 (and $x50 $x1199 $x63 $x571 $x573 $x1396)))))
blanchet@57170
   620
(let ((@x1410 (trans @x1401 (rewrite (= (and $x50 $x1199 $x63 $x571 $x573 $x1396) $x1406)) (= $x1119 $x1406))))
blanchet@57170
   621
(let (($x524 (>= ?0 1)))
blanchet@57170
   622
(let (($x1172 (or $x1157 $x524 $x534)))
blanchet@57170
   623
(let ((@x1164 (monotonicity (rewrite (= $x526 (not (or $x1157 $x524)))) (= $x529 (not (not (or $x1157 $x524)))))))
blanchet@57170
   624
(let ((@x1168 (trans @x1164 (rewrite (= (not (not (or $x1157 $x524))) (or $x1157 $x524))) (= $x529 (or $x1157 $x524)))))
blanchet@57170
   625
(let ((@x1176 (trans (monotonicity @x1168 (= $x538 (or (or $x1157 $x524) $x534))) (rewrite (= (or (or $x1157 $x524) $x534) $x1172)) (= $x538 $x1172))))
blanchet@57170
   626
(let ((@x1416 (monotonicity (quant-intro @x1176 (= $x541 $x1177)) (monotonicity @x1410 (= $x1124 $x1411)) (= $x1127 (and $x1177 $x1411)))))
blanchet@57170
   627
(let ((@x1141 (monotonicity (rewrite (= (and $x835 $x833) (not (or $x1134 $x832)))) (= $x831 (not (not (or $x1134 $x832)))))))
blanchet@57170
   628
(let ((@x1145 (trans @x1141 (rewrite (= (not (not (or $x1134 $x832))) (or $x1134 $x832))) (= $x831 (or $x1134 $x832)))))
blanchet@57170
   629
(let ((@x1153 (trans (monotonicity @x1145 (= $x840 (or (or $x1134 $x832) $x839))) (rewrite (= (or (or $x1134 $x832) $x839) $x1149)) (= $x840 $x1149))))
blanchet@57170
   630
(let ((@x1427 (monotonicity (monotonicity @x1153 (= $x841 $x1154)) (trans @x1416 (rewrite (= (and $x1177 $x1411) $x1420)) (= $x1127 $x1420)) (= $x1130 $x1425))))
blanchet@57170
   631
(let (($x939 (<= (+ ?x937 ?x744) 0)))
blanchet@57170
   632
(let (($x941 (not (or (not (and $x931 (not (>= (+ ?v0!3 ?x685) 0)))) $x939))))
blanchet@57170
   633
(let (($x958 (or $x941 $x954)))
blanchet@57170
   634
(let (($x966 (not $x789)))
blanchet@57170
   635
(let (($x969 (and $x966 $x958)))
blanchet@57170
   636
(let (($x927 (not $x730)))
blanchet@57170
   637
(let (($x962 (and $x927 $x958)))
blanchet@57170
   638
(let (($x973 (or $x962 $x969)))
blanchet@57170
   639
(let (($x924 (not $x675)))
blanchet@57170
   640
(let (($x977 (and $x924 $x973)))
blanchet@57170
   641
(let (($x908 (not (or $x903 (<= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_4$)) 0)))))
blanchet@57170
   642
(let (($x912 (and $x890 $x908)))
blanchet@57170
   643
(let (($x916 (or $x877 $x912)))
blanchet@57170
   644
(let (($x871 (not $x617)))
blanchet@57170
   645
(let (($x920 (and $x871 $x916)))
blanchet@57170
   646
(let (($x981 (or $x920 $x977)))
blanchet@57170
   647
(let (($x985 (and $x591 $x981)))
blanchet@57170
   648
(let (($x989 (or $x851 $x985)))
blanchet@57170
   649
(let (($x993 (and $x541 $x989)))
blanchet@57170
   650
(let (($x997 (or $x841 $x993)))
blanchet@57170
   651
(let (($x1076 (= (or (not (and $x931 (not (>= (+ ?v0!3 ?x685) 0)))) $x939) $x1075)))
blanchet@57170
   652
(let ((@x1067 (monotonicity (rewrite (= (+ ?x937 ?x744) (+ ?x744 ?x937))) (= $x939 (<= (+ ?x744 ?x937) 0)))))
blanchet@57170
   653
(let ((@x1074 (trans @x1067 (rewrite (= (<= (+ ?x744 ?x937) 0) $x1070)) (= $x939 $x1070))))
blanchet@57170
   654
(let ((@x1045 (monotonicity (rewrite (= (+ ?v0!3 ?x685) (+ ?x685 ?v0!3))) (= (>= (+ ?v0!3 ?x685) 0) (>= (+ ?x685 ?v0!3) 0)))))
blanchet@57170
   655
(let ((@x1052 (trans @x1045 (rewrite (= (>= (+ ?x685 ?v0!3) 0) $x1048)) (= (>= (+ ?v0!3 ?x685) 0) $x1048))))
blanchet@57170
   656
(let ((@x1058 (monotonicity (monotonicity @x1052 (= (not (>= (+ ?v0!3 ?x685) 0)) $x1053)) (= (and $x931 (not (>= (+ ?v0!3 ?x685) 0))) $x1056))))
blanchet@57170
   657
(let ((@x1061 (monotonicity @x1058 (= (not (and $x931 (not (>= (+ ?v0!3 ?x685) 0)))) $x1059))))
blanchet@57170
   658
(let ((@x1083 (monotonicity (monotonicity (monotonicity @x1061 @x1074 $x1076) (= $x941 $x1078)) (= $x958 $x1081))))
blanchet@57170
   659
(let ((@x1096 (monotonicity (rewrite (= $x966 $x784)) @x1083 (= $x969 (and $x784 $x1081)))))
blanchet@57170
   660
(let ((@x1086 (monotonicity (rewrite (= $x927 $x725)) @x1083 (= $x962 (and $x725 $x1081)))))
blanchet@57170
   661
(let ((@x1104 (monotonicity (trans @x1086 (rewrite (= (and $x725 $x1081) $x1087)) (= $x962 $x1087)) (trans @x1096 (rewrite (= (and $x784 $x1081) $x1097)) (= $x969 $x1097)) (= $x973 $x1102))))
blanchet@57170
   662
(let ((@x1107 (monotonicity (rewrite (= $x924 $x670)) @x1104 (= $x977 (and $x670 $x1102)))))
blanchet@57170
   663
(let (($x1017 (= (or $x903 (<= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_4$)) 0)) $x1016)))
blanchet@57170
   664
(let (($x906 (<= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_4$)) 0)))
blanchet@57170
   665
(let (($x1012 (= (<= (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!2)) 0) $x1011)))
blanchet@57170
   666
(let (($x1007 (= $x906 (<= (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!2)) 0))))
blanchet@57170
   667
(let (($x1004 (= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_4$)) (+ (* (- 1) v_b_max_G_4$) (v_b_array$ ?v0!2)))))
blanchet@57170
   668
(let ((@x1015 (trans (monotonicity (rewrite $x1004) $x1007) (rewrite $x1012) (= $x906 $x1011))))
blanchet@57170
   669
(let ((@x1024 (monotonicity (monotonicity (monotonicity @x1015 $x1017) (= $x908 $x1019)) (= $x912 $x1022))))
blanchet@57170
   670
(let ((@x1030 (monotonicity (rewrite (= $x871 $x612)) (monotonicity @x1024 (= $x916 $x1025)) (= $x920 (and $x612 $x1025)))))
blanchet@57170
   671
(let ((@x1115 (monotonicity (trans @x1030 (rewrite (= (and $x612 $x1025) $x1031)) (= $x920 $x1031)) (trans @x1107 (rewrite (= (and $x670 $x1102) $x1108)) (= $x977 $x1108)) (= $x981 $x1113))))
blanchet@57170
   672
(let ((@x1123 (trans (monotonicity @x1115 (= $x985 (and $x591 $x1113))) (rewrite (= (and $x591 $x1113) $x1119)) (= $x985 $x1119))))
blanchet@57170
   673
(let ((@x1132 (monotonicity (monotonicity (monotonicity @x1123 (= $x989 $x1124)) (= $x993 $x1127)) (= $x997 $x1130))))
blanchet@57170
   674
(let ((@x950 (nnf-neg (nnf-pos (refl (~ $x749 $x749)) (~ $x752 $x752)) (~ (not $x755) $x752))))
blanchet@57170
   675
(let ((@x961 (nnf-neg (sk (~ $x755 $x941)) (nnf-neg @x950 (refl (~ $x951 $x951)) (~ (not $x758) $x954)) (~ (not $x761) $x958))))
blanchet@57170
   676
(let ((@x976 (nnf-neg (nnf-neg (refl (~ $x927 $x927)) @x961 (~ (not $x764) $x962)) (nnf-neg (refl (~ $x966 $x966)) @x961 (~ (not $x792) $x969)) (~ (not $x795) $x973))))
blanchet@57170
   677
(let ((@x915 (nnf-neg (nnf-neg (sk (~ $x635 $x890)) (~ (not $x638) $x890)) (sk (~ (not $x649) $x908)) (~ (not $x652) $x912))))
blanchet@57170
   678
(let ((@x919 (nnf-neg (nnf-neg (refl (~ (not $x632) (not $x632))) (~ $x638 $x877)) @x915 (~ (not $x655) $x916))))
blanchet@57170
   679
(let ((@x984 (nnf-neg (nnf-neg (refl (~ $x871 $x871)) @x919 (~ (not $x658) $x920)) (nnf-neg (refl (~ $x924 $x924)) @x976 (~ (not $x798) $x977)) (~ (not $x801) $x981))))
blanchet@57170
   680
(let ((@x867 (monotonicity (refl (~ $x50 $x50)) (nnf-pos (refl (~ $x564 $x564)) (~ $x567 $x567)) (refl (~ $x63 $x63)) (refl (~ $x571 $x571)) (refl (~ $x573 $x573)) (~ $x591 $x591))))
blanchet@57170
   681
(let ((@x988 (nnf-neg (nnf-neg @x867 (~ (not $x596) $x591)) @x984 (~ (not $x804) $x985))))
blanchet@57170
   682
(let ((@x850 (nnf-neg (nnf-pos (refl (~ $x538 $x538)) (~ $x541 $x541)) (~ (not $x544) $x541))))
blanchet@57170
   683
(let ((@x996 (nnf-neg @x850 (nnf-neg (refl (~ $x851 $x851)) @x988 (~ (not $x807) $x989)) (~ (not $x810) $x993))))
blanchet@57170
   684
(let ((@x1000 (mp~ (not-or-elim (mp (asserted $x162) @x823 $x819) (not $x813)) (nnf-neg (sk (~ $x544 $x841)) @x996 (~ (not $x813) $x997)) $x997)))
blanchet@57170
   685
(let ((@x1949 (mp (mp (mp @x1000 @x1132 $x1130) @x1427 $x1425) (monotonicity @x1945 (= $x1425 $x1946)) $x1946)))
blanchet@57170
   686
(let ((@x2062 (unit-resolution (def-axiom (or $x1940 $x1934)) (unit-resolution @x1949 (lemma @x1690 $x1149) $x1943) $x1934)))
blanchet@57170
   687
(let ((@x2069 (unit-resolution (def-axiom (or $x1937 $x851 $x1931)) (mp @x827 (symm (commutativity (= $x50 $x31)) (= $x31 $x50)) $x50) (or $x1937 $x1931))))
blanchet@57170
   688
(let ((@x2070 (unit-resolution @x2069 @x2062 $x1931)))
blanchet@57170
   689
(let ((@x2170 (monotonicity (unit-resolution (def-axiom (or $x1904 $x144)) @x2149 $x144) (= ?x135 ?x62))))
blanchet@57170
   690
(let ((@x2173 (trans @x2170 (unit-resolution (def-axiom (or $x1928 $x63)) @x2070 $x63) (= ?x135 v_b_max_G_1$))))
blanchet@57170
   691
(let ((@x2174 (trans @x2173 (symm (unit-resolution (def-axiom (or $x1904 $x145)) @x2149 $x145) $x1780) $x136)))
blanchet@57170
   692
(let ((@x1523 (def-axiom (or $x1886 $x951))))
blanchet@57170
   693
(let ((@x1808 (def-axiom (or $x1895 $x1318 $x1889))))
blanchet@57170
   694
(let ((@x2176 (unit-resolution @x1808 (unit-resolution @x1523 @x2174 $x1886) (unit-resolution (def-axiom (or $x1904 $x1892)) @x2149 $x1892) $x1318)))
blanchet@57170
   695
(let ((@x1812 (def-axiom (or $x1313 $x1436))))
blanchet@57170
   696
(let ((@x2181 (unit-resolution ((_ th-lemma arith assign-bounds 1 -1 -1) (or $x1453 $x692 $x1070 (not $x1782))) (unit-resolution @x1812 @x2176 $x1436) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x1780) $x1782)) @x2162 $x1782) (unit-resolution (def-axiom (or $x1904 $x689)) @x2149 $x689) $x1453)))
blanchet@57170
   697
(let ((@x1565 ((_ th-lemma arith triangle-eq) (or $x1563 $x1445))))
blanchet@57170
   698
(let (($x1558 (= v_b_p_G_0$ ?v0!3)))
blanchet@57170
   699
(let ((?x1046 (* (- 1) ?v0!3)))
blanchet@57170
   700
(let ((?x1510 (+ v_b_p_G_0$ ?x1046)))
blanchet@57170
   701
(let (($x1560 (>= ?x1510 0)))
blanchet@57170
   702
(let (($x1522 (>= ?x686 (- 1))))
blanchet@57170
   703
(let ((@x2186 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1362 $x1522)) (unit-resolution (def-axiom (or $x1904 $x684)) @x2149 $x684) $x1522)))
blanchet@57170
   704
(let ((@x2190 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x1560 $x1048 (not $x1522))) (unit-resolution (def-axiom (or $x1313 $x1053)) @x2176 $x1053) @x2186 $x1560)))
blanchet@57170
   705
(let (($x1511 (<= ?x1510 0)))
blanchet@57170
   706
(let (($x1488 (>= (+ v_b_max_G_1$ ?x1068) 0)))
blanchet@57170
   707
(let (($x1955 (not $x1488)))
blanchet@57170
   708
(let ((@x2193 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x1955 $x1070 (not $x1782))) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x1780) $x1782)) @x2162 $x1782) (unit-resolution @x1812 @x2176 $x1436) $x1955)))
blanchet@57170
   709
(let ((@x2093 (unit-resolution (def-axiom (or $x1928 $x1853)) @x2070 $x1853)))
blanchet@57170
   710
(let (($x1476 (or $x1858 $x1298 $x1511 $x1488)))
blanchet@57170
   711
(let (($x1535 (<= (+ ?x937 (* (- 1) v_b_max_G_1$)) 0)))
blanchet@57170
   712
(let (($x1549 (>= (+ ?v0!3 ?x549) 0)))
blanchet@57170
   713
(let (($x1501 (or $x1298 $x1549 $x1535)))
blanchet@57170
   714
(let (($x1464 (or $x1858 $x1501)))
blanchet@57170
   715
(let (($x1478 (= (+ ?x937 (* (- 1) v_b_max_G_1$)) (+ (* (- 1) v_b_max_G_1$) ?x937))))
blanchet@57170
   716
(let ((@x1486 (monotonicity (rewrite $x1478) (= $x1535 (<= (+ (* (- 1) v_b_max_G_1$) ?x937) 0)))))
blanchet@57170
   717
(let ((@x1472 (trans @x1486 (rewrite (= (<= (+ (* (- 1) v_b_max_G_1$) ?x937) 0) $x1488)) (= $x1535 $x1488))))
blanchet@57170
   718
(let ((@x1509 (monotonicity (rewrite (= (+ ?v0!3 ?x549) (+ ?x549 ?v0!3))) (= $x1549 (>= (+ ?x549 ?v0!3) 0)))))
blanchet@57170
   719
(let ((@x1497 (trans @x1509 (rewrite (= (>= (+ ?x549 ?v0!3) 0) $x1511)) (= $x1549 $x1511))))
blanchet@57170
   720
(let ((@x1470 (monotonicity (monotonicity @x1497 @x1472 (= $x1501 (or $x1298 $x1511 $x1488))) (= $x1464 (or $x1858 (or $x1298 $x1511 $x1488))))))
blanchet@57170
   721
(let ((@x1450 (trans @x1470 (rewrite (= (or $x1858 (or $x1298 $x1511 $x1488)) $x1476)) (= $x1464 $x1476))))
blanchet@57170
   722
(let ((@x2195 (unit-resolution (mp ((_ quant-inst ?v0!3) $x1464) @x1450 $x1476) @x2093 (unit-resolution (def-axiom (or $x1313 $x931)) @x2176 $x931) @x2193 $x1511)))
blanchet@57170
   723
(let ((@x2196 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1558 (not $x1511) (not $x1560))) @x2195 @x2190 $x1558)))
blanchet@57170
   724
(let ((@x1551 (monotonicity (symm (hypothesis $x1558) (= ?v0!3 v_b_p_G_0$)) (= ?x937 ?x101))))
blanchet@57170
   725
(let ((@x1540 (lemma (unit-resolution (hypothesis $x1563) (symm @x1551 $x1559) false) (or (not $x1558) $x1559))))
blanchet@57170
   726
(let ((@x2198 (lemma (unit-resolution @x1540 @x2196 (unit-resolution @x1565 @x2181 $x1563) false) $x1904)))
blanchet@57170
   727
(let (($x1990 (<= (+ v_b_max_G_1$ (* (- 1) v_b_max_G_4$)) 0)))
blanchet@57170
   728
(let (($x1988 (= v_b_max_G_1$ v_b_max_G_4$)))
blanchet@57170
   729
(let ((@x2109 (symm (unit-resolution (def-axiom (or $x1872 $x73)) (hypothesis $x1875) $x73) $x1988)))
blanchet@57170
   730
(let (($x2025 (>= (+ v_b_max_G_1$ (* (- 1) (v_b_array$ ?v0!2))) 0)))
blanchet@57170
   731
(let (($x901 (not $x900)))
blanchet@57170
   732
(let (($x1835 (not $x1861)))
blanchet@57170
   733
(let (($x2042 (= ?x62 v_b_max_G_4$)))
blanchet@57170
   734
(let (($x2043 (or $x1286 (<= (+ v_b_length$ (* (- 1) v_b_k_G_0$)) 0) $x2042)))
blanchet@57170
   735
(let ((@x2073 (trans (unit-resolution (def-axiom (or $x1928 $x63)) @x2070 $x63) (symm (hypothesis $x73) $x1988) $x2042)))
blanchet@57170
   736
(let ((@x2076 (unit-resolution ((_ quant-inst v_b_k_G_0$) (or $x1835 (not $x2043))) (hypothesis $x1861) (unit-resolution (def-axiom (or $x2043 (not $x2042))) @x2073 $x2043) false)))
blanchet@57170
   737
(let ((@x2115 (unit-resolution (lemma @x2076 (or $x1835 $x1289)) (unit-resolution (def-axiom (or $x1872 $x73)) (hypothesis $x1875) $x73) $x1835)))
blanchet@57170
   738
(let ((@x2116 (unit-resolution (def-axiom (or $x1869 $x1861 $x1275)) @x2115 (unit-resolution (def-axiom (or $x1872 $x1866)) (hypothesis $x1875) $x1866) $x1275)))
blanchet@57170
   739
(let ((@x2103 ((_ th-lemma arith farkas -1 -1 1) (hypothesis (<= (+ v_b_p_G_0$ (* (- 1) ?v0!2)) 0)) (hypothesis $x600) (hypothesis $x901) false)))
blanchet@57170
   740
(let ((@x2106 (lemma @x2103 (or (not (<= (+ v_b_p_G_0$ (* (- 1) ?v0!2)) 0)) $x661 $x900))))
blanchet@57170
   741
(let ((@x2119 (unit-resolution @x2106 (unit-resolution (def-axiom (or $x1872 $x600)) (hypothesis $x1875) $x600) (unit-resolution (def-axiom (or $x1274 $x901)) @x2116 $x901) (not (<= (+ v_b_p_G_0$ (* (- 1) ?v0!2)) 0)))))
blanchet@57170
   742
(let (($x2032 (<= (+ v_b_p_G_0$ (* (- 1) ?v0!2)) 0)))
blanchet@57170
   743
(let (($x2056 (or $x1858 $x1247 $x2032 $x2025)))
blanchet@57170
   744
(let (($x2009 (<= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_1$)) 0)))
blanchet@57170
   745
(let (($x2001 (>= (+ ?v0!2 ?x549) 0)))
blanchet@57170
   746
(let (($x2010 (or $x1247 $x2001 $x2009)))
blanchet@57170
   747
(let (($x2060 (or $x1858 $x2010)))
blanchet@57170
   748
(let (($x2026 (= (<= (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!2)) 0) $x2025)))
blanchet@57170
   749
(let (($x2020 (= $x2009 (<= (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!2)) 0))))
blanchet@57170
   750
(let (($x2038 (= (+ (v_b_array$ ?v0!2) (* (- 1) v_b_max_G_1$)) (+ (* (- 1) v_b_max_G_1$) (v_b_array$ ?v0!2)))))
blanchet@57170
   751
(let ((@x2052 (trans (monotonicity (rewrite $x2038) $x2020) (rewrite $x2026) (= $x2009 $x2025))))
blanchet@57170
   752
(let ((@x2018 (monotonicity (rewrite (= (+ ?v0!2 ?x549) (+ ?x549 ?v0!2))) (= $x2001 (>= (+ ?x549 ?v0!2) 0)))))
blanchet@57170
   753
(let ((@x2036 (trans @x2018 (rewrite (= (>= (+ ?x549 ?v0!2) 0) $x2032)) (= $x2001 $x2032))))
blanchet@57170
   754
(let ((@x2031 (monotonicity (monotonicity @x2036 @x2052 (= $x2010 (or $x1247 $x2032 $x2025))) (= $x2060 (or $x1858 (or $x1247 $x2032 $x2025))))))
blanchet@57170
   755
(let ((@x2079 (trans @x2031 (rewrite (= (or $x1858 (or $x1247 $x2032 $x2025)) $x2056)) (= $x2060 $x2056))))
blanchet@57170
   756
(let ((@x2122 (unit-resolution (mp ((_ quant-inst ?v0!2) $x2060) @x2079 $x2056) @x2093 (unit-resolution (def-axiom (or $x1274 $x897)) @x2116 $x897) (or $x2032 $x2025))))
blanchet@57170
   757
(let ((@x2125 ((_ th-lemma arith farkas 1 -1 1) (unit-resolution (def-axiom (or $x1274 (not $x1011))) @x2116 (not $x1011)) (unit-resolution @x2122 @x2119 $x2025) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x1988) $x1990)) @x2109 $x1990) false)))
blanchet@57170
   758
(let ((@x2133 (unit-resolution (def-axiom (or $x1925 $x1875 $x1919)) (lemma @x2125 $x1872) (unit-resolution (def-axiom (or $x1928 $x1922)) @x2070 $x1922) $x1919)))
blanchet@57170
   759
(let ((@x2003 (unit-resolution (def-axiom (or $x1913 $x1901 $x1907)) (unit-resolution (def-axiom (or $x1916 $x1910)) @x2133 $x1910) $x1910)))
blanchet@57170
   760
(let ((@x2004 (unit-resolution @x2003 @x2198 $x1901)))
blanchet@57170
   761
(let ((@x1528 (trans (monotonicity (hypothesis $x107) (= ?x135 ?x101)) (symm (hypothesis $x104) (= ?x101 v_b_max_G_2$)) (= ?x135 v_b_max_G_2$))))
blanchet@57170
   762
(let ((@x1529 (trans @x1528 (symm (hypothesis $x109) (= v_b_max_G_2$ v_b_max_G_3$)) $x136)))
blanchet@57170
   763
(let ((@x1532 (lemma (unit-resolution (hypothesis $x951) @x1529 false) (or $x136 $x1361 $x1359 $x1360))))
blanchet@57170
   764
(let ((@x2140 (unit-resolution @x1532 (unit-resolution (def-axiom (or $x1898 $x109)) @x2004 $x109) (unit-resolution (def-axiom (or $x1898 $x104)) @x2004 $x104) (unit-resolution (def-axiom (or $x1898 $x107)) @x2004 $x107) $x136)))
blanchet@57170
   765
(let ((@x2128 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1362 $x1522)) (unit-resolution (def-axiom (or $x1898 $x684)) @x2004 $x684) $x1522)))
blanchet@57170
   766
(let ((@x1460 (unit-resolution @x1808 (unit-resolution @x1523 (hypothesis $x136) $x1886) (hypothesis $x1892) $x1318)))
blanchet@57170
   767
(let ((@x1539 (def-axiom (or $x1313 $x1053))))
blanchet@57170
   768
(let (($x1965 (not $x1560)))
blanchet@57170
   769
(let (($x1597 (<= (+ ?x101 ?x744) 0)))
blanchet@57170
   770
(let ((@x1431 (trans (symm (hypothesis $x104) (= ?x101 v_b_max_G_2$)) (symm (hypothesis $x109) (= v_b_max_G_2$ v_b_max_G_3$)) (= ?x101 v_b_max_G_3$))))
blanchet@57170
   771
(let ((@x1435 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x101 v_b_max_G_3$)) $x1597)) @x1431 $x1597)))
blanchet@57170
   772
(let ((@x1437 (lemma ((_ th-lemma arith farkas -1 -1 1) (hypothesis $x1436) (hypothesis $x1597) (hypothesis $x1445) false) (or $x1453 $x1070 (not $x1597)))))
blanchet@57170
   773
(let ((@x1952 (unit-resolution @x1565 (unit-resolution @x1437 (unit-resolution @x1812 @x1460 $x1436) @x1435 $x1453) $x1563)))
blanchet@57170
   774
(let ((@x1958 (unit-resolution ((_ th-lemma arith assign-bounds 1 1 1) (or $x1955 $x1070 (not $x1597) $x689)) (unit-resolution @x1812 @x1460 $x1436) @x1435 (hypothesis $x692) $x1955)))
blanchet@57170
   775
(let ((@x1962 (unit-resolution (mp ((_ quant-inst ?v0!3) $x1464) @x1450 $x1476) (hypothesis $x1853) (unit-resolution (def-axiom (or $x1313 $x931)) @x1460 $x931) (or $x1511 $x1488))))
blanchet@57170
   776
(let ((@x1969 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x1558 (not $x1511) $x1965)) (unit-resolution @x1962 @x1958 $x1511) (or $x1558 $x1965))))
blanchet@57170
   777
(let ((@x1971 ((_ th-lemma arith farkas -1 1 1) (unit-resolution @x1969 (unit-resolution @x1540 @x1952 (not $x1558)) $x1965) (hypothesis $x1522) (unit-resolution @x1539 @x1460 $x1053) false)))
blanchet@57170
   778
(let ((@x2130 (unit-resolution (lemma @x1971 (or $x951 (not $x1522) $x1858 $x689 $x1895 $x1359 $x1361)) @x2093 (or $x951 (not $x1522) $x689 $x1895 $x1359 $x1361))))
blanchet@57170
   779
(unit-resolution @x2130 @x2128 @x2140 (unit-resolution (def-axiom (or $x1898 $x692)) @x2004 $x692) (unit-resolution (def-axiom (or $x1898 $x1892)) @x2004 $x1892) (unit-resolution (def-axiom (or $x1898 $x104)) @x2004 $x104) (unit-resolution (def-axiom (or $x1898 $x109)) @x2004 $x109) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
blanchet@57170
   780