(int x_0_0 0 12)
(int x_0_1 0 12)
(int x_0_2 0 12)
(int x_0_3 0 12)
(int x_0_4 0 12)
(int x_0_5 0 12)
(int x_0_6 0 12)
(int x_0_7 0 12)
(int x_1_0 0 12)
(int x_1_1 0 12)
(int x_1_2 0 12)
(int x_1_3 0 12)
(int x_1_4 0 12)
(int x_1_5 0 12)
(int x_1_6 0 12)
(int x_1_7 0 12)
(int x_2_0 0 12)
(int x_2_1 0 12)
(int x_2_2 0 12)
(int x_2_3 0 12)
(int x_2_4 0 12)
(int x_2_5 0 12)
(int x_2_6 0 12)
(int x_2_7 0 12)
(int x_3_0 0 12)
(int x_3_1 0 12)
(int x_3_2 0 12)
(int x_3_3 0 12)
(int x_3_4 0 12)
(int x_3_5 0 12)
(int x_3_6 0 12)
(int x_3_7 0 12)
(int x_4_0 0 12)
(int x_4_1 0 12)
(int x_4_2 0 12)
(int x_4_3 0 12)
(int x_4_4 0 12)
(int x_4_5 0 12)
(int x_4_6 0 12)
(int x_4_7 0 12)
(int x_5_0 0 12)
(int x_5_1 0 12)
(int x_5_2 0 12)
(int x_5_3 0 12)
(int x_5_4 0 12)
(int x_5_5 0 12)
(int x_5_6 0 12)
(int x_5_7 0 12)

