YES

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l69, true>
<l1, l2, true, par{bDomain^0 -> (0 + tmp___6^0)}>
<l3, l1, (10 <= (0 + nY^0)), par{tmp___6^0 -> 0}>
<l3, l1, ((1 + nY^0) <= 10), par{tmp___6^0 -> 1}>
<l4, l5, true, par{bAllDifferent^0 -> (0 + tmp^0)}>
<l6, l1, (10 <= (0 + nR^0)), par{tmp___6^0 -> 0}>
<l6, l3, ((1 + nR^0) <= 10)>
<l7, l1, (10 <= (0 + nO^0)), par{tmp___6^0 -> 0}>
<l7, l6, ((1 + nO^0) <= 10)>
<l8, l1, (10 <= (0 + nM^0)), par{tmp___6^0 -> 0}>
<l8, l7, ((1 + nM^0) <= 10)>
<l9, l1, (10 <= (0 + nD^0)), par{tmp___6^0 -> 0}>
<l9, l8, ((1 + nD^0) <= 10)>
<l10, l1, (10 <= (0 + nN^0)), par{tmp___6^0 -> 0}>
<l10, l9, ((1 + nN^0) <= 10)>
<l11, l1, (10 <= (0 + nE^0)), par{tmp___6^0 -> 0}>
<l11, l10, ((1 + nE^0) <= 10)>
<l12, l1, (10 <= (0 + nS^0)), par{tmp___6^0 -> 0}>
<l12, l11, ((1 + nS^0) <= 10)>
<l13, l12, true, par{bAllDifferent^0 -> (0 + tmp___5^0)}>
<l14, l4, true, par{tmp^0 -> 1}>
<l15, l13, true, par{tmp___5^0 -> 1}>
<l16, l13, ((0 + nR^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nR^0)), par{tmp___5^0 -> 0}>
<l16, l15, ((1 + nY^0) <= (0 + nR^0))>
<l16, l15, ((1 + nR^0) <= (0 + nY^0))>
<l17, l13, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{tmp___5^0 -> 0}>
<l17, l16, (1 <= (0 + bAllDifferent^0))>
<l17, l16, ((1 + bAllDifferent^0) <= 0)>
<l18, l17, true, par{bAllDifferent^0 -> (0 + tmp___4^0)}>
<l19, l18, true, par{tmp___4^0 -> 1}>
<l20, l18, ((0 + nO^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nO^0)), par{tmp___4^0 -> 0}>
<l20, l19, ((1 + nY^0) <= (0 + nO^0))>
<l20, l19, ((1 + nO^0) <= (0 + nY^0))>
<l21, l18, ((0 + nO^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nO^0)), par{tmp___4^0 -> 0}>
<l21, l20, ((1 + nR^0) <= (0 + nO^0))>
<l21, l20, ((1 + nO^0) <= (0 + nR^0))>
<l22, l4, ((0 + nS^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nS^0)), par{tmp^0 -> 0}>
<l22, l14, ((1 + nY^0) <= (0 + nS^0))>
<l22, l14, ((1 + nS^0) <= (0 + nY^0))>
<l23, l18, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{tmp___4^0 -> 0}>
<l23, l21, (1 <= (0 + bAllDifferent^0))>
<l23, l21, ((1 + bAllDifferent^0) <= 0)>
<l24, l23, true, par{bAllDifferent^0 -> (0 + tmp___3^0)}>
<l25, l24, true, par{tmp___3^0 -> 1}>
<l26, l24, ((0 + nM^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nM^0)), par{tmp___3^0 -> 0}>
<l26, l25, ((1 + nY^0) <= (0 + nM^0))>
<l26, l25, ((1 + nM^0) <= (0 + nY^0))>
<l27, l24, ((0 + nM^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nM^0)), par{tmp___3^0 -> 0}>
<l27, l26, ((1 + nR^0) <= (0 + nM^0))>
<l27, l26, ((1 + nM^0) <= (0 + nR^0))>
<l28, l24, ((0 + nM^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nM^0)), par{tmp___3^0 -> 0}>
<l28, l27, ((1 + nO^0) <= (0 + nM^0))>
<l28, l27, ((1 + nM^0) <= (0 + nO^0))>
<l29, l4, ((0 + nS^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nS^0)), par{tmp^0 -> 0}>
<l29, l22, ((1 + nR^0) <= (0 + nS^0))>
<l29, l22, ((1 + nS^0) <= (0 + nR^0))>
<l30, l24, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{tmp___3^0 -> 0}>
<l30, l28, (1 <= (0 + bAllDifferent^0))>
<l30, l28, ((1 + bAllDifferent^0) <= 0)>
<l31, l30, true, par{bAllDifferent^0 -> (0 + tmp___2^0)}>
<l32, l31, true, par{tmp___2^0 -> 1}>
<l33, l31, ((0 + nD^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nD^0)), par{tmp___2^0 -> 0}>
<l33, l32, ((1 + nY^0) <= (0 + nD^0))>
<l33, l32, ((1 + nD^0) <= (0 + nY^0))>
<l34, l31, ((0 + nD^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nD^0)), par{tmp___2^0 -> 0}>
<l34, l33, ((1 + nR^0) <= (0 + nD^0))>
<l34, l33, ((1 + nD^0) <= (0 + nR^0))>
<l35, l4, ((0 + nS^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nS^0)), par{tmp^0 -> 0}>
<l35, l29, ((1 + nO^0) <= (0 + nS^0))>
<l35, l29, ((1 + nS^0) <= (0 + nO^0))>
<l36, l31, ((0 + nD^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nD^0)), par{tmp___2^0 -> 0}>
<l36, l34, ((1 + nO^0) <= (0 + nD^0))>
<l36, l34, ((1 + nD^0) <= (0 + nO^0))>
<l37, l31, ((0 + nD^0) <= (0 + nM^0)) /\ ((0 + nM^0) <= (0 + nD^0)), par{tmp___2^0 -> 0}>
<l37, l36, ((1 + nM^0) <= (0 + nD^0))>
<l37, l36, ((1 + nD^0) <= (0 + nM^0))>
<l38, l31, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{tmp___2^0 -> 0}>
<l38, l37, (1 <= (0 + bAllDifferent^0))>
<l38, l37, ((1 + bAllDifferent^0) <= 0)>
<l39, l38, true, par{bAllDifferent^0 -> (0 + tmp___1^0)}>
<l40, l4, ((0 + nS^0) <= (0 + nM^0)) /\ ((0 + nM^0) <= (0 + nS^0)), par{tmp^0 -> 0}>
<l40, l35, ((1 + nM^0) <= (0 + nS^0))>
<l40, l35, ((1 + nS^0) <= (0 + nM^0))>
<l41, l39, true, par{tmp___1^0 -> 1}>
<l42, l39, ((0 + nN^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nN^0)), par{tmp___1^0 -> 0}>
<l42, l41, ((1 + nY^0) <= (0 + nN^0))>
<l42, l41, ((1 + nN^0) <= (0 + nY^0))>
<l43, l39, ((0 + nN^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nN^0)), par{tmp___1^0 -> 0}>
<l43, l42, ((1 + nR^0) <= (0 + nN^0))>
<l43, l42, ((1 + nN^0) <= (0 + nR^0))>
<l44, l39, ((0 + nN^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nN^0)), par{tmp___1^0 -> 0}>
<l44, l43, ((1 + nO^0) <= (0 + nN^0))>
<l44, l43, ((1 + nN^0) <= (0 + nO^0))>
<l45, l39, ((0 + nN^0) <= (0 + nM^0)) /\ ((0 + nM^0) <= (0 + nN^0)), par{tmp___1^0 -> 0}>
<l45, l44, ((1 + nM^0) <= (0 + nN^0))>
<l45, l44, ((1 + nN^0) <= (0 + nM^0))>
<l46, l39, ((0 + nN^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nN^0)), par{tmp___1^0 -> 0}>
<l46, l45, ((1 + nD^0) <= (0 + nN^0))>
<l46, l45, ((1 + nN^0) <= (0 + nD^0))>
<l47, l39, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{tmp___1^0 -> 0}>
<l47, l46, (1 <= (0 + bAllDifferent^0))>
<l47, l46, ((1 + bAllDifferent^0) <= 0)>
<l48, l4, ((0 + nS^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nS^0)), par{tmp^0 -> 0}>
<l48, l40, ((1 + nD^0) <= (0 + nS^0))>
<l48, l40, ((1 + nS^0) <= (0 + nD^0))>
<l49, l47, true, par{bAllDifferent^0 -> (0 + tmp___0^0)}>
<l50, l49, true, par{tmp___0^0 -> 1}>
<l51, l49, ((0 + nE^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nE^0)), par{tmp___0^0 -> 0}>
<l51, l50, ((1 + nY^0) <= (0 + nE^0))>
<l51, l50, ((1 + nE^0) <= (0 + nY^0))>
<l52, l49, ((0 + nE^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nE^0)), par{tmp___0^0 -> 0}>
<l52, l51, ((1 + nR^0) <= (0 + nE^0))>
<l52, l51, ((1 + nE^0) <= (0 + nR^0))>
<l53, l49, ((0 + nE^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nE^0)), par{tmp___0^0 -> 0}>
<l53, l52, ((1 + nO^0) <= (0 + nE^0))>
<l53, l52, ((1 + nE^0) <= (0 + nO^0))>
<l54, l49, ((0 + nE^0) <= (0 + nM^0)) /\ ((0 + nM^0) <= (0 + nE^0)), par{tmp___0^0 -> 0}>
<l54, l53, ((1 + nM^0) <= (0 + nE^0))>
<l54, l53, ((1 + nE^0) <= (0 + nM^0))>
<l55, l4, ((0 + nS^0) <= (0 + nN^0)) /\ ((0 + nN^0) <= (0 + nS^0)), par{tmp^0 -> 0}>
<l55, l48, ((1 + nN^0) <= (0 + nS^0))>
<l55, l48, ((1 + nS^0) <= (0 + nN^0))>
<l56, l49, ((0 + nE^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nE^0)), par{tmp___0^0 -> 0}>
<l56, l54, ((1 + nD^0) <= (0 + nE^0))>
<l56, l54, ((1 + nE^0) <= (0 + nD^0))>
<l57, l49, ((0 + nE^0) <= (0 + nN^0)) /\ ((0 + nN^0) <= (0 + nE^0)), par{tmp___0^0 -> 0}>
<l57, l56, ((1 + nN^0) <= (0 + nE^0))>
<l57, l56, ((1 + nE^0) <= (0 + nN^0))>
<l5, l49, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{tmp___0^0 -> 0}>
<l5, l57, (1 <= (0 + bAllDifferent^0))>
<l5, l57, ((1 + bAllDifferent^0) <= 0)>
<l58, l59, true>
<l60, l58, true, par{tmp___8^0 -> 0}>
<l61, l58, ((0 + bSum^0) <= 0) /\ (0 <= (0 + bSum^0)), par{tmp___8^0 -> 1}>
<l61, l60, (1 <= (0 + bSum^0))>
<l61, l60, ((1 + bSum^0) <= 0)>
<l62, l58, ((0 + bNoLeadingZeros^0) <= 0) /\ (0 <= (0 + bNoLeadingZeros^0)), par{tmp___8^0 -> 1}>
<l62, l61, (1 <= (0 + bNoLeadingZeros^0))>
<l62, l61, ((1 + bNoLeadingZeros^0) <= 0)>
<l63, l58, ((0 + bDomain^0) <= 0) /\ (0 <= (0 + bDomain^0)), par{tmp___8^0 -> 1}>
<l63, l62, (1 <= (0 + bDomain^0))>
<l63, l62, ((1 + bDomain^0) <= 0)>
<l64, l58, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{tmp___8^0 -> 1}>
<l64, l63, (1 <= (0 + bAllDifferent^0))>
<l64, l63, ((1 + bAllDifferent^0) <= 0)>
<l65, l64, (undef3172 = undef3172), par{bNoLeadingZeros^0 -> (0 + tmp___7^0), bSum^0 -> undef3172}>
<l66, l65, true, par{tmp___7^0 -> 1}>
<l67, l65, ((0 + nS^0) <= 0) /\ (0 <= (0 + nS^0)), par{tmp___7^0 -> 0}>
<l67, l66, (1 <= (0 + nS^0))>
<l67, l66, ((1 + nS^0) <= 0)>
<l2, l65, ((0 + nM^0) <= 0) /\ (0 <= (0 + nM^0)), par{tmp___7^0 -> 0}>
<l2, l67, (1 <= (0 + nM^0))>
<l2, l67, ((1 + nM^0) <= 0)>
<l68, l4, ((0 + nS^0) <= (0 + nE^0)) /\ ((0 + nE^0) <= (0 + nS^0)), par{tmp^0 -> 0}>
<l68, l55, ((1 + nE^0) <= (0 + nS^0))>
<l68, l55, ((1 + nS^0) <= (0 + nE^0))>
<l69, l68, true>

Fresh variables:
undef3172, 

Undef variables:
undef3172, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l5, ((0 + nS^0) <= (0 + nE^0)) /\ ((0 + nE^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l0, l5, ((1 + nE^0) <= (0 + nS^0)) /\ ((0 + nS^0) <= (0 + nN^0)) /\ ((0 + nN^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l0, l5, ((1 + nE^0) <= (0 + nS^0)) /\ ((1 + nN^0) <= (0 + nS^0)) /\ ((0 + nS^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l0, l40, ((1 + nE^0) <= (0 + nS^0)) /\ ((1 + nN^0) <= (0 + nS^0)) /\ ((1 + nD^0) <= (0 + nS^0))>
<l0, l40, ((1 + nE^0) <= (0 + nS^0)) /\ ((1 + nN^0) <= (0 + nS^0)) /\ ((1 + nS^0) <= (0 + nD^0))>
<l0, l5, ((1 + nE^0) <= (0 + nS^0)) /\ ((1 + nS^0) <= (0 + nN^0)) /\ ((0 + nS^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l0, l40, ((1 + nE^0) <= (0 + nS^0)) /\ ((1 + nS^0) <= (0 + nN^0)) /\ ((1 + nD^0) <= (0 + nS^0))>
<l0, l40, ((1 + nE^0) <= (0 + nS^0)) /\ ((1 + nS^0) <= (0 + nN^0)) /\ ((1 + nS^0) <= (0 + nD^0))>
<l0, l5, ((1 + nS^0) <= (0 + nE^0)) /\ ((0 + nS^0) <= (0 + nN^0)) /\ ((0 + nN^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l0, l5, ((1 + nS^0) <= (0 + nE^0)) /\ ((1 + nN^0) <= (0 + nS^0)) /\ ((0 + nS^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l0, l40, ((1 + nS^0) <= (0 + nE^0)) /\ ((1 + nN^0) <= (0 + nS^0)) /\ ((1 + nD^0) <= (0 + nS^0))>
<l0, l40, ((1 + nS^0) <= (0 + nE^0)) /\ ((1 + nN^0) <= (0 + nS^0)) /\ ((1 + nS^0) <= (0 + nD^0))>
<l0, l5, ((1 + nS^0) <= (0 + nE^0)) /\ ((1 + nS^0) <= (0 + nN^0)) /\ ((0 + nS^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l0, l40, ((1 + nS^0) <= (0 + nE^0)) /\ ((1 + nS^0) <= (0 + nN^0)) /\ ((1 + nD^0) <= (0 + nS^0))>
<l0, l40, ((1 + nS^0) <= (0 + nE^0)) /\ ((1 + nS^0) <= (0 + nN^0)) /\ ((1 + nS^0) <= (0 + nD^0))>
<l2, l59, ((0 + nM^0) <= 0) /\ (0 <= (0 + nM^0)) /\ (undef3172 = undef3172) /\ ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{bNoLeadingZeros^0 -> (0 + 0), bSum^0 -> undef3172}>
<l2, l63, ((0 + nM^0) <= 0) /\ (0 <= (0 + nM^0)) /\ (undef3172 = undef3172) /\ (1 <= (0 + bAllDifferent^0)), par{bNoLeadingZeros^0 -> (0 + 0), bSum^0 -> undef3172}>
<l2, l63, ((0 + nM^0) <= 0) /\ (0 <= (0 + nM^0)) /\ (undef3172 = undef3172) /\ ((1 + bAllDifferent^0) <= 0), par{bNoLeadingZeros^0 -> (0 + 0), bSum^0 -> undef3172}>
<l2, l59, (1 <= (0 + nM^0)) /\ ((0 + nS^0) <= 0) /\ (0 <= (0 + nS^0)) /\ (undef3172 = undef3172) /\ ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{bNoLeadingZeros^0 -> (0 + 0), bSum^0 -> undef3172}>
<l2, l63, (1 <= (0 + nM^0)) /\ ((0 + nS^0) <= 0) /\ (0 <= (0 + nS^0)) /\ (undef3172 = undef3172) /\ (1 <= (0 + bAllDifferent^0)), par{bNoLeadingZeros^0 -> (0 + 0), bSum^0 -> undef3172}>
<l2, l63, (1 <= (0 + nM^0)) /\ ((0 + nS^0) <= 0) /\ (0 <= (0 + nS^0)) /\ (undef3172 = undef3172) /\ ((1 + bAllDifferent^0) <= 0), par{bNoLeadingZeros^0 -> (0 + 0), bSum^0 -> undef3172}>
<l2, l59, (1 <= (0 + nM^0)) /\ (1 <= (0 + nS^0)) /\ (undef3172 = undef3172) /\ ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{bNoLeadingZeros^0 -> (0 + 1), bSum^0 -> undef3172}>
<l2, l63, (1 <= (0 + nM^0)) /\ (1 <= (0 + nS^0)) /\ (undef3172 = undef3172) /\ (1 <= (0 + bAllDifferent^0)), par{bNoLeadingZeros^0 -> (0 + 1), bSum^0 -> undef3172}>
<l2, l63, (1 <= (0 + nM^0)) /\ (1 <= (0 + nS^0)) /\ (undef3172 = undef3172) /\ ((1 + bAllDifferent^0) <= 0), par{bNoLeadingZeros^0 -> (0 + 1), bSum^0 -> undef3172}>
<l2, l59, (1 <= (0 + nM^0)) /\ ((1 + nS^0) <= 0) /\ (undef3172 = undef3172) /\ ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{bNoLeadingZeros^0 -> (0 + 1), bSum^0 -> undef3172}>
<l2, l63, (1 <= (0 + nM^0)) /\ ((1 + nS^0) <= 0) /\ (undef3172 = undef3172) /\ (1 <= (0 + bAllDifferent^0)), par{bNoLeadingZeros^0 -> (0 + 1), bSum^0 -> undef3172}>
<l2, l63, (1 <= (0 + nM^0)) /\ ((1 + nS^0) <= 0) /\ (undef3172 = undef3172) /\ ((1 + bAllDifferent^0) <= 0), par{bNoLeadingZeros^0 -> (0 + 1), bSum^0 -> undef3172}>
<l2, l59, ((1 + nM^0) <= 0) /\ ((0 + nS^0) <= 0) /\ (0 <= (0 + nS^0)) /\ (undef3172 = undef3172) /\ ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{bNoLeadingZeros^0 -> (0 + 0), bSum^0 -> undef3172}>
<l2, l63, ((1 + nM^0) <= 0) /\ ((0 + nS^0) <= 0) /\ (0 <= (0 + nS^0)) /\ (undef3172 = undef3172) /\ (1 <= (0 + bAllDifferent^0)), par{bNoLeadingZeros^0 -> (0 + 0), bSum^0 -> undef3172}>
<l2, l63, ((1 + nM^0) <= 0) /\ ((0 + nS^0) <= 0) /\ (0 <= (0 + nS^0)) /\ (undef3172 = undef3172) /\ ((1 + bAllDifferent^0) <= 0), par{bNoLeadingZeros^0 -> (0 + 0), bSum^0 -> undef3172}>
<l2, l59, ((1 + nM^0) <= 0) /\ (1 <= (0 + nS^0)) /\ (undef3172 = undef3172) /\ ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{bNoLeadingZeros^0 -> (0 + 1), bSum^0 -> undef3172}>
<l2, l63, ((1 + nM^0) <= 0) /\ (1 <= (0 + nS^0)) /\ (undef3172 = undef3172) /\ (1 <= (0 + bAllDifferent^0)), par{bNoLeadingZeros^0 -> (0 + 1), bSum^0 -> undef3172}>
<l2, l63, ((1 + nM^0) <= 0) /\ (1 <= (0 + nS^0)) /\ (undef3172 = undef3172) /\ ((1 + bAllDifferent^0) <= 0), par{bNoLeadingZeros^0 -> (0 + 1), bSum^0 -> undef3172}>
<l2, l59, ((1 + nM^0) <= 0) /\ ((1 + nS^0) <= 0) /\ (undef3172 = undef3172) /\ ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{bNoLeadingZeros^0 -> (0 + 1), bSum^0 -> undef3172}>
<l2, l63, ((1 + nM^0) <= 0) /\ ((1 + nS^0) <= 0) /\ (undef3172 = undef3172) /\ (1 <= (0 + bAllDifferent^0)), par{bNoLeadingZeros^0 -> (0 + 1), bSum^0 -> undef3172}>
<l2, l63, ((1 + nM^0) <= 0) /\ ((1 + nS^0) <= 0) /\ (undef3172 = undef3172) /\ ((1 + bAllDifferent^0) <= 0), par{bNoLeadingZeros^0 -> (0 + 1), bSum^0 -> undef3172}>
<l5, l47, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l5, l47, (1 <= (0 + bAllDifferent^0)) /\ ((0 + nE^0) <= (0 + nN^0)) /\ ((0 + nN^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l5, l47, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nN^0) <= (0 + nE^0)) /\ ((0 + nE^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l5, l54, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nN^0) <= (0 + nE^0)) /\ ((1 + nD^0) <= (0 + nE^0))>
<l5, l54, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nN^0) <= (0 + nE^0)) /\ ((1 + nE^0) <= (0 + nD^0))>
<l5, l47, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nE^0) <= (0 + nN^0)) /\ ((0 + nE^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l5, l54, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nE^0) <= (0 + nN^0)) /\ ((1 + nD^0) <= (0 + nE^0))>
<l5, l54, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nE^0) <= (0 + nN^0)) /\ ((1 + nE^0) <= (0 + nD^0))>
<l5, l47, ((1 + bAllDifferent^0) <= 0) /\ ((0 + nE^0) <= (0 + nN^0)) /\ ((0 + nN^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l5, l47, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nN^0) <= (0 + nE^0)) /\ ((0 + nE^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l5, l54, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nN^0) <= (0 + nE^0)) /\ ((1 + nD^0) <= (0 + nE^0))>
<l5, l54, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nN^0) <= (0 + nE^0)) /\ ((1 + nE^0) <= (0 + nD^0))>
<l5, l47, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nE^0) <= (0 + nN^0)) /\ ((0 + nE^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l5, l54, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nE^0) <= (0 + nN^0)) /\ ((1 + nD^0) <= (0 + nE^0))>
<l5, l54, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nE^0) <= (0 + nN^0)) /\ ((1 + nE^0) <= (0 + nD^0))>
<l10, l2, (10 <= (0 + nN^0)), par{bDomain^0 -> (0 + 0)}>
<l10, l2, ((1 + nN^0) <= 10) /\ (10 <= (0 + nD^0)), par{bDomain^0 -> (0 + 0)}>
<l10, l2, ((1 + nN^0) <= 10) /\ ((1 + nD^0) <= 10) /\ (10 <= (0 + nM^0)), par{bDomain^0 -> (0 + 0)}>
<l10, l2, ((1 + nN^0) <= 10) /\ ((1 + nD^0) <= 10) /\ ((1 + nM^0) <= 10) /\ (10 <= (0 + nO^0)), par{bDomain^0 -> (0 + 0)}>
<l10, l2, ((1 + nN^0) <= 10) /\ ((1 + nD^0) <= 10) /\ ((1 + nM^0) <= 10) /\ ((1 + nO^0) <= 10) /\ (10 <= (0 + nR^0)), par{bDomain^0 -> (0 + 0)}>
<l10, l2, ((1 + nN^0) <= 10) /\ ((1 + nD^0) <= 10) /\ ((1 + nM^0) <= 10) /\ ((1 + nO^0) <= 10) /\ ((1 + nR^0) <= 10) /\ (10 <= (0 + nY^0)), par{bDomain^0 -> (0 + 0)}>
<l10, l2, ((1 + nN^0) <= 10) /\ ((1 + nD^0) <= 10) /\ ((1 + nM^0) <= 10) /\ ((1 + nO^0) <= 10) /\ ((1 + nR^0) <= 10) /\ ((1 + nY^0) <= 10), par{bDomain^0 -> (0 + 1)}>
<l17, l2, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)) /\ (10 <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0), bDomain^0 -> (0 + 0)}>
<l17, l2, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)) /\ ((1 + nS^0) <= 10) /\ (10 <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0), bDomain^0 -> (0 + 0)}>
<l17, l10, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)) /\ ((1 + nS^0) <= 10) /\ ((1 + nE^0) <= 10), par{bAllDifferent^0 -> (0 + 0)}>
<l17, l2, (1 <= (0 + bAllDifferent^0)) /\ ((0 + nR^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nR^0)) /\ (10 <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0), bDomain^0 -> (0 + 0)}>
<l17, l2, (1 <= (0 + bAllDifferent^0)) /\ ((0 + nR^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nR^0)) /\ ((1 + nS^0) <= 10) /\ (10 <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0), bDomain^0 -> (0 + 0)}>
<l17, l10, (1 <= (0 + bAllDifferent^0)) /\ ((0 + nR^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nR^0)) /\ ((1 + nS^0) <= 10) /\ ((1 + nE^0) <= 10), par{bAllDifferent^0 -> (0 + 0)}>
<l17, l2, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nY^0) <= (0 + nR^0)) /\ (10 <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 1), bDomain^0 -> (0 + 0)}>
<l17, l2, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nY^0) <= (0 + nR^0)) /\ ((1 + nS^0) <= 10) /\ (10 <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 1), bDomain^0 -> (0 + 0)}>
<l17, l10, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nY^0) <= (0 + nR^0)) /\ ((1 + nS^0) <= 10) /\ ((1 + nE^0) <= 10), par{bAllDifferent^0 -> (0 + 1)}>
<l17, l2, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nR^0) <= (0 + nY^0)) /\ (10 <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 1), bDomain^0 -> (0 + 0)}>
<l17, l2, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nR^0) <= (0 + nY^0)) /\ ((1 + nS^0) <= 10) /\ (10 <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 1), bDomain^0 -> (0 + 0)}>
<l17, l10, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nR^0) <= (0 + nY^0)) /\ ((1 + nS^0) <= 10) /\ ((1 + nE^0) <= 10), par{bAllDifferent^0 -> (0 + 1)}>
<l17, l2, ((1 + bAllDifferent^0) <= 0) /\ ((0 + nR^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nR^0)) /\ (10 <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0), bDomain^0 -> (0 + 0)}>
<l17, l2, ((1 + bAllDifferent^0) <= 0) /\ ((0 + nR^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nR^0)) /\ ((1 + nS^0) <= 10) /\ (10 <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0), bDomain^0 -> (0 + 0)}>
<l17, l10, ((1 + bAllDifferent^0) <= 0) /\ ((0 + nR^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nR^0)) /\ ((1 + nS^0) <= 10) /\ ((1 + nE^0) <= 10), par{bAllDifferent^0 -> (0 + 0)}>
<l17, l2, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nY^0) <= (0 + nR^0)) /\ (10 <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 1), bDomain^0 -> (0 + 0)}>
<l17, l2, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nY^0) <= (0 + nR^0)) /\ ((1 + nS^0) <= 10) /\ (10 <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 1), bDomain^0 -> (0 + 0)}>
<l17, l10, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nY^0) <= (0 + nR^0)) /\ ((1 + nS^0) <= 10) /\ ((1 + nE^0) <= 10), par{bAllDifferent^0 -> (0 + 1)}>
<l17, l2, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nR^0) <= (0 + nY^0)) /\ (10 <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 1), bDomain^0 -> (0 + 0)}>
<l17, l2, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nR^0) <= (0 + nY^0)) /\ ((1 + nS^0) <= 10) /\ (10 <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 1), bDomain^0 -> (0 + 0)}>
<l17, l10, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nR^0) <= (0 + nY^0)) /\ ((1 + nS^0) <= 10) /\ ((1 + nE^0) <= 10), par{bAllDifferent^0 -> (0 + 1)}>
<l22, l5, ((0 + nS^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l22, l5, ((1 + nY^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l22, l5, ((1 + nS^0) <= (0 + nY^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l23, l17, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l23, l17, (1 <= (0 + bAllDifferent^0)) /\ ((0 + nO^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nO^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l23, l17, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nR^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nO^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l23, l17, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nR^0) <= (0 + nO^0)) /\ ((1 + nY^0) <= (0 + nO^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l23, l17, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nR^0) <= (0 + nO^0)) /\ ((1 + nO^0) <= (0 + nY^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l23, l17, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nO^0) <= (0 + nR^0)) /\ ((0 + nO^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nO^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l23, l17, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nO^0) <= (0 + nR^0)) /\ ((1 + nY^0) <= (0 + nO^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l23, l17, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nO^0) <= (0 + nR^0)) /\ ((1 + nO^0) <= (0 + nY^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l23, l17, ((1 + bAllDifferent^0) <= 0) /\ ((0 + nO^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nO^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l23, l17, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nR^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nO^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l23, l17, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nR^0) <= (0 + nO^0)) /\ ((1 + nY^0) <= (0 + nO^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l23, l17, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nR^0) <= (0 + nO^0)) /\ ((1 + nO^0) <= (0 + nY^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l23, l17, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nO^0) <= (0 + nR^0)) /\ ((0 + nO^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nO^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l23, l17, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nO^0) <= (0 + nR^0)) /\ ((1 + nY^0) <= (0 + nO^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l23, l17, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nO^0) <= (0 + nR^0)) /\ ((1 + nO^0) <= (0 + nY^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l26, l23, ((0 + nM^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nM^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l26, l23, ((1 + nY^0) <= (0 + nM^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l26, l23, ((1 + nM^0) <= (0 + nY^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l30, l23, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l30, l23, (1 <= (0 + bAllDifferent^0)) /\ ((0 + nM^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nM^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l30, l23, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nO^0) <= (0 + nM^0)) /\ ((0 + nM^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nM^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l30, l26, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nO^0) <= (0 + nM^0)) /\ ((1 + nR^0) <= (0 + nM^0))>
<l30, l26, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nO^0) <= (0 + nM^0)) /\ ((1 + nM^0) <= (0 + nR^0))>
<l30, l23, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nM^0) <= (0 + nO^0)) /\ ((0 + nM^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nM^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l30, l26, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nM^0) <= (0 + nO^0)) /\ ((1 + nR^0) <= (0 + nM^0))>
<l30, l26, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nM^0) <= (0 + nO^0)) /\ ((1 + nM^0) <= (0 + nR^0))>
<l30, l23, ((1 + bAllDifferent^0) <= 0) /\ ((0 + nM^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nM^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l30, l23, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nO^0) <= (0 + nM^0)) /\ ((0 + nM^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nM^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l30, l26, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nO^0) <= (0 + nM^0)) /\ ((1 + nR^0) <= (0 + nM^0))>
<l30, l26, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nO^0) <= (0 + nM^0)) /\ ((1 + nM^0) <= (0 + nR^0))>
<l30, l23, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nM^0) <= (0 + nO^0)) /\ ((0 + nM^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nM^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l30, l26, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nM^0) <= (0 + nO^0)) /\ ((1 + nR^0) <= (0 + nM^0))>
<l30, l26, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nM^0) <= (0 + nO^0)) /\ ((1 + nM^0) <= (0 + nR^0))>
<l34, l30, ((0 + nD^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nD^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l34, l30, ((1 + nR^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nD^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l34, l30, ((1 + nR^0) <= (0 + nD^0)) /\ ((1 + nY^0) <= (0 + nD^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l34, l30, ((1 + nR^0) <= (0 + nD^0)) /\ ((1 + nD^0) <= (0 + nY^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l34, l30, ((1 + nD^0) <= (0 + nR^0)) /\ ((0 + nD^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nD^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l34, l30, ((1 + nD^0) <= (0 + nR^0)) /\ ((1 + nY^0) <= (0 + nD^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l34, l30, ((1 + nD^0) <= (0 + nR^0)) /\ ((1 + nD^0) <= (0 + nY^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l38, l30, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l38, l30, (1 <= (0 + bAllDifferent^0)) /\ ((0 + nD^0) <= (0 + nM^0)) /\ ((0 + nM^0) <= (0 + nD^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l38, l30, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nM^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nD^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l38, l34, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nM^0) <= (0 + nD^0)) /\ ((1 + nO^0) <= (0 + nD^0))>
<l38, l34, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nM^0) <= (0 + nD^0)) /\ ((1 + nD^0) <= (0 + nO^0))>
<l38, l30, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nD^0) <= (0 + nM^0)) /\ ((0 + nD^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nD^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l38, l34, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nD^0) <= (0 + nM^0)) /\ ((1 + nO^0) <= (0 + nD^0))>
<l38, l34, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nD^0) <= (0 + nM^0)) /\ ((1 + nD^0) <= (0 + nO^0))>
<l38, l30, ((1 + bAllDifferent^0) <= 0) /\ ((0 + nD^0) <= (0 + nM^0)) /\ ((0 + nM^0) <= (0 + nD^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l38, l30, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nM^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nD^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l38, l34, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nM^0) <= (0 + nD^0)) /\ ((1 + nO^0) <= (0 + nD^0))>
<l38, l34, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nM^0) <= (0 + nD^0)) /\ ((1 + nD^0) <= (0 + nO^0))>
<l38, l30, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nD^0) <= (0 + nM^0)) /\ ((0 + nD^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nD^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l38, l34, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nD^0) <= (0 + nM^0)) /\ ((1 + nO^0) <= (0 + nD^0))>
<l38, l34, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nD^0) <= (0 + nM^0)) /\ ((1 + nD^0) <= (0 + nO^0))>
<l40, l5, ((0 + nS^0) <= (0 + nM^0)) /\ ((0 + nM^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l40, l5, ((1 + nM^0) <= (0 + nS^0)) /\ ((0 + nS^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l40, l5, ((1 + nM^0) <= (0 + nS^0)) /\ ((1 + nO^0) <= (0 + nS^0)) /\ ((0 + nS^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l40, l22, ((1 + nM^0) <= (0 + nS^0)) /\ ((1 + nO^0) <= (0 + nS^0)) /\ ((1 + nR^0) <= (0 + nS^0))>
<l40, l22, ((1 + nM^0) <= (0 + nS^0)) /\ ((1 + nO^0) <= (0 + nS^0)) /\ ((1 + nS^0) <= (0 + nR^0))>
<l40, l5, ((1 + nM^0) <= (0 + nS^0)) /\ ((1 + nS^0) <= (0 + nO^0)) /\ ((0 + nS^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l40, l22, ((1 + nM^0) <= (0 + nS^0)) /\ ((1 + nS^0) <= (0 + nO^0)) /\ ((1 + nR^0) <= (0 + nS^0))>
<l40, l22, ((1 + nM^0) <= (0 + nS^0)) /\ ((1 + nS^0) <= (0 + nO^0)) /\ ((1 + nS^0) <= (0 + nR^0))>
<l40, l5, ((1 + nS^0) <= (0 + nM^0)) /\ ((0 + nS^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l40, l5, ((1 + nS^0) <= (0 + nM^0)) /\ ((1 + nO^0) <= (0 + nS^0)) /\ ((0 + nS^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l40, l22, ((1 + nS^0) <= (0 + nM^0)) /\ ((1 + nO^0) <= (0 + nS^0)) /\ ((1 + nR^0) <= (0 + nS^0))>
<l40, l22, ((1 + nS^0) <= (0 + nM^0)) /\ ((1 + nO^0) <= (0 + nS^0)) /\ ((1 + nS^0) <= (0 + nR^0))>
<l40, l5, ((1 + nS^0) <= (0 + nM^0)) /\ ((1 + nS^0) <= (0 + nO^0)) /\ ((0 + nS^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nS^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l40, l22, ((1 + nS^0) <= (0 + nM^0)) /\ ((1 + nS^0) <= (0 + nO^0)) /\ ((1 + nR^0) <= (0 + nS^0))>
<l40, l22, ((1 + nS^0) <= (0 + nM^0)) /\ ((1 + nS^0) <= (0 + nO^0)) /\ ((1 + nS^0) <= (0 + nR^0))>
<l44, l38, ((0 + nN^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l44, l38, ((1 + nO^0) <= (0 + nN^0)) /\ ((0 + nN^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l44, l38, ((1 + nO^0) <= (0 + nN^0)) /\ ((1 + nR^0) <= (0 + nN^0)) /\ ((0 + nN^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l44, l38, ((1 + nO^0) <= (0 + nN^0)) /\ ((1 + nR^0) <= (0 + nN^0)) /\ ((1 + nY^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l44, l38, ((1 + nO^0) <= (0 + nN^0)) /\ ((1 + nR^0) <= (0 + nN^0)) /\ ((1 + nN^0) <= (0 + nY^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l44, l38, ((1 + nO^0) <= (0 + nN^0)) /\ ((1 + nN^0) <= (0 + nR^0)) /\ ((0 + nN^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l44, l38, ((1 + nO^0) <= (0 + nN^0)) /\ ((1 + nN^0) <= (0 + nR^0)) /\ ((1 + nY^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l44, l38, ((1 + nO^0) <= (0 + nN^0)) /\ ((1 + nN^0) <= (0 + nR^0)) /\ ((1 + nN^0) <= (0 + nY^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l44, l38, ((1 + nN^0) <= (0 + nO^0)) /\ ((0 + nN^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l44, l38, ((1 + nN^0) <= (0 + nO^0)) /\ ((1 + nR^0) <= (0 + nN^0)) /\ ((0 + nN^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l44, l38, ((1 + nN^0) <= (0 + nO^0)) /\ ((1 + nR^0) <= (0 + nN^0)) /\ ((1 + nY^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l44, l38, ((1 + nN^0) <= (0 + nO^0)) /\ ((1 + nR^0) <= (0 + nN^0)) /\ ((1 + nN^0) <= (0 + nY^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l44, l38, ((1 + nN^0) <= (0 + nO^0)) /\ ((1 + nN^0) <= (0 + nR^0)) /\ ((0 + nN^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l44, l38, ((1 + nN^0) <= (0 + nO^0)) /\ ((1 + nN^0) <= (0 + nR^0)) /\ ((1 + nY^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l44, l38, ((1 + nN^0) <= (0 + nO^0)) /\ ((1 + nN^0) <= (0 + nR^0)) /\ ((1 + nN^0) <= (0 + nY^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l47, l38, ((0 + bAllDifferent^0) <= 0) /\ (0 <= (0 + bAllDifferent^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l47, l38, (1 <= (0 + bAllDifferent^0)) /\ ((0 + nN^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l47, l38, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nD^0) <= (0 + nN^0)) /\ ((0 + nN^0) <= (0 + nM^0)) /\ ((0 + nM^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l47, l44, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nD^0) <= (0 + nN^0)) /\ ((1 + nM^0) <= (0 + nN^0))>
<l47, l44, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nD^0) <= (0 + nN^0)) /\ ((1 + nN^0) <= (0 + nM^0))>
<l47, l38, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nN^0) <= (0 + nD^0)) /\ ((0 + nN^0) <= (0 + nM^0)) /\ ((0 + nM^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l47, l44, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nN^0) <= (0 + nD^0)) /\ ((1 + nM^0) <= (0 + nN^0))>
<l47, l44, (1 <= (0 + bAllDifferent^0)) /\ ((1 + nN^0) <= (0 + nD^0)) /\ ((1 + nN^0) <= (0 + nM^0))>
<l47, l38, ((1 + bAllDifferent^0) <= 0) /\ ((0 + nN^0) <= (0 + nD^0)) /\ ((0 + nD^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l47, l38, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nD^0) <= (0 + nN^0)) /\ ((0 + nN^0) <= (0 + nM^0)) /\ ((0 + nM^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l47, l44, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nD^0) <= (0 + nN^0)) /\ ((1 + nM^0) <= (0 + nN^0))>
<l47, l44, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nD^0) <= (0 + nN^0)) /\ ((1 + nN^0) <= (0 + nM^0))>
<l47, l38, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nN^0) <= (0 + nD^0)) /\ ((0 + nN^0) <= (0 + nM^0)) /\ ((0 + nM^0) <= (0 + nN^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l47, l44, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nN^0) <= (0 + nD^0)) /\ ((1 + nM^0) <= (0 + nN^0))>
<l47, l44, ((1 + bAllDifferent^0) <= 0) /\ ((1 + nN^0) <= (0 + nD^0)) /\ ((1 + nN^0) <= (0 + nM^0))>
<l51, l47, ((0 + nE^0) <= (0 + nY^0)) /\ ((0 + nY^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l51, l47, ((1 + nY^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l51, l47, ((1 + nE^0) <= (0 + nY^0)), par{bAllDifferent^0 -> (0 + 1)}>
<l54, l47, ((0 + nE^0) <= (0 + nM^0)) /\ ((0 + nM^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l54, l47, ((1 + nM^0) <= (0 + nE^0)) /\ ((0 + nE^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l54, l47, ((1 + nM^0) <= (0 + nE^0)) /\ ((1 + nO^0) <= (0 + nE^0)) /\ ((0 + nE^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l54, l51, ((1 + nM^0) <= (0 + nE^0)) /\ ((1 + nO^0) <= (0 + nE^0)) /\ ((1 + nR^0) <= (0 + nE^0))>
<l54, l51, ((1 + nM^0) <= (0 + nE^0)) /\ ((1 + nO^0) <= (0 + nE^0)) /\ ((1 + nE^0) <= (0 + nR^0))>
<l54, l47, ((1 + nM^0) <= (0 + nE^0)) /\ ((1 + nE^0) <= (0 + nO^0)) /\ ((0 + nE^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l54, l51, ((1 + nM^0) <= (0 + nE^0)) /\ ((1 + nE^0) <= (0 + nO^0)) /\ ((1 + nR^0) <= (0 + nE^0))>
<l54, l51, ((1 + nM^0) <= (0 + nE^0)) /\ ((1 + nE^0) <= (0 + nO^0)) /\ ((1 + nE^0) <= (0 + nR^0))>
<l54, l47, ((1 + nE^0) <= (0 + nM^0)) /\ ((0 + nE^0) <= (0 + nO^0)) /\ ((0 + nO^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l54, l47, ((1 + nE^0) <= (0 + nM^0)) /\ ((1 + nO^0) <= (0 + nE^0)) /\ ((0 + nE^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l54, l51, ((1 + nE^0) <= (0 + nM^0)) /\ ((1 + nO^0) <= (0 + nE^0)) /\ ((1 + nR^0) <= (0 + nE^0))>
<l54, l51, ((1 + nE^0) <= (0 + nM^0)) /\ ((1 + nO^0) <= (0 + nE^0)) /\ ((1 + nE^0) <= (0 + nR^0))>
<l54, l47, ((1 + nE^0) <= (0 + nM^0)) /\ ((1 + nE^0) <= (0 + nO^0)) /\ ((0 + nE^0) <= (0 + nR^0)) /\ ((0 + nR^0) <= (0 + nE^0)), par{bAllDifferent^0 -> (0 + 0)}>
<l54, l51, ((1 + nE^0) <= (0 + nM^0)) /\ ((1 + nE^0) <= (0 + nO^0)) /\ ((1 + nR^0) <= (0 + nE^0))>
<l54, l51, ((1 + nE^0) <= (0 + nM^0)) /\ ((1 + nE^0) <= (0 + nO^0)) /\ ((1 + nE^0) <= (0 + nR^0))>
<l63, l59, ((0 + bDomain^0) <= 0) /\ (0 <= (0 + bDomain^0))>
<l63, l59, (1 <= (0 + bDomain^0)) /\ ((0 + bNoLeadingZeros^0) <= 0) /\ (0 <= (0 + bNoLeadingZeros^0))>
<l63, l59, (1 <= (0 + bDomain^0)) /\ (1 <= (0 + bNoLeadingZeros^0)) /\ ((0 + bSum^0) <= 0) /\ (0 <= (0 + bSum^0))>
<l63, l59, (1 <= (0 + bDomain^0)) /\ (1 <= (0 + bNoLeadingZeros^0)) /\ (1 <= (0 + bSum^0))>
<l63, l59, (1 <= (0 + bDomain^0)) /\ (1 <= (0 + bNoLeadingZeros^0)) /\ ((1 + bSum^0) <= 0)>
<l63, l59, (1 <= (0 + bDomain^0)) /\ ((1 + bNoLeadingZeros^0) <= 0) /\ ((0 + bSum^0) <= 0) /\ (0 <= (0 + bSum^0))>
<l63, l59, (1 <= (0 + bDomain^0)) /\ ((1 + bNoLeadingZeros^0) <= 0) /\ (1 <= (0 + bSum^0))>
<l63, l59, (1 <= (0 + bDomain^0)) /\ ((1 + bNoLeadingZeros^0) <= 0) /\ ((1 + bSum^0) <= 0)>
<l63, l59, ((1 + bDomain^0) <= 0) /\ ((0 + bNoLeadingZeros^0) <= 0) /\ (0 <= (0 + bNoLeadingZeros^0))>
<l63, l59, ((1 + bDomain^0) <= 0) /\ (1 <= (0 + bNoLeadingZeros^0)) /\ ((0 + bSum^0) <= 0) /\ (0 <= (0 + bSum^0))>
<l63, l59, ((1 + bDomain^0) <= 0) /\ (1 <= (0 + bNoLeadingZeros^0)) /\ (1 <= (0 + bSum^0))>
<l63, l59, ((1 + bDomain^0) <= 0) /\ (1 <= (0 + bNoLeadingZeros^0)) /\ ((1 + bSum^0) <= 0)>
<l63, l59, ((1 + bDomain^0) <= 0) /\ ((1 + bNoLeadingZeros^0) <= 0) /\ ((0 + bSum^0) <= 0) /\ (0 <= (0 + bSum^0))>
<l63, l59, ((1 + bDomain^0) <= 0) /\ ((1 + bNoLeadingZeros^0) <= 0) /\ (1 <= (0 + bSum^0))>
<l63, l59, ((1 + bDomain^0) <= 0) /\ ((1 + bNoLeadingZeros^0) <= 0) /\ ((1 + bSum^0) <= 0)>

Fresh variables:
undef3172, 

Undef variables:
undef3172, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

*************************************************************
*******************************************************************************************
***********************       WORKING TRANSITION SYSTEM (DAG)       ***********************
*******************************************************************************************

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
Variables:

Graph 2:
Transitions:
Variables:

Graph 3:
Transitions:
Variables:

Graph 4:
Transitions:
Variables:

Graph 5:
Transitions:
Variables:

Graph 6:
Transitions:
Variables:

Graph 7:
Transitions:
Variables:

Graph 8:
Transitions:
Variables:

Graph 9:
Transitions:
Variables:

Graph 10:
Transitions:
Variables:

Graph 11:
Transitions:
Variables:

Graph 12:
Transitions:
Variables:

Graph 13:
Transitions:
Variables:

Graph 14:
Transitions:
Variables:

Graph 15:
Transitions:
Variables:

Graph 16:
Transitions:
Variables:

Graph 17:
Transitions:
Variables:

Precedence: 
Graph 0

Graph 1
<l0, l40, 1 + nD^0 <= nS^0 /\ 1 + nE^0 <= nS^0 /\ 1 + nN^0 <= nS^0, {all remain the same}>
<l0, l40, 1 + nS^0 <= nD^0 /\ 1 + nE^0 <= nS^0 /\ 1 + nN^0 <= nS^0, {all remain the same}>
<l0, l40, 1 + nD^0 <= nS^0 /\ 1 + nE^0 <= nS^0 /\ 1 + nS^0 <= nN^0, {all remain the same}>
<l0, l40, 1 + nS^0 <= nD^0 /\ 1 + nE^0 <= nS^0 /\ 1 + nS^0 <= nN^0, {all remain the same}>
<l0, l40, 1 + nD^0 <= nS^0 /\ 1 + nS^0 <= nE^0 /\ 1 + nN^0 <= nS^0, {all remain the same}>
<l0, l40, 1 + nS^0 <= nD^0 /\ 1 + nS^0 <= nE^0 /\ 1 + nN^0 <= nS^0, {all remain the same}>
<l0, l40, 1 + nD^0 <= nS^0 /\ 1 + nS^0 <= nE^0 /\ 1 + nS^0 <= nN^0, {all remain the same}>
<l0, l40, 1 + nS^0 <= nD^0 /\ 1 + nS^0 <= nE^0 /\ 1 + nS^0 <= nN^0, {all remain the same}>

Graph 2
<l40, l22, 1 + nM^0 <= nS^0 /\ 1 + nO^0 <= nS^0 /\ 1 + nR^0 <= nS^0, {all remain the same}>
<l40, l22, 1 + nM^0 <= nS^0 /\ 1 + nO^0 <= nS^0 /\ 1 + nS^0 <= nR^0, {all remain the same}>
<l40, l22, 1 + nM^0 <= nS^0 /\ 1 + nS^0 <= nO^0 /\ 1 + nR^0 <= nS^0, {all remain the same}>
<l40, l22, 1 + nM^0 <= nS^0 /\ 1 + nS^0 <= nO^0 /\ 1 + nS^0 <= nR^0, {all remain the same}>
<l40, l22, 1 + nS^0 <= nM^0 /\ 1 + nO^0 <= nS^0 /\ 1 + nR^0 <= nS^0, {all remain the same}>
<l40, l22, 1 + nS^0 <= nM^0 /\ 1 + nO^0 <= nS^0 /\ 1 + nS^0 <= nR^0, {all remain the same}>
<l40, l22, 1 + nS^0 <= nM^0 /\ 1 + nS^0 <= nO^0 /\ 1 + nR^0 <= nS^0, {all remain the same}>
<l40, l22, 1 + nS^0 <= nM^0 /\ 1 + nS^0 <= nO^0 /\ 1 + nS^0 <= nR^0, {all remain the same}>

Graph 3
<l0, l5, nE^0 = nS^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l0, l5, 1 + nE^0 <= nS^0 /\ nN^0 = nS^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l0, l5, 1 + nE^0 <= nS^0 /\ 1 + nN^0 <= nS^0 /\ nD^0 = nS^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l0, l5, 1 + nE^0 <= nS^0 /\ 1 + nS^0 <= nN^0 /\ nD^0 = nS^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l0, l5, 1 + nS^0 <= nE^0 /\ nN^0 = nS^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l0, l5, 1 + nS^0 <= nE^0 /\ 1 + nN^0 <= nS^0 /\ nD^0 = nS^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l0, l5, 1 + nS^0 <= nE^0 /\ 1 + nS^0 <= nN^0 /\ nD^0 = nS^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l22, l5, nS^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l22, l5, 1 + nY^0 <= nS^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l22, l5, 1 + nS^0 <= nY^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l40, l5, nM^0 = nS^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l40, l5, 1 + nM^0 <= nS^0 /\ nO^0 = nS^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l40, l5, 1 + nM^0 <= nS^0 /\ 1 + nO^0 <= nS^0 /\ nR^0 = nS^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l40, l5, 1 + nM^0 <= nS^0 /\ 1 + nS^0 <= nO^0 /\ nR^0 = nS^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l40, l5, 1 + nS^0 <= nM^0 /\ nO^0 = nS^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l40, l5, 1 + nS^0 <= nM^0 /\ 1 + nO^0 <= nS^0 /\ nR^0 = nS^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l40, l5, 1 + nS^0 <= nM^0 /\ 1 + nS^0 <= nO^0 /\ nR^0 = nS^0, {bAllDifferent^0 -> 0, rest remain the same}>

Graph 4
<l5, l54, 1 <= bAllDifferent^0 /\ 1 + nD^0 <= nE^0 /\ 1 + nN^0 <= nE^0, {all remain the same}>
<l5, l54, 1 <= bAllDifferent^0 /\ 1 + nE^0 <= nD^0 /\ 1 + nN^0 <= nE^0, {all remain the same}>
<l5, l54, 1 <= bAllDifferent^0 /\ 1 + nD^0 <= nE^0 /\ 1 + nE^0 <= nN^0, {all remain the same}>
<l5, l54, 1 <= bAllDifferent^0 /\ 1 + nE^0 <= nD^0 /\ 1 + nE^0 <= nN^0, {all remain the same}>
<l5, l54, 1 + bAllDifferent^0 <= 0 /\ 1 + nD^0 <= nE^0 /\ 1 + nN^0 <= nE^0, {all remain the same}>
<l5, l54, 1 + bAllDifferent^0 <= 0 /\ 1 + nE^0 <= nD^0 /\ 1 + nN^0 <= nE^0, {all remain the same}>
<l5, l54, 1 + bAllDifferent^0 <= 0 /\ 1 + nD^0 <= nE^0 /\ 1 + nE^0 <= nN^0, {all remain the same}>
<l5, l54, 1 + bAllDifferent^0 <= 0 /\ 1 + nE^0 <= nD^0 /\ 1 + nE^0 <= nN^0, {all remain the same}>

Graph 5
<l54, l51, 1 + nM^0 <= nE^0 /\ 1 + nO^0 <= nE^0 /\ 1 + nR^0 <= nE^0, {all remain the same}>
<l54, l51, 1 + nE^0 <= nR^0 /\ 1 + nM^0 <= nE^0 /\ 1 + nO^0 <= nE^0, {all remain the same}>
<l54, l51, 1 + nE^0 <= nO^0 /\ 1 + nM^0 <= nE^0 /\ 1 + nR^0 <= nE^0, {all remain the same}>
<l54, l51, 1 + nE^0 <= nO^0 /\ 1 + nE^0 <= nR^0 /\ 1 + nM^0 <= nE^0, {all remain the same}>
<l54, l51, 1 + nE^0 <= nM^0 /\ 1 + nO^0 <= nE^0 /\ 1 + nR^0 <= nE^0, {all remain the same}>
<l54, l51, 1 + nE^0 <= nM^0 /\ 1 + nE^0 <= nR^0 /\ 1 + nO^0 <= nE^0, {all remain the same}>
<l54, l51, 1 + nE^0 <= nM^0 /\ 1 + nE^0 <= nO^0 /\ 1 + nR^0 <= nE^0, {all remain the same}>
<l54, l51, 1 + nE^0 <= nM^0 /\ 1 + nE^0 <= nO^0 /\ 1 + nE^0 <= nR^0, {all remain the same}>

Graph 6
<l5, l47, bAllDifferent^0 = 0, {bAllDifferent^0 -> 0, rest remain the same}>
<l5, l47, 1 <= bAllDifferent^0 /\ nE^0 = nN^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l5, l47, 1 <= bAllDifferent^0 /\ 1 + nN^0 <= nE^0 /\ nD^0 = nE^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l5, l47, 1 <= bAllDifferent^0 /\ 1 + nE^0 <= nN^0 /\ nD^0 = nE^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l5, l47, 1 + bAllDifferent^0 <= 0 /\ nE^0 = nN^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l5, l47, 1 + bAllDifferent^0 <= 0 /\ 1 + nN^0 <= nE^0 /\ nD^0 = nE^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l5, l47, 1 + bAllDifferent^0 <= 0 /\ 1 + nE^0 <= nN^0 /\ nD^0 = nE^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l51, l47, nE^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l51, l47, 1 + nY^0 <= nE^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l51, l47, 1 + nE^0 <= nY^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l54, l47, nE^0 = nM^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l54, l47, 1 + nM^0 <= nE^0 /\ nE^0 = nO^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l54, l47, 1 + nM^0 <= nE^0 /\ 1 + nO^0 <= nE^0 /\ nE^0 = nR^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l54, l47, 1 + nE^0 <= nO^0 /\ 1 + nM^0 <= nE^0 /\ nE^0 = nR^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l54, l47, 1 + nE^0 <= nM^0 /\ nE^0 = nO^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l54, l47, 1 + nE^0 <= nM^0 /\ 1 + nO^0 <= nE^0 /\ nE^0 = nR^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l54, l47, 1 + nE^0 <= nM^0 /\ 1 + nE^0 <= nO^0 /\ nE^0 = nR^0, {bAllDifferent^0 -> 0, rest remain the same}>

Graph 7
<l47, l44, 1 <= bAllDifferent^0 /\ 1 + nD^0 <= nN^0 /\ 1 + nM^0 <= nN^0, {all remain the same}>
<l47, l44, 1 <= bAllDifferent^0 /\ 1 + nD^0 <= nN^0 /\ 1 + nN^0 <= nM^0, {all remain the same}>
<l47, l44, 1 <= bAllDifferent^0 /\ 1 + nN^0 <= nD^0 /\ 1 + nM^0 <= nN^0, {all remain the same}>
<l47, l44, 1 <= bAllDifferent^0 /\ 1 + nN^0 <= nD^0 /\ 1 + nN^0 <= nM^0, {all remain the same}>
<l47, l44, 1 + bAllDifferent^0 <= 0 /\ 1 + nD^0 <= nN^0 /\ 1 + nM^0 <= nN^0, {all remain the same}>
<l47, l44, 1 + bAllDifferent^0 <= 0 /\ 1 + nD^0 <= nN^0 /\ 1 + nN^0 <= nM^0, {all remain the same}>
<l47, l44, 1 + bAllDifferent^0 <= 0 /\ 1 + nN^0 <= nD^0 /\ 1 + nM^0 <= nN^0, {all remain the same}>
<l47, l44, 1 + bAllDifferent^0 <= 0 /\ 1 + nN^0 <= nD^0 /\ 1 + nN^0 <= nM^0, {all remain the same}>

Graph 8
<l44, l38, nN^0 = nO^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l44, l38, 1 + nO^0 <= nN^0 /\ nN^0 = nR^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l44, l38, 1 + nO^0 <= nN^0 /\ 1 + nR^0 <= nN^0 /\ nN^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l44, l38, 1 + nO^0 <= nN^0 /\ 1 + nR^0 <= nN^0 /\ 1 + nY^0 <= nN^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l44, l38, 1 + nN^0 <= nY^0 /\ 1 + nO^0 <= nN^0 /\ 1 + nR^0 <= nN^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l44, l38, 1 + nN^0 <= nR^0 /\ 1 + nO^0 <= nN^0 /\ nN^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l44, l38, 1 + nN^0 <= nR^0 /\ 1 + nO^0 <= nN^0 /\ 1 + nY^0 <= nN^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l44, l38, 1 + nN^0 <= nR^0 /\ 1 + nN^0 <= nY^0 /\ 1 + nO^0 <= nN^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l44, l38, 1 + nN^0 <= nO^0 /\ nN^0 = nR^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l44, l38, 1 + nN^0 <= nO^0 /\ 1 + nR^0 <= nN^0 /\ nN^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l44, l38, 1 + nN^0 <= nO^0 /\ 1 + nR^0 <= nN^0 /\ 1 + nY^0 <= nN^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l44, l38, 1 + nN^0 <= nO^0 /\ 1 + nN^0 <= nY^0 /\ 1 + nR^0 <= nN^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l44, l38, 1 + nN^0 <= nO^0 /\ 1 + nN^0 <= nR^0 /\ nN^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l44, l38, 1 + nN^0 <= nO^0 /\ 1 + nN^0 <= nR^0 /\ 1 + nY^0 <= nN^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l44, l38, 1 + nN^0 <= nO^0 /\ 1 + nN^0 <= nR^0 /\ 1 + nN^0 <= nY^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l47, l38, bAllDifferent^0 = 0, {bAllDifferent^0 -> 0, rest remain the same}>
<l47, l38, 1 <= bAllDifferent^0 /\ nD^0 = nN^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l47, l38, 1 <= bAllDifferent^0 /\ 1 + nD^0 <= nN^0 /\ nM^0 = nN^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l47, l38, 1 <= bAllDifferent^0 /\ 1 + nN^0 <= nD^0 /\ nM^0 = nN^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l47, l38, 1 + bAllDifferent^0 <= 0 /\ nD^0 = nN^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l47, l38, 1 + bAllDifferent^0 <= 0 /\ 1 + nD^0 <= nN^0 /\ nM^0 = nN^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l47, l38, 1 + bAllDifferent^0 <= 0 /\ 1 + nN^0 <= nD^0 /\ nM^0 = nN^0, {bAllDifferent^0 -> 0, rest remain the same}>

Graph 9
<l38, l34, 1 <= bAllDifferent^0 /\ 1 + nM^0 <= nD^0 /\ 1 + nO^0 <= nD^0, {all remain the same}>
<l38, l34, 1 <= bAllDifferent^0 /\ 1 + nD^0 <= nO^0 /\ 1 + nM^0 <= nD^0, {all remain the same}>
<l38, l34, 1 <= bAllDifferent^0 /\ 1 + nD^0 <= nM^0 /\ 1 + nO^0 <= nD^0, {all remain the same}>
<l38, l34, 1 <= bAllDifferent^0 /\ 1 + nD^0 <= nM^0 /\ 1 + nD^0 <= nO^0, {all remain the same}>
<l38, l34, 1 + bAllDifferent^0 <= 0 /\ 1 + nM^0 <= nD^0 /\ 1 + nO^0 <= nD^0, {all remain the same}>
<l38, l34, 1 + bAllDifferent^0 <= 0 /\ 1 + nD^0 <= nO^0 /\ 1 + nM^0 <= nD^0, {all remain the same}>
<l38, l34, 1 + bAllDifferent^0 <= 0 /\ 1 + nD^0 <= nM^0 /\ 1 + nO^0 <= nD^0, {all remain the same}>
<l38, l34, 1 + bAllDifferent^0 <= 0 /\ 1 + nD^0 <= nM^0 /\ 1 + nD^0 <= nO^0, {all remain the same}>

Graph 10
<l34, l30, nD^0 = nR^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l34, l30, 1 + nR^0 <= nD^0 /\ nD^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l34, l30, 1 + nR^0 <= nD^0 /\ 1 + nY^0 <= nD^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l34, l30, 1 + nD^0 <= nY^0 /\ 1 + nR^0 <= nD^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l34, l30, 1 + nD^0 <= nR^0 /\ nD^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l34, l30, 1 + nD^0 <= nR^0 /\ 1 + nY^0 <= nD^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l34, l30, 1 + nD^0 <= nR^0 /\ 1 + nD^0 <= nY^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l38, l30, bAllDifferent^0 = 0, {bAllDifferent^0 -> 0, rest remain the same}>
<l38, l30, 1 <= bAllDifferent^0 /\ nD^0 = nM^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l38, l30, 1 <= bAllDifferent^0 /\ 1 + nM^0 <= nD^0 /\ nD^0 = nO^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l38, l30, 1 <= bAllDifferent^0 /\ 1 + nD^0 <= nM^0 /\ nD^0 = nO^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l38, l30, 1 + bAllDifferent^0 <= 0 /\ nD^0 = nM^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l38, l30, 1 + bAllDifferent^0 <= 0 /\ 1 + nM^0 <= nD^0 /\ nD^0 = nO^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l38, l30, 1 + bAllDifferent^0 <= 0 /\ 1 + nD^0 <= nM^0 /\ nD^0 = nO^0, {bAllDifferent^0 -> 0, rest remain the same}>

Graph 11
<l30, l26, 1 <= bAllDifferent^0 /\ 1 + nO^0 <= nM^0 /\ 1 + nR^0 <= nM^0, {all remain the same}>
<l30, l26, 1 <= bAllDifferent^0 /\ 1 + nM^0 <= nR^0 /\ 1 + nO^0 <= nM^0, {all remain the same}>
<l30, l26, 1 <= bAllDifferent^0 /\ 1 + nM^0 <= nO^0 /\ 1 + nR^0 <= nM^0, {all remain the same}>
<l30, l26, 1 <= bAllDifferent^0 /\ 1 + nM^0 <= nO^0 /\ 1 + nM^0 <= nR^0, {all remain the same}>
<l30, l26, 1 + bAllDifferent^0 <= 0 /\ 1 + nO^0 <= nM^0 /\ 1 + nR^0 <= nM^0, {all remain the same}>
<l30, l26, 1 + bAllDifferent^0 <= 0 /\ 1 + nM^0 <= nR^0 /\ 1 + nO^0 <= nM^0, {all remain the same}>
<l30, l26, 1 + bAllDifferent^0 <= 0 /\ 1 + nM^0 <= nO^0 /\ 1 + nR^0 <= nM^0, {all remain the same}>
<l30, l26, 1 + bAllDifferent^0 <= 0 /\ 1 + nM^0 <= nO^0 /\ 1 + nM^0 <= nR^0, {all remain the same}>

Graph 12
<l26, l23, nM^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l26, l23, 1 + nY^0 <= nM^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l26, l23, 1 + nM^0 <= nY^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l30, l23, bAllDifferent^0 = 0, {bAllDifferent^0 -> 0, rest remain the same}>
<l30, l23, 1 <= bAllDifferent^0 /\ nM^0 = nO^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l30, l23, 1 <= bAllDifferent^0 /\ 1 + nO^0 <= nM^0 /\ nM^0 = nR^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l30, l23, 1 <= bAllDifferent^0 /\ 1 + nM^0 <= nO^0 /\ nM^0 = nR^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l30, l23, 1 + bAllDifferent^0 <= 0 /\ nM^0 = nO^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l30, l23, 1 + bAllDifferent^0 <= 0 /\ 1 + nO^0 <= nM^0 /\ nM^0 = nR^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l30, l23, 1 + bAllDifferent^0 <= 0 /\ 1 + nM^0 <= nO^0 /\ nM^0 = nR^0, {bAllDifferent^0 -> 0, rest remain the same}>

Graph 13
<l23, l17, bAllDifferent^0 = 0, {bAllDifferent^0 -> 0, rest remain the same}>
<l23, l17, 1 <= bAllDifferent^0 /\ nO^0 = nR^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l23, l17, 1 <= bAllDifferent^0 /\ 1 + nR^0 <= nO^0 /\ nO^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l23, l17, 1 <= bAllDifferent^0 /\ 1 + nR^0 <= nO^0 /\ 1 + nY^0 <= nO^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l23, l17, 1 <= bAllDifferent^0 /\ 1 + nO^0 <= nY^0 /\ 1 + nR^0 <= nO^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l23, l17, 1 <= bAllDifferent^0 /\ 1 + nO^0 <= nR^0 /\ nO^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l23, l17, 1 <= bAllDifferent^0 /\ 1 + nO^0 <= nR^0 /\ 1 + nY^0 <= nO^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l23, l17, 1 <= bAllDifferent^0 /\ 1 + nO^0 <= nR^0 /\ 1 + nO^0 <= nY^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l23, l17, 1 + bAllDifferent^0 <= 0 /\ nO^0 = nR^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l23, l17, 1 + bAllDifferent^0 <= 0 /\ 1 + nR^0 <= nO^0 /\ nO^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l23, l17, 1 + bAllDifferent^0 <= 0 /\ 1 + nR^0 <= nO^0 /\ 1 + nY^0 <= nO^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l23, l17, 1 + bAllDifferent^0 <= 0 /\ 1 + nO^0 <= nY^0 /\ 1 + nR^0 <= nO^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l23, l17, 1 + bAllDifferent^0 <= 0 /\ 1 + nO^0 <= nR^0 /\ nO^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l23, l17, 1 + bAllDifferent^0 <= 0 /\ 1 + nO^0 <= nR^0 /\ 1 + nY^0 <= nO^0, {bAllDifferent^0 -> 1, rest remain the same}>
<l23, l17, 1 + bAllDifferent^0 <= 0 /\ 1 + nO^0 <= nR^0 /\ 1 + nO^0 <= nY^0, {bAllDifferent^0 -> 1, rest remain the same}>

Graph 14
<l17, l10, nE^0 <= 9 /\ nS^0 <= 9 /\ bAllDifferent^0 = 0, {bAllDifferent^0 -> 0, rest remain the same}>
<l17, l10, 1 <= bAllDifferent^0 /\ nE^0 <= 9 /\ nS^0 <= 9 /\ nR^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l17, l10, 1 <= bAllDifferent^0 /\ 1 + nY^0 <= nR^0 /\ nE^0 <= 9 /\ nS^0 <= 9, {bAllDifferent^0 -> 1, rest remain the same}>
<l17, l10, 1 <= bAllDifferent^0 /\ 1 + nR^0 <= nY^0 /\ nE^0 <= 9 /\ nS^0 <= 9, {bAllDifferent^0 -> 1, rest remain the same}>
<l17, l10, 1 + bAllDifferent^0 <= 0 /\ nE^0 <= 9 /\ nS^0 <= 9 /\ nR^0 = nY^0, {bAllDifferent^0 -> 0, rest remain the same}>
<l17, l10, 1 + bAllDifferent^0 <= 0 /\ 1 + nY^0 <= nR^0 /\ nE^0 <= 9 /\ nS^0 <= 9, {bAllDifferent^0 -> 1, rest remain the same}>
<l17, l10, 1 + bAllDifferent^0 <= 0 /\ 1 + nR^0 <= nY^0 /\ nE^0 <= 9 /\ nS^0 <= 9, {bAllDifferent^0 -> 1, rest remain the same}>

Graph 15
<l10, l2, 10 <= nN^0, {bDomain^0 -> 0, rest remain the same}>
<l10, l2, 10 <= nD^0 /\ nN^0 <= 9, {bDomain^0 -> 0, rest remain the same}>
<l10, l2, 10 <= nM^0 /\ nD^0 <= 9 /\ nN^0 <= 9, {bDomain^0 -> 0, rest remain the same}>
<l10, l2, 10 <= nO^0 /\ nD^0 <= 9 /\ nM^0 <= 9 /\ nN^0 <= 9, {bDomain^0 -> 0, rest remain the same}>
<l10, l2, 10 <= nR^0 /\ nD^0 <= 9 /\ nM^0 <= 9 /\ nN^0 <= 9 /\ nO^0 <= 9, {bDomain^0 -> 0, rest remain the same}>
<l10, l2, 10 <= nY^0 /\ nD^0 <= 9 /\ nM^0 <= 9 /\ nN^0 <= 9 /\ nO^0 <= 9 /\ nR^0 <= 9, {bDomain^0 -> 0, rest remain the same}>
<l10, l2, nD^0 <= 9 /\ nM^0 <= 9 /\ nN^0 <= 9 /\ nO^0 <= 9 /\ nR^0 <= 9 /\ nY^0 <= 9, {bDomain^0 -> 1, rest remain the same}>
<l17, l2, 10 <= nS^0 /\ bAllDifferent^0 = 0, {bAllDifferent^0 -> 0, bDomain^0 -> 0, rest remain the same}>
<l17, l2, 10 <= nE^0 /\ nS^0 <= 9 /\ bAllDifferent^0 = 0, {bAllDifferent^0 -> 0, bDomain^0 -> 0, rest remain the same}>
<l17, l2, 10 <= nS^0 /\ 1 <= bAllDifferent^0 /\ nR^0 = nY^0, {bAllDifferent^0 -> 0, bDomain^0 -> 0, rest remain the same}>
<l17, l2, 10 <= nE^0 /\ 1 <= bAllDifferent^0 /\ nS^0 <= 9 /\ nR^0 = nY^0, {bAllDifferent^0 -> 0, bDomain^0 -> 0, rest remain the same}>
<l17, l2, 10 <= nS^0 /\ 1 <= bAllDifferent^0 /\ 1 + nY^0 <= nR^0, {bAllDifferent^0 -> 1, bDomain^0 -> 0, rest remain the same}>
<l17, l2, 10 <= nE^0 /\ 1 <= bAllDifferent^0 /\ 1 + nY^0 <= nR^0 /\ nS^0 <= 9, {bAllDifferent^0 -> 1, bDomain^0 -> 0, rest remain the same}>
<l17, l2, 10 <= nS^0 /\ 1 <= bAllDifferent^0 /\ 1 + nR^0 <= nY^0, {bAllDifferent^0 -> 1, bDomain^0 -> 0, rest remain the same}>
<l17, l2, 10 <= nE^0 /\ 1 <= bAllDifferent^0 /\ 1 + nR^0 <= nY^0 /\ nS^0 <= 9, {bAllDifferent^0 -> 1, bDomain^0 -> 0, rest remain the same}>
<l17, l2, 10 <= nS^0 /\ 1 + bAllDifferent^0 <= 0 /\ nR^0 = nY^0, {bAllDifferent^0 -> 0, bDomain^0 -> 0, rest remain the same}>
<l17, l2, 10 <= nE^0 /\ 1 + bAllDifferent^0 <= 0 /\ nS^0 <= 9 /\ nR^0 = nY^0, {bAllDifferent^0 -> 0, bDomain^0 -> 0, rest remain the same}>
<l17, l2, 10 <= nS^0 /\ 1 + bAllDifferent^0 <= 0 /\ 1 + nY^0 <= nR^0, {bAllDifferent^0 -> 1, bDomain^0 -> 0, rest remain the same}>
<l17, l2, 10 <= nE^0 /\ 1 + bAllDifferent^0 <= 0 /\ 1 + nY^0 <= nR^0 /\ nS^0 <= 9, {bAllDifferent^0 -> 1, bDomain^0 -> 0, rest remain the same}>
<l17, l2, 10 <= nS^0 /\ 1 + bAllDifferent^0 <= 0 /\ 1 + nR^0 <= nY^0, {bAllDifferent^0 -> 1, bDomain^0 -> 0, rest remain the same}>
<l17, l2, 10 <= nE^0 /\ 1 + bAllDifferent^0 <= 0 /\ 1 + nR^0 <= nY^0 /\ nS^0 <= 9, {bAllDifferent^0 -> 1, bDomain^0 -> 0, rest remain the same}>

Graph 16
<l2, l63, 1 <= bAllDifferent^0 /\ nM^0 = 0, {bNoLeadingZeros^0 -> 0, bSum^0 -> undef3172, rest remain the same}>
<l2, l63, 1 + bAllDifferent^0 <= 0 /\ nM^0 = 0, {bNoLeadingZeros^0 -> 0, bSum^0 -> undef3172, rest remain the same}>
<l2, l63, 1 <= bAllDifferent^0 /\ 1 <= nM^0 /\ nS^0 = 0, {bNoLeadingZeros^0 -> 0, bSum^0 -> undef3172, rest remain the same}>
<l2, l63, 1 + bAllDifferent^0 <= 0 /\ 1 <= nM^0 /\ nS^0 = 0, {bNoLeadingZeros^0 -> 0, bSum^0 -> undef3172, rest remain the same}>
<l2, l63, 1 <= bAllDifferent^0 /\ 1 <= nM^0 /\ 1 <= nS^0, {bNoLeadingZeros^0 -> 1, bSum^0 -> undef3172, rest remain the same}>
<l2, l63, 1 + bAllDifferent^0 <= 0 /\ 1 <= nM^0 /\ 1 <= nS^0, {bNoLeadingZeros^0 -> 1, bSum^0 -> undef3172, rest remain the same}>
<l2, l63, 1 <= bAllDifferent^0 /\ 1 <= nM^0 /\ 1 + nS^0 <= 0, {bNoLeadingZeros^0 -> 1, bSum^0 -> undef3172, rest remain the same}>
<l2, l63, 1 + bAllDifferent^0 <= 0 /\ 1 <= nM^0 /\ 1 + nS^0 <= 0, {bNoLeadingZeros^0 -> 1, bSum^0 -> undef3172, rest remain the same}>
<l2, l63, 1 <= bAllDifferent^0 /\ 1 + nM^0 <= 0 /\ nS^0 = 0, {bNoLeadingZeros^0 -> 0, bSum^0 -> undef3172, rest remain the same}>
<l2, l63, 1 + bAllDifferent^0 <= 0 /\ 1 + nM^0 <= 0 /\ nS^0 = 0, {bNoLeadingZeros^0 -> 0, bSum^0 -> undef3172, rest remain the same}>
<l2, l63, 1 <= bAllDifferent^0 /\ 1 + nM^0 <= 0 /\ 1 <= nS^0, {bNoLeadingZeros^0 -> 1, bSum^0 -> undef3172, rest remain the same}>
<l2, l63, 1 + bAllDifferent^0 <= 0 /\ 1 + nM^0 <= 0 /\ 1 <= nS^0, {bNoLeadingZeros^0 -> 1, bSum^0 -> undef3172, rest remain the same}>
<l2, l63, 1 <= bAllDifferent^0 /\ 1 + nM^0 <= 0 /\ 1 + nS^0 <= 0, {bNoLeadingZeros^0 -> 1, bSum^0 -> undef3172, rest remain the same}>
<l2, l63, 1 + bAllDifferent^0 <= 0 /\ 1 + nM^0 <= 0 /\ 1 + nS^0 <= 0, {bNoLeadingZeros^0 -> 1, bSum^0 -> undef3172, rest remain the same}>

Graph 17
<l2, l59, bAllDifferent^0 = 0 /\ nM^0 = 0, {bNoLeadingZeros^0 -> 0, bSum^0 -> undef3172, rest remain the same}>
<l2, l59, 1 <= nM^0 /\ bAllDifferent^0 = 0 /\ nS^0 = 0, {bNoLeadingZeros^0 -> 0, bSum^0 -> undef3172, rest remain the same}>
<l2, l59, 1 <= nM^0 /\ 1 <= nS^0 /\ bAllDifferent^0 = 0, {bNoLeadingZeros^0 -> 1, bSum^0 -> undef3172, rest remain the same}>
<l2, l59, 1 <= nM^0 /\ 1 + nS^0 <= 0 /\ bAllDifferent^0 = 0, {bNoLeadingZeros^0 -> 1, bSum^0 -> undef3172, rest remain the same}>
<l2, l59, 1 + nM^0 <= 0 /\ bAllDifferent^0 = 0 /\ nS^0 = 0, {bNoLeadingZeros^0 -> 0, bSum^0 -> undef3172, rest remain the same}>
<l2, l59, 1 + nM^0 <= 0 /\ 1 <= nS^0 /\ bAllDifferent^0 = 0, {bNoLeadingZeros^0 -> 1, bSum^0 -> undef3172, rest remain the same}>
<l2, l59, 1 + nM^0 <= 0 /\ 1 + nS^0 <= 0 /\ bAllDifferent^0 = 0, {bNoLeadingZeros^0 -> 1, bSum^0 -> undef3172, rest remain the same}>
<l63, l59, bDomain^0 = 0, {all remain the same}>
<l63, l59, 1 <= bDomain^0 /\ bNoLeadingZeros^0 = 0, {all remain the same}>
<l63, l59, 1 <= bDomain^0 /\ 1 <= bNoLeadingZeros^0 /\ bSum^0 = 0, {all remain the same}>
<l63, l59, 1 <= bDomain^0 /\ 1 <= bNoLeadingZeros^0 /\ 1 <= bSum^0, {all remain the same}>
<l63, l59, 1 <= bDomain^0 /\ 1 <= bNoLeadingZeros^0 /\ 1 + bSum^0 <= 0, {all remain the same}>
<l63, l59, 1 <= bDomain^0 /\ 1 + bNoLeadingZeros^0 <= 0 /\ bSum^0 = 0, {all remain the same}>
<l63, l59, 1 <= bDomain^0 /\ 1 + bNoLeadingZeros^0 <= 0 /\ 1 <= bSum^0, {all remain the same}>
<l63, l59, 1 <= bDomain^0 /\ 1 + bNoLeadingZeros^0 <= 0 /\ 1 + bSum^0 <= 0, {all remain the same}>
<l63, l59, 1 + bDomain^0 <= 0 /\ bNoLeadingZeros^0 = 0, {all remain the same}>
<l63, l59, 1 + bDomain^0 <= 0 /\ 1 <= bNoLeadingZeros^0 /\ bSum^0 = 0, {all remain the same}>
<l63, l59, 1 + bDomain^0 <= 0 /\ 1 <= bNoLeadingZeros^0 /\ 1 <= bSum^0, {all remain the same}>
<l63, l59, 1 + bDomain^0 <= 0 /\ 1 <= bNoLeadingZeros^0 /\ 1 + bSum^0 <= 0, {all remain the same}>
<l63, l59, 1 + bDomain^0 <= 0 /\ 1 + bNoLeadingZeros^0 <= 0 /\ bSum^0 = 0, {all remain the same}>
<l63, l59, 1 + bDomain^0 <= 0 /\ 1 + bNoLeadingZeros^0 <= 0 /\ 1 <= bSum^0, {all remain the same}>
<l63, l59, 1 + bDomain^0 <= 0 /\ 1 + bNoLeadingZeros^0 <= 0 /\ 1 + bSum^0 <= 0, {all remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 2 , 15 )
( 5 , 3 )
( 10 , 14 )
( 17 , 13 )
( 22 , 2 )
( 23 , 12 )
( 26 , 11 )
( 30 , 10 )
( 34 , 9 )
( 38 , 8 )
( 40 , 1 )
( 44 , 7 )
( 47 , 6 )
( 51 , 5 )
( 54 , 4 )
( 59 , 17 )
( 63 , 16 )

*******************************************************************************************
********************************    CHECKING ASSERTIONS    ********************************
*******************************************************************************************

Proving termination of subgraph 0
Proving termination of subgraph 1
Analyzing SCC {l40}...
No cycles found.

Proving termination of subgraph 2
Analyzing SCC {l22}...
No cycles found.

Proving termination of subgraph 3
Analyzing SCC {l5}...
No cycles found.

Proving termination of subgraph 4
Analyzing SCC {l54}...
No cycles found.

Proving termination of subgraph 5
Analyzing SCC {l51}...
No cycles found.

Proving termination of subgraph 6
Analyzing SCC {l47}...
No cycles found.

Proving termination of subgraph 7
Analyzing SCC {l44}...
No cycles found.

Proving termination of subgraph 8
Analyzing SCC {l38}...
No cycles found.

Proving termination of subgraph 9
Analyzing SCC {l34}...
No cycles found.

Proving termination of subgraph 10
Analyzing SCC {l30}...
No cycles found.

Proving termination of subgraph 11
Analyzing SCC {l26}...
No cycles found.

Proving termination of subgraph 12
Analyzing SCC {l23}...
No cycles found.

Proving termination of subgraph 13
Analyzing SCC {l17}...
No cycles found.

Proving termination of subgraph 14
Analyzing SCC {l10}...
No cycles found.

Proving termination of subgraph 15
Analyzing SCC {l2}...
No cycles found.

Proving termination of subgraph 16
Analyzing SCC {l63}...
No cycles found.

Proving termination of subgraph 17
Analyzing SCC {l59}...
No cycles found.

Program Terminates