Model checking results
======================
inv1[1][0][2]...............................................................true
inv1[1][1][2]...............................................................true
inv10[1][0][2]..............................................................true
inv10[1][1][2]..............................................................true
inv2[0][0][2]...............................................................true
inv2[2][0][2]...............................................................true
inv2[0][1][2]...............................................................true
inv2[2][1][2]...............................................................true
inv3[1][0][2]...............................................................true
inv3[1][1][2]...............................................................true
inv4[1][0][2]...............................................................true
inv4[1][1][2]...............................................................true
inv5[1][0][2]...............................................................true
inv5[1][1][2]...............................................................true
inv6[1][0]..................................................................true
inv6[1][1]..................................................................true
inv7[1][0][2]...............................................................true
inv7[1][1][2]...............................................................true
inv8[0][0][2]...............................................................true
inv8[2][0][2]...............................................................true
inv8[0][1][2]...............................................................true
inv8[2][1][2]...............................................................true
inv9[1][0][2]...............................................................true
inv9[1][1][2]...............................................................true
progress1[1][0][2]..........................................................true
progress1[1][1][2]..........................................................true
progress2[0][0][2]..........................................................true
progress2[2][0][2]..........................................................true
progress2[0][1][2]..........................................................true
progress2[2][1][2]..........................................................true
progress3[1][2].............................................................true

See file "progress.warn" for warnings.

user time...............................................................201.08 s
system time...............................................................1.26 s

Resources used
==============
user time...............................................................201.08 s
system time...............................................................1.26 s
BDD nodes allocated.......................................................362976
data segment size..............................................................0