YES(?,PRIMREC) * Step 1: FromIts MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && 0 >= 1 + A && B = C && D = A && E = F && G = H] 1. start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] 2. start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && B = C && D = A && E = F && G = H] 3. start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && H >= C && A >= 0 && B = C && D = A && E = F && G = H] 4. lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && H >= B && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] 6. lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && B >= 0 && A >= D && G = H] 7. lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && A >= D && G = H] 8. lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && H >= B && A >= D && G = H] 9. cut(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && 1 + D = 0 && G = H] 10. cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && B >= 0 && A >= 1 + D && G = H] 11. cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && A >= 1 + D && G = H] 12. cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 (?,1) && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && H >= B && D >= 0 && A >= 1 + D && G = H] 13. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,A,F,F,H,H) True (1,1) Signature: {(cut,8);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [0->{},1->{6,7,8},2->{9,10,11,12},3->{4,5},4->{9,10,11,12},5->{4,5},6->{6,7,8},7->{9,10,11,12},8->{4,5} ,9->{},10->{6,7,8},11->{9,10,11,12},12->{4,5},13->{0,1,2,3}] + Applied Processor: FromIts + Details: () * Step 2: AddSinks MAYBE + Considered Problem: Rules: start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && 0 >= 1 + A && B = C && D = A && E = F && G = H] start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && B = C && D = A && E = F && G = H] start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && H >= C && A >= 0 && B = C && D = A && E = F && G = H] lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && H >= B && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && B >= 0 && A >= D && G = H] lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && A >= D && G = H] lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && H >= B && A >= D && G = H] cut(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && 1 + D = 0 && G = H] cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && B >= 0 && A >= 1 + D && G = H] cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && A >= 1 + D && G = H] cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && H >= B && D >= 0 && A >= 1 + D && G = H] start0(A,B,C,D,E,F,G,H) -> start(A,C,C,A,F,F,H,H) True Signature: {(cut,8);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Rule Graph: [0->{},1->{6,7,8},2->{9,10,11,12},3->{4,5},4->{9,10,11,12},5->{4,5},6->{6,7,8},7->{9,10,11,12},8->{4,5} ,9->{},10->{6,7,8},11->{9,10,11,12},12->{4,5},13->{0,1,2,3}] + Applied Processor: AddSinks + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && 0 >= 1 + A && B = C && D = A && E = F && G = H] start(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] start(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && B = C && D = A && E = F && G = H] start(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && H >= C && A >= 0 && B = C && D = A && E = F && G = H] lbl72(A,B,C,D,E,F,G,H) -> cut(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && H >= B && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl42(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && B >= 0 && A >= D && G = H] lbl42(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && A >= D && G = H] lbl42(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && H >= B && A >= D && G = H] cut(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && 1 + D = 0 && G = H] cut(A,B,C,D,E,F,G,H) -> lbl42(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && B >= 0 && A >= 1 + D && G = H] cut(A,B,C,D,E,F,G,H) -> cut(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && A >= 1 + D && G = H] cut(A,B,C,D,E,F,G,H) -> lbl72(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && H >= B && D >= 0 && A >= 1 + D && G = H] start0(A,B,C,D,E,F,G,H) -> start(A,C,C,A,F,F,H,H) True stop(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True stop(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True stop(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True stop(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True Signature: {(cut,8);(exitus616,8);(lbl42,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Rule Graph: [0->{17},1->{6,7,8},2->{9,10,11,12},3->{4,5},4->{9,10,11,12},5->{4,5},6->{6,7,8},7->{9,10,11,12},8->{4,5} ,9->{14,15,16},10->{6,7,8},11->{9,10,11,12},12->{4,5},13->{0,1,2,3}] + Applied Processor: Unfold + Details: () * Step 4: Decompose MAYBE + Considered Problem: Rules: start.0(A,B,C,D,E,F,G,H) -> stop.17(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && 0 >= 1 + A && B = C && D = A && E = F && G = H] start.1(A,B,C,D,E,F,G,H) -> lbl42.6(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] start.1(A,B,C,D,E,F,G,H) -> lbl42.7(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] start.1(A,B,C,D,E,F,G,H) -> lbl42.8(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] start.2(A,B,C,D,E,F,G,H) -> cut.9(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && B = C && D = A && E = F && G = H] start.2(A,B,C,D,E,F,G,H) -> cut.10(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && B = C && D = A && E = F && G = H] start.2(A,B,C,D,E,F,G,H) -> cut.11(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && B = C && D = A && E = F && G = H] start.2(A,B,C,D,E,F,G,H) -> cut.12(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && B = C && D = A && E = F && G = H] start.3(A,B,C,D,E,F,G,H) -> lbl72.4(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && H >= C && A >= 0 && B = C && D = A && E = F && G = H] start.3(A,B,C,D,E,F,G,H) -> lbl72.5(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && H >= C && A >= 0 && B = C && D = A && E = F && G = H] lbl72.4(A,B,C,D,E,F,G,H) -> cut.9(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl72.4(A,B,C,D,E,F,G,H) -> cut.10(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl72.4(A,B,C,D,E,F,G,H) -> cut.11(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl72.4(A,B,C,D,E,F,G,H) -> cut.12(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl72.5(A,B,C,D,E,F,G,H) -> lbl72.4(A,1 + B,C,D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && H >= B && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl72.5(A,B,C,D,E,F,G,H) -> lbl72.5(A,1 + B,C,D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && H >= B && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl42.6(A,B,C,D,E,F,G,H) -> lbl42.6(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && B >= 0 && A >= D && G = H] lbl42.6(A,B,C,D,E,F,G,H) -> lbl42.7(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && B >= 0 && A >= D && G = H] lbl42.6(A,B,C,D,E,F,G,H) -> lbl42.8(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && B >= 0 && A >= D && G = H] lbl42.7(A,B,C,D,E,F,G,H) -> cut.9(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && A >= D && G = H] lbl42.7(A,B,C,D,E,F,G,H) -> cut.10(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && A >= D && G = H] lbl42.7(A,B,C,D,E,F,G,H) -> cut.11(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && A >= D && G = H] lbl42.7(A,B,C,D,E,F,G,H) -> cut.12(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && A >= D && G = H] lbl42.8(A,B,C,D,E,F,G,H) -> lbl72.4(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && H >= B && A >= D && G = H] lbl42.8(A,B,C,D,E,F,G,H) -> lbl72.5(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && H >= B && A >= D && G = H] cut.9(A,B,C,D,E,F,G,H) -> stop.14(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && 1 + D = 0 && G = H] cut.9(A,B,C,D,E,F,G,H) -> stop.15(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && 1 + D = 0 && G = H] cut.9(A,B,C,D,E,F,G,H) -> stop.16(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && 1 + D = 0 && G = H] cut.10(A,B,C,D,E,F,G,H) -> lbl42.6(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && B >= 0 && A >= 1 + D && G = H] cut.10(A,B,C,D,E,F,G,H) -> lbl42.7(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && B >= 0 && A >= 1 + D && G = H] cut.10(A,B,C,D,E,F,G,H) -> lbl42.8(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && B >= 0 && A >= 1 + D && G = H] cut.11(A,B,C,D,E,F,G,H) -> cut.9(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && A >= 1 + D && G = H] cut.11(A,B,C,D,E,F,G,H) -> cut.10(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && A >= 1 + D && G = H] cut.11(A,B,C,D,E,F,G,H) -> cut.11(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && A >= 1 + D && G = H] cut.11(A,B,C,D,E,F,G,H) -> cut.12(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && A >= 1 + D && G = H] cut.12(A,B,C,D,E,F,G,H) -> lbl72.4(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && H >= B && D >= 0 && A >= 1 + D && G = H] cut.12(A,B,C,D,E,F,G,H) -> lbl72.5(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && H >= B && D >= 0 && A >= 1 + D && G = H] start0.13(A,B,C,D,E,F,G,H) -> start.0(A,C,C,A,F,F,H,H) True start0.13(A,B,C,D,E,F,G,H) -> start.1(A,C,C,A,F,F,H,H) True start0.13(A,B,C,D,E,F,G,H) -> start.2(A,C,C,A,F,F,H,H) True start0.13(A,B,C,D,E,F,G,H) -> start.3(A,C,C,A,F,F,H,H) True stop.14(A,B,C,D,E,F,G,H) -> exitus616.18(A,B,C,D,E,F,G,H) True stop.15(A,B,C,D,E,F,G,H) -> exitus616.18(A,B,C,D,E,F,G,H) True stop.16(A,B,C,D,E,F,G,H) -> exitus616.18(A,B,C,D,E,F,G,H) True stop.17(A,B,C,D,E,F,G,H) -> exitus616.18(A,B,C,D,E,F,G,H) True Signature: {(cut.10,8) ;(cut.11,8) ;(cut.12,8) ;(cut.9,8) ;(exitus616.18,8) ;(lbl42.6,8) ;(lbl42.7,8) ;(lbl42.8,8) ;(lbl72.4,8) ;(lbl72.5,8) ;(start.0,8) ;(start.1,8) ;(start.2,8) ;(start.3,8) ;(start0.13,8) ;(stop.14,8) ;(stop.15,8) ;(stop.16,8) ;(stop.17,8)} Rule Graph: [0->{44},1->{16,17,18},2->{19,20,21,22},3->{23,24},4->{25,26,27},5->{28,29,30},6->{31,32,33,34},7->{35,36} ,8->{10,11,12,13},9->{14,15},10->{25,26,27},11->{28,29,30},12->{31,32,33,34},13->{35,36},14->{10,11,12,13} ,15->{14,15},16->{16,17,18},17->{19,20,21,22},18->{23,24},19->{25,26,27},20->{28,29,30},21->{31,32,33,34} ,22->{35,36},23->{10,11,12,13},24->{14,15},25->{41},26->{42},27->{43},28->{16,17,18},29->{19,20,21,22} ,30->{23,24},31->{25,26,27},32->{28,29,30},33->{31,32,33,34},34->{35,36},35->{10,11,12,13},36->{14,15} ,37->{0},38->{1,2,3},39->{4,5,6,7},40->{8,9},41->{},42->{},43->{},44->{}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44] | `- p:[16,28,11,14,15,24,18,30,20,17,29,32,12,23,35,13,22,34,21,33,36] c: [11,12,13,14,17,18,20,21,22,23,24,28,29,30,32,33,34,35,36] | +- p:[16] c: [16] | `- p:[15] c: [15] * Step 5: AbstractSize MAYBE + Considered Problem: (Rules: start.0(A,B,C,D,E,F,G,H) -> stop.17(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && 0 >= 1 + A && B = C && D = A && E = F && G = H] start.1(A,B,C,D,E,F,G,H) -> lbl42.6(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] start.1(A,B,C,D,E,F,G,H) -> lbl42.7(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] start.1(A,B,C,D,E,F,G,H) -> lbl42.8(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && C >= 0 && B = C && D = A && E = F && G = H] start.2(A,B,C,D,E,F,G,H) -> cut.9(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && B = C && D = A && E = F && G = H] start.2(A,B,C,D,E,F,G,H) -> cut.10(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && B = C && D = A && E = F && G = H] start.2(A,B,C,D,E,F,G,H) -> cut.11(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && B = C && D = A && E = F && G = H] start.2(A,B,C,D,E,F,G,H) -> cut.12(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 0 && B = C && D = A && E = F && G = H] start.3(A,B,C,D,E,F,G,H) -> lbl72.4(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && H >= C && A >= 0 && B = C && D = A && E = F && G = H] start.3(A,B,C,D,E,F,G,H) -> lbl72.5(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && E + -1*F >= 0 && -1*E + F >= 0 && A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && H >= C && A >= 0 && B = C && D = A && E = F && G = H] lbl72.4(A,B,C,D,E,F,G,H) -> cut.9(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl72.4(A,B,C,D,E,F,G,H) -> cut.10(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl72.4(A,B,C,D,E,F,G,H) -> cut.11(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl72.4(A,B,C,D,E,F,G,H) -> cut.12(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl72.5(A,B,C,D,E,F,G,H) -> lbl72.4(A,1 + B,C,D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && H >= B && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl72.5(A,B,C,D,E,F,G,H) -> lbl72.5(A,1 + B,C,D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1*E + H >= 0 && 1 + -1*B + H >= 0 && -1*E + G >= 0 && 1 + -1*B + G >= 0 && -1 + B + -1*E >= 0 && 1 + -1*B + E >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && H >= B && A >= 1 + D && 1 + H >= B && 1 + E = B && G = H] lbl42.6(A,B,C,D,E,F,G,H) -> lbl42.6(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && B >= 0 && A >= D && G = H] lbl42.6(A,B,C,D,E,F,G,H) -> lbl42.7(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && B >= 0 && A >= D && G = H] lbl42.6(A,B,C,D,E,F,G,H) -> lbl42.8(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && B >= 0 && A >= D && G = H] lbl42.7(A,B,C,D,E,F,G,H) -> cut.9(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && A >= D && G = H] lbl42.7(A,B,C,D,E,F,G,H) -> cut.10(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && A >= D && G = H] lbl42.7(A,B,C,D,E,F,G,H) -> cut.11(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && A >= D && G = H] lbl42.7(A,B,C,D,E,F,G,H) -> cut.12(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && A >= D && G = H] lbl42.8(A,B,C,D,E,F,G,H) -> lbl72.4(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && H >= B && A >= D && G = H] lbl42.8(A,B,C,D,E,F,G,H) -> lbl72.5(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && A + -1*D >= 0 && D >= 0 && 1 + B + D >= 0 && A + D >= 0 && 1 + B >= 0 && 1 + A + B >= 0 && A >= 0 && H >= B && A >= D && G = H] cut.9(A,B,C,D,E,F,G,H) -> stop.14(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && 1 + D = 0 && G = H] cut.9(A,B,C,D,E,F,G,H) -> stop.15(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && 1 + D = 0 && G = H] cut.9(A,B,C,D,E,F,G,H) -> stop.16(A,B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && 1 + D = 0 && G = H] cut.10(A,B,C,D,E,F,G,H) -> lbl42.6(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && B >= 0 && A >= 1 + D && G = H] cut.10(A,B,C,D,E,F,G,H) -> lbl42.7(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && B >= 0 && A >= 1 + D && G = H] cut.10(A,B,C,D,E,F,G,H) -> lbl42.8(A,-1 + B,C,D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && B >= 0 && A >= 1 + D && G = H] cut.11(A,B,C,D,E,F,G,H) -> cut.9(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && A >= 1 + D && G = H] cut.11(A,B,C,D,E,F,G,H) -> cut.10(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && A >= 1 + D && G = H] cut.11(A,B,C,D,E,F,G,H) -> cut.11(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && A >= 1 + D && G = H] cut.11(A,B,C,D,E,F,G,H) -> cut.12(A,B,C,-1 + D,E,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && D >= 0 && A >= 1 + D && G = H] cut.12(A,B,C,D,E,F,G,H) -> lbl72.4(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && H >= B && D >= 0 && A >= 1 + D && G = H] cut.12(A,B,C,D,E,F,G,H) -> lbl72.5(A,1 + B,C,-1 + D,B,F,G,H) [G + -1*H >= 0 && -1*G + H >= 0 && -1 + A + -1*D >= 0 && 1 + D >= 0 && 1 + A + D >= 0 && A >= 0 && H >= B && D >= 0 && A >= 1 + D && G = H] start0.13(A,B,C,D,E,F,G,H) -> start.0(A,C,C,A,F,F,H,H) True start0.13(A,B,C,D,E,F,G,H) -> start.1(A,C,C,A,F,F,H,H) True start0.13(A,B,C,D,E,F,G,H) -> start.2(A,C,C,A,F,F,H,H) True start0.13(A,B,C,D,E,F,G,H) -> start.3(A,C,C,A,F,F,H,H) True stop.14(A,B,C,D,E,F,G,H) -> exitus616.18(A,B,C,D,E,F,G,H) True stop.15(A,B,C,D,E,F,G,H) -> exitus616.18(A,B,C,D,E,F,G,H) True stop.16(A,B,C,D,E,F,G,H) -> exitus616.18(A,B,C,D,E,F,G,H) True stop.17(A,B,C,D,E,F,G,H) -> exitus616.18(A,B,C,D,E,F,G,H) True Signature: {(cut.10,8) ;(cut.11,8) ;(cut.12,8) ;(cut.9,8) ;(exitus616.18,8) ;(lbl42.6,8) ;(lbl42.7,8) ;(lbl42.8,8) ;(lbl72.4,8) ;(lbl72.5,8) ;(start.0,8) ;(start.1,8) ;(start.2,8) ;(start.3,8) ;(start0.13,8) ;(stop.14,8) ;(stop.15,8) ;(stop.16,8) ;(stop.17,8)} Rule Graph: [0->{44},1->{16,17,18},2->{19,20,21,22},3->{23,24},4->{25,26,27},5->{28,29,30},6->{31,32,33,34},7->{35,36} ,8->{10,11,12,13},9->{14,15},10->{25,26,27},11->{28,29,30},12->{31,32,33,34},13->{35,36},14->{10,11,12,13} ,15->{14,15},16->{16,17,18},17->{19,20,21,22},18->{23,24},19->{25,26,27},20->{28,29,30},21->{31,32,33,34} ,22->{35,36},23->{10,11,12,13},24->{14,15},25->{41},26->{42},27->{43},28->{16,17,18},29->{19,20,21,22} ,30->{23,24},31->{25,26,27},32->{28,29,30},33->{31,32,33,34},34->{35,36},35->{10,11,12,13},36->{14,15} ,37->{0},38->{1,2,3},39->{4,5,6,7},40->{8,9},41->{},42->{},43->{},44->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44] | `- p:[16,28,11,14,15,24,18,30,20,17,29,32,12,23,35,13,22,34,21,33,36] c: [11,12,13,14,17,18,20,21,22,23,24,28,29,30,32,33,34,35,36] | +- p:[16] c: [16] | `- p:[15] c: [15]) + Applied Processor: AbstractSize Minimize + Details: () * Step 6: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,0.0,0.0.0,0.0.1] start.0 ~> stop.17 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] start.1 ~> lbl42.6 [A <= A, B <= K + C, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] start.1 ~> lbl42.7 [A <= A, B <= K + C, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] start.1 ~> lbl42.8 [A <= A, B <= K + C, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] start.2 ~> cut.9 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H] start.2 ~> cut.10 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H] start.2 ~> cut.11 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H] start.2 ~> cut.12 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H] start.3 ~> lbl72.4 [A <= A, B <= K + C, C <= C, D <= K + D, E <= B, F <= F, G <= G, H <= H] start.3 ~> lbl72.5 [A <= A, B <= K + C, C <= C, D <= K + D, E <= B, F <= F, G <= G, H <= H] lbl72.4 ~> cut.9 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] lbl72.4 ~> cut.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] lbl72.4 ~> cut.11 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] lbl72.4 ~> cut.12 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] lbl72.5 ~> lbl72.4 [A <= A, B <= K + B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] lbl72.5 ~> lbl72.5 [A <= A, B <= K + B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] lbl42.6 ~> lbl42.6 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] lbl42.6 ~> lbl42.7 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] lbl42.6 ~> lbl42.8 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] lbl42.7 ~> cut.9 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H] lbl42.7 ~> cut.10 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H] lbl42.7 ~> cut.11 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H] lbl42.7 ~> cut.12 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H] lbl42.8 ~> lbl72.4 [A <= A, B <= K + H, C <= C, D <= K + D, E <= B, F <= F, G <= G, H <= H] lbl42.8 ~> lbl72.5 [A <= A, B <= K + H, C <= C, D <= K + D, E <= B, F <= F, G <= G, H <= H] cut.9 ~> stop.14 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] cut.9 ~> stop.15 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] cut.9 ~> stop.16 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] cut.10 ~> lbl42.6 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] cut.10 ~> lbl42.7 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] cut.10 ~> lbl42.8 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] cut.11 ~> cut.9 [A <= A, B <= B, C <= C, D <= A, E <= E, F <= F, G <= G, H <= H] cut.11 ~> cut.10 [A <= A, B <= B, C <= C, D <= A, E <= E, F <= F, G <= G, H <= H] cut.11 ~> cut.11 [A <= A, B <= B, C <= C, D <= A, E <= E, F <= F, G <= G, H <= H] cut.11 ~> cut.12 [A <= A, B <= B, C <= C, D <= A, E <= E, F <= F, G <= G, H <= H] cut.12 ~> lbl72.4 [A <= A, B <= K + B, C <= C, D <= A, E <= B, F <= F, G <= G, H <= H] cut.12 ~> lbl72.5 [A <= A, B <= K + B, C <= C, D <= A, E <= B, F <= F, G <= G, H <= H] start0.13 ~> start.0 [A <= A, B <= C, C <= C, D <= A, E <= F, F <= F, G <= H, H <= H] start0.13 ~> start.1 [A <= A, B <= C, C <= C, D <= A, E <= F, F <= F, G <= H, H <= H] start0.13 ~> start.2 [A <= A, B <= C, C <= C, D <= A, E <= F, F <= F, G <= H, H <= H] start0.13 ~> start.3 [A <= A, B <= C, C <= C, D <= A, E <= F, F <= F, G <= H, H <= H] stop.14 ~> exitus616.18 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] stop.15 ~> exitus616.18 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] stop.16 ~> exitus616.18 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] stop.17 ~> exitus616.18 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] + Loop: [0.0 <= K + D] lbl42.6 ~> lbl42.6 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] cut.10 ~> lbl42.6 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] lbl72.4 ~> cut.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] lbl72.5 ~> lbl72.4 [A <= A, B <= K + B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] lbl72.5 ~> lbl72.5 [A <= A, B <= K + B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] lbl42.8 ~> lbl72.5 [A <= A, B <= K + H, C <= C, D <= K + D, E <= B, F <= F, G <= G, H <= H] lbl42.6 ~> lbl42.8 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] cut.10 ~> lbl42.8 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] lbl42.7 ~> cut.10 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H] lbl42.6 ~> lbl42.7 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] cut.10 ~> lbl42.7 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] cut.11 ~> cut.10 [A <= A, B <= B, C <= C, D <= A, E <= E, F <= F, G <= G, H <= H] lbl72.4 ~> cut.11 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] lbl42.8 ~> lbl72.4 [A <= A, B <= K + H, C <= C, D <= K + D, E <= B, F <= F, G <= G, H <= H] cut.12 ~> lbl72.4 [A <= A, B <= K + B, C <= C, D <= A, E <= B, F <= F, G <= G, H <= H] lbl72.4 ~> cut.12 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] lbl42.7 ~> cut.12 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H] cut.11 ~> cut.12 [A <= A, B <= B, C <= C, D <= A, E <= E, F <= F, G <= G, H <= H] lbl42.7 ~> cut.11 [A <= A, B <= B, C <= C, D <= K + D, E <= E, F <= F, G <= G, H <= H] cut.11 ~> cut.11 [A <= A, B <= B, C <= C, D <= A, E <= E, F <= F, G <= G, H <= H] cut.12 ~> lbl72.5 [A <= A, B <= K + B, C <= C, D <= A, E <= B, F <= F, G <= G, H <= H] + Loop: [0.0.0 <= K + B + D] lbl42.6 ~> lbl42.6 [A <= A, B <= K + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] + Loop: [0.0.1 <= K + B + H] lbl72.5 ~> lbl72.5 [A <= A, B <= K + B, C <= C, D <= D, E <= B, F <= F, G <= G, H <= H] + Applied Processor: AbstractFlow + Details: () * Step 7: Lare MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,0.0,0.0.0,0.0.1] start.0 ~> stop.17 [] start.1 ~> lbl42.6 [C ~+> B,K ~+> B] start.1 ~> lbl42.7 [C ~+> B,K ~+> B] start.1 ~> lbl42.8 [C ~+> B,K ~+> B] start.2 ~> cut.9 [D ~+> D,K ~+> D] start.2 ~> cut.10 [D ~+> D,K ~+> D] start.2 ~> cut.11 [D ~+> D,K ~+> D] start.2 ~> cut.12 [D ~+> D,K ~+> D] start.3 ~> lbl72.4 [B ~=> E,C ~+> B,D ~+> D,K ~+> B,K ~+> D] start.3 ~> lbl72.5 [B ~=> E,C ~+> B,D ~+> D,K ~+> B,K ~+> D] lbl72.4 ~> cut.9 [] lbl72.4 ~> cut.10 [] lbl72.4 ~> cut.11 [] lbl72.4 ~> cut.12 [] lbl72.5 ~> lbl72.4 [B ~=> E,B ~+> B,K ~+> B] lbl72.5 ~> lbl72.5 [B ~=> E,B ~+> B,K ~+> B] lbl42.6 ~> lbl42.6 [B ~+> B,K ~+> B] lbl42.6 ~> lbl42.7 [B ~+> B,K ~+> B] lbl42.6 ~> lbl42.8 [B ~+> B,K ~+> B] lbl42.7 ~> cut.9 [D ~+> D,K ~+> D] lbl42.7 ~> cut.10 [D ~+> D,K ~+> D] lbl42.7 ~> cut.11 [D ~+> D,K ~+> D] lbl42.7 ~> cut.12 [D ~+> D,K ~+> D] lbl42.8 ~> lbl72.4 [B ~=> E,D ~+> D,H ~+> B,K ~+> B,K ~+> D] lbl42.8 ~> lbl72.5 [B ~=> E,D ~+> D,H ~+> B,K ~+> B,K ~+> D] cut.9 ~> stop.14 [] cut.9 ~> stop.15 [] cut.9 ~> stop.16 [] cut.10 ~> lbl42.6 [B ~+> B,K ~+> B] cut.10 ~> lbl42.7 [B ~+> B,K ~+> B] cut.10 ~> lbl42.8 [B ~+> B,K ~+> B] cut.11 ~> cut.9 [A ~=> D] cut.11 ~> cut.10 [A ~=> D] cut.11 ~> cut.11 [A ~=> D] cut.11 ~> cut.12 [A ~=> D] cut.12 ~> lbl72.4 [A ~=> D,B ~=> E,B ~+> B,K ~+> B] cut.12 ~> lbl72.5 [A ~=> D,B ~=> E,B ~+> B,K ~+> B] start0.13 ~> start.0 [A ~=> D,C ~=> B,F ~=> E,H ~=> G] start0.13 ~> start.1 [A ~=> D,C ~=> B,F ~=> E,H ~=> G] start0.13 ~> start.2 [A ~=> D,C ~=> B,F ~=> E,H ~=> G] start0.13 ~> start.3 [A ~=> D,C ~=> B,F ~=> E,H ~=> G] stop.14 ~> exitus616.18 [] stop.15 ~> exitus616.18 [] stop.16 ~> exitus616.18 [] stop.17 ~> exitus616.18 [] + Loop: [D ~+> 0.0,K ~+> 0.0] lbl42.6 ~> lbl42.6 [B ~+> B,K ~+> B] cut.10 ~> lbl42.6 [B ~+> B,K ~+> B] lbl72.4 ~> cut.10 [] lbl72.5 ~> lbl72.4 [B ~=> E,B ~+> B,K ~+> B] lbl72.5 ~> lbl72.5 [B ~=> E,B ~+> B,K ~+> B] lbl42.8 ~> lbl72.5 [B ~=> E,D ~+> D,H ~+> B,K ~+> B,K ~+> D] lbl42.6 ~> lbl42.8 [B ~+> B,K ~+> B] cut.10 ~> lbl42.8 [B ~+> B,K ~+> B] lbl42.7 ~> cut.10 [D ~+> D,K ~+> D] lbl42.6 ~> lbl42.7 [B ~+> B,K ~+> B] cut.10 ~> lbl42.7 [B ~+> B,K ~+> B] cut.11 ~> cut.10 [A ~=> D] lbl72.4 ~> cut.11 [] lbl42.8 ~> lbl72.4 [B ~=> E,D ~+> D,H ~+> B,K ~+> B,K ~+> D] cut.12 ~> lbl72.4 [A ~=> D,B ~=> E,B ~+> B,K ~+> B] lbl72.4 ~> cut.12 [] lbl42.7 ~> cut.12 [D ~+> D,K ~+> D] cut.11 ~> cut.12 [A ~=> D] lbl42.7 ~> cut.11 [D ~+> D,K ~+> D] cut.11 ~> cut.11 [A ~=> D] cut.12 ~> lbl72.5 [A ~=> D,B ~=> E,B ~+> B,K ~+> B] + Loop: [B ~+> 0.0.0,D ~+> 0.0.0,K ~+> 0.0.0] lbl42.6 ~> lbl42.6 [B ~+> B,K ~+> B] + Loop: [B ~+> 0.0.1,H ~+> 0.0.1,K ~+> 0.0.1] lbl72.5 ~> lbl72.5 [B ~=> E,B ~+> B,K ~+> B] + Applied Processor: Lare + Details: start0.13 ~> exitus616.18 [A ~=> D ,C ~=> B ,C ~=> E ,F ~=> E ,H ~=> G ,A ~+> D ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,C ~+> B ,C ~+> E ,C ~+> 0.0.0 ,C ~+> 0.0.1 ,C ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> E ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,C ~*> B ,C ~*> E ,C ~*> 0.0.0 ,C ~*> 0.0.1 ,C ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,A ~^> B ,A ~^> E ,A ~^> 0.0.0 ,A ~^> 0.0.1 ,A ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] + lbl72.4> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] cut.11> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl42.7> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl72.4> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] cut.11> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl42.7> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl72.4> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] cut.11> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl42.7> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl72.4> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] cut.11> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl42.7> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl72.4> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] cut.11> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl42.7> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl72.4> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] cut.11> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl42.7> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl72.4> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] cut.11> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl42.7> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl72.4> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] cut.11> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] lbl42.7> [A ~=> D ,B ~=> E ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> E ,B ~+> 0.0.0 ,B ~+> 0.0.1 ,B ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,H ~+> B ,H ~+> E ,H ~+> 0.0.0 ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.1 ,K ~+> tick ,A ~*> B ,A ~*> E ,A ~*> 0.0.0 ,A ~*> 0.0.1 ,A ~*> tick ,B ~*> B ,B ~*> E ,B ~*> 0.0.0 ,B ~*> 0.0.1 ,B ~*> tick ,D ~*> B ,D ~*> D ,D ~*> E ,D ~*> 0.0.0 ,D ~*> 0.0.1 ,D ~*> tick ,H ~*> B ,H ~*> E ,H ~*> 0.0.0 ,H ~*> 0.0.1 ,H ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> 0.0.1 ,K ~*> tick ,D ~^> B ,D ~^> E ,D ~^> 0.0.0 ,D ~^> 0.0.1 ,D ~^> tick ,K ~^> B ,K ~^> E ,K ~^> 0.0.0 ,K ~^> 0.0.1 ,K ~^> tick] + lbl42.6> [B ~+> B ,B ~+> 0.0.0 ,B ~+> tick ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0.0 ,K ~+> tick ,B ~*> B ,D ~*> B ,K ~*> B] + lbl72.5> [B ~=> E ,B ~+> B ,B ~+> E ,B ~+> 0.0.1 ,B ~+> tick ,H ~+> 0.0.1 ,H ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> E ,K ~+> 0.0.1 ,K ~+> tick ,B ~*> B ,H ~*> B ,K ~*> B ,K ~*> E] YES(?,PRIMREC)