Model checking results
======================
inv1[0][2]..................................................................true
inv1[1][2]..................................................................true
inv2[0][0][2]...............................................................true
inv2[0][1][2]...............................................................true
inv2[1][0][2]...............................................................true
inv2[1][1][2]...............................................................true
inv3[0][4][2]...............................................................true
inv3[0][2][2]...............................................................true
inv3[0][2][4]...............................................................true
inv3[1][4][2]...............................................................true
inv3[1][2][2]...............................................................true
inv3[1][2][4]...............................................................true
valid[0][2].................................................................true
valid[1][2].................................................................true

See file "valid.warn" for warnings.

user time................................................................12.76 s
system time...............................................................0.42 s

Resources used
==============
user time................................................................12.76 s
system time...............................................................0.42 s
BDD nodes allocated........................................................62817
data segment size..............................................................0