(||
(&&
(= x_0_0 1)
(= x_0_1 2)
(= x_0_2 3)
(= x_0_3 0)
)
(&&
(= x_0_0 0)
(= x_0_1 1)
(= x_0_2 2)
(= x_0_3 3)
(= x_0_4 0)
)
(&&
(= x_0_1 0)
(= x_0_2 1)
(= x_0_3 2)
(= x_0_4 3)
(= x_0_5 0)
)
(&&
(= x_0_2 0)
(= x_0_3 1)
(= x_0_4 2)
(= x_0_5 3)
(= x_0_6 0)
)
(&&
(= x_0_3 0)
(= x_0_4 1)
(= x_0_5 2)
(= x_0_6 3)
(= x_0_7 0)
)
(&&
(= x_0_4 0)
(= x_0_5 1)
(= x_0_6 2)
(= x_0_7 3)
)
(&&
(= x_1_0 1)
(= x_1_1 2)
(= x_1_2 3)
(= x_1_3 0)
)
(&&
(= x_1_0 0)
(= x_1_1 1)
(= x_1_2 2)
(= x_1_3 3)
(= x_1_4 0)
)
(&&
(= x_1_1 0)
(= x_1_2 1)
(= x_1_3 2)
(= x_1_4 3)
(= x_1_5 0)
)
(&&
(= x_1_2 0)
(= x_1_3 1)
(= x_1_4 2)
(= x_1_5 3)
(= x_1_6 0)
)
(&&
(= x_1_3 0)
(= x_1_4 1)
(= x_1_5 2)
(= x_1_6 3)
(= x_1_7 0)
)
(&&
(= x_1_4 0)
(= x_1_5 1)
(= x_1_6 2)
(= x_1_7 3)
)
(&&
(= x_2_0 1)
(= x_2_1 2)
(= x_2_2 3)
(= x_2_3 0)
)
(&&
(= x_2_0 0)
(= x_2_1 1)
(= x_2_2 2)
(= x_2_3 3)
(= x_2_4 0)
)
(&&
(= x_2_1 0)
(= x_2_2 1)
(= x_2_3 2)
(= x_2_4 3)
(= x_2_5 0)
)
(&&
(= x_2_2 0)
(= x_2_3 1)
(= x_2_4 2)
(= x_2_5 3)
(= x_2_6 0)
)
(&&
(= x_2_3 0)
(= x_2_4 1)
(= x_2_5 2)
(= x_2_6 3)
(= x_2_7 0)
)
(&&
(= x_2_4 0)
(= x_2_5 1)
(= x_2_6 2)
(= x_2_7 3)
)
(&&
(= x_3_0 1)
(= x_3_1 2)
(= x_3_2 3)
(= x_3_3 0)
)
(&&
(= x_3_0 0)
(= x_3_1 1)
(= x_3_2 2)
(= x_3_3 3)
(= x_3_4 0)
)
(&&
(= x_3_1 0)
(= x_3_2 1)
(= x_3_3 2)
(= x_3_4 3)
(= x_3_5 0)
)
(&&
(= x_3_2 0)
(= x_3_3 1)
(= x_3_4 2)
(= x_3_5 3)
(= x_3_6 0)
)
(&&
(= x_3_3 0)
(= x_3_4 1)
(= x_3_5 2)
(= x_3_6 3)
(= x_3_7 0)
)
(&&
(= x_3_4 0)
(= x_3_5 1)
(= x_3_6 2)
(= x_3_7 3)
)
(&&
(= x_4_0 1)
(= x_4_1 2)
(= x_4_2 3)
(= x_4_3 0)
)
(&&
(= x_4_0 0)
(= x_4_1 1)
(= x_4_2 2)
(= x_4_3 3)
(= x_4_4 0)
)
(&&
(= x_4_1 0)
(= x_4_2 1)
(= x_4_3 2)
(= x_4_4 3)
(= x_4_5 0)
)
(&&
(= x_4_2 0)
(= x_4_3 1)
(= x_4_4 2)
(= x_4_5 3)
(= x_4_6 0)
)
(&&
(= x_4_3 0)
(= x_4_4 1)
(= x_4_5 2)
(= x_4_6 3)
(= x_4_7 0)
)
(&&
(= x_4_4 0)
(= x_4_5 1)
(= x_4_6 2)
(= x_4_7 3)
)
(&&
(= x_5_0 1)
(= x_5_1 2)
(= x_5_2 3)
(= x_5_3 0)
)
(&&
(= x_5_0 0)
(= x_5_1 1)
(= x_5_2 2)
(= x_5_3 3)
(= x_5_4 0)
)
(&&
(= x_5_1 0)
(= x_5_2 1)
(= x_5_3 2)
(= x_5_4 3)
(= x_5_5 0)
)
(&&
(= x_5_2 0)
(= x_5_3 1)
(= x_5_4 2)
(= x_5_5 3)
(= x_5_6 0)
)
(&&
(= x_5_3 0)
(= x_5_4 1)
(= x_5_5 2)
(= x_5_6 3)
(= x_5_7 0)
)
(&&
(= x_5_4 0)
(= x_5_5 1)
(= x_5_6 2)
(= x_5_7 3)
)
(&&
(= x_0_0 1)
(= x_1_0 2)
(= x_2_0 3)
(= x_0_3 0)
)
(&&
(= x_0_0 0)
(= x_1_0 1)
(= x_2_0 2)
(= x_3_0 3)
(= x_0_4 0)
)
(&&
(= x_0_1 0)
(= x_2_0 1)
(= x_3_0 2)
(= x_4_0 3)
(= x_0_5 0)
)
(&&
(= x_0_2 0)
(= x_3_0 1)
(= x_4_0 2)
(= x_5_0 3)
(= x_0_6 0)
)
(&&
(= x_0_1 1)
(= x_1_1 2)
(= x_2_1 3)
(= x_1_3 0)
)
(&&
(= x_1_0 0)
(= x_1_1 1)
(= x_2_1 2)
(= x_3_1 3)
(= x_1_4 0)
)
(&&
(= x_1_1 0)
(= x_2_1 1)
(= x_3_1 2)
(= x_4_1 3)
(= x_1_5 0)
)
(&&
(= x_1_2 0)
(= x_3_1 1)
(= x_4_1 2)
(= x_5_1 3)
(= x_1_6 0)
)
(&&
(= x_0_2 1)
(= x_1_2 2)
(= x_2_2 3)
(= x_2_3 0)
)
(&&
(= x_2_0 0)
(= x_1_2 1)
(= x_2_2 2)
(= x_3_2 3)
(= x_2_4 0)
)
(&&
(= x_2_1 0)
(= x_2_2 1)
(= x_3_2 2)
(= x_4_2 3)
(= x_2_5 0)
)
(&&
(= x_2_2 0)
(= x_3_2 1)
(= x_4_2 2)
(= x_5_2 3)
(= x_2_6 0)
)
(&&
(= x_0_3 1)
(= x_1_3 2)
(= x_2_3 3)
(= x_3_3 0)
)
(&&
(= x_3_0 0)
(= x_1_3 1)
(= x_2_3 2)
(= x_3_3 3)
(= x_3_4 0)
)
(&&
(= x_3_1 0)
(= x_2_3 1)
(= x_3_3 2)
(= x_4_3 3)
(= x_3_5 0)
)
(&&
(= x_3_2 0)
(= x_3_3 1)
(= x_4_3 2)
(= x_5_3 3)
(= x_3_6 0)
)
(&&
(= x_0_4 1)
(= x_1_4 2)
(= x_2_4 3)
(= x_4_3 0)
)
(&&
(= x_4_0 0)
(= x_1_4 1)
(= x_2_4 2)
(= x_3_4 3)
(= x_4_4 0)
)
(&&
(= x_4_1 0)
(= x_2_4 1)
(= x_3_4 2)
(= x_4_4 3)
(= x_4_5 0)
)
(&&
(= x_4_2 0)
(= x_3_4 1)
(= x_4_4 2)
(= x_5_4 3)
(= x_4_6 0)
)
(&&
(= x_0_5 1)
(= x_1_5 2)
(= x_2_5 3)
(= x_5_3 0)
)
(&&
(= x_5_0 0)
(= x_1_5 1)
(= x_2_5 2)
(= x_3_5 3)
(= x_5_4 0)
)
(&&
(= x_5_1 0)
(= x_2_5 1)
(= x_3_5 2)
(= x_4_5 3)
(= x_5_5 0)
)
(&&
(= x_5_2 0)
(= x_3_5 1)
(= x_4_5 2)
(= x_5_5 3)
(= x_5_6 0)
)
(&&
(= x_0_6 1)
(= x_1_6 2)
(= x_2_6 3)
(= x_6_3 0)
)
(&&
(= x_6_0 0)
(= x_1_6 1)
(= x_2_6 2)
(= x_3_6 3)
(= x_6_4 0)
)
(&&
(= x_6_1 0)
(= x_2_6 1)
(= x_3_6 2)
(= x_4_6 3)
(= x_6_5 0)
)
(&&
(= x_6_2 0)
(= x_3_6 1)
(= x_4_6 2)
(= x_5_6 3)
(= x_6_6 0)
)
(&&
(= x_0_7 1)
(= x_1_7 2)
(= x_2_7 3)
(= x_7_3 0)
)
(&&
(= x_7_0 0)
(= x_1_7 1)
(= x_2_7 2)
(= x_3_7 3)
(= x_7_4 0)
)
(&&
(= x_7_1 0)
(= x_2_7 1)
(= x_3_7 2)
(= x_4_7 3)
(= x_7_5 0)
)
(&&
(= x_7_2 0)
(= x_3_7 1)
(= x_4_7 2)
(= x_5_7 3)
(= x_7_6 0)
)
)
(||
(&&
(= x_0_0 3)
(= x_0_1 4)
(= x_0_2 5)
(= x_0_3 0)
)
(&&
(= x_0_0 0)
(= x_0_1 3)
(= x_0_2 4)
(= x_0_3 5)
(= x_0_4 0)
)
(&&
(= x_0_1 0)
(= x_0_2 3)
(= x_0_3 4)
(= x_0_4 5)
(= x_0_5 0)
)
(&&
(= x_0_2 0)
(= x_0_3 3)
(= x_0_4 4)
(= x_0_5 5)
(= x_0_6 0)
)
(&&
(= x_0_3 0)
(= x_0_4 3)
(= x_0_5 4)
(= x_0_6 5)
(= x_0_7 0)
)
(&&
(= x_0_4 0)
(= x_0_5 3)
(= x_0_6 4)
(= x_0_7 5)
)
(&&
(= x_1_0 3)
(= x_1_1 4)
(= x_1_2 5)
(= x_1_3 0)
)
(&&
(= x_1_0 0)
(= x_1_1 3)
(= x_1_2 4)
(= x_1_3 5)
(= x_1_4 0)
)
(&&
(= x_1_1 0)
(= x_1_2 3)
(= x_1_3 4)
(= x_1_4 5)
(= x_1_5 0)
)
(&&
(= x_1_2 0)
(= x_1_3 3)
(= x_1_4 4)
(= x_1_5 5)
(= x_1_6 0)
)
(&&
(= x_1_3 0)
(= x_1_4 3)
(= x_1_5 4)
(= x_1_6 5)
(= x_1_7 0)
)
(&&
(= x_1_4 0)
(= x_1_5 3)
(= x_1_6 4)
(= x_1_7 5)
)
(&&
(= x_2_0 3)
(= x_2_1 4)
(= x_2_2 5)
(= x_2_3 0)
)
(&&
(= x_2_0 0)
(= x_2_1 3)
(= x_2_2 4)
(= x_2_3 5)
(= x_2_4 0)
)
(&&
(= x_2_1 0)
(= x_2_2 3)
(= x_2_3 4)
(= x_2_4 5)
(= x_2_5 0)
)
(&&
(= x_2_2 0)
(= x_2_3 3)
(= x_2_4 4)
(= x_2_5 5)
(= x_2_6 0)
)
(&&
(= x_2_3 0)
(= x_2_4 3)
(= x_2_5 4)
(= x_2_6 5)
(= x_2_7 0)
)
(&&
(= x_2_4 0)
(= x_2_5 3)
(= x_2_6 4)
(= x_2_7 5)
)
(&&
(= x_3_0 3)
(= x_3_1 4)
(= x_3_2 5)
(= x_3_3 0)
)
(&&
(= x_3_0 0)
(= x_3_1 3)
(= x_3_2 4)
(= x_3_3 5)
(= x_3_4 0)
)
(&&
(= x_3_1 0)
(= x_3_2 3)
(= x_3_3 4)
(= x_3_4 5)
(= x_3_5 0)
)
(&&
(= x_3_2 0)
(= x_3_3 3)
(= x_3_4 4)
(= x_3_5 5)
(= x_3_6 0)
)
(&&
(= x_3_3 0)
(= x_3_4 3)
(= x_3_5 4)
(= x_3_6 5)
(= x_3_7 0)
)
(&&
(= x_3_4 0)
(= x_3_5 3)
(= x_3_6 4)
(= x_3_7 5)
)
(&&
(= x_4_0 3)
(= x_4_1 4)
(= x_4_2 5)
(= x_4_3 0)
)
(&&
(= x_4_0 0)
(= x_4_1 3)
(= x_4_2 4)
(= x_4_3 5)
(= x_4_4 0)
)
(&&
(= x_4_1 0)
(= x_4_2 3)
(= x_4_3 4)
(= x_4_4 5)
(= x_4_5 0)
)
(&&
(= x_4_2 0)
(= x_4_3 3)
(= x_4_4 4)
(= x_4_5 5)
(= x_4_6 0)
)
(&&
(= x_4_3 0)
(= x_4_4 3)
(= x_4_5 4)
(= x_4_6 5)
(= x_4_7 0)
)
(&&
(= x_4_4 0)
(= x_4_5 3)
(= x_4_6 4)
(= x_4_7 5)
)
(&&
(= x_5_0 3)
(= x_5_1 4)
(= x_5_2 5)
(= x_5_3 0)
)
(&&
(= x_5_0 0)
(= x_5_1 3)
(= x_5_2 4)
(= x_5_3 5)
(= x_5_4 0)
)
(&&
(= x_5_1 0)
(= x_5_2 3)
(= x_5_3 4)
(= x_5_4 5)
(= x_5_5 0)
)
(&&
(= x_5_2 0)
(= x_5_3 3)
(= x_5_4 4)
(= x_5_5 5)
(= x_5_6 0)
)
(&&
(= x_5_3 0)
(= x_5_4 3)
(= x_5_5 4)
(= x_5_6 5)
(= x_5_7 0)
)
(&&
(= x_5_4 0)
(= x_5_5 3)
(= x_5_6 4)
(= x_5_7 5)
)
(&&
(= x_0_0 3)
(= x_1_0 4)
(= x_2_0 5)
(= x_0_3 0)
)
(&&
(= x_0_0 0)
(= x_1_0 3)
(= x_2_0 4)
(= x_3_0 5)
(= x_0_4 0)
)
(&&
(= x_0_1 0)
(= x_2_0 3)
(= x_3_0 4)
(= x_4_0 5)
(= x_0_5 0)
)
(&&
(= x_0_2 0)
(= x_3_0 3)
(= x_4_0 4)
(= x_5_0 5)
(= x_0_6 0)
)
(&&
(= x_0_1 3)
(= x_1_1 4)
(= x_2_1 5)
(= x_1_3 0)
)
(&&
(= x_1_0 0)
(= x_1_1 3)
(= x_2_1 4)
(= x_3_1 5)
(= x_1_4 0)
)
(&&
(= x_1_1 0)
(= x_2_1 3)
(= x_3_1 4)
(= x_4_1 5)
(= x_1_5 0)
)
(&&
(= x_1_2 0)
(= x_3_1 3)
(= x_4_1 4)
(= x_5_1 5)
(= x_1_6 0)
)
(&&
(= x_0_2 3)
(= x_1_2 4)
(= x_2_2 5)
(= x_2_3 0)
)
(&&
(= x_2_0 0)
(= x_1_2 3)
(= x_2_2 4)
(= x_3_2 5)
(= x_2_4 0)
)
(&&
(= x_2_1 0)
(= x_2_2 3)
(= x_3_2 4)
(= x_4_2 5)
(= x_2_5 0)
)
(&&
(= x_2_2 0)
(= x_3_2 3)
(= x_4_2 4)
(= x_5_2 5)
(= x_2_6 0)
)
(&&
(= x_0_3 3)
(= x_1_3 4)
(= x_2_3 5)
(= x_3_3 0)
)
(&&
(= x_3_0 0)
(= x_1_3 3)
(= x_2_3 4)
(= x_3_3 5)
(= x_3_4 0)
)
(&&
(= x_3_1 0)
(= x_2_3 3)
(= x_3_3 4)
(= x_4_3 5)
(= x_3_5 0)
)
(&&
(= x_3_2 0)
(= x_3_3 3)
(= x_4_3 4)
(= x_5_3 5)
(= x_3_6 0)
)
(&&
(= x_0_4 3)
(= x_1_4 4)
(= x_2_4 5)
(= x_4_3 0)
)
(&&
(= x_4_0 0)
(= x_1_4 3)
(= x_2_4 4)
(= x_3_4 5)
(= x_4_4 0)
)
(&&
(= x_4_1 0)
(= x_2_4 3)
(= x_3_4 4)
(= x_4_4 5)
(= x_4_5 0)
)
(&&
(= x_4_2 0)
(= x_3_4 3)
(= x_4_4 4)
(= x_5_4 5)
(= x_4_6 0)
)
(&&
(= x_0_5 3)
(= x_1_5 4)
(= x_2_5 5)
(= x_5_3 0)
)
(&&
(= x_5_0 0)
(= x_1_5 3)
(= x_2_5 4)
(= x_3_5 5)
(= x_5_4 0)
)
(&&
(= x_5_1 0)
(= x_2_5 3)
(= x_3_5 4)
(= x_4_5 5)
(= x_5_5 0)
)
(&&
(= x_5_2 0)
(= x_3_5 3)
(= x_4_5 4)
(= x_5_5 5)
(= x_5_6 0)
)
(&&
(= x_0_6 3)
(= x_1_6 4)
(= x_2_6 5)
(= x_6_3 0)
)
(&&
(= x_6_0 0)
(= x_1_6 3)
(= x_2_6 4)
(= x_3_6 5)
(= x_6_4 0)
)
(&&
(= x_6_1 0)
(= x_2_6 3)
(= x_3_6 4)
(= x_4_6 5)
(= x_6_5 0)
)
(&&
(= x_6_2 0)
(= x_3_6 3)
(= x_4_6 4)
(= x_5_6 5)
(= x_6_6 0)
)
(&&
(= x_0_7 3)
(= x_1_7 4)
(= x_2_7 5)
(= x_7_3 0)
)
(&&
(= x_7_0 0)
(= x_1_7 3)
(= x_2_7 4)
(= x_3_7 5)
(= x_7_4 0)
)
(&&
(= x_7_1 0)
(= x_2_7 3)
(= x_3_7 4)
(= x_4_7 5)
(= x_7_5 0)
)
(&&
(= x_7_2 0)
(= x_3_7 3)
(= x_4_7 4)
(= x_5_7 5)
(= x_7_6 0)
)
)
(||
(&&
(= x_0_0 2)
(= x_0_1 6)
(= x_0_2 1)
(= x_0_3 7)
(= x_0_4 0)
)
(&&
(= x_0_0 0)
(= x_0_1 2)
(= x_0_2 6)
(= x_0_3 1)
(= x_0_4 7)
(= x_0_5 0)
)
(&&
(= x_0_1 0)
(= x_0_2 2)
(= x_0_3 6)
(= x_0_4 1)
(= x_0_5 7)
(= x_0_6 0)
)
(&&
(= x_0_2 0)
(= x_0_3 2)
(= x_0_4 6)
(= x_0_5 1)
(= x_0_6 7)
(= x_0_7 0)
)
(&&
(= x_0_3 0)
(= x_0_4 2)
(= x_0_5 6)
(= x_0_6 1)
(= x_0_7 7)
)
(&&
(= x_1_0 2)
(= x_1_1 6)
(= x_1_2 1)
(= x_1_3 7)
(= x_1_4 0)
)
(&&
(= x_1_0 0)
(= x_1_1 2)
(= x_1_2 6)
(= x_1_3 1)
(= x_1_4 7)
(= x_1_5 0)
)
(&&
(= x_1_1 0)
(= x_1_2 2)
(= x_1_3 6)
(= x_1_4 1)
(= x_1_5 7)
(= x_1_6 0)
)
(&&
(= x_1_2 0)
(= x_1_3 2)
(= x_1_4 6)
(= x_1_5 1)
(= x_1_6 7)
(= x_1_7 0)
)
(&&
(= x_1_3 0)
(= x_1_4 2)
(= x_1_5 6)
(= x_1_6 1)
(= x_1_7 7)
)
(&&
(= x_2_0 2)
(= x_2_1 6)
(= x_2_2 1)
(= x_2_3 7)
(= x_2_4 0)
)
(&&
(= x_2_0 0)
(= x_2_1 2)
(= x_2_2 6)
(= x_2_3 1)
(= x_2_4 7)
(= x_2_5 0)
)
(&&
(= x_2_1 0)
(= x_2_2 2)
(= x_2_3 6)
(= x_2_4 1)
(= x_2_5 7)
(= x_2_6 0)
)
(&&
(= x_2_2 0)
(= x_2_3 2)
(= x_2_4 6)
(= x_2_5 1)
(= x_2_6 7)
(= x_2_7 0)
)
(&&
(= x_2_3 0)
(= x_2_4 2)
(= x_2_5 6)
(= x_2_6 1)
(= x_2_7 7)
)
(&&
(= x_3_0 2)
(= x_3_1 6)
(= x_3_2 1)
(= x_3_3 7)
(= x_3_4 0)
)
(&&
(= x_3_0 0)
(= x_3_1 2)
(= x_3_2 6)
(= x_3_3 1)
(= x_3_4 7)
(= x_3_5 0)
)
(&&
(= x_3_1 0)
(= x_3_2 2)
(= x_3_3 6)
(= x_3_4 1)
(= x_3_5 7)
(= x_3_6 0)
)
(&&
(= x_3_2 0)
(= x_3_3 2)
(= x_3_4 6)
(= x_3_5 1)
(= x_3_6 7)
(= x_3_7 0)
)
(&&
(= x_3_3 0)
(= x_3_4 2)
(= x_3_5 6)
(= x_3_6 1)
(= x_3_7 7)
)
(&&
(= x_4_0 2)
(= x_4_1 6)
(= x_4_2 1)
(= x_4_3 7)
(= x_4_4 0)
)
(&&
(= x_4_0 0)
(= x_4_1 2)
(= x_4_2 6)
(= x_4_3 1)
(= x_4_4 7)
(= x_4_5 0)
)
(&&
(= x_4_1 0)
(= x_4_2 2)
(= x_4_3 6)
(= x_4_4 1)
(= x_4_5 7)
(= x_4_6 0)
)
(&&
(= x_4_2 0)
(= x_4_3 2)
(= x_4_4 6)
(= x_4_5 1)
(= x_4_6 7)
(= x_4_7 0)
)
(&&
(= x_4_3 0)
(= x_4_4 2)
(= x_4_5 6)
(= x_4_6 1)
(= x_4_7 7)
)
(&&
(= x_5_0 2)
(= x_5_1 6)
(= x_5_2 1)
(= x_5_3 7)
(= x_5_4 0)
)
(&&
(= x_5_0 0)
(= x_5_1 2)
(= x_5_2 6)
(= x_5_3 1)
(= x_5_4 7)
(= x_5_5 0)
)
(&&
(= x_5_1 0)
(= x_5_2 2)
(= x_5_3 6)
(= x_5_4 1)
(= x_5_5 7)
(= x_5_6 0)
)
(&&
(= x_5_2 0)
(= x_5_3 2)
(= x_5_4 6)
(= x_5_5 1)
(= x_5_6 7)
(= x_5_7 0)
)
(&&
(= x_5_3 0)
(= x_5_4 2)
(= x_5_5 6)
(= x_5_6 1)
(= x_5_7 7)
)
(&&
(= x_0_0 2)
(= x_1_0 6)
(= x_2_0 1)
(= x_3_0 7)
(= x_0_4 0)
)
(&&
(= x_0_0 0)
(= x_1_0 2)
(= x_2_0 6)
(= x_3_0 1)
(= x_4_0 7)
(= x_0_5 0)
)
(&&
(= x_0_1 0)
(= x_2_0 2)
(= x_3_0 6)
(= x_4_0 1)
(= x_5_0 7)
(= x_0_6 0)
)
(&&
(= x_0_1 2)
(= x_1_1 6)
(= x_2_1 1)
(= x_3_1 7)
(= x_1_4 0)
)
(&&
(= x_1_0 0)
(= x_1_1 2)
(= x_2_1 6)
(= x_3_1 1)
(= x_4_1 7)
(= x_1_5 0)
)
(&&
(= x_1_1 0)
(= x_2_1 2)
(= x_3_1 6)
(= x_4_1 1)
(= x_5_1 7)
(= x_1_6 0)
)
(&&
(= x_0_2 2)
(= x_1_2 6)
(= x_2_2 1)
(= x_3_2 7)
(= x_2_4 0)
)
(&&
(= x_2_0 0)
(= x_1_2 2)
(= x_2_2 6)
(= x_3_2 1)
(= x_4_2 7)
(= x_2_5 0)
)
(&&
(= x_2_1 0)
(= x_2_2 2)
(= x_3_2 6)
(= x_4_2 1)
(= x_5_2 7)
(= x_2_6 0)
)
(&&
(= x_0_3 2)
(= x_1_3 6)
(= x_2_3 1)
(= x_3_3 7)
(= x_3_4 0)
)
(&&
(= x_3_0 0)
(= x_1_3 2)
(= x_2_3 6)
(= x_3_3 1)
(= x_4_3 7)
(= x_3_5 0)
)
(&&
(= x_3_1 0)
(= x_2_3 2)
(= x_3_3 6)
(= x_4_3 1)
(= x_5_3 7)
(= x_3_6 0)
)
(&&
(= x_0_4 2)
(= x_1_4 6)
(= x_2_4 1)
(= x_3_4 7)
(= x_4_4 0)
)
(&&
(= x_4_0 0)
(= x_1_4 2)
(= x_2_4 6)
(= x_3_4 1)
(= x_4_4 7)
(= x_4_5 0)
)
(&&
(= x_4_1 0)
(= x_2_4 2)
(= x_3_4 6)
(= x_4_4 1)
(= x_5_4 7)
(= x_4_6 0)
)
(&&
(= x_0_5 2)
(= x_1_5 6)
(= x_2_5 1)
(= x_3_5 7)
(= x_5_4 0)
)
(&&
(= x_5_0 0)
(= x_1_5 2)
(= x_2_5 6)
(= x_3_5 1)
(= x_4_5 7)
(= x_5_5 0)
)
(&&
(= x_5_1 0)
(= x_2_5 2)
(= x_3_5 6)
(= x_4_5 1)
(= x_5_5 7)
(= x_5_6 0)
)
(&&
(= x_0_6 2)
(= x_1_6 6)
(= x_2_6 1)
(= x_3_6 7)
(= x_6_4 0)
)
(&&
(= x_6_0 0)
(= x_1_6 2)
(= x_2_6 6)
(= x_3_6 1)
(= x_4_6 7)
(= x_6_5 0)
)
(&&
(= x_6_1 0)
(= x_2_6 2)
(= x_3_6 6)
(= x_4_6 1)
(= x_5_6 7)
(= x_6_6 0)
)
(&&
(= x_0_7 2)
(= x_1_7 6)
(= x_2_7 1)
(= x_3_7 7)
(= x_7_4 0)
)
(&&
(= x_7_0 0)
(= x_1_7 2)
(= x_2_7 6)
(= x_3_7 1)
(= x_4_7 7)
(= x_7_5 0)
)
(&&
(= x_7_1 0)
(= x_2_7 2)
(= x_3_7 6)
(= x_4_7 1)
(= x_5_7 7)
(= x_7_6 0)
)
)
(||
(&&
(= x_0_0 5)
(= x_0_1 2)
(= x_0_2 8)
(= x_0_3 7)
(= x_0_4 0)
)
(&&
(= x_0_0 0)
(= x_0_1 5)
(= x_0_2 2)
(= x_0_3 8)
(= x_0_4 7)
(= x_0_5 0)
)
(&&
(= x_0_1 0)
(= x_0_2 5)
(= x_0_3 2)
(= x_0_4 8)
(= x_0_5 7)
(= x_0_6 0)
)
(&&
(= x_0_2 0)
(= x_0_3 5)
(= x_0_4 2)
(= x_0_5 8)
(= x_0_6 7)
(= x_0_7 0)
)
(&&
(= x_0_3 0)
(= x_0_4 5)
(= x_0_5 2)
(= x_0_6 8)
(= x_0_7 7)
)
(&&
(= x_1_0 5)
(= x_1_1 2)
(= x_1_2 8)
(= x_1_3 7)
(= x_1_4 0)
)
(&&
(= x_1_0 0)
(= x_1_1 5)
(= x_1_2 2)
(= x_1_3 8)
(= x_1_4 7)
(= x_1_5 0)
)
(&&
(= x_1_1 0)
(= x_1_2 5)
(= x_1_3 2)
(= x_1_4 8)
(= x_1_5 7)
(= x_1_6 0)
)
(&&
(= x_1_2 0)
(= x_1_3 5)
(= x_1_4 2)
(= x_1_5 8)
(= x_1_6 7)
(= x_1_7 0)
)
(&&
(= x_1_3 0)
(= x_1_4 5)
(= x_1_5 2)
(= x_1_6 8)
(= x_1_7 7)
)
(&&
(= x_2_0 5)
(= x_2_1 2)
(= x_2_2 8)
(= x_2_3 7)
(= x_2_4 0)
)
(&&
(= x_2_0 0)
(= x_2_1 5)
(= x_2_2 2)
(= x_2_3 8)
(= x_2_4 7)
(= x_2_5 0)
)
(&&
(= x_2_1 0)
(= x_2_2 5)
(= x_2_3 2)
(= x_2_4 8)
(= x_2_5 7)
(= x_2_6 0)
)
(&&
(= x_2_2 0)
(= x_2_3 5)
(= x_2_4 2)
(= x_2_5 8)
(= x_2_6 7)
(= x_2_7 0)
)
(&&
(= x_2_3 0)
(= x_2_4 5)
(= x_2_5 2)
(= x_2_6 8)
(= x_2_7 7)
)
(&&
(= x_3_0 5)
(= x_3_1 2)
(= x_3_2 8)
(= x_3_3 7)
(= x_3_4 0)
)
(&&
(= x_3_0 0)
(= x_3_1 5)
(= x_3_2 2)
(= x_3_3 8)
(= x_3_4 7)
(= x_3_5 0)
)
(&&
(= x_3_1 0)
(= x_3_2 5)
(= x_3_3 2)
(= x_3_4 8)
(= x_3_5 7)
(= x_3_6 0)
)
(&&
(= x_3_2 0)
(= x_3_3 5)
(= x_3_4 2)
(= x_3_5 8)
(= x_3_6 7)
(= x_3_7 0)
)
(&&
(= x_3_3 0)
(= x_3_4 5)
(= x_3_5 2)
(= x_3_6 8)
(= x_3_7 7)
)
(&&
(= x_4_0 5)
(= x_4_1 2)
(= x_4_2 8)
(= x_4_3 7)
(= x_4_4 0)
)
(&&
(= x_4_0 0)
(= x_4_1 5)
(= x_4_2 2)
(= x_4_3 8)
(= x_4_4 7)
(= x_4_5 0)
)
(&&
(= x_4_1 0)
(= x_4_2 5)
(= x_4_3 2)
(= x_4_4 8)
(= x_4_5 7)
(= x_4_6 0)
)
(&&
(= x_4_2 0)
(= x_4_3 5)
(= x_4_4 2)
(= x_4_5 8)
(= x_4_6 7)
(= x_4_7 0)
)
(&&
(= x_4_3 0)
(= x_4_4 5)
(= x_4_5 2)
(= x_4_6 8)
(= x_4_7 7)
)
(&&
(= x_5_0 5)
(= x_5_1 2)
(= x_5_2 8)
(= x_5_3 7)
(= x_5_4 0)
)
(&&
(= x_5_0 0)
(= x_5_1 5)
(= x_5_2 2)
(= x_5_3 8)
(= x_5_4 7)
(= x_5_5 0)
)
(&&
(= x_5_1 0)
(= x_5_2 5)
(= x_5_3 2)
(= x_5_4 8)
(= x_5_5 7)
(= x_5_6 0)
)
(&&
(= x_5_2 0)
(= x_5_3 5)
(= x_5_4 2)
(= x_5_5 8)
(= x_5_6 7)
(= x_5_7 0)
)
(&&
(= x_5_3 0)
(= x_5_4 5)
(= x_5_5 2)
(= x_5_6 8)
(= x_5_7 7)
)
(&&
(= x_0_0 5)
(= x_1_0 2)
(= x_2_0 8)
(= x_3_0 7)
(= x_0_4 0)
)
(&&
(= x_0_0 0)
(= x_1_0 5)
(= x_2_0 2)
(= x_3_0 8)
(= x_4_0 7)
(= x_0_5 0)
)
(&&
(= x_0_1 0)
(= x_2_0 5)
(= x_3_0 2)
(= x_4_0 8)
(= x_5_0 7)
(= x_0_6 0)
)
(&&
(= x_0_1 5)
(= x_1_1 2)
(= x_2_1 8)
(= x_3_1 7)
(= x_1_4 0)
)
(&&
(= x_1_0 0)
(= x_1_1 5)
(= x_2_1 2)
(= x_3_1 8)
(= x_4_1 7)
(= x_1_5 0)
)
(&&
(= x_1_1 0)
(= x_2_1 5)
(= x_3_1 2)
(= x_4_1 8)
(= x_5_1 7)
(= x_1_6 0)
)
(&&
(= x_0_2 5)
(= x_1_2 2)
(= x_2_2 8)
(= x_3_2 7)
(= x_2_4 0)
)
(&&
(= x_2_0 0)
(= x_1_2 5)
(= x_2_2 2)
(= x_3_2 8)
(= x_4_2 7)
(= x_2_5 0)
)
(&&
(= x_2_1 0)
(= x_2_2 5)
(= x_3_2 2)
(= x_4_2 8)
(= x_5_2 7)
(= x_2_6 0)
)
(&&
(= x_0_3 5)
(= x_1_3 2)
(= x_2_3 8)
(= x_3_3 7)
(= x_3_4 0)
)
(&&
(= x_3_0 0)
(= x_1_3 5)
(= x_2_3 2)
(= x_3_3 8)
(= x_4_3 7)
(= x_3_5 0)
)
(&&
(= x_3_1 0)
(= x_2_3 5)
(= x_3_3 2)
(= x_4_3 8)
(= x_5_3 7)
(= x_3_6 0)
)
(&&
(= x_0_4 5)
(= x_1_4 2)
(= x_2_4 8)
(= x_3_4 7)
(= x_4_4 0)
)
(&&
(= x_4_0 0)
(= x_1_4 5)
(= x_2_4 2)
(= x_3_4 8)
(= x_4_4 7)
(= x_4_5 0)
)
(&&
(= x_4_1 0)
(= x_2_4 5)
(= x_3_4 2)
(= x_4_4 8)
(= x_5_4 7)
(= x_4_6 0)
)
(&&
(= x_0_5 5)
(= x_1_5 2)
(= x_2_5 8)
(= x_3_5 7)
(= x_5_4 0)
)
(&&
(= x_5_0 0)
(= x_1_5 5)
(= x_2_5 2)
(= x_3_5 8)
(= x_4_5 7)
(= x_5_5 0)
)
(&&
(= x_5_1 0)
(= x_2_5 5)
(= x_3_5 2)
(= x_4_5 8)
(= x_5_5 7)
(= x_5_6 0)
)
(&&
(= x_0_6 5)
(= x_1_6 2)
(= x_2_6 8)
(= x_3_6 7)
(= x_6_4 0)
)
(&&
(= x_6_0 0)
(= x_1_6 5)
(= x_2_6 2)
(= x_3_6 8)
(= x_4_6 7)
(= x_6_5 0)
)
(&&
(= x_6_1 0)
(= x_2_6 5)
(= x_3_6 2)
(= x_4_6 8)
(= x_5_6 7)
(= x_6_6 0)
)
(&&
(= x_0_7 5)
(= x_1_7 2)
(= x_2_7 8)
(= x_3_7 7)
(= x_7_4 0)
)
(&&
(= x_7_0 0)
(= x_1_7 5)
(= x_2_7 2)
(= x_3_7 8)
(= x_4_7 7)
(= x_7_5 0)
)
(&&
(= x_7_1 0)
(= x_2_7 5)
(= x_3_7 2)
(= x_4_7 8)
(= x_5_7 7)
(= x_7_6 0)
)
)
(||
(&&
(= x_0_0 9)
(= x_0_1 7)
(= x_0_2 0)
)
(&&
(= x_0_0 0)
(= x_0_1 9)
(= x_0_2 7)
(= x_0_3 0)
)
(&&
(= x_0_1 0)
(= x_0_2 9)
(= x_0_3 7)
(= x_0_4 0)
)
(&&
(= x_0_2 0)
(= x_0_3 9)
(= x_0_4 7)
(= x_0_5 0)
)
(&&
(= x_0_3 0)
(= x_0_4 9)
(= x_0_5 7)
(= x_0_6 0)
)
(&&
(= x_0_4 0)
(= x_0_5 9)
(= x_0_6 7)
(= x_0_7 0)
)
(&&
(= x_0_5 0)
(= x_0_6 9)
(= x_0_7 7)
)
(&&
(= x_1_0 9)
(= x_1_1 7)
(= x_1_2 0)
)
(&&
(= x_1_0 0)
(= x_1_1 9)
(= x_1_2 7)
(= x_1_3 0)
)
(&&
(= x_1_1 0)
(= x_1_2 9)
(= x_1_3 7)
(= x_1_4 0)
)
(&&
(= x_1_2 0)
(= x_1_3 9)
(= x_1_4 7)
(= x_1_5 0)
)
(&&
(= x_1_3 0)
(= x_1_4 9)
(= x_1_5 7)
(= x_1_6 0)
)
(&&
(= x_1_4 0)
(= x_1_5 9)
(= x_1_6 7)
(= x_1_7 0)
)
(&&
(= x_1_5 0)
(= x_1_6 9)
(= x_1_7 7)
)
(&&
(= x_2_0 9)
(= x_2_1 7)
(= x_2_2 0)
)
(&&
(= x_2_0 0)
(= x_2_1 9)
(= x_2_2 7)
(= x_2_3 0)
)
(&&
(= x_2_1 0)
(= x_2_2 9)
(= x_2_3 7)
(= x_2_4 0)
)
(&&
(= x_2_2 0)
(= x_2_3 9)
(= x_2_4 7)
(= x_2_5 0)
)
(&&
(= x_2_3 0)
(= x_2_4 9)
(= x_2_5 7)
(= x_2_6 0)
)
(&&
(= x_2_4 0)
(= x_2_5 9)
(= x_2_6 7)
(= x_2_7 0)
)
(&&
(= x_2_5 0)
(= x_2_6 9)
(= x_2_7 7)
)
(&&
(= x_3_0 9)
(= x_3_1 7)
(= x_3_2 0)
)
(&&
(= x_3_0 0)
(= x_3_1 9)
(= x_3_2 7)
(= x_3_3 0)
)
(&&
(= x_3_1 0)
(= x_3_2 9)
(= x_3_3 7)
(= x_3_4 0)
)
(&&
(= x_3_2 0)
(= x_3_3 9)
(= x_3_4 7)
(= x_3_5 0)
)
(&&
(= x_3_3 0)
(= x_3_4 9)
(= x_3_5 7)
(= x_3_6 0)
)
(&&
(= x_3_4 0)
(= x_3_5 9)
(= x_3_6 7)
(= x_3_7 0)
)
(&&
(= x_3_5 0)
(= x_3_6 9)
(= x_3_7 7)
)
(&&
(= x_4_0 9)
(= x_4_1 7)
(= x_4_2 0)
)
(&&
(= x_4_0 0)
(= x_4_1 9)
(= x_4_2 7)
(= x_4_3 0)
)
(&&
(= x_4_1 0)
(= x_4_2 9)
(= x_4_3 7)
(= x_4_4 0)
)
(&&
(= x_4_2 0)
(= x_4_3 9)
(= x_4_4 7)
(= x_4_5 0)
)
(&&
(= x_4_3 0)
(= x_4_4 9)
(= x_4_5 7)
(= x_4_6 0)
)
(&&
(= x_4_4 0)
(= x_4_5 9)
(= x_4_6 7)
(= x_4_7 0)
)
(&&
(= x_4_5 0)
(= x_4_6 9)
(= x_4_7 7)
)
(&&
(= x_5_0 9)
(= x_5_1 7)
(= x_5_2 0)
)
(&&
(= x_5_0 0)
(= x_5_1 9)
(= x_5_2 7)
(= x_5_3 0)
)
(&&
(= x_5_1 0)
(= x_5_2 9)
(= x_5_3 7)
(= x_5_4 0)
)
(&&
(= x_5_2 0)
(= x_5_3 9)
(= x_5_4 7)
(= x_5_5 0)
)
(&&
(= x_5_3 0)
(= x_5_4 9)
(= x_5_5 7)
(= x_5_6 0)
)
(&&
(= x_5_4 0)
(= x_5_5 9)
(= x_5_6 7)
(= x_5_7 0)
)
(&&
(= x_5_5 0)
(= x_5_6 9)
(= x_5_7 7)
)
(&&
(= x_0_0 9)
(= x_1_0 7)
(= x_0_2 0)
)
(&&
(= x_0_0 0)
(= x_1_0 9)
(= x_2_0 7)
(= x_0_3 0)
)
(&&
(= x_0_1 0)
(= x_2_0 9)
(= x_3_0 7)
(= x_0_4 0)
)
(&&
(= x_0_2 0)
(= x_3_0 9)
(= x_4_0 7)
(= x_0_5 0)
)
(&&
(= x_0_3 0)
(= x_4_0 9)
(= x_5_0 7)
(= x_0_6 0)
)
(&&
(= x_0_1 9)
(= x_1_1 7)
(= x_1_2 0)
)
(&&
(= x_1_0 0)
(= x_1_1 9)
(= x_2_1 7)
(= x_1_3 0)
)
(&&
(= x_1_1 0)
(= x_2_1 9)
(= x_3_1 7)
(= x_1_4 0)
)
(&&
(= x_1_2 0)
(= x_3_1 9)
(= x_4_1 7)
(= x_1_5 0)
)
(&&
(= x_1_3 0)
(= x_4_1 9)
(= x_5_1 7)
(= x_1_6 0)
)
(&&
(= x_0_2 9)
(= x_1_2 7)
(= x_2_2 0)
)
(&&
(= x_2_0 0)
(= x_1_2 9)
(= x_2_2 7)
(= x_2_3 0)
)
(&&
(= x_2_1 0)
(= x_2_2 9)
(= x_3_2 7)
(= x_2_4 0)
)
(&&
(= x_2_2 0)
(= x_3_2 9)
(= x_4_2 7)
(= x_2_5 0)
)
(&&
(= x_2_3 0)
(= x_4_2 9)
(= x_5_2 7)
(= x_2_6 0)
)
(&&
(= x_0_3 9)
(= x_1_3 7)
(= x_3_2 0)
)
(&&
(= x_3_0 0)
(= x_1_3 9)
(= x_2_3 7)
(= x_3_3 0)
)
(&&
(= x_3_1 0)
(= x_2_3 9)
(= x_3_3 7)
(= x_3_4 0)
)
(&&
(= x_3_2 0)
(= x_3_3 9)
(= x_4_3 7)
(= x_3_5 0)
)
(&&
(= x_3_3 0)
(= x_4_3 9)
(= x_5_3 7)
(= x_3_6 0)
)
(&&
(= x_0_4 9)
(= x_1_4 7)
(= x_4_2 0)
)
(&&
(= x_4_0 0)
(= x_1_4 9)
(= x_2_4 7)
(= x_4_3 0)
)
(&&
(= x_4_1 0)
(= x_2_4 9)
(= x_3_4 7)
(= x_4_4 0)
)
(&&
(= x_4_2 0)
(= x_3_4 9)
(= x_4_4 7)
(= x_4_5 0)
)
(&&
(= x_4_3 0)
(= x_4_4 9)
(= x_5_4 7)
(= x_4_6 0)
)
(&&
(= x_0_5 9)
(= x_1_5 7)
(= x_5_2 0)
)
(&&
(= x_5_0 0)
(= x_1_5 9)
(= x_2_5 7)
(= x_5_3 0)
)
(&&
(= x_5_1 0)
(= x_2_5 9)
(= x_3_5 7)
(= x_5_4 0)
)
(&&
(= x_5_2 0)
(= x_3_5 9)
(= x_4_5 7)
(= x_5_5 0)
)
(&&
(= x_5_3 0)
(= x_4_5 9)
(= x_5_5 7)
(= x_5_6 0)
)
(&&
(= x_0_6 9)
(= x_1_6 7)
(= x_6_2 0)
)
(&&
(= x_6_0 0)
(= x_1_6 9)
(= x_2_6 7)
(= x_6_3 0)
)
(&&
(= x_6_1 0)
(= x_2_6 9)
(= x_3_6 7)
(= x_6_4 0)
)
(&&
(= x_6_2 0)
(= x_3_6 9)
(= x_4_6 7)
(= x_6_5 0)
)
(&&
(= x_6_3 0)
(= x_4_6 9)
(= x_5_6 7)
(= x_6_6 0)
)
(&&
(= x_0_7 9)
(= x_1_7 7)
(= x_7_2 0)
)
(&&
(= x_7_0 0)
(= x_1_7 9)
(= x_2_7 7)
(= x_7_3 0)
)
(&&
(= x_7_1 0)
(= x_2_7 9)
(= x_3_7 7)
(= x_7_4 0)
)
(&&
(= x_7_2 0)
(= x_3_7 9)
(= x_4_7 7)
(= x_7_5 0)
)
(&&
(= x_7_3 0)
(= x_4_7 9)
(= x_5_7 7)
(= x_7_6 0)
)
)
(||
(&&
(= x_0_0 6)
(= x_0_1 10)
(= x_0_2 5)
(= x_0_3 0)
)
(&&
(= x_0_0 0)
(= x_0_1 6)
(= x_0_2 10)
(= x_0_3 5)
(= x_0_4 0)
)
(&&
(= x_0_1 0)
(= x_0_2 6)
(= x_0_3 10)
(= x_0_4 5)
(= x_0_5 0)
)
(&&
(= x_0_2 0)
(= x_0_3 6)
(= x_0_4 10)
(= x_0_5 5)
(= x_0_6 0)
)
(&&
(= x_0_3 0)
(= x_0_4 6)
(= x_0_5 10)
(= x_0_6 5)
(= x_0_7 0)
)
(&&
(= x_0_4 0)
(= x_0_5 6)
(= x_0_6 10)
(= x_0_7 5)
)
(&&
(= x_1_0 6)
(= x_1_1 10)
(= x_1_2 5)
(= x_1_3 0)
)
(&&
(= x_1_0 0)
(= x_1_1 6)
(= x_1_2 10)
(= x_1_3 5)
(= x_1_4 0)
)
(&&
(= x_1_1 0)
(= x_1_2 6)
(= x_1_3 10)
(= x_1_4 5)
(= x_1_5 0)
)
(&&
(= x_1_2 0)
(= x_1_3 6)
(= x_1_4 10)
(= x_1_5 5)
(= x_1_6 0)
)
(&&
(= x_1_3 0)
(= x_1_4 6)
(= x_1_5 10)
(= x_1_6 5)
(= x_1_7 0)
)
(&&
(= x_1_4 0)
(= x_1_5 6)
(= x_1_6 10)
(= x_1_7 5)
)
(&&
(= x_2_0 6)
(= x_2_1 10)
(= x_2_2 5)
(= x_2_3 0)
)
(&&
(= x_2_0 0)
(= x_2_1 6)
(= x_2_2 10)
(= x_2_3 5)
(= x_2_4 0)
)
(&&
(= x_2_1 0)
(= x_2_2 6)
(= x_2_3 10)
(= x_2_4 5)
(= x_2_5 0)
)
(&&
(= x_2_2 0)
(= x_2_3 6)
(= x_2_4 10)
(= x_2_5 5)
(= x_2_6 0)
)
(&&
(= x_2_3 0)
(= x_2_4 6)
(= x_2_5 10)
(= x_2_6 5)
(= x_2_7 0)
)
(&&
(= x_2_4 0)
(= x_2_5 6)
(= x_2_6 10)
(= x_2_7 5)
)
(&&
(= x_3_0 6)
(= x_3_1 10)
(= x_3_2 5)
(= x_3_3 0)
)
(&&
(= x_3_0 0)
(= x_3_1 6)
(= x_3_2 10)
(= x_3_3 5)
(= x_3_4 0)
)
(&&
(= x_3_1 0)
(= x_3_2 6)
(= x_3_3 10)
(= x_3_4 5)
(= x_3_5 0)
)
(&&
(= x_3_2 0)
(= x_3_3 6)
(= x_3_4 10)
(= x_3_5 5)
(= x_3_6 0)
)
(&&
(= x_3_3 0)
(= x_3_4 6)
(= x_3_5 10)
(= x_3_6 5)
(= x_3_7 0)
)
(&&
(= x_3_4 0)
(= x_3_5 6)
(= x_3_6 10)
(= x_3_7 5)
)
(&&
(= x_4_0 6)
(= x_4_1 10)
(= x_4_2 5)
(= x_4_3 0)
)
(&&
(= x_4_0 0)
(= x_4_1 6)
(= x_4_2 10)
(= x_4_3 5)
(= x_4_4 0)
)
(&&
(= x_4_1 0)
(= x_4_2 6)
(= x_4_3 10)
(= x_4_4 5)
(= x_4_5 0)
)
(&&
(= x_4_2 0)
(= x_4_3 6)
(= x_4_4 10)
(= x_4_5 5)
(= x_4_6 0)
)
(&&
(= x_4_3 0)
(= x_4_4 6)
(= x_4_5 10)
(= x_4_6 5)
(= x_4_7 0)
)
(&&
(= x_4_4 0)
(= x_4_5 6)
(= x_4_6 10)
(= x_4_7 5)
)
(&&
(= x_5_0 6)
(= x_5_1 10)
(= x_5_2 5)
(= x_5_3 0)
)
(&&
(= x_5_0 0)
(= x_5_1 6)
(= x_5_2 10)
(= x_5_3 5)
(= x_5_4 0)
)
(&&
(= x_5_1 0)
(= x_5_2 6)
(= x_5_3 10)
(= x_5_4 5)
(= x_5_5 0)
)
(&&
(= x_5_2 0)
(= x_5_3 6)
(= x_5_4 10)
(= x_5_5 5)
(= x_5_6 0)
)
(&&
(= x_5_3 0)
(= x_5_4 6)
(= x_5_5 10)
(= x_5_6 5)
(= x_5_7 0)
)
(&&
(= x_5_4 0)
(= x_5_5 6)
(= x_5_6 10)
(= x_5_7 5)
)
(&&
(= x_0_0 6)
(= x_1_0 10)
(= x_2_0 5)
(= x_0_3 0)
)
(&&
(= x_0_0 0)
(= x_1_0 6)
(= x_2_0 10)
(= x_3_0 5)
(= x_0_4 0)
)
(&&
(= x_0_1 0)
(= x_2_0 6)
(= x_3_0 10)
(= x_4_0 5)
(= x_0_5 0)
)
(&&
(= x_0_2 0)
(= x_3_0 6)
(= x_4_0 10)
(= x_5_0 5)
(= x_0_6 0)
)
(&&
(= x_0_1 6)
(= x_1_1 10)
(= x_2_1 5)
(= x_1_3 0)
)
(&&
(= x_1_0 0)
(= x_1_1 6)
(= x_2_1 10)
(= x_3_1 5)
(= x_1_4 0)
)
(&&
(= x_1_1 0)
(= x_2_1 6)
(= x_3_1 10)
(= x_4_1 5)
(= x_1_5 0)
)
(&&
(= x_1_2 0)
(= x_3_1 6)
(= x_4_1 10)
(= x_5_1 5)
(= x_1_6 0)
)
(&&
(= x_0_2 6)
(= x_1_2 10)
(= x_2_2 5)
(= x_2_3 0)
)
(&&
(= x_2_0 0)
(= x_1_2 6)
(= x_2_2 10)
(= x_3_2 5)
(= x_2_4 0)
)
(&&
(= x_2_1 0)
(= x_2_2 6)
(= x_3_2 10)
(= x_4_2 5)
(= x_2_5 0)
)
(&&
(= x_2_2 0)
(= x_3_2 6)
(= x_4_2 10)
(= x_5_2 5)
(= x_2_6 0)
)
(&&
(= x_0_3 6)
(= x_1_3 10)
(= x_2_3 5)
(= x_3_3 0)
)
(&&
(= x_3_0 0)
(= x_1_3 6)
(= x_2_3 10)
(= x_3_3 5)
(= x_3_4 0)
)
(&&
(= x_3_1 0)
(= x_2_3 6)
(= x_3_3 10)
(= x_4_3 5)
(= x_3_5 0)
)
(&&
(= x_3_2 0)
(= x_3_3 6)
(= x_4_3 10)
(= x_5_3 5)
(= x_3_6 0)
)
(&&
(= x_0_4 6)
(= x_1_4 10)
(= x_2_4 5)
(= x_4_3 0)
)
(&&
(= x_4_0 0)
(= x_1_4 6)
(= x_2_4 10)
(= x_3_4 5)
(= x_4_4 0)
)
(&&
(= x_4_1 0)
(= x_2_4 6)
(= x_3_4 10)
(= x_4_4 5)
(= x_4_5 0)
)
(&&
(= x_4_2 0)
(= x_3_4 6)
(= x_4_4 10)
(= x_5_4 5)
(= x_4_6 0)
)
(&&
(= x_0_5 6)
(= x_1_5 10)
(= x_2_5 5)
(= x_5_3 0)
)
(&&
(= x_5_0 0)
(= x_1_5 6)
(= x_2_5 10)
(= x_3_5 5)
(= x_5_4 0)
)
(&&
(= x_5_1 0)
(= x_2_5 6)
(= x_3_5 10)
(= x_4_5 5)
(= x_5_5 0)
)
(&&
(= x_5_2 0)
(= x_3_5 6)
(= x_4_5 10)
(= x_5_5 5)
(= x_5_6 0)
)
(&&
(= x_0_6 6)
(= x_1_6 10)
(= x_2_6 5)
(= x_6_3 0)
)
(&&
(= x_6_0 0)
(= x_1_6 6)
(= x_2_6 10)
(= x_3_6 5)
(= x_6_4 0)
)
(&&
(= x_6_1 0)
(= x_2_6 6)
(= x_3_6 10)
(= x_4_6 5)
(= x_6_5 0)
)
(&&
(= x_6_2 0)
(= x_3_6 6)
(= x_4_6 10)
(= x_5_6 5)
(= x_6_6 0)
)
(&&
(= x_0_7 6)
(= x_1_7 10)
(= x_2_7 5)
(= x_7_3 0)
)
(&&
(= x_7_0 0)
(= x_1_7 6)
(= x_2_7 10)
(= x_3_7 5)
(= x_7_4 0)
)
(&&
(= x_7_1 0)
(= x_2_7 6)
(= x_3_7 10)
(= x_4_7 5)
(= x_7_5 0)
)
(&&
(= x_7_2 0)
(= x_3_7 6)
(= x_4_7 10)
(= x_5_7 5)
(= x_7_6 0)
)
)
(||
(&&
(= x_0_0 1)
(= x_0_1 2)
(= x_0_2 10)
(= x_0_3 0)
)
(&&
(= x_0_0 0)
(= x_0_1 1)
(= x_0_2 2)
(= x_0_3 10)
(= x_0_4 0)
)
(&&
(= x_0_1 0)
(= x_0_2 1)
(= x_0_3 2)
(= x_0_4 10)
(= x_0_5 0)
)
(&&
(= x_0_2 0)
(= x_0_3 1)
(= x_0_4 2)
(= x_0_5 10)
(= x_0_6 0)
)
(&&
(= x_0_3 0)
(= x_0_4 1)
(= x_0_5 2)
(= x_0_6 10)
(= x_0_7 0)
)
(&&
(= x_0_4 0)
(= x_0_5 1)
(= x_0_6 2)
(= x_0_7 10)
)
(&&
(= x_1_0 1)
(= x_1_1 2)
(= x_1_2 10)
(= x_1_3 0)
)
(&&
(= x_1_0 0)
(= x_1_1 1)
(= x_1_2 2)
(= x_1_3 10)
(= x_1_4 0)
)
(&&
(= x_1_1 0)
(= x_1_2 1)
(= x_1_3 2)
(= x_1_4 10)
(= x_1_5 0)
)
(&&
(= x_1_2 0)
(= x_1_3 1)
(= x_1_4 2)
(= x_1_5 10)
(= x_1_6 0)
)
(&&
(= x_1_3 0)
(= x_1_4 1)
(= x_1_5 2)
(= x_1_6 10)
(= x_1_7 0)
)
(&&
(= x_1_4 0)
(= x_1_5 1)
(= x_1_6 2)
(= x_1_7 10)
)
(&&
(= x_2_0 1)
(= x_2_1 2)
(= x_2_2 10)
(= x_2_3 0)
)
(&&
(= x_2_0 0)
(= x_2_1 1)
(= x_2_2 2)
(= x_2_3 10)
(= x_2_4 0)
)
(&&
(= x_2_1 0)
(= x_2_2 1)
(= x_2_3 2)
(= x_2_4 10)
(= x_2_5 0)
)
(&&
(= x_2_2 0)
(= x_2_3 1)
(= x_2_4 2)
(= x_2_5 10)
(= x_2_6 0)
)
(&&
(= x_2_3 0)
(= x_2_4 1)
(= x_2_5 2)
(= x_2_6 10)
(= x_2_7 0)
)
(&&
(= x_2_4 0)
(= x_2_5 1)
(= x_2_6 2)
(= x_2_7 10)
)
(&&
(= x_3_0 1)
(= x_3_1 2)
(= x_3_2 10)
(= x_3_3 0)
)
(&&
(= x_3_0 0)
(= x_3_1 1)
(= x_3_2 2)
(= x_3_3 10)
(= x_3_4 0)
)
(&&
(= x_3_1 0)
(= x_3_2 1)
(= x_3_3 2)
(= x_3_4 10)
(= x_3_5 0)
)
(&&
(= x_3_2 0)
(= x_3_3 1)
(= x_3_4 2)
(= x_3_5 10)
(= x_3_6 0)
)
(&&
(= x_3_3 0)
(= x_3_4 1)
(= x_3_5 2)
(= x_3_6 10)
(= x_3_7 0)
)
(&&
(= x_3_4 0)
(= x_3_5 1)
(= x_3_6 2)
(= x_3_7 10)
)
(&&
(= x_4_0 1)
(= x_4_1 2)
(= x_4_2 10)
(= x_4_3 0)
)
(&&
(= x_4_0 0)
(= x_4_1 1)
(= x_4_2 2)
(= x_4_3 10)
(= x_4_4 0)
)
(&&
(= x_4_1 0)
(= x_4_2 1)
(= x_4_3 2)
(= x_4_4 10)
(= x_4_5 0)
)
(&&
(= x_4_2 0)
(= x_4_3 1)
(= x_4_4 2)
(= x_4_5 10)
(= x_4_6 0)
)
(&&
(= x_4_3 0)
(= x_4_4 1)
(= x_4_5 2)
(= x_4_6 10)
(= x_4_7 0)
)
(&&
(= x_4_4 0)
(= x_4_5 1)
(= x_4_6 2)
(= x_4_7 10)
)
(&&
(= x_5_0 1)
(= x_5_1 2)
(= x_5_2 10)
(= x_5_3 0)
)
(&&
(= x_5_0 0)
(= x_5_1 1)
(= x_5_2 2)
(= x_5_3 10)
(= x_5_4 0)
)
(&&
(= x_5_1 0)
(= x_5_2 1)
(= x_5_3 2)
(= x_5_4 10)
(= x_5_5 0)
)
(&&
(= x_5_2 0)
(= x_5_3 1)
(= x_5_4 2)
(= x_5_5 10)
(= x_5_6 0)
)
(&&
(= x_5_3 0)
(= x_5_4 1)
(= x_5_5 2)
(= x_5_6 10)
(= x_5_7 0)
)
(&&
(= x_5_4 0)
(= x_5_5 1)
(= x_5_6 2)
(= x_5_7 10)
)
(&&
(= x_0_0 1)
(= x_1_0 2)
(= x_2_0 10)
(= x_0_3 0)
)
(&&
(= x_0_0 0)
(= x_1_0 1)
(= x_2_0 2)
(= x_3_0 10)
(= x_0_4 0)
)
(&&
(= x_0_1 0)
(= x_2_0 1)
(= x_3_0 2)
(= x_4_0 10)
(= x_0_5 0)
)
(&&
(= x_0_2 0)
(= x_3_0 1)
(= x_4_0 2)
(= x_5_0 10)
(= x_0_6 0)
)
(&&
(= x_0_1 1)
(= x_1_1 2)
(= x_2_1 10)
(= x_1_3 0)
)
(&&
(= x_1_0 0)
(= x_1_1 1)
(= x_2_1 2)
(= x_3_1 10)
(= x_1_4 0)
)
(&&
(= x_1_1 0)
(= x_2_1 1)
(= x_3_1 2)
(= x_4_1 10)
(= x_1_5 0)
)
(&&
(= x_1_2 0)
(= x_3_1 1)
(= x_4_1 2)
(= x_5_1 10)
(= x_1_6 0)
)
(&&
(= x_0_2 1)
(= x_1_2 2)
(= x_2_2 10)
(= x_2_3 0)
)
(&&
(= x_2_0 0)
(= x_1_2 1)
(= x_2_2 2)
(= x_3_2 10)
(= x_2_4 0)
)
(&&
(= x_2_1 0)
(= x_2_2 1)
(= x_3_2 2)
(= x_4_2 10)
(= x_2_5 0)
)
(&&
(= x_2_2 0)
(= x_3_2 1)
(= x_4_2 2)
(= x_5_2 10)
(= x_2_6 0)
)
(&&
(= x_0_3 1)
(= x_1_3 2)
(= x_2_3 10)
(= x_3_3 0)
)
(&&
(= x_3_0 0)
(= x_1_3 1)
(= x_2_3 2)
(= x_3_3 10)
(= x_3_4 0)
)
(&&
(= x_3_1 0)
(= x_2_3 1)
(= x_3_3 2)
(= x_4_3 10)
(= x_3_5 0)
)
(&&
(= x_3_2 0)
(= x_3_3 1)
(= x_4_3 2)
(= x_5_3 10)
(= x_3_6 0)
)
(&&
(= x_0_4 1)
(= x_1_4 2)
(= x_2_4 10)
(= x_4_3 0)
)
(&&
(= x_4_0 0)
(= x_1_4 1)
(= x_2_4 2)
(= x_3_4 10)
(= x_4_4 0)
)
(&&
(= x_4_1 0)
(= x_2_4 1)
(= x_3_4 2)
(= x_4_4 10)
(= x_4_5 0)
)
(&&
(= x_4_2 0)
(= x_3_4 1)
(= x_4_4 2)
(= x_5_4 10)
(= x_4_6 0)
)
(&&
(= x_0_5 1)
(= x_1_5 2)
(= x_2_5 10)
(= x_5_3 0)
)
(&&
(= x_5_0 0)
(= x_1_5 1)
(= x_2_5 2)
(= x_3_5 10)
(= x_5_4 0)
)
(&&
(= x_5_1 0)
(= x_2_5 1)
(= x_3_5 2)
(= x_4_5 10)
(= x_5_5 0)
)
(&&
(= x_5_2 0)
(= x_3_5 1)
(= x_4_5 2)
(= x_5_5 10)
(= x_5_6 0)
)
(&&
(= x_0_6 1)
(= x_1_6 2)
(= x_2_6 10)
(= x_6_3 0)
)
(&&
(= x_6_0 0)
(= x_1_6 1)
(= x_2_6 2)
(= x_3_6 10)
(= x_6_4 0)
)
(&&
(= x_6_1 0)
(= x_2_6 1)
(= x_3_6 2)
(= x_4_6 10)
(= x_6_5 0)
)
(&&
(= x_6_2 0)
(= x_3_6 1)
(= x_4_6 2)
(= x_5_6 10)
(= x_6_6 0)
)
(&&
(= x_0_7 1)
(= x_1_7 2)
(= x_2_7 10)
(= x_7_3 0)
)
(&&
(= x_7_0 0)
(= x_1_7 1)
(= x_2_7 2)
(= x_3_7 10)
(= x_7_4 0)
)
(&&
(= x_7_1 0)
(= x_2_7 1)
(= x_3_7 2)
(= x_4_7 10)
(= x_7_5 0)
)
(&&
(= x_7_2 0)
(= x_3_7 1)
(= x_4_7 2)
(= x_5_7 10)
(= x_7_6 0)
)
)
(||
(&&
(= x_0_0 11)
(= x_0_1 12)
(= x_0_2 1)
(= x_0_3 0)
)
(&&
(= x_0_0 0)
(= x_0_1 11)
(= x_0_2 12)
(= x_0_3 1)
(= x_0_4 0)
)
(&&
(= x_0_1 0)
(= x_0_2 11)
(= x_0_3 12)
(= x_0_4 1)
(= x_0_5 0)
)
(&&
(= x_0_2 0)
(= x_0_3 11)
(= x_0_4 12)
(= x_0_5 1)
(= x_0_6 0)
)
(&&
(= x_0_3 0)
(= x_0_4 11)
(= x_0_5 12)
(= x_0_6 1)
(= x_0_7 0)
)
(&&
(= x_0_4 0)
(= x_0_5 11)
(= x_0_6 12)
(= x_0_7 1)
)
(&&
(= x_1_0 11)
(= x_1_1 12)
(= x_1_2 1)
(= x_1_3 0)
)
(&&
(= x_1_0 0)
(= x_1_1 11)
(= x_1_2 12)
(= x_1_3 1)
(= x_1_4 0)
)
(&&
(= x_1_1 0)
(= x_1_2 11)
(= x_1_3 12)
(= x_1_4 1)
(= x_1_5 0)
)
(&&
(= x_1_2 0)
(= x_1_3 11)
(= x_1_4 12)
(= x_1_5 1)
(= x_1_6 0)
)
(&&
(= x_1_3 0)
(= x_1_4 11)
(= x_1_5 12)
(= x_1_6 1)
(= x_1_7 0)
)
(&&
(= x_1_4 0)
(= x_1_5 11)
(= x_1_6 12)
(= x_1_7 1)
)
(&&
(= x_2_0 11)
(= x_2_1 12)
(= x_2_2 1)
(= x_2_3 0)
)
(&&
(= x_2_0 0)
(= x_2_1 11)
(= x_2_2 12)
(= x_2_3 1)
(= x_2_4 0)
)
(&&
(= x_2_1 0)
(= x_2_2 11)
(= x_2_3 12)
(= x_2_4 1)
(= x_2_5 0)
)
(&&
(= x_2_2 0)
(= x_2_3 11)
(= x_2_4 12)
(= x_2_5 1)
(= x_2_6 0)
)
(&&
(= x_2_3 0)
(= x_2_4 11)
(= x_2_5 12)
(= x_2_6 1)
(= x_2_7 0)
)
(&&
(= x_2_4 0)
(= x_2_5 11)
(= x_2_6 12)
(= x_2_7 1)
)
(&&
(= x_3_0 11)
(= x_3_1 12)
(= x_3_2 1)
(= x_3_3 0)
)
(&&
(= x_3_0 0)
(= x_3_1 11)
(= x_3_2 12)
(= x_3_3 1)
(= x_3_4 0)
)
(&&
(= x_3_1 0)
(= x_3_2 11)
(= x_3_3 12)
(= x_3_4 1)
(= x_3_5 0)
)
(&&
(= x_3_2 0)
(= x_3_3 11)
(= x_3_4 12)
(= x_3_5 1)
(= x_3_6 0)
)
(&&
(= x_3_3 0)
(= x_3_4 11)
(= x_3_5 12)
(= x_3_6 1)
(= x_3_7 0)
)
(&&
(= x_3_4 0)
(= x_3_5 11)
(= x_3_6 12)
(= x_3_7 1)
)
(&&
(= x_4_0 11)
(= x_4_1 12)
(= x_4_2 1)
(= x_4_3 0)
)
(&&
(= x_4_0 0)
(= x_4_1 11)
(= x_4_2 12)
(= x_4_3 1)
(= x_4_4 0)
)
(&&
(= x_4_1 0)
(= x_4_2 11)
(= x_4_3 12)
(= x_4_4 1)
(= x_4_5 0)
)
(&&
(= x_4_2 0)
(= x_4_3 11)
(= x_4_4 12)
(= x_4_5 1)
(= x_4_6 0)
)
(&&
(= x_4_3 0)
(= x_4_4 11)
(= x_4_5 12)
(= x_4_6 1)
(= x_4_7 0)
)
(&&
(= x_4_4 0)
(= x_4_5 11)
(= x_4_6 12)
(= x_4_7 1)
)
(&&
(= x_5_0 11)
(= x_5_1 12)
(= x_5_2 1)
(= x_5_3 0)
)
(&&
(= x_5_0 0)
(= x_5_1 11)
(= x_5_2 12)
(= x_5_3 1)
(= x_5_4 0)
)
(&&
(= x_5_1 0)
(= x_5_2 11)
(= x_5_3 12)
(= x_5_4 1)
(= x_5_5 0)
)
(&&
(= x_5_2 0)
(= x_5_3 11)
(= x_5_4 12)
(= x_5_5 1)
(= x_5_6 0)
)
(&&
(= x_5_3 0)
(= x_5_4 11)
(= x_5_5 12)
(= x_5_6 1)
(= x_5_7 0)
)
(&&
(= x_5_4 0)
(= x_5_5 11)
(= x_5_6 12)
(= x_5_7 1)
)
(&&
(= x_0_0 11)
(= x_1_0 12)
(= x_2_0 1)
(= x_0_3 0)
)
(&&
(= x_0_0 0)
(= x_1_0 11)
(= x_2_0 12)
(= x_3_0 1)
(= x_0_4 0)
)
(&&
(= x_0_1 0)
(= x_2_0 11)
(= x_3_0 12)
(= x_4_0 1)
(= x_0_5 0)
)
(&&
(= x_0_2 0)
(= x_3_0 11)
(= x_4_0 12)
(= x_5_0 1)
(= x_0_6 0)
)
(&&
(= x_0_1 11)
(= x_1_1 12)
(= x_2_1 1)
(= x_1_3 0)
)
(&&
(= x_1_0 0)
(= x_1_1 11)
(= x_2_1 12)
(= x_3_1 1)
(= x_1_4 0)
)
(&&
(= x_1_1 0)
(= x_2_1 11)
(= x_3_1 12)
(= x_4_1 1)
(= x_1_5 0)
)
(&&
(= x_1_2 0)
(= x_3_1 11)
(= x_4_1 12)
(= x_5_1 1)
(= x_1_6 0)
)
(&&
(= x_0_2 11)
(= x_1_2 12)
(= x_2_2 1)
(= x_2_3 0)
)
(&&
(= x_2_0 0)
(= x_1_2 11)
(= x_2_2 12)
(= x_3_2 1)
(= x_2_4 0)
)
(&&
(= x_2_1 0)
(= x_2_2 11)
(= x_3_2 12)
(= x_4_2 1)
(= x_2_5 0)
)
(&&
(= x_2_2 0)
(= x_3_2 11)
(= x_4_2 12)
(= x_5_2 1)
(= x_2_6 0)
)
(&&
(= x_0_3 11)
(= x_1_3 12)
(= x_2_3 1)
(= x_3_3 0)
)
(&&
(= x_3_0 0)
(= x_1_3 11)
(= x_2_3 12)
(= x_3_3 1)
(= x_3_4 0)
)
(&&
(= x_3_1 0)
(= x_2_3 11)
(= x_3_3 12)
(= x_4_3 1)
(= x_3_5 0)
)
(&&
(= x_3_2 0)
(= x_3_3 11)
(= x_4_3 12)
(= x_5_3 1)
(= x_3_6 0)
)
(&&
(= x_0_4 11)
(= x_1_4 12)
(= x_2_4 1)
(= x_4_3 0)
)
(&&
(= x_4_0 0)
(= x_1_4 11)
(= x_2_4 12)
(= x_3_4 1)
(= x_4_4 0)
)
(&&
(= x_4_1 0)
(= x_2_4 11)
(= x_3_4 12)
(= x_4_4 1)
(= x_4_5 0)
)
(&&
(= x_4_2 0)
(= x_3_4 11)
(= x_4_4 12)
(= x_5_4 1)
(= x_4_6 0)
)
(&&
(= x_0_5 11)
(= x_1_5 12)
(= x_2_5 1)
(= x_5_3 0)
)
(&&
(= x_5_0 0)
(= x_1_5 11)
(= x_2_5 12)
(= x_3_5 1)
(= x_5_4 0)
)
(&&
(= x_5_1 0)
(= x_2_5 11)
(= x_3_5 12)
(= x_4_5 1)
(= x_5_5 0)
)
(&&
(= x_5_2 0)
(= x_3_5 11)
(= x_4_5 12)
(= x_5_5 1)
(= x_5_6 0)
)
(&&
(= x_0_6 11)
(= x_1_6 12)
(= x_2_6 1)
(= x_6_3 0)
)
(&&
(= x_6_0 0)
(= x_1_6 11)
(= x_2_6 12)
(= x_3_6 1)
(= x_6_4 0)
)
(&&
(= x_6_1 0)
(= x_2_6 11)
(= x_3_6 12)
(= x_4_6 1)
(= x_6_5 0)
)
(&&
(= x_6_2 0)
(= x_3_6 11)
(= x_4_6 12)
(= x_5_6 1)
(= x_6_6 0)
)
(&&
(= x_0_7 11)
(= x_1_7 12)
(= x_2_7 1)
(= x_7_3 0)
)
(&&
(= x_7_0 0)
(= x_1_7 11)
(= x_2_7 12)
(= x_3_7 1)
(= x_7_4 0)
)
(&&
(= x_7_1 0)
(= x_2_7 11)
(= x_3_7 12)
(= x_4_7 1)
(= x_7_5 0)
)
(&&
(= x_7_2 0)
(= x_3_7 11)
(= x_4_7 12)
(= x_5_7 1)
(= x_7_6 0)
)
)



