| benchmark | AProVE | polytool |
|---|---|---|
| tpdb-8.0/LP/LP/BCGGV05/ackerman.pl | YES 1871 | YES 5025 |
| tpdb-8.0/LP/LP/BCGGV05/delete-fbf.pl | YES 2661 | YES 3602 |
| tpdb-8.0/LP/LP/BCGGV05/delete-ffb.pl | YES 2497 | YES 3610 |
| tpdb-8.0/LP/LP/BCGGV05/der-bf.pl | YES 3251 | YES 9873 |
| tpdb-8.0/LP/LP/BCGGV05/der-fb.pl | MAYBE 31209 | MAYBE 59991 |
| tpdb-8.0/LP/LP/BCGGV05/flat-bf.pl | YES 2079 | YES 1434 |
| tpdb-8.0/LP/LP/BCGGV05/flatlength-ffb.pl | MAYBE 3878 | MAYBE 1485 |
| tpdb-8.0/LP/LP/BCGGV05/g.pl | MAYBE 5043 | MAYBE 841 |
| tpdb-8.0/LP/LP/BCGGV05/inorder-bf.pl | YES 1935 | YES 2646 |
| tpdb-8.0/LP/LP/BCGGV05/insert-bff.pl | MAYBE 56050 | MAYBE 2381 |
| tpdb-8.0/LP/LP/BCGGV05/length.pl | YES 1742 | YES 634 |
| tpdb-8.0/LP/LP/BCGGV05/less-fb.pl | YES 1736 | YES 630 |
| tpdb-8.0/LP/LP/BCGGV05/list.pl | YES 1738 | YES 624 |
| tpdb-8.0/LP/LP/BCGGV05/maximum-bff.pl | YES 1863 | YES 1195 |
| tpdb-8.0/LP/LP/BCGGV05/member-fb.pl | YES 1750 | YES 629 |
| tpdb-8.0/LP/LP/BCGGV05/mult.pl | YES 1864 | YES 1305 |
| tpdb-8.0/LP/LP/BCGGV05/numeral.pl | YES 1741 | YES 623 |
| tpdb-8.0/LP/LP/BCGGV05/palindrome.pl | YES 1799 | YES 705 |
| tpdb-8.0/LP/LP/BCGGV05/slowsort-bb.pl | YES 2448 | YES 4142 |
| tpdb-8.0/LP/LP/BCGGV05/slowsort-fb.pl | MAYBE 4549 | MAYBE 4313 |
| tpdb-8.0/LP/LP/BCGGV05/sublist-fb.pl | YES 1819 | YES 713 |
| tpdb-8.0/LP/LP/BCGGV05/t.pl | YES 2204 | YES 3090 |
| tpdb-8.0/LP/LP/BCGGV05/transpose-bb.pl | YES 1919 | YES 4776 |
| tpdb-8.0/LP/LP/BCGGV05/tree_member-fb.pl | YES 1846 | YES 687 |
| tpdb-8.0/LP/LP/BCGGV05/tree.pl | YES 1838 | YES 792 |
| tpdb-8.0/LP/LP/lpexamples/ackermann-ioi.pl | MAYBE 37385 | MAYBE 2560 |
| tpdb-8.0/LP/LP/lpexamples/ackermann.pl | YES 1859 | YES 5120 |
| tpdb-8.0/LP/LP/lpexamples/average-ioi.pl | YES 1800 | YES 1499 |
| tpdb-8.0/LP/LP/lpexamples/average.pl | YES 2096 | YES 1587 |
| tpdb-8.0/LP/LP/lpexamples/log2a-oi.pl | MAYBE 7610 | MAYBE 822 |
| tpdb-8.0/LP/LP/lpexamples/log2b-oi.pl | TIMEOUT 60931 | MAYBE 1182 |
| tpdb-8.0/LP/LP/lpexamples/log2b.pl | YES 2145 | YES 1657 |
| tpdb-8.0/LP/LP/lpexamples/mapcolor.pl | TIMEOUT 60685 | MAYBE 1678 |
| tpdb-8.0/LP/LP/lpexamples/mergesort.pl | YES 3543 | YES 15896 |
| tpdb-8.0/LP/LP/lpexamples/shapes.pl | YES 4641 | TIMEOUT 60154 |
| tpdb-8.0/LP/LP/SGST06/at.pl | YES 1755 | YES 103 |
| tpdb-8.0/LP/LP/SGST06/avg-bfb.pl | YES 1829 | YES 1497 |
| tpdb-8.0/LP/LP/SGST06/blist.pl | YES 1856 | YES 1305 |
| tpdb-8.0/LP/LP/SGST06/btappend.pl | YES 2008 | YES 1451 |
| tpdb-8.0/LP/LP/SGST06/cconfdel.pl | YES 2195 | YES 2652 |
| tpdb-8.0/LP/LP/SGST06/cnfequiv.pl | YES 6913 | MAYBE 4030 |
| tpdb-8.0/LP/LP/SGST06/confdel.pl | YES 2183 | YES 2525 |
| tpdb-8.0/LP/LP/SGST06/gopher.pl | YES 2050 | YES 848 |
| tpdb-8.0/LP/LP/SGST06/hbal_tree.pl | YES 2411 | MAYBE 2534 |
| tpdb-8.0/LP/LP/SGST06/incomplete_variant.pl | YES 1683 | YES 93 |
| tpdb-8.0/LP/LP/SGST06/perm.pl | YES 1966 | YES 2054 |
| tpdb-8.0/LP/LP/SGST06/p.pl | YES 3159 | YES 4723 |
| tpdb-8.0/LP/LP/SGST06/pplus2.pl | YES 2043 | YES 2311 |
| tpdb-8.0/LP/LP/SGST06/preorder.pl | YES 1915 | YES 1977 |
| tpdb-8.0/LP/LP/SGST06/rev.pl | YES 3378 | YES 3791 |
| tpdb-8.0/LP/LP/SGST06/shuffle.pl | YES 2177 | YES 2511 |
| tpdb-8.0/LP/LP/SGST06/toyama.pl | YES 1637 | YES 89 |
| tpdb-8.0/LP/LP/SGST06/transpose2.pl | MAYBE 3925 | MAYBE 8071 |
| tpdb-8.0/LP/LP/talp_apt/member.pl | YES 1742 | YES 620 |
| tpdb-8.0/LP/LP/talp_apt/naive_rev-oi.pl | MAYBE 5413 | MAYBE 659 |
| tpdb-8.0/LP/LP/talp_apt/ordered.pl | YES 2189 | YES 1550 |
| tpdb-8.0/LP/LP/talp_apt/overlap.pl | YES 1891 | YES 1338 |
| tpdb-8.0/LP/LP/talp_apt/permutation.pl | YES 2137 | YES 2651 |
| tpdb-8.0/LP/LP/talp_apt/quicksort.pl | YES 3165 | YES 8343 |
| tpdb-8.0/LP/LP/talp_apt/select1.pl | YES 1746 | YES 634 |
| tpdb-8.0/LP/LP/talp_apt/select.pl | YES 1748 | YES 683 |
| tpdb-8.0/LP/LP/talp_apt/subset1.pl | MAYBE 10532 | MAYBE 1478 |
| tpdb-8.0/LP/LP/talp_apt/sum.pl | YES 1757 | YES 631 |
| tpdb-8.0/LP/LP/talp_dds/append.pl | YES 1752 | YES 691 |
| tpdb-8.0/LP/LP/talp_dds/dis_con-bis.pl | YES 1866 | YES 945 |
| tpdb-8.0/LP/LP/talp_dds/dis_con.pl | YES 1900 | YES 945 |
| tpdb-8.0/LP/LP/talp_dds/duplicate.pl | YES 1822 | YES 696 |
| tpdb-8.0/LP/LP/talp_dds/merge.pl | YES 2521 | YES 4197 |
| tpdb-8.0/LP/LP/talp_dds/permute.pl | YES 2018 | YES 1536 |
| tpdb-8.0/LP/LP/talp_dds/reverse-iio.pl | YES 1815 | YES 690 |
| tpdb-8.0/LP/LP/talp_dds/reverse.pl | YES 1762 | YES 688 |
| tpdb-8.0/LP/LP/talp_dds/sum-ioi.pl | YES 1914 | YES 1537 |
| tpdb-8.0/LP/LP/talp_dds/sum.pl | YES 1876 | YES 1619 |
| tpdb-8.0/LP/LP/talp_mixed/ack.pl | YES 1812 | YES 5103 |
| tpdb-8.0/LP/LP/talp_mixed/hanoiapp.suc.pl | YES 2806 | YES 4309 |
| tpdb-8.0/LP/LP/talp_mixed/mergesort.pl | YES 5077 | TIMEOUT 60198 |
| tpdb-8.0/LP/LP/talp_mixed/p.pl | YES 2045 | YES 1349 |
| tpdb-8.0/LP/LP/talp_mixed/queens.pl | YES 3024 | YES 6053 |
| tpdb-8.0/LP/LP/talp_mixed/rotate.pl | YES 1855 | YES 1277 |
| tpdb-8.0/LP/LP/talp_mixed/sameleaves.pl | YES 2287 | YES 1769 |
| tpdb-8.0/LP/LP/talp_mixed/sicstus1.pl | YES 1789 | YES 715 |
| tpdb-8.0/LP/LP/talp_mixed/sublist.pl | YES 1808 | YES 1352 |
| tpdb-8.0/LP/LP/talp_mixed/zebra.pl | YES 2627 | YES 2036 |
| tpdb-8.0/LP/LP/talp_plumer/pl1.1.pl | MAYBE 2996 | MAYBE 651 |
| tpdb-8.0/LP/LP/talp_plumer/pl3.1.1.pl | MAYBE 4318 | MAYBE 662 |
| tpdb-8.0/LP/LP/talp_plumer/pl4.0.1-oooi.pl | MAYBE 3136 | MAYBE 643 |
| tpdb-8.0/LP/LP/talp_plumer/pl4.0.1.pl | YES 1825 | YES 700 |
| tpdb-8.0/LP/LP/talp_plumer/pl4.4.3.pl | YES 2558 | YES 3372 |
| tpdb-8.0/LP/LP/talp_plumer/pl4.5.3a.pl | MAYBE 2937 | MAYBE 631 |
| tpdb-8.0/LP/LP/talp_plumer/pl4.5.3b.pl | MAYBE 3569 | MAYBE 624 |
| tpdb-8.0/LP/LP/talp_plumer/pl7.6.2a.pl | MAYBE 18287 | MAYBE 2439 |
| tpdb-8.0/LP/LP/talp_plumer/pl7.6.2b.pl | MAYBE 52430 | MAYBE 6114 |
| tpdb-8.0/LP/LP/talp_plumer/pl8.2.1.pl | YES 4475 | TIMEOUT 60199 |
| tpdb-8.0/LP/LP/talp_talp/binary3.pl | YES 3360 | YES 6588 |
| tpdb-8.0/LP/LP/talp_talp/example4.pl | YES 1737 | YES 624 |
| tpdb-8.0/LP/LP/talp_talp/gcd.pl | YES 3296 | YES 5220 |
| tpdb-8.0/LP/LP/talp_talp/nat.pl | YES 1956 | YES 2306 |
| tpdb-8.0/LP/LP/talp_talp/normal.pl | YES 2134 | YES 1686 |
| tpdb-8.0/LP/LP/talp_talp/palindrome.pl | YES 1801 | YES 702 |
| tpdb-8.0/LP/LP/talp_talp/reminder.pl | YES 2375 | YES 2277 |
| tpdb-8.0/LP/LP/talp_talp/slowsort-oi.pl | MAYBE 3789 | MAYBE 3009 |
| tpdb-8.0/LP/LP/talp_talp/slowsort.pl | YES 2400 | YES 2961 |
| tpdb-8.0/LP/LP/talp_talp/vangelder.pl | YES 5619 | YES 9831 |
| tpdb-8.0/LP/LP/terminweb_new/append-ooi.pl | YES 1702 | YES 691 |
| tpdb-8.0/LP/LP/terminweb_new/backwards_append.pl | YES 1768 | YES 693 |
| tpdb-8.0/LP/LP/terminweb_new/basic_append.pl | YES 1690 | YES 692 |
| tpdb-8.0/LP/LP/terminweb_new/NJ1.pl | YES 1813 | YES 698 |
| tpdb-8.0/LP/LP/terminweb_new/NJ2.pl | YES 1813 | YES 722 |
| tpdb-8.0/LP/LP/terminweb_new/NJ3.pl | YES 1857 | YES 5141 |
| tpdb-8.0/LP/LP/terminweb_new/NJ6.pl | YES 1857 | YES 1317 |
| tpdb-8.0/LP/LP/terminweb_new/preorder_dl.pl | YES 1905 | YES 2007 |
| tpdb-8.0/LP/LP/terminweb_new/transpose.pl | YES 1958 | YES 3426 |
| tpdb-8.0/LP/LP/terminweb_new/ways.pl | YES 6034 | YES 9338 |
| tpdb-8.0/LP/LP/terminweb_old/append3.pl | YES 1809 | YES 706 |
| tpdb-8.0/LP/LP/terminweb_old/balance_tree2.pl | MAYBE 29899 | TIMEOUT 60147 |
| tpdb-8.0/LP/LP/terminweb_old/inorder.pl | YES 1936 | YES 2308 |
| tpdb-8.0/LP/LP/terminweb_old/interleave.pl | YES 1757 | YES 682 |
| tpdb-8.0/LP/LP/terminweb_old/permutation2.pl | YES 1964 | YES 1542 |
| tpdb-8.0/LP/LP/terminweb_old/rotate.pl | YES 1866 | YES 1308 |
| tpdb-8.0/LP/LP/terminweb_old/sublist_bad.pl | MAYBE 3014 | MAYBE 1258 |
| tpdb-8.0/LP/LP/terminweb_old/sublist.pl | YES 1838 | YES 693 |
| tpdb-8.0/LP/LP/terminweb_old/subset-no.pl | MAYBE 10354 | MAYBE 1470 |
| tpdb-8.0/LP/LP/terminweb_old/untupled_bal_tree.pl | YES 2384 | MAYBE 28423 | 100 | 94 |