==> YES, main.fstb terminates. max_dim = 2

+-----------------------------------------------------------------------------+
|                             Ranking Function                                |
+-----------------------------------------------------------------------------+

state evalwisestart:
4

state evalwiseentryin:
3

state evalwisereturnin:
1

state evalwisebb6in:
2
(((-3*A)+(-3*B))+(6*A__o))+(6*B__o)

state evalwisebb3in:
2
(((-1+(-3*A))+(-3*B))+(6*A__o))+(6*B__o)

state evalwisebb4in:
2
(((-2+(-3*A))+(-3*B))+(6*A__o))+(6*B__o)

state evalwisebb5in:
2
(((-2+(-3*A))+(-3*B))+(6*A__o))+(6*B__o)

state evalwisestop:
0

state ____evalwisestart:
5


+-----------------------------------------------------------------------------+
|                         Worst Case Execution Time                           |
+-----------------------------------------------------------------------------+

/---
/
| A__o'+(-1*B__o') >= 0
| -2+B__o' >= 0
| 1 >= 0
\

(((((((1+1)+1)+((1+B__o')+A__o'))+((-2+B__o')+A__o'))+(-3+(2*B__o')))+((-2+B__o')+A__o'))+1)+1

/
| -3+(2*A__o') >= 0
| (-1*A__o')+B__o' >= 0
| -2+B__o' >= 0
| (1+A__o')+(-1*B__o') >= 0
\

(((((((1+1)+1)+((1+B__o')+A__o'))+((-2+B__o')+A__o'))+(-3+(2*B__o')))+(-2+(2*A__o')))+1)+1

/
| 1+(-1*B__o') >= 0
| (-3+A__o')+B__o' >= 0
| B__o' >= 0
\

((((((1+1)+1)+((1+B__o')+A__o'))+((-2+B__o')+A__o'))+((-2+B__o')+A__o'))+1)+1

/
| -3+(2*A__o') >= 0
| (-1+(-1*A__o'))+B__o' >= 0
| 1 >= 0
\

(((((((1+1)+1)+((1+B__o')+A__o'))+((-2+B__o')+A__o'))+((-2+B__o')+A__o'))+(-2+(2*A__o')))+1)+1

/
| -1+A__o' = 0
| -2+B__o' = 0
| 1 >= 0
\

((((((1+1)+1)+((1+B__o')+A__o'))+((-2+B__o')+A__o'))+(-3+(2*B__o')))+1)+1

/
| A__o' >= 0
| (-3+A__o')+B__o' >= 0
| 2+(-2*A__o') >= 0
\

((((((1+1)+1)+((1+B__o')+A__o'))+((-2+B__o')+A__o'))+((-2+B__o')+A__o'))+1)+1

/
| A__o' >= 0
| (-3+A__o')+B__o' >= 0
| (-2+(-1*A__o'))+B__o' >= 0
| 2+(-2*A__o') >= 0
\

((((((1+1)+1)+((1+B__o')+A__o'))+((-2+B__o')+A__o'))+((-2+B__o')+A__o'))+1)+1

/
| A__o' >= 0
| B__o' >= 0
| 1+(-1*B__o') >= 0
| 2+(-2*A__o') >= 0
\

((((1+1)+1)+((1+B__o')+A__o'))+1)+1

/
| B__o' >= 0
| A__o'+(-1*B__o') >= 0
| (2+(-1*A__o'))+(-1*B__o') >= 0
\

((((1+1)+1)+((1+B__o')+A__o'))+1)+1

/
| A__o' = 0
| -2+B__o' = 0
| 1 >= 0
\

((((1+1)+1)+((1+B__o')+A__o'))+1)+1

\---