(= 18 (+
  (if ( > x_0_0 0 ) 1 0)
  (if ( > x_0_1 0 ) 1 0)
  (if ( > x_0_2 0 ) 1 0)
  (if ( > x_0_3 0 ) 1 0)
  (if ( > x_0_4 0 ) 1 0)
  (if ( > x_0_5 0 ) 1 0)
  (if ( > x_0_6 0 ) 1 0)
  (if ( > x_0_7 0 ) 1 0)
  (if ( > x_1_0 0 ) 1 0)
  (if ( > x_1_1 0 ) 1 0)
  (if ( > x_1_2 0 ) 1 0)
  (if ( > x_1_3 0 ) 1 0)
  (if ( > x_1_4 0 ) 1 0)
  (if ( > x_1_5 0 ) 1 0)
  (if ( > x_1_6 0 ) 1 0)
  (if ( > x_1_7 0 ) 1 0)
  (if ( > x_2_0 0 ) 1 0)
  (if ( > x_2_1 0 ) 1 0)
  (if ( > x_2_2 0 ) 1 0)
  (if ( > x_2_3 0 ) 1 0)
  (if ( > x_2_4 0 ) 1 0)
  (if ( > x_2_5 0 ) 1 0)
  (if ( > x_2_6 0 ) 1 0)
  (if ( > x_2_7 0 ) 1 0)
  (if ( > x_3_0 0 ) 1 0)
  (if ( > x_3_1 0 ) 1 0)
  (if ( > x_3_2 0 ) 1 0)
  (if ( > x_3_3 0 ) 1 0)
  (if ( > x_3_4 0 ) 1 0)
  (if ( > x_3_5 0 ) 1 0)
  (if ( > x_3_6 0 ) 1 0)
  (if ( > x_3_7 0 ) 1 0)
  (if ( > x_4_0 0 ) 1 0)
  (if ( > x_4_1 0 ) 1 0)
  (if ( > x_4_2 0 ) 1 0)
  (if ( > x_4_3 0 ) 1 0)
  (if ( > x_4_4 0 ) 1 0)
  (if ( > x_4_5 0 ) 1 0)
  (if ( > x_4_6 0 ) 1 0)
  (if ( > x_4_7 0 ) 1 0)
  (if ( > x_5_0 0 ) 1 0)
  (if ( > x_5_1 0 ) 1 0)
  (if ( > x_5_2 0 ) 1 0)
  (if ( > x_5_3 0 ) 1 0)
  (if ( > x_5_4 0 ) 1 0)
  (if ( > x_5_5 0 ) 1 0)
  (if ( > x_5_6 0 ) 1 0)
  (if ( > x_5_7 0 ) 1 0)
) )
(> 4 (+
 (if ( > x_0_0 0 ) 1 0)
 (if ( > x_1_0 0 ) 1 0)
 (if ( > x_0_1 0 ) 1 0)
 (if ( > x_1_1 0 ) 1 0)
))
(> 4 (+
 (if ( > x_0_1 0 ) 1 0)
 (if ( > x_1_1 0 ) 1 0)
 (if ( > x_0_2 0 ) 1 0)
 (if ( > x_1_2 0 ) 1 0)
))
(> 4 (+
 (if ( > x_0_2 0 ) 1 0)
 (if ( > x_1_2 0 ) 1 0)
 (if ( > x_0_3 0 ) 1 0)
 (if ( > x_1_3 0 ) 1 0)
))
(> 4 (+
 (if ( > x_0_3 0 ) 1 0)
 (if ( > x_1_3 0 ) 1 0)
 (if ( > x_0_4 0 ) 1 0)
 (if ( > x_1_4 0 ) 1 0)
))
(> 4 (+
 (if ( > x_0_4 0 ) 1 0)
 (if ( > x_1_4 0 ) 1 0)
 (if ( > x_0_5 0 ) 1 0)
 (if ( > x_1_5 0 ) 1 0)
))
(> 4 (+
 (if ( > x_0_5 0 ) 1 0)
 (if ( > x_1_5 0 ) 1 0)
 (if ( > x_0_6 0 ) 1 0)
 (if ( > x_1_6 0 ) 1 0)
))
(> 4 (+
 (if ( > x_0_6 0 ) 1 0)
 (if ( > x_1_6 0 ) 1 0)
 (if ( > x_0_7 0 ) 1 0)
 (if ( > x_1_7 0 ) 1 0)
))
(> 4 (+
 (if ( > x_1_0 0 ) 1 0)
 (if ( > x_2_0 0 ) 1 0)
 (if ( > x_1_1 0 ) 1 0)
 (if ( > x_2_1 0 ) 1 0)
))
(> 4 (+
 (if ( > x_1_1 0 ) 1 0)
 (if ( > x_2_1 0 ) 1 0)
 (if ( > x_1_2 0 ) 1 0)
 (if ( > x_2_2 0 ) 1 0)
))
(> 4 (+
 (if ( > x_1_2 0 ) 1 0)
 (if ( > x_2_2 0 ) 1 0)
 (if ( > x_1_3 0 ) 1 0)
 (if ( > x_2_3 0 ) 1 0)
))
(> 4 (+
 (if ( > x_1_3 0 ) 1 0)
 (if ( > x_2_3 0 ) 1 0)
 (if ( > x_1_4 0 ) 1 0)
 (if ( > x_2_4 0 ) 1 0)
))
(> 4 (+
 (if ( > x_1_4 0 ) 1 0)
 (if ( > x_2_4 0 ) 1 0)
 (if ( > x_1_5 0 ) 1 0)
 (if ( > x_2_5 0 ) 1 0)
))
(> 4 (+
 (if ( > x_1_5 0 ) 1 0)
 (if ( > x_2_5 0 ) 1 0)
 (if ( > x_1_6 0 ) 1 0)
 (if ( > x_2_6 0 ) 1 0)
))
(> 4 (+
 (if ( > x_1_6 0 ) 1 0)
 (if ( > x_2_6 0 ) 1 0)
 (if ( > x_1_7 0 ) 1 0)
 (if ( > x_2_7 0 ) 1 0)
))
(> 4 (+
 (if ( > x_2_0 0 ) 1 0)
 (if ( > x_3_0 0 ) 1 0)
 (if ( > x_2_1 0 ) 1 0)
 (if ( > x_3_1 0 ) 1 0)
))
(> 4 (+
 (if ( > x_2_1 0 ) 1 0)
 (if ( > x_3_1 0 ) 1 0)
 (if ( > x_2_2 0 ) 1 0)
 (if ( > x_3_2 0 ) 1 0)
))
(> 4 (+
 (if ( > x_2_2 0 ) 1 0)
 (if ( > x_3_2 0 ) 1 0)
 (if ( > x_2_3 0 ) 1 0)
 (if ( > x_3_3 0 ) 1 0)
))
(> 4 (+
 (if ( > x_2_3 0 ) 1 0)
 (if ( > x_3_3 0 ) 1 0)
 (if ( > x_2_4 0 ) 1 0)
 (if ( > x_3_4 0 ) 1 0)
))
(> 4 (+
 (if ( > x_2_4 0 ) 1 0)
 (if ( > x_3_4 0 ) 1 0)
 (if ( > x_2_5 0 ) 1 0)
 (if ( > x_3_5 0 ) 1 0)
))
(> 4 (+
 (if ( > x_2_5 0 ) 1 0)
 (if ( > x_3_5 0 ) 1 0)
 (if ( > x_2_6 0 ) 1 0)
 (if ( > x_3_6 0 ) 1 0)
))
(> 4 (+
 (if ( > x_2_6 0 ) 1 0)
 (if ( > x_3_6 0 ) 1 0)
 (if ( > x_2_7 0 ) 1 0)
 (if ( > x_3_7 0 ) 1 0)
))
(> 4 (+
 (if ( > x_3_0 0 ) 1 0)
 (if ( > x_4_0 0 ) 1 0)
 (if ( > x_3_1 0 ) 1 0)
 (if ( > x_4_1 0 ) 1 0)
))
(> 4 (+
 (if ( > x_3_1 0 ) 1 0)
 (if ( > x_4_1 0 ) 1 0)
 (if ( > x_3_2 0 ) 1 0)
 (if ( > x_4_2 0 ) 1 0)
))
(> 4 (+
 (if ( > x_3_2 0 ) 1 0)
 (if ( > x_4_2 0 ) 1 0)
 (if ( > x_3_3 0 ) 1 0)
 (if ( > x_4_3 0 ) 1 0)
))
(> 4 (+
 (if ( > x_3_3 0 ) 1 0)
 (if ( > x_4_3 0 ) 1 0)
 (if ( > x_3_4 0 ) 1 0)
 (if ( > x_4_4 0 ) 1 0)
))
(> 4 (+
 (if ( > x_3_4 0 ) 1 0)
 (if ( > x_4_4 0 ) 1 0)
 (if ( > x_3_5 0 ) 1 0)
 (if ( > x_4_5 0 ) 1 0)
))
(> 4 (+
 (if ( > x_3_5 0 ) 1 0)
 (if ( > x_4_5 0 ) 1 0)
 (if ( > x_3_6 0 ) 1 0)
 (if ( > x_4_6 0 ) 1 0)
))
(> 4 (+
 (if ( > x_3_6 0 ) 1 0)
 (if ( > x_4_6 0 ) 1 0)
 (if ( > x_3_7 0 ) 1 0)
 (if ( > x_4_7 0 ) 1 0)
))
(> 4 (+
 (if ( > x_4_0 0 ) 1 0)
 (if ( > x_5_0 0 ) 1 0)
 (if ( > x_4_1 0 ) 1 0)
 (if ( > x_5_1 0 ) 1 0)
))
(> 4 (+
 (if ( > x_4_1 0 ) 1 0)
 (if ( > x_5_1 0 ) 1 0)
 (if ( > x_4_2 0 ) 1 0)
 (if ( > x_5_2 0 ) 1 0)
))
(> 4 (+
 (if ( > x_4_2 0 ) 1 0)
 (if ( > x_5_2 0 ) 1 0)
 (if ( > x_4_3 0 ) 1 0)
 (if ( > x_5_3 0 ) 1 0)
))
(> 4 (+
 (if ( > x_4_3 0 ) 1 0)
 (if ( > x_5_3 0 ) 1 0)
 (if ( > x_4_4 0 ) 1 0)
 (if ( > x_5_4 0 ) 1 0)
))
(> 4 (+
 (if ( > x_4_4 0 ) 1 0)
 (if ( > x_5_4 0 ) 1 0)
 (if ( > x_4_5 0 ) 1 0)
 (if ( > x_5_5 0 ) 1 0)
))
(> 4 (+
 (if ( > x_4_5 0 ) 1 0)
 (if ( > x_5_5 0 ) 1 0)
 (if ( > x_4_6 0 ) 1 0)
 (if ( > x_5_6 0 ) 1 0)
))
(> 4 (+
 (if ( > x_4_6 0 ) 1 0)
 (if ( > x_5_6 0 ) 1 0)
 (if ( > x_4_7 0 ) 1 0)
 (if ( > x_5_7 0 ) 1 0)
))