src/HOL/SMT_Examples/SMT_Examples.certs

use 'smt2' in SMT examples as much as currently possible

d97439af6f5bc7794ab403d0f6cc318d103016a1 1288 0
#2 := false
decl f1 :: S1
#3 := f1
decl f9 :: S1
#25 := f9
#26 := (= f9 f1)
decl f20 :: S1
#59 := f20
#60 := (= f20 f1)
decl f21 :: S1
#61 := f21
#62 := (= f21 f1)
#249 := (not #62)
decl f31 :: S1
#97 := f31
#98 := (= f31 f1)
decl f62 :: S1
#207 := f62
#208 := (= f62 f1)
decl f58 :: S1
#189 := f58
#190 := (= f58 f1)
#388 := (not #190)
decl f47 :: S1
#151 := f47
#152 := (= f47 f1)
#289 := (not #98)
#980 := [hypothesis]: #289
decl f46 :: S1
#149 := f46
#150 := (= f46 f1)
#346 := (not #150)
decl f48 :: S1
#156 := f48
#157 := (= f48 f1)
decl f57 :: S1
#187 := f57
#188 := (= f57 f1)
#387 := (not #188)
decl f45 :: S1
#144 := f45
#145 := (= f45 f1)
#339 := (not #145)
decl f42 :: S1
#135 := f42
#136 := (= f42 f1)
#1467 := (or #136 #98)
decl f40 :: S1
#128 := f40
#129 := (= f40 f1)
#330 := (not #136)
#1095 := [hypothesis]: #330
decl f32 :: S1
#99 := f32
#100 := (= f32 f1)
#290 := (not #100)
decl f16 :: S1
#46 := f16
#47 := (= f16 f1)
decl f17 :: S1
#48 := f17
#49 := (= f17 f1)
#236 := (not #49)
decl f28 :: S1
#86 := f28
#87 := (= f28 f1)
#1450 := (or #87 #98 #136)
decl f29 :: S1
#90 := f29
#91 := (= f29 f1)
#281 := (not #91)
#322 := (not #129)
#277 := (not #87)
#867 := [hypothesis]: #277
#1427 := (or #322 #87)
decl f51 :: S1
#166 := f51
#167 := (= f51 f1)
#363 := (not #167)
decl f54 :: S1
#175 := f54
#176 := (= f54 f1)
decl f56 :: S1
#182 := f56
#183 := (= f56 f1)
#380 := (not #183)
#372 := (not #176)
#1160 := [hypothesis]: #372
#1189 := (or #388 #176)
decl f18 :: S1
#52 := f18
#53 := (= f18 f1)
decl f33 :: S1
#104 := f33
#105 := (= f33 f1)
#297 := (not #105)
decl f36 :: S1
#113 := f36
#114 := (= f36 f1)
#347 := (not #152)
#1155 := [hypothesis]: #190
#393 := (or #388 #347)
#730 := [asserted]: #393
#1156 := [unit-resolution #730 #1155]: #347
#389 := (or #387 #388)
#726 := [asserted]: #389
#1157 := [unit-resolution #726 #1155]: #387
#194 := (or #188 #157)
decl f6 :: S1
#16 := f6
#17 := (= f6 f1)
#579 := (or #17 #188 #157)
#840 := (iff #579 #194)
#835 := (or false #188 #157)
#838 := (iff #835 #194)
#839 := [rewrite]: #838
#836 := (iff #579 #835)
#759 := (iff #17 false)
#18 := (not #17)
#439 := [asserted]: #18
#760 := [iff-false #439]: #759
#837 := [monotonicity #760]: #836
#841 := [trans #837 #839]: #840
#195 := (or #17 #194)
#580 := (iff #195 #579)
#581 := [rewrite]: #580
#568 := [asserted]: #195
#582 := [mp #568 #581]: #579
#842 := [mp #582 #841]: #194
#1158 := [unit-resolution #842 #1157]: #157
#354 := (not #157)
#355 := (or #354 #346)
#702 := [asserted]: #355
#1159 := [unit-resolution #702 #1158]: #346
decl f44 :: S1
#142 := f44
#143 := (= f44 f1)
#338 := (not #143)
decl f61 :: S1
#203 := f61
#204 := (= f61 f1)
decl f60 :: S1
#199 := f60
#200 := (= f60 f1)
#400 := (not #200)
decl f37 :: S1
#118 := f37
#119 := (= f37 f1)
#313 := (not #119)
#356 := (or #354 #313)
#703 := [asserted]: #356
#1161 := [unit-resolution #703 #1158]: #313
#983 := (or #400 #150 #152 #119)
#248 := (not #60)
decl f23 :: S1
#68 := f23
#69 := (= f23 f1)
decl f34 :: S1
#106 := f34
#107 := (= f34 f1)
#298 := (not #107)
#1051 := [hypothesis]: #347
#1052 := [hypothesis]: #346
#306 := (not #114)
decl f25 :: S1
#75 := f25
#76 := (= f25 f1)
decl f39 :: S1
#124 := f39
#125 := (= f39 f1)
#318 := (not #125)
decl f50 :: S1
#162 := f50
#163 := (= f50 f1)
decl f59 :: S1
#196 := f59
#197 := (= f59 f1)
#398 := (not #197)
#1024 := [hypothesis]: #200
#401 := (or #400 #398)
#736 := [asserted]: #401
#1021 := [unit-resolution #736 #1024]: #398
#198 := (or #197 #163)
#573 := [asserted]: #198
#1022 := [unit-resolution #573 #1021]: #163
#359 := (not #163)
#362 := (or #359 #318)
#707 := [asserted]: #362
#1019 := [unit-resolution #707 #1022]: #318
decl f26 :: S1
#80 := f26
#81 := (= f26 f1)
#1153 := [hypothesis]: #313
decl f35 :: S1
#111 := f35
#112 := (= f35 f1)
#305 := (not #112)
decl f43 :: S1
#137 := f43
#138 := (= f43 f1)
#331 := (not #138)
decl f52 :: S1
#168 := f52
#169 := (= f52 f1)
#364 := (not #169)
#402 := (or #400 #364)
#737 := [asserted]: #402
#1020 := [unit-resolution #737 #1024]: #364
decl f49 :: S1
#160 := f49
#161 := (= f49 f1)
#358 := (not #161)
#360 := (or #358 #359)
#705 := [asserted]: #360
#1017 := [unit-resolution #705 #1022]: #358
decl f41 :: S1
#130 := f41
#131 := (= f41 f1)
#323 := (not #131)
#1126 := (or #323 #119 #125)
#272 := (not #81)
decl f15 :: S1
#43 := f15
#44 := (= f15 f1)
decl f13 :: S1
#37 := f13
#38 := (= f13 f1)
#228 := (not #38)
decl f11 :: S1
#31 := f11
#32 := (= f11 f1)
#218 := (not #26)
decl f7 :: S1
#19 := f7
#20 := (= f7 f1)
decl f8 :: S1
#21 := f8
#22 := (= f8 f1)
#214 := (not #22)
#1154 := [hypothesis]: #318
decl f38 :: S1
#122 := f38
#123 := (= f38 f1)
#317 := (not #123)
#1151 := [hypothesis]: #131
#327 := (or #323 #317)
#681 := [asserted]: #327
#1152 := [unit-resolution #681 #1151]: #317
#524 := (or #123 #125 #87)
#126 := (or #125 #87)
#127 := (or #123 #126)
#525 := (iff #127 #524)
#526 := [rewrite]: #525
#513 := [asserted]: #127
#527 := [mp #513 #526]: #524
#1149 := [unit-resolution #527 #1152 #1154]: #87
#280 := (or #277 #236)
#647 := [asserted]: #280
#1150 := [unit-resolution #647 #1149]: #236
#783 := (or #47 #49)
decl f4 :: S1
#10 := f4
#11 := (= f4 f1)
#464 := (or #47 #49 #11)
#786 := (iff #464 #783)
#780 := (or #47 #49 false)
#784 := (iff #780 #783)
#785 := [rewrite]: #784
#781 := (iff #464 #780)
#755 := (iff #11 false)
#12 := (not #11)
#437 := [asserted]: #12
#756 := [iff-false #437]: #755
#782 := [monotonicity #756]: #781
#787 := [trans #782 #785]: #786
#50 := (or #49 #11)
#51 := (or #47 #50)
#465 := (iff #51 #464)
#466 := [rewrite]: #465
#457 := [asserted]: #51
#467 := [mp #457 #466]: #464
#788 := [mp #467 #787]: #783
#1147 := [unit-resolution #788 #1150]: #47
#235 := (not #47)
#247 := (or #235 #214)
#623 := [asserted]: #247
#1148 := [unit-resolution #623 #1147]: #214
#764 := (or #20 #22)
decl f3 :: S1
#7 := f3
#8 := (= f3 f1)
#443 := (or #20 #22 #8)
#767 := (iff #443 #764)
#761 := (or #20 #22 false)
#765 := (iff #761 #764)
#766 := [rewrite]: #765
#762 := (iff #443 #761)
#752 := (iff #8 false)
#9 := (not #8)
#436 := [asserted]: #9
#754 := [iff-false #436]: #752
#763 := [monotonicity #754]: #762
#768 := [trans #763 #766]: #767
#23 := (or #22 #8)
#24 := (or #20 #23)
#444 := (iff #24 #443)
#445 := [rewrite]: #444
#440 := [asserted]: #24
#446 := [mp #440 #445]: #443
#769 := [mp #446 #768]: #764
#1145 := [unit-resolution #769 #1148]: #20
#213 := (not #20)
#221 := (or #218 #213)
#606 := [asserted]: #221
#1146 := [unit-resolution #606 #1145]: #218
decl f12 :: S1
#33 := f12
#34 := (= f12 f1)
#224 := (not #34)
decl f30 :: S1
#92 := f30
#93 := (= f30 f1)
#282 := (not #93)
#328 := (or #323 #282)
#682 := [asserted]: #328
#1143 := [unit-resolution #682 #1151]: #282
decl f27 :: S1
#84 := f27
#85 := (= f27 f1)
#276 := (not #85)
#278 := (or #276 #277)
#645 := [asserted]: #278
#1144 := [unit-resolution #645 #1149]: #276
decl f19 :: S1
#54 := f19
#55 := (= f19 f1)
#241 := (not #55)
#245 := (or #241 #235)
#621 := [asserted]: #245
#1141 := [unit-resolution #621 #1147]: #241
#499 := (or #91 #93 #85 #55)
#94 := (or #85 #55)
#95 := (or #93 #94)
#96 := (or #91 #95)
#500 := (iff #96 #499)
#501 := [rewrite]: #500
#488 := [asserted]: #96
#502 := [mp #488 #501]: #499
#1142 := [unit-resolution #502 #1141 #1144 #1143]: #91
#296 := (or #281 #249)
#659 := [asserted]: #296
#1139 := [unit-resolution #659 #1142]: #249
#240 := (not #53)
#243 := (or #240 #235)
#619 := [asserted]: #243
#1140 := [unit-resolution #619 #1147]: #240
decl f10 :: S1
#27 := f10
#28 := (= f10 f1)
#219 := (not #28)
#222 := (or #219 #213)
#607 := [asserted]: #222
#1137 := [unit-resolution #607 #1145]: #219
#474 := (or #60 #62 #53 #28)
#63 := (or #53 #28)
#64 := (or #62 #63)
#65 := (or #60 #64)
#475 := (iff #65 #474)
#476 := [rewrite]: #475
#463 := [asserted]: #65
#477 := [mp #463 #476]: #474
#1138 := [unit-resolution #477 #1137 #1140 #1139]: #60
#263 := (or #248 #224)
#635 := [asserted]: #263
#1135 := [unit-resolution #635 #1138]: #224
#453 := (or #32 #34 #26)
#35 := (or #34 #26)
#36 := (or #32 #35)
#454 := (iff #36 #453)
#455 := [rewrite]: #454
#442 := [asserted]: #36
#456 := [mp #442 #455]: #453
#1136 := [unit-resolution #456 #1135 #1146]: #32
#223 := (not #32)
#231 := (or #228 #223)
#612 := [asserted]: #231
#1133 := [unit-resolution #612 #1136]: #228
#45 := (or #44 #38)
#452 := [asserted]: #45
#1134 := [unit-resolution #452 #1133]: #44
#233 := (not #44)
#274 := (or #272 #233)
#643 := [asserted]: #274
#1131 := [unit-resolution #643 #1134]: #272
#519 := (or #119 #112 #81)
#120 := (or #112 #81)
#121 := (or #119 #120)
#520 := (iff #121 #519)
#521 := [rewrite]: #520
#508 := [asserted]: #121
#522 := [mp #508 #521]: #519
#1132 := [unit-resolution #522 #1131 #1153]: #112
decl f14 :: S1
#39 := f14
#40 := (= f14 f1)
#229 := (not #40)
#232 := (or #229 #223)
#613 := [asserted]: #232
#1129 := [unit-resolution #613 #1136]: #229
decl f22 :: S1
#66 := f22
#67 := (= f22 f1)
#256 := (not #67)
#259 := (or #256 #248)
#631 := [asserted]: #259
#1130 := [unit-resolution #631 #1138]: #256
decl f24 :: S1
#73 := f24
#74 := (= f24 f1)
#264 := (not #74)
#275 := (or #264 #233)
#644 := [asserted]: #275
#1127 := [unit-resolution #644 #1134]: #264
#484 := (or #74 #76 #67 #40)
#77 := (or #67 #40)
#78 := (or #76 #77)
#79 := (or #74 #78)
#485 := (iff #79 #484)
#486 := [rewrite]: #485
#473 := [asserted]: #79
#487 := [mp #473 #486]: #484
#1128 := [unit-resolution #487 #1127 #1130 #1129]: #76
#265 := (not #76)
#309 := (or #305 #265)
#668 := [asserted]: #309
#1125 := [unit-resolution #668 #1128 #1132]: false
#1123 := [lemma #1125]: #1126
#1018 := [unit-resolution #1123 #1019 #1153]: #323
#559 := (or #167 #169 #161 #131)
#170 := (or #161 #131)
#171 := (or #169 #170)
#172 := (or #167 #171)
#560 := (iff #172 #559)
#561 := [rewrite]: #560
#548 := [asserted]: #172
#562 := [mp #548 #561]: #559
#1015 := [unit-resolution #562 #1018 #1017 #1020]: #167
#378 := (or #363 #331)
#719 := [asserted]: #378
#1016 := [unit-resolution #719 #1015]: #331
#1026 := (or #305 #138 #125 #150 #152)
#1049 := [hypothesis]: #112
#307 := (or #305 #306)
#666 := [asserted]: #307
#1050 := [unit-resolution #666 #1049]: #306
#544 := (or #150 #152 #143 #114)
#153 := (or #143 #114)
#154 := (or #152 #153)
#155 := (or #150 #154)
#545 := (iff #155 #544)
#546 := [rewrite]: #545
#533 := [asserted]: #155
#547 := [mp #533 #546]: #544
#1047 := [unit-resolution #547 #1050 #1052 #1051]: #143
#342 := (or #338 #298)
#692 := [asserted]: #342
#1048 := [unit-resolution #692 #1047]: #298
#308 := (or #305 #297)
#667 := [asserted]: #308
#1045 := [unit-resolution #667 #1049]: #297
#341 := (or #338 #330)
#691 := [asserted]: #341
#1046 := [unit-resolution #691 #1047]: #330
#1096 := [hypothesis]: #331
#1063 := (or #277 #138 #136 #105 #107)
#1083 := [hypothesis]: #87
#1084 := [unit-resolution #647 #1083]: #236
#1081 := [unit-resolution #788 #1084]: #47
#1082 := [unit-resolution #623 #1081]: #214
#1079 := [unit-resolution #769 #1082]: #20
#1080 := [unit-resolution #607 #1079]: #219
#1077 := [unit-resolution #619 #1081]: #240
#1078 := [hypothesis]: #298
#1075 := [hypothesis]: #297
#1076 := [unit-resolution #621 #1081]: #241
#1073 := [unit-resolution #645 #1083]: #276
#1085 := (or #289 #85 #55 #138 #136)
#1093 := [hypothesis]: #98
#291 := (or #289 #290)
#654 := [asserted]: #291
#1094 := [unit-resolution #654 #1093]: #290
#534 := (or #136 #138 #129 #100)
#139 := (or #129 #100)
#140 := (or #138 #139)
#141 := (or #136 #140)
#535 := (iff #141 #534)
#536 := [rewrite]: #535
#523 := [asserted]: #141
#537 := [mp #523 #536]: #534
#1091 := [unit-resolution #537 #1094 #1096 #1095]: #129
#1092 := [hypothesis]: #241
#1089 := [hypothesis]: #276
#292 := (or #289 #281)
#655 := [asserted]: #292
#1090 := [unit-resolution #655 #1093]: #281
#1087 := [unit-resolution #502 #1090 #1089 #1092]: #93
#326 := (or #322 #282)
#680 := [asserted]: #326
#1088 := [unit-resolution #680 #1087 #1091]: false
#1086 := [lemma #1088]: #1085
#1074 := [unit-resolution #1086 #1073 #1076 #1096 #1095]: #289
#509 := (or #105 #107 #98 #69)
#108 := (or #98 #69)
#109 := (or #107 #108)
#110 := (or #105 #109)
#510 := (iff #110 #509)
#511 := [rewrite]: #510
#498 := [asserted]: #110
#512 := [mp #498 #511]: #509
#1071 := [unit-resolution #512 #1074 #1075 #1078]: #69
#257 := (not #69)
#261 := (or #257 #248)
#633 := [asserted]: #261
#1072 := [unit-resolution #633 #1071]: #248
#1069 := [unit-resolution #477 #1072 #1077 #1080]: #62
#295 := (or #290 #249)
#658 := [asserted]: #295
#1070 := [unit-resolution #658 #1069]: #290
#1067 := [unit-resolution #537 #1070 #1096 #1095]: #129
#1068 := [unit-resolution #659 #1069]: #281
#1065 := [unit-resolution #502 #1068 #1073 #1076]: #93
#1066 := [unit-resolution #680 #1065 #1067]: false
#1064 := [lemma #1066]: #1063
#1043 := [unit-resolution #1064 #1046 #1096 #1045 #1048]: #277
#1044 := [unit-resolution #527 #1043 #1154]: #123
#325 := (or #322 #317)
#679 := [asserted]: #325
#1041 := [unit-resolution #679 #1044]: #322
#1042 := [unit-resolution #537 #1041 #1096 #1046]: #100
#1039 := [unit-resolution #654 #1042]: #289
#1040 := [unit-resolution #512 #1039 #1045 #1048]: #69
#1037 := [unit-resolution #633 #1040]: #248
#1038 := [unit-resolution #658 #1042]: #249
#294 := (or #290 #281)
#657 := [asserted]: #294
#1035 := [unit-resolution #657 #1042]: #281
#329 := (or #317 #282)
#683 := [asserted]: #329
#1036 := [unit-resolution #683 #1044]: #282
#1053 := (or #235 #62 #60)
#1061 := [hypothesis]: #248
#1062 := [hypothesis]: #249
#1059 := [hypothesis]: #47
#1060 := [unit-resolution #619 #1059]: #240
#1057 := [unit-resolution #477 #1060 #1062 #1061]: #28
#1058 := [unit-resolution #623 #1059]: #214
#1055 := [unit-resolution #769 #1058]: #20
#1056 := [unit-resolution #607 #1055 #1057]: false
#1054 := [lemma #1056]: #1053
#1033 := [unit-resolution #1054 #1038 #1037]: #235
#1034 := [unit-resolution #788 #1033]: #49
#279 := (or #276 #236)
#646 := [asserted]: #279
#1031 := [unit-resolution #646 #1034]: #276
#1032 := [unit-resolution #502 #1031 #1036 #1035]: #55
#242 := (or #240 #241)
#618 := [asserted]: #242
#1029 := [unit-resolution #618 #1032]: #240
#1030 := [unit-resolution #477 #1029 #1038 #1037]: #28
#246 := (or #241 #214)
#622 := [asserted]: #246
#1027 := [unit-resolution #622 #1032]: #214
#1028 := [unit-resolution #769 #1027]: #20
#1025 := [unit-resolution #607 #1028 #1030]: false
#1023 := [lemma #1025]: #1026
#1013 := [unit-resolution #1023 #1016 #1019 #1052 #1051]: #305
#1014 := [unit-resolution #522 #1013 #1153]: #81
#1097 := (or #272 #125 #76)
#1124 := [hypothesis]: #81
#1121 := [unit-resolution #643 #1124]: #233
#1122 := [unit-resolution #452 #1121]: #38
#1119 := [unit-resolution #612 #1122]: #223
#273 := (or #272 #264)
#642 := [asserted]: #273
#1120 := [unit-resolution #642 #1124]: #264
#1117 := [hypothesis]: #265
#230 := (or #228 #229)
#611 := [asserted]: #230
#1118 := [unit-resolution #611 #1122]: #229
#1115 := [unit-resolution #487 #1118 #1117 #1120]: #67
#260 := (or #256 #224)
#632 := [asserted]: #260
#1116 := [unit-resolution #632 #1115]: #224
#1113 := [unit-resolution #456 #1116 #1119]: #26
#220 := (or #218 #219)
#605 := [asserted]: #220
#1114 := [unit-resolution #605 #1113]: #219
#1111 := [unit-resolution #631 #1115]: #248
#1112 := [unit-resolution #606 #1113]: #213
#1109 := [unit-resolution #769 #1112]: #22
#244 := (or #240 #214)
#620 := [asserted]: #244
#1110 := [unit-resolution #620 #1109]: #240
#1107 := [unit-resolution #477 #1110 #1111 #1114]: #62
#1108 := [unit-resolution #659 #1107]: #281
#1105 := [unit-resolution #622 #1109]: #241
#1106 := [unit-resolution #623 #1109]: #235
#1103 := [unit-resolution #788 #1106]: #49
#1104 := [unit-resolution #646 #1103]: #276
#1101 := [unit-resolution #502 #1104 #1105 #1108]: #93
#1102 := [unit-resolution #647 #1103]: #277
#1099 := [unit-resolution #527 #1102 #1154]: #123
#1100 := [unit-resolution #683 #1099 #1101]: false
#1098 := [lemma #1100]: #1097
#1011 := [unit-resolution #1098 #1014 #1019]: #76
#311 := (or #306 #265)
#670 := [asserted]: #311
#1012 := [unit-resolution #670 #1011]: #306
#1009 := [unit-resolution #547 #1012 #1052 #1051]: #143
#1010 := [unit-resolution #692 #1009]: #298
#312 := (or #297 #265)
#671 := [asserted]: #312
#1007 := [unit-resolution #671 #1011]: #297
#1008 := [unit-resolution #691 #1009]: #330
#1005 := [unit-resolution #1064 #1008 #1016 #1007 #1010]: #277
#1006 := [unit-resolution #527 #1005 #1019]: #123
#1003 := [unit-resolution #679 #1006]: #322
#1004 := [unit-resolution #537 #1003 #1016 #1008]: #100
#1001 := [unit-resolution #654 #1004]: #289
#1002 := [unit-resolution #512 #1001 #1007 #1010]: #69
#999 := [unit-resolution #633 #1002]: #248
#1000 := [unit-resolution #658 #1004]: #249
#997 := [unit-resolution #643 #1014]: #233
#998 := [unit-resolution #452 #997]: #38
#995 := [unit-resolution #612 #998]: #223
#262 := (or #257 #224)
#634 := [asserted]: #262
#996 := [unit-resolution #634 #1002]: #224
#993 := [unit-resolution #456 #996 #995]: #26
#994 := [unit-resolution #605 #993]: #219
#991 := [unit-resolution #477 #994 #1000 #999]: #53
#992 := [unit-resolution #657 #1004]: #281
#989 := [unit-resolution #683 #1006]: #282
#990 := [unit-resolution #1054 #999 #1000]: #235
#987 := [unit-resolution #788 #990]: #49
#988 := [unit-resolution #646 #987]: #276
#985 := [unit-resolution #502 #988 #989 #992]: #55
#986 := [unit-resolution #618 #985 #991]: false
#984 := [lemma #986]: #983
#1162 := [unit-resolution #984 #1159 #1156 #1161]: #400
#590 := (or #204 #200 #176)
#205 := (or #200 #176)
#206 := (or #204 #205)
#591 := (iff #206 #590)
#592 := [rewrite]: #591
#583 := [asserted]: #206
#593 := [mp #583 #592]: #590
#1163 := [unit-resolution #593 #1162 #1160]: #204
#404 := (not #204)
#411 := (or #404 #380)
#744 := [asserted]: #411
#1164 := [unit-resolution #744 #1163]: #380
decl f55 :: S1
#180 := f55
#181 := (= f55 f1)
#379 := (not #181)
#392 := (or #388 #379)
#729 := [asserted]: #392
#1165 := [unit-resolution #729 #1155]: #379
decl f53 :: S1
#173 := f53
#174 := (= f53 f1)
#371 := (not #174)
#913 := (or #248 #181 #183 #150 #152 #119)
#937 := [hypothesis]: #60
#938 := [unit-resolution #631 #937]: #256
#939 := (or #306 #67 #119)
#971 := [hypothesis]: #256
#950 := [hypothesis]: #114
#947 := [unit-resolution #670 #950]: #265
#948 := [unit-resolution #666 #950]: #305
#945 := [unit-resolution #522 #948 #1153]: #81
#946 := [unit-resolution #642 #945]: #264
#943 := [unit-resolution #487 #946 #947 #971]: #40
#944 := [unit-resolution #643 #945]: #233
#941 := [unit-resolution #452 #944]: #38
#942 := [unit-resolution #611 #941 #943]: false
#940 := [lemma #942]: #939
#935 := [unit-resolution #940 #938 #1153]: #306
#936 := [unit-resolution #547 #935 #1052 #1051]: #143
#933 := [unit-resolution #691 #936]: #330
#934 := [unit-resolution #635 #937]: #224
#952 := (or #223 #67 #119)
#959 := [hypothesis]: #32
#960 := [unit-resolution #612 #959]: #228
#957 := [unit-resolution #452 #960]: #44
#958 := [unit-resolution #643 #957]: #272
#955 := [unit-resolution #522 #958 #1153]: #112
#956 := [unit-resolution #613 #959]: #229
#953 := [unit-resolution #644 #957]: #264
#954 := [unit-resolution #487 #953 #956 #971]: #76
#951 := [unit-resolution #668 #954 #955]: false
#949 := [lemma #951]: #952
#931 := [unit-resolution #949 #938 #1153]: #223
#932 := [unit-resolution #456 #931 #934]: #26
#929 := [unit-resolution #606 #932]: #213
#930 := [unit-resolution #769 #929]: #22
#927 := [unit-resolution #622 #930]: #241
#928 := [unit-resolution #623 #930]: #235
#925 := [unit-resolution #788 #928]: #49
#926 := [unit-resolution #646 #925]: #276
#961 := (or #297 #67 #119)
#972 := [hypothesis]: #105
#969 := [unit-resolution #671 #972]: #265
#970 := [unit-resolution #667 #972]: #305
#967 := [unit-resolution #522 #970 #1153]: #81
#968 := [unit-resolution #642 #967]: #264
#965 := [unit-resolution #487 #968 #969 #971]: #40
#966 := [unit-resolution #643 #967]: #233
#963 := [unit-resolution #452 #966]: #38
#964 := [unit-resolution #611 #963 #965]: false
#962 := [lemma #964]: #961
#923 := [unit-resolution #962 #938 #1153]: #297
#924 := [unit-resolution #633 #937]: #257
#921 := [unit-resolution #692 #936]: #298
#922 := [unit-resolution #512 #921 #924 #923]: #98
#919 := [hypothesis]: #380
#920 := [hypothesis]: #379
#340 := (or #338 #339)
#690 := [asserted]: #340
#917 := [unit-resolution #690 #936]: #339
#569 := (or #181 #183 #174 #145)
#184 := (or #174 #145)
#185 := (or #183 #184)
#186 := (or #181 #185)
#570 := (iff #186 #569)
#571 := [rewrite]: #570
#558 := [asserted]: #186
#572 := [mp #558 #571]: #569
#918 := [unit-resolution #572 #917 #920 #919]: #174
#375 := (or #371 #331)
#716 := [asserted]: #375
#915 := [unit-resolution #716 #918]: #331
#916 := [unit-resolution #1086 #915 #922 #926 #927 #933]: false
#914 := [lemma #916]: #913
#1166 := [unit-resolution #914 #1165 #1164 #1159 #1156 #1161]: #248
#753 := (or #371 #150 #152 #119 #60)
#793 := [hypothesis]: #174
#374 := (or #371 #363)
#715 := [asserted]: #374
#794 := [unit-resolution #715 #793]: #363
#791 := [unit-resolution #716 #793]: #331
#802 := (or #236 #119 #150 #152 #138 #60 #167)
#881 := [hypothesis]: #363
#819 := [hypothesis]: #49
#820 := [unit-resolution #647 #819]: #277
#834 := (or #322 #167 #87)
#849 := [hypothesis]: #129
#324 := (or #322 #323)
#678 := [asserted]: #324
#850 := [unit-resolution #678 #849]: #323
#847 := [unit-resolution #679 #849]: #317
#848 := [unit-resolution #527 #847 #867]: #125
#361 := (or #358 #318)
#706 := [asserted]: #361
#845 := [unit-resolution #706 #848]: #358
#846 := [unit-resolution #562 #845 #881 #850]: #169
#843 := [unit-resolution #707 #848]: #359
#844 := [unit-resolution #573 #843]: #197
#403 := (or #398 #364)
#738 := [asserted]: #403
#833 := [unit-resolution #738 #844 #846]: false
#831 := [lemma #833]: #834
#817 := [unit-resolution #831 #820 #881]: #322
#818 := [unit-resolution #646 #819]: #276
#851 := (or #282 #167 #87)
#869 := [hypothesis]: #93
#870 := [unit-resolution #682 #869]: #323
#868 := [unit-resolution #683 #869]: #317
#865 := [unit-resolution #527 #868 #867]: #125
#866 := [unit-resolution #706 #865]: #358
#863 := [unit-resolution #562 #866 #881 #870]: #169
#864 := [unit-resolution #707 #865]: #359
#861 := [unit-resolution #573 #864]: #197
#862 := [unit-resolution #738 #861 #863]: false
#852 := [lemma #862]: #851
#815 := [unit-resolution #852 #820 #881]: #282
#821 := (or #55 #138 #129 #150 #152 #93 #85 #60 #119)
#832 := [hypothesis]: #322
#829 := [hypothesis]: #282
#830 := [unit-resolution #502 #1092 #829 #1089]: #91
#827 := [unit-resolution #657 #830]: #290
#891 := (or #67 #55 #85 #138 #60 #150 #152 #119)
#911 := [unit-resolution #940 #971 #1153]: #306
#912 := [unit-resolution #547 #911 #1052 #1051]: #143
#909 := [unit-resolution #691 #912]: #330
#910 := [unit-resolution #949 #971 #1153]: #223
#907 := [unit-resolution #962 #971 #1153]: #297
#908 := [unit-resolution #692 #912]: #298
#905 := [unit-resolution #1086 #909 #1096 #1089 #1092]: #289
#906 := [unit-resolution #512 #905 #908 #907]: #69
#903 := [unit-resolution #634 #906]: #224
#904 := [unit-resolution #456 #903 #910]: #26
#901 := [unit-resolution #605 #904]: #219
#902 := [unit-resolution #606 #904]: #213
#899 := [unit-resolution #769 #902]: #22
#900 := [unit-resolution #620 #899]: #240
#897 := [unit-resolution #477 #900 #1061 #901]: #62
#898 := [unit-resolution #658 #897]: #290
#895 := [unit-resolution #537 #898 #1096 #909]: #129
#896 := [unit-resolution #659 #897]: #281
#893 := [unit-resolution #502 #896 #1092 #1089]: #93
#894 := [unit-resolution #680 #893 #895]: false
#892 := [lemma #894]: #891
#828 := [unit-resolution #892 #1092 #1089 #1096 #1061 #1052 #1051 #1153]: #67
#258 := (or #256 #257)
#630 := [asserted]: #258
#825 := [unit-resolution #630 #828]: #257
#826 := [unit-resolution #655 #830]: #289
#973 := (or #330 #69 #98 #150 #152)
#981 := [hypothesis]: #136
#982 := [unit-resolution #691 #981]: #338
#979 := [unit-resolution #547 #982 #1052 #1051]: #114
#977 := [hypothesis]: #257
#345 := (or #330 #298)
#695 := [asserted]: #345
#978 := [unit-resolution #695 #981]: #298
#975 := [unit-resolution #512 #978 #977 #980]: #105
#310 := (or #306 #297)
#669 := [asserted]: #310
#976 := [unit-resolution #669 #975 #979]: false
#974 := [lemma #976]: #973
#823 := [unit-resolution #974 #826 #825 #1052 #1051]: #330
#824 := [unit-resolution #537 #823 #827 #1096 #832]: false
#822 := [lemma #824]: #821
#816 := [unit-resolution #822 #817 #1096 #1052 #1051 #815 #818 #1061 #1153]: #55
#813 := [unit-resolution #618 #816]: #240
#814 := [unit-resolution #622 #816]: #214
#811 := [unit-resolution #769 #814]: #20
#812 := [unit-resolution #607 #811]: #219
#809 := [unit-resolution #477 #812 #1061 #813]: #62
#810 := [unit-resolution #658 #809]: #290
#807 := [unit-resolution #537 #810 #1096 #817]: #136
#808 := [unit-resolution #691 #807]: #338
#805 := [unit-resolution #547 #808 #1052 #1051]: #114
#293 := (or #289 #249)
#656 := [asserted]: #293
#806 := [unit-resolution #656 #809]: #289
#803 := [unit-resolution #974 #807 #806 #1052 #1051]: #69
#804 := [unit-resolution #630 #803]: #256
#801 := [unit-resolution #940 #804 #805 #1153]: false
#799 := [lemma #801]: #802
#792 := [unit-resolution #799 #791 #1052 #1051 #1153 #1061 #794]: #236
#789 := [unit-resolution #788 #792]: #47
#790 := [unit-resolution #1054 #789 #1061]: #62
#778 := [unit-resolution #658 #790]: #290
#779 := [unit-resolution #656 #790]: #289
#795 := (or #330 #119 #150 #152 #98)
#800 := [unit-resolution #974 #981 #980 #1052 #1051]: #69
#797 := [unit-resolution #630 #800]: #256
#798 := [unit-resolution #940 #797 #979 #1153]: false
#796 := [lemma #798]: #795
#776 := [unit-resolution #796 #779 #1052 #1051 #1153]: #330
#777 := [unit-resolution #537 #776 #791 #778]: #129
#774 := [unit-resolution #831 #777 #794]: #87
#775 := [unit-resolution #659 #790]: #281
#772 := [unit-resolution #621 #789]: #241
#773 := [unit-resolution #680 #777]: #282
#770 := [unit-resolution #502 #773 #772 #775]: #85
#771 := [unit-resolution #645 #770 #774]: false
#751 := [lemma #771]: #753
#1167 := [unit-resolution #751 #1159 #1156 #1161 #1166]: #371
#1168 := [unit-resolution #572 #1167 #1165 #1164]: #145
#1169 := [unit-resolution #690 #1168]: #338
#1170 := [unit-resolution #547 #1169 #1159 #1156]: #114
#1171 := [unit-resolution #669 #1170]: #297
#344 := (or #339 #298)
#694 := [asserted]: #344
#1172 := [unit-resolution #694 #1168]: #298
#1173 := [unit-resolution #940 #1170 #1161]: #67
#1174 := [unit-resolution #630 #1173]: #257
#1175 := [unit-resolution #512 #1174 #1172 #1171]: #98
#1176 := [unit-resolution #656 #1175]: #249
#1177 := [unit-resolution #632 #1173]: #224
#1178 := [unit-resolution #666 #1170]: #305
#1179 := [unit-resolution #522 #1178 #1161]: #81
#1180 := [unit-resolution #643 #1179]: #233
#1181 := [unit-resolution #452 #1180]: #38
#1182 := [unit-resolution #612 #1181]: #223
#1183 := [unit-resolution #456 #1182 #1177]: #26
#1184 := [unit-resolution #605 #1183]: #219
#1185 := [unit-resolution #477 #1184 #1166 #1176]: #53
#1186 := [unit-resolution #606 #1183]: #213
#1187 := [unit-resolution #769 #1186]: #22
#1188 := [unit-resolution #620 #1187 #1185]: false
#1190 := [lemma #1188]: #1189
#1365 := [unit-resolution #1190 #1160]: #388
#211 := (or #208 #190)
decl f5 :: S1
#13 := f5
#14 := (= f5 f1)
#600 := (or #14 #208 #190)
#858 := (iff #600 #211)
#853 := (or false #208 #190)
#856 := (iff #853 #211)
#857 := [rewrite]: #856
#854 := (iff #600 #853)
#757 := (iff #14 false)
#15 := (not #14)
#438 := [asserted]: #15
#758 := [iff-false #438]: #757
#855 := [monotonicity #758]: #854
#859 := [trans #855 #857]: #858
#212 := (or #14 #211)
#601 := (iff #212 #600)
#602 := [rewrite]: #601
#589 := [asserted]: #212
#603 := [mp #589 #602]: #600
#860 := [mp #603 #859]: #211
#1366 := [unit-resolution #860 #1365]: #208
#408 := (not #208)
#410 := (or #408 #380)
#743 := [asserted]: #410
#1367 := [unit-resolution #743 #1366]: #380
#409 := (or #408 #404)
#742 := [asserted]: #409
#1368 := [unit-resolution #742 #1366]: #404
#1369 := [unit-resolution #593 #1368 #1160]: #200
#1239 := (or #119 #183 #400)
#1224 := [unit-resolution #1123 #1153 #1019]: #323
#1225 := [unit-resolution #562 #1224 #1017 #1020]: #167
#1226 := [unit-resolution #715 #1225]: #371
#1222 := (or #379 #400 #119)
#1216 := [hypothesis]: #181
#390 := (or #387 #379)
#727 := [asserted]: #390
#1217 := [unit-resolution #727 #1216]: #387
#1218 := [unit-resolution #842 #1217]: #157
#394 := (or #379 #347)
#731 := [asserted]: #394
#1219 := [unit-resolution #731 #1216]: #347
#1220 := [unit-resolution #984 #1219 #1024 #1153]: #150
#1221 := [unit-resolution #702 #1220 #1218]: false
#1223 := [lemma #1221]: #1222
#1227 := [unit-resolution #1223 #1153 #1024]: #379
#1228 := [unit-resolution #572 #1227 #1226 #919]: #145
#1229 := [unit-resolution #694 #1228]: #298
#1192 := (or #297 #125 #119)
#1191 := [unit-resolution #1098 #967 #969 #1154]: false
#1193 := [lemma #1191]: #1192
#1230 := [unit-resolution #1193 #1153 #1019]: #297
#1231 := [unit-resolution #719 #1225]: #331
#343 := (or #339 #330)
#693 := [asserted]: #343
#1232 := [unit-resolution #693 #1228]: #330
#1233 := [unit-resolution #1064 #1232 #1231 #1230 #1229]: #277
#1234 := [unit-resolution #527 #1233 #1019]: #123
#1214 := (or #339 #138 #119 #125 #98)
#1194 := [hypothesis]: #145
#1195 := [unit-resolution #693 #1194]: #330
#1196 := [unit-resolution #694 #1194]: #298
#1197 := [unit-resolution #1193 #1153 #1154]: #297
#1198 := [unit-resolution #1064 #1195 #1096 #1197 #1196]: #277
#1199 := [unit-resolution #527 #1198 #1154]: #123
#1200 := [unit-resolution #679 #1199]: #322
#1201 := [unit-resolution #537 #1200 #1096 #1195]: #100
#1202 := [unit-resolution #658 #1201]: #249
#1203 := [unit-resolution #512 #1196 #1197 #980]: #69
#1204 := [unit-resolution #633 #1203]: #248
#1205 := [unit-resolution #634 #1203]: #224
#1206 := [unit-resolution #630 #1203]: #256
#1207 := [unit-resolution #949 #1206 #1153]: #223
#1208 := [unit-resolution #456 #1207 #1205]: #26
#1209 := [unit-resolution #605 #1208]: #219
#1210 := [unit-resolution #477 #1209 #1204 #1202]: #53
#1211 := [unit-resolution #606 #1208]: #213
#1212 := [unit-resolution #769 #1211]: #22
#1213 := [unit-resolution #620 #1212 #1210]: false
#1215 := [lemma #1213]: #1214
#1235 := [unit-resolution #1215 #1228 #1153 #1019 #1231]: #98
#1236 := [unit-resolution #654 #1235]: #290
#1237 := [unit-resolution #537 #1236 #1231 #1232]: #129
#1238 := [unit-resolution #679 #1237 #1234]: false
#1240 := [lemma #1238]: #1239
#1370 := [unit-resolution #1240 #1367 #1369]: #119
#1371 := [unit-resolution #703 #1370]: #354
#1372 := [unit-resolution #842 #1371]: #188
#1373 := [unit-resolution #727 #1372]: #379
#1374 := [unit-resolution #737 #1369]: #364
#1375 := [unit-resolution #736 #1369]: #398
#1376 := [unit-resolution #573 #1375]: #163
#1377 := [unit-resolution #705 #1376]: #358
#1378 := [unit-resolution #707 #1376]: #318
#391 := (or #387 #347)
#728 := [asserted]: #391
#1379 := [unit-resolution #728 #1372]: #347
#357 := (or #346 #313)
#704 := [asserted]: #357
#1380 := [unit-resolution #704 #1370]: #346
#1351 := (or #98 #125 #161 #169 #181 #183 #150 #152)
#1258 := [hypothesis]: #364
#1259 := [hypothesis]: #358
#1332 := (or #136 #150 #152 #181 #183 #125 #161 #169 #98)
#1317 := (or #129 #125 #136 #161 #169 #181 #183 #150 #152 #98)
#1297 := (or #105 #125 #98 #161 #169 #181 #183 #129 #136)
#1276 := (or #290 #125 #161 #169 #181 #183 #98 #105)
#1256 := [hypothesis]: #100
#1257 := [unit-resolution #657 #1256]: #281
#1260 := [unit-resolution #658 #1256]: #249
#1254 := (or #60 #62 #91 #125)
#1241 := [hypothesis]: #281
#1242 := [unit-resolution #1054 #1061 #1062]: #235
#1243 := [unit-resolution #788 #1242]: #49
#1244 := [unit-resolution #646 #1243]: #276
#1245 := [unit-resolution #647 #1243]: #277
#1246 := [unit-resolution #527 #1245 #1154]: #123
#1247 := [unit-resolution #683 #1246]: #282
#1248 := [unit-resolution #502 #1247 #1244 #1241]: #55
#1249 := [unit-resolution #618 #1248]: #240
#1250 := [unit-resolution #477 #1249 #1061 #1062]: #28
#1251 := [unit-resolution #622 #1248]: #214
#1252 := [unit-resolution #769 #1251]: #20
#1253 := [unit-resolution #607 #1252 #1250]: false
#1255 := [lemma #1253]: #1254
#1261 := [unit-resolution #1255 #1260 #1257 #1154]: #60
#1262 := [unit-resolution #633 #1261]: #257
#1263 := [unit-resolution #512 #1262 #980 #1075]: #107
#1264 := [unit-resolution #694 #1263]: #339
#1265 := [unit-resolution #572 #1264 #920 #919]: #174
#1266 := [unit-resolution #715 #1265]: #363
#1267 := [unit-resolution #562 #1266 #1259 #1258]: #131
#1268 := [unit-resolution #682 #1267]: #282
#1269 := [unit-resolution #681 #1267]: #317
#1270 := [unit-resolution #527 #1269 #1154]: #87
#1271 := [unit-resolution #645 #1270]: #276
#1272 := [unit-resolution #502 #1271 #1268 #1257]: #55
#1273 := [unit-resolution #647 #1270]: #236
#1274 := [unit-resolution #788 #1273]: #47
#1275 := [unit-resolution #621 #1274 #1272]: false
#1277 := [lemma #1275]: #1276
#1278 := [unit-resolution #1277 #1075 #1259 #1258 #920 #919 #980 #1154]: #290
#1279 := [unit-resolution #537 #1278 #832 #1095]: #138
#1280 := [unit-resolution #716 #1279]: #371
#1281 := [unit-resolution #572 #1280 #920 #919]: #145
#1282 := [unit-resolution #694 #1281]: #298
#1283 := [unit-resolution #512 #1282 #980 #1075]: #69
#1284 := [unit-resolution #633 #1283]: #248
#1285 := [unit-resolution #719 #1279]: #363
#1286 := [unit-resolution #562 #1285 #1259 #1258]: #131
#1287 := [unit-resolution #681 #1286]: #317
#1288 := [unit-resolution #527 #1287 #1154]: #87
#1289 := [unit-resolution #647 #1288]: #236
#1290 := [unit-resolution #788 #1289]: #47
#1291 := [unit-resolution #1054 #1290 #1284]: #62
#1292 := [unit-resolution #645 #1288]: #276
#1293 := [unit-resolution #682 #1286]: #282
#1294 := [unit-resolution #621 #1290]: #241
#1295 := [unit-resolution #502 #1294 #1293 #1292]: #91
#1296 := [unit-resolution #659 #1295 #1291]: false
#1298 := [lemma #1296]: #1297
#1299 := [unit-resolution #1298 #832 #980 #1259 #1258 #920 #919 #1154 #1095]: #105
#1300 := [unit-resolution #669 #1299]: #306
#1301 := [unit-resolution #547 #1300 #1052 #1051]: #143
#1302 := [unit-resolution #690 #1301]: #339
#1303 := [unit-resolution #572 #1302 #920 #919]: #174
#1304 := [unit-resolution #716 #1303]: #331
#1305 := [unit-resolution #537 #1304 #832 #1095]: #100
#1306 := [unit-resolution #657 #1305]: #281
#1307 := [unit-resolution #715 #1303]: #363
#1308 := [unit-resolution #562 #1307 #1259 #1258]: #131
#1309 := [unit-resolution #682 #1308]: #282
#1310 := [unit-resolution #681 #1308]: #317
#1311 := [unit-resolution #527 #1310 #1154]: #87
#1312 := [unit-resolution #645 #1311]: #276
#1313 := [unit-resolution #502 #1312 #1309 #1306]: #55
#1314 := [unit-resolution #647 #1311]: #236
#1315 := [unit-resolution #788 #1314]: #47
#1316 := [unit-resolution #621 #1315 #1313]: false
#1318 := [lemma #1316]: #1317
#1319 := [unit-resolution #1318 #1095 #1154 #1259 #1258 #920 #919 #1052 #1051 #980]: #129
#1320 := [unit-resolution #678 #1319]: #323
#1321 := [unit-resolution #562 #1320 #1259 #1258]: #167
#1322 := [unit-resolution #715 #1321]: #371
#1323 := [unit-resolution #572 #1322 #920 #919]: #145
#1324 := [unit-resolution #690 #1323]: #338
#1325 := [unit-resolution #547 #1324 #1052 #1051]: #114
#1326 := [unit-resolution #679 #1319]: #317
#1327 := [unit-resolution #527 #1326 #1154]: #87
#335 := (or #331 #322)
#687 := [asserted]: #335
#1328 := [unit-resolution #687 #1319]: #331
#1329 := [unit-resolution #694 #1323]: #298
#1330 := [unit-resolution #1064 #1329 #1095 #1328 #1327]: #105
#1331 := [unit-resolution #669 #1330 #1325]: false
#1333 := [lemma #1331]: #1332
#1334 := [unit-resolution #1333 #980 #1051 #920 #919 #1154 #1259 #1258 #1052]: #136
#1335 := [unit-resolution #974 #1334 #980 #1052 #1051]: #69
#1336 := [unit-resolution #633 #1335]: #248
#1337 := [unit-resolution #693 #1334]: #339
#1338 := [unit-resolution #572 #1337 #920 #919]: #174
#1339 := [unit-resolution #715 #1338]: #363
#1340 := [unit-resolution #562 #1339 #1259 #1258]: #131
#1341 := [unit-resolution #681 #1340]: #317
#1342 := [unit-resolution #527 #1341 #1154]: #87
#1343 := [unit-resolution #647 #1342]: #236
#1344 := [unit-resolution #788 #1343]: #47
#1345 := [unit-resolution #1054 #1344 #1336]: #62
#1346 := [unit-resolution #645 #1342]: #276
#1347 := [unit-resolution #682 #1340]: #282
#1348 := [unit-resolution #621 #1344]: #241
#1349 := [unit-resolution #502 #1348 #1347 #1346]: #91
#1350 := [unit-resolution #659 #1349 #1345]: false
#1352 := [lemma #1350]: #1351
#1381 := [unit-resolution #1352 #1378 #1377 #1374 #1373 #1367 #1380 #1379]: #98
#1382 := [unit-resolution #654 #1381]: #290
#1363 := (or #317 #100 #181 #183 #161 #169)
#1353 := [hypothesis]: #123
#1354 := [unit-resolution #681 #1353]: #323
#1355 := [unit-resolution #562 #1354 #1259 #1258]: #167
#1356 := [unit-resolution #715 #1355]: #371
#1357 := [unit-resolution #572 #1356 #920 #919]: #145
#1358 := [unit-resolution #679 #1353]: #322
#1359 := [hypothesis]: #290
#1360 := [unit-resolution #719 #1355]: #331
#1361 := [unit-resolution #537 #1360 #1359 #1358]: #136
#1362 := [unit-resolution #693 #1361 #1357]: false
#1364 := [lemma #1362]: #1363
#1383 := [unit-resolution #1364 #1382 #1373 #1367 #1377 #1374]: #317
#1384 := [unit-resolution #527 #1383 #1378]: #87
#1385 := [unit-resolution #645 #1384]: #276
#1386 := [unit-resolution #655 #1381]: #281
#1387 := [unit-resolution #647 #1384]: #236
#1388 := [unit-resolution #788 #1387]: #47
#1389 := [unit-resolution #621 #1388]: #241
#1390 := [unit-resolution #502 #1389 #1386 #1385]: #93
#1391 := [unit-resolution #682 #1390]: #323
#1392 := [unit-resolution #562 #1391 #1377 #1374]: #167
#1393 := [unit-resolution #715 #1392]: #371
#1394 := [unit-resolution #572 #1393 #1373 #1367]: #145
#1395 := [unit-resolution #680 #1390]: #322
#1396 := [unit-resolution #719 #1392]: #331
#1397 := [unit-resolution #537 #1396 #1382 #1395]: #136
#1398 := [unit-resolution #693 #1397 #1394]: false
#1399 := [lemma #1398]: #176
#376 := (or #372 #363)
#717 := [asserted]: #376
#1426 := [unit-resolution #717 #1399]: #363
#1428 := [unit-resolution #831 #1426]: #1427
#1429 := [unit-resolution #1428 #867]: #322
#1431 := (or #136 #129 #100)
#377 := (or #372 #331)
#718 := [asserted]: #377
#1430 := [unit-resolution #718 #1399]: #331
#1432 := [unit-resolution #537 #1430]: #1431
#1433 := [unit-resolution #1432 #1429 #1095]: #100
#1434 := [unit-resolution #657 #1433]: #281
#1435 := (or #282 #87)
#1436 := [unit-resolution #852 #1426]: #1435
#1437 := [unit-resolution #1436 #867]: #282
#1419 := (or #214 #93 #91)
#1413 := [hypothesis]: #22
#1414 := [unit-resolution #622 #1413]: #241
#1415 := [unit-resolution #502 #1414 #829 #1241]: #85
#1416 := [unit-resolution #623 #1413]: #235
#1417 := [unit-resolution #788 #1416]: #49
#1418 := [unit-resolution #646 #1417 #1415]: false
#1420 := [lemma #1418]: #1419
#1438 := [unit-resolution #1420 #1437 #1434]: #214
#1439 := [unit-resolution #769 #1438]: #20
#1440 := [unit-resolution #607 #1439]: #219
#1441 := [unit-resolution #658 #1433]: #249
#1442 := [unit-resolution #606 #1439]: #218
#1424 := (or #248 #26 #98)
#1421 := [hypothesis]: #218
#1411 := (or #223 #98 #69 #67)
#1400 := [unit-resolution #949 #959 #971]: #119
#1401 := [unit-resolution #703 #1400]: #354
#1402 := [unit-resolution #842 #1401]: #188
#1403 := [unit-resolution #728 #1402]: #347
#1404 := [unit-resolution #704 #1400]: #346
#1405 := [unit-resolution #487 #953 #971 #956]: #76
#1406 := [unit-resolution #670 #1405]: #306
#1407 := [unit-resolution #547 #1406 #1404 #1403]: #143
#1408 := [unit-resolution #671 #1405]: #297
#1409 := [unit-resolution #512 #1408 #980 #977]: #107
#1410 := [unit-resolution #692 #1409 #1407]: false
#1412 := [lemma #1410]: #1411
#1422 := [unit-resolution #1412 #924 #980 #938]: #223
#1423 := [unit-resolution #456 #1422 #934 #1421]: false
#1425 := [lemma #1423]: #1424
#1443 := [unit-resolution #1425 #1442 #980]: #248
#1444 := [unit-resolution #477 #1443 #1441 #1440]: #53
#1445 := [unit-resolution #618 #1444]: #241
#1446 := [unit-resolution #1054 #1443 #1441]: #235
#1447 := [unit-resolution #788 #1446]: #49
#1448 := [unit-resolution #646 #1447]: #276
#1449 := [unit-resolution #502 #1448 #1445 #1437 #1434]: false
#1451 := [lemma #1449]: #1450
#1452 := [unit-resolution #1451 #1095 #980]: #87
#1453 := [unit-resolution #647 #1452]: #236
#1454 := [unit-resolution #788 #1453]: #47
#1455 := [unit-resolution #623 #1454]: #214
#1456 := [unit-resolution #769 #1455]: #20
#1457 := [unit-resolution #606 #1456]: #218
#1458 := [unit-resolution #1425 #1457 #980]: #248
#1459 := [unit-resolution #1054 #1458 #1454]: #62
#1460 := [unit-resolution #658 #1459]: #290
#1461 := [unit-resolution #1432 #1460 #1095]: #129
#1462 := [unit-resolution #621 #1454]: #241
#1463 := [unit-resolution #645 #1452]: #276
#1464 := [unit-resolution #659 #1459]: #281
#1465 := [unit-resolution #502 #1464 #1463 #1462]: #93
#1466 := [unit-resolution #680 #1465 #1461]: false
#1468 := [lemma #1466]: #1467
#1481 := [unit-resolution #1468 #980]: #136
#1482 := [unit-resolution #693 #1481]: #339
#1479 := (or #387 #145)
#1469 := [hypothesis]: #188
#1470 := [unit-resolution #726 #1469]: #388
#1471 := [unit-resolution #860 #1470]: #208
#1472 := [hypothesis]: #339
#1473 := [unit-resolution #727 #1469]: #379
#1475 := (or #181 #183 #145)
#373 := (or #371 #372)
#714 := [asserted]: #373
#1474 := [unit-resolution #714 #1399]: #371
#1476 := [unit-resolution #572 #1474]: #1475
#1477 := [unit-resolution #1476 #1473 #1472]: #183
#1478 := [unit-resolution #743 #1477 #1471]: false
#1480 := [lemma #1478]: #1479
#1483 := [unit-resolution #1480 #1482]: #387
#1484 := [unit-resolution #842 #1483]: #157
#1485 := [unit-resolution #702 #1484]: #346
#1486 := [unit-resolution #703 #1484]: #313
#1487 := [unit-resolution #796 #1486 #1481 #1485 #980]: #152
#1488 := [unit-resolution #730 #1487]: #388
#1489 := [unit-resolution #860 #1488]: #208
#1490 := [unit-resolution #731 #1487]: #379
#1491 := [unit-resolution #1476 #1490 #1482]: #183
#1492 := [unit-resolution #743 #1491 #1489]: false
#1493 := [lemma #1492]: #98
#1515 := [unit-resolution #656 #1493]: #249
#1511 := [unit-resolution #655 #1493]: #281
#1512 := [unit-resolution #1420 #829 #1511]: #214
#1513 := [unit-resolution #769 #1512]: #20
#1514 := [unit-resolution #607 #1513]: #219
#1516 := [unit-resolution #606 #1513]: #218
#1509 := (or #248 #26)
#1494 := [unit-resolution #654 #1493]: #290
#1495 := [unit-resolution #1432 #1095 #1494]: #129
#300 := (or #297 #289)
#661 := [asserted]: #300
#1496 := [unit-resolution #661 #1493]: #297
#302 := (or #298 #289)
#663 := [asserted]: #302
#1497 := [unit-resolution #663 #1493]: #298
#1498 := (or #277 #136 #105 #107)
#1499 := [unit-resolution #1064 #1430]: #1498
#1500 := [unit-resolution #1499 #1095 #1497 #1496]: #277
#1501 := [unit-resolution #1428 #1500 #1495]: false
#1502 := [lemma #1501]: #136
#1503 := [unit-resolution #693 #1502]: #339
#1504 := [unit-resolution #1480 #1503]: #387
#1505 := [unit-resolution #842 #1504]: #157
#1506 := [unit-resolution #703 #1505]: #313
#1507 := [unit-resolution #949 #938 #1506]: #223
#1508 := [unit-resolution #456 #1507 #934 #1421]: false
#1510 := [lemma #1508]: #1509
#1517 := [unit-resolution #1510 #1516]: #248
#1518 := [unit-resolution #477 #1517 #1515 #1514]: #53
#1519 := [unit-resolution #618 #1518]: #241
#1520 := [unit-resolution #1054 #1517 #1515]: #235
#1521 := [unit-resolution #788 #1520]: #49
#1522 := [unit-resolution #646 #1521]: #276
#1523 := [unit-resolution #502 #1522 #1519 #1511 #829]: false
#1524 := [lemma #1523]: #93
#1525 := [unit-resolution #1436 #1524]: #87
#321 := (or #318 #277)
#677 := [asserted]: #321
#1526 := [unit-resolution #677 #1525]: #318
#1527 := [unit-resolution #1255 #1526 #1511 #1515]: #60
#1528 := [unit-resolution #1510 #1527]: #26
#1529 := [unit-resolution #647 #1525]: #236
#1530 := [unit-resolution #788 #1529]: #47
#1531 := [unit-resolution #623 #1530]: #214
#1532 := [unit-resolution #769 #1531]: #20
[unit-resolution #606 #1532 #1528]: false
unsat
a69a9e8c5e31ec6b9da4cf96f47b52cf6b9404d9 117 0
#2 := false
decl f3 :: (-> S3 S2 S1)
#10 := (:var 0 S2)
decl f4 :: (-> S4 S1 S3)
decl f6 :: S1
#16 := f6
decl f5 :: S4
#7 := f5
#17 := (f4 f5 f6)
#18 := (f3 #17 #10)
#573 := (pattern #18)
decl f1 :: S1
#3 := f1
#19 := (= #18 f1)
#76 := (not #19)
#574 := (forall (vars (?v0 S2)) (:pat #573) #76)
decl f7 :: S2
#21 := f7
#22 := (f3 #17 f7)
#23 := (= #22 f1)
#150 := (= f6 f1)
#151 := (iff #23 #150)
#8 := (:var 1 S1)
#9 := (f4 f5 #8)
#11 := (f3 #9 #10)
#566 := (pattern #11)
#13 := (= #8 f1)
#12 := (= #11 f1)
#14 := (iff #12 #13)
#567 := (forall (vars (?v0 S1) (?v1 S2)) (:pat #566) #14)
#15 := (forall (vars (?v0 S1) (?v1 S2)) #14)
#570 := (iff #15 #567)
#568 := (iff #14 #14)
#569 := [refl]: #568
#571 := [quant-intro #569]: #570
#62 := (~ #15 #15)
#60 := (~ #14 #14)
#61 := [refl]: #60
#63 := [nnf-pos #61]: #62
#46 := [asserted]: #15
#53 := [mp~ #46 #63]: #15
#572 := [mp #53 #571]: #567
#152 := (not #567)
#228 := (or #152 #151)
#561 := [quant-inst #16 #21]: #228
#237 := [unit-resolution #561 #572]: #151
decl ?v0!0 :: S2
#66 := ?v0!0
#67 := (f3 #17 ?v0!0)
#68 := (= #67 f1)
#236 := (iff #68 #150)
#238 := (or #152 #236)
#229 := [quant-inst #16 #66]: #238
#227 := [unit-resolution #229 #572]: #236
#240 := (not #236)
#199 := (or #240 #150)
#55 := (not #23)
#215 := [hypothesis]: #55
#83 := (or #68 #23)
#79 := (forall (vars (?v0 S2)) #76)
#82 := (or #79 #55)
#84 := (and #83 #82)
#20 := (exists (vars (?v0 S2)) #19)
#48 := (not #20)
#49 := (iff #48 #23)
#85 := (~ #49 #84)
#57 := (~ #23 #23)
#65 := [refl]: #57
#64 := (~ #55 #55)
#56 := [refl]: #64
#80 := (~ #48 #79)
#77 := (~ #76 #76)
#78 := [refl]: #77
#81 := [nnf-neg #78]: #80
#73 := (not #48)
#74 := (~ #73 #68)
#69 := (~ #20 #68)
#70 := [sk]: #69
#75 := [nnf-neg #70]: #74
#86 := [nnf-pos #75 #81 #56 #65]: #85
#24 := (iff #20 #23)
#25 := (not #24)
#50 := (iff #25 #49)
#51 := [rewrite]: #50
#47 := [asserted]: #25
#54 := [mp #47 #51]: #49
#87 := [mp~ #54 #86]: #84
#90 := [and-elim #87]: #83
#557 := [unit-resolution #90 #215]: #68
#243 := (not #68)
#222 := (or #240 #243 #150)
#558 := [def-axiom]: #222
#541 := [unit-resolution #558 #557]: #199
#203 := [unit-resolution #541 #227]: #150
#241 := (not #150)
#562 := (not #151)
#204 := (or #562 #241)
#563 := (or #562 #23 #241)
#564 := [def-axiom]: #563
#205 := [unit-resolution #564 #215]: #204
#206 := [unit-resolution #205 #203 #237]: false
#543 := [lemma #206]: #23
#579 := (or #574 #55)
#580 := (iff #82 #579)
#577 := (iff #79 #574)
#575 := (iff #76 #76)
#576 := [refl]: #575
#578 := [quant-intro #576]: #577
#581 := [monotonicity #578]: #580
#91 := [and-elim #87]: #82
#582 := [mp #91 #581]: #579
#242 := [unit-resolution #582 #543]: #574
#555 := (not #574)
#214 := (or #555 #55)
#219 := [quant-inst #21]: #214
[unit-resolution #219 #543 #242]: false
unsat
fdf61e060f49731790f4d6c8f9b26c21349c60b3 117 0
#2 := false
decl f1 :: S1
#3 := f1
decl f7 :: S1
#25 := f7
#206 := (= f7 f1)
decl f3 :: (-> S3 S2 S1)
decl f6 :: S2
#20 := f6
decl f4 :: (-> S4 S1 S3)
decl f5 :: S4
#7 := f5
#26 := (f4 f5 f7)
#30 := (f3 #26 f6)
#31 := (= #30 f1)
#292 := (iff #31 #206)
#10 := (:var 0 S2)
#8 := (:var 1 S1)
#9 := (f4 f5 #8)
#11 := (f3 #9 #10)
#622 := (pattern #11)
#13 := (= #8 f1)
#12 := (= #11 f1)
#14 := (iff #12 #13)
#623 := (forall (vars (?v0 S1) (?v1 S2)) (:pat #622) #14)
#15 := (forall (vars (?v0 S1) (?v1 S2)) #14)
#626 := (iff #15 #623)
#624 := (iff #14 #14)
#625 := [refl]: #624
#627 := [quant-intro #625]: #626
#73 := (~ #15 #15)
#71 := (~ #14 #14)
#72 := [refl]: #71
#74 := [nnf-pos #72]: #73
#54 := [asserted]: #15
#62 := [mp~ #54 #74]: #15
#628 := [mp #62 #627]: #623
#295 := (not #623)
#611 := (or #295 #292)
#270 := [quant-inst #25 #20]: #611
#297 := [unit-resolution #270 #628]: #292
decl ?v0!3 :: S2
#120 := ?v0!3
#123 := (f3 #26 ?v0!3)
#124 := (= #123 f1)
#296 := (iff #124 #206)
#299 := (or #295 #296)
#278 := [quant-inst #25 #120]: #299
#298 := [unit-resolution #278 #628]: #296
#614 := (not #296)
#599 := (or #614 #206)
#108 := (not #31)
#27 := (f3 #26 #10)
#654 := (pattern #27)
#28 := (= #27 f1)
#132 := (not #28)
#655 := (forall (vars (?v0 S2)) (:pat #654) #132)
#207 := [hypothesis]: #31
#660 := (or #655 #108)
#135 := (forall (vars (?v0 S2)) #132)
#138 := (or #135 #108)
#661 := (iff #138 #660)
#658 := (iff #135 #655)
#656 := (iff #132 #132)
#657 := [refl]: #656
#659 := [quant-intro #657]: #658
#662 := [monotonicity #659]: #661
#139 := (or #124 #31)
#140 := (and #139 #138)
#29 := (exists (vars (?v0 S2)) #28)
#57 := (not #29)
#58 := (iff #57 #31)
#141 := (~ #58 #140)
#81 := (~ #31 #31)
#119 := [refl]: #81
#109 := (~ #108 #108)
#80 := [refl]: #109
#136 := (~ #57 #135)
#133 := (~ #132 #132)
#134 := [refl]: #133
#137 := [nnf-neg #134]: #136
#129 := (not #57)
#130 := (~ #129 #124)
#125 := (~ #29 #124)
#126 := [sk]: #125
#131 := [nnf-neg #126]: #130
#142 := [nnf-pos #131 #137 #80 #119]: #141
#32 := (iff #29 #31)
#33 := (not #32)
#59 := (iff #33 #58)
#60 := [rewrite]: #59
#56 := [asserted]: #33
#63 := [mp #56 #60]: #58
#143 := [mp~ #63 #142]: #140
#147 := [and-elim #143]: #138
#663 := [mp #147 #662]: #660
#293 := [unit-resolution #663 #207]: #655
#610 := (not #655)
#283 := (or #610 #108)
#284 := [quant-inst #20]: #283
#617 := [unit-resolution #284 #207 #293]: false
#618 := [lemma #617]: #108
#146 := [and-elim #143]: #139
#262 := [unit-resolution #146 #618]: #124
#208 := (not #124)
#294 := (or #614 #208 #206)
#285 := [def-axiom]: #294
#600 := [unit-resolution #285 #262]: #599
#601 := [unit-resolution #600 #298]: #206
#616 := (not #206)
#275 := (not #292)
#602 := (or #275 #616)
#612 := (or #275 #31 #616)
#271 := [def-axiom]: #612
#603 := [unit-resolution #271 #618]: #602
[unit-resolution #603 #601 #297]: false
unsat
43550507f510d81bc4fb9ef8c1fd14424eaa9070 37 0
#2 := false
#10 := 0::Int
decl f3 :: Int
#7 := f3
#12 := (<= f3 0::Int)
#54 := (not #12)
decl f4 :: Int
#8 := f4
#13 := (<= f4 0::Int)
#9 := (* f3 f4)
#11 := (<= #9 0::Int)
#37 := (not #11)
#44 := (or #37 #12 #13)
#47 := (not #44)
#14 := (or #12 #13)
#15 := (implies #11 #14)
#16 := (not #15)
#50 := (iff #16 #47)
#38 := (or #37 #14)
#41 := (not #38)
#48 := (iff #41 #47)
#45 := (iff #38 #44)
#46 := [rewrite]: #45
#49 := [monotonicity #46]: #48
#42 := (iff #16 #41)
#39 := (iff #15 #38)
#40 := [rewrite]: #39
#43 := [monotonicity #40]: #42
#51 := [trans #43 #49]: #50
#36 := [asserted]: #16
#52 := [mp #36 #51]: #47
#55 := [not-or-elim #52]: #54
#56 := (not #13)
#57 := [not-or-elim #52]: #56
#53 := [not-or-elim #52]: #11
[th-lemma arith farkas 1 1 1 #53 #57 #55]: false
unsat
76d09b53549e91e8b6b69b6b905b5e8307464c6f 106 0
#2 := false
decl f7 :: S2
#19 := f7
decl f3 :: (-> S3 S2 S2)
decl f4 :: S3
#7 := f4
#20 := (f3 f4 f7)
#21 := (= #20 f7)
#74 := (not #21)
decl f1 :: S1
#3 := f1
decl f5 :: (-> S4 S1 S1)
decl f6 :: S4
#12 := f6
#22 := (f5 f6 f1)
#23 := (= #22 f1)
#75 := (not #23)
#558 := [hypothesis]: #75
#13 := (:var 0 S1)
#14 := (f5 f6 #13)
#569 := (pattern #14)
#16 := (= #13 f1)
#15 := (= #14 f1)
#17 := (iff #15 #16)
#570 := (forall (vars (?v0 S1)) (:pat #569) #17)
#18 := (forall (vars (?v0 S1)) #17)
#573 := (iff #18 #570)
#571 := (iff #17 #17)
#572 := [refl]: #571
#574 := [quant-intro #572]: #573
#62 := (~ #18 #18)
#61 := (~ #17 #17)
#72 := [refl]: #61
#63 := [nnf-pos #72]: #62
#48 := [asserted]: #18
#73 := [mp~ #48 #63]: #18
#575 := [mp #73 #574]: #570
#239 := (not #570)
#218 := (or #239 #23)
#146 := (= f1 f1)
#147 := (iff #23 #146)
#554 := (or #239 #147)
#212 := (iff #554 #218)
#550 := (iff #218 #218)
#223 := [rewrite]: #550
#238 := (iff #147 #23)
#1 := true
#24 := (iff #23 true)
#50 := (iff #24 #23)
#51 := [rewrite]: #50
#236 := (iff #147 #24)
#232 := (iff #146 true)
#225 := [rewrite]: #232
#237 := [monotonicity #225]: #236
#235 := [trans #237 #51]: #238
#343 := [monotonicity #235]: #212
#224 := [trans #343 #223]: #212
#556 := [quant-inst #3]: #554
#557 := [mp #556 #224]: #218
#559 := [unit-resolution #557 #575 #558]: false
#560 := [lemma #559]: #23
#64 := (or #74 #75)
#52 := (and #21 #23)
#55 := (not #52)
#81 := (iff #55 #64)
#65 := (not #64)
#76 := (not #65)
#79 := (iff #76 #64)
#80 := [rewrite]: #79
#77 := (iff #55 #76)
#66 := (iff #52 #65)
#67 := [rewrite]: #66
#78 := [monotonicity #67]: #77
#82 := [trans #78 #80]: #81
#25 := (and #21 #24)
#26 := (not #25)
#56 := (iff #26 #55)
#53 := (iff #25 #52)
#54 := [monotonicity #51]: #53
#57 := [monotonicity #54]: #56
#49 := [asserted]: #26
#60 := [mp #49 #57]: #55
#83 := [mp #60 #82]: #64
#555 := [unit-resolution #83 #560]: #74
#8 := (:var 0 S2)
#9 := (f3 f4 #8)
#562 := (pattern #9)
#10 := (= #9 #8)
#563 := (forall (vars (?v0 S2)) (:pat #562) #10)
#11 := (forall (vars (?v0 S2)) #10)
#566 := (iff #11 #563)
#564 := (iff #10 #10)
#565 := [refl]: #564
#567 := [quant-intro #565]: #566
#70 := (~ #11 #11)
#68 := (~ #10 #10)
#69 := [refl]: #68
#71 := [nnf-pos #69]: #70
#47 := [asserted]: #11
#59 := [mp~ #47 #71]: #11
#568 := [mp #59 #567]: #563
#551 := (not #563)
#210 := (or #551 #21)
#215 := [quant-inst #19]: #210
[unit-resolution #215 #568 #555]: false
unsat
d9c8c0d6c38991be073d0ed9988535642e4f47a6 396 0
#2 := false
decl f12 :: (-> S9 S10 S4)
decl f14 :: (-> S1 S10)
decl f1 :: S1
#3 := f1
#120 := (f14 f1)
decl f13 :: S9
#19 := f13
#121 := (f12 f13 #120)
decl f3 :: (-> S2 S3 S4)
decl f5 :: (-> Int S3)
#117 := 3::Int
#118 := (f5 3::Int)
decl f4 :: S2
#7 := f4
#119 := (f3 f4 #118)
#122 := (= #119 #121)
decl f15 :: (-> S11 S12 S4)
decl f17 :: (-> S13 S12 S12)
decl f20 :: S12
#26 := f20
decl f18 :: (-> S14 S1 S13)
decl f19 :: S14
#24 := f19
#513 := (f18 f19 f1)
#514 := (f17 #513 f20)
decl f16 :: S11
#23 := f16
#495 := (f15 f16 #514)
#626 := (= #495 #121)
#831 := (= #121 #495)
#20 := (:var 0 S1)
#25 := (f18 f19 #20)
#848 := (pattern #25)
#21 := (f14 #20)
#847 := (pattern #21)
#27 := (f17 #25 f20)
#28 := (f15 f16 #27)
#22 := (f12 f13 #21)
#29 := (= #22 #28)
#849 := (forall (vars (?v0 S1)) (:pat #847 #848) #29)
#30 := (forall (vars (?v0 S1)) #29)
#852 := (iff #30 #849)
#850 := (iff #29 #29)
#851 := [refl]: #850
#853 := [quant-intro #851]: #852
#302 := (~ #30 #30)
#301 := (~ #29 #29)
#346 := [refl]: #301
#303 := [nnf-pos #346]: #302
#159 := [asserted]: #30
#347 := [mp~ #159 #303]: #30
#854 := [mp #347 #853]: #849
#620 := (not #849)
#827 := (or #620 #831)
#500 := [quant-inst #3]: #827
#646 := [unit-resolution #500 #854]: #831
#627 := [symm #646]: #626
#636 := (= #119 #495)
decl f23 :: S11
#43 := f23
#524 := (f15 f23 #514)
#617 := (= #524 #495)
#802 := (= #495 #524)
#41 := (:var 0 S12)
#44 := (f15 f23 #41)
#856 := (pattern #44)
#42 := (f15 f16 #41)
#855 := (pattern #42)
#45 := (= #42 #44)
#857 := (forall (vars (?v0 S12)) (:pat #855 #856) #45)
#46 := (forall (vars (?v0 S12)) #45)
#860 := (iff #46 #857)
#858 := (iff #45 #45)
#859 := [refl]: #858
#861 := [quant-intro #859]: #860
#304 := (~ #46 #46)
#348 := (~ #45 #45)
#349 := [refl]: #348
#305 := [nnf-pos #349]: #304
#164 := [asserted]: #46
#312 := [mp~ #164 #305]: #46
#862 := [mp #312 #861]: #857
#834 := (not #857)
#805 := (or #834 #802)
#794 := [quant-inst #514]: #805
#645 := [unit-resolution #794 #862]: #802
#624 := [symm #645]: #617
#635 := (= #119 #524)
decl f27 :: (-> S17 Int S4)
decl f31 :: (-> S19 S4 Int)
#101 := (f15 f23 f20)
decl f32 :: S19
#74 := f32
#804 := (f31 f32 #101)
#80 := 1::Int
#801 := (+ 1::Int #804)
decl f28 :: S17
#57 := f28
#795 := (f27 f28 #801)
#655 := (= #795 #524)
#796 := (= #524 #795)
#70 := (:var 1 S1)
#71 := (f18 f19 #70)
#72 := (f17 #71 #41)
#899 := (pattern #72)
#106 := (f31 f32 #44)
#214 := (+ 1::Int #106)
#219 := (f27 f28 #214)
#105 := (f15 f23 #72)
#222 := (= #105 #219)
#900 := (forall (vars (?v0 S1) (?v1 S12)) (:pat #899) #222)
#225 := (forall (vars (?v0 S1) (?v1 S12)) #222)
#903 := (iff #225 #900)
#901 := (iff #222 #222)
#902 := [refl]: #901
#904 := [quant-intro #902]: #903
#324 := (~ #225 #225)
#358 := (~ #222 #222)
#359 := [refl]: #358
#325 := [nnf-pos #359]: #324
#58 := 0::Int
#81 := (+ 0::Int 1::Int)
#107 := (+ #106 #81)
#108 := (f27 f28 #107)
#109 := (= #105 #108)
#110 := (forall (vars (?v0 S1) (?v1 S12)) #109)
#226 := (iff #110 #225)
#223 := (iff #109 #222)
#220 := (= #108 #219)
#217 := (= #107 #214)
#211 := (+ #106 1::Int)
#215 := (= #211 #214)
#216 := [rewrite]: #215
#212 := (= #107 #211)
#169 := (= #81 1::Int)
#170 := [rewrite]: #169
#213 := [monotonicity #170]: #212
#218 := [trans #213 #216]: #217
#221 := [monotonicity #218]: #220
#224 := [monotonicity #221]: #223
#227 := [quant-intro #224]: #226
#210 := [asserted]: #110
#230 := [mp #210 #227]: #225
#328 := [mp~ #230 #325]: #225
#905 := [mp #328 #904]: #900
#797 := (not #900)
#798 := (or #797 #796)
#793 := [quant-inst #3 #26]: #798
#644 := [unit-resolution #793 #905]: #796
#616 := [symm #644]: #655
#633 := (= #119 #795)
decl f6 :: (-> S5 S6 S4)
decl f11 :: S6
#14 := f11
decl f24 :: S5
#49 := f24
#103 := (f6 f24 f11)
#810 := (f31 f32 #103)
#807 := (+ 1::Int #810)
#522 := (f27 f28 #807)
#654 := (= #522 #795)
#648 := (= #795 #522)
#638 := (= #801 #807)
#682 := (= 1::Int #807)
#689 := (= #807 1::Int)
#792 := (<= #810 0::Int)
#791 := (= #810 0::Int)
#59 := (f27 f28 0::Int)
#487 := (f31 f32 #59)
#492 := (= #487 0::Int)
#8 := (:var 0 Int)
#130 := (f27 f28 #8)
#920 := (pattern #130)
#131 := (f31 f32 #130)
#132 := (= #131 #8)
#260 := (>= #8 0::Int)
#261 := (not #260)
#264 := (or #261 #132)
#921 := (forall (vars (?v0 Int)) (:pat #920) #264)
#267 := (forall (vars (?v0 Int)) #264)
#924 := (iff #267 #921)
#922 := (iff #264 #264)
#923 := [refl]: #922
#925 := [quant-intro #923]: #924
#336 := (~ #267 #267)
#335 := (~ #264 #264)
#362 := [refl]: #335
#337 := [nnf-pos #362]: #336
#129 := (<= 0::Int #8)
#133 := (implies #129 #132)
#134 := (forall (vars (?v0 Int)) #133)
#270 := (iff #134 #267)
#251 := (not #129)
#252 := (or #251 #132)
#255 := (forall (vars (?v0 Int)) #252)
#268 := (iff #255 #267)
#265 := (iff #252 #264)
#262 := (iff #251 #261)
#258 := (iff #129 #260)
#259 := [rewrite]: #258
#263 := [monotonicity #259]: #262
#266 := [monotonicity #263]: #265
#269 := [quant-intro #266]: #268
#256 := (iff #134 #255)
#253 := (iff #133 #252)
#254 := [rewrite]: #253
#257 := [quant-intro #254]: #256
#271 := [trans #257 #269]: #270
#250 := [asserted]: #134
#272 := [mp #250 #271]: #267
#363 := [mp~ #272 #337]: #267
#926 := [mp #363 #925]: #921
#822 := (not #921)
#824 := (or #822 #492)
#501 := (>= 0::Int 0::Int)
#837 := (not #501)
#829 := (or #837 #492)
#463 := (or #822 #829)
#825 := (iff #463 #824)
#826 := (iff #824 #824)
#812 := [rewrite]: #826
#821 := (iff #829 #492)
#817 := (or false #492)
#820 := (iff #817 #492)
#815 := [rewrite]: #820
#818 := (iff #829 #817)
#479 := (iff #837 false)
#1 := true
#472 := (not true)
#477 := (iff #472 false)
#478 := [rewrite]: #477
#814 := (iff #837 #472)
#488 := (iff #501 true)
#830 := [rewrite]: #488
#476 := [monotonicity #830]: #814
#816 := [trans #476 #478]: #479
#819 := [monotonicity #816]: #818
#458 := [trans #819 #815]: #821
#823 := [monotonicity #458]: #825
#813 := [trans #823 #812]: #825
#464 := [quant-inst #58]: #463
#520 := [mp #464 #813]: #824
#696 := [unit-resolution #520 #926]: #492
#697 := (= #810 #487)
#104 := (= #103 #59)
#208 := [asserted]: #104
#700 := [monotonicity #208]: #697
#701 := [trans #700 #696]: #791
#702 := (not #791)
#698 := (or #702 #792)
#703 := [th-lemma arith triangle-eq]: #698
#683 := [unit-resolution #703 #701]: #792
#799 := (>= #810 0::Int)
#629 := (or #702 #799)
#684 := [th-lemma arith triangle-eq]: #629
#665 := [unit-resolution #684 #701]: #799
#690 := [th-lemma arith eq-propagate -1 -1 #665 #683]: #689
#637 := [symm #690]: #682
#681 := (= #801 1::Int)
#641 := (<= #804 0::Int)
#640 := (= #804 0::Int)
#659 := (= #804 #487)
#102 := (= #101 #59)
#207 := [asserted]: #102
#666 := [monotonicity #207]: #659
#625 := [trans #666 #696]: #640
#656 := (not #640)
#658 := (or #656 #641)
#660 := [th-lemma arith triangle-eq]: #658
#667 := [unit-resolution #660 #625]: #641
#642 := (>= #804 0::Int)
#669 := (or #656 #642)
#670 := [th-lemma arith triangle-eq]: #669
#671 := [unit-resolution #670 #625]: #642
#661 := [th-lemma arith eq-propagate -1 -1 #671 #667]: #681
#643 := [trans #661 #637]: #638
#649 := [monotonicity #643]: #648
#639 := [symm #649]: #654
#631 := (= #119 #522)
decl f8 :: (-> S7 S6 S6)
decl f9 :: (-> S8 Int S7)
decl f10 :: S8
#12 := f10
#509 := (f9 f10 3::Int)
#510 := (f8 #509 f11)
#532 := (f6 f24 #510)
#523 := (= #532 #522)
#47 := (:var 0 S6)
#88 := (:var 1 Int)
#89 := (f9 f10 #88)
#90 := (f8 #89 #47)
#906 := (pattern #90)
#50 := (f6 f24 #47)
#112 := (f31 f32 #50)
#233 := (+ 1::Int #112)
#238 := (f27 f28 #233)
#111 := (f6 f24 #90)
#241 := (= #111 #238)
#907 := (forall (vars (?v0 Int) (?v1 S6)) (:pat #906) #241)
#244 := (forall (vars (?v0 Int) (?v1 S6)) #241)
#910 := (iff #244 #907)
#908 := (iff #241 #241)
#909 := [refl]: #908
#911 := [quant-intro #909]: #910
#330 := (~ #244 #244)
#329 := (~ #241 #241)
#326 := [refl]: #329
#331 := [nnf-pos #326]: #330
#113 := (+ #112 #81)
#114 := (f27 f28 #113)
#115 := (= #111 #114)
#116 := (forall (vars (?v0 Int) (?v1 S6)) #115)
#245 := (iff #116 #244)
#242 := (iff #115 #241)
#239 := (= #114 #238)
#236 := (= #113 #233)
#229 := (+ #112 1::Int)
#234 := (= #229 #233)
#235 := [rewrite]: #234
#231 := (= #113 #229)
#232 := [monotonicity #170]: #231
#237 := [trans #232 #235]: #236
#240 := [monotonicity #237]: #239
#243 := [monotonicity #240]: #242
#246 := [quant-intro #243]: #245
#228 := [asserted]: #116
#249 := [mp #228 #246]: #244
#327 := [mp~ #249 #331]: #244
#912 := [mp #327 #911]: #907
#803 := (not #907)
#517 := (or #803 #523)
#800 := [quant-inst #117 #14]: #517
#694 := [unit-resolution #800 #912]: #523
#628 := (= #119 #532)
decl f7 :: S5
#11 := f7
#511 := (f6 f7 #510)
#806 := (= #511 #532)
#864 := (pattern #50)
#48 := (f6 f7 #47)
#863 := (pattern #48)
#51 := (= #48 #50)
#865 := (forall (vars (?v0 S6)) (:pat #863 #864) #51)
#52 := (forall (vars (?v0 S6)) #51)
#868 := (iff #52 #865)
#866 := (iff #51 #51)
#867 := [refl]: #866
#869 := [quant-intro #867]: #868
#314 := (~ #52 #52)
#313 := (~ #51 #51)
#310 := [refl]: #313
#315 := [nnf-pos #310]: #314
#165 := [asserted]: #52
#311 := [mp~ #165 #315]: #52
#870 := [mp #311 #869]: #865
#832 := (not #865)
#811 := (or #832 #806)
#521 := [quant-inst #510]: #811
#693 := [unit-resolution #521 #870]: #806
#502 := (= #119 #511)
#13 := (f9 f10 #8)
#840 := (pattern #13)
#9 := (f5 #8)
#839 := (pattern #9)
#15 := (f8 #13 f11)
#16 := (f6 f7 #15)
#10 := (f3 f4 #9)
#17 := (= #10 #16)
#841 := (forall (vars (?v0 Int)) (:pat #839 #840) #17)
#18 := (forall (vars (?v0 Int)) #17)
#844 := (iff #18 #841)
#842 := (iff #17 #17)
#843 := [refl]: #842
#845 := [quant-intro #843]: #844
#344 := (~ #18 #18)
#342 := (~ #17 #17)
#343 := [refl]: #342
#345 := [nnf-pos #343]: #344
#158 := [asserted]: #18
#300 := [mp~ #158 #345]: #18
#846 := [mp #300 #845]: #841
#515 := (not #841)
#512 := (or #515 #502)
#516 := [quant-inst #117]: #512
#647 := [unit-resolution #516 #846]: #502
#630 := [trans #647 #693]: #628
#632 := [trans #630 #694]: #631
#634 := [trans #632 #639]: #633
#618 := [trans #634 #616]: #635
#606 := [trans #618 #624]: #636
#607 := [trans #606 #627]: #122
#123 := (not #122)
#247 := [asserted]: #123
[unit-resolution #247 #607]: false
unsat