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