MAYBE * Step 1: UnsatRules MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] (?,1) 1. lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [G >= 2*A (?,1) && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && E >= 0 && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] 2. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 0 && G = 0 && K = L && I = L && 1 + M = L && A = 0] (?,1) 3. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl121(Q,B,C,D,E,F,G,H,0,J,K,L,M,N,O,P) [A >= 1 (?,1) && 0 >= L && A >= 0 && E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 2*A && K = L && I = L && 1 + M = L && G = A] 4. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,G,H,0,J,K,L,M,N,O,P) [L >= 1 (?,1) && A >= 1 && A >= 0 && E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 2*A && K = L && I = L && 1 + M = L && G = A] 5. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] (?,1) 6. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] (?,1) 7. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && 1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] (?,1) 8. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] (?,1) 9. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl121(Q,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [L >= 1 + E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = L && K = L && 1 + M = L] (?,1) 10. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] (?,1) 11. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,O,H,I,J,K,L,M,N,O,P) [L >= 2*O && 0 >= O && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] (?,1) 12. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P) [L >= 2*O && O >= 1 && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] (?,1) 13. start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> start(B,B,D,D,F,F,H,H,J,J,L,L,N,N,P,P) True (1,1) Signature: {(lbl101,16);(lbl121,16);(lbl123,16);(lbl21,16);(lbl53,16);(lbl71,16);(start,16);(start0,16);(stop,16)} Flow Graph: [0->{11,12},1->{2,3,4},2->{},3->{1},4->{7,8},5->{5,6},6->{9,10},7->{5,6},8->{9,10},9->{1},10->{7,8},11->{} ,12->{7,8},13->{0}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [3] * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] (?,1) 1. lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [G >= 2*A (?,1) && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && E >= 0 && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] 2. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 0 && G = 0 && K = L && I = L && 1 + M = L && A = 0] (?,1) 4. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,G,H,0,J,K,L,M,N,O,P) [L >= 1 (?,1) && A >= 1 && A >= 0 && E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 2*A && K = L && I = L && 1 + M = L && G = A] 5. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] (?,1) 6. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] (?,1) 7. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && 1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] (?,1) 8. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] (?,1) 9. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl121(Q,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [L >= 1 + E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = L && K = L && 1 + M = L] (?,1) 10. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] (?,1) 11. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,O,H,I,J,K,L,M,N,O,P) [L >= 2*O && 0 >= O && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] (?,1) 12. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P) [L >= 2*O && O >= 1 && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] (?,1) 13. start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> start(B,B,D,D,F,F,H,H,J,J,L,L,N,N,P,P) True (1,1) Signature: {(lbl101,16);(lbl121,16);(lbl123,16);(lbl21,16);(lbl53,16);(lbl71,16);(start,16);(start0,16);(stop,16)} Flow Graph: [0->{11,12},1->{2,4},2->{},4->{7,8},5->{5,6},6->{9,10},7->{5,6},8->{9,10},9->{1},10->{7,8},11->{},12->{7 ,8},13->{0}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,7),(12,7)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] (?,1) 1. lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [G >= 2*A (?,1) && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && E >= 0 && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] 2. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 0 && G = 0 && K = L && I = L && 1 + M = L && A = 0] (?,1) 4. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,G,H,0,J,K,L,M,N,O,P) [L >= 1 (?,1) && A >= 1 && A >= 0 && E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 2*A && K = L && I = L && 1 + M = L && G = A] 5. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] (?,1) 6. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] (?,1) 7. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && 1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] (?,1) 8. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] (?,1) 9. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl121(Q,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [L >= 1 + E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = L && K = L && 1 + M = L] (?,1) 10. lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] (?,1) 11. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,O,H,I,J,K,L,M,N,O,P) [L >= 2*O && 0 >= O && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] (?,1) 12. lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P) [L >= 2*O && O >= 1 && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] (?,1) 13. start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> start(B,B,D,D,F,F,H,H,J,J,L,L,N,N,P,P) True (1,1) Signature: {(lbl101,16);(lbl121,16);(lbl123,16);(lbl21,16);(lbl53,16);(lbl71,16);(start,16);(start0,16);(stop,16)} Flow Graph: [0->{11,12},1->{2,4},2->{},4->{8},5->{5,6},6->{9,10},7->{5,6},8->{9,10},9->{1},10->{7,8},11->{},12->{8} ,13->{0}] + Applied Processor: FromIts + Details: () * Step 4: Unfold MAYBE + Considered Problem: Rules: start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [G >= 2*A && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && E >= 0 && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 0 && G = 0 && K = L && I = L && 1 + M = L && A = 0] lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,G,H,0,J,K,L,M,N,O,P) [L >= 1 && A >= 1 && A >= 0 && E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 2*A && K = L && I = L && 1 + M = L && G = A] lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && 1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl121(Q,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [L >= 1 + E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = L && K = L && 1 + M = L] lbl53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop(A,B,C,D,E,F,O,H,I,J,K,L,M,N,O,P) [L >= 2*O && 0 >= O && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] lbl21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P) [L >= 2*O && O >= 1 && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> start(B,B,D,D,F,F,H,H,J,J,L,L,N,N,P,P) True Signature: {(lbl101,16);(lbl121,16);(lbl123,16);(lbl21,16);(lbl53,16);(lbl71,16);(start,16);(start0,16);(stop,16)} Rule Graph: [0->{11,12},1->{2,4},2->{},4->{8},5->{5,6},6->{9,10},7->{5,6},8->{9,10},9->{1},10->{7,8},11->{},12->{8} ,13->{0}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: start.0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21.11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] start.0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21.12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] lbl121.1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123.2(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [G >= 2*A && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && E >= 0 && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] lbl121.1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123.4(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [G >= 2*A && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && E >= 0 && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] lbl123.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop.14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 0 && G = 0 && K = L && I = L && 1 + M = L && A = 0] lbl123.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71.8(A,B,Q,D,0,F,G,H,0,J,K,L,M,N,O,P) [L >= 1 && A >= 1 && A >= 0 && E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 2*A && K = L && I = L && 1 + M = L && G = A] lbl101.5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101.5(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl101.5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101.6(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl101.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53.9(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl101.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53.10(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl71.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101.5(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && 1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] lbl71.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101.6(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && 1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] lbl71.8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53.9(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] lbl71.8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53.10(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] lbl53.9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl121.1(Q,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [L >= 1 + E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = L && K = L && 1 + M = L] lbl53.10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71.7(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] lbl53.10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71.8(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] lbl21.11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop.14(A,B,C,D,E,F,O,H,I,J,K,L,M,N,O,P) [L >= 2*O && 0 >= O && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] lbl21.12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71.8(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P) [L >= 2*O && O >= 1 && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] start0.13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> start.0(B,B,D,D,F,F,H,H,J,J,L,L,N,N,P,P) True Signature: {(lbl101.5,16) ;(lbl101.6,16) ;(lbl121.1,16) ;(lbl123.2,16) ;(lbl123.4,16) ;(lbl21.11,16) ;(lbl21.12,16) ;(lbl53.10,16) ;(lbl53.9,16) ;(lbl71.7,16) ;(lbl71.8,16) ;(start.0,16) ;(start0.13,16) ;(stop.14,16)} Rule Graph: [0->{17},1->{18},2->{4},3->{5},4->{},5->{12,13},6->{6,7},7->{8,9},8->{14},9->{15,16},10->{6,7},11->{8,9} ,12->{14},13->{15,16},14->{2,3},15->{10,11},16->{12,13},17->{},18->{12,13},19->{0,1}] + Applied Processor: AddSinks + Details: () * Step 6: Decompose MAYBE + Considered Problem: Rules: start.0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21.11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] start.0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21.12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] lbl121.1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123.2(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [G >= 2*A && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && E >= 0 && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] lbl121.1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123.4(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [G >= 2*A && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && E >= 0 && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] lbl123.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop.14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 0 && G = 0 && K = L && I = L && 1 + M = L && A = 0] lbl123.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71.8(A,B,Q,D,0,F,G,H,0,J,K,L,M,N,O,P) [L >= 1 && A >= 1 && A >= 0 && E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 2*A && K = L && I = L && 1 + M = L && G = A] lbl101.5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101.5(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl101.5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101.6(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl101.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53.9(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl101.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53.10(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl71.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101.5(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && 1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] lbl71.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101.6(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && 1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] lbl71.8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53.9(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] lbl71.8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53.10(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] lbl53.9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl121.1(Q,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [L >= 1 + E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = L && K = L && 1 + M = L] lbl53.10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71.7(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] lbl53.10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71.8(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] lbl21.11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop.14(A,B,C,D,E,F,O,H,I,J,K,L,M,N,O,P) [L >= 2*O && 0 >= O && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] lbl21.12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71.8(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P) [L >= 2*O && O >= 1 && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] start0.13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> start.0(B,B,D,D,F,F,H,H,J,J,L,L,N,N,P,P) True stop.14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) True stop.14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) True Signature: {(exitus616,16) ;(lbl101.5,16) ;(lbl101.6,16) ;(lbl121.1,16) ;(lbl123.2,16) ;(lbl123.4,16) ;(lbl21.11,16) ;(lbl21.12,16) ;(lbl53.10,16) ;(lbl53.9,16) ;(lbl71.7,16) ;(lbl71.8,16) ;(start.0,16) ;(start0.13,16) ;(stop.14,16)} Rule Graph: [0->{17},1->{18},2->{4},3->{5},4->{20},5->{12,13},6->{6,7},7->{8,9},8->{14},9->{15,16},10->{6,7},11->{8,9} ,12->{14},13->{15,16},14->{2,3},15->{10,11},16->{12,13},17->{21},18->{12,13},19->{0,1}] + 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] | `- p:[12,5,3,14,8,7,6,10,15,9,11,13,16] c: [3,5,8,12,14] | `- p:[6,10,15,9,7,11,13,16] c: [7,9,10,11,13,15,16] | `- p:[6] c: [6] * Step 7: AbstractSize MAYBE + Considered Problem: (Rules: start.0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21.11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] start.0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl21.12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Q,P) [A = B && C = D && E = F && G = H && I = J && K = L && M = N && O = P] lbl121.1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123.2(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [G >= 2*A && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && E >= 0 && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] lbl121.1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl123.4(A,B,C,D,E,F,A,H,I,J,K,L,M,N,O,P) [G >= 2*A && 1 + 2*A >= G && 1 + 2*O >= L && O >= G && E >= 0 && G >= 1 && L >= 1 + E && K = L && I = L && 1 + M = L] lbl123.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop.14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 0 && G = 0 && K = L && I = L && 1 + M = L && A = 0] lbl123.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71.8(A,B,Q,D,0,F,G,H,0,J,K,L,M,N,O,P) [L >= 1 && A >= 1 && A >= 0 && E >= 0 && 1 + 2*O >= L && O >= 1 && L >= 1 + E && O >= 2*A && K = L && I = L && 1 + M = L && G = A] lbl101.5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101.5(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl101.5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101.6(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl101.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53.9(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl101.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53.10(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [I >= E + G && O >= G && L >= 1 + I && G >= 1 && 1 + 2*O >= L && E >= 0 && K = L] lbl71.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101.5(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && 1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] lbl71.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl101.6(A,B,C,D,E + -1*G,F,G,H,I,J,K,L,M,N,O,P) [E >= G && 1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] lbl71.8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53.9(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] lbl71.8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl53.10(A,B,C,D,E,F,G,H,1 + I,J,K,L,I,N,O,P) [1 + 2*O >= L && O >= G && G >= 1 && E >= 0 && L >= 1 + E && I = E && K = L] lbl53.9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl121.1(Q,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) [L >= 1 + E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = L && K = L && 1 + M = L] lbl53.10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71.7(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] lbl53.10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71.8(A,B,Q,D,I,F,G,H,I,J,K,L,M,N,O,P) [L >= 2 + M && L >= 1 + M && M >= E && G >= 1 && E >= 0 && O >= G && 1 + 2*O >= L && I = 1 + M && K = L] lbl21.11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> stop.14(A,B,C,D,E,F,O,H,I,J,K,L,M,N,O,P) [L >= 2*O && 0 >= O && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] lbl21.12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> lbl71.8(A,B,Q,D,0,F,O,H,0,J,K,L,M,N,O,P) [L >= 2*O && O >= 1 && 1 + 2*O >= L && M = N && A = B && C = D && E = F && G = H && I = J && K = L] start0.13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> start.0(B,B,D,D,F,F,H,H,J,J,L,L,N,N,P,P) True stop.14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) True stop.14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P) True Signature: {(exitus616,16) ;(lbl101.5,16) ;(lbl101.6,16) ;(lbl121.1,16) ;(lbl123.2,16) ;(lbl123.4,16) ;(lbl21.11,16) ;(lbl21.12,16) ;(lbl53.10,16) ;(lbl53.9,16) ;(lbl71.7,16) ;(lbl71.8,16) ;(start.0,16) ;(start0.13,16) ;(stop.14,16)} Rule Graph: [0->{17},1->{18},2->{4},3->{5},4->{20},5->{12,13},6->{6,7},7->{8,9},8->{14},9->{15,16},10->{6,7},11->{8,9} ,12->{14},13->{15,16},14->{2,3},15->{10,11},16->{12,13},17->{21},18->{12,13},19->{0,1}] ,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] | `- p:[12,5,3,14,8,7,6,10,15,9,11,13,16] c: [3,5,8,12,14] | `- p:[6,10,15,9,7,11,13,16] c: [7,9,10,11,13,15,16] | `- p:[6] c: [6]) + Applied Processor: AbstractSize Minimize + Details: () * Step 8: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,0.0,0.0.0,0.0.0.0] start.0 ~> lbl21.11 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= unknown, P <= P] start.0 ~> lbl21.12 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= unknown, P <= P] lbl121.1 ~> lbl123.2 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= A, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl121.1 ~> lbl123.4 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= A, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl123.2 ~> stop.14 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl123.4 ~> lbl71.8 [A <= A, B <= B, C <= unknown, D <= D, E <= 0*K, F <= F, G <= G, H <= H, I <= 0*K, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl101.5 ~> lbl101.5 [A <= A, B <= B, C <= C, D <= D, E <= L, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl101.5 ~> lbl101.6 [A <= A, B <= B, C <= C, D <= D, E <= L, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl101.6 ~> lbl53.9 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= L, J <= J, K <= K, L <= L, M <= I, N <= N, O <= O, P <= P] lbl101.6 ~> lbl53.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= L, J <= J, K <= K, L <= L, M <= I, N <= N, O <= O, P <= P] lbl71.7 ~> lbl101.5 [A <= A, B <= B, C <= C, D <= D, E <= K, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl71.7 ~> lbl101.6 [A <= A, B <= B, C <= C, D <= D, E <= K, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl71.8 ~> lbl53.9 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= L, J <= J, K <= K, L <= L, M <= I, N <= N, O <= O, P <= P] lbl71.8 ~> lbl53.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= L, J <= J, K <= K, L <= L, M <= I, N <= N, O <= O, P <= P] lbl53.9 ~> lbl121.1 [A <= unknown, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl53.10 ~> lbl71.7 [A <= A, B <= B, C <= unknown, D <= D, E <= I, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl53.10 ~> lbl71.8 [A <= A, B <= B, C <= unknown, D <= D, E <= I, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl21.11 ~> stop.14 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= O, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl21.12 ~> lbl71.8 [A <= A, B <= B, C <= unknown, D <= D, E <= 0*K, F <= F, G <= O, H <= H, I <= 0*K, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] start0.13 ~> start.0 [A <= B, B <= B, C <= D, D <= D, E <= F, F <= F, G <= H, H <= H, I <= J, J <= J, K <= L, L <= L, M <= N, N <= N, O <= P, P <= P] stop.14 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] stop.14 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] + Loop: [0.0 <= 2*K + 2*G] lbl71.8 ~> lbl53.9 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= L, J <= J, K <= K, L <= L, M <= I, N <= N, O <= O, P <= P] lbl123.4 ~> lbl71.8 [A <= A, B <= B, C <= unknown, D <= D, E <= 0*K, F <= F, G <= G, H <= H, I <= 0*K, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl121.1 ~> lbl123.4 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= A, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl53.9 ~> lbl121.1 [A <= unknown, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl101.6 ~> lbl53.9 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= L, J <= J, K <= K, L <= L, M <= I, N <= N, O <= O, P <= P] lbl101.5 ~> lbl101.6 [A <= A, B <= B, C <= C, D <= D, E <= L, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl101.5 ~> lbl101.5 [A <= A, B <= B, C <= C, D <= D, E <= L, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl71.7 ~> lbl101.5 [A <= A, B <= B, C <= C, D <= D, E <= K, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl53.10 ~> lbl71.7 [A <= A, B <= B, C <= unknown, D <= D, E <= I, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl101.6 ~> lbl53.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= L, J <= J, K <= K, L <= L, M <= I, N <= N, O <= O, P <= P] lbl71.7 ~> lbl101.6 [A <= A, B <= B, C <= C, D <= D, E <= K, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl71.8 ~> lbl53.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= L, J <= J, K <= K, L <= L, M <= I, N <= N, O <= O, P <= P] lbl53.10 ~> lbl71.8 [A <= A, B <= B, C <= unknown, D <= D, E <= I, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] + Loop: [0.0.0 <= K + E + I + K + L] lbl101.5 ~> lbl101.5 [A <= A, B <= B, C <= C, D <= D, E <= L, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl71.7 ~> lbl101.5 [A <= A, B <= B, C <= C, D <= D, E <= K, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl53.10 ~> lbl71.7 [A <= A, B <= B, C <= unknown, D <= D, E <= I, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl101.6 ~> lbl53.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= L, J <= J, K <= K, L <= L, M <= I, N <= N, O <= O, P <= P] lbl101.5 ~> lbl101.6 [A <= A, B <= B, C <= C, D <= D, E <= L, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl71.7 ~> lbl101.6 [A <= A, B <= B, C <= C, D <= D, E <= K, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] lbl71.8 ~> lbl53.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= L, J <= J, K <= K, L <= L, M <= I, N <= N, O <= O, P <= P] lbl53.10 ~> lbl71.8 [A <= A, B <= B, C <= unknown, D <= D, E <= I, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] + Loop: [0.0.0.0 <= E] lbl101.5 ~> lbl101.5 [A <= A, B <= B, C <= C, D <= D, E <= L, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P] + Applied Processor: AbstractFlow + Details: () * Step 9: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,0.0,0.0.0,0.0.0.0] start.0 ~> lbl21.11 [huge ~=> O] start.0 ~> lbl21.12 [huge ~=> O] lbl121.1 ~> lbl123.2 [A ~=> G] lbl121.1 ~> lbl123.4 [A ~=> G] lbl123.2 ~> stop.14 [] lbl123.4 ~> lbl71.8 [K ~=> E,K ~=> I,huge ~=> C] lbl101.5 ~> lbl101.5 [L ~=> E] lbl101.5 ~> lbl101.6 [L ~=> E] lbl101.6 ~> lbl53.9 [I ~=> M,L ~=> I] lbl101.6 ~> lbl53.10 [I ~=> M,L ~=> I] lbl71.7 ~> lbl101.5 [K ~=> E] lbl71.7 ~> lbl101.6 [K ~=> E] lbl71.8 ~> lbl53.9 [I ~=> M,L ~=> I] lbl71.8 ~> lbl53.10 [I ~=> M,L ~=> I] lbl53.9 ~> lbl121.1 [huge ~=> A] lbl53.10 ~> lbl71.7 [I ~=> E,huge ~=> C] lbl53.10 ~> lbl71.8 [I ~=> E,huge ~=> C] lbl21.11 ~> stop.14 [O ~=> G] lbl21.12 ~> lbl71.8 [O ~=> G,K ~=> E,K ~=> I,huge ~=> C] start0.13 ~> start.0 [B ~=> A,D ~=> C,F ~=> E,H ~=> G,J ~=> I,L ~=> K,N ~=> M,P ~=> O] stop.14 ~> exitus616 [] stop.14 ~> exitus616 [] + Loop: [G ~*> 0.0,K ~*> 0.0] lbl71.8 ~> lbl53.9 [I ~=> M,L ~=> I] lbl123.4 ~> lbl71.8 [K ~=> E,K ~=> I,huge ~=> C] lbl121.1 ~> lbl123.4 [A ~=> G] lbl53.9 ~> lbl121.1 [huge ~=> A] lbl101.6 ~> lbl53.9 [I ~=> M,L ~=> I] lbl101.5 ~> lbl101.6 [L ~=> E] lbl101.5 ~> lbl101.5 [L ~=> E] lbl71.7 ~> lbl101.5 [K ~=> E] lbl53.10 ~> lbl71.7 [I ~=> E,huge ~=> C] lbl101.6 ~> lbl53.10 [I ~=> M,L ~=> I] lbl71.7 ~> lbl101.6 [K ~=> E] lbl71.8 ~> lbl53.10 [I ~=> M,L ~=> I] lbl53.10 ~> lbl71.8 [I ~=> E,huge ~=> C] + Loop: [E ~+> 0.0.0,I ~+> 0.0.0,K ~+> 0.0.0,L ~+> 0.0.0,K ~+> 0.0.0] lbl101.5 ~> lbl101.5 [L ~=> E] lbl71.7 ~> lbl101.5 [K ~=> E] lbl53.10 ~> lbl71.7 [I ~=> E,huge ~=> C] lbl101.6 ~> lbl53.10 [I ~=> M,L ~=> I] lbl101.5 ~> lbl101.6 [L ~=> E] lbl71.7 ~> lbl101.6 [K ~=> E] lbl71.8 ~> lbl53.10 [I ~=> M,L ~=> I] lbl53.10 ~> lbl71.8 [I ~=> E,huge ~=> C] + Loop: [E ~=> 0.0.0.0] lbl101.5 ~> lbl101.5 [L ~=> E] + Applied Processor: Lare + Details: Unknown bound. MAYBE