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