| Example | MCNP | AProVE fixed abstraction | AProVE |
|---|
| Aprove_09/AProVEMath.mc (intermediate clpq, original jar) | MAYBE | 2.439 | YES | 16.830 | YES | 19.251 |
| Aprove_09/Collatz.mc (intermediate clpq, original jar) | MAYBE | 0.401 | MAYBE | 13.557 | TIMEOUT | 60 |
| Aprove_09/Convert.mc (intermediate clpq, original jar) | MAYBE | 1.613 | MAYBE | 18.024 | YES | 10.449 |
| Aprove_09/Count.mc (intermediate clpq, original jar) | MAYBE | 23.127 | MAYBE | 21.281 | YES | 34.129 |
| Aprove_09/CountMetaList.mc (intermediate clpq, original jar) | MAYBE | 2.650 | MAYBE | 17.258 | YES | 19.591 |
| Aprove_09/CountUpRound.mc (intermediate clpq, original jar) | YES | 0.105 | YES | 2.651 | YES | 2.630 |
| Aprove_09/DivMinus.mc (intermediate clpq, original jar) | YES | 0.036 | YES | 2.187 | YES | 2.633 |
| Aprove_09/DivMinus2.mc (intermediate clpq, original jar) | YES | 0.220 | YES | 2.820 | YES | 5.468 |
| Aprove_09/DivWithoutMinus.mc (intermediate clpq, original jar) | YES | 0.227 | YES | 3.113 | YES | 5.842 |
| Aprove_09/Duplicate.mc (intermediate clpq, original jar) | MAYBE | 0.212 | YES | 2.918 | YES | 3.086 |
| Aprove_09/DuplicateNodes.mc (intermediate clpq, original jar) | MAYBE | 13.360 | YES | 18.078 | YES | 11.749 |
| Aprove_09/Flatten.mc (intermediate clpq, original jar) | MAYBE | 3.328 | MAYBE | 27.951 | YES | 12.758 |
| Aprove_09/FlattenTree.mc (intermediate clpq, original jar) | MAYBE | 12.864 | MAYBE | 18.259 | YES | 7.668 |
| Aprove_09/GCD.mc (intermediate clpq, original jar) | YES | 8.166 | MAYBE | 19.927 | TIMEOUT | 60 |
| Aprove_09/GCD2.mc (intermediate clpq, original jar) | YES | 1.746 | YES | 18.285 | YES | 11.570 |
| Aprove_09/GCD3.mc (intermediate clpq, original jar) | YES | 0.258 | YES | 6.780 | YES | 5.928 |
| Aprove_09/GCD4.mc (intermediate clpq, original jar) | YES | 0.257 | YES | 3.651 | YES | 4.340 |
| Aprove_09/GCD5.mc (intermediate clpq, original jar) | MAYBE | 0.173 | MAYBE | 12.651 | YES | 13.428 |
| Aprove_09/LessLeaves.mc (intermediate clpq, original jar) | TIMEOUT | 60 | MAYBE | 21.573 | YES | 20.635 |
| Aprove_09/ListContent.mc (intermediate clpq, original jar) | MAYBE | 0.515 | MAYBE | 15.279 | YES | 4.519 |
| Aprove_09/ListContentArbitrary.mc (intermediate clpq, original jar) | MAYBE | 1.412 | YES | 7.526 | YES | 6.990 |
| Aprove_09/ListContentTail.mc (intermediate clpq, original jar) | MAYBE | 47.281 | YES | 17.347 | YES | 10.215 |
| Aprove_09/ListDuplicate.mc (intermediate clpq, original jar) | MAYBE | 0.338 | MAYBE | 14.695 | YES | 15.175 |
| Aprove_09/Log.mc (intermediate clpq, original jar) | MAYBE | 3.615 | YES | 17.063 | YES | 31.719 |
| Aprove_09/LogAG.mc (intermediate clpq, original jar) | MAYBE | 2.362 | YES | 24.082 | YES | 32.217 |
| Aprove_09/LogBuiltIn.mc (intermediate clpq, original jar) | MAYBE | 0.277 | YES | 2.834 | YES | 2.767 |
| Aprove_09/LogIterative.mc (intermediate clpq, original jar) | MAYBE | 0.304 | YES | 5.408 | YES | 5.219 |
| Aprove_09/LogMult.mc (intermediate clpq, original jar) | MAYBE | 0.272 | MAYBE | 12.816 | TIMEOUT | 60 |
| Aprove_09/McCarthyIterative.mc (intermediate clpq, original jar) | MAYBE | 0.514 | MAYBE | 19.305 | TIMEOUT | 60 |
| Aprove_09/MinusBuiltIn.mc (intermediate clpq, original jar) | YES | 0.017 | YES | 2.374 | YES | 2.209 |
| Aprove_09/MinusUserDefined.mc (intermediate clpq, original jar) | MAYBE | 1.966 | MAYBE | 19.757 | TIMEOUT | 60 |
| Aprove_09/MirrorTree.mc (intermediate clpq, original jar) | MAYBE | 12.655 | MAYBE | 25.705 | YES | 11.313 |
| Aprove_09/Mod.mc (intermediate clpq, original jar) | YES | 0.178 | YES | 5.264 | YES | 4.610 |
| Aprove_09/Overflow.mc (intermediate clpq, original jar) | YES | 0.011 | YES | 2.099 | YES | 2.200 |
| Aprove_09/PastaA1.mc (intermediate clpq, original jar) | YES | 0.096 | YES | 3.179 | YES | 2.858 |
| Aprove_09/PastaA10.mc (intermediate clpq, original jar) | YES | 0.110 | MAYBE | 15.254 | YES | 23.569 |
| Aprove_09/PastaA4.mc (intermediate clpq, original jar) | YES | 0.013 | YES | 2.383 | YES | 2.071 |
| Aprove_09/PastaA5.mc (intermediate clpq, original jar) | YES | 0.015 | YES | 2.269 | YES | 2.169 |
| Aprove_09/PastaA6.mc (intermediate clpq, original jar) | MAYBE | 0.202 | YES | 2.407 | YES | 2.386 |
| Aprove_09/PastaA7.mc (intermediate clpq, original jar) | YES | 0.019 | YES | 2.414 | YES | 2.355 |
| Aprove_09/PastaA8.mc (intermediate clpq, original jar) | MAYBE | 0.217 | YES | 2.182 | YES | 2.121 |
| Aprove_09/PastaA9.mc (intermediate clpq, original jar) | YES | 0.019 | YES | 2.308 | YES | 2.874 |
| Aprove_09/PastaB1.mc (intermediate clpq, original jar) | YES | 0.028 | YES | 2.124 | YES | 2.257 |
| Aprove_09/PastaB10.mc (intermediate clpq, original jar) | YES | 0.140 | YES | 2.914 | YES | 3.193 |
| Aprove_09/PastaB11.mc (intermediate clpq, original jar) | YES | 0.524 | YES | 3.433 | YES | 2.990 |
| Aprove_09/PastaB12.mc (intermediate clpq, original jar) | YES | 0.144 | YES | 2.502 | YES | 2.433 |
| Aprove_09/PastaB13.mc (intermediate clpq, original jar) | YES | 1.014 | TIMEOUT | 60 | YES | 27.637 |
| Aprove_09/PastaB14.mc (intermediate clpq, original jar) | YES | 0.065 | YES | 2.564 | YES | 3.375 |
| Aprove_09/PastaB15.mc (intermediate clpq, original jar) | YES | 0.103 | YES | 3.453 | YES | 4.600 |
| Aprove_09/PastaB16.mc (intermediate clpq, original jar) | YES | 0.127 | YES | 3.089 | YES | 2.951 |
| Aprove_09/PastaB17.mc (intermediate clpq, original jar) | YES | 0.762 | YES | 4.597 | YES | 3.306 |
| Aprove_09/PastaB18.mc (intermediate clpq, original jar) | YES | 0.185 | YES | 3.837 | YES | 8.926 |
| Aprove_09/PastaB2.mc (intermediate clpq, original jar) | YES | 0.019 | YES | 2.202 | YES | 2.199 |
| Aprove_09/PastaB3.mc (intermediate clpq, original jar) | YES | 0.021 | YES | 2.241 | YES | 2.911 |
| Aprove_09/PastaB4.mc (intermediate clpq, original jar) | YES | 0.021 | YES | 2.510 | YES | 2.425 |
| Aprove_09/PastaB5.mc (intermediate clpq, original jar) | YES | 0.022 | YES | 2.294 | YES | 3.114 |
| Aprove_09/PastaB6.mc (intermediate clpq, original jar) | YES | 0.027 | YES | 2.218 | YES | 2.254 |
| Aprove_09/PastaB7.mc (intermediate clpq, original jar) | YES | 0.039 | YES | 2.310 | YES | 2.308 |
| Aprove_09/PastaB8.mc (intermediate clpq, original jar) | MAYBE | 0.378 | YES | 4.306 | YES | 4.398 |
| Aprove_09/PastaC1.mc (intermediate clpq, original jar) | YES | 0.154 | YES | 5.305 | YES | 5.106 |
| Aprove_09/PastaC10.mc (intermediate clpq, original jar) | MAYBE | 0.580 | MAYBE | 24.189 | YES | 4.736 |
| Aprove_09/PastaC11.mc (intermediate clpq, original jar) | YES | 0.347 | YES | 4.531 | YES | 27.500 |
| Aprove_09/PastaC2.mc (intermediate clpq, original jar) | YES | 0.107 | YES | 3.056 | YES | 3.042 |
| Aprove_09/PastaC3.mc (intermediate clpq, original jar) | YES | 0.162 | YES | 3.442 | YES | 2.950 |
| Aprove_09/PastaC5.mc (intermediate clpq, original jar) | MAYBE | 0.356 | MAYBE | 17.561 | MAYBE | 45.522 |
| Aprove_09/PastaC7.mc (intermediate clpq, original jar) | YES | 0.018 | YES | 2.343 | YES | 2.290 |
| Aprove_09/PastaC9.mc (intermediate clpq, original jar) | YES | 0.321 | YES | 6.643 | YES | 4.637 |
| Aprove_09/PlusSwap.mc (intermediate clpq, original jar) | YES | 0.034 | YES | 3.821 | YES | 3.865 |
| Aprove_09/Round3.mc (intermediate clpq, original jar) | MAYBE | 0.162 | MAYBE | 12.375 | YES | 13.238 |
| Aprove_09/RunningPointers.mc (intermediate clpq, original jar) | MAYBE | 0.496 | MAYBE | 15.149 | YES | 4.074 |
| Aprove_09/Samefringe.mc (intermediate clpq, original jar) | TIMEOUT | 60 | MAYBE | 24.198 | YES | 24.193 |
| Aprove_09/Shuffle.mc (intermediate clpq, original jar) | MAYBE | 0.992 | MAYBE | 15.186 | YES | 5.244 |
| Aprove_09/SortCount.mc (intermediate clpq, original jar) | TIMEOUT | 60 | TIMEOUT | 60 | TIMEOUT | 60 |
| Aprove_09/StupidArray.mc (intermediate clpq, original jar) | YES | 0.000 | YES | 2.227 | YES | 2.072 |
| Aprove_09/Take.mc (intermediate clpq, original jar) | YES | 0.021 | YES | 2.512 | YES | 2.440 |
| AProVE_10/AG313.mc (intermediate clpq, original jar) | YES | 0.040 | YES | 2.468 | YES | 2.739 |
| AProVE_10/ArrayClasses.mc (intermediate clpq, original jar) | YES | 0.000 | YES | 1.537 | YES | 1.586 |
| AProVE_10/CyclicList.mc (intermediate clpq, original jar) | YES | 0.000 | YES | 6.565 | YES | 5.651 |
| AProVE_10/CyclicPair.mc (intermediate clpq, original jar) | YES | 0.000 | YES | 1.575 | YES | 1.582 |
| AProVE_10/CyclicPair2.mc (intermediate clpq, original jar) | MAYBE | 0.099 | MAYBE | 11.923 | YES | 1.726 |
| AProVE_10/DuplicateTreePath.mc (intermediate clpq, original jar) | MAYBE | 13.903 | YES | 16.695 | YES | 10.182 |
| AProVE_10/FlattenRTA.mc (intermediate clpq, original jar) | MAYBE | 19.653 | MAYBE | 57.229 | YES | 20.446 |
| AProVE_10/IntPath.mc (intermediate clpq, original jar) | YES | 0.000 | YES | 1.625 | YES | 1.586 |
| AProVE_10/IntPath2.mc (intermediate clpq, original jar) | YES | 0.000 | YES | 1.512 | YES | 1.688 |
| AProVE_10/IntRTA.mc (intermediate clpq, original jar) | YES | 0.017 | YES | 2.255 | YES | 2.168 |
| AProVE_10/NestedLoop.mc (intermediate clpq, original jar) | YES | 2.593 | TIMEOUT | 60 | TIMEOUT | 60 |
| AProVE_10/NullPair.mc (intermediate clpq, original jar) | YES | 0.000 | YES | 1.590 | YES | 1.526 |
| AProVE_10/SharingPair.mc (intermediate clpq, original jar) | MAYBE | 3.946 | MAYBE | 13.883 | YES | 19.884 |
| AProVE_10/TypeSwitch.mc (intermediate clpq, original jar) | YES | 0.000 | YES | 1.630 | YES | 1.690 |
| Costa_Julia_09/Break.mc (intermediate clpq, original jar) | YES | 0.011 | YES | 2.087 | YES | 2.260 |
| Costa_Julia_09/Continue.mc (intermediate clpq, original jar) | MAYBE | 0.095 | MAYBE | 11.686 | MAYBE | 14.821 |
| Costa_Julia_09/Continue1.mc (intermediate clpq, original jar) | YES | 0.069 | YES | 2.546 | YES | 2.351 |
| Costa_Julia_09/costa09-example_1.mc (intermediate clpq, original jar) | YES | 0.048 | YES | 6.622 | YES | 6.629 |
| Costa_Julia_09/costa09-example_2.mc (intermediate clpq, original jar) | MAYBE | 0.151 | YES | 2.756 | YES | 2.642 |
| Costa_Julia_09/costa09-example_3.mc (intermediate clpq, original jar) | YES | 0.012 | YES | 2.138 | YES | 2.234 |
| Costa_Julia_09/costa09-example_4.mc (intermediate clpq, original jar) | YES | 0.028 | YES | 2.355 | YES | 2.494 |
| Costa_Julia_09/costa09-example_5.mc (intermediate clpq, original jar) | MAYBE | 0.095 | MAYBE | 11.803 | MAYBE | 14.855 |
| Costa_Julia_09/CyclicalListDuplicate.mc (intermediate clpq, original jar) | MAYBE | 0.348 | MAYBE | 15.322 | MAYBE | 39.907 |
| Costa_Julia_09/Exc.mc (intermediate clpq, original jar) | YES | 0.100 | YES | 2.698 | YES | 2.321 |
| Costa_Julia_09/Exc1.mc (intermediate clpq, original jar) | MAYBE | 0.712 | MAYBE | 14.470 | MAYBE | 30.001 |
| Costa_Julia_09/Exc2.mc (intermediate clpq, original jar) | MAYBE | 0.775 | MAYBE | 14.504 | MAYBE | 32.513 |
| Costa_Julia_09/Exc3.mc (intermediate clpq, original jar) | MAYBE | 0.360 | MAYBE | 13.978 | MAYBE | 13.992 |
| Costa_Julia_09/Exc4.mc (intermediate clpq, original jar) | MAYBE | 0.890 | MAYBE | 14.622 | MAYBE | 52.779 |
| Costa_Julia_09/Exc5.mc (intermediate clpq, original jar) | MAYBE | 0.792 | MAYBE | 14.458 | MAYBE | 15.986 |
| Costa_Julia_09/Init.mc (intermediate clpq, original jar) | MAYBE | 0.094 | MAYBE | 11.750 | MAYBE | 15.099 |
| Costa_Julia_09/KnapsackDP.mc (intermediate clpq, original jar) | YES | 3.464 | TIMEOUT | 60 | TIMEOUT | 60 |
| Costa_Julia_09/Loop1.mc (intermediate clpq, original jar) | MAYBE | 0.203 | MAYBE | 13.036 | YES | 2.496 |
| Costa_Julia_09/Nested.mc (intermediate clpq, original jar) | YES | 0.061 | YES | 3.537 | YES | 3.072 |
| Costa_Julia_09/Sequence.mc (intermediate clpq, original jar) | YES | 0.021 | YES | 4.265 | YES | 4.333 |
| Costa_Julia_09/Sharing.mc (intermediate clpq, original jar) | MAYBE | 0.110 | MAYBE | 12.012 | YES | 1.813 |
| Costa_Julia_09/TestJulia1.mc (intermediate clpq, original jar) | MAYBE | 0.091 | MAYBE | 12.233 | MAYBE | 14.900 |
| Costa_Julia_09/TestJulia2.mc (intermediate clpq, original jar) | MAYBE | 0.093 | MAYBE | 11.984 | MAYBE | 15.366 |
| Costa_Julia_09/TestJulia3.mc (intermediate clpq, original jar) | MAYBE | 0.348 | MAYBE | 14.634 | TIMEOUT | 60 |
| Costa_Julia_09/TestJulia4.mc (intermediate clpq, original jar) | MAYBE | 0.201 | MAYBE | 13.821 | TIMEOUT | 60 |
| Julia_10_Iterative/Carre.mc (intermediate clpq, original jar) | MAYBE | 0.711 | MAYBE | 48.063 | YES | 9.968 |
| Julia_10_Iterative/Infix2Postfix.mc (intermediate clpq, original jar) | TIMEOUT | 60 | MAYBE | 47.455 | TIMEOUT | 60 |
| Julia_10_Iterative/Iterations.mc (intermediate clpq, original jar) | MAYBE | 14.353 | TIMEOUT | 60 | TIMEOUT | 60 |
| Julia_10_Iterative/NonPeriodic.mc (intermediate clpq, original jar) | YES | 0.000 | YES | 1.572 | YES | 1.573 |
| Julia_10_Iterative/RSA.mc (intermediate clpq, original jar) | TIMEOUT | 60 | TIMEOUT | 60 | TIMEOUT | 60 |
| Julia_10_Iterative/Test11.mc (intermediate clpq, original jar) | MAYBE | 12.233 | TIMEOUT | 60 | TIMEOUT | 60 |
| Julia_10_Iterative/Test13Loops.mc (intermediate clpq, original jar) | MAYBE | 5.406 | MAYBE | 44.374 | MAYBE | 55.661 |
| Julia_10_Iterative/Test2.mc (intermediate clpq, original jar) | YES | 1.792 | YES | 10.337 | YES | 8.697 |
| Julia_10_Iterative/Test3.mc (intermediate clpq, original jar) | TIMEOUT | 60 | MAYBE | 44.522 | TIMEOUT | 60 |
| Julia_10_Iterative/Test5.mc (intermediate clpq, original jar) | TIMEOUT | 60 | MAYBE | 44.661 | TIMEOUT | 60 |
| Julia_10_Iterative/Test7.mc (intermediate clpq, original jar) | MAYBE | 3.531 | MAYBE | 38.192 | TIMEOUT | 60 |
| Julia_10_Iterative/Test9.mc (intermediate clpq, original jar) | TIMEOUT | 60 | YES | 28.687 | TIMEOUT | 60 |
| Julia_10_Iterative/TriTas.mc (intermediate clpq, original jar) | MAYBE | 13.370 | TIMEOUT | 60 | TIMEOUT | 60 |