\define INIT (golden.bit0.value = 1 * (golden.bit1.value = 1 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (  faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * (  faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (  faulty.bit2.value = 0))))+ golden.bit1.value = 0 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * (  faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (  faulty.bit1.value = 0 * (faulty.bit2.value = 1 )))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (  faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (  faulty.bit1.value = 0 * (  faulty.bit2.value = 0)))))+ golden.bit0.value = 0 * (golden.bit1.value = 1 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (  faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 )))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (  faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * (  faulty.bit2.value = 0))))+ golden.bit1.value = 0 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (  faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * (  faulty.bit2.value = 0)))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (  faulty.bit1.value = 0 * (  faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (  faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))))))