(* 1 *) A[#1] = L7 &&
        A[#2] = L7

(* 2 *) #1 < #2 &&
        A[#1] = L6 &&
        A[#2] = L7

(* 3 *) A[#1] = L6 &&
        A[#2] = L7 &&
        X[#1, #2] = True

(* 4 *) #1 < #2 &&
        A[#1] = L5 &&
        A[#2] = L7 &&
        X[#1, #2] = True

(* 5 *) #1 < #2 &&
        A[#1] = L6 &&
        A[#2] = L6 &&
        X[#2, #1] = True

(* 6 *) A[#1] = L7 &&
        S[#1] = False

(* 7 *) #1 < #2 &&
        A[#1] = L5 &&
        A[#2] = L7 &&
        W[#2] = False &&
        X[#1, #2] = False

(* 8 *) #1 < #2 &&
        A[#1] = L5 &&
        A[#2] = L6 &&
        X[#1, #2] = True &&
        X[#2, #1] = True

(* 9 *) A[#1] = L6 &&
        S[#1] = False

(* 10 *) A[#1] = L3 &&
         A[#2] = L7

(* 11 *) A[#1] = L4 &&
         A[#2] = L7

(* 12 *) #1 < #2 &&
         A[#1] = L5 &&
         A[#2] = L6 &&
         W[#2] = False &&
         X[#1, #2] = False &&
         X[#2, #1] = True

(* 13 *) A[#1] = L5 &&
         S[#1] = False

(* 14 *) A[#1] = L2 &&
         A[#2] = L7

(* 15 *) A[#1] = L3 &&
         A[#2] = L6

(* 16 *) A[#1] = L4 &&
         A[#2] = L6

(* 17 *) A[#1] = L3 &&
         S[#1] = False

(* 18 *) A[#1] = L2 &&
         A[#2] = L6

(* 19 *) A[#1] = L3 &&
         A[#2] = L5 &&
         X[#2, #1] = True

(* 20 *) A[#1] = L4 &&
         A[#2] = L5 &&
         X[#2, #1] = True

(* 21 *) A[#1] = L2 &&
         A[#2] = L5

(* 22 *) A[#1] = L3 &&
         W[#1] = False

(* 23 *) A[#1] = L4 &&
         W[#1] = False

(* 24 *) A[#1] = L2 &&
         A[#2] = L3 &&
         X[#2, #1] = True

(* 25 *) A[#1] = L2 &&
         S[#1] = True

(* 26 *) A[#2] = L2 &&
         X[#2, #1] = True

(* 27 *) A[#1] = L2 &&
         B[#1] = True

(* 28 *) A[#1] = L2 &&
         W[#1] = True

(* 29 *) A[#1] = L1 &&
         S[#1] = True

(* 30 *) A[#2] = L1 &&
         X[#2, #1] = True

(* 31 *) A[#1] = L1 &&
         W[#1] = True

(* 32 *) A[#1] = L0 &&
         S[#1] = True

(* 33 *) A[#2] = L0 &&
         X[#2, #1] = True

(* 34 *) A[#1] = L0 &&
         W[#1] = True

(* 35 *) A[#2] = L7 &&
         X[#2, #1] = True

(* 36 *) A[#1] = L7 &&
         W[#1] = True

(* 37 *) A[#1] = L6 &&
         W[#1] = True

(* 38 *) A[#1] = L5 &&
         W[#1] = True