MAYBE * Step 1: TrivialSCCs 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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: 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) 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,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,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,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 3: 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) 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,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,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,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 4: AddSinks 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) 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,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,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,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: AddSinks + Details: () * Step 5: 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) 14. lbl123(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 (?,1) 15. lbl21(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 (?,1) Signature: {(exitus616,16) ;(lbl101,16) ;(lbl121,16) ;(lbl123,16) ;(lbl21,16) ;(lbl53,16) ;(lbl71,16) ;(start,16) ;(start0,16) ;(stop,16)} Flow Graph: [0->{11,12,15},1->{2,4,14},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},14->{},15->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,7),(12,7)] * Step 6: LooptreeTransformer 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) 14. lbl123(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 (?,1) 15. lbl21(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 (?,1) Signature: {(exitus616,16) ;(lbl101,16) ;(lbl121,16) ;(lbl123,16) ;(lbl21,16) ;(lbl53,16) ;(lbl71,16) ;(start,16) ;(start0,16) ;(stop,16)} Flow Graph: [0->{11,12,15},1->{2,4,14},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},14->{},15->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,4,5,6,7,8,9,10,11,12,13,14,15] | `- p:[8,4,1,9,6,5,7,10] c: [9] | `- p:[8,10,6,5,7] c: [10] | `- p:[5] c: [5] * Step 7: SizeAbstraction 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) 14. lbl123(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 (?,1) 15. lbl21(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 (?,1) Signature: {(exitus616,16) ;(lbl101,16) ;(lbl121,16) ;(lbl123,16) ;(lbl21,16) ;(lbl53,16) ;(lbl71,16) ;(start,16) ;(start0,16) ;(stop,16)} Flow Graph: [0->{11,12,15},1->{2,4,14},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},14->{},15->{}] ,We construct a looptree: P: [0,1,2,4,5,6,7,8,9,10,11,12,13,14,15] | `- p:[8,4,1,9,6,5,7,10] c: [9] | `- p:[8,10,6,5,7] c: [10] | `- p:[5] c: [5]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 8: FlowAbstraction 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 ~> lbl21 [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 ~> lbl123 [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 ~> stop [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 ~> lbl71 [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 ~> lbl101 [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 ~> lbl53 [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 ~> lbl101 [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 ~> lbl53 [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 ~> lbl121 [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 ~> lbl71 [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 ~> stop [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 ~> lbl71 [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 ~> start [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] lbl123 ~> 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] lbl21 ~> 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*A + 2*G] lbl71 ~> lbl53 [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 ~> lbl71 [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 ~> lbl123 [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 ~> lbl121 [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 ~> lbl53 [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 ~> lbl101 [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 ~> lbl101 [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 ~> lbl71 [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 + I + M + 2*O] lbl71 ~> lbl53 [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 ~> lbl71 [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 ~> lbl53 [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 ~> lbl101 [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 ~> lbl101 [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] + Loop: [0.0.0.0 <= K + E] lbl101 ~> lbl101 [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: FlowAbstraction + 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 ~> lbl21 [huge ~=> O] lbl121 ~> lbl123 [A ~=> G] lbl123 ~> stop [] lbl123 ~> lbl71 [K ~=> E,K ~=> I,huge ~=> C] lbl101 ~> lbl101 [L ~=> E] lbl101 ~> lbl53 [I ~=> M,L ~=> I] lbl71 ~> lbl101 [K ~=> E] lbl71 ~> lbl53 [I ~=> M,L ~=> I] lbl53 ~> lbl121 [huge ~=> A] lbl53 ~> lbl71 [I ~=> E,huge ~=> C] lbl21 ~> stop [O ~=> G] lbl21 ~> lbl71 [O ~=> G,K ~=> E,K ~=> I,huge ~=> C] start0 ~> start [B ~=> A,D ~=> C,F ~=> E,H ~=> G,J ~=> I,L ~=> K,N ~=> M,P ~=> O] lbl123 ~> exitus616 [] lbl21 ~> exitus616 [] + Loop: [A ~*> 0.0,G ~*> 0.0,K ~*> 0.0] lbl71 ~> lbl53 [I ~=> M,L ~=> I] lbl123 ~> lbl71 [K ~=> E,K ~=> I,huge ~=> C] lbl121 ~> lbl123 [A ~=> G] lbl53 ~> lbl121 [huge ~=> A] lbl101 ~> lbl53 [I ~=> M,L ~=> I] lbl101 ~> lbl101 [L ~=> E] lbl71 ~> lbl101 [K ~=> E] lbl53 ~> lbl71 [I ~=> E,huge ~=> C] + Loop: [I ~+> 0.0.0,M ~+> 0.0.0,K ~+> 0.0.0,O ~*> 0.0.0] lbl71 ~> lbl53 [I ~=> M,L ~=> I] lbl53 ~> lbl71 [I ~=> E,huge ~=> C] lbl101 ~> lbl53 [I ~=> M,L ~=> I] lbl101 ~> lbl101 [L ~=> E] lbl71 ~> lbl101 [K ~=> E] + Loop: [E ~+> 0.0.0.0,K ~+> 0.0.0.0] lbl101 ~> lbl101 [L ~=> E] + Applied Processor: LareProcessor + Details: Unknown bound. MAYBE