Model checking results
======================
coin1[0][0][2]..............................................................true
coin1[1][0][2]..............................................................true
coin1[3][0][2]..............................................................true
coin1[0][1][2]..............................................................true
coin1[1][1][2]..............................................................true
coin1[3][1][2]..............................................................true
coin2[1][0].................................................................true
coin2[1][1].................................................................true
corrupted1[1][0]............................................................true
corrupted1[1][1]............................................................true
corrupted1[1][2]............................................................true
corrupted2[3][0][0].........................................................true
corrupted2[1][0][0].........................................................true
corrupted2[0][0][0].........................................................true
corrupted2[3][0][1].........................................................true
corrupted2[1][0][1].........................................................true
corrupted2[0][0][1].........................................................true
corrupted2[3][1][0].........................................................true
corrupted2[1][1][0].........................................................true
corrupted2[0][1][0].........................................................true
corrupted2[3][1][1].........................................................true
corrupted2[1][1][1].........................................................true
corrupted2[0][1][1].........................................................true
corrupted5[1][0][2].........................................................true
corrupted5[1][1][2].........................................................true
corrupted5[1][2][2].........................................................true
corrupted6[0][0][0][2]......................................................true
corrupted6[1][0][0][2]......................................................true
corrupted6[3][0][0][2]......................................................true
corrupted6[0][0][1][2]......................................................true
corrupted6[1][0][1][2]......................................................true
corrupted6[3][0][1][2]......................................................true
corrupted6[0][1][0][2]......................................................true
corrupted6[1][1][0][2]......................................................true
corrupted6[3][1][0][2]......................................................true
corrupted6[0][1][1][2]......................................................true
corrupted6[1][1][1][2]......................................................true
corrupted6[3][1][1][2]......................................................true
lemma1[0][2]................................................................true
lemma1[1][2]................................................................true
lemma10[0][0][0][2].........................................................true
lemma10[2][0][0][2].........................................................true
lemma10[0][0][1][2].........................................................true
lemma10[2][0][1][2].........................................................true
lemma10[0][1][0][2].........................................................true
lemma10[2][1][0][2].........................................................true
lemma10[0][1][1][2].........................................................true
lemma10[2][1][1][2].........................................................true
lemma11[1][0][0]............................................................true
lemma11[1][0][1]............................................................true
lemma11[1][1][0]............................................................true
lemma11[1][1][1]............................................................true
lemma12[2][0][0][1][2]......................................................true
lemma12[0][0][0][1][2]......................................................true
lemma12[2][0][0][4][2]......................................................true
lemma12[0][0][0][4][2]......................................................true
lemma12[2][0][1][1][2]......................................................true
lemma12[0][0][1][1][2]......................................................true
lemma12[2][0][1][4][2]......................................................true
lemma12[0][0][1][4][2]......................................................true
lemma12[2][1][0][1][2]......................................................true
lemma12[0][1][0][1][2]......................................................true
lemma12[2][1][0][4][2]......................................................true
lemma12[0][1][0][4][2]......................................................true
lemma12[2][1][1][1][2]......................................................true
lemma12[0][1][1][1][2]......................................................true
lemma12[2][1][1][4][2]......................................................true
lemma12[0][1][1][4][2]......................................................true
lemma13[2][0][0][0][2]......................................................true
lemma13[0][0][0][0][2]......................................................true
lemma13[2][0][0][2][2]......................................................true
lemma13[0][0][0][2][2]......................................................true
lemma13[2][0][1][0][2]......................................................true
lemma13[0][0][1][0][2]......................................................true
lemma13[2][0][1][2][2]......................................................true
lemma13[0][0][1][2][2]......................................................true
lemma13[2][1][0][0][2]......................................................true
lemma13[0][1][0][0][2]......................................................true
lemma13[2][1][0][2][2]......................................................true
lemma13[0][1][0][2][2]......................................................true
lemma13[2][1][1][0][2]......................................................true
lemma13[0][1][1][0][2]......................................................true
lemma13[2][1][1][2][2]......................................................true
lemma13[0][1][1][2][2]......................................................true
lemma14[2][0][0][2].........................................................true
lemma14[0][0][0][2].........................................................true
lemma14[2][0][2][2].........................................................true
lemma14[0][0][2][2].........................................................true
lemma14[2][0][4][2].........................................................true
lemma14[0][0][4][2].........................................................true
lemma14[2][0][3][2].........................................................true
lemma14[0][0][3][2].........................................................true
lemma14[2][1][0][2].........................................................true
lemma14[0][1][0][2].........................................................true
lemma14[2][1][2][2].........................................................true
lemma14[0][1][2][2].........................................................true
lemma14[2][1][4][2].........................................................true
lemma14[0][1][4][2].........................................................true
lemma14[2][1][3][2].........................................................true
lemma14[0][1][3][2].........................................................true
lemma15[2][0][0][2].........................................................true
lemma15[0][0][0][2].........................................................true
lemma15[2][0][2][2].........................................................true
lemma15[0][0][2][2].........................................................true
lemma15[2][0][4][2].........................................................true
lemma15[0][0][4][2].........................................................true
lemma15[2][0][3][2].........................................................true
lemma15[0][0][3][2].........................................................true
lemma15[2][1][0][2].........................................................true
lemma15[0][1][0][2].........................................................true
lemma15[2][1][2][2].........................................................true
lemma15[0][1][2][2].........................................................true
lemma15[2][1][4][2].........................................................true
lemma15[0][1][4][2].........................................................true
lemma15[2][1][3][2].........................................................true
lemma15[0][1][3][2].........................................................true
lemma16[1][0][3]............................................................true
lemma16[1][0][4]............................................................true
lemma16[1][0][1]............................................................true
lemma16[1][0][0]............................................................true
lemma16[1][1][3]............................................................true
lemma16[1][1][4]............................................................true
lemma16[1][1][1]............................................................true
lemma16[1][1][0]............................................................true
lemma17[1][0][3]............................................................true
lemma17[1][0][4]............................................................true
lemma17[1][0][1]............................................................true
lemma17[1][0][0]............................................................true
lemma17[1][1][3]............................................................true
lemma17[1][1][4]............................................................true
lemma17[1][1][1]............................................................true
lemma17[1][1][0]............................................................true
lemma18[1][1][2]............................................................true
lemma18[1][4][2]............................................................true
lemma19[1][4]...............................................................true
lemma19[1][1]...............................................................true
lemma2[0]...................................................................true
lemma2[1]...................................................................true
lemma20[1][1][2]............................................................true
lemma20[1][4][2]............................................................true
lemma21[1][0][2]............................................................true
lemma21[1][2][2]............................................................true
lemma22[1][0][1][2].........................................................true
lemma22[1][0][4][2].........................................................true
lemma22[1][1][1][2].........................................................true
lemma22[1][1][4][2].........................................................true
lemma22[1][2][1][2].........................................................true
lemma22[1][2][4][2].........................................................true
lemma23[1][0][4]............................................................true
lemma23[1][0][1]............................................................true
lemma23[1][1][4]............................................................true
lemma23[1][1][1]............................................................true
lemma23[1][2][4]............................................................true
lemma23[1][2][1]............................................................true
lemma24[1][0][2]............................................................true
lemma24[1][1][2]............................................................true
lemma24[1][2][2]............................................................true
lemma25[1][0]...............................................................true
lemma25[1][1]...............................................................true
lemma25[1][2]...............................................................true
lemma26[1][0][1][2].........................................................true
lemma26[1][0][4][2].........................................................true
lemma26[1][1][1][2].........................................................true
lemma26[1][1][4][2].........................................................true
lemma26[1][2][1][2].........................................................true
lemma26[1][2][4][2].........................................................true
lemma27[1][0][0][2].........................................................true
lemma27[1][0][2][2].........................................................true
lemma27[1][1][0][2].........................................................true
lemma27[1][1][2][2].........................................................true
lemma27[1][2][0][2].........................................................true
lemma27[1][2][2][2].........................................................true
lemma28[1][0][2]............................................................true
lemma28[1][2][2]............................................................true
lemma28[1][4][2]............................................................true
lemma28[1][3][2]............................................................true
lemma29[1][0][2]............................................................true
lemma29[1][2][2]............................................................true
lemma29[1][4][2]............................................................true
lemma29[1][3][2]............................................................true
lemma3[2]...................................................................true
lemma30[1][0][2]............................................................true
lemma30[1][2][2]............................................................true
lemma30[1][4][2]............................................................true
lemma30[1][3][2]............................................................true
lemma31[1][3]...............................................................true
lemma31[1][4]...............................................................true
lemma31[1][1]...............................................................true
lemma31[1][0]...............................................................true
lemma32[1][3]...............................................................true
lemma32[1][4]...............................................................true
lemma32[1][1]...............................................................true
lemma32[1][0]...............................................................true
lemma33[1][3]...............................................................true
lemma33[1][4]...............................................................true
lemma33[1][1]...............................................................true
lemma33[1][0]...............................................................true
lemma37[0][2]...............................................................true
lemma37[2][2]...............................................................true
lemma39[1][2][3]............................................................true
lemma39[1][2][1]............................................................true
lemma39[3][2][1]............................................................true
lemma4[2][0][2].............................................................true
lemma4[0][0][2].............................................................true
lemma4[2][2][2].............................................................true
lemma4[0][2][2].............................................................true
lemma4[2][4][2].............................................................true
lemma4[0][4][2].............................................................true
lemma40[1][4][2]............................................................true
lemma40[1][2][2]............................................................true
lemma40[1][2][4]............................................................true
lemma41[1][4][2]............................................................true
lemma41[1][2][2]............................................................true
lemma41[1][2][4]............................................................true
lemma5[1][4]................................................................true
lemma5[1][1]................................................................true
lemma6[2][1][2].............................................................true
lemma6[0][1][2].............................................................true
lemma6[2][4][2].............................................................true
lemma6[0][4][2].............................................................true
lemma7[2][0][2].............................................................true
lemma7[0][0][2].............................................................true
lemma7[2][2][2].............................................................true
lemma7[0][2][2].............................................................true
lemma8[2][0][0][1][2].......................................................true
lemma8[0][0][0][1][2].......................................................true
lemma8[2][0][0][4][2].......................................................true
lemma8[0][0][0][4][2].......................................................true
lemma8[2][0][1][1][2].......................................................true
lemma8[0][0][1][1][2].......................................................true
lemma8[2][0][1][4][2].......................................................true
lemma8[0][0][1][4][2].......................................................true
lemma8[2][1][0][1][2].......................................................true
lemma8[0][1][0][1][2].......................................................true
lemma8[2][1][0][4][2].......................................................true
lemma8[0][1][0][4][2].......................................................true
lemma8[2][1][1][1][2].......................................................true
lemma8[0][1][1][1][2].......................................................true
lemma8[2][1][1][4][2].......................................................true
lemma8[0][1][1][4][2].......................................................true
lemma9[1][0][0][4]..........................................................true
lemma9[1][0][0][1]..........................................................true
lemma9[1][0][1][4]..........................................................true
lemma9[1][0][1][1]..........................................................true
lemma9[1][1][0][4]..........................................................true
lemma9[1][1][0][1]..........................................................true
lemma9[1][1][1][4]..........................................................true
lemma9[1][1][1][1]..........................................................true

See file "lemmas.warn" for warnings.

user time...............................................................274.46 s
system time...............................................................2.75 s

Resources used
==============
user time...............................................................274.46 s
system time...............................................................2.75 s
BDD nodes allocated.......................................................186337
data segment size..............................................................0