475 #552 := [mp #61 #551]: #547 |
475 #552 := [mp #61 #551]: #547 |
476 #130 := (not #547) |
476 #130 := (not #547) |
477 #216 := (or #130 #23) |
477 #216 := (or #130 #23) |
478 #131 := [quant-inst #16 #19]: #216 |
478 #131 := [quant-inst #16 #19]: #216 |
479 [unit-resolution #131 #552 #62]: false |
479 [unit-resolution #131 #552 #62]: false |
|
480 unsat |
|
481 53042978396971446eabf6039172bd47071e3fd3 67 0 |
|
482 #2 := false |
|
483 decl f1 :: S1 |
|
484 #3 := f1 |
|
485 decl f3 :: (-> Int S1) |
|
486 decl ?v0!0 :: Int |
|
487 #55 := ?v0!0 |
|
488 #56 := (f3 ?v0!0) |
|
489 #57 := (= #56 f1) |
|
490 #58 := (not #57) |
|
491 decl ?v1!1 :: Int |
|
492 #66 := ?v1!1 |
|
493 #67 := (f3 ?v1!1) |
|
494 #68 := (= #67 f1) |
|
495 #69 := (or #57 #68) |
|
496 #70 := (not #69) |
|
497 #86 := (and #57 #70) |
|
498 #63 := (not #58) |
|
499 #76 := (and #63 #70) |
|
500 #87 := (iff #76 #86) |
|
501 #84 := (iff #63 #57) |
|
502 #85 := [rewrite]: #84 |
|
503 #88 := [monotonicity #85]: #87 |
|
504 #7 := (:var 0 Int) |
|
505 #8 := (f3 #7) |
|
506 #9 := (= #8 f1) |
|
507 #10 := (:var 1 Int) |
|
508 #11 := (f3 #10) |
|
509 #12 := (= #11 f1) |
|
510 #13 := (or #12 #9) |
|
511 #14 := (forall (vars (?v1 Int)) #13) |
|
512 #39 := (not #9) |
|
513 #40 := (or #39 #14) |
|
514 #43 := (forall (vars (?v0 Int)) #40) |
|
515 #46 := (not #43) |
|
516 #79 := (~ #46 #76) |
|
517 #50 := (or #57 #9) |
|
518 #52 := (forall (vars (?v1 Int)) #50) |
|
519 #59 := (or #58 #52) |
|
520 #60 := (not #59) |
|
521 #77 := (~ #60 #76) |
|
522 #71 := (not #52) |
|
523 #72 := (~ #71 #70) |
|
524 #73 := [sk]: #72 |
|
525 #64 := (~ #63 #63) |
|
526 #65 := [refl]: #64 |
|
527 #78 := [nnf-neg #65 #73]: #77 |
|
528 #61 := (~ #46 #60) |
|
529 #62 := [sk]: #61 |
|
530 #80 := [trans #62 #78]: #79 |
|
531 #15 := (implies #9 #14) |
|
532 #16 := (forall (vars (?v0 Int)) #15) |
|
533 #17 := (not #16) |
|
534 #47 := (iff #17 #46) |
|
535 #44 := (iff #16 #43) |
|
536 #41 := (iff #15 #40) |
|
537 #42 := [rewrite]: #41 |
|
538 #45 := [quant-intro #42]: #44 |
|
539 #48 := [monotonicity #45]: #47 |
|
540 #38 := [asserted]: #17 |
|
541 #51 := [mp #38 #48]: #46 |
|
542 #81 := [mp~ #51 #80]: #76 |
|
543 #82 := [mp #81 #88]: #86 |
|
544 #89 := [and-elim #82]: #70 |
|
545 #90 := [not-or-elim #89]: #58 |
|
546 #83 := [and-elim #82]: #57 |
|
547 [unit-resolution #83 #90]: false |
480 unsat |
548 unsat |
481 d97439af6f5bc7794ab403d0f6cc318d103016a1 1288 0 |
549 d97439af6f5bc7794ab403d0f6cc318d103016a1 1288 0 |
482 #2 := false |
550 #2 := false |
483 decl f1 :: S1 |
551 decl f1 :: S1 |
484 #3 := f1 |
552 #3 := f1 |
1765 #1530 := [unit-resolution #788 #1529]: #47 |
1833 #1530 := [unit-resolution #788 #1529]: #47 |
1766 #1531 := [unit-resolution #623 #1530]: #214 |
1834 #1531 := [unit-resolution #623 #1530]: #214 |
1767 #1532 := [unit-resolution #769 #1531]: #20 |
1835 #1532 := [unit-resolution #769 #1531]: #20 |
1768 [unit-resolution #606 #1532 #1528]: false |
1836 [unit-resolution #606 #1532 #1528]: false |
1769 unsat |
1837 unsat |
1770 53042978396971446eabf6039172bd47071e3fd3 67 0 |
|
1771 #2 := false |
|
1772 decl f1 :: S1 |
|
1773 #3 := f1 |
|
1774 decl f3 :: (-> Int S1) |
|
1775 decl ?v0!0 :: Int |
|
1776 #55 := ?v0!0 |
|
1777 #56 := (f3 ?v0!0) |
|
1778 #57 := (= #56 f1) |
|
1779 #58 := (not #57) |
|
1780 decl ?v1!1 :: Int |
|
1781 #66 := ?v1!1 |
|
1782 #67 := (f3 ?v1!1) |
|
1783 #68 := (= #67 f1) |
|
1784 #69 := (or #57 #68) |
|
1785 #70 := (not #69) |
|
1786 #86 := (and #57 #70) |
|
1787 #63 := (not #58) |
|
1788 #76 := (and #63 #70) |
|
1789 #87 := (iff #76 #86) |
|
1790 #84 := (iff #63 #57) |
|
1791 #85 := [rewrite]: #84 |
|
1792 #88 := [monotonicity #85]: #87 |
|
1793 #7 := (:var 0 Int) |
|
1794 #8 := (f3 #7) |
|
1795 #9 := (= #8 f1) |
|
1796 #10 := (:var 1 Int) |
|
1797 #11 := (f3 #10) |
|
1798 #12 := (= #11 f1) |
|
1799 #13 := (or #12 #9) |
|
1800 #14 := (forall (vars (?v1 Int)) #13) |
|
1801 #39 := (not #9) |
|
1802 #40 := (or #39 #14) |
|
1803 #43 := (forall (vars (?v0 Int)) #40) |
|
1804 #46 := (not #43) |
|
1805 #79 := (~ #46 #76) |
|
1806 #50 := (or #57 #9) |
|
1807 #52 := (forall (vars (?v1 Int)) #50) |
|
1808 #59 := (or #58 #52) |
|
1809 #60 := (not #59) |
|
1810 #77 := (~ #60 #76) |
|
1811 #71 := (not #52) |
|
1812 #72 := (~ #71 #70) |
|
1813 #73 := [sk]: #72 |
|
1814 #64 := (~ #63 #63) |
|
1815 #65 := [refl]: #64 |
|
1816 #78 := [nnf-neg #65 #73]: #77 |
|
1817 #61 := (~ #46 #60) |
|
1818 #62 := [sk]: #61 |
|
1819 #80 := [trans #62 #78]: #79 |
|
1820 #15 := (implies #9 #14) |
|
1821 #16 := (forall (vars (?v0 Int)) #15) |
|
1822 #17 := (not #16) |
|
1823 #47 := (iff #17 #46) |
|
1824 #44 := (iff #16 #43) |
|
1825 #41 := (iff #15 #40) |
|
1826 #42 := [rewrite]: #41 |
|
1827 #45 := [quant-intro #42]: #44 |
|
1828 #48 := [monotonicity #45]: #47 |
|
1829 #38 := [asserted]: #17 |
|
1830 #51 := [mp #38 #48]: #46 |
|
1831 #81 := [mp~ #51 #80]: #76 |
|
1832 #82 := [mp #81 #88]: #86 |
|
1833 #89 := [and-elim #82]: #70 |
|
1834 #90 := [not-or-elim #89]: #58 |
|
1835 #83 := [and-elim #82]: #57 |
|
1836 [unit-resolution #83 #90]: false |
|
1837 unsat |
|
1838 a69a9e8c5e31ec6b9da4cf96f47b52cf6b9404d9 117 0 |
1838 a69a9e8c5e31ec6b9da4cf96f47b52cf6b9404d9 117 0 |
1839 #2 := false |
1839 #2 := false |
1840 decl f3 :: (-> S3 S2 S1) |
1840 decl f3 :: (-> S3 S2 S1) |
1841 #10 := (:var 0 S2) |
1841 #10 := (:var 0 S2) |
1842 decl f4 :: (-> S4 S1 S3) |
1842 decl f4 :: (-> S4 S1 S3) |
2069 #612 := (or #275 #31 #616) |
2069 #612 := (or #275 #31 #616) |
2070 #271 := [def-axiom]: #612 |
2070 #271 := [def-axiom]: #612 |
2071 #603 := [unit-resolution #271 #618]: #602 |
2071 #603 := [unit-resolution #271 #618]: #602 |
2072 [unit-resolution #603 #601 #297]: false |
2072 [unit-resolution #603 #601 #297]: false |
2073 unsat |
2073 unsat |
|
2074 0ce3a745d60cdbf0fe26b07c5e76de09d459dd25 17 0 |
|
2075 #2 := false |
|
2076 #7 := 3::Int |
|
2077 #8 := (= 3::Int 3::Int) |
|
2078 #9 := (not #8) |
|
2079 #38 := (iff #9 false) |
|
2080 #1 := true |
|
2081 #33 := (not true) |
|
2082 #36 := (iff #33 false) |
|
2083 #37 := [rewrite]: #36 |
|
2084 #34 := (iff #9 #33) |
|
2085 #31 := (iff #8 true) |
|
2086 #32 := [rewrite]: #31 |
|
2087 #35 := [monotonicity #32]: #34 |
|
2088 #39 := [trans #35 #37]: #38 |
|
2089 #30 := [asserted]: #9 |
|
2090 [mp #30 #39]: false |
|
2091 unsat |
2074 5c792581e65682628e5c59ca9f3f8801e6aeba72 61 0 |
2092 5c792581e65682628e5c59ca9f3f8801e6aeba72 61 0 |
2075 #2 := false |
2093 #2 := false |
2076 decl f1 :: S1 |
2094 decl f1 :: S1 |
2077 #3 := f1 |
2095 #3 := f1 |
2078 decl f3 :: (-> S2 S1) |
2096 decl f3 :: (-> S2 S1) |
2130 #556 := [mp #57 #555]: #551 |
2148 #556 := [mp #57 #555]: #551 |
2131 #135 := (not #551) |
2149 #135 := (not #551) |
2132 #221 := (or #135 #45) |
2150 #221 := (or #135 #45) |
2133 #136 := [quant-inst #7]: #221 |
2151 #136 := [quant-inst #7]: #221 |
2134 [unit-resolution #136 #556 #52]: false |
2152 [unit-resolution #136 #556 #52]: false |
2135 unsat |
|
2136 0ce3a745d60cdbf0fe26b07c5e76de09d459dd25 17 0 |
|
2137 #2 := false |
|
2138 #7 := 3::Int |
|
2139 #8 := (= 3::Int 3::Int) |
|
2140 #9 := (not #8) |
|
2141 #38 := (iff #9 false) |
|
2142 #1 := true |
|
2143 #33 := (not true) |
|
2144 #36 := (iff #33 false) |
|
2145 #37 := [rewrite]: #36 |
|
2146 #34 := (iff #9 #33) |
|
2147 #31 := (iff #8 true) |
|
2148 #32 := [rewrite]: #31 |
|
2149 #35 := [monotonicity #32]: #34 |
|
2150 #39 := [trans #35 #37]: #38 |
|
2151 #30 := [asserted]: #9 |
|
2152 [mp #30 #39]: false |
|
2153 unsat |
2153 unsat |
2154 1532b1dde71eb42ca0a012bb62d9bbadf37fa326 17 0 |
2154 1532b1dde71eb42ca0a012bb62d9bbadf37fa326 17 0 |
2155 #2 := false |
2155 #2 := false |
2156 #7 := 3::Real |
2156 #7 := 3::Real |
2157 #8 := (= 3::Real 3::Real) |
2157 #8 := (= 3::Real 3::Real) |
3227 #225 := [not-or-elim #205]: #224 |
3227 #225 := [not-or-elim #205]: #224 |
3228 #362 := [mp #225 #361]: #351 |
3228 #362 := [mp #225 #361]: #351 |
3229 #496 := [unit-resolution #362 #495]: #104 |
3229 #496 := [unit-resolution #362 #495]: #104 |
3230 #497 := [unit-resolution #456 #496 #490]: #20 |
3230 #497 := [unit-resolution #456 #496 #490]: #20 |
3231 [unit-resolution #497 #501]: false |
3231 [unit-resolution #497 #501]: false |
|
3232 unsat |
|
3233 70bd6436662c1fd4b8c8a6f696914593051990e6 52 0 |
|
3234 #2 := false |
|
3235 #11 := 1::Real |
|
3236 decl f3 :: Real |
|
3237 #7 := f3 |
|
3238 #9 := 2::Real |
|
3239 #10 := (* 2::Real f3) |
|
3240 #12 := (+ #10 1::Real) |
|
3241 #8 := (+ f3 f3) |
|
3242 #13 := (< #8 #12) |
|
3243 #14 := (or false #13) |
|
3244 #15 := (or #13 #14) |
|
3245 #16 := (not #15) |
|
3246 #72 := (iff #16 false) |
|
3247 #40 := (+ 1::Real #10) |
|
3248 #43 := (< #10 #40) |
|
3249 #60 := (not #43) |
|
3250 #70 := (iff #60 false) |
|
3251 #1 := true |
|
3252 #65 := (not true) |
|
3253 #68 := (iff #65 false) |
|
3254 #69 := [rewrite]: #68 |
|
3255 #66 := (iff #60 #65) |
|
3256 #63 := (iff #43 true) |
|
3257 #64 := [rewrite]: #63 |
|
3258 #67 := [monotonicity #64]: #66 |
|
3259 #71 := [trans #67 #69]: #70 |
|
3260 #61 := (iff #16 #60) |
|
3261 #58 := (iff #15 #43) |
|
3262 #53 := (or #43 #43) |
|
3263 #56 := (iff #53 #43) |
|
3264 #57 := [rewrite]: #56 |
|
3265 #54 := (iff #15 #53) |
|
3266 #51 := (iff #14 #43) |
|
3267 #46 := (or false #43) |
|
3268 #49 := (iff #46 #43) |
|
3269 #50 := [rewrite]: #49 |
|
3270 #47 := (iff #14 #46) |
|
3271 #44 := (iff #13 #43) |
|
3272 #41 := (= #12 #40) |
|
3273 #42 := [rewrite]: #41 |
|
3274 #38 := (= #8 #10) |
|
3275 #39 := [rewrite]: #38 |
|
3276 #45 := [monotonicity #39 #42]: #44 |
|
3277 #48 := [monotonicity #45]: #47 |
|
3278 #52 := [trans #48 #50]: #51 |
|
3279 #55 := [monotonicity #45 #52]: #54 |
|
3280 #59 := [trans #55 #57]: #58 |
|
3281 #62 := [monotonicity #59]: #61 |
|
3282 #73 := [trans #62 #71]: #72 |
|
3283 #37 := [asserted]: #16 |
|
3284 [mp #37 #73]: false |
3232 unsat |
3285 unsat |
3233 6e7ef563e385e00340c905e5fb44172a278ff733 2215 0 |
3286 6e7ef563e385e00340c905e5fb44172a278ff733 2215 0 |
3234 #2 := false |
3287 #2 := false |
3235 decl f12 :: Int |
3288 decl f12 :: Int |
3236 #52 := f12 |
3289 #52 := f12 |
5443 #2261 := [unit-resolution #856 #2242]: #748 |
5496 #2261 := [unit-resolution #856 #2242]: #748 |
5444 #2262 := [unit-resolution #2119 #2261 #2042 #2260 #2239]: #738 |
5497 #2262 := [unit-resolution #2119 #2261 #2042 #2260 #2239]: #738 |
5445 #2263 := [unit-resolution #2122 #2248 #2251 #2024 #2260 #2243]: #739 |
5498 #2263 := [unit-resolution #2122 #2248 #2251 #2024 #2260 #2243]: #739 |
5446 #2264 := [unit-resolution #1544 #2263 #2262]: #65 |
5499 #2264 := [unit-resolution #1544 #2263 #2262]: #65 |
5447 [unit-resolution #658 #2264 #2259]: false |
5500 [unit-resolution #658 #2264 #2259]: false |
5448 unsat |
|
5449 70bd6436662c1fd4b8c8a6f696914593051990e6 52 0 |
|
5450 #2 := false |
|
5451 #11 := 1::Real |
|
5452 decl f3 :: Real |
|
5453 #7 := f3 |
|
5454 #9 := 2::Real |
|
5455 #10 := (* 2::Real f3) |
|
5456 #12 := (+ #10 1::Real) |
|
5457 #8 := (+ f3 f3) |
|
5458 #13 := (< #8 #12) |
|
5459 #14 := (or false #13) |
|
5460 #15 := (or #13 #14) |
|
5461 #16 := (not #15) |
|
5462 #72 := (iff #16 false) |
|
5463 #40 := (+ 1::Real #10) |
|
5464 #43 := (< #10 #40) |
|
5465 #60 := (not #43) |
|
5466 #70 := (iff #60 false) |
|
5467 #1 := true |
|
5468 #65 := (not true) |
|
5469 #68 := (iff #65 false) |
|
5470 #69 := [rewrite]: #68 |
|
5471 #66 := (iff #60 #65) |
|
5472 #63 := (iff #43 true) |
|
5473 #64 := [rewrite]: #63 |
|
5474 #67 := [monotonicity #64]: #66 |
|
5475 #71 := [trans #67 #69]: #70 |
|
5476 #61 := (iff #16 #60) |
|
5477 #58 := (iff #15 #43) |
|
5478 #53 := (or #43 #43) |
|
5479 #56 := (iff #53 #43) |
|
5480 #57 := [rewrite]: #56 |
|
5481 #54 := (iff #15 #53) |
|
5482 #51 := (iff #14 #43) |
|
5483 #46 := (or false #43) |
|
5484 #49 := (iff #46 #43) |
|
5485 #50 := [rewrite]: #49 |
|
5486 #47 := (iff #14 #46) |
|
5487 #44 := (iff #13 #43) |
|
5488 #41 := (= #12 #40) |
|
5489 #42 := [rewrite]: #41 |
|
5490 #38 := (= #8 #10) |
|
5491 #39 := [rewrite]: #38 |
|
5492 #45 := [monotonicity #39 #42]: #44 |
|
5493 #48 := [monotonicity #45]: #47 |
|
5494 #52 := [trans #48 #50]: #51 |
|
5495 #55 := [monotonicity #45 #52]: #54 |
|
5496 #59 := [trans #55 #57]: #58 |
|
5497 #62 := [monotonicity #59]: #61 |
|
5498 #73 := [trans #62 #71]: #72 |
|
5499 #37 := [asserted]: #16 |
|
5500 [mp #37 #73]: false |
|
5501 unsat |
5501 unsat |
5502 68356683e9cf34e34d65674fa3c8a62835e193a4 341 0 |
5502 68356683e9cf34e34d65674fa3c8a62835e193a4 341 0 |
5503 #2 := false |
5503 #2 := false |
5504 #24 := 0::Int |
5504 #24 := 0::Int |
5505 decl f3 :: Int |
5505 decl f3 :: Int |
10826 #525 := [trans #539 #534]: #23 |
10826 #525 := [trans #539 #534]: #23 |
10827 #69 := (not #23) |
10827 #69 := (not #23) |
10828 #71 := [not-or-elim #70]: #69 |
10828 #71 := [not-or-elim #70]: #69 |
10829 [unit-resolution #71 #525]: false |
10829 [unit-resolution #71 #525]: false |
10830 unsat |
10830 unsat |
|
10831 8fa5494ea43f950aa9add5e070d1d34c34426a1b 29 0 |
|
10832 #2 := false |
|
10833 #1 := true |
|
10834 decl f1 :: S1 |
|
10835 #3 := f1 |
|
10836 decl f3 :: (-> S1 S1) |
|
10837 decl f2 :: S1 |
|
10838 #4 := f2 |
|
10839 decl f4 :: (-> S2 S1) |
|
10840 #7 := (:var 0 S2) |
|
10841 #8 := (f4 #7) |
|
10842 #9 := (= #8 f1) |
|
10843 #10 := (forall (vars (?v0 S2)) #9) |
|
10844 #11 := (if #10 f1 f2) |
|
10845 #12 := (f3 #11) |
|
10846 #13 := (= #12 f1) |
|
10847 #14 := (implies #13 true) |
|
10848 #15 := (not #14) |
|
10849 #44 := (iff #15 false) |
|
10850 #39 := (not true) |
|
10851 #42 := (iff #39 false) |
|
10852 #43 := [rewrite]: #42 |
|
10853 #40 := (iff #15 #39) |
|
10854 #37 := (iff #14 true) |
|
10855 #38 := [rewrite]: #37 |
|
10856 #41 := [monotonicity #38]: #40 |
|
10857 #45 := [trans #41 #43]: #44 |
|
10858 #36 := [asserted]: #15 |
|
10859 [mp #36 #45]: false |
|
10860 unsat |
10831 2fd48adc6f5c51aec7f5f7945dc6937d8ac8fd61 424 0 |
10861 2fd48adc6f5c51aec7f5f7945dc6937d8ac8fd61 424 0 |
10832 #2 := false |
10862 #2 := false |
10833 decl f9 :: (-> S6 S7 S7) |
10863 decl f9 :: (-> S6 S7 S7) |
10834 decl f12 :: S7 |
10864 decl f12 :: S7 |
10835 #22 := f12 |
10865 #22 := f12 |
11275 #36 := [rewrite]: #35 |
11305 #36 := [rewrite]: #35 |
11276 #39 := [monotonicity #36]: #38 |
11306 #39 := [monotonicity #36]: #38 |
11277 #43 := [trans #39 #41]: #42 |
11307 #43 := [trans #39 #41]: #42 |
11278 #34 := [asserted]: #13 |
11308 #34 := [asserted]: #13 |
11279 [mp #34 #43]: false |
11309 [mp #34 #43]: false |
11280 unsat |
|
11281 8fa5494ea43f950aa9add5e070d1d34c34426a1b 29 0 |
|
11282 #2 := false |
|
11283 #1 := true |
|
11284 decl f1 :: S1 |
|
11285 #3 := f1 |
|
11286 decl f3 :: (-> S1 S1) |
|
11287 decl f2 :: S1 |
|
11288 #4 := f2 |
|
11289 decl f4 :: (-> S2 S1) |
|
11290 #7 := (:var 0 S2) |
|
11291 #8 := (f4 #7) |
|
11292 #9 := (= #8 f1) |
|
11293 #10 := (forall (vars (?v0 S2)) #9) |
|
11294 #11 := (if #10 f1 f2) |
|
11295 #12 := (f3 #11) |
|
11296 #13 := (= #12 f1) |
|
11297 #14 := (implies #13 true) |
|
11298 #15 := (not #14) |
|
11299 #44 := (iff #15 false) |
|
11300 #39 := (not true) |
|
11301 #42 := (iff #39 false) |
|
11302 #43 := [rewrite]: #42 |
|
11303 #40 := (iff #15 #39) |
|
11304 #37 := (iff #14 true) |
|
11305 #38 := [rewrite]: #37 |
|
11306 #41 := [monotonicity #38]: #40 |
|
11307 #45 := [trans #41 #43]: #44 |
|
11308 #36 := [asserted]: #15 |
|
11309 [mp #36 #45]: false |
|
11310 unsat |
11310 unsat |
11311 5e86b4c9726ef5b2868f22c9ea608e9e3558803e 344 0 |
11311 5e86b4c9726ef5b2868f22c9ea608e9e3558803e 344 0 |
11312 #2 := false |
11312 #2 := false |
11313 decl f7 :: (-> S5 Int S2) |
11313 decl f7 :: (-> S5 Int S2) |
11314 #28 := 6::Int |
11314 #28 := 6::Int |