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

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

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

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

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

(* 6 *) A[#1] = L7 &&
        B[#1] = True

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

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

(* 9 *) A[#1] = L6 &&
        B[#1] = True

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

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

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

(* 13 *) A[#1] = L5 &&
         B[#1] = True

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

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

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

(* 17 *) A[#1] = L3 &&
         B[#1] = True

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

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

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

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

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

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

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

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

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

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

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

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

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

(* 31 *) A[#1] = L4 &&
         B[#1] = True