AProVE & TcT
AProVE RNTSirc(n)O(1)O(n)O(n2)O(n3)O(n>3)EXPINF
O(1)411--------1
O(n)--17422------15
O(n2)--152------59
O(n3)----4152--15
O(n>3)----1--2--7
EXP--32------5
INF121222872--329