The proofs generated by KoAT can be downloaded here.
| Example | Result | Runtime |
|---|---|---|
| prob_cfr/cfr01.koat | Maybe | 0.77 s |
| prob_cfr/cfr02.koat | Maybe | 1.06 s |
| prob_cfr/cfr03.koat | Maybe | 1.43 s |
| prob_cfr/cfr04.koat | Maybe | 1.83 s |
| prob_cfr/cfr05.koat | Maybe | 1.42 s |
| prob_cfr/cfr06.koat | Maybe | 1.84 s |
| prob_cfr/cfr07.koat | O(n²) | 0.69 s |
| prob_cfr/cfr08.koat | Maybe | 1.37 s |
| prob_cfr/cfr09.koat | Maybe | 1.06 s |
| prob_cfr/cfr10.koat | Maybe | 1.80 s |
| prob_cfr/cfr11.koat | Maybe | 1.04 s |
| prob_cfr/cfr12.koat | Maybe | 1.68 s |
| prob_cfr/cfr13.koat | O(n) | 0.78 s |
| prob_cfr/cfr14.koat | Maybe | 1.24 s |
| prob_cfr/cfr15.koat | Maybe | 0.77 s |
| Absynth-Suite/2drwalk.koat | O(n) | 35.34 s |
| Absynth-Suite/C4B_t09.koat | O(n) | 0.69 s |
| Absynth-Suite/C4B_t13.koat | O(n) | 0.78 s |
| Absynth-Suite/C4B_t15.koat | O(n) | 0.67 s |
| Absynth-Suite/C4B_t19.koat | O(n) | 0.82 s |
| Absynth-Suite/C4B_t30.koat | O(n) | 0.78 s |
| Absynth-Suite/C4B_t61.koat | O(n) | 0.59 s |
| Absynth-Suite/bayesian.koat | O(n) | 4.47 s |
| Absynth-Suite/ber.koat | O(n) | 0.57 s |
| Absynth-Suite/bin.koat | O(n) | 0.68 s |
| Absynth-Suite/complex.koat | O(n²) | 2.03 s |
| Absynth-Suite/condand.koat | O(n) | 0.47 s |
| Absynth-Suite/cooling.koat | O(n) | 0.91 s |
| Absynth-Suite/coupon.koat | O(1) | 1.33 s |
| Absynth-Suite/cowboy_duel.koat | O(1) | 0.66 s |
| Absynth-Suite/cowboy_duel_3way.koat | O(1) | 2.26 s |
| Absynth-Suite/fcall.koat | Maybe | 1.19 s |
| Absynth-Suite/filling.koat | O(n) | 2.45 s |
| Absynth-Suite/geo.koat | O(1) | 0.59 s |
| Absynth-Suite/hyper.koat | O(n) | 0.62 s |
| Absynth-Suite/linear01.koat | O(n) | 0.44 s |
| Absynth-Suite/miner.koat | O(n) | 1.97 s |
| Absynth-Suite/multirace.koat | Maybe | 1.52 s |
| Absynth-Suite/no_loop.koat | O(1) | 0.34 s |
| Absynth-Suite/pol04.koat | Maybe | 1.59 s |
| Absynth-Suite/pol05.koat | Maybe | 1.34 s |
| Absynth-Suite/pol06.koat | O(1) | 2.45 s |
| Absynth-Suite/pol07.koat | O(n²) | 0.93 s |
| Absynth-Suite/prdwalk.koat | O(n) | 0.71 s |
| Absynth-Suite/prnes.koat | O(n) | 1.62 s |
| Absynth-Suite/prseq.koat | O(n) | 0.88 s |
| Absynth-Suite/prseq_bin.koat | O(n) | 0.93 s |
| Absynth-Suite/prspeed.koat | Maybe | 1.83 s |
| Absynth-Suite/race.koat | O(n) | 0.84 s |
| Absynth-Suite/rdbub.koat | O(n²) | 1.17 s |
| Absynth-Suite/rdseql.koat | O(n) | 0.72 s |
| Absynth-Suite/rdspeed.koat | O(n) | 1.10 s |
| Absynth-Suite/rdwalk.koat | O(n) | 0.76 s |
| Absynth-Suite/rfind_lv.koat | O(1) | 0.58 s |
| Absynth-Suite/rfind_mc.koat | O(n) | 0.57 s |
| Absynth-Suite/robot.koat | O(n) | 3.52 s |
| Absynth-Suite/roulette.koat | O(n) | 3.00 s |
| Absynth-Suite/sampling.koat | O(n) | 2.11 s |
| Absynth-Suite/simple_recursive.koat | O(n) | 0.67 s |
| Absynth-Suite/sprdwalk.koat | O(n) | 0.60 s |
| Absynth-Suite/trader.koat | Maybe | 3.43 s |
| KoAT-Suite/C4B_t132.koat | O(n) | 0.71 s |
| KoAT-Suite/alain.c.koat | O(n³) | 6.44 s |
| KoAT-Suite/complex2.koat | O(n²) | 1.85 s |
| KoAT-Suite/cousot9.koat | O(n²) | 2.06 s |
| KoAT-Suite/ex_paper1.c.koat | O(n²) | 10.82 s |
| KoAT-Suite/fib_exp_size.koat | EXP | 1.02 s |
| KoAT-Suite/fig5.koat | O(n) | 0.52 s |
| KoAT-Suite/fig6.koat | O(1) | 0.76 s |
| KoAT-Suite/fig7.koat | O(1) | 0.38 s |
| KoAT-Suite/geo_race.koat | O(n) | 0.52 s |
| KoAT-Suite/knuth_morris_pratt.c.koat | O(n) | 19.46 s |
| KoAT-Suite/leading.1.koat | O(n²) | 0.90 s |
| KoAT-Suite/leading.koat | O(n²) | 0.93 s |
| KoAT-Suite/multirace2.koat | O(n²) | 1.09 s |
| KoAT-Suite/neg_init_upd.koat | O(n) | 0.79 s |
| KoAT-Suite/nested_break.koat | Maybe | 1.04 s |
| KoAT-Suite/nested_rdwalk.koat | O(n) | 0.75 s |
| KoAT-Suite/nested_size.koat | O(n⁵) | 1.59 s |
| KoAT-Suite/nondet_countdown.koat | Maybe | 0.99 s |
| KoAT-Suite/prob_loop.koat | O(n) | 0.94 s |
| KoAT-Suite/prseq2.koat | O(n) | 0.84 s |
| KoAT-Suite/rank3.c.koat | O(n²) | 17.97 s |
| KoAT-Suite/rdseql2.koat | O(n) | 0.49 s |
| KoAT-Suite/realheapsort.koat | O(n²) | 5.54 s |
| KoAT-Suite/selectsort.koat | O(n²) | 3.42 s |
| KoAT-Suite/simple_nested.koat | O(n²) | 0.85 s |
| KoAT-Suite/spctrm.koat | O(n²) | 9.42 s |
| KoAT-Suite/trunc_selectsort.koat | O(n²) | 3.14 s |
| KoAT-Suite/two_arrays2.koat | O(n) | 9.65 s |