src/HOL/SMT_Examples/SMT_Examples.certs
author blanchet
Thu Mar 13 13:18:13 2014 +0100 (2014-03-13)
changeset 56079 175ac95720d4
parent 55421 0aaca907aeab
child 56111 5b76e1790c38
permissions -rw-r--r--
use 'smt2' in SMT examples as much as currently possible
     1 d97439af6f5bc7794ab403d0f6cc318d103016a1 1288 0
     2 #2 := false
     3 decl f1 :: S1
     4 #3 := f1
     5 decl f9 :: S1
     6 #25 := f9
     7 #26 := (= f9 f1)
     8 decl f20 :: S1
     9 #59 := f20
    10 #60 := (= f20 f1)
    11 decl f21 :: S1
    12 #61 := f21
    13 #62 := (= f21 f1)
    14 #249 := (not #62)
    15 decl f31 :: S1
    16 #97 := f31
    17 #98 := (= f31 f1)
    18 decl f62 :: S1
    19 #207 := f62
    20 #208 := (= f62 f1)
    21 decl f58 :: S1
    22 #189 := f58
    23 #190 := (= f58 f1)
    24 #388 := (not #190)
    25 decl f47 :: S1
    26 #151 := f47
    27 #152 := (= f47 f1)
    28 #289 := (not #98)
    29 #980 := [hypothesis]: #289
    30 decl f46 :: S1
    31 #149 := f46
    32 #150 := (= f46 f1)
    33 #346 := (not #150)
    34 decl f48 :: S1
    35 #156 := f48
    36 #157 := (= f48 f1)
    37 decl f57 :: S1
    38 #187 := f57
    39 #188 := (= f57 f1)
    40 #387 := (not #188)
    41 decl f45 :: S1
    42 #144 := f45
    43 #145 := (= f45 f1)
    44 #339 := (not #145)
    45 decl f42 :: S1
    46 #135 := f42
    47 #136 := (= f42 f1)
    48 #1467 := (or #136 #98)
    49 decl f40 :: S1
    50 #128 := f40
    51 #129 := (= f40 f1)
    52 #330 := (not #136)
    53 #1095 := [hypothesis]: #330
    54 decl f32 :: S1
    55 #99 := f32
    56 #100 := (= f32 f1)
    57 #290 := (not #100)
    58 decl f16 :: S1
    59 #46 := f16
    60 #47 := (= f16 f1)
    61 decl f17 :: S1
    62 #48 := f17
    63 #49 := (= f17 f1)
    64 #236 := (not #49)
    65 decl f28 :: S1
    66 #86 := f28
    67 #87 := (= f28 f1)
    68 #1450 := (or #87 #98 #136)
    69 decl f29 :: S1
    70 #90 := f29
    71 #91 := (= f29 f1)
    72 #281 := (not #91)
    73 #322 := (not #129)
    74 #277 := (not #87)
    75 #867 := [hypothesis]: #277
    76 #1427 := (or #322 #87)
    77 decl f51 :: S1
    78 #166 := f51
    79 #167 := (= f51 f1)
    80 #363 := (not #167)
    81 decl f54 :: S1
    82 #175 := f54
    83 #176 := (= f54 f1)
    84 decl f56 :: S1
    85 #182 := f56
    86 #183 := (= f56 f1)
    87 #380 := (not #183)
    88 #372 := (not #176)
    89 #1160 := [hypothesis]: #372
    90 #1189 := (or #388 #176)
    91 decl f18 :: S1
    92 #52 := f18
    93 #53 := (= f18 f1)
    94 decl f33 :: S1
    95 #104 := f33
    96 #105 := (= f33 f1)
    97 #297 := (not #105)
    98 decl f36 :: S1
    99 #113 := f36
   100 #114 := (= f36 f1)
   101 #347 := (not #152)
   102 #1155 := [hypothesis]: #190
   103 #393 := (or #388 #347)
   104 #730 := [asserted]: #393
   105 #1156 := [unit-resolution #730 #1155]: #347
   106 #389 := (or #387 #388)
   107 #726 := [asserted]: #389
   108 #1157 := [unit-resolution #726 #1155]: #387
   109 #194 := (or #188 #157)
   110 decl f6 :: S1
   111 #16 := f6
   112 #17 := (= f6 f1)
   113 #579 := (or #17 #188 #157)
   114 #840 := (iff #579 #194)
   115 #835 := (or false #188 #157)
   116 #838 := (iff #835 #194)
   117 #839 := [rewrite]: #838
   118 #836 := (iff #579 #835)
   119 #759 := (iff #17 false)
   120 #18 := (not #17)
   121 #439 := [asserted]: #18
   122 #760 := [iff-false #439]: #759
   123 #837 := [monotonicity #760]: #836
   124 #841 := [trans #837 #839]: #840
   125 #195 := (or #17 #194)
   126 #580 := (iff #195 #579)
   127 #581 := [rewrite]: #580
   128 #568 := [asserted]: #195
   129 #582 := [mp #568 #581]: #579
   130 #842 := [mp #582 #841]: #194
   131 #1158 := [unit-resolution #842 #1157]: #157
   132 #354 := (not #157)
   133 #355 := (or #354 #346)
   134 #702 := [asserted]: #355
   135 #1159 := [unit-resolution #702 #1158]: #346
   136 decl f44 :: S1
   137 #142 := f44
   138 #143 := (= f44 f1)
   139 #338 := (not #143)
   140 decl f61 :: S1
   141 #203 := f61
   142 #204 := (= f61 f1)
   143 decl f60 :: S1
   144 #199 := f60
   145 #200 := (= f60 f1)
   146 #400 := (not #200)
   147 decl f37 :: S1
   148 #118 := f37
   149 #119 := (= f37 f1)
   150 #313 := (not #119)
   151 #356 := (or #354 #313)
   152 #703 := [asserted]: #356
   153 #1161 := [unit-resolution #703 #1158]: #313
   154 #983 := (or #400 #150 #152 #119)
   155 #248 := (not #60)
   156 decl f23 :: S1
   157 #68 := f23
   158 #69 := (= f23 f1)
   159 decl f34 :: S1
   160 #106 := f34
   161 #107 := (= f34 f1)
   162 #298 := (not #107)
   163 #1051 := [hypothesis]: #347
   164 #1052 := [hypothesis]: #346
   165 #306 := (not #114)
   166 decl f25 :: S1
   167 #75 := f25
   168 #76 := (= f25 f1)
   169 decl f39 :: S1
   170 #124 := f39
   171 #125 := (= f39 f1)
   172 #318 := (not #125)
   173 decl f50 :: S1
   174 #162 := f50
   175 #163 := (= f50 f1)
   176 decl f59 :: S1
   177 #196 := f59
   178 #197 := (= f59 f1)
   179 #398 := (not #197)
   180 #1024 := [hypothesis]: #200
   181 #401 := (or #400 #398)
   182 #736 := [asserted]: #401
   183 #1021 := [unit-resolution #736 #1024]: #398
   184 #198 := (or #197 #163)
   185 #573 := [asserted]: #198
   186 #1022 := [unit-resolution #573 #1021]: #163
   187 #359 := (not #163)
   188 #362 := (or #359 #318)
   189 #707 := [asserted]: #362
   190 #1019 := [unit-resolution #707 #1022]: #318
   191 decl f26 :: S1
   192 #80 := f26
   193 #81 := (= f26 f1)
   194 #1153 := [hypothesis]: #313
   195 decl f35 :: S1
   196 #111 := f35
   197 #112 := (= f35 f1)
   198 #305 := (not #112)
   199 decl f43 :: S1
   200 #137 := f43
   201 #138 := (= f43 f1)
   202 #331 := (not #138)
   203 decl f52 :: S1
   204 #168 := f52
   205 #169 := (= f52 f1)
   206 #364 := (not #169)
   207 #402 := (or #400 #364)
   208 #737 := [asserted]: #402
   209 #1020 := [unit-resolution #737 #1024]: #364
   210 decl f49 :: S1
   211 #160 := f49
   212 #161 := (= f49 f1)
   213 #358 := (not #161)
   214 #360 := (or #358 #359)
   215 #705 := [asserted]: #360
   216 #1017 := [unit-resolution #705 #1022]: #358
   217 decl f41 :: S1
   218 #130 := f41
   219 #131 := (= f41 f1)
   220 #323 := (not #131)
   221 #1126 := (or #323 #119 #125)
   222 #272 := (not #81)
   223 decl f15 :: S1
   224 #43 := f15
   225 #44 := (= f15 f1)
   226 decl f13 :: S1
   227 #37 := f13
   228 #38 := (= f13 f1)
   229 #228 := (not #38)
   230 decl f11 :: S1
   231 #31 := f11
   232 #32 := (= f11 f1)
   233 #218 := (not #26)
   234 decl f7 :: S1
   235 #19 := f7
   236 #20 := (= f7 f1)
   237 decl f8 :: S1
   238 #21 := f8
   239 #22 := (= f8 f1)
   240 #214 := (not #22)
   241 #1154 := [hypothesis]: #318
   242 decl f38 :: S1
   243 #122 := f38
   244 #123 := (= f38 f1)
   245 #317 := (not #123)
   246 #1151 := [hypothesis]: #131
   247 #327 := (or #323 #317)
   248 #681 := [asserted]: #327
   249 #1152 := [unit-resolution #681 #1151]: #317
   250 #524 := (or #123 #125 #87)
   251 #126 := (or #125 #87)
   252 #127 := (or #123 #126)
   253 #525 := (iff #127 #524)
   254 #526 := [rewrite]: #525
   255 #513 := [asserted]: #127
   256 #527 := [mp #513 #526]: #524
   257 #1149 := [unit-resolution #527 #1152 #1154]: #87
   258 #280 := (or #277 #236)
   259 #647 := [asserted]: #280
   260 #1150 := [unit-resolution #647 #1149]: #236
   261 #783 := (or #47 #49)
   262 decl f4 :: S1
   263 #10 := f4
   264 #11 := (= f4 f1)
   265 #464 := (or #47 #49 #11)
   266 #786 := (iff #464 #783)
   267 #780 := (or #47 #49 false)
   268 #784 := (iff #780 #783)
   269 #785 := [rewrite]: #784
   270 #781 := (iff #464 #780)
   271 #755 := (iff #11 false)
   272 #12 := (not #11)
   273 #437 := [asserted]: #12
   274 #756 := [iff-false #437]: #755
   275 #782 := [monotonicity #756]: #781
   276 #787 := [trans #782 #785]: #786
   277 #50 := (or #49 #11)
   278 #51 := (or #47 #50)
   279 #465 := (iff #51 #464)
   280 #466 := [rewrite]: #465
   281 #457 := [asserted]: #51
   282 #467 := [mp #457 #466]: #464
   283 #788 := [mp #467 #787]: #783
   284 #1147 := [unit-resolution #788 #1150]: #47
   285 #235 := (not #47)
   286 #247 := (or #235 #214)
   287 #623 := [asserted]: #247
   288 #1148 := [unit-resolution #623 #1147]: #214
   289 #764 := (or #20 #22)
   290 decl f3 :: S1
   291 #7 := f3
   292 #8 := (= f3 f1)
   293 #443 := (or #20 #22 #8)
   294 #767 := (iff #443 #764)
   295 #761 := (or #20 #22 false)
   296 #765 := (iff #761 #764)
   297 #766 := [rewrite]: #765
   298 #762 := (iff #443 #761)
   299 #752 := (iff #8 false)
   300 #9 := (not #8)
   301 #436 := [asserted]: #9
   302 #754 := [iff-false #436]: #752
   303 #763 := [monotonicity #754]: #762
   304 #768 := [trans #763 #766]: #767
   305 #23 := (or #22 #8)
   306 #24 := (or #20 #23)
   307 #444 := (iff #24 #443)
   308 #445 := [rewrite]: #444
   309 #440 := [asserted]: #24
   310 #446 := [mp #440 #445]: #443
   311 #769 := [mp #446 #768]: #764
   312 #1145 := [unit-resolution #769 #1148]: #20
   313 #213 := (not #20)
   314 #221 := (or #218 #213)
   315 #606 := [asserted]: #221
   316 #1146 := [unit-resolution #606 #1145]: #218
   317 decl f12 :: S1
   318 #33 := f12
   319 #34 := (= f12 f1)
   320 #224 := (not #34)
   321 decl f30 :: S1
   322 #92 := f30
   323 #93 := (= f30 f1)
   324 #282 := (not #93)
   325 #328 := (or #323 #282)
   326 #682 := [asserted]: #328
   327 #1143 := [unit-resolution #682 #1151]: #282
   328 decl f27 :: S1
   329 #84 := f27
   330 #85 := (= f27 f1)
   331 #276 := (not #85)
   332 #278 := (or #276 #277)
   333 #645 := [asserted]: #278
   334 #1144 := [unit-resolution #645 #1149]: #276
   335 decl f19 :: S1
   336 #54 := f19
   337 #55 := (= f19 f1)
   338 #241 := (not #55)
   339 #245 := (or #241 #235)
   340 #621 := [asserted]: #245
   341 #1141 := [unit-resolution #621 #1147]: #241
   342 #499 := (or #91 #93 #85 #55)
   343 #94 := (or #85 #55)
   344 #95 := (or #93 #94)
   345 #96 := (or #91 #95)
   346 #500 := (iff #96 #499)
   347 #501 := [rewrite]: #500
   348 #488 := [asserted]: #96
   349 #502 := [mp #488 #501]: #499
   350 #1142 := [unit-resolution #502 #1141 #1144 #1143]: #91
   351 #296 := (or #281 #249)
   352 #659 := [asserted]: #296
   353 #1139 := [unit-resolution #659 #1142]: #249
   354 #240 := (not #53)
   355 #243 := (or #240 #235)
   356 #619 := [asserted]: #243
   357 #1140 := [unit-resolution #619 #1147]: #240
   358 decl f10 :: S1
   359 #27 := f10
   360 #28 := (= f10 f1)
   361 #219 := (not #28)
   362 #222 := (or #219 #213)
   363 #607 := [asserted]: #222
   364 #1137 := [unit-resolution #607 #1145]: #219
   365 #474 := (or #60 #62 #53 #28)
   366 #63 := (or #53 #28)
   367 #64 := (or #62 #63)
   368 #65 := (or #60 #64)
   369 #475 := (iff #65 #474)
   370 #476 := [rewrite]: #475
   371 #463 := [asserted]: #65
   372 #477 := [mp #463 #476]: #474
   373 #1138 := [unit-resolution #477 #1137 #1140 #1139]: #60
   374 #263 := (or #248 #224)
   375 #635 := [asserted]: #263
   376 #1135 := [unit-resolution #635 #1138]: #224
   377 #453 := (or #32 #34 #26)
   378 #35 := (or #34 #26)
   379 #36 := (or #32 #35)
   380 #454 := (iff #36 #453)
   381 #455 := [rewrite]: #454
   382 #442 := [asserted]: #36
   383 #456 := [mp #442 #455]: #453
   384 #1136 := [unit-resolution #456 #1135 #1146]: #32
   385 #223 := (not #32)
   386 #231 := (or #228 #223)
   387 #612 := [asserted]: #231
   388 #1133 := [unit-resolution #612 #1136]: #228
   389 #45 := (or #44 #38)
   390 #452 := [asserted]: #45
   391 #1134 := [unit-resolution #452 #1133]: #44
   392 #233 := (not #44)
   393 #274 := (or #272 #233)
   394 #643 := [asserted]: #274
   395 #1131 := [unit-resolution #643 #1134]: #272
   396 #519 := (or #119 #112 #81)
   397 #120 := (or #112 #81)
   398 #121 := (or #119 #120)
   399 #520 := (iff #121 #519)
   400 #521 := [rewrite]: #520
   401 #508 := [asserted]: #121
   402 #522 := [mp #508 #521]: #519
   403 #1132 := [unit-resolution #522 #1131 #1153]: #112
   404 decl f14 :: S1
   405 #39 := f14
   406 #40 := (= f14 f1)
   407 #229 := (not #40)
   408 #232 := (or #229 #223)
   409 #613 := [asserted]: #232
   410 #1129 := [unit-resolution #613 #1136]: #229
   411 decl f22 :: S1
   412 #66 := f22
   413 #67 := (= f22 f1)
   414 #256 := (not #67)
   415 #259 := (or #256 #248)
   416 #631 := [asserted]: #259
   417 #1130 := [unit-resolution #631 #1138]: #256
   418 decl f24 :: S1
   419 #73 := f24
   420 #74 := (= f24 f1)
   421 #264 := (not #74)
   422 #275 := (or #264 #233)
   423 #644 := [asserted]: #275
   424 #1127 := [unit-resolution #644 #1134]: #264
   425 #484 := (or #74 #76 #67 #40)
   426 #77 := (or #67 #40)
   427 #78 := (or #76 #77)
   428 #79 := (or #74 #78)
   429 #485 := (iff #79 #484)
   430 #486 := [rewrite]: #485
   431 #473 := [asserted]: #79
   432 #487 := [mp #473 #486]: #484
   433 #1128 := [unit-resolution #487 #1127 #1130 #1129]: #76
   434 #265 := (not #76)
   435 #309 := (or #305 #265)
   436 #668 := [asserted]: #309
   437 #1125 := [unit-resolution #668 #1128 #1132]: false
   438 #1123 := [lemma #1125]: #1126
   439 #1018 := [unit-resolution #1123 #1019 #1153]: #323
   440 #559 := (or #167 #169 #161 #131)
   441 #170 := (or #161 #131)
   442 #171 := (or #169 #170)
   443 #172 := (or #167 #171)
   444 #560 := (iff #172 #559)
   445 #561 := [rewrite]: #560
   446 #548 := [asserted]: #172
   447 #562 := [mp #548 #561]: #559
   448 #1015 := [unit-resolution #562 #1018 #1017 #1020]: #167
   449 #378 := (or #363 #331)
   450 #719 := [asserted]: #378
   451 #1016 := [unit-resolution #719 #1015]: #331
   452 #1026 := (or #305 #138 #125 #150 #152)
   453 #1049 := [hypothesis]: #112
   454 #307 := (or #305 #306)
   455 #666 := [asserted]: #307
   456 #1050 := [unit-resolution #666 #1049]: #306
   457 #544 := (or #150 #152 #143 #114)
   458 #153 := (or #143 #114)
   459 #154 := (or #152 #153)
   460 #155 := (or #150 #154)
   461 #545 := (iff #155 #544)
   462 #546 := [rewrite]: #545
   463 #533 := [asserted]: #155
   464 #547 := [mp #533 #546]: #544
   465 #1047 := [unit-resolution #547 #1050 #1052 #1051]: #143
   466 #342 := (or #338 #298)
   467 #692 := [asserted]: #342
   468 #1048 := [unit-resolution #692 #1047]: #298
   469 #308 := (or #305 #297)
   470 #667 := [asserted]: #308
   471 #1045 := [unit-resolution #667 #1049]: #297
   472 #341 := (or #338 #330)
   473 #691 := [asserted]: #341
   474 #1046 := [unit-resolution #691 #1047]: #330
   475 #1096 := [hypothesis]: #331
   476 #1063 := (or #277 #138 #136 #105 #107)
   477 #1083 := [hypothesis]: #87
   478 #1084 := [unit-resolution #647 #1083]: #236
   479 #1081 := [unit-resolution #788 #1084]: #47
   480 #1082 := [unit-resolution #623 #1081]: #214
   481 #1079 := [unit-resolution #769 #1082]: #20
   482 #1080 := [unit-resolution #607 #1079]: #219
   483 #1077 := [unit-resolution #619 #1081]: #240
   484 #1078 := [hypothesis]: #298
   485 #1075 := [hypothesis]: #297
   486 #1076 := [unit-resolution #621 #1081]: #241
   487 #1073 := [unit-resolution #645 #1083]: #276
   488 #1085 := (or #289 #85 #55 #138 #136)
   489 #1093 := [hypothesis]: #98
   490 #291 := (or #289 #290)
   491 #654 := [asserted]: #291
   492 #1094 := [unit-resolution #654 #1093]: #290
   493 #534 := (or #136 #138 #129 #100)
   494 #139 := (or #129 #100)
   495 #140 := (or #138 #139)
   496 #141 := (or #136 #140)
   497 #535 := (iff #141 #534)
   498 #536 := [rewrite]: #535
   499 #523 := [asserted]: #141
   500 #537 := [mp #523 #536]: #534
   501 #1091 := [unit-resolution #537 #1094 #1096 #1095]: #129
   502 #1092 := [hypothesis]: #241
   503 #1089 := [hypothesis]: #276
   504 #292 := (or #289 #281)
   505 #655 := [asserted]: #292
   506 #1090 := [unit-resolution #655 #1093]: #281
   507 #1087 := [unit-resolution #502 #1090 #1089 #1092]: #93
   508 #326 := (or #322 #282)
   509 #680 := [asserted]: #326
   510 #1088 := [unit-resolution #680 #1087 #1091]: false
   511 #1086 := [lemma #1088]: #1085
   512 #1074 := [unit-resolution #1086 #1073 #1076 #1096 #1095]: #289
   513 #509 := (or #105 #107 #98 #69)
   514 #108 := (or #98 #69)
   515 #109 := (or #107 #108)
   516 #110 := (or #105 #109)
   517 #510 := (iff #110 #509)
   518 #511 := [rewrite]: #510
   519 #498 := [asserted]: #110
   520 #512 := [mp #498 #511]: #509
   521 #1071 := [unit-resolution #512 #1074 #1075 #1078]: #69
   522 #257 := (not #69)
   523 #261 := (or #257 #248)
   524 #633 := [asserted]: #261
   525 #1072 := [unit-resolution #633 #1071]: #248
   526 #1069 := [unit-resolution #477 #1072 #1077 #1080]: #62
   527 #295 := (or #290 #249)
   528 #658 := [asserted]: #295
   529 #1070 := [unit-resolution #658 #1069]: #290
   530 #1067 := [unit-resolution #537 #1070 #1096 #1095]: #129
   531 #1068 := [unit-resolution #659 #1069]: #281
   532 #1065 := [unit-resolution #502 #1068 #1073 #1076]: #93
   533 #1066 := [unit-resolution #680 #1065 #1067]: false
   534 #1064 := [lemma #1066]: #1063
   535 #1043 := [unit-resolution #1064 #1046 #1096 #1045 #1048]: #277
   536 #1044 := [unit-resolution #527 #1043 #1154]: #123
   537 #325 := (or #322 #317)
   538 #679 := [asserted]: #325
   539 #1041 := [unit-resolution #679 #1044]: #322
   540 #1042 := [unit-resolution #537 #1041 #1096 #1046]: #100
   541 #1039 := [unit-resolution #654 #1042]: #289
   542 #1040 := [unit-resolution #512 #1039 #1045 #1048]: #69
   543 #1037 := [unit-resolution #633 #1040]: #248
   544 #1038 := [unit-resolution #658 #1042]: #249
   545 #294 := (or #290 #281)
   546 #657 := [asserted]: #294
   547 #1035 := [unit-resolution #657 #1042]: #281
   548 #329 := (or #317 #282)
   549 #683 := [asserted]: #329
   550 #1036 := [unit-resolution #683 #1044]: #282
   551 #1053 := (or #235 #62 #60)
   552 #1061 := [hypothesis]: #248
   553 #1062 := [hypothesis]: #249
   554 #1059 := [hypothesis]: #47
   555 #1060 := [unit-resolution #619 #1059]: #240
   556 #1057 := [unit-resolution #477 #1060 #1062 #1061]: #28
   557 #1058 := [unit-resolution #623 #1059]: #214
   558 #1055 := [unit-resolution #769 #1058]: #20
   559 #1056 := [unit-resolution #607 #1055 #1057]: false
   560 #1054 := [lemma #1056]: #1053
   561 #1033 := [unit-resolution #1054 #1038 #1037]: #235
   562 #1034 := [unit-resolution #788 #1033]: #49
   563 #279 := (or #276 #236)
   564 #646 := [asserted]: #279
   565 #1031 := [unit-resolution #646 #1034]: #276
   566 #1032 := [unit-resolution #502 #1031 #1036 #1035]: #55
   567 #242 := (or #240 #241)
   568 #618 := [asserted]: #242
   569 #1029 := [unit-resolution #618 #1032]: #240
   570 #1030 := [unit-resolution #477 #1029 #1038 #1037]: #28
   571 #246 := (or #241 #214)
   572 #622 := [asserted]: #246
   573 #1027 := [unit-resolution #622 #1032]: #214
   574 #1028 := [unit-resolution #769 #1027]: #20
   575 #1025 := [unit-resolution #607 #1028 #1030]: false
   576 #1023 := [lemma #1025]: #1026
   577 #1013 := [unit-resolution #1023 #1016 #1019 #1052 #1051]: #305
   578 #1014 := [unit-resolution #522 #1013 #1153]: #81
   579 #1097 := (or #272 #125 #76)
   580 #1124 := [hypothesis]: #81
   581 #1121 := [unit-resolution #643 #1124]: #233
   582 #1122 := [unit-resolution #452 #1121]: #38
   583 #1119 := [unit-resolution #612 #1122]: #223
   584 #273 := (or #272 #264)
   585 #642 := [asserted]: #273
   586 #1120 := [unit-resolution #642 #1124]: #264
   587 #1117 := [hypothesis]: #265
   588 #230 := (or #228 #229)
   589 #611 := [asserted]: #230
   590 #1118 := [unit-resolution #611 #1122]: #229
   591 #1115 := [unit-resolution #487 #1118 #1117 #1120]: #67
   592 #260 := (or #256 #224)
   593 #632 := [asserted]: #260
   594 #1116 := [unit-resolution #632 #1115]: #224
   595 #1113 := [unit-resolution #456 #1116 #1119]: #26
   596 #220 := (or #218 #219)
   597 #605 := [asserted]: #220
   598 #1114 := [unit-resolution #605 #1113]: #219
   599 #1111 := [unit-resolution #631 #1115]: #248
   600 #1112 := [unit-resolution #606 #1113]: #213
   601 #1109 := [unit-resolution #769 #1112]: #22
   602 #244 := (or #240 #214)
   603 #620 := [asserted]: #244
   604 #1110 := [unit-resolution #620 #1109]: #240
   605 #1107 := [unit-resolution #477 #1110 #1111 #1114]: #62
   606 #1108 := [unit-resolution #659 #1107]: #281
   607 #1105 := [unit-resolution #622 #1109]: #241
   608 #1106 := [unit-resolution #623 #1109]: #235
   609 #1103 := [unit-resolution #788 #1106]: #49
   610 #1104 := [unit-resolution #646 #1103]: #276
   611 #1101 := [unit-resolution #502 #1104 #1105 #1108]: #93
   612 #1102 := [unit-resolution #647 #1103]: #277
   613 #1099 := [unit-resolution #527 #1102 #1154]: #123
   614 #1100 := [unit-resolution #683 #1099 #1101]: false
   615 #1098 := [lemma #1100]: #1097
   616 #1011 := [unit-resolution #1098 #1014 #1019]: #76
   617 #311 := (or #306 #265)
   618 #670 := [asserted]: #311
   619 #1012 := [unit-resolution #670 #1011]: #306
   620 #1009 := [unit-resolution #547 #1012 #1052 #1051]: #143
   621 #1010 := [unit-resolution #692 #1009]: #298
   622 #312 := (or #297 #265)
   623 #671 := [asserted]: #312
   624 #1007 := [unit-resolution #671 #1011]: #297
   625 #1008 := [unit-resolution #691 #1009]: #330
   626 #1005 := [unit-resolution #1064 #1008 #1016 #1007 #1010]: #277
   627 #1006 := [unit-resolution #527 #1005 #1019]: #123
   628 #1003 := [unit-resolution #679 #1006]: #322
   629 #1004 := [unit-resolution #537 #1003 #1016 #1008]: #100
   630 #1001 := [unit-resolution #654 #1004]: #289
   631 #1002 := [unit-resolution #512 #1001 #1007 #1010]: #69
   632 #999 := [unit-resolution #633 #1002]: #248
   633 #1000 := [unit-resolution #658 #1004]: #249
   634 #997 := [unit-resolution #643 #1014]: #233
   635 #998 := [unit-resolution #452 #997]: #38
   636 #995 := [unit-resolution #612 #998]: #223
   637 #262 := (or #257 #224)
   638 #634 := [asserted]: #262
   639 #996 := [unit-resolution #634 #1002]: #224
   640 #993 := [unit-resolution #456 #996 #995]: #26
   641 #994 := [unit-resolution #605 #993]: #219
   642 #991 := [unit-resolution #477 #994 #1000 #999]: #53
   643 #992 := [unit-resolution #657 #1004]: #281
   644 #989 := [unit-resolution #683 #1006]: #282
   645 #990 := [unit-resolution #1054 #999 #1000]: #235
   646 #987 := [unit-resolution #788 #990]: #49
   647 #988 := [unit-resolution #646 #987]: #276
   648 #985 := [unit-resolution #502 #988 #989 #992]: #55
   649 #986 := [unit-resolution #618 #985 #991]: false
   650 #984 := [lemma #986]: #983
   651 #1162 := [unit-resolution #984 #1159 #1156 #1161]: #400
   652 #590 := (or #204 #200 #176)
   653 #205 := (or #200 #176)
   654 #206 := (or #204 #205)
   655 #591 := (iff #206 #590)
   656 #592 := [rewrite]: #591
   657 #583 := [asserted]: #206
   658 #593 := [mp #583 #592]: #590
   659 #1163 := [unit-resolution #593 #1162 #1160]: #204
   660 #404 := (not #204)
   661 #411 := (or #404 #380)
   662 #744 := [asserted]: #411
   663 #1164 := [unit-resolution #744 #1163]: #380
   664 decl f55 :: S1
   665 #180 := f55
   666 #181 := (= f55 f1)
   667 #379 := (not #181)
   668 #392 := (or #388 #379)
   669 #729 := [asserted]: #392
   670 #1165 := [unit-resolution #729 #1155]: #379
   671 decl f53 :: S1
   672 #173 := f53
   673 #174 := (= f53 f1)
   674 #371 := (not #174)
   675 #913 := (or #248 #181 #183 #150 #152 #119)
   676 #937 := [hypothesis]: #60
   677 #938 := [unit-resolution #631 #937]: #256
   678 #939 := (or #306 #67 #119)
   679 #971 := [hypothesis]: #256
   680 #950 := [hypothesis]: #114
   681 #947 := [unit-resolution #670 #950]: #265
   682 #948 := [unit-resolution #666 #950]: #305
   683 #945 := [unit-resolution #522 #948 #1153]: #81
   684 #946 := [unit-resolution #642 #945]: #264
   685 #943 := [unit-resolution #487 #946 #947 #971]: #40
   686 #944 := [unit-resolution #643 #945]: #233
   687 #941 := [unit-resolution #452 #944]: #38
   688 #942 := [unit-resolution #611 #941 #943]: false
   689 #940 := [lemma #942]: #939
   690 #935 := [unit-resolution #940 #938 #1153]: #306
   691 #936 := [unit-resolution #547 #935 #1052 #1051]: #143
   692 #933 := [unit-resolution #691 #936]: #330
   693 #934 := [unit-resolution #635 #937]: #224
   694 #952 := (or #223 #67 #119)
   695 #959 := [hypothesis]: #32
   696 #960 := [unit-resolution #612 #959]: #228
   697 #957 := [unit-resolution #452 #960]: #44
   698 #958 := [unit-resolution #643 #957]: #272
   699 #955 := [unit-resolution #522 #958 #1153]: #112
   700 #956 := [unit-resolution #613 #959]: #229
   701 #953 := [unit-resolution #644 #957]: #264
   702 #954 := [unit-resolution #487 #953 #956 #971]: #76
   703 #951 := [unit-resolution #668 #954 #955]: false
   704 #949 := [lemma #951]: #952
   705 #931 := [unit-resolution #949 #938 #1153]: #223
   706 #932 := [unit-resolution #456 #931 #934]: #26
   707 #929 := [unit-resolution #606 #932]: #213
   708 #930 := [unit-resolution #769 #929]: #22
   709 #927 := [unit-resolution #622 #930]: #241
   710 #928 := [unit-resolution #623 #930]: #235
   711 #925 := [unit-resolution #788 #928]: #49
   712 #926 := [unit-resolution #646 #925]: #276
   713 #961 := (or #297 #67 #119)
   714 #972 := [hypothesis]: #105
   715 #969 := [unit-resolution #671 #972]: #265
   716 #970 := [unit-resolution #667 #972]: #305
   717 #967 := [unit-resolution #522 #970 #1153]: #81
   718 #968 := [unit-resolution #642 #967]: #264
   719 #965 := [unit-resolution #487 #968 #969 #971]: #40
   720 #966 := [unit-resolution #643 #967]: #233
   721 #963 := [unit-resolution #452 #966]: #38
   722 #964 := [unit-resolution #611 #963 #965]: false
   723 #962 := [lemma #964]: #961
   724 #923 := [unit-resolution #962 #938 #1153]: #297
   725 #924 := [unit-resolution #633 #937]: #257
   726 #921 := [unit-resolution #692 #936]: #298
   727 #922 := [unit-resolution #512 #921 #924 #923]: #98
   728 #919 := [hypothesis]: #380
   729 #920 := [hypothesis]: #379
   730 #340 := (or #338 #339)
   731 #690 := [asserted]: #340
   732 #917 := [unit-resolution #690 #936]: #339
   733 #569 := (or #181 #183 #174 #145)
   734 #184 := (or #174 #145)
   735 #185 := (or #183 #184)
   736 #186 := (or #181 #185)
   737 #570 := (iff #186 #569)
   738 #571 := [rewrite]: #570
   739 #558 := [asserted]: #186
   740 #572 := [mp #558 #571]: #569
   741 #918 := [unit-resolution #572 #917 #920 #919]: #174
   742 #375 := (or #371 #331)
   743 #716 := [asserted]: #375
   744 #915 := [unit-resolution #716 #918]: #331
   745 #916 := [unit-resolution #1086 #915 #922 #926 #927 #933]: false
   746 #914 := [lemma #916]: #913
   747 #1166 := [unit-resolution #914 #1165 #1164 #1159 #1156 #1161]: #248
   748 #753 := (or #371 #150 #152 #119 #60)
   749 #793 := [hypothesis]: #174
   750 #374 := (or #371 #363)
   751 #715 := [asserted]: #374
   752 #794 := [unit-resolution #715 #793]: #363
   753 #791 := [unit-resolution #716 #793]: #331
   754 #802 := (or #236 #119 #150 #152 #138 #60 #167)
   755 #881 := [hypothesis]: #363
   756 #819 := [hypothesis]: #49
   757 #820 := [unit-resolution #647 #819]: #277
   758 #834 := (or #322 #167 #87)
   759 #849 := [hypothesis]: #129
   760 #324 := (or #322 #323)
   761 #678 := [asserted]: #324
   762 #850 := [unit-resolution #678 #849]: #323
   763 #847 := [unit-resolution #679 #849]: #317
   764 #848 := [unit-resolution #527 #847 #867]: #125
   765 #361 := (or #358 #318)
   766 #706 := [asserted]: #361
   767 #845 := [unit-resolution #706 #848]: #358
   768 #846 := [unit-resolution #562 #845 #881 #850]: #169
   769 #843 := [unit-resolution #707 #848]: #359
   770 #844 := [unit-resolution #573 #843]: #197
   771 #403 := (or #398 #364)
   772 #738 := [asserted]: #403
   773 #833 := [unit-resolution #738 #844 #846]: false
   774 #831 := [lemma #833]: #834
   775 #817 := [unit-resolution #831 #820 #881]: #322
   776 #818 := [unit-resolution #646 #819]: #276
   777 #851 := (or #282 #167 #87)
   778 #869 := [hypothesis]: #93
   779 #870 := [unit-resolution #682 #869]: #323
   780 #868 := [unit-resolution #683 #869]: #317
   781 #865 := [unit-resolution #527 #868 #867]: #125
   782 #866 := [unit-resolution #706 #865]: #358
   783 #863 := [unit-resolution #562 #866 #881 #870]: #169
   784 #864 := [unit-resolution #707 #865]: #359
   785 #861 := [unit-resolution #573 #864]: #197
   786 #862 := [unit-resolution #738 #861 #863]: false
   787 #852 := [lemma #862]: #851
   788 #815 := [unit-resolution #852 #820 #881]: #282
   789 #821 := (or #55 #138 #129 #150 #152 #93 #85 #60 #119)
   790 #832 := [hypothesis]: #322
   791 #829 := [hypothesis]: #282
   792 #830 := [unit-resolution #502 #1092 #829 #1089]: #91
   793 #827 := [unit-resolution #657 #830]: #290
   794 #891 := (or #67 #55 #85 #138 #60 #150 #152 #119)
   795 #911 := [unit-resolution #940 #971 #1153]: #306
   796 #912 := [unit-resolution #547 #911 #1052 #1051]: #143
   797 #909 := [unit-resolution #691 #912]: #330
   798 #910 := [unit-resolution #949 #971 #1153]: #223
   799 #907 := [unit-resolution #962 #971 #1153]: #297
   800 #908 := [unit-resolution #692 #912]: #298
   801 #905 := [unit-resolution #1086 #909 #1096 #1089 #1092]: #289
   802 #906 := [unit-resolution #512 #905 #908 #907]: #69
   803 #903 := [unit-resolution #634 #906]: #224
   804 #904 := [unit-resolution #456 #903 #910]: #26
   805 #901 := [unit-resolution #605 #904]: #219
   806 #902 := [unit-resolution #606 #904]: #213
   807 #899 := [unit-resolution #769 #902]: #22
   808 #900 := [unit-resolution #620 #899]: #240
   809 #897 := [unit-resolution #477 #900 #1061 #901]: #62
   810 #898 := [unit-resolution #658 #897]: #290
   811 #895 := [unit-resolution #537 #898 #1096 #909]: #129
   812 #896 := [unit-resolution #659 #897]: #281
   813 #893 := [unit-resolution #502 #896 #1092 #1089]: #93
   814 #894 := [unit-resolution #680 #893 #895]: false
   815 #892 := [lemma #894]: #891
   816 #828 := [unit-resolution #892 #1092 #1089 #1096 #1061 #1052 #1051 #1153]: #67
   817 #258 := (or #256 #257)
   818 #630 := [asserted]: #258
   819 #825 := [unit-resolution #630 #828]: #257
   820 #826 := [unit-resolution #655 #830]: #289
   821 #973 := (or #330 #69 #98 #150 #152)
   822 #981 := [hypothesis]: #136
   823 #982 := [unit-resolution #691 #981]: #338
   824 #979 := [unit-resolution #547 #982 #1052 #1051]: #114
   825 #977 := [hypothesis]: #257
   826 #345 := (or #330 #298)
   827 #695 := [asserted]: #345
   828 #978 := [unit-resolution #695 #981]: #298
   829 #975 := [unit-resolution #512 #978 #977 #980]: #105
   830 #310 := (or #306 #297)
   831 #669 := [asserted]: #310
   832 #976 := [unit-resolution #669 #975 #979]: false
   833 #974 := [lemma #976]: #973
   834 #823 := [unit-resolution #974 #826 #825 #1052 #1051]: #330
   835 #824 := [unit-resolution #537 #823 #827 #1096 #832]: false
   836 #822 := [lemma #824]: #821
   837 #816 := [unit-resolution #822 #817 #1096 #1052 #1051 #815 #818 #1061 #1153]: #55
   838 #813 := [unit-resolution #618 #816]: #240
   839 #814 := [unit-resolution #622 #816]: #214
   840 #811 := [unit-resolution #769 #814]: #20
   841 #812 := [unit-resolution #607 #811]: #219
   842 #809 := [unit-resolution #477 #812 #1061 #813]: #62
   843 #810 := [unit-resolution #658 #809]: #290
   844 #807 := [unit-resolution #537 #810 #1096 #817]: #136
   845 #808 := [unit-resolution #691 #807]: #338
   846 #805 := [unit-resolution #547 #808 #1052 #1051]: #114
   847 #293 := (or #289 #249)
   848 #656 := [asserted]: #293
   849 #806 := [unit-resolution #656 #809]: #289
   850 #803 := [unit-resolution #974 #807 #806 #1052 #1051]: #69
   851 #804 := [unit-resolution #630 #803]: #256
   852 #801 := [unit-resolution #940 #804 #805 #1153]: false
   853 #799 := [lemma #801]: #802
   854 #792 := [unit-resolution #799 #791 #1052 #1051 #1153 #1061 #794]: #236
   855 #789 := [unit-resolution #788 #792]: #47
   856 #790 := [unit-resolution #1054 #789 #1061]: #62
   857 #778 := [unit-resolution #658 #790]: #290
   858 #779 := [unit-resolution #656 #790]: #289
   859 #795 := (or #330 #119 #150 #152 #98)
   860 #800 := [unit-resolution #974 #981 #980 #1052 #1051]: #69
   861 #797 := [unit-resolution #630 #800]: #256
   862 #798 := [unit-resolution #940 #797 #979 #1153]: false
   863 #796 := [lemma #798]: #795
   864 #776 := [unit-resolution #796 #779 #1052 #1051 #1153]: #330
   865 #777 := [unit-resolution #537 #776 #791 #778]: #129
   866 #774 := [unit-resolution #831 #777 #794]: #87
   867 #775 := [unit-resolution #659 #790]: #281
   868 #772 := [unit-resolution #621 #789]: #241
   869 #773 := [unit-resolution #680 #777]: #282
   870 #770 := [unit-resolution #502 #773 #772 #775]: #85
   871 #771 := [unit-resolution #645 #770 #774]: false
   872 #751 := [lemma #771]: #753
   873 #1167 := [unit-resolution #751 #1159 #1156 #1161 #1166]: #371
   874 #1168 := [unit-resolution #572 #1167 #1165 #1164]: #145
   875 #1169 := [unit-resolution #690 #1168]: #338
   876 #1170 := [unit-resolution #547 #1169 #1159 #1156]: #114
   877 #1171 := [unit-resolution #669 #1170]: #297
   878 #344 := (or #339 #298)
   879 #694 := [asserted]: #344
   880 #1172 := [unit-resolution #694 #1168]: #298
   881 #1173 := [unit-resolution #940 #1170 #1161]: #67
   882 #1174 := [unit-resolution #630 #1173]: #257
   883 #1175 := [unit-resolution #512 #1174 #1172 #1171]: #98
   884 #1176 := [unit-resolution #656 #1175]: #249
   885 #1177 := [unit-resolution #632 #1173]: #224
   886 #1178 := [unit-resolution #666 #1170]: #305
   887 #1179 := [unit-resolution #522 #1178 #1161]: #81
   888 #1180 := [unit-resolution #643 #1179]: #233
   889 #1181 := [unit-resolution #452 #1180]: #38
   890 #1182 := [unit-resolution #612 #1181]: #223
   891 #1183 := [unit-resolution #456 #1182 #1177]: #26
   892 #1184 := [unit-resolution #605 #1183]: #219
   893 #1185 := [unit-resolution #477 #1184 #1166 #1176]: #53
   894 #1186 := [unit-resolution #606 #1183]: #213
   895 #1187 := [unit-resolution #769 #1186]: #22
   896 #1188 := [unit-resolution #620 #1187 #1185]: false
   897 #1190 := [lemma #1188]: #1189
   898 #1365 := [unit-resolution #1190 #1160]: #388
   899 #211 := (or #208 #190)
   900 decl f5 :: S1
   901 #13 := f5
   902 #14 := (= f5 f1)
   903 #600 := (or #14 #208 #190)
   904 #858 := (iff #600 #211)
   905 #853 := (or false #208 #190)
   906 #856 := (iff #853 #211)
   907 #857 := [rewrite]: #856
   908 #854 := (iff #600 #853)
   909 #757 := (iff #14 false)
   910 #15 := (not #14)
   911 #438 := [asserted]: #15
   912 #758 := [iff-false #438]: #757
   913 #855 := [monotonicity #758]: #854
   914 #859 := [trans #855 #857]: #858
   915 #212 := (or #14 #211)
   916 #601 := (iff #212 #600)
   917 #602 := [rewrite]: #601
   918 #589 := [asserted]: #212
   919 #603 := [mp #589 #602]: #600
   920 #860 := [mp #603 #859]: #211
   921 #1366 := [unit-resolution #860 #1365]: #208
   922 #408 := (not #208)
   923 #410 := (or #408 #380)
   924 #743 := [asserted]: #410
   925 #1367 := [unit-resolution #743 #1366]: #380
   926 #409 := (or #408 #404)
   927 #742 := [asserted]: #409
   928 #1368 := [unit-resolution #742 #1366]: #404
   929 #1369 := [unit-resolution #593 #1368 #1160]: #200
   930 #1239 := (or #119 #183 #400)
   931 #1224 := [unit-resolution #1123 #1153 #1019]: #323
   932 #1225 := [unit-resolution #562 #1224 #1017 #1020]: #167
   933 #1226 := [unit-resolution #715 #1225]: #371
   934 #1222 := (or #379 #400 #119)
   935 #1216 := [hypothesis]: #181
   936 #390 := (or #387 #379)
   937 #727 := [asserted]: #390
   938 #1217 := [unit-resolution #727 #1216]: #387
   939 #1218 := [unit-resolution #842 #1217]: #157
   940 #394 := (or #379 #347)
   941 #731 := [asserted]: #394
   942 #1219 := [unit-resolution #731 #1216]: #347
   943 #1220 := [unit-resolution #984 #1219 #1024 #1153]: #150
   944 #1221 := [unit-resolution #702 #1220 #1218]: false
   945 #1223 := [lemma #1221]: #1222
   946 #1227 := [unit-resolution #1223 #1153 #1024]: #379
   947 #1228 := [unit-resolution #572 #1227 #1226 #919]: #145
   948 #1229 := [unit-resolution #694 #1228]: #298
   949 #1192 := (or #297 #125 #119)
   950 #1191 := [unit-resolution #1098 #967 #969 #1154]: false
   951 #1193 := [lemma #1191]: #1192
   952 #1230 := [unit-resolution #1193 #1153 #1019]: #297
   953 #1231 := [unit-resolution #719 #1225]: #331
   954 #343 := (or #339 #330)
   955 #693 := [asserted]: #343
   956 #1232 := [unit-resolution #693 #1228]: #330
   957 #1233 := [unit-resolution #1064 #1232 #1231 #1230 #1229]: #277
   958 #1234 := [unit-resolution #527 #1233 #1019]: #123
   959 #1214 := (or #339 #138 #119 #125 #98)
   960 #1194 := [hypothesis]: #145
   961 #1195 := [unit-resolution #693 #1194]: #330
   962 #1196 := [unit-resolution #694 #1194]: #298
   963 #1197 := [unit-resolution #1193 #1153 #1154]: #297
   964 #1198 := [unit-resolution #1064 #1195 #1096 #1197 #1196]: #277
   965 #1199 := [unit-resolution #527 #1198 #1154]: #123
   966 #1200 := [unit-resolution #679 #1199]: #322
   967 #1201 := [unit-resolution #537 #1200 #1096 #1195]: #100
   968 #1202 := [unit-resolution #658 #1201]: #249
   969 #1203 := [unit-resolution #512 #1196 #1197 #980]: #69
   970 #1204 := [unit-resolution #633 #1203]: #248
   971 #1205 := [unit-resolution #634 #1203]: #224
   972 #1206 := [unit-resolution #630 #1203]: #256
   973 #1207 := [unit-resolution #949 #1206 #1153]: #223
   974 #1208 := [unit-resolution #456 #1207 #1205]: #26
   975 #1209 := [unit-resolution #605 #1208]: #219
   976 #1210 := [unit-resolution #477 #1209 #1204 #1202]: #53
   977 #1211 := [unit-resolution #606 #1208]: #213
   978 #1212 := [unit-resolution #769 #1211]: #22
   979 #1213 := [unit-resolution #620 #1212 #1210]: false
   980 #1215 := [lemma #1213]: #1214
   981 #1235 := [unit-resolution #1215 #1228 #1153 #1019 #1231]: #98
   982 #1236 := [unit-resolution #654 #1235]: #290
   983 #1237 := [unit-resolution #537 #1236 #1231 #1232]: #129
   984 #1238 := [unit-resolution #679 #1237 #1234]: false
   985 #1240 := [lemma #1238]: #1239
   986 #1370 := [unit-resolution #1240 #1367 #1369]: #119
   987 #1371 := [unit-resolution #703 #1370]: #354
   988 #1372 := [unit-resolution #842 #1371]: #188
   989 #1373 := [unit-resolution #727 #1372]: #379
   990 #1374 := [unit-resolution #737 #1369]: #364
   991 #1375 := [unit-resolution #736 #1369]: #398
   992 #1376 := [unit-resolution #573 #1375]: #163
   993 #1377 := [unit-resolution #705 #1376]: #358
   994 #1378 := [unit-resolution #707 #1376]: #318
   995 #391 := (or #387 #347)
   996 #728 := [asserted]: #391
   997 #1379 := [unit-resolution #728 #1372]: #347
   998 #357 := (or #346 #313)
   999 #704 := [asserted]: #357
  1000 #1380 := [unit-resolution #704 #1370]: #346
  1001 #1351 := (or #98 #125 #161 #169 #181 #183 #150 #152)
  1002 #1258 := [hypothesis]: #364
  1003 #1259 := [hypothesis]: #358
  1004 #1332 := (or #136 #150 #152 #181 #183 #125 #161 #169 #98)
  1005 #1317 := (or #129 #125 #136 #161 #169 #181 #183 #150 #152 #98)
  1006 #1297 := (or #105 #125 #98 #161 #169 #181 #183 #129 #136)
  1007 #1276 := (or #290 #125 #161 #169 #181 #183 #98 #105)
  1008 #1256 := [hypothesis]: #100
  1009 #1257 := [unit-resolution #657 #1256]: #281
  1010 #1260 := [unit-resolution #658 #1256]: #249
  1011 #1254 := (or #60 #62 #91 #125)
  1012 #1241 := [hypothesis]: #281
  1013 #1242 := [unit-resolution #1054 #1061 #1062]: #235
  1014 #1243 := [unit-resolution #788 #1242]: #49
  1015 #1244 := [unit-resolution #646 #1243]: #276
  1016 #1245 := [unit-resolution #647 #1243]: #277
  1017 #1246 := [unit-resolution #527 #1245 #1154]: #123
  1018 #1247 := [unit-resolution #683 #1246]: #282
  1019 #1248 := [unit-resolution #502 #1247 #1244 #1241]: #55
  1020 #1249 := [unit-resolution #618 #1248]: #240
  1021 #1250 := [unit-resolution #477 #1249 #1061 #1062]: #28
  1022 #1251 := [unit-resolution #622 #1248]: #214
  1023 #1252 := [unit-resolution #769 #1251]: #20
  1024 #1253 := [unit-resolution #607 #1252 #1250]: false
  1025 #1255 := [lemma #1253]: #1254
  1026 #1261 := [unit-resolution #1255 #1260 #1257 #1154]: #60
  1027 #1262 := [unit-resolution #633 #1261]: #257
  1028 #1263 := [unit-resolution #512 #1262 #980 #1075]: #107
  1029 #1264 := [unit-resolution #694 #1263]: #339
  1030 #1265 := [unit-resolution #572 #1264 #920 #919]: #174
  1031 #1266 := [unit-resolution #715 #1265]: #363
  1032 #1267 := [unit-resolution #562 #1266 #1259 #1258]: #131
  1033 #1268 := [unit-resolution #682 #1267]: #282
  1034 #1269 := [unit-resolution #681 #1267]: #317
  1035 #1270 := [unit-resolution #527 #1269 #1154]: #87
  1036 #1271 := [unit-resolution #645 #1270]: #276
  1037 #1272 := [unit-resolution #502 #1271 #1268 #1257]: #55
  1038 #1273 := [unit-resolution #647 #1270]: #236
  1039 #1274 := [unit-resolution #788 #1273]: #47
  1040 #1275 := [unit-resolution #621 #1274 #1272]: false
  1041 #1277 := [lemma #1275]: #1276
  1042 #1278 := [unit-resolution #1277 #1075 #1259 #1258 #920 #919 #980 #1154]: #290
  1043 #1279 := [unit-resolution #537 #1278 #832 #1095]: #138
  1044 #1280 := [unit-resolution #716 #1279]: #371
  1045 #1281 := [unit-resolution #572 #1280 #920 #919]: #145
  1046 #1282 := [unit-resolution #694 #1281]: #298
  1047 #1283 := [unit-resolution #512 #1282 #980 #1075]: #69
  1048 #1284 := [unit-resolution #633 #1283]: #248
  1049 #1285 := [unit-resolution #719 #1279]: #363
  1050 #1286 := [unit-resolution #562 #1285 #1259 #1258]: #131
  1051 #1287 := [unit-resolution #681 #1286]: #317
  1052 #1288 := [unit-resolution #527 #1287 #1154]: #87
  1053 #1289 := [unit-resolution #647 #1288]: #236
  1054 #1290 := [unit-resolution #788 #1289]: #47
  1055 #1291 := [unit-resolution #1054 #1290 #1284]: #62
  1056 #1292 := [unit-resolution #645 #1288]: #276
  1057 #1293 := [unit-resolution #682 #1286]: #282
  1058 #1294 := [unit-resolution #621 #1290]: #241
  1059 #1295 := [unit-resolution #502 #1294 #1293 #1292]: #91
  1060 #1296 := [unit-resolution #659 #1295 #1291]: false
  1061 #1298 := [lemma #1296]: #1297
  1062 #1299 := [unit-resolution #1298 #832 #980 #1259 #1258 #920 #919 #1154 #1095]: #105
  1063 #1300 := [unit-resolution #669 #1299]: #306
  1064 #1301 := [unit-resolution #547 #1300 #1052 #1051]: #143
  1065 #1302 := [unit-resolution #690 #1301]: #339
  1066 #1303 := [unit-resolution #572 #1302 #920 #919]: #174
  1067 #1304 := [unit-resolution #716 #1303]: #331
  1068 #1305 := [unit-resolution #537 #1304 #832 #1095]: #100
  1069 #1306 := [unit-resolution #657 #1305]: #281
  1070 #1307 := [unit-resolution #715 #1303]: #363
  1071 #1308 := [unit-resolution #562 #1307 #1259 #1258]: #131
  1072 #1309 := [unit-resolution #682 #1308]: #282
  1073 #1310 := [unit-resolution #681 #1308]: #317
  1074 #1311 := [unit-resolution #527 #1310 #1154]: #87
  1075 #1312 := [unit-resolution #645 #1311]: #276
  1076 #1313 := [unit-resolution #502 #1312 #1309 #1306]: #55
  1077 #1314 := [unit-resolution #647 #1311]: #236
  1078 #1315 := [unit-resolution #788 #1314]: #47
  1079 #1316 := [unit-resolution #621 #1315 #1313]: false
  1080 #1318 := [lemma #1316]: #1317
  1081 #1319 := [unit-resolution #1318 #1095 #1154 #1259 #1258 #920 #919 #1052 #1051 #980]: #129
  1082 #1320 := [unit-resolution #678 #1319]: #323
  1083 #1321 := [unit-resolution #562 #1320 #1259 #1258]: #167
  1084 #1322 := [unit-resolution #715 #1321]: #371
  1085 #1323 := [unit-resolution #572 #1322 #920 #919]: #145
  1086 #1324 := [unit-resolution #690 #1323]: #338
  1087 #1325 := [unit-resolution #547 #1324 #1052 #1051]: #114
  1088 #1326 := [unit-resolution #679 #1319]: #317
  1089 #1327 := [unit-resolution #527 #1326 #1154]: #87
  1090 #335 := (or #331 #322)
  1091 #687 := [asserted]: #335
  1092 #1328 := [unit-resolution #687 #1319]: #331
  1093 #1329 := [unit-resolution #694 #1323]: #298
  1094 #1330 := [unit-resolution #1064 #1329 #1095 #1328 #1327]: #105
  1095 #1331 := [unit-resolution #669 #1330 #1325]: false
  1096 #1333 := [lemma #1331]: #1332
  1097 #1334 := [unit-resolution #1333 #980 #1051 #920 #919 #1154 #1259 #1258 #1052]: #136
  1098 #1335 := [unit-resolution #974 #1334 #980 #1052 #1051]: #69
  1099 #1336 := [unit-resolution #633 #1335]: #248
  1100 #1337 := [unit-resolution #693 #1334]: #339
  1101 #1338 := [unit-resolution #572 #1337 #920 #919]: #174
  1102 #1339 := [unit-resolution #715 #1338]: #363
  1103 #1340 := [unit-resolution #562 #1339 #1259 #1258]: #131
  1104 #1341 := [unit-resolution #681 #1340]: #317
  1105 #1342 := [unit-resolution #527 #1341 #1154]: #87
  1106 #1343 := [unit-resolution #647 #1342]: #236
  1107 #1344 := [unit-resolution #788 #1343]: #47
  1108 #1345 := [unit-resolution #1054 #1344 #1336]: #62
  1109 #1346 := [unit-resolution #645 #1342]: #276
  1110 #1347 := [unit-resolution #682 #1340]: #282
  1111 #1348 := [unit-resolution #621 #1344]: #241
  1112 #1349 := [unit-resolution #502 #1348 #1347 #1346]: #91
  1113 #1350 := [unit-resolution #659 #1349 #1345]: false
  1114 #1352 := [lemma #1350]: #1351
  1115 #1381 := [unit-resolution #1352 #1378 #1377 #1374 #1373 #1367 #1380 #1379]: #98
  1116 #1382 := [unit-resolution #654 #1381]: #290
  1117 #1363 := (or #317 #100 #181 #183 #161 #169)
  1118 #1353 := [hypothesis]: #123
  1119 #1354 := [unit-resolution #681 #1353]: #323
  1120 #1355 := [unit-resolution #562 #1354 #1259 #1258]: #167
  1121 #1356 := [unit-resolution #715 #1355]: #371
  1122 #1357 := [unit-resolution #572 #1356 #920 #919]: #145
  1123 #1358 := [unit-resolution #679 #1353]: #322
  1124 #1359 := [hypothesis]: #290
  1125 #1360 := [unit-resolution #719 #1355]: #331
  1126 #1361 := [unit-resolution #537 #1360 #1359 #1358]: #136
  1127 #1362 := [unit-resolution #693 #1361 #1357]: false
  1128 #1364 := [lemma #1362]: #1363
  1129 #1383 := [unit-resolution #1364 #1382 #1373 #1367 #1377 #1374]: #317
  1130 #1384 := [unit-resolution #527 #1383 #1378]: #87
  1131 #1385 := [unit-resolution #645 #1384]: #276
  1132 #1386 := [unit-resolution #655 #1381]: #281
  1133 #1387 := [unit-resolution #647 #1384]: #236
  1134 #1388 := [unit-resolution #788 #1387]: #47
  1135 #1389 := [unit-resolution #621 #1388]: #241
  1136 #1390 := [unit-resolution #502 #1389 #1386 #1385]: #93
  1137 #1391 := [unit-resolution #682 #1390]: #323
  1138 #1392 := [unit-resolution #562 #1391 #1377 #1374]: #167
  1139 #1393 := [unit-resolution #715 #1392]: #371
  1140 #1394 := [unit-resolution #572 #1393 #1373 #1367]: #145
  1141 #1395 := [unit-resolution #680 #1390]: #322
  1142 #1396 := [unit-resolution #719 #1392]: #331
  1143 #1397 := [unit-resolution #537 #1396 #1382 #1395]: #136
  1144 #1398 := [unit-resolution #693 #1397 #1394]: false
  1145 #1399 := [lemma #1398]: #176
  1146 #376 := (or #372 #363)
  1147 #717 := [asserted]: #376
  1148 #1426 := [unit-resolution #717 #1399]: #363
  1149 #1428 := [unit-resolution #831 #1426]: #1427
  1150 #1429 := [unit-resolution #1428 #867]: #322
  1151 #1431 := (or #136 #129 #100)
  1152 #377 := (or #372 #331)
  1153 #718 := [asserted]: #377
  1154 #1430 := [unit-resolution #718 #1399]: #331
  1155 #1432 := [unit-resolution #537 #1430]: #1431
  1156 #1433 := [unit-resolution #1432 #1429 #1095]: #100
  1157 #1434 := [unit-resolution #657 #1433]: #281
  1158 #1435 := (or #282 #87)
  1159 #1436 := [unit-resolution #852 #1426]: #1435
  1160 #1437 := [unit-resolution #1436 #867]: #282
  1161 #1419 := (or #214 #93 #91)
  1162 #1413 := [hypothesis]: #22
  1163 #1414 := [unit-resolution #622 #1413]: #241
  1164 #1415 := [unit-resolution #502 #1414 #829 #1241]: #85
  1165 #1416 := [unit-resolution #623 #1413]: #235
  1166 #1417 := [unit-resolution #788 #1416]: #49
  1167 #1418 := [unit-resolution #646 #1417 #1415]: false
  1168 #1420 := [lemma #1418]: #1419
  1169 #1438 := [unit-resolution #1420 #1437 #1434]: #214
  1170 #1439 := [unit-resolution #769 #1438]: #20
  1171 #1440 := [unit-resolution #607 #1439]: #219
  1172 #1441 := [unit-resolution #658 #1433]: #249
  1173 #1442 := [unit-resolution #606 #1439]: #218
  1174 #1424 := (or #248 #26 #98)
  1175 #1421 := [hypothesis]: #218
  1176 #1411 := (or #223 #98 #69 #67)
  1177 #1400 := [unit-resolution #949 #959 #971]: #119
  1178 #1401 := [unit-resolution #703 #1400]: #354
  1179 #1402 := [unit-resolution #842 #1401]: #188
  1180 #1403 := [unit-resolution #728 #1402]: #347
  1181 #1404 := [unit-resolution #704 #1400]: #346
  1182 #1405 := [unit-resolution #487 #953 #971 #956]: #76
  1183 #1406 := [unit-resolution #670 #1405]: #306
  1184 #1407 := [unit-resolution #547 #1406 #1404 #1403]: #143
  1185 #1408 := [unit-resolution #671 #1405]: #297
  1186 #1409 := [unit-resolution #512 #1408 #980 #977]: #107
  1187 #1410 := [unit-resolution #692 #1409 #1407]: false
  1188 #1412 := [lemma #1410]: #1411
  1189 #1422 := [unit-resolution #1412 #924 #980 #938]: #223
  1190 #1423 := [unit-resolution #456 #1422 #934 #1421]: false
  1191 #1425 := [lemma #1423]: #1424
  1192 #1443 := [unit-resolution #1425 #1442 #980]: #248
  1193 #1444 := [unit-resolution #477 #1443 #1441 #1440]: #53
  1194 #1445 := [unit-resolution #618 #1444]: #241
  1195 #1446 := [unit-resolution #1054 #1443 #1441]: #235
  1196 #1447 := [unit-resolution #788 #1446]: #49
  1197 #1448 := [unit-resolution #646 #1447]: #276
  1198 #1449 := [unit-resolution #502 #1448 #1445 #1437 #1434]: false
  1199 #1451 := [lemma #1449]: #1450
  1200 #1452 := [unit-resolution #1451 #1095 #980]: #87
  1201 #1453 := [unit-resolution #647 #1452]: #236
  1202 #1454 := [unit-resolution #788 #1453]: #47
  1203 #1455 := [unit-resolution #623 #1454]: #214
  1204 #1456 := [unit-resolution #769 #1455]: #20
  1205 #1457 := [unit-resolution #606 #1456]: #218
  1206 #1458 := [unit-resolution #1425 #1457 #980]: #248
  1207 #1459 := [unit-resolution #1054 #1458 #1454]: #62
  1208 #1460 := [unit-resolution #658 #1459]: #290
  1209 #1461 := [unit-resolution #1432 #1460 #1095]: #129
  1210 #1462 := [unit-resolution #621 #1454]: #241
  1211 #1463 := [unit-resolution #645 #1452]: #276
  1212 #1464 := [unit-resolution #659 #1459]: #281
  1213 #1465 := [unit-resolution #502 #1464 #1463 #1462]: #93
  1214 #1466 := [unit-resolution #680 #1465 #1461]: false
  1215 #1468 := [lemma #1466]: #1467
  1216 #1481 := [unit-resolution #1468 #980]: #136
  1217 #1482 := [unit-resolution #693 #1481]: #339
  1218 #1479 := (or #387 #145)
  1219 #1469 := [hypothesis]: #188
  1220 #1470 := [unit-resolution #726 #1469]: #388
  1221 #1471 := [unit-resolution #860 #1470]: #208
  1222 #1472 := [hypothesis]: #339
  1223 #1473 := [unit-resolution #727 #1469]: #379
  1224 #1475 := (or #181 #183 #145)
  1225 #373 := (or #371 #372)
  1226 #714 := [asserted]: #373
  1227 #1474 := [unit-resolution #714 #1399]: #371
  1228 #1476 := [unit-resolution #572 #1474]: #1475
  1229 #1477 := [unit-resolution #1476 #1473 #1472]: #183
  1230 #1478 := [unit-resolution #743 #1477 #1471]: false
  1231 #1480 := [lemma #1478]: #1479
  1232 #1483 := [unit-resolution #1480 #1482]: #387
  1233 #1484 := [unit-resolution #842 #1483]: #157
  1234 #1485 := [unit-resolution #702 #1484]: #346
  1235 #1486 := [unit-resolution #703 #1484]: #313
  1236 #1487 := [unit-resolution #796 #1486 #1481 #1485 #980]: #152
  1237 #1488 := [unit-resolution #730 #1487]: #388
  1238 #1489 := [unit-resolution #860 #1488]: #208
  1239 #1490 := [unit-resolution #731 #1487]: #379
  1240 #1491 := [unit-resolution #1476 #1490 #1482]: #183
  1241 #1492 := [unit-resolution #743 #1491 #1489]: false
  1242 #1493 := [lemma #1492]: #98
  1243 #1515 := [unit-resolution #656 #1493]: #249
  1244 #1511 := [unit-resolution #655 #1493]: #281
  1245 #1512 := [unit-resolution #1420 #829 #1511]: #214
  1246 #1513 := [unit-resolution #769 #1512]: #20
  1247 #1514 := [unit-resolution #607 #1513]: #219
  1248 #1516 := [unit-resolution #606 #1513]: #218
  1249 #1509 := (or #248 #26)
  1250 #1494 := [unit-resolution #654 #1493]: #290
  1251 #1495 := [unit-resolution #1432 #1095 #1494]: #129
  1252 #300 := (or #297 #289)
  1253 #661 := [asserted]: #300
  1254 #1496 := [unit-resolution #661 #1493]: #297
  1255 #302 := (or #298 #289)
  1256 #663 := [asserted]: #302
  1257 #1497 := [unit-resolution #663 #1493]: #298
  1258 #1498 := (or #277 #136 #105 #107)
  1259 #1499 := [unit-resolution #1064 #1430]: #1498
  1260 #1500 := [unit-resolution #1499 #1095 #1497 #1496]: #277
  1261 #1501 := [unit-resolution #1428 #1500 #1495]: false
  1262 #1502 := [lemma #1501]: #136
  1263 #1503 := [unit-resolution #693 #1502]: #339
  1264 #1504 := [unit-resolution #1480 #1503]: #387
  1265 #1505 := [unit-resolution #842 #1504]: #157
  1266 #1506 := [unit-resolution #703 #1505]: #313
  1267 #1507 := [unit-resolution #949 #938 #1506]: #223
  1268 #1508 := [unit-resolution #456 #1507 #934 #1421]: false
  1269 #1510 := [lemma #1508]: #1509
  1270 #1517 := [unit-resolution #1510 #1516]: #248
  1271 #1518 := [unit-resolution #477 #1517 #1515 #1514]: #53
  1272 #1519 := [unit-resolution #618 #1518]: #241
  1273 #1520 := [unit-resolution #1054 #1517 #1515]: #235
  1274 #1521 := [unit-resolution #788 #1520]: #49
  1275 #1522 := [unit-resolution #646 #1521]: #276
  1276 #1523 := [unit-resolution #502 #1522 #1519 #1511 #829]: false
  1277 #1524 := [lemma #1523]: #93
  1278 #1525 := [unit-resolution #1436 #1524]: #87
  1279 #321 := (or #318 #277)
  1280 #677 := [asserted]: #321
  1281 #1526 := [unit-resolution #677 #1525]: #318
  1282 #1527 := [unit-resolution #1255 #1526 #1511 #1515]: #60
  1283 #1528 := [unit-resolution #1510 #1527]: #26
  1284 #1529 := [unit-resolution #647 #1525]: #236
  1285 #1530 := [unit-resolution #788 #1529]: #47
  1286 #1531 := [unit-resolution #623 #1530]: #214
  1287 #1532 := [unit-resolution #769 #1531]: #20
  1288 [unit-resolution #606 #1532 #1528]: false
  1289 unsat
  1290 a69a9e8c5e31ec6b9da4cf96f47b52cf6b9404d9 117 0
  1291 #2 := false
  1292 decl f3 :: (-> S3 S2 S1)
  1293 #10 := (:var 0 S2)
  1294 decl f4 :: (-> S4 S1 S3)
  1295 decl f6 :: S1
  1296 #16 := f6
  1297 decl f5 :: S4
  1298 #7 := f5
  1299 #17 := (f4 f5 f6)
  1300 #18 := (f3 #17 #10)
  1301 #573 := (pattern #18)
  1302 decl f1 :: S1
  1303 #3 := f1
  1304 #19 := (= #18 f1)
  1305 #76 := (not #19)
  1306 #574 := (forall (vars (?v0 S2)) (:pat #573) #76)
  1307 decl f7 :: S2
  1308 #21 := f7
  1309 #22 := (f3 #17 f7)
  1310 #23 := (= #22 f1)
  1311 #150 := (= f6 f1)
  1312 #151 := (iff #23 #150)
  1313 #8 := (:var 1 S1)
  1314 #9 := (f4 f5 #8)
  1315 #11 := (f3 #9 #10)
  1316 #566 := (pattern #11)
  1317 #13 := (= #8 f1)
  1318 #12 := (= #11 f1)
  1319 #14 := (iff #12 #13)
  1320 #567 := (forall (vars (?v0 S1) (?v1 S2)) (:pat #566) #14)
  1321 #15 := (forall (vars (?v0 S1) (?v1 S2)) #14)
  1322 #570 := (iff #15 #567)
  1323 #568 := (iff #14 #14)
  1324 #569 := [refl]: #568
  1325 #571 := [quant-intro #569]: #570
  1326 #62 := (~ #15 #15)
  1327 #60 := (~ #14 #14)
  1328 #61 := [refl]: #60
  1329 #63 := [nnf-pos #61]: #62
  1330 #46 := [asserted]: #15
  1331 #53 := [mp~ #46 #63]: #15
  1332 #572 := [mp #53 #571]: #567
  1333 #152 := (not #567)
  1334 #228 := (or #152 #151)
  1335 #561 := [quant-inst #16 #21]: #228
  1336 #237 := [unit-resolution #561 #572]: #151
  1337 decl ?v0!0 :: S2
  1338 #66 := ?v0!0
  1339 #67 := (f3 #17 ?v0!0)
  1340 #68 := (= #67 f1)
  1341 #236 := (iff #68 #150)
  1342 #238 := (or #152 #236)
  1343 #229 := [quant-inst #16 #66]: #238
  1344 #227 := [unit-resolution #229 #572]: #236
  1345 #240 := (not #236)
  1346 #199 := (or #240 #150)
  1347 #55 := (not #23)
  1348 #215 := [hypothesis]: #55
  1349 #83 := (or #68 #23)
  1350 #79 := (forall (vars (?v0 S2)) #76)
  1351 #82 := (or #79 #55)
  1352 #84 := (and #83 #82)
  1353 #20 := (exists (vars (?v0 S2)) #19)
  1354 #48 := (not #20)
  1355 #49 := (iff #48 #23)
  1356 #85 := (~ #49 #84)
  1357 #57 := (~ #23 #23)
  1358 #65 := [refl]: #57
  1359 #64 := (~ #55 #55)
  1360 #56 := [refl]: #64
  1361 #80 := (~ #48 #79)
  1362 #77 := (~ #76 #76)
  1363 #78 := [refl]: #77
  1364 #81 := [nnf-neg #78]: #80
  1365 #73 := (not #48)
  1366 #74 := (~ #73 #68)
  1367 #69 := (~ #20 #68)
  1368 #70 := [sk]: #69
  1369 #75 := [nnf-neg #70]: #74
  1370 #86 := [nnf-pos #75 #81 #56 #65]: #85
  1371 #24 := (iff #20 #23)
  1372 #25 := (not #24)
  1373 #50 := (iff #25 #49)
  1374 #51 := [rewrite]: #50
  1375 #47 := [asserted]: #25
  1376 #54 := [mp #47 #51]: #49
  1377 #87 := [mp~ #54 #86]: #84
  1378 #90 := [and-elim #87]: #83
  1379 #557 := [unit-resolution #90 #215]: #68
  1380 #243 := (not #68)
  1381 #222 := (or #240 #243 #150)
  1382 #558 := [def-axiom]: #222
  1383 #541 := [unit-resolution #558 #557]: #199
  1384 #203 := [unit-resolution #541 #227]: #150
  1385 #241 := (not #150)
  1386 #562 := (not #151)
  1387 #204 := (or #562 #241)
  1388 #563 := (or #562 #23 #241)
  1389 #564 := [def-axiom]: #563
  1390 #205 := [unit-resolution #564 #215]: #204
  1391 #206 := [unit-resolution #205 #203 #237]: false
  1392 #543 := [lemma #206]: #23
  1393 #579 := (or #574 #55)
  1394 #580 := (iff #82 #579)
  1395 #577 := (iff #79 #574)
  1396 #575 := (iff #76 #76)
  1397 #576 := [refl]: #575
  1398 #578 := [quant-intro #576]: #577
  1399 #581 := [monotonicity #578]: #580
  1400 #91 := [and-elim #87]: #82
  1401 #582 := [mp #91 #581]: #579
  1402 #242 := [unit-resolution #582 #543]: #574
  1403 #555 := (not #574)
  1404 #214 := (or #555 #55)
  1405 #219 := [quant-inst #21]: #214
  1406 [unit-resolution #219 #543 #242]: false
  1407 unsat
  1408 fdf61e060f49731790f4d6c8f9b26c21349c60b3 117 0
  1409 #2 := false
  1410 decl f1 :: S1
  1411 #3 := f1
  1412 decl f7 :: S1
  1413 #25 := f7
  1414 #206 := (= f7 f1)
  1415 decl f3 :: (-> S3 S2 S1)
  1416 decl f6 :: S2
  1417 #20 := f6
  1418 decl f4 :: (-> S4 S1 S3)
  1419 decl f5 :: S4
  1420 #7 := f5
  1421 #26 := (f4 f5 f7)
  1422 #30 := (f3 #26 f6)
  1423 #31 := (= #30 f1)
  1424 #292 := (iff #31 #206)
  1425 #10 := (:var 0 S2)
  1426 #8 := (:var 1 S1)
  1427 #9 := (f4 f5 #8)
  1428 #11 := (f3 #9 #10)
  1429 #622 := (pattern #11)
  1430 #13 := (= #8 f1)
  1431 #12 := (= #11 f1)
  1432 #14 := (iff #12 #13)
  1433 #623 := (forall (vars (?v0 S1) (?v1 S2)) (:pat #622) #14)
  1434 #15 := (forall (vars (?v0 S1) (?v1 S2)) #14)
  1435 #626 := (iff #15 #623)
  1436 #624 := (iff #14 #14)
  1437 #625 := [refl]: #624
  1438 #627 := [quant-intro #625]: #626
  1439 #73 := (~ #15 #15)
  1440 #71 := (~ #14 #14)
  1441 #72 := [refl]: #71
  1442 #74 := [nnf-pos #72]: #73
  1443 #54 := [asserted]: #15
  1444 #62 := [mp~ #54 #74]: #15
  1445 #628 := [mp #62 #627]: #623
  1446 #295 := (not #623)
  1447 #611 := (or #295 #292)
  1448 #270 := [quant-inst #25 #20]: #611
  1449 #297 := [unit-resolution #270 #628]: #292
  1450 decl ?v0!3 :: S2
  1451 #120 := ?v0!3
  1452 #123 := (f3 #26 ?v0!3)
  1453 #124 := (= #123 f1)
  1454 #296 := (iff #124 #206)
  1455 #299 := (or #295 #296)
  1456 #278 := [quant-inst #25 #120]: #299
  1457 #298 := [unit-resolution #278 #628]: #296
  1458 #614 := (not #296)
  1459 #599 := (or #614 #206)
  1460 #108 := (not #31)
  1461 #27 := (f3 #26 #10)
  1462 #654 := (pattern #27)
  1463 #28 := (= #27 f1)
  1464 #132 := (not #28)
  1465 #655 := (forall (vars (?v0 S2)) (:pat #654) #132)
  1466 #207 := [hypothesis]: #31
  1467 #660 := (or #655 #108)
  1468 #135 := (forall (vars (?v0 S2)) #132)
  1469 #138 := (or #135 #108)
  1470 #661 := (iff #138 #660)
  1471 #658 := (iff #135 #655)
  1472 #656 := (iff #132 #132)
  1473 #657 := [refl]: #656
  1474 #659 := [quant-intro #657]: #658
  1475 #662 := [monotonicity #659]: #661
  1476 #139 := (or #124 #31)
  1477 #140 := (and #139 #138)
  1478 #29 := (exists (vars (?v0 S2)) #28)
  1479 #57 := (not #29)
  1480 #58 := (iff #57 #31)
  1481 #141 := (~ #58 #140)
  1482 #81 := (~ #31 #31)
  1483 #119 := [refl]: #81
  1484 #109 := (~ #108 #108)
  1485 #80 := [refl]: #109
  1486 #136 := (~ #57 #135)
  1487 #133 := (~ #132 #132)
  1488 #134 := [refl]: #133
  1489 #137 := [nnf-neg #134]: #136
  1490 #129 := (not #57)
  1491 #130 := (~ #129 #124)
  1492 #125 := (~ #29 #124)
  1493 #126 := [sk]: #125
  1494 #131 := [nnf-neg #126]: #130
  1495 #142 := [nnf-pos #131 #137 #80 #119]: #141
  1496 #32 := (iff #29 #31)
  1497 #33 := (not #32)
  1498 #59 := (iff #33 #58)
  1499 #60 := [rewrite]: #59
  1500 #56 := [asserted]: #33
  1501 #63 := [mp #56 #60]: #58
  1502 #143 := [mp~ #63 #142]: #140
  1503 #147 := [and-elim #143]: #138
  1504 #663 := [mp #147 #662]: #660
  1505 #293 := [unit-resolution #663 #207]: #655
  1506 #610 := (not #655)
  1507 #283 := (or #610 #108)
  1508 #284 := [quant-inst #20]: #283
  1509 #617 := [unit-resolution #284 #207 #293]: false
  1510 #618 := [lemma #617]: #108
  1511 #146 := [and-elim #143]: #139
  1512 #262 := [unit-resolution #146 #618]: #124
  1513 #208 := (not #124)
  1514 #294 := (or #614 #208 #206)
  1515 #285 := [def-axiom]: #294
  1516 #600 := [unit-resolution #285 #262]: #599
  1517 #601 := [unit-resolution #600 #298]: #206
  1518 #616 := (not #206)
  1519 #275 := (not #292)
  1520 #602 := (or #275 #616)
  1521 #612 := (or #275 #31 #616)
  1522 #271 := [def-axiom]: #612
  1523 #603 := [unit-resolution #271 #618]: #602
  1524 [unit-resolution #603 #601 #297]: false
  1525 unsat
  1526 43550507f510d81bc4fb9ef8c1fd14424eaa9070 37 0
  1527 #2 := false
  1528 #10 := 0::Int
  1529 decl f3 :: Int
  1530 #7 := f3
  1531 #12 := (<= f3 0::Int)
  1532 #54 := (not #12)
  1533 decl f4 :: Int
  1534 #8 := f4
  1535 #13 := (<= f4 0::Int)
  1536 #9 := (* f3 f4)
  1537 #11 := (<= #9 0::Int)
  1538 #37 := (not #11)
  1539 #44 := (or #37 #12 #13)
  1540 #47 := (not #44)
  1541 #14 := (or #12 #13)
  1542 #15 := (implies #11 #14)
  1543 #16 := (not #15)
  1544 #50 := (iff #16 #47)
  1545 #38 := (or #37 #14)
  1546 #41 := (not #38)
  1547 #48 := (iff #41 #47)
  1548 #45 := (iff #38 #44)
  1549 #46 := [rewrite]: #45
  1550 #49 := [monotonicity #46]: #48
  1551 #42 := (iff #16 #41)
  1552 #39 := (iff #15 #38)
  1553 #40 := [rewrite]: #39
  1554 #43 := [monotonicity #40]: #42
  1555 #51 := [trans #43 #49]: #50
  1556 #36 := [asserted]: #16
  1557 #52 := [mp #36 #51]: #47
  1558 #55 := [not-or-elim #52]: #54
  1559 #56 := (not #13)
  1560 #57 := [not-or-elim #52]: #56
  1561 #53 := [not-or-elim #52]: #11
  1562 [th-lemma arith farkas 1 1 1 #53 #57 #55]: false
  1563 unsat
  1564 76d09b53549e91e8b6b69b6b905b5e8307464c6f 106 0
  1565 #2 := false
  1566 decl f7 :: S2
  1567 #19 := f7
  1568 decl f3 :: (-> S3 S2 S2)
  1569 decl f4 :: S3
  1570 #7 := f4
  1571 #20 := (f3 f4 f7)
  1572 #21 := (= #20 f7)
  1573 #74 := (not #21)
  1574 decl f1 :: S1
  1575 #3 := f1
  1576 decl f5 :: (-> S4 S1 S1)
  1577 decl f6 :: S4
  1578 #12 := f6
  1579 #22 := (f5 f6 f1)
  1580 #23 := (= #22 f1)
  1581 #75 := (not #23)
  1582 #558 := [hypothesis]: #75
  1583 #13 := (:var 0 S1)
  1584 #14 := (f5 f6 #13)
  1585 #569 := (pattern #14)
  1586 #16 := (= #13 f1)
  1587 #15 := (= #14 f1)
  1588 #17 := (iff #15 #16)
  1589 #570 := (forall (vars (?v0 S1)) (:pat #569) #17)
  1590 #18 := (forall (vars (?v0 S1)) #17)
  1591 #573 := (iff #18 #570)
  1592 #571 := (iff #17 #17)
  1593 #572 := [refl]: #571
  1594 #574 := [quant-intro #572]: #573
  1595 #62 := (~ #18 #18)
  1596 #61 := (~ #17 #17)
  1597 #72 := [refl]: #61
  1598 #63 := [nnf-pos #72]: #62
  1599 #48 := [asserted]: #18
  1600 #73 := [mp~ #48 #63]: #18
  1601 #575 := [mp #73 #574]: #570
  1602 #239 := (not #570)
  1603 #218 := (or #239 #23)
  1604 #146 := (= f1 f1)
  1605 #147 := (iff #23 #146)
  1606 #554 := (or #239 #147)
  1607 #212 := (iff #554 #218)
  1608 #550 := (iff #218 #218)
  1609 #223 := [rewrite]: #550
  1610 #238 := (iff #147 #23)
  1611 #1 := true
  1612 #24 := (iff #23 true)
  1613 #50 := (iff #24 #23)
  1614 #51 := [rewrite]: #50
  1615 #236 := (iff #147 #24)
  1616 #232 := (iff #146 true)
  1617 #225 := [rewrite]: #232
  1618 #237 := [monotonicity #225]: #236
  1619 #235 := [trans #237 #51]: #238
  1620 #343 := [monotonicity #235]: #212
  1621 #224 := [trans #343 #223]: #212
  1622 #556 := [quant-inst #3]: #554
  1623 #557 := [mp #556 #224]: #218
  1624 #559 := [unit-resolution #557 #575 #558]: false
  1625 #560 := [lemma #559]: #23
  1626 #64 := (or #74 #75)
  1627 #52 := (and #21 #23)
  1628 #55 := (not #52)
  1629 #81 := (iff #55 #64)
  1630 #65 := (not #64)
  1631 #76 := (not #65)
  1632 #79 := (iff #76 #64)
  1633 #80 := [rewrite]: #79
  1634 #77 := (iff #55 #76)
  1635 #66 := (iff #52 #65)
  1636 #67 := [rewrite]: #66
  1637 #78 := [monotonicity #67]: #77
  1638 #82 := [trans #78 #80]: #81
  1639 #25 := (and #21 #24)
  1640 #26 := (not #25)
  1641 #56 := (iff #26 #55)
  1642 #53 := (iff #25 #52)
  1643 #54 := [monotonicity #51]: #53
  1644 #57 := [monotonicity #54]: #56
  1645 #49 := [asserted]: #26
  1646 #60 := [mp #49 #57]: #55
  1647 #83 := [mp #60 #82]: #64
  1648 #555 := [unit-resolution #83 #560]: #74
  1649 #8 := (:var 0 S2)
  1650 #9 := (f3 f4 #8)
  1651 #562 := (pattern #9)
  1652 #10 := (= #9 #8)
  1653 #563 := (forall (vars (?v0 S2)) (:pat #562) #10)
  1654 #11 := (forall (vars (?v0 S2)) #10)
  1655 #566 := (iff #11 #563)
  1656 #564 := (iff #10 #10)
  1657 #565 := [refl]: #564
  1658 #567 := [quant-intro #565]: #566
  1659 #70 := (~ #11 #11)
  1660 #68 := (~ #10 #10)
  1661 #69 := [refl]: #68
  1662 #71 := [nnf-pos #69]: #70
  1663 #47 := [asserted]: #11
  1664 #59 := [mp~ #47 #71]: #11
  1665 #568 := [mp #59 #567]: #563
  1666 #551 := (not #563)
  1667 #210 := (or #551 #21)
  1668 #215 := [quant-inst #19]: #210
  1669 [unit-resolution #215 #568 #555]: false
  1670 unsat
  1671 d9c8c0d6c38991be073d0ed9988535642e4f47a6 396 0
  1672 #2 := false
  1673 decl f12 :: (-> S9 S10 S4)
  1674 decl f14 :: (-> S1 S10)
  1675 decl f1 :: S1
  1676 #3 := f1
  1677 #120 := (f14 f1)
  1678 decl f13 :: S9
  1679 #19 := f13
  1680 #121 := (f12 f13 #120)
  1681 decl f3 :: (-> S2 S3 S4)
  1682 decl f5 :: (-> Int S3)
  1683 #117 := 3::Int
  1684 #118 := (f5 3::Int)
  1685 decl f4 :: S2
  1686 #7 := f4
  1687 #119 := (f3 f4 #118)
  1688 #122 := (= #119 #121)
  1689 decl f15 :: (-> S11 S12 S4)
  1690 decl f17 :: (-> S13 S12 S12)
  1691 decl f20 :: S12
  1692 #26 := f20
  1693 decl f18 :: (-> S14 S1 S13)
  1694 decl f19 :: S14
  1695 #24 := f19
  1696 #513 := (f18 f19 f1)
  1697 #514 := (f17 #513 f20)
  1698 decl f16 :: S11
  1699 #23 := f16
  1700 #495 := (f15 f16 #514)
  1701 #626 := (= #495 #121)
  1702 #831 := (= #121 #495)
  1703 #20 := (:var 0 S1)
  1704 #25 := (f18 f19 #20)
  1705 #848 := (pattern #25)
  1706 #21 := (f14 #20)
  1707 #847 := (pattern #21)
  1708 #27 := (f17 #25 f20)
  1709 #28 := (f15 f16 #27)
  1710 #22 := (f12 f13 #21)
  1711 #29 := (= #22 #28)
  1712 #849 := (forall (vars (?v0 S1)) (:pat #847 #848) #29)
  1713 #30 := (forall (vars (?v0 S1)) #29)
  1714 #852 := (iff #30 #849)
  1715 #850 := (iff #29 #29)
  1716 #851 := [refl]: #850
  1717 #853 := [quant-intro #851]: #852
  1718 #302 := (~ #30 #30)
  1719 #301 := (~ #29 #29)
  1720 #346 := [refl]: #301
  1721 #303 := [nnf-pos #346]: #302
  1722 #159 := [asserted]: #30
  1723 #347 := [mp~ #159 #303]: #30
  1724 #854 := [mp #347 #853]: #849
  1725 #620 := (not #849)
  1726 #827 := (or #620 #831)
  1727 #500 := [quant-inst #3]: #827
  1728 #646 := [unit-resolution #500 #854]: #831
  1729 #627 := [symm #646]: #626
  1730 #636 := (= #119 #495)
  1731 decl f23 :: S11
  1732 #43 := f23
  1733 #524 := (f15 f23 #514)
  1734 #617 := (= #524 #495)
  1735 #802 := (= #495 #524)
  1736 #41 := (:var 0 S12)
  1737 #44 := (f15 f23 #41)
  1738 #856 := (pattern #44)
  1739 #42 := (f15 f16 #41)
  1740 #855 := (pattern #42)
  1741 #45 := (= #42 #44)
  1742 #857 := (forall (vars (?v0 S12)) (:pat #855 #856) #45)
  1743 #46 := (forall (vars (?v0 S12)) #45)
  1744 #860 := (iff #46 #857)
  1745 #858 := (iff #45 #45)
  1746 #859 := [refl]: #858
  1747 #861 := [quant-intro #859]: #860
  1748 #304 := (~ #46 #46)
  1749 #348 := (~ #45 #45)
  1750 #349 := [refl]: #348
  1751 #305 := [nnf-pos #349]: #304
  1752 #164 := [asserted]: #46
  1753 #312 := [mp~ #164 #305]: #46
  1754 #862 := [mp #312 #861]: #857
  1755 #834 := (not #857)
  1756 #805 := (or #834 #802)
  1757 #794 := [quant-inst #514]: #805
  1758 #645 := [unit-resolution #794 #862]: #802
  1759 #624 := [symm #645]: #617
  1760 #635 := (= #119 #524)
  1761 decl f27 :: (-> S17 Int S4)
  1762 decl f31 :: (-> S19 S4 Int)
  1763 #101 := (f15 f23 f20)
  1764 decl f32 :: S19
  1765 #74 := f32
  1766 #804 := (f31 f32 #101)
  1767 #80 := 1::Int
  1768 #801 := (+ 1::Int #804)
  1769 decl f28 :: S17
  1770 #57 := f28
  1771 #795 := (f27 f28 #801)
  1772 #655 := (= #795 #524)
  1773 #796 := (= #524 #795)
  1774 #70 := (:var 1 S1)
  1775 #71 := (f18 f19 #70)
  1776 #72 := (f17 #71 #41)
  1777 #899 := (pattern #72)
  1778 #106 := (f31 f32 #44)
  1779 #214 := (+ 1::Int #106)
  1780 #219 := (f27 f28 #214)
  1781 #105 := (f15 f23 #72)
  1782 #222 := (= #105 #219)
  1783 #900 := (forall (vars (?v0 S1) (?v1 S12)) (:pat #899) #222)
  1784 #225 := (forall (vars (?v0 S1) (?v1 S12)) #222)
  1785 #903 := (iff #225 #900)
  1786 #901 := (iff #222 #222)
  1787 #902 := [refl]: #901
  1788 #904 := [quant-intro #902]: #903
  1789 #324 := (~ #225 #225)
  1790 #358 := (~ #222 #222)
  1791 #359 := [refl]: #358
  1792 #325 := [nnf-pos #359]: #324
  1793 #58 := 0::Int
  1794 #81 := (+ 0::Int 1::Int)
  1795 #107 := (+ #106 #81)
  1796 #108 := (f27 f28 #107)
  1797 #109 := (= #105 #108)
  1798 #110 := (forall (vars (?v0 S1) (?v1 S12)) #109)
  1799 #226 := (iff #110 #225)
  1800 #223 := (iff #109 #222)
  1801 #220 := (= #108 #219)
  1802 #217 := (= #107 #214)
  1803 #211 := (+ #106 1::Int)
  1804 #215 := (= #211 #214)
  1805 #216 := [rewrite]: #215
  1806 #212 := (= #107 #211)
  1807 #169 := (= #81 1::Int)
  1808 #170 := [rewrite]: #169
  1809 #213 := [monotonicity #170]: #212
  1810 #218 := [trans #213 #216]: #217
  1811 #221 := [monotonicity #218]: #220
  1812 #224 := [monotonicity #221]: #223
  1813 #227 := [quant-intro #224]: #226
  1814 #210 := [asserted]: #110
  1815 #230 := [mp #210 #227]: #225
  1816 #328 := [mp~ #230 #325]: #225
  1817 #905 := [mp #328 #904]: #900
  1818 #797 := (not #900)
  1819 #798 := (or #797 #796)
  1820 #793 := [quant-inst #3 #26]: #798
  1821 #644 := [unit-resolution #793 #905]: #796
  1822 #616 := [symm #644]: #655
  1823 #633 := (= #119 #795)
  1824 decl f6 :: (-> S5 S6 S4)
  1825 decl f11 :: S6
  1826 #14 := f11
  1827 decl f24 :: S5
  1828 #49 := f24
  1829 #103 := (f6 f24 f11)
  1830 #810 := (f31 f32 #103)
  1831 #807 := (+ 1::Int #810)
  1832 #522 := (f27 f28 #807)
  1833 #654 := (= #522 #795)
  1834 #648 := (= #795 #522)
  1835 #638 := (= #801 #807)
  1836 #682 := (= 1::Int #807)
  1837 #689 := (= #807 1::Int)
  1838 #792 := (<= #810 0::Int)
  1839 #791 := (= #810 0::Int)
  1840 #59 := (f27 f28 0::Int)
  1841 #487 := (f31 f32 #59)
  1842 #492 := (= #487 0::Int)
  1843 #8 := (:var 0 Int)
  1844 #130 := (f27 f28 #8)
  1845 #920 := (pattern #130)
  1846 #131 := (f31 f32 #130)
  1847 #132 := (= #131 #8)
  1848 #260 := (>= #8 0::Int)
  1849 #261 := (not #260)
  1850 #264 := (or #261 #132)
  1851 #921 := (forall (vars (?v0 Int)) (:pat #920) #264)
  1852 #267 := (forall (vars (?v0 Int)) #264)
  1853 #924 := (iff #267 #921)
  1854 #922 := (iff #264 #264)
  1855 #923 := [refl]: #922
  1856 #925 := [quant-intro #923]: #924
  1857 #336 := (~ #267 #267)
  1858 #335 := (~ #264 #264)
  1859 #362 := [refl]: #335
  1860 #337 := [nnf-pos #362]: #336
  1861 #129 := (<= 0::Int #8)
  1862 #133 := (implies #129 #132)
  1863 #134 := (forall (vars (?v0 Int)) #133)
  1864 #270 := (iff #134 #267)
  1865 #251 := (not #129)
  1866 #252 := (or #251 #132)
  1867 #255 := (forall (vars (?v0 Int)) #252)
  1868 #268 := (iff #255 #267)
  1869 #265 := (iff #252 #264)
  1870 #262 := (iff #251 #261)
  1871 #258 := (iff #129 #260)
  1872 #259 := [rewrite]: #258
  1873 #263 := [monotonicity #259]: #262
  1874 #266 := [monotonicity #263]: #265
  1875 #269 := [quant-intro #266]: #268
  1876 #256 := (iff #134 #255)
  1877 #253 := (iff #133 #252)
  1878 #254 := [rewrite]: #253
  1879 #257 := [quant-intro #254]: #256
  1880 #271 := [trans #257 #269]: #270
  1881 #250 := [asserted]: #134
  1882 #272 := [mp #250 #271]: #267
  1883 #363 := [mp~ #272 #337]: #267
  1884 #926 := [mp #363 #925]: #921
  1885 #822 := (not #921)
  1886 #824 := (or #822 #492)
  1887 #501 := (>= 0::Int 0::Int)
  1888 #837 := (not #501)
  1889 #829 := (or #837 #492)
  1890 #463 := (or #822 #829)
  1891 #825 := (iff #463 #824)
  1892 #826 := (iff #824 #824)
  1893 #812 := [rewrite]: #826
  1894 #821 := (iff #829 #492)
  1895 #817 := (or false #492)
  1896 #820 := (iff #817 #492)
  1897 #815 := [rewrite]: #820
  1898 #818 := (iff #829 #817)
  1899 #479 := (iff #837 false)
  1900 #1 := true
  1901 #472 := (not true)
  1902 #477 := (iff #472 false)
  1903 #478 := [rewrite]: #477
  1904 #814 := (iff #837 #472)
  1905 #488 := (iff #501 true)
  1906 #830 := [rewrite]: #488
  1907 #476 := [monotonicity #830]: #814
  1908 #816 := [trans #476 #478]: #479
  1909 #819 := [monotonicity #816]: #818
  1910 #458 := [trans #819 #815]: #821
  1911 #823 := [monotonicity #458]: #825
  1912 #813 := [trans #823 #812]: #825
  1913 #464 := [quant-inst #58]: #463
  1914 #520 := [mp #464 #813]: #824
  1915 #696 := [unit-resolution #520 #926]: #492
  1916 #697 := (= #810 #487)
  1917 #104 := (= #103 #59)
  1918 #208 := [asserted]: #104
  1919 #700 := [monotonicity #208]: #697
  1920 #701 := [trans #700 #696]: #791
  1921 #702 := (not #791)
  1922 #698 := (or #702 #792)
  1923 #703 := [th-lemma arith triangle-eq]: #698
  1924 #683 := [unit-resolution #703 #701]: #792
  1925 #799 := (>= #810 0::Int)
  1926 #629 := (or #702 #799)
  1927 #684 := [th-lemma arith triangle-eq]: #629
  1928 #665 := [unit-resolution #684 #701]: #799
  1929 #690 := [th-lemma arith eq-propagate -1 -1 #665 #683]: #689
  1930 #637 := [symm #690]: #682
  1931 #681 := (= #801 1::Int)
  1932 #641 := (<= #804 0::Int)
  1933 #640 := (= #804 0::Int)
  1934 #659 := (= #804 #487)
  1935 #102 := (= #101 #59)
  1936 #207 := [asserted]: #102
  1937 #666 := [monotonicity #207]: #659
  1938 #625 := [trans #666 #696]: #640
  1939 #656 := (not #640)
  1940 #658 := (or #656 #641)
  1941 #660 := [th-lemma arith triangle-eq]: #658
  1942 #667 := [unit-resolution #660 #625]: #641
  1943 #642 := (>= #804 0::Int)
  1944 #669 := (or #656 #642)
  1945 #670 := [th-lemma arith triangle-eq]: #669
  1946 #671 := [unit-resolution #670 #625]: #642
  1947 #661 := [th-lemma arith eq-propagate -1 -1 #671 #667]: #681
  1948 #643 := [trans #661 #637]: #638
  1949 #649 := [monotonicity #643]: #648
  1950 #639 := [symm #649]: #654
  1951 #631 := (= #119 #522)
  1952 decl f8 :: (-> S7 S6 S6)
  1953 decl f9 :: (-> S8 Int S7)
  1954 decl f10 :: S8
  1955 #12 := f10
  1956 #509 := (f9 f10 3::Int)
  1957 #510 := (f8 #509 f11)
  1958 #532 := (f6 f24 #510)
  1959 #523 := (= #532 #522)
  1960 #47 := (:var 0 S6)
  1961 #88 := (:var 1 Int)
  1962 #89 := (f9 f10 #88)
  1963 #90 := (f8 #89 #47)
  1964 #906 := (pattern #90)
  1965 #50 := (f6 f24 #47)
  1966 #112 := (f31 f32 #50)
  1967 #233 := (+ 1::Int #112)
  1968 #238 := (f27 f28 #233)
  1969 #111 := (f6 f24 #90)
  1970 #241 := (= #111 #238)
  1971 #907 := (forall (vars (?v0 Int) (?v1 S6)) (:pat #906) #241)
  1972 #244 := (forall (vars (?v0 Int) (?v1 S6)) #241)
  1973 #910 := (iff #244 #907)
  1974 #908 := (iff #241 #241)
  1975 #909 := [refl]: #908
  1976 #911 := [quant-intro #909]: #910
  1977 #330 := (~ #244 #244)
  1978 #329 := (~ #241 #241)
  1979 #326 := [refl]: #329
  1980 #331 := [nnf-pos #326]: #330
  1981 #113 := (+ #112 #81)
  1982 #114 := (f27 f28 #113)
  1983 #115 := (= #111 #114)
  1984 #116 := (forall (vars (?v0 Int) (?v1 S6)) #115)
  1985 #245 := (iff #116 #244)
  1986 #242 := (iff #115 #241)
  1987 #239 := (= #114 #238)
  1988 #236 := (= #113 #233)
  1989 #229 := (+ #112 1::Int)
  1990 #234 := (= #229 #233)
  1991 #235 := [rewrite]: #234
  1992 #231 := (= #113 #229)
  1993 #232 := [monotonicity #170]: #231
  1994 #237 := [trans #232 #235]: #236
  1995 #240 := [monotonicity #237]: #239
  1996 #243 := [monotonicity #240]: #242
  1997 #246 := [quant-intro #243]: #245
  1998 #228 := [asserted]: #116
  1999 #249 := [mp #228 #246]: #244
  2000 #327 := [mp~ #249 #331]: #244
  2001 #912 := [mp #327 #911]: #907
  2002 #803 := (not #907)
  2003 #517 := (or #803 #523)
  2004 #800 := [quant-inst #117 #14]: #517
  2005 #694 := [unit-resolution #800 #912]: #523
  2006 #628 := (= #119 #532)
  2007 decl f7 :: S5
  2008 #11 := f7
  2009 #511 := (f6 f7 #510)
  2010 #806 := (= #511 #532)
  2011 #864 := (pattern #50)
  2012 #48 := (f6 f7 #47)
  2013 #863 := (pattern #48)
  2014 #51 := (= #48 #50)
  2015 #865 := (forall (vars (?v0 S6)) (:pat #863 #864) #51)
  2016 #52 := (forall (vars (?v0 S6)) #51)
  2017 #868 := (iff #52 #865)
  2018 #866 := (iff #51 #51)
  2019 #867 := [refl]: #866
  2020 #869 := [quant-intro #867]: #868
  2021 #314 := (~ #52 #52)
  2022 #313 := (~ #51 #51)
  2023 #310 := [refl]: #313
  2024 #315 := [nnf-pos #310]: #314
  2025 #165 := [asserted]: #52
  2026 #311 := [mp~ #165 #315]: #52
  2027 #870 := [mp #311 #869]: #865
  2028 #832 := (not #865)
  2029 #811 := (or #832 #806)
  2030 #521 := [quant-inst #510]: #811
  2031 #693 := [unit-resolution #521 #870]: #806
  2032 #502 := (= #119 #511)
  2033 #13 := (f9 f10 #8)
  2034 #840 := (pattern #13)
  2035 #9 := (f5 #8)
  2036 #839 := (pattern #9)
  2037 #15 := (f8 #13 f11)
  2038 #16 := (f6 f7 #15)
  2039 #10 := (f3 f4 #9)
  2040 #17 := (= #10 #16)
  2041 #841 := (forall (vars (?v0 Int)) (:pat #839 #840) #17)
  2042 #18 := (forall (vars (?v0 Int)) #17)
  2043 #844 := (iff #18 #841)
  2044 #842 := (iff #17 #17)
  2045 #843 := [refl]: #842
  2046 #845 := [quant-intro #843]: #844
  2047 #344 := (~ #18 #18)
  2048 #342 := (~ #17 #17)
  2049 #343 := [refl]: #342
  2050 #345 := [nnf-pos #343]: #344
  2051 #158 := [asserted]: #18
  2052 #300 := [mp~ #158 #345]: #18
  2053 #846 := [mp #300 #845]: #841
  2054 #515 := (not #841)
  2055 #512 := (or #515 #502)
  2056 #516 := [quant-inst #117]: #512
  2057 #647 := [unit-resolution #516 #846]: #502
  2058 #630 := [trans #647 #693]: #628
  2059 #632 := [trans #630 #694]: #631
  2060 #634 := [trans #632 #639]: #633
  2061 #618 := [trans #634 #616]: #635
  2062 #606 := [trans #618 #624]: #636
  2063 #607 := [trans #606 #627]: #122
  2064 #123 := (not #122)
  2065 #247 := [asserted]: #123
  2066 [unit-resolution #247 #607]: false
  2067 unsat