Model checking results
======================
agree1[2][1][4].............................................................true
agree1[2][1][2].............................................................true
agree1[4][1][2].............................................................true
agree2[2][1][4].............................................................true
agree2[2][1][2].............................................................true
agree2[4][1][2].............................................................true
agree3[2][2][4].............................................................true
agree3[2][2][2].............................................................true
agree3[4][2][2].............................................................true
agree3[2][0][4].............................................................true
agree3[2][0][2].............................................................true
agree3[4][0][2].............................................................true
inv1[2][1][0]...............................................................true
inv1[2][1][1]...............................................................true
inv2[2][2][0][0][4].........................................................true
inv2[2][2][0][0][2].........................................................true
inv2[4][2][0][0][2].........................................................true
inv2[2][0][0][0][4].........................................................true
inv2[2][0][0][0][2].........................................................true
inv2[4][0][0][0][2].........................................................true
inv2[2][2][0][1][4].........................................................true
inv2[2][2][0][1][2].........................................................true
inv2[4][2][0][1][2].........................................................true
inv2[2][0][0][1][4].........................................................true
inv2[2][0][0][1][2].........................................................true
inv2[4][0][0][1][2].........................................................true
inv2[2][2][1][0][4].........................................................true
inv2[2][2][1][0][2].........................................................true
inv2[4][2][1][0][2].........................................................true
inv2[2][0][1][0][4].........................................................true
inv2[2][0][1][0][2].........................................................true
inv2[4][0][1][0][2].........................................................true
inv2[2][2][1][1][4].........................................................true
inv2[2][2][1][1][2].........................................................true
inv2[4][2][1][1][2].........................................................true
inv2[2][0][1][1][4].........................................................true
inv2[2][0][1][1][2].........................................................true
inv2[4][0][1][1][2].........................................................true
inv3[2][1][0][4]............................................................true
inv3[2][1][0][2]............................................................true
inv3[4][1][0][2]............................................................true
inv3[2][1][1][4]............................................................true
inv3[2][1][1][2]............................................................true
inv3[4][1][1][2]............................................................true
inv4[2][1][0][4]............................................................true
inv4[2][1][0][2]............................................................true
inv4[4][1][0][2]............................................................true
inv4[2][1][1][4]............................................................true
inv4[2][1][1][2]............................................................true
inv4[4][1][1][2]............................................................true

See file "agreement.warn" for warnings.

user time..............................................................1002.52 s
system time...............................................................1.87 s

Resources used
==============
user time..............................................................1002.52 s
system time...............................................................1.87 s
BDD nodes allocated.......................................................288935
data segment size..............................................................0