x1 = A
x2 = C9
x3 = C9X
x4 = X
x5 = AC9X
x6 = AC9
x7 = C3
x8 = C3_star
x9 = C3_starX
x10 = C9_starX
x11 = C9_star
x12 = AC9_star
x13 = AC9_starX
x14 = C9X_C3_star
x15 = AC9X_C3_star
x16 = C9_starX_C3_star
x17 = AC9_starX_C3_star