MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f1(A,1 + B,D,Z,D,A1,B,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [A >= 1 + B && B >= 0] (?,1) 1. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [B1 >= 1 + H && I >= 0 && A1 >= 1 + B1 && Z >= 2 && J = 0] (?,1) 2. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [B1 >= 1 + H && I >= 0 && B1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 3. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [H >= 1 + B1 && I >= 0 && A1 >= 1 + B1 && Z >= 2 && J = 0] (?,1) 4. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [H >= 1 + B1 && I >= 0 && B1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 5. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f10(A,B,C,D,E,F,G,G1,I,F1,Z,B1,C1,D1,E1,H1,A1,R,S,T,U,V,W,X,Y) [I >= 0 && 0 >= 1 + B1 && Z >= 2 && J = H] (?,1) 6. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f10(A,B,C,D,E,F,G,G1,I,F1,Z,B1,C1,D1,E1,H1,A1,R,S,T,U,V,W,X,Y) [I >= 0 && B1 >= 1 && Z >= 2 && J = H] (?,1) 7. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 8. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 9. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 10. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 11. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f10(A,B,C,D,E,F,G,F1,I,E1,Z,L,B1,C1,D1,G1,A1,R,S,T,U,V,W,X,Y) [Z >= 2 && R >= 0 && J = H] (?,1) 12. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f10(B1,D1,C1,K1,H1,F,G,P1,I,O1,A1,0,L1,M1,N1,Q1,F1,R,S,T,Z,E1,G1,X,Y) [0 >= I1 && 0 >= A1 && 0 >= J1] (1,1) 13. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f1(A1,2,B1,C1,B1,F,G,H,I,J,A1,L,M,N,O,P,Q,R,S,T,Z,V,B1,D1,Y) [A1 >= 2] (1,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2 && 0 >= 1 + C] (?,1) 15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] (?,1) 16. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] (?,1) 17. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2 && C >= 1] (?,1) Signature: {(f1,25);(f10,25);(f7,25);(f8,25);(f9,25)} Flow Graph: [0->{0,14,15,16,17},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7 ,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{},13->{0,14,15,16,17},14->{7,8,9 ,10,11},15->{7,8,9,10,11},16->{7,8,9,10,11},17->{7,8,9,10,11}] + Applied Processor: ArgumentFilter [3,4,5,6,10,11,12,13,14,15,16,18,19,20,21,22,23,24] + Details: We remove following argument positions: [3,4,5,6,10,11,12,13,14,15,16,18,19,20,21,22,23,24]. * Step 2: UnsatRules MAYBE + Considered Problem: Rules: 0. f1(A,B,C,H,I,J,R) -> f1(A,1 + B,D,H,I,J,R) [A >= 1 + B && B >= 0] (?,1) 1. f7(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,R) [B1 >= 1 + H && I >= 0 && A1 >= 1 + B1 && Z >= 2 && J = 0] (?,1) 2. f7(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,R) [B1 >= 1 + H && I >= 0 && B1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 3. f7(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,R) [H >= 1 + B1 && I >= 0 && A1 >= 1 + B1 && Z >= 2 && J = 0] (?,1) 4. f7(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,R) [H >= 1 + B1 && I >= 0 && B1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 5. f7(A,B,C,H,I,J,R) -> f10(A,B,C,G1,I,F1,R) [I >= 0 && 0 >= 1 + B1 && Z >= 2 && J = H] (?,1) 6. f7(A,B,C,H,I,J,R) -> f10(A,B,C,G1,I,F1,R) [I >= 0 && B1 >= 1 && Z >= 2 && J = H] (?,1) 7. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 8. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 9. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 10. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 11. f8(A,B,C,H,I,J,R) -> f10(A,B,C,F1,I,E1,R) [Z >= 2 && R >= 0 && J = H] (?,1) 12. f9(A,B,C,H,I,J,R) -> f10(B1,D1,C1,P1,I,O1,R) [0 >= I1 && 0 >= A1 && 0 >= J1] (1,1) 13. f9(A,B,C,H,I,J,R) -> f1(A1,2,B1,H,I,J,R) [A1 >= 2] (1,1) 14. f1(A,B,C,H,I,J,R) -> f8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2 && 0 >= 1 + C] (?,1) 15. f1(A,B,C,H,I,J,R) -> f8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] (?,1) 16. f1(A,B,C,H,I,J,R) -> f8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] (?,1) 17. f1(A,B,C,H,I,J,R) -> f8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2 && C >= 1] (?,1) Signature: {(f1,25);(f10,25);(f7,25);(f8,25);(f9,25)} Flow Graph: [0->{0,14,15,16,17},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7 ,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{},13->{0,14,15,16,17},14->{7,8,9 ,10,11},15->{7,8,9,10,11},16->{7,8,9,10,11},17->{7,8,9,10,11}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [14,17] * Step 3: UnreachableRules MAYBE + Considered Problem: Rules: 0. f1(A,B,C,H,I,J,R) -> f1(A,1 + B,D,H,I,J,R) [A >= 1 + B && B >= 0] (?,1) 1. f7(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,R) [B1 >= 1 + H && I >= 0 && A1 >= 1 + B1 && Z >= 2 && J = 0] (?,1) 2. f7(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,R) [B1 >= 1 + H && I >= 0 && B1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 3. f7(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,R) [H >= 1 + B1 && I >= 0 && A1 >= 1 + B1 && Z >= 2 && J = 0] (?,1) 4. f7(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,R) [H >= 1 + B1 && I >= 0 && B1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 5. f7(A,B,C,H,I,J,R) -> f10(A,B,C,G1,I,F1,R) [I >= 0 && 0 >= 1 + B1 && Z >= 2 && J = H] (?,1) 6. f7(A,B,C,H,I,J,R) -> f10(A,B,C,G1,I,F1,R) [I >= 0 && B1 >= 1 && Z >= 2 && J = H] (?,1) 7. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 8. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 9. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 10. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 11. f8(A,B,C,H,I,J,R) -> f10(A,B,C,F1,I,E1,R) [Z >= 2 && R >= 0 && J = H] (?,1) 12. f9(A,B,C,H,I,J,R) -> f10(B1,D1,C1,P1,I,O1,R) [0 >= I1 && 0 >= A1 && 0 >= J1] (1,1) 13. f9(A,B,C,H,I,J,R) -> f1(A1,2,B1,H,I,J,R) [A1 >= 2] (1,1) 15. f1(A,B,C,H,I,J,R) -> f8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] (?,1) 16. f1(A,B,C,H,I,J,R) -> f8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] (?,1) Signature: {(f1,25);(f10,25);(f7,25);(f8,25);(f9,25)} Flow Graph: [0->{0,15,16},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7,8,9,10 ,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{},13->{0,15,16},15->{7,8,9,10,11} ,16->{7,8,9,10,11}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [1,2,3,4,5,6] * Step 4: UnsatPaths MAYBE + Considered Problem: Rules: 0. f1(A,B,C,H,I,J,R) -> f1(A,1 + B,D,H,I,J,R) [A >= 1 + B && B >= 0] (?,1) 7. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 8. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 9. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 10. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 11. f8(A,B,C,H,I,J,R) -> f10(A,B,C,F1,I,E1,R) [Z >= 2 && R >= 0 && J = H] (?,1) 12. f9(A,B,C,H,I,J,R) -> f10(B1,D1,C1,P1,I,O1,R) [0 >= I1 && 0 >= A1 && 0 >= J1] (1,1) 13. f9(A,B,C,H,I,J,R) -> f1(A1,2,B1,H,I,J,R) [A1 >= 2] (1,1) 15. f1(A,B,C,H,I,J,R) -> f8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] (?,1) 16. f1(A,B,C,H,I,J,R) -> f8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] (?,1) Signature: {(f1,25);(f10,25);(f7,25);(f8,25);(f9,25)} Flow Graph: [0->{0,15,16},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{},13->{0,15 ,16},15->{7,8,9,10,11},16->{7,8,9,10,11}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(15,11),(16,11)] * Step 5: FromIts MAYBE + Considered Problem: Rules: 0. f1(A,B,C,H,I,J,R) -> f1(A,1 + B,D,H,I,J,R) [A >= 1 + B && B >= 0] (?,1) 7. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 8. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 9. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 10. f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 11. f8(A,B,C,H,I,J,R) -> f10(A,B,C,F1,I,E1,R) [Z >= 2 && R >= 0 && J = H] (?,1) 12. f9(A,B,C,H,I,J,R) -> f10(B1,D1,C1,P1,I,O1,R) [0 >= I1 && 0 >= A1 && 0 >= J1] (1,1) 13. f9(A,B,C,H,I,J,R) -> f1(A1,2,B1,H,I,J,R) [A1 >= 2] (1,1) 15. f1(A,B,C,H,I,J,R) -> f8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] (?,1) 16. f1(A,B,C,H,I,J,R) -> f8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] (?,1) Signature: {(f1,25);(f10,25);(f7,25);(f8,25);(f9,25)} Flow Graph: [0->{0,15,16},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{},13->{0,15 ,16},15->{7,8,9,10},16->{7,8,9,10}] + Applied Processor: FromIts + Details: () * Step 6: Unfold MAYBE + Considered Problem: Rules: f1(A,B,C,H,I,J,R) -> f1(A,1 + B,D,H,I,J,R) [A >= 1 + B && B >= 0] f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8(A,B,C,H,I,J,R) -> f8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8(A,B,C,H,I,J,R) -> f10(A,B,C,F1,I,E1,R) [Z >= 2 && R >= 0 && J = H] f9(A,B,C,H,I,J,R) -> f10(B1,D1,C1,P1,I,O1,R) [0 >= I1 && 0 >= A1 && 0 >= J1] f9(A,B,C,H,I,J,R) -> f1(A1,2,B1,H,I,J,R) [A1 >= 2] f1(A,B,C,H,I,J,R) -> f8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] f1(A,B,C,H,I,J,R) -> f8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] Signature: {(f1,25);(f10,25);(f7,25);(f8,25);(f9,25)} Rule Graph: [0->{0,15,16},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{},13->{0,15 ,16},15->{7,8,9,10},16->{7,8,9,10}] + Applied Processor: Unfold + Details: () * Step 7: AddSinks MAYBE + Considered Problem: Rules: f1.0(A,B,C,H,I,J,R) -> f1.0(A,1 + B,D,H,I,J,R) [A >= 1 + B && B >= 0] f1.0(A,B,C,H,I,J,R) -> f1.15(A,1 + B,D,H,I,J,R) [A >= 1 + B && B >= 0] f1.0(A,B,C,H,I,J,R) -> f1.16(A,1 + B,D,H,I,J,R) [A >= 1 + B && B >= 0] f8.7(A,B,C,H,I,J,R) -> f8.7(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.7(A,B,C,H,I,J,R) -> f8.8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.7(A,B,C,H,I,J,R) -> f8.9(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.7(A,B,C,H,I,J,R) -> f8.10(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.7(A,B,C,H,I,J,R) -> f8.11(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.7(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.9(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.10(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.11(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.7(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.9(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.10(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.11(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.7(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.9(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.10(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.11(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.11(A,B,C,H,I,J,R) -> f10.17(A,B,C,F1,I,E1,R) [Z >= 2 && R >= 0 && J = H] f9.12(A,B,C,H,I,J,R) -> f10.17(B1,D1,C1,P1,I,O1,R) [0 >= I1 && 0 >= A1 && 0 >= J1] f9.13(A,B,C,H,I,J,R) -> f1.0(A1,2,B1,H,I,J,R) [A1 >= 2] f9.13(A,B,C,H,I,J,R) -> f1.15(A1,2,B1,H,I,J,R) [A1 >= 2] f9.13(A,B,C,H,I,J,R) -> f1.16(A1,2,B1,H,I,J,R) [A1 >= 2] f1.15(A,B,C,H,I,J,R) -> f8.7(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] f1.15(A,B,C,H,I,J,R) -> f8.8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] f1.15(A,B,C,H,I,J,R) -> f8.9(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] f1.15(A,B,C,H,I,J,R) -> f8.10(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] f1.16(A,B,C,H,I,J,R) -> f8.7(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] f1.16(A,B,C,H,I,J,R) -> f8.8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] f1.16(A,B,C,H,I,J,R) -> f8.9(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] f1.16(A,B,C,H,I,J,R) -> f8.10(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] Signature: {(f1.0,7) ;(f1.15,7) ;(f1.16,7) ;(f10.17,7) ;(f8.10,7) ;(f8.11,7) ;(f8.7,7) ;(f8.8,7) ;(f8.9,7) ;(f9.12,7) ;(f9.13,7)} Rule Graph: [0->{0,1,2},1->{28,29,30,31},2->{32,33,34,35},3->{3,4,5,6,7},4->{8,9,10,11,12},5->{13,14,15,16,17},6->{18 ,19,20,21,22},7->{23},8->{3,4,5,6,7},9->{8,9,10,11,12},10->{13,14,15,16,17},11->{18,19,20,21,22},12->{23} ,13->{3,4,5,6,7},14->{8,9,10,11,12},15->{13,14,15,16,17},16->{18,19,20,21,22},17->{23},18->{3,4,5,6,7} ,19->{8,9,10,11,12},20->{13,14,15,16,17},21->{18,19,20,21,22},22->{23},23->{},24->{},25->{0,1,2},26->{28,29 ,30,31},27->{32,33,34,35},28->{3,4,5,6,7},29->{8,9,10,11,12},30->{13,14,15,16,17},31->{18,19,20,21,22} ,32->{3,4,5,6,7},33->{8,9,10,11,12},34->{13,14,15,16,17},35->{18,19,20,21,22}] + Applied Processor: AddSinks + Details: () * Step 8: Decompose MAYBE + Considered Problem: Rules: f1.0(A,B,C,H,I,J,R) -> f1.0(A,1 + B,D,H,I,J,R) [A >= 1 + B && B >= 0] f1.0(A,B,C,H,I,J,R) -> f1.15(A,1 + B,D,H,I,J,R) [A >= 1 + B && B >= 0] f1.0(A,B,C,H,I,J,R) -> f1.16(A,1 + B,D,H,I,J,R) [A >= 1 + B && B >= 0] f8.7(A,B,C,H,I,J,R) -> f8.7(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.7(A,B,C,H,I,J,R) -> f8.8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.7(A,B,C,H,I,J,R) -> f8.9(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.7(A,B,C,H,I,J,R) -> f8.10(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.7(A,B,C,H,I,J,R) -> f8.11(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.7(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.9(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.10(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.11(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.7(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.9(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.10(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.11(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.7(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.9(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.10(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.11(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.11(A,B,C,H,I,J,R) -> f10.17(A,B,C,F1,I,E1,R) [Z >= 2 && R >= 0 && J = H] f9.12(A,B,C,H,I,J,R) -> f10.17(B1,D1,C1,P1,I,O1,R) [0 >= I1 && 0 >= A1 && 0 >= J1] f9.13(A,B,C,H,I,J,R) -> f1.0(A1,2,B1,H,I,J,R) [A1 >= 2] f9.13(A,B,C,H,I,J,R) -> f1.15(A1,2,B1,H,I,J,R) [A1 >= 2] f9.13(A,B,C,H,I,J,R) -> f1.16(A1,2,B1,H,I,J,R) [A1 >= 2] f1.15(A,B,C,H,I,J,R) -> f8.7(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] f1.15(A,B,C,H,I,J,R) -> f8.8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] f1.15(A,B,C,H,I,J,R) -> f8.9(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] f1.15(A,B,C,H,I,J,R) -> f8.10(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] f1.16(A,B,C,H,I,J,R) -> f8.7(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] f1.16(A,B,C,H,I,J,R) -> f8.8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] f1.16(A,B,C,H,I,J,R) -> f8.9(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] f1.16(A,B,C,H,I,J,R) -> f8.10(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True Signature: {(exitus616,7) ;(f1.0,7) ;(f1.15,7) ;(f1.16,7) ;(f10.17,7) ;(f8.10,7) ;(f8.11,7) ;(f8.7,7) ;(f8.8,7) ;(f8.9,7) ;(f9.12,7) ;(f9.13,7)} Rule Graph: [0->{0,1,2},1->{28,29,30,31},2->{32,33,34,35},3->{3,4,5,6,7},4->{8,9,10,11,12},5->{13,14,15,16,17},6->{18 ,19,20,21,22},7->{23},8->{3,4,5,6,7},9->{8,9,10,11,12},10->{13,14,15,16,17},11->{18,19,20,21,22},12->{23} ,13->{3,4,5,6,7},14->{8,9,10,11,12},15->{13,14,15,16,17},16->{18,19,20,21,22},17->{23},18->{3,4,5,6,7} ,19->{8,9,10,11,12},20->{13,14,15,16,17},21->{18,19,20,21,22},22->{23},23->{36,37,38,39,40,41,42,43,44,45,46 ,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82 ,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99},24->{100},25->{0,1,2},26->{28,29,30,31},27->{32,33,34 ,35},28->{3,4,5,6,7},29->{8,9,10,11,12},30->{13,14,15,16,17},31->{18,19,20,21,22},32->{3,4,5,6,7},33->{8,9 ,10,11,12},34->{13,14,15,16,17},35->{18,19,20,21,22}] + 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,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100] | +- p:[0] c: [0] | `- p:[3,8,4,13,5,18,6,11,9,14,10,19,16,15,20,21] c: [3,4,5,6,8,9,10,11,13,14,15,16,18,19,20,21] * Step 9: AbstractSize MAYBE + Considered Problem: (Rules: f1.0(A,B,C,H,I,J,R) -> f1.0(A,1 + B,D,H,I,J,R) [A >= 1 + B && B >= 0] f1.0(A,B,C,H,I,J,R) -> f1.15(A,1 + B,D,H,I,J,R) [A >= 1 + B && B >= 0] f1.0(A,B,C,H,I,J,R) -> f1.16(A,1 + B,D,H,I,J,R) [A >= 1 + B && B >= 0] f8.7(A,B,C,H,I,J,R) -> f8.7(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.7(A,B,C,H,I,J,R) -> f8.8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.7(A,B,C,H,I,J,R) -> f8.9(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.7(A,B,C,H,I,J,R) -> f8.10(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.7(A,B,C,H,I,J,R) -> f8.11(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.7(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.8(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.9(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.10(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.8(A,B,C,H,I,J,R) -> f8.11(A,B,C,H,I,0,-1 + R) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.7(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.9(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.10(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.9(A,B,C,H,I,J,R) -> f8.11(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.7(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.8(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.9(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.10(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.10(A,B,C,H,I,J,R) -> f8.11(A,B,C,H,I,0,-1 + R) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] f8.11(A,B,C,H,I,J,R) -> f10.17(A,B,C,F1,I,E1,R) [Z >= 2 && R >= 0 && J = H] f9.12(A,B,C,H,I,J,R) -> f10.17(B1,D1,C1,P1,I,O1,R) [0 >= I1 && 0 >= A1 && 0 >= J1] f9.13(A,B,C,H,I,J,R) -> f1.0(A1,2,B1,H,I,J,R) [A1 >= 2] f9.13(A,B,C,H,I,J,R) -> f1.15(A1,2,B1,H,I,J,R) [A1 >= 2] f9.13(A,B,C,H,I,J,R) -> f1.16(A1,2,B1,H,I,J,R) [A1 >= 2] f1.15(A,B,C,H,I,J,R) -> f8.7(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] f1.15(A,B,C,H,I,J,R) -> f8.8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] f1.15(A,B,C,H,I,J,R) -> f8.9(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] f1.15(A,B,C,H,I,J,R) -> f8.10(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2] f1.16(A,B,C,H,I,J,R) -> f8.7(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] f1.16(A,B,C,H,I,J,R) -> f8.8(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] f1.16(A,B,C,H,I,J,R) -> f8.9(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] f1.16(A,B,C,H,I,J,R) -> f8.10(A1,C1,B1,C,R,0,R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True f10.17(A,B,C,H,I,J,R) -> exitus616(A,B,C,H,I,J,R) True Signature: {(exitus616,7) ;(f1.0,7) ;(f1.15,7) ;(f1.16,7) ;(f10.17,7) ;(f8.10,7) ;(f8.11,7) ;(f8.7,7) ;(f8.8,7) ;(f8.9,7) ;(f9.12,7) ;(f9.13,7)} Rule Graph: [0->{0,1,2},1->{28,29,30,31},2->{32,33,34,35},3->{3,4,5,6,7},4->{8,9,10,11,12},5->{13,14,15,16,17},6->{18 ,19,20,21,22},7->{23},8->{3,4,5,6,7},9->{8,9,10,11,12},10->{13,14,15,16,17},11->{18,19,20,21,22},12->{23} ,13->{3,4,5,6,7},14->{8,9,10,11,12},15->{13,14,15,16,17},16->{18,19,20,21,22},17->{23},18->{3,4,5,6,7} ,19->{8,9,10,11,12},20->{13,14,15,16,17},21->{18,19,20,21,22},22->{23},23->{36,37,38,39,40,41,42,43,44,45,46 ,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82 ,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99},24->{100},25->{0,1,2},26->{28,29,30,31},27->{32,33,34 ,35},28->{3,4,5,6,7},29->{8,9,10,11,12},30->{13,14,15,16,17},31->{18,19,20,21,22},32->{3,4,5,6,7},33->{8,9 ,10,11,12},34->{13,14,15,16,17},35->{18,19,20,21,22}] ,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,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100] | +- p:[0] c: [0] | `- p:[3,8,4,13,5,18,6,11,9,14,10,19,16,15,20,21] c: [3,4,5,6,8,9,10,11,13,14,15,16,18,19,20,21]) + Applied Processor: AbstractSize Minimize + Details: () * Step 10: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,H,I,J,R,0.0,0.1] f1.0 ~> f1.0 [A <= A, B <= A, C <= unknown, H <= H, I <= I, J <= J, R <= R] f1.0 ~> f1.15 [A <= A, B <= A, C <= unknown, H <= H, I <= I, J <= J, R <= R] f1.0 ~> f1.16 [A <= A, B <= A, C <= unknown, H <= H, I <= I, J <= J, R <= R] f8.7 ~> f8.7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.7 ~> f8.8 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.7 ~> f8.9 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.7 ~> f8.10 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.7 ~> f8.11 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.8 ~> f8.7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.8 ~> f8.8 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.8 ~> f8.9 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.8 ~> f8.10 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.8 ~> f8.11 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.9 ~> f8.7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.9 ~> f8.8 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.9 ~> f8.9 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.9 ~> f8.10 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.9 ~> f8.11 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.10 ~> f8.7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.10 ~> f8.8 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.10 ~> f8.9 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.10 ~> f8.10 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.10 ~> f8.11 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.11 ~> f10.17 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= unknown, R <= R] f9.12 ~> f10.17 [A <= unknown, B <= unknown, C <= unknown, H <= unknown, I <= I, J <= unknown, R <= R] f9.13 ~> f1.0 [A <= unknown, B <= 2*K, C <= unknown, H <= H, I <= I, J <= J, R <= R] f9.13 ~> f1.15 [A <= unknown, B <= 2*K, C <= unknown, H <= H, I <= I, J <= J, R <= R] f9.13 ~> f1.16 [A <= unknown, B <= 2*K, C <= unknown, H <= H, I <= I, J <= J, R <= R] f1.15 ~> f8.7 [A <= unknown, B <= unknown, C <= unknown, H <= C, I <= R, J <= 0*K, R <= R] f1.15 ~> f8.8 [A <= unknown, B <= unknown, C <= unknown, H <= C, I <= R, J <= 0*K, R <= R] f1.15 ~> f8.9 [A <= unknown, B <= unknown, C <= unknown, H <= C, I <= R, J <= 0*K, R <= R] f1.15 ~> f8.10 [A <= unknown, B <= unknown, C <= unknown, H <= C, I <= R, J <= 0*K, R <= R] f1.16 ~> f8.7 [A <= unknown, B <= unknown, C <= unknown, H <= C, I <= R, J <= 0*K, R <= R] f1.16 ~> f8.8 [A <= unknown, B <= unknown, C <= unknown, H <= C, I <= R, J <= 0*K, R <= R] f1.16 ~> f8.9 [A <= unknown, B <= unknown, C <= unknown, H <= C, I <= R, J <= 0*K, R <= R] f1.16 ~> f8.10 [A <= unknown, B <= unknown, C <= unknown, H <= C, I <= R, J <= 0*K, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] f10.17 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, R <= R] + Loop: [0.0 <= K + A + B] f1.0 ~> f1.0 [A <= A, B <= A, C <= unknown, H <= H, I <= I, J <= J, R <= R] + Loop: [0.1 <= K + R] f8.7 ~> f8.7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.8 ~> f8.7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.7 ~> f8.8 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.9 ~> f8.7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.7 ~> f8.9 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.10 ~> f8.7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.7 ~> f8.10 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.8 ~> f8.10 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.8 ~> f8.8 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.9 ~> f8.8 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.8 ~> f8.9 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.10 ~> f8.8 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.9 ~> f8.10 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.9 ~> f8.9 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.10 ~> f8.9 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] f8.10 ~> f8.10 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= 0*K, R <= K + R] + Applied Processor: AbstractFlow + Details: () * Step 11: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,H,I,J,R,0.0,0.1] f1.0 ~> f1.0 [A ~=> B,huge ~=> C] f1.0 ~> f1.15 [A ~=> B,huge ~=> C] f1.0 ~> f1.16 [A ~=> B,huge ~=> C] f8.7 ~> f8.7 [K ~=> J,R ~+> R,K ~+> R] f8.7 ~> f8.8 [K ~=> J,R ~+> R,K ~+> R] f8.7 ~> f8.9 [K ~=> J,R ~+> R,K ~+> R] f8.7 ~> f8.10 [K ~=> J,R ~+> R,K ~+> R] f8.7 ~> f8.11 [K ~=> J,R ~+> R,K ~+> R] f8.8 ~> f8.7 [K ~=> J,R ~+> R,K ~+> R] f8.8 ~> f8.8 [K ~=> J,R ~+> R,K ~+> R] f8.8 ~> f8.9 [K ~=> J,R ~+> R,K ~+> R] f8.8 ~> f8.10 [K ~=> J,R ~+> R,K ~+> R] f8.8 ~> f8.11 [K ~=> J,R ~+> R,K ~+> R] f8.9 ~> f8.7 [K ~=> J,R ~+> R,K ~+> R] f8.9 ~> f8.8 [K ~=> J,R ~+> R,K ~+> R] f8.9 ~> f8.9 [K ~=> J,R ~+> R,K ~+> R] f8.9 ~> f8.10 [K ~=> J,R ~+> R,K ~+> R] f8.9 ~> f8.11 [K ~=> J,R ~+> R,K ~+> R] f8.10 ~> f8.7 [K ~=> J,R ~+> R,K ~+> R] f8.10 ~> f8.8 [K ~=> J,R ~+> R,K ~+> R] f8.10 ~> f8.9 [K ~=> J,R ~+> R,K ~+> R] f8.10 ~> f8.10 [K ~=> J,R ~+> R,K ~+> R] f8.10 ~> f8.11 [K ~=> J,R ~+> R,K ~+> R] f8.11 ~> f10.17 [huge ~=> H,huge ~=> J] f9.12 ~> f10.17 [huge ~=> A,huge ~=> B,huge ~=> C,huge ~=> H,huge ~=> J] f9.13 ~> f1.0 [K ~=> B,huge ~=> A,huge ~=> C] f9.13 ~> f1.15 [K ~=> B,huge ~=> A,huge ~=> C] f9.13 ~> f1.16 [K ~=> B,huge ~=> A,huge ~=> C] f1.15 ~> f8.7 [C ~=> H,R ~=> I,K ~=> J,huge ~=> A,huge ~=> B,huge ~=> C] f1.15 ~> f8.8 [C ~=> H,R ~=> I,K ~=> J,huge ~=> A,huge ~=> B,huge ~=> C] f1.15 ~> f8.9 [C ~=> H,R ~=> I,K ~=> J,huge ~=> A,huge ~=> B,huge ~=> C] f1.15 ~> f8.10 [C ~=> H,R ~=> I,K ~=> J,huge ~=> A,huge ~=> B,huge ~=> C] f1.16 ~> f8.7 [C ~=> H,R ~=> I,K ~=> J,huge ~=> A,huge ~=> B,huge ~=> C] f1.16 ~> f8.8 [C ~=> H,R ~=> I,K ~=> J,huge ~=> A,huge ~=> B,huge ~=> C] f1.16 ~> f8.9 [C ~=> H,R ~=> I,K ~=> J,huge ~=> A,huge ~=> B,huge ~=> C] f1.16 ~> f8.10 [C ~=> H,R ~=> I,K ~=> J,huge ~=> A,huge ~=> B,huge ~=> C] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] f10.17 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f1.0 ~> f1.0 [A ~=> B,huge ~=> C] + Loop: [R ~+> 0.1,K ~+> 0.1] f8.7 ~> f8.7 [K ~=> J,R ~+> R,K ~+> R] f8.8 ~> f8.7 [K ~=> J,R ~+> R,K ~+> R] f8.7 ~> f8.8 [K ~=> J,R ~+> R,K ~+> R] f8.9 ~> f8.7 [K ~=> J,R ~+> R,K ~+> R] f8.7 ~> f8.9 [K ~=> J,R ~+> R,K ~+> R] f8.10 ~> f8.7 [K ~=> J,R ~+> R,K ~+> R] f8.7 ~> f8.10 [K ~=> J,R ~+> R,K ~+> R] f8.8 ~> f8.10 [K ~=> J,R ~+> R,K ~+> R] f8.8 ~> f8.8 [K ~=> J,R ~+> R,K ~+> R] f8.9 ~> f8.8 [K ~=> J,R ~+> R,K ~+> R] f8.8 ~> f8.9 [K ~=> J,R ~+> R,K ~+> R] f8.10 ~> f8.8 [K ~=> J,R ~+> R,K ~+> R] f8.9 ~> f8.10 [K ~=> J,R ~+> R,K ~+> R] f8.9 ~> f8.9 [K ~=> J,R ~+> R,K ~+> R] f8.10 ~> f8.9 [K ~=> J,R ~+> R,K ~+> R] f8.10 ~> f8.10 [K ~=> J,R ~+> R,K ~+> R] + Applied Processor: Lare + Details: Unknown bound. MAYBE