ws1s; ex2 X: all2 X1, X2, X3, X4, X5, X6, X7, X8, X9, X10:( (X1 sub X2 & X2 sub X3) => X1 sub X3) & ( (X1 sub X2 & X2 sub X4) => X1 sub X4) & ( (X1 sub X2 & X2 sub X5) => X1 sub X5) & ( (X1 sub X2 & X2 sub X6) => X1 sub X6) & ( (X1 sub X2 & X2 sub X7) => X1 sub X7) & ( (X1 sub X2 & X2 sub X8) => X1 sub X8) & ( (X1 sub X2 & X2 sub X9) => X1 sub X9) & ( (X1 sub X2 & X2 sub X10) => X1 sub X10) & ( (X1 sub X3 & X3 sub X2) => X1 sub X2) & ( (X1 sub X3 & X3 sub X4) => X1 sub X4) & ( (X1 sub X3 & X3 sub X5) => X1 sub X5) & ( (X1 sub X3 & X3 sub X6) => X1 sub X6) & ( (X1 sub X3 & X3 sub X7) => X1 sub X7) & ( (X1 sub X3 & X3 sub X8) => X1 sub X8) & ( (X1 sub X3 & X3 sub X9) => X1 sub X9) & ( (X1 sub X3 & X3 sub X10) => X1 sub X10) & ( (X1 sub X4 & X4 sub X2) => X1 sub X2) & ( (X1 sub X4 & X4 sub X3) => X1 sub X3) & ( (X1 sub X4 & X4 sub X5) => X1 sub X5) & ( (X1 sub X4 & X4 sub X6) => X1 sub X6) & ( (X1 sub X4 & X4 sub X7) => X1 sub X7) & ( (X1 sub X4 & X4 sub X8) => X1 sub X8) & ( (X1 sub X4 & X4 sub X9) => X1 sub X9) & ( (X1 sub X4 & X4 sub X10) => X1 sub X10) & ( (X1 sub X5 & X5 sub X2) => X1 sub X2) & ( (X1 sub X5 & X5 sub X3) => X1 sub X3) & ( (X1 sub X5 & X5 sub X4) => X1 sub X4) & ( (X1 sub X5 & X5 sub X6) => X1 sub X6) & ( (X1 sub X5 & X5 sub X7) => X1 sub X7) & ( (X1 sub X5 & X5 sub X8) => X1 sub X8) & ( (X1 sub X5 & X5 sub X9) => X1 sub X9) & ( (X1 sub X5 & X5 sub X10) => X1 sub X10) & ( (X1 sub X6 & X6 sub X2) => X1 sub X2) & ( (X1 sub X6 & X6 sub X3) => X1 sub X3) & ( (X1 sub X6 & X6 sub X4) => X1 sub X4) & ( (X1 sub X6 & X6 sub X5) => X1 sub X5) & ( (X1 sub X6 & X6 sub X7) => X1 sub X7) & ( (X1 sub X6 & X6 sub X8) => X1 sub X8) & ( (X1 sub X6 & X6 sub X9) => X1 sub X9) & ( (X1 sub X6 & X6 sub X10) => X1 sub X10) & ( (X1 sub X7 & X7 sub X2) => X1 sub X2) & ( (X1 sub X7 & X7 sub X3) => X1 sub X3) & ( (X1 sub X7 & X7 sub X4) => X1 sub X4) & ( (X1 sub X7 & X7 sub X5) => X1 sub X5) & ( (X1 sub X7 & X7 sub X6) => X1 sub X6) & ( (X1 sub X7 & X7 sub X8) => X1 sub X8) & ( (X1 sub X7 & X7 sub X9) => X1 sub X9) & ( (X1 sub X7 & X7 sub X10) => X1 sub X10) & ( (X1 sub X8 & X8 sub X2) => X1 sub X2) & ( (X1 sub X8 & X8 sub X3) => X1 sub X3) & ( (X1 sub X8 & X8 sub X4) => X1 sub X4) & ( (X1 sub X8 & X8 sub X5) => X1 sub X5) & ( (X1 sub X8 & X8 sub X6) => X1 sub X6) & ( (X1 sub X8 & X8 sub X7) => X1 sub X7) & ( (X1 sub X8 & X8 sub X9) => X1 sub X9) & ( (X1 sub X8 & X8 sub X10) => X1 sub X10) & ( (X1 sub X9 & X9 sub X2) => X1 sub X2) & ( (X1 sub X9 & X9 sub X3) => X1 sub X3) & ( (X1 sub X9 & X9 sub X4) => X1 sub X4) & ( (X1 sub X9 & X9 sub X5) => X1 sub X5) & ( (X1 sub X9 & X9 sub X6) => X1 sub X6) & ( (X1 sub X9 & X9 sub X7) => X1 sub X7) & ( (X1 sub X9 & X9 sub X8) => X1 sub X8) & ( (X1 sub X9 & X9 sub X10) => X1 sub X10) & ( (X1 sub X10 & X10 sub X2) => X1 sub X2) & ( (X1 sub X10 & X10 sub X3) => X1 sub X3) & ( (X1 sub X10 & X10 sub X4) => X1 sub X4) & ( (X1 sub X10 & X10 sub X5) => X1 sub X5) & ( (X1 sub X10 & X10 sub X6) => X1 sub X6) & ( (X1 sub X10 & X10 sub X7) => X1 sub X7) & ( (X1 sub X10 & X10 sub X8) => X1 sub X8) & ( (X1 sub X10 & X10 sub X9) => X1 sub X9) & ( (X2 sub X1 & X1 sub X3) => X2 sub X3) & ( (X2 sub X1 & X1 sub X4) => X2 sub X4) & ( (X2 sub X1 & X1 sub X5) => X2 sub X5) & ( (X2 sub X1 & X1 sub X6) => X2 sub X6) & ( (X2 sub X1 & X1 sub X7) => X2 sub X7) & ( (X2 sub X1 & X1 sub X8) => X2 sub X8) & ( (X2 sub X1 & X1 sub X9) => X2 sub X9) & ( (X2 sub X1 & X1 sub X10) => X2 sub X10) & ( (X2 sub X3 & X3 sub X1) => X2 sub X1) & ( (X2 sub X3 & X3 sub X4) => X2 sub X4) & ( (X2 sub X3 & X3 sub X5) => X2 sub X5) & ( (X2 sub X3 & X3 sub X6) => X2 sub X6) & ( (X2 sub X3 & X3 sub X7) => X2 sub X7) & ( (X2 sub X3 & X3 sub X8) => X2 sub X8) & ( (X2 sub X3 & X3 sub X9) => X2 sub X9) & ( (X2 sub X3 & X3 sub X10) => X2 sub X10) & ( (X2 sub X4 & X4 sub X1) => X2 sub X1) & ( (X2 sub X4 & X4 sub X3) => X2 sub X3) & ( (X2 sub X4 & X4 sub X5) => X2 sub X5) & ( (X2 sub X4 & X4 sub X6) => X2 sub X6) & ( (X2 sub X4 & X4 sub X7) => X2 sub X7) & ( (X2 sub X4 & X4 sub X8) => X2 sub X8) & ( (X2 sub X4 & X4 sub X9) => X2 sub X9) & ( (X2 sub X4 & X4 sub X10) => X2 sub X10) & ( (X2 sub X5 & X5 sub X1) => X2 sub X1) & ( (X2 sub X5 & X5 sub X3) => X2 sub X3) & ( (X2 sub X5 & X5 sub X4) => X2 sub X4) & ( (X2 sub X5 & X5 sub X6) => X2 sub X6) & ( (X2 sub X5 & X5 sub X7) => X2 sub X7) & ( (X2 sub X5 & X5 sub X8) => X2 sub X8) & ( (X2 sub X5 & X5 sub X9) => X2 sub X9) & ( (X2 sub X5 & X5 sub X10) => X2 sub X10) & ( (X2 sub X6 & X6 sub X1) => X2 sub X1) & ( (X2 sub X6 & X6 sub X3) => X2 sub X3) & ( (X2 sub X6 & X6 sub X4) => X2 sub X4) & ( (X2 sub X6 & X6 sub X5) => X2 sub X5) & ( (X2 sub X6 & X6 sub X7) => X2 sub X7) & ( (X2 sub X6 & X6 sub X8) => X2 sub X8) & ( (X2 sub X6 & X6 sub X9) => X2 sub X9) & ( (X2 sub X6 & X6 sub X10) => X2 sub X10) & ( (X2 sub X7 & X7 sub X1) => X2 sub X1) & ( (X2 sub X7 & X7 sub X3) => X2 sub X3) & ( (X2 sub X7 & X7 sub X4) => X2 sub X4) & ( (X2 sub X7 & X7 sub X5) => X2 sub X5) & ( (X2 sub X7 & X7 sub X6) => X2 sub X6) & ( (X2 sub X7 & X7 sub X8) => X2 sub X8) & ( (X2 sub X7 & X7 sub X9) => X2 sub X9) & ( (X2 sub X7 & X7 sub X10) => X2 sub X10) & ( (X2 sub X8 & X8 sub X1) => X2 sub X1) & ( (X2 sub X8 & X8 sub X3) => X2 sub X3) & ( (X2 sub X8 & X8 sub X4) => X2 sub X4) & ( (X2 sub X8 & X8 sub X5) => X2 sub X5) & ( (X2 sub X8 & X8 sub X6) => X2 sub X6) & ( (X2 sub X8 & X8 sub X7) => X2 sub X7) & ( (X2 sub X8 & X8 sub X9) => X2 sub X9) & ( (X2 sub X8 & X8 sub X10) => X2 sub X10) & ( (X2 sub X9 & X9 sub X1) => X2 sub X1) & ( (X2 sub X9 & X9 sub X3) => X2 sub X3) & ( (X2 sub X9 & X9 sub X4) => X2 sub X4) & ( (X2 sub X9 & X9 sub X5) => X2 sub X5) & ( (X2 sub X9 & X9 sub X6) => X2 sub X6) & ( (X2 sub X9 & X9 sub X7) => X2 sub X7) & ( (X2 sub X9 & X9 sub X8) => X2 sub X8) & ( (X2 sub X9 & X9 sub X10) => X2 sub X10) & ( (X2 sub X10 & X10 sub X1) => X2 sub X1) & ( (X2 sub X10 & X10 sub X3) => X2 sub X3) & ( (X2 sub X10 & X10 sub X4) => X2 sub X4) & ( (X2 sub X10 & X10 sub X5) => X2 sub X5) & ( (X2 sub X10 & X10 sub X6) => X2 sub X6) & ( (X2 sub X10 & X10 sub X7) => X2 sub X7) & ( (X2 sub X10 & X10 sub X8) => X2 sub X8) & ( (X2 sub X10 & X10 sub X9) => X2 sub X9) & ( (X3 sub X1 & X1 sub X2) => X3 sub X2) & ( (X3 sub X1 & X1 sub X4) => X3 sub X4) & ( (X3 sub X1 & X1 sub X5) => X3 sub X5) & ( (X3 sub X1 & X1 sub X6) => X3 sub X6) & ( (X3 sub X1 & X1 sub X7) => X3 sub X7) & ( (X3 sub X1 & X1 sub X8) => X3 sub X8) & ( (X3 sub X1 & X1 sub X9) => X3 sub X9) & ( (X3 sub X1 & X1 sub X10) => X3 sub X10) & ( (X3 sub X2 & X2 sub X1) => X3 sub X1) & ( (X3 sub X2 & X2 sub X4) => X3 sub X4) & ( (X3 sub X2 & X2 sub X5) => X3 sub X5) & ( (X3 sub X2 & X2 sub X6) => X3 sub X6) & ( (X3 sub X2 & X2 sub X7) => X3 sub X7) & ( (X3 sub X2 & X2 sub X8) => X3 sub X8) & ( (X3 sub X2 & X2 sub X9) => X3 sub X9) & ( (X3 sub X2 & X2 sub X10) => X3 sub X10) & ( (X3 sub X4 & X4 sub X1) => X3 sub X1) & ( (X3 sub X4 & X4 sub X2) => X3 sub X2) & ( (X3 sub X4 & X4 sub X5) => X3 sub X5) & ( (X3 sub X4 & X4 sub X6) => X3 sub X6) & ( (X3 sub X4 & X4 sub X7) => X3 sub X7) & ( (X3 sub X4 & X4 sub X8) => X3 sub X8) & ( (X3 sub X4 & X4 sub X9) => X3 sub X9) & ( (X3 sub X4 & X4 sub X10) => X3 sub X10) & ( (X3 sub X5 & X5 sub X1) => X3 sub X1) & ( (X3 sub X5 & X5 sub X2) => X3 sub X2) & ( (X3 sub X5 & X5 sub X4) => X3 sub X4) & ( (X3 sub X5 & X5 sub X6) => X3 sub X6) & ( (X3 sub X5 & X5 sub X7) => X3 sub X7) & ( (X3 sub X5 & X5 sub X8) => X3 sub X8) & ( (X3 sub X5 & X5 sub X9) => X3 sub X9) & ( (X3 sub X5 & X5 sub X10) => X3 sub X10) & ( (X3 sub X6 & X6 sub X1) => X3 sub X1) & ( (X3 sub X6 & X6 sub X2) => X3 sub X2) & ( (X3 sub X6 & X6 sub X4) => X3 sub X4) & ( (X3 sub X6 & X6 sub X5) => X3 sub X5) & ( (X3 sub X6 & X6 sub X7) => X3 sub X7) & ( (X3 sub X6 & X6 sub X8) => X3 sub X8) & ( (X3 sub X6 & X6 sub X9) => X3 sub X9) & ( (X3 sub X6 & X6 sub X10) => X3 sub X10) & ( (X3 sub X7 & X7 sub X1) => X3 sub X1) & ( (X3 sub X7 & X7 sub X2) => X3 sub X2) & ( (X3 sub X7 & X7 sub X4) => X3 sub X4) & ( (X3 sub X7 & X7 sub X5) => X3 sub X5) & ( (X3 sub X7 & X7 sub X6) => X3 sub X6) & ( (X3 sub X7 & X7 sub X8) => X3 sub X8) & ( (X3 sub X7 & X7 sub X9) => X3 sub X9) & ( (X3 sub X7 & X7 sub X10) => X3 sub X10) & ( (X3 sub X8 & X8 sub X1) => X3 sub X1) & ( (X3 sub X8 & X8 sub X2) => X3 sub X2) & ( (X3 sub X8 & X8 sub X4) => X3 sub X4) & ( (X3 sub X8 & X8 sub X5) => X3 sub X5) & ( (X3 sub X8 & X8 sub X6) => X3 sub X6) & ( (X3 sub X8 & X8 sub X7) => X3 sub X7) & ( (X3 sub X8 & X8 sub X9) => X3 sub X9) & ( (X3 sub X8 & X8 sub X10) => X3 sub X10) & ( (X3 sub X9 & X9 sub X1) => X3 sub X1) & ( (X3 sub X9 & X9 sub X2) => X3 sub X2) & ( (X3 sub X9 & X9 sub X4) => X3 sub X4) & ( (X3 sub X9 & X9 sub X5) => X3 sub X5) & ( (X3 sub X9 & X9 sub X6) => X3 sub X6) & ( (X3 sub X9 & X9 sub X7) => X3 sub X7) & ( (X3 sub X9 & X9 sub X8) => X3 sub X8) & ( (X3 sub X9 & X9 sub X10) => X3 sub X10) & ( (X3 sub X10 & X10 sub X1) => X3 sub X1) & ( (X3 sub X10 & X10 sub X2) => X3 sub X2) & ( (X3 sub X10 & X10 sub X4) => X3 sub X4) & ( (X3 sub X10 & X10 sub X5) => X3 sub X5) & ( (X3 sub X10 & X10 sub X6) => X3 sub X6) & ( (X3 sub X10 & X10 sub X7) => X3 sub X7) & ( (X3 sub X10 & X10 sub X8) => X3 sub X8) & ( (X3 sub X10 & X10 sub X9) => X3 sub X9) & ( (X4 sub X1 & X1 sub X2) => X4 sub X2) & ( (X4 sub X1 & X1 sub X3) => X4 sub X3) & ( (X4 sub X1 & X1 sub X5) => X4 sub X5) & ( (X4 sub X1 & X1 sub X6) => X4 sub X6) & ( (X4 sub X1 & X1 sub X7) => X4 sub X7) & ( (X4 sub X1 & X1 sub X8) => X4 sub X8) & ( (X4 sub X1 & X1 sub X9) => X4 sub X9) & ( (X4 sub X1 & X1 sub X10) => X4 sub X10) & ( (X4 sub X2 & X2 sub X1) => X4 sub X1) & ( (X4 sub X2 & X2 sub X3) => X4 sub X3) & ( (X4 sub X2 & X2 sub X5) => X4 sub X5) & ( (X4 sub X2 & X2 sub X6) => X4 sub X6) & ( (X4 sub X2 & X2 sub X7) => X4 sub X7) & ( (X4 sub X2 & X2 sub X8) => X4 sub X8) & ( (X4 sub X2 & X2 sub X9) => X4 sub X9) & ( (X4 sub X2 & X2 sub X10) => X4 sub X10) & ( (X4 sub X3 & X3 sub X1) => X4 sub X1) & ( (X4 sub X3 & X3 sub X2) => X4 sub X2) & ( (X4 sub X3 & X3 sub X5) => X4 sub X5) & ( (X4 sub X3 & X3 sub X6) => X4 sub X6) & ( (X4 sub X3 & X3 sub X7) => X4 sub X7) & ( (X4 sub X3 & X3 sub X8) => X4 sub X8) & ( (X4 sub X3 & X3 sub X9) => X4 sub X9) & ( (X4 sub X3 & X3 sub X10) => X4 sub X10) & ( (X4 sub X5 & X5 sub X1) => X4 sub X1) & ( (X4 sub X5 & X5 sub X2) => X4 sub X2) & ( (X4 sub X5 & X5 sub X3) => X4 sub X3) & ( (X4 sub X5 & X5 sub X6) => X4 sub X6) & ( (X4 sub X5 & X5 sub X7) => X4 sub X7) & ( (X4 sub X5 & X5 sub X8) => X4 sub X8) & ( (X4 sub X5 & X5 sub X9) => X4 sub X9) & ( (X4 sub X5 & X5 sub X10) => X4 sub X10) & ( (X4 sub X6 & X6 sub X1) => X4 sub X1) & ( (X4 sub X6 & X6 sub X2) => X4 sub X2) & ( (X4 sub X6 & X6 sub X3) => X4 sub X3) & ( (X4 sub X6 & X6 sub X5) => X4 sub X5) & ( (X4 sub X6 & X6 sub X7) => X4 sub X7) & ( (X4 sub X6 & X6 sub X8) => X4 sub X8) & ( (X4 sub X6 & X6 sub X9) => X4 sub X9) & ( (X4 sub X6 & X6 sub X10) => X4 sub X10) & ( (X4 sub X7 & X7 sub X1) => X4 sub X1) & ( (X4 sub X7 & X7 sub X2) => X4 sub X2) & ( (X4 sub X7 & X7 sub X3) => X4 sub X3) & ( (X4 sub X7 & X7 sub X5) => X4 sub X5) & ( (X4 sub X7 & X7 sub X6) => X4 sub X6) & ( (X4 sub X7 & X7 sub X8) => X4 sub X8) & ( (X4 sub X7 & X7 sub X9) => X4 sub X9) & ( (X4 sub X7 & X7 sub X10) => X4 sub X10) & ( (X4 sub X8 & X8 sub X1) => X4 sub X1) & ( (X4 sub X8 & X8 sub X2) => X4 sub X2) & ( (X4 sub X8 & X8 sub X3) => X4 sub X3) & ( (X4 sub X8 & X8 sub X5) => X4 sub X5) & ( (X4 sub X8 & X8 sub X6) => X4 sub X6) & ( (X4 sub X8 & X8 sub X7) => X4 sub X7) & ( (X4 sub X8 & X8 sub X9) => X4 sub X9) & ( (X4 sub X8 & X8 sub X10) => X4 sub X10) & ( (X4 sub X9 & X9 sub X1) => X4 sub X1) & ( (X4 sub X9 & X9 sub X2) => X4 sub X2) & ( (X4 sub X9 & X9 sub X3) => X4 sub X3) & ( (X4 sub X9 & X9 sub X5) => X4 sub X5) & ( (X4 sub X9 & X9 sub X6) => X4 sub X6) & ( (X4 sub X9 & X9 sub X7) => X4 sub X7) & ( (X4 sub X9 & X9 sub X8) => X4 sub X8) & ( (X4 sub X9 & X9 sub X10) => X4 sub X10) & ( (X4 sub X10 & X10 sub X1) => X4 sub X1) & ( (X4 sub X10 & X10 sub X2) => X4 sub X2) & ( (X4 sub X10 & X10 sub X3) => X4 sub X3) & ( (X4 sub X10 & X10 sub X5) => X4 sub X5) & ( (X4 sub X10 & X10 sub X6) => X4 sub X6) & ( (X4 sub X10 & X10 sub X7) => X4 sub X7) & ( (X4 sub X10 & X10 sub X8) => X4 sub X8) & ( (X4 sub X10 & X10 sub X9) => X4 sub X9) & ( (X5 sub X1 & X1 sub X2) => X5 sub X2) & ( (X5 sub X1 & X1 sub X3) => X5 sub X3) & ( (X5 sub X1 & X1 sub X4) => X5 sub X4) & ( (X5 sub X1 & X1 sub X6) => X5 sub X6) & ( (X5 sub X1 & X1 sub X7) => X5 sub X7) & ( (X5 sub X1 & X1 sub X8) => X5 sub X8) & ( (X5 sub X1 & X1 sub X9) => X5 sub X9) & ( (X5 sub X1 & X1 sub X10) => X5 sub X10) & ( (X5 sub X2 & X2 sub X1) => X5 sub X1) & ( (X5 sub X2 & X2 sub X3) => X5 sub X3) & ( (X5 sub X2 & X2 sub X4) => X5 sub X4) & ( (X5 sub X2 & X2 sub X6) => X5 sub X6) & ( (X5 sub X2 & X2 sub X7) => X5 sub X7) & ( (X5 sub X2 & X2 sub X8) => X5 sub X8) & ( (X5 sub X2 & X2 sub X9) => X5 sub X9) & ( (X5 sub X2 & X2 sub X10) => X5 sub X10) & ( (X5 sub X3 & X3 sub X1) => X5 sub X1) & ( (X5 sub X3 & X3 sub X2) => X5 sub X2) & ( (X5 sub X3 & X3 sub X4) => X5 sub X4) & ( (X5 sub X3 & X3 sub X6) => X5 sub X6) & ( (X5 sub X3 & X3 sub X7) => X5 sub X7) & ( (X5 sub X3 & X3 sub X8) => X5 sub X8) & ( (X5 sub X3 & X3 sub X9) => X5 sub X9) & ( (X5 sub X3 & X3 sub X10) => X5 sub X10) & ( (X5 sub X4 & X4 sub X1) => X5 sub X1) & ( (X5 sub X4 & X4 sub X2) => X5 sub X2) & ( (X5 sub X4 & X4 sub X3) => X5 sub X3) & ( (X5 sub X4 & X4 sub X6) => X5 sub X6) & ( (X5 sub X4 & X4 sub X7) => X5 sub X7) & ( (X5 sub X4 & X4 sub X8) => X5 sub X8) & ( (X5 sub X4 & X4 sub X9) => X5 sub X9) & ( (X5 sub X4 & X4 sub X10) => X5 sub X10) & ( (X5 sub X6 & X6 sub X1) => X5 sub X1) & ( (X5 sub X6 & X6 sub X2) => X5 sub X2) & ( (X5 sub X6 & X6 sub X3) => X5 sub X3) & ( (X5 sub X6 & X6 sub X4) => X5 sub X4) & ( (X5 sub X6 & X6 sub X7) => X5 sub X7) & ( (X5 sub X6 & X6 sub X8) => X5 sub X8) & ( (X5 sub X6 & X6 sub X9) => X5 sub X9) & ( (X5 sub X6 & X6 sub X10) => X5 sub X10) & ( (X5 sub X7 & X7 sub X1) => X5 sub X1) & ( (X5 sub X7 & X7 sub X2) => X5 sub X2) & ( (X5 sub X7 & X7 sub X3) => X5 sub X3) & ( (X5 sub X7 & X7 sub X4) => X5 sub X4) & ( (X5 sub X7 & X7 sub X6) => X5 sub X6) & ( (X5 sub X7 & X7 sub X8) => X5 sub X8) & ( (X5 sub X7 & X7 sub X9) => X5 sub X9) & ( (X5 sub X7 & X7 sub X10) => X5 sub X10) & ( (X5 sub X8 & X8 sub X1) => X5 sub X1) & ( (X5 sub X8 & X8 sub X2) => X5 sub X2) & ( (X5 sub X8 & X8 sub X3) => X5 sub X3) & ( (X5 sub X8 & X8 sub X4) => X5 sub X4) & ( (X5 sub X8 & X8 sub X6) => X5 sub X6) & ( (X5 sub X8 & X8 sub X7) => X5 sub X7) & ( (X5 sub X8 & X8 sub X9) => X5 sub X9) & ( (X5 sub X8 & X8 sub X10) => X5 sub X10) & ( (X5 sub X9 & X9 sub X1) => X5 sub X1) & ( (X5 sub X9 & X9 sub X2) => X5 sub X2) & ( (X5 sub X9 & X9 sub X3) => X5 sub X3) & ( (X5 sub X9 & X9 sub X4) => X5 sub X4) & ( (X5 sub X9 & X9 sub X6) => X5 sub X6) & ( (X5 sub X9 & X9 sub X7) => X5 sub X7) & ( (X5 sub X9 & X9 sub X8) => X5 sub X8) & ( (X5 sub X9 & X9 sub X10) => X5 sub X10) & ( (X5 sub X10 & X10 sub X1) => X5 sub X1) & ( (X5 sub X10 & X10 sub X2) => X5 sub X2) & ( (X5 sub X10 & X10 sub X3) => X5 sub X3) & ( (X5 sub X10 & X10 sub X4) => X5 sub X4) & ( (X5 sub X10 & X10 sub X6) => X5 sub X6) & ( (X5 sub X10 & X10 sub X7) => X5 sub X7) & ( (X5 sub X10 & X10 sub X8) => X5 sub X8) & ( (X5 sub X10 & X10 sub X9) => X5 sub X9) & ( (X6 sub X1 & X1 sub X2) => X6 sub X2) & ( (X6 sub X1 & X1 sub X3) => X6 sub X3) & ( (X6 sub X1 & X1 sub X4) => X6 sub X4) & ( (X6 sub X1 & X1 sub X5) => X6 sub X5) & ( (X6 sub X1 & X1 sub X7) => X6 sub X7) & ( (X6 sub X1 & X1 sub X8) => X6 sub X8) & ( (X6 sub X1 & X1 sub X9) => X6 sub X9) & ( (X6 sub X1 & X1 sub X10) => X6 sub X10) & ( (X6 sub X2 & X2 sub X1) => X6 sub X1) & ( (X6 sub X2 & X2 sub X3) => X6 sub X3) & ( (X6 sub X2 & X2 sub X4) => X6 sub X4) & ( (X6 sub X2 & X2 sub X5) => X6 sub X5) & ( (X6 sub X2 & X2 sub X7) => X6 sub X7) & ( (X6 sub X2 & X2 sub X8) => X6 sub X8) & ( (X6 sub X2 & X2 sub X9) => X6 sub X9) & ( (X6 sub X2 & X2 sub X10) => X6 sub X10) & ( (X6 sub X3 & X3 sub X1) => X6 sub X1) & ( (X6 sub X3 & X3 sub X2) => X6 sub X2) & ( (X6 sub X3 & X3 sub X4) => X6 sub X4) & ( (X6 sub X3 & X3 sub X5) => X6 sub X5) & ( (X6 sub X3 & X3 sub X7) => X6 sub X7) & ( (X6 sub X3 & X3 sub X8) => X6 sub X8) & ( (X6 sub X3 & X3 sub X9) => X6 sub X9) & ( (X6 sub X3 & X3 sub X10) => X6 sub X10) & ( (X6 sub X4 & X4 sub X1) => X6 sub X1) & ( (X6 sub X4 & X4 sub X2) => X6 sub X2) & ( (X6 sub X4 & X4 sub X3) => X6 sub X3) & ( (X6 sub X4 & X4 sub X5) => X6 sub X5) & ( (X6 sub X4 & X4 sub X7) => X6 sub X7) & ( (X6 sub X4 & X4 sub X8) => X6 sub X8) & ( (X6 sub X4 & X4 sub X9) => X6 sub X9) & ( (X6 sub X4 & X4 sub X10) => X6 sub X10) & ( (X6 sub X5 & X5 sub X1) => X6 sub X1) & ( (X6 sub X5 & X5 sub X2) => X6 sub X2) & ( (X6 sub X5 & X5 sub X3) => X6 sub X3) & ( (X6 sub X5 & X5 sub X4) => X6 sub X4) & ( (X6 sub X5 & X5 sub X7) => X6 sub X7) & ( (X6 sub X5 & X5 sub X8) => X6 sub X8) & ( (X6 sub X5 & X5 sub X9) => X6 sub X9) & ( (X6 sub X5 & X5 sub X10) => X6 sub X10) & ( (X6 sub X7 & X7 sub X1) => X6 sub X1) & ( (X6 sub X7 & X7 sub X2) => X6 sub X2) & ( (X6 sub X7 & X7 sub X3) => X6 sub X3) & ( (X6 sub X7 & X7 sub X4) => X6 sub X4) & ( (X6 sub X7 & X7 sub X5) => X6 sub X5) & ( (X6 sub X7 & X7 sub X8) => X6 sub X8) & ( (X6 sub X7 & X7 sub X9) => X6 sub X9) & ( (X6 sub X7 & X7 sub X10) => X6 sub X10) & ( (X6 sub X8 & X8 sub X1) => X6 sub X1) & ( (X6 sub X8 & X8 sub X2) => X6 sub X2) & ( (X6 sub X8 & X8 sub X3) => X6 sub X3) & ( (X6 sub X8 & X8 sub X4) => X6 sub X4) & ( (X6 sub X8 & X8 sub X5) => X6 sub X5) & ( (X6 sub X8 & X8 sub X7) => X6 sub X7) & ( (X6 sub X8 & X8 sub X9) => X6 sub X9) & ( (X6 sub X8 & X8 sub X10) => X6 sub X10) & ( (X6 sub X9 & X9 sub X1) => X6 sub X1) & ( (X6 sub X9 & X9 sub X2) => X6 sub X2) & ( (X6 sub X9 & X9 sub X3) => X6 sub X3) & ( (X6 sub X9 & X9 sub X4) => X6 sub X4) & ( (X6 sub X9 & X9 sub X5) => X6 sub X5) & ( (X6 sub X9 & X9 sub X7) => X6 sub X7) & ( (X6 sub X9 & X9 sub X8) => X6 sub X8) & ( (X6 sub X9 & X9 sub X10) => X6 sub X10) & ( (X6 sub X10 & X10 sub X1) => X6 sub X1) & ( (X6 sub X10 & X10 sub X2) => X6 sub X2) & ( (X6 sub X10 & X10 sub X3) => X6 sub X3) & ( (X6 sub X10 & X10 sub X4) => X6 sub X4) & ( (X6 sub X10 & X10 sub X5) => X6 sub X5) & ( (X6 sub X10 & X10 sub X7) => X6 sub X7) & ( (X6 sub X10 & X10 sub X8) => X6 sub X8) & ( (X6 sub X10 & X10 sub X9) => X6 sub X9) & ( (X7 sub X1 & X1 sub X2) => X7 sub X2) & ( (X7 sub X1 & X1 sub X3) => X7 sub X3) & ( (X7 sub X1 & X1 sub X4) => X7 sub X4) & ( (X7 sub X1 & X1 sub X5) => X7 sub X5) & ( (X7 sub X1 & X1 sub X6) => X7 sub X6) & ( (X7 sub X1 & X1 sub X8) => X7 sub X8) & ( (X7 sub X1 & X1 sub X9) => X7 sub X9) & ( (X7 sub X1 & X1 sub X10) => X7 sub X10) & ( (X7 sub X2 & X2 sub X1) => X7 sub X1) & ( (X7 sub X2 & X2 sub X3) => X7 sub X3) & ( (X7 sub X2 & X2 sub X4) => X7 sub X4) & ( (X7 sub X2 & X2 sub X5) => X7 sub X5) & ( (X7 sub X2 & X2 sub X6) => X7 sub X6) & ( (X7 sub X2 & X2 sub X8) => X7 sub X8) & ( (X7 sub X2 & X2 sub X9) => X7 sub X9) & ( (X7 sub X2 & X2 sub X10) => X7 sub X10) & ( (X7 sub X3 & X3 sub X1) => X7 sub X1) & ( (X7 sub X3 & X3 sub X2) => X7 sub X2) & ( (X7 sub X3 & X3 sub X4) => X7 sub X4) & ( (X7 sub X3 & X3 sub X5) => X7 sub X5) & ( (X7 sub X3 & X3 sub X6) => X7 sub X6) & ( (X7 sub X3 & X3 sub X8) => X7 sub X8) & ( (X7 sub X3 & X3 sub X9) => X7 sub X9) & ( (X7 sub X3 & X3 sub X10) => X7 sub X10) & ( (X7 sub X4 & X4 sub X1) => X7 sub X1) & ( (X7 sub X4 & X4 sub X2) => X7 sub X2) & ( (X7 sub X4 & X4 sub X3) => X7 sub X3) & ( (X7 sub X4 & X4 sub X5) => X7 sub X5) & ( (X7 sub X4 & X4 sub X6) => X7 sub X6) & ( (X7 sub X4 & X4 sub X8) => X7 sub X8) & ( (X7 sub X4 & X4 sub X9) => X7 sub X9) & ( (X7 sub X4 & X4 sub X10) => X7 sub X10) & ( (X7 sub X5 & X5 sub X1) => X7 sub X1) & ( (X7 sub X5 & X5 sub X2) => X7 sub X2) & ( (X7 sub X5 & X5 sub X3) => X7 sub X3) & ( (X7 sub X5 & X5 sub X4) => X7 sub X4) & ( (X7 sub X5 & X5 sub X6) => X7 sub X6) & ( (X7 sub X5 & X5 sub X8) => X7 sub X8) & ( (X7 sub X5 & X5 sub X9) => X7 sub X9) & ( (X7 sub X5 & X5 sub X10) => X7 sub X10) & ( (X7 sub X6 & X6 sub X1) => X7 sub X1) & ( (X7 sub X6 & X6 sub X2) => X7 sub X2) & ( (X7 sub X6 & X6 sub X3) => X7 sub X3) & ( (X7 sub X6 & X6 sub X4) => X7 sub X4) & ( (X7 sub X6 & X6 sub X5) => X7 sub X5) & ( (X7 sub X6 & X6 sub X8) => X7 sub X8) & ( (X7 sub X6 & X6 sub X9) => X7 sub X9) & ( (X7 sub X6 & X6 sub X10) => X7 sub X10) & ( (X7 sub X8 & X8 sub X1) => X7 sub X1) & ( (X7 sub X8 & X8 sub X2) => X7 sub X2) & ( (X7 sub X8 & X8 sub X3) => X7 sub X3) & ( (X7 sub X8 & X8 sub X4) => X7 sub X4) & ( (X7 sub X8 & X8 sub X5) => X7 sub X5) & ( (X7 sub X8 & X8 sub X6) => X7 sub X6) & ( (X7 sub X8 & X8 sub X9) => X7 sub X9) & ( (X7 sub X8 & X8 sub X10) => X7 sub X10) & ( (X7 sub X9 & X9 sub X1) => X7 sub X1) & ( (X7 sub X9 & X9 sub X2) => X7 sub X2) & ( (X7 sub X9 & X9 sub X3) => X7 sub X3) & ( (X7 sub X9 & X9 sub X4) => X7 sub X4) & ( (X7 sub X9 & X9 sub X5) => X7 sub X5) & ( (X7 sub X9 & X9 sub X6) => X7 sub X6) & ( (X7 sub X9 & X9 sub X8) => X7 sub X8) & ( (X7 sub X9 & X9 sub X10) => X7 sub X10) & ( (X7 sub X10 & X10 sub X1) => X7 sub X1) & ( (X7 sub X10 & X10 sub X2) => X7 sub X2) & ( (X7 sub X10 & X10 sub X3) => X7 sub X3) & ( (X7 sub X10 & X10 sub X4) => X7 sub X4) & ( (X7 sub X10 & X10 sub X5) => X7 sub X5) & ( (X7 sub X10 & X10 sub X6) => X7 sub X6) & ( (X7 sub X10 & X10 sub X8) => X7 sub X8) & ( (X7 sub X10 & X10 sub X9) => X7 sub X9) & ( (X8 sub X1 & X1 sub X2) => X8 sub X2) & ( (X8 sub X1 & X1 sub X3) => X8 sub X3) & ( (X8 sub X1 & X1 sub X4) => X8 sub X4) & ( (X8 sub X1 & X1 sub X5) => X8 sub X5) & ( (X8 sub X1 & X1 sub X6) => X8 sub X6) & ( (X8 sub X1 & X1 sub X7) => X8 sub X7) & ( (X8 sub X1 & X1 sub X9) => X8 sub X9) & ( (X8 sub X1 & X1 sub X10) => X8 sub X10) & ( (X8 sub X2 & X2 sub X1) => X8 sub X1) & ( (X8 sub X2 & X2 sub X3) => X8 sub X3) & ( (X8 sub X2 & X2 sub X4) => X8 sub X4) & ( (X8 sub X2 & X2 sub X5) => X8 sub X5) & ( (X8 sub X2 & X2 sub X6) => X8 sub X6) & ( (X8 sub X2 & X2 sub X7) => X8 sub X7) & ( (X8 sub X2 & X2 sub X9) => X8 sub X9) & ( (X8 sub X2 & X2 sub X10) => X8 sub X10) & ( (X8 sub X3 & X3 sub X1) => X8 sub X1) & ( (X8 sub X3 & X3 sub X2) => X8 sub X2) & ( (X8 sub X3 & X3 sub X4) => X8 sub X4) & ( (X8 sub X3 & X3 sub X5) => X8 sub X5) & ( (X8 sub X3 & X3 sub X6) => X8 sub X6) & ( (X8 sub X3 & X3 sub X7) => X8 sub X7) & ( (X8 sub X3 & X3 sub X9) => X8 sub X9) & ( (X8 sub X3 & X3 sub X10) => X8 sub X10) & ( (X8 sub X4 & X4 sub X1) => X8 sub X1) & ( (X8 sub X4 & X4 sub X2) => X8 sub X2) & ( (X8 sub X4 & X4 sub X3) => X8 sub X3) & ( (X8 sub X4 & X4 sub X5) => X8 sub X5) & ( (X8 sub X4 & X4 sub X6) => X8 sub X6) & ( (X8 sub X4 & X4 sub X7) => X8 sub X7) & ( (X8 sub X4 & X4 sub X9) => X8 sub X9) & ( (X8 sub X4 & X4 sub X10) => X8 sub X10) & ( (X8 sub X5 & X5 sub X1) => X8 sub X1) & ( (X8 sub X5 & X5 sub X2) => X8 sub X2) & ( (X8 sub X5 & X5 sub X3) => X8 sub X3) & ( (X8 sub X5 & X5 sub X4) => X8 sub X4) & ( (X8 sub X5 & X5 sub X6) => X8 sub X6) & ( (X8 sub X5 & X5 sub X7) => X8 sub X7) & ( (X8 sub X5 & X5 sub X9) => X8 sub X9) & ( (X8 sub X5 & X5 sub X10) => X8 sub X10) & ( (X8 sub X6 & X6 sub X1) => X8 sub X1) & ( (X8 sub X6 & X6 sub X2) => X8 sub X2) & ( (X8 sub X6 & X6 sub X3) => X8 sub X3) & ( (X8 sub X6 & X6 sub X4) => X8 sub X4) & ( (X8 sub X6 & X6 sub X5) => X8 sub X5) & ( (X8 sub X6 & X6 sub X7) => X8 sub X7) & ( (X8 sub X6 & X6 sub X9) => X8 sub X9) & ( (X8 sub X6 & X6 sub X10) => X8 sub X10) & ( (X8 sub X7 & X7 sub X1) => X8 sub X1) & ( (X8 sub X7 & X7 sub X2) => X8 sub X2) & ( (X8 sub X7 & X7 sub X3) => X8 sub X3) & ( (X8 sub X7 & X7 sub X4) => X8 sub X4) & ( (X8 sub X7 & X7 sub X5) => X8 sub X5) & ( (X8 sub X7 & X7 sub X6) => X8 sub X6) & ( (X8 sub X7 & X7 sub X9) => X8 sub X9) & ( (X8 sub X7 & X7 sub X10) => X8 sub X10) & ( (X8 sub X9 & X9 sub X1) => X8 sub X1) & ( (X8 sub X9 & X9 sub X2) => X8 sub X2) & ( (X8 sub X9 & X9 sub X3) => X8 sub X3) & ( (X8 sub X9 & X9 sub X4) => X8 sub X4) & ( (X8 sub X9 & X9 sub X5) => X8 sub X5) & ( (X8 sub X9 & X9 sub X6) => X8 sub X6) & ( (X8 sub X9 & X9 sub X7) => X8 sub X7) & ( (X8 sub X9 & X9 sub X10) => X8 sub X10) & ( (X8 sub X10 & X10 sub X1) => X8 sub X1) & ( (X8 sub X10 & X10 sub X2) => X8 sub X2) & ( (X8 sub X10 & X10 sub X3) => X8 sub X3) & ( (X8 sub X10 & X10 sub X4) => X8 sub X4) & ( (X8 sub X10 & X10 sub X5) => X8 sub X5) & ( (X8 sub X10 & X10 sub X6) => X8 sub X6) & ( (X8 sub X10 & X10 sub X7) => X8 sub X7) & ( (X8 sub X10 & X10 sub X9) => X8 sub X9) & ( (X9 sub X1 & X1 sub X2) => X9 sub X2) & ( (X9 sub X1 & X1 sub X3) => X9 sub X3) & ( (X9 sub X1 & X1 sub X4) => X9 sub X4) & ( (X9 sub X1 & X1 sub X5) => X9 sub X5) & ( (X9 sub X1 & X1 sub X6) => X9 sub X6) & ( (X9 sub X1 & X1 sub X7) => X9 sub X7) & ( (X9 sub X1 & X1 sub X8) => X9 sub X8) & ( (X9 sub X1 & X1 sub X10) => X9 sub X10) & ( (X9 sub X2 & X2 sub X1) => X9 sub X1) & ( (X9 sub X2 & X2 sub X3) => X9 sub X3) & ( (X9 sub X2 & X2 sub X4) => X9 sub X4) & ( (X9 sub X2 & X2 sub X5) => X9 sub X5) & ( (X9 sub X2 & X2 sub X6) => X9 sub X6) & ( (X9 sub X2 & X2 sub X7) => X9 sub X7) & ( (X9 sub X2 & X2 sub X8) => X9 sub X8) & ( (X9 sub X2 & X2 sub X10) => X9 sub X10) & ( (X9 sub X3 & X3 sub X1) => X9 sub X1) & ( (X9 sub X3 & X3 sub X2) => X9 sub X2) & ( (X9 sub X3 & X3 sub X4) => X9 sub X4) & ( (X9 sub X3 & X3 sub X5) => X9 sub X5) & ( (X9 sub X3 & X3 sub X6) => X9 sub X6) & ( (X9 sub X3 & X3 sub X7) => X9 sub X7) & ( (X9 sub X3 & X3 sub X8) => X9 sub X8) & ( (X9 sub X3 & X3 sub X10) => X9 sub X10) & ( (X9 sub X4 & X4 sub X1) => X9 sub X1) & ( (X9 sub X4 & X4 sub X2) => X9 sub X2) & ( (X9 sub X4 & X4 sub X3) => X9 sub X3) & ( (X9 sub X4 & X4 sub X5) => X9 sub X5) & ( (X9 sub X4 & X4 sub X6) => X9 sub X6) & ( (X9 sub X4 & X4 sub X7) => X9 sub X7) & ( (X9 sub X4 & X4 sub X8) => X9 sub X8) & ( (X9 sub X4 & X4 sub X10) => X9 sub X10) & ( (X9 sub X5 & X5 sub X1) => X9 sub X1) & ( (X9 sub X5 & X5 sub X2) => X9 sub X2) & ( (X9 sub X5 & X5 sub X3) => X9 sub X3) & ( (X9 sub X5 & X5 sub X4) => X9 sub X4) & ( (X9 sub X5 & X5 sub X6) => X9 sub X6) & ( (X9 sub X5 & X5 sub X7) => X9 sub X7) & ( (X9 sub X5 & X5 sub X8) => X9 sub X8) & ( (X9 sub X5 & X5 sub X10) => X9 sub X10) & ( (X9 sub X6 & X6 sub X1) => X9 sub X1) & ( (X9 sub X6 & X6 sub X2) => X9 sub X2) & ( (X9 sub X6 & X6 sub X3) => X9 sub X3) & ( (X9 sub X6 & X6 sub X4) => X9 sub X4) & ( (X9 sub X6 & X6 sub X5) => X9 sub X5) & ( (X9 sub X6 & X6 sub X7) => X9 sub X7) & ( (X9 sub X6 & X6 sub X8) => X9 sub X8) & ( (X9 sub X6 & X6 sub X10) => X9 sub X10) & ( (X9 sub X7 & X7 sub X1) => X9 sub X1) & ( (X9 sub X7 & X7 sub X2) => X9 sub X2) & ( (X9 sub X7 & X7 sub X3) => X9 sub X3) & ( (X9 sub X7 & X7 sub X4) => X9 sub X4) & ( (X9 sub X7 & X7 sub X5) => X9 sub X5) & ( (X9 sub X7 & X7 sub X6) => X9 sub X6) & ( (X9 sub X7 & X7 sub X8) => X9 sub X8) & ( (X9 sub X7 & X7 sub X10) => X9 sub X10) & ( (X9 sub X8 & X8 sub X1) => X9 sub X1) & ( (X9 sub X8 & X8 sub X2) => X9 sub X2) & ( (X9 sub X8 & X8 sub X3) => X9 sub X3) & ( (X9 sub X8 & X8 sub X4) => X9 sub X4) & ( (X9 sub X8 & X8 sub X5) => X9 sub X5) & ( (X9 sub X8 & X8 sub X6) => X9 sub X6) & ( (X9 sub X8 & X8 sub X7) => X9 sub X7) & ( (X9 sub X8 & X8 sub X10) => X9 sub X10) & ( (X9 sub X10 & X10 sub X1) => X9 sub X1) & ( (X9 sub X10 & X10 sub X2) => X9 sub X2) & ( (X9 sub X10 & X10 sub X3) => X9 sub X3) & ( (X9 sub X10 & X10 sub X4) => X9 sub X4) & ( (X9 sub X10 & X10 sub X5) => X9 sub X5) & ( (X9 sub X10 & X10 sub X6) => X9 sub X6) & ( (X9 sub X10 & X10 sub X7) => X9 sub X7) & ( (X9 sub X10 & X10 sub X8) => X9 sub X8) & ( (X10 sub X1 & X1 sub X2) => X10 sub X2) & ( (X10 sub X1 & X1 sub X3) => X10 sub X3) & ( (X10 sub X1 & X1 sub X4) => X10 sub X4) & ( (X10 sub X1 & X1 sub X5) => X10 sub X5) & ( (X10 sub X1 & X1 sub X6) => X10 sub X6) & ( (X10 sub X1 & X1 sub X7) => X10 sub X7) & ( (X10 sub X1 & X1 sub X8) => X10 sub X8) & ( (X10 sub X1 & X1 sub X9) => X10 sub X9) & ( (X10 sub X2 & X2 sub X1) => X10 sub X1) & ( (X10 sub X2 & X2 sub X3) => X10 sub X3) & ( (X10 sub X2 & X2 sub X4) => X10 sub X4) & ( (X10 sub X2 & X2 sub X5) => X10 sub X5) & ( (X10 sub X2 & X2 sub X6) => X10 sub X6) & ( (X10 sub X2 & X2 sub X7) => X10 sub X7) & ( (X10 sub X2 & X2 sub X8) => X10 sub X8) & ( (X10 sub X2 & X2 sub X9) => X10 sub X9) & ( (X10 sub X3 & X3 sub X1) => X10 sub X1) & ( (X10 sub X3 & X3 sub X2) => X10 sub X2) & ( (X10 sub X3 & X3 sub X4) => X10 sub X4) & ( (X10 sub X3 & X3 sub X5) => X10 sub X5) & ( (X10 sub X3 & X3 sub X6) => X10 sub X6) & ( (X10 sub X3 & X3 sub X7) => X10 sub X7) & ( (X10 sub X3 & X3 sub X8) => X10 sub X8) & ( (X10 sub X3 & X3 sub X9) => X10 sub X9) & ( (X10 sub X4 & X4 sub X1) => X10 sub X1) & ( (X10 sub X4 & X4 sub X2) => X10 sub X2) & ( (X10 sub X4 & X4 sub X3) => X10 sub X3) & ( (X10 sub X4 & X4 sub X5) => X10 sub X5) & ( (X10 sub X4 & X4 sub X6) => X10 sub X6) & ( (X10 sub X4 & X4 sub X7) => X10 sub X7) & ( (X10 sub X4 & X4 sub X8) => X10 sub X8) & ( (X10 sub X4 & X4 sub X9) => X10 sub X9) & ( (X10 sub X5 & X5 sub X1) => X10 sub X1) & ( (X10 sub X5 & X5 sub X2) => X10 sub X2) & ( (X10 sub X5 & X5 sub X3) => X10 sub X3) & ( (X10 sub X5 & X5 sub X4) => X10 sub X4) & ( (X10 sub X5 & X5 sub X6) => X10 sub X6) & ( (X10 sub X5 & X5 sub X7) => X10 sub X7) & ( (X10 sub X5 & X5 sub X8) => X10 sub X8) & ( (X10 sub X5 & X5 sub X9) => X10 sub X9) & ( (X10 sub X6 & X6 sub X1) => X10 sub X1) & ( (X10 sub X6 & X6 sub X2) => X10 sub X2) & ( (X10 sub X6 & X6 sub X3) => X10 sub X3) & ( (X10 sub X6 & X6 sub X4) => X10 sub X4) & ( (X10 sub X6 & X6 sub X5) => X10 sub X5) & ( (X10 sub X6 & X6 sub X7) => X10 sub X7) & ( (X10 sub X6 & X6 sub X8) => X10 sub X8) & ( (X10 sub X6 & X6 sub X9) => X10 sub X9) & ( (X10 sub X7 & X7 sub X1) => X10 sub X1) & ( (X10 sub X7 & X7 sub X2) => X10 sub X2) & ( (X10 sub X7 & X7 sub X3) => X10 sub X3) & ( (X10 sub X7 & X7 sub X4) => X10 sub X4) & ( (X10 sub X7 & X7 sub X5) => X10 sub X5) & ( (X10 sub X7 & X7 sub X6) => X10 sub X6) & ( (X10 sub X7 & X7 sub X8) => X10 sub X8) & ( (X10 sub X7 & X7 sub X9) => X10 sub X9) & ( (X10 sub X8 & X8 sub X1) => X10 sub X1) & ( (X10 sub X8 & X8 sub X2) => X10 sub X2) & ( (X10 sub X8 & X8 sub X3) => X10 sub X3) & ( (X10 sub X8 & X8 sub X4) => X10 sub X4) & ( (X10 sub X8 & X8 sub X5) => X10 sub X5) & ( (X10 sub X8 & X8 sub X6) => X10 sub X6) & ( (X10 sub X8 & X8 sub X7) => X10 sub X7) & ( (X10 sub X8 & X8 sub X9) => X10 sub X9) & ( (X10 sub X9 & X9 sub X1) => X10 sub X1) & ( (X10 sub X9 & X9 sub X2) => X10 sub X2) & ( (X10 sub X9 & X9 sub X3) => X10 sub X3) & ( (X10 sub X9 & X9 sub X4) => X10 sub X4) & ( (X10 sub X9 & X9 sub X5) => X10 sub X5) & ( (X10 sub X9 & X9 sub X6) => X10 sub X6) & ( (X10 sub X9 & X9 sub X7) => X10 sub X7) & ( (X10 sub X9 & X9 sub X8) => X10 sub X8) & X1 sub X & X2 sub X & X3 sub X & X4 sub X & X5 sub X & X6 sub X & X7 sub X & X8 sub X & X9 sub X & X10 sub X;