3292 val!5 -> val!6 |
3292 val!5 -> val!6 |
3293 val!4 -> val!7 |
3293 val!4 -> val!7 |
3294 else -> val!7 |
3294 else -> val!7 |
3295 } |
3295 } |
3296 sat |
3296 sat |
|
3297 qkVrmXMcHAG5MLuJ9d8jXQ 211 0 |
|
3298 #2 := false |
|
3299 #33 := 0::real |
|
3300 decl uf_11 :: (-> T5 T6 real) |
|
3301 decl uf_15 :: T6 |
|
3302 #28 := uf_15 |
|
3303 decl uf_16 :: T5 |
|
3304 #30 := uf_16 |
|
3305 #31 := (uf_11 uf_16 uf_15) |
|
3306 decl uf_12 :: (-> T7 T8 T5) |
|
3307 decl uf_14 :: T8 |
|
3308 #26 := uf_14 |
|
3309 decl uf_13 :: (-> T1 T7) |
|
3310 decl uf_8 :: T1 |
|
3311 #16 := uf_8 |
|
3312 #25 := (uf_13 uf_8) |
|
3313 #27 := (uf_12 #25 uf_14) |
|
3314 #29 := (uf_11 #27 uf_15) |
|
3315 #73 := -1::real |
|
3316 #84 := (* -1::real #29) |
|
3317 #85 := (+ #84 #31) |
|
3318 #74 := (* -1::real #31) |
|
3319 #75 := (+ #29 #74) |
|
3320 #112 := (>= #75 0::real) |
|
3321 #119 := (ite #112 #75 #85) |
|
3322 #127 := (* -1::real #119) |
|
3323 decl uf_17 :: T5 |
|
3324 #37 := uf_17 |
|
3325 #38 := (uf_11 uf_17 uf_15) |
|
3326 #102 := -1/3::real |
|
3327 #103 := (* -1/3::real #38) |
|
3328 #128 := (+ #103 #127) |
|
3329 #100 := 1/3::real |
|
3330 #101 := (* 1/3::real #31) |
|
3331 #129 := (+ #101 #128) |
|
3332 #130 := (<= #129 0::real) |
|
3333 #131 := (not #130) |
|
3334 #40 := 3::real |
|
3335 #39 := (- #31 #38) |
|
3336 #41 := (/ #39 3::real) |
|
3337 #32 := (- #29 #31) |
|
3338 #35 := (- #32) |
|
3339 #34 := (< #32 0::real) |
|
3340 #36 := (ite #34 #35 #32) |
|
3341 #42 := (< #36 #41) |
|
3342 #136 := (iff #42 #131) |
|
3343 #104 := (+ #101 #103) |
|
3344 #78 := (< #75 0::real) |
|
3345 #90 := (ite #78 #85 #75) |
|
3346 #109 := (< #90 #104) |
|
3347 #134 := (iff #109 #131) |
|
3348 #124 := (< #119 #104) |
|
3349 #132 := (iff #124 #131) |
|
3350 #133 := [rewrite]: #132 |
|
3351 #125 := (iff #109 #124) |
|
3352 #122 := (= #90 #119) |
|
3353 #113 := (not #112) |
|
3354 #116 := (ite #113 #85 #75) |
|
3355 #120 := (= #116 #119) |
|
3356 #121 := [rewrite]: #120 |
|
3357 #117 := (= #90 #116) |
|
3358 #114 := (iff #78 #113) |
|
3359 #115 := [rewrite]: #114 |
|
3360 #118 := [monotonicity #115]: #117 |
|
3361 #123 := [trans #118 #121]: #122 |
|
3362 #126 := [monotonicity #123]: #125 |
|
3363 #135 := [trans #126 #133]: #134 |
|
3364 #110 := (iff #42 #109) |
|
3365 #107 := (= #41 #104) |
|
3366 #93 := (* -1::real #38) |
|
3367 #94 := (+ #31 #93) |
|
3368 #97 := (/ #94 3::real) |
|
3369 #105 := (= #97 #104) |
|
3370 #106 := [rewrite]: #105 |
|
3371 #98 := (= #41 #97) |
|
3372 #95 := (= #39 #94) |
|
3373 #96 := [rewrite]: #95 |
|
3374 #99 := [monotonicity #96]: #98 |
|
3375 #108 := [trans #99 #106]: #107 |
|
3376 #91 := (= #36 #90) |
|
3377 #76 := (= #32 #75) |
|
3378 #77 := [rewrite]: #76 |
|
3379 #88 := (= #35 #85) |
|
3380 #81 := (- #75) |
|
3381 #86 := (= #81 #85) |
|
3382 #87 := [rewrite]: #86 |
|
3383 #82 := (= #35 #81) |
|
3384 #83 := [monotonicity #77]: #82 |
|
3385 #89 := [trans #83 #87]: #88 |
|
3386 #79 := (iff #34 #78) |
|
3387 #80 := [monotonicity #77]: #79 |
|
3388 #92 := [monotonicity #80 #89 #77]: #91 |
|
3389 #111 := [monotonicity #92 #108]: #110 |
|
3390 #137 := [trans #111 #135]: #136 |
|
3391 #72 := [asserted]: #42 |
|
3392 #138 := [mp #72 #137]: #131 |
|
3393 decl uf_1 :: T1 |
|
3394 #4 := uf_1 |
|
3395 #43 := (uf_13 uf_1) |
|
3396 #44 := (uf_12 #43 uf_14) |
|
3397 #45 := (uf_11 #44 uf_15) |
|
3398 #149 := (* -1::real #45) |
|
3399 #150 := (+ #38 #149) |
|
3400 #140 := (+ #93 #45) |
|
3401 #161 := (<= #150 0::real) |
|
3402 #168 := (ite #161 #140 #150) |
|
3403 #176 := (* -1::real #168) |
|
3404 #177 := (+ #103 #176) |
|
3405 #178 := (+ #101 #177) |
|
3406 #179 := (<= #178 0::real) |
|
3407 #180 := (not #179) |
|
3408 #46 := (- #45 #38) |
|
3409 #48 := (- #46) |
|
3410 #47 := (< #46 0::real) |
|
3411 #49 := (ite #47 #48 #46) |
|
3412 #50 := (< #49 #41) |
|
3413 #185 := (iff #50 #180) |
|
3414 #143 := (< #140 0::real) |
|
3415 #155 := (ite #143 #150 #140) |
|
3416 #158 := (< #155 #104) |
|
3417 #183 := (iff #158 #180) |
|
3418 #173 := (< #168 #104) |
|
3419 #181 := (iff #173 #180) |
|
3420 #182 := [rewrite]: #181 |
|
3421 #174 := (iff #158 #173) |
|
3422 #171 := (= #155 #168) |
|
3423 #162 := (not #161) |
|
3424 #165 := (ite #162 #150 #140) |
|
3425 #169 := (= #165 #168) |
|
3426 #170 := [rewrite]: #169 |
|
3427 #166 := (= #155 #165) |
|
3428 #163 := (iff #143 #162) |
|
3429 #164 := [rewrite]: #163 |
|
3430 #167 := [monotonicity #164]: #166 |
|
3431 #172 := [trans #167 #170]: #171 |
|
3432 #175 := [monotonicity #172]: #174 |
|
3433 #184 := [trans #175 #182]: #183 |
|
3434 #159 := (iff #50 #158) |
|
3435 #156 := (= #49 #155) |
|
3436 #141 := (= #46 #140) |
|
3437 #142 := [rewrite]: #141 |
|
3438 #153 := (= #48 #150) |
|
3439 #146 := (- #140) |
|
3440 #151 := (= #146 #150) |
|
3441 #152 := [rewrite]: #151 |
|
3442 #147 := (= #48 #146) |
|
3443 #148 := [monotonicity #142]: #147 |
|
3444 #154 := [trans #148 #152]: #153 |
|
3445 #144 := (iff #47 #143) |
|
3446 #145 := [monotonicity #142]: #144 |
|
3447 #157 := [monotonicity #145 #154 #142]: #156 |
|
3448 #160 := [monotonicity #157 #108]: #159 |
|
3449 #186 := [trans #160 #184]: #185 |
|
3450 #139 := [asserted]: #50 |
|
3451 #187 := [mp #139 #186]: #180 |
|
3452 #299 := (+ #140 #176) |
|
3453 #300 := (<= #299 0::real) |
|
3454 #290 := (= #140 #168) |
|
3455 #329 := [hypothesis]: #162 |
|
3456 #191 := (+ #29 #149) |
|
3457 #192 := (<= #191 0::real) |
|
3458 #51 := (<= #29 #45) |
|
3459 #193 := (iff #51 #192) |
|
3460 #194 := [rewrite]: #193 |
|
3461 #188 := [asserted]: #51 |
|
3462 #195 := [mp #188 #194]: #192 |
|
3463 #298 := (+ #75 #127) |
|
3464 #301 := (<= #298 0::real) |
|
3465 #284 := (= #75 #119) |
|
3466 #302 := [hypothesis]: #113 |
|
3467 #296 := (+ #85 #127) |
|
3468 #297 := (<= #296 0::real) |
|
3469 #285 := (= #85 #119) |
|
3470 #288 := (or #112 #285) |
|
3471 #289 := [def-axiom]: #288 |
|
3472 #303 := [unit-resolution #289 #302]: #285 |
|
3473 #304 := (not #285) |
|
3474 #305 := (or #304 #297) |
|
3475 #306 := [th-lemma]: #305 |
|
3476 #307 := [unit-resolution #306 #303]: #297 |
|
3477 #315 := (not #290) |
|
3478 #310 := (not #300) |
|
3479 #311 := (or #310 #112) |
|
3480 #308 := [hypothesis]: #300 |
|
3481 #309 := [th-lemma #308 #307 #138 #302 #187 #195]: false |
|
3482 #312 := [lemma #309]: #311 |
|
3483 #322 := [unit-resolution #312 #302]: #310 |
|
3484 #316 := (or #315 #300) |
|
3485 #313 := [hypothesis]: #310 |
|
3486 #314 := [hypothesis]: #290 |
|
3487 #317 := [th-lemma]: #316 |
|
3488 #318 := [unit-resolution #317 #314 #313]: false |
|
3489 #319 := [lemma #318]: #316 |
|
3490 #323 := [unit-resolution #319 #322]: #315 |
|
3491 #292 := (or #162 #290) |
|
3492 #293 := [def-axiom]: #292 |
|
3493 #324 := [unit-resolution #293 #323]: #162 |
|
3494 #325 := [th-lemma #324 #307 #138 #302 #195]: false |
|
3495 #326 := [lemma #325]: #112 |
|
3496 #286 := (or #113 #284) |
|
3497 #287 := [def-axiom]: #286 |
|
3498 #330 := [unit-resolution #287 #326]: #284 |
|
3499 #331 := (not #284) |
|
3500 #332 := (or #331 #301) |
|
3501 #333 := [th-lemma]: #332 |
|
3502 #334 := [unit-resolution #333 #330]: #301 |
|
3503 #335 := [th-lemma #326 #334 #195 #329 #138]: false |
|
3504 #336 := [lemma #335]: #161 |
|
3505 #327 := [unit-resolution #293 #336]: #290 |
|
3506 #328 := [unit-resolution #319 #327]: #300 |
|
3507 [th-lemma #326 #334 #195 #328 #187 #138]: false |
|
3508 unsat |