YES * Step 1: UnsatRules YES + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 3. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] (?,1) 4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (?,1) 5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (?,1) 6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 7. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [J >= C && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] (?,1) 8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1) 9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (?,1) && C >= 1 + J && J >= A && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] 10. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + J,G,1,I,J,K,L) [A >= 1 + J (?,1) && E >= 1 && C >= 1 + J && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] 11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (?,1) 12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1) 13. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + J,G,1 + H,I,J,K,L) [A >= 1 + F (?,1) && E >= 1 + H && A + C >= 1 + F && A >= 0 && E >= H && F >= A && H >= 1 && J = F && L = A && D = E && B = C] 14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (?,1) 15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (?,1) 16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1) Signature: {(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)} Flow Graph: [0->{},1->{},2->{},3->{},4->{7,8,9,10},5->{11,12,13},6->{14,15},7->{},8->{7,8,9,10},9->{11,12,13},10->{14 ,15},11->{7,8,9,10},12->{11,12,13},13->{14,15},14->{11,12,13},15->{14,15},16->{0,1,2,3,4,5,6}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [13] * Step 2: UnsatPaths YES + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 3. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] (?,1) 4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (?,1) 5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (?,1) 6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 7. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [J >= C && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] (?,1) 8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1) 9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (?,1) && C >= 1 + J && J >= A && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] 10. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + J,G,1,I,J,K,L) [A >= 1 + J (?,1) && E >= 1 && C >= 1 + J && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] 11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (?,1) 12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1) 14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (?,1) 15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (?,1) 16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1) Signature: {(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)} Flow Graph: [0->{},1->{},2->{},3->{},4->{7,8,9,10},5->{11,12},6->{14,15},7->{},8->{7,8,9,10},9->{11,12},10->{14,15} ,11->{7,8,9,10},12->{11,12},14->{11,12},15->{14,15},16->{0,1,2,3,4,5,6}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,9),(4,10),(8,9),(8,10),(11,8),(11,10)] * Step 3: UnreachableRules YES + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 3. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] (?,1) 4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (?,1) 5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (?,1) 6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 7. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [J >= C && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] (?,1) 8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1) 9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (?,1) && C >= 1 + J && J >= A && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] 10. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + J,G,1,I,J,K,L) [A >= 1 + J (?,1) && E >= 1 && C >= 1 + J && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] 11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (?,1) 12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1) 14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (?,1) 15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (?,1) 16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1) Signature: {(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)} Flow Graph: [0->{},1->{},2->{},3->{},4->{7,8},5->{11,12},6->{14,15},7->{},8->{7,8},9->{11,12},10->{14,15},11->{7,9} ,12->{11,12},14->{11,12},15->{14,15},16->{0,1,2,3,4,5,6}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [10] * Step 4: FromIts YES + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 3. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] (?,1) 4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] (?,1) 5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] (?,1) 6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] (?,1) 7. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [J >= C && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] (?,1) 8. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] (?,1) 9. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 (?,1) && C >= 1 + J && J >= A && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] 11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] (?,1) 12. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] (?,1) 14. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] (?,1) 15. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] (?,1) 16. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1) Signature: {(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)} Flow Graph: [0->{},1->{},2->{},3->{},4->{7,8},5->{11,12},6->{14,15},7->{},8->{7,8},9->{11,12},11->{7,9},12->{11,12} ,14->{11,12},15->{14,15},16->{0,1,2,3,4,5,6}] + Applied Processor: FromIts + Details: () * Step 5: Decompose YES + Considered Problem: Rules: start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [J >= C && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 && C >= 1 + J && J >= A && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True Signature: {(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)} Rule Graph: [0->{},1->{},2->{},3->{},4->{7,8},5->{11,12},6->{14,15},7->{},8->{7,8},9->{11,12},11->{7,9},12->{11,12} ,14->{11,12},15->{14,15},16->{0,1,2,3,4,5,6}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,11,12,14,15,16] | +- p:[15] c: [15] | +- p:[11,9,12] c: [9,11] | | | `- p:[12] c: [12] | `- p:[8] c: [8] * Step 6: CloseWith YES + Considered Problem: (Rules: start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [J >= C && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [C >= 1 + J && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E >= 1 && C >= 1 + J && J >= A && E >= 0 && A >= 0 && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [A + C >= 1 + F && A >= 0 && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E >= 1 + H && F >= A && A + C >= 1 + F && A >= 0 && E >= H && H >= 1 && J = F && L = A && D = E && B = C] lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [A >= 1 + J && E >= 1 && J >= 0 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [A >= 1 + F && F >= 1 + J && E >= 1 && J >= 0 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True Signature: {(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)} Rule Graph: [0->{},1->{},2->{},3->{},4->{7,8},5->{11,12},6->{14,15},7->{},8->{7,8},9->{11,12},11->{7,9},12->{11,12} ,14->{11,12},15->{14,15},16->{0,1,2,3,4,5,6}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,11,12,14,15,16] | +- p:[15] c: [15] | +- p:[11,9,12] c: [9,11] | | | `- p:[12] c: [12] | `- p:[8] c: [8]) + Applied Processor: CloseWith True + Details: () YES