YES(?,PRIMREC) * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H) -> f0(A,B,C,D,E,F,G,H) True (1,1) 1. f0(A,B,C,D,E,F,G,H) -> f58(A,B,C,D,E,F,G,H) [B >= A] (?,1) 2. f0(A,B,C,D,E,F,G,H) -> f12(A,B,0,B,E,F,G,H) [A >= 1 + B] (?,1) 3. f12(A,B,C,D,E,F,G,H) -> f35(A,B,C,B,E,F,G,H) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] (?,1) 4. f12(A,B,C,D,E,F,G,H) -> f12(A,B,J,E,1 + E,I,K,H) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] (?,1) 5. f12(A,B,C,D,E,F,G,H) -> f12(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] (?,1) 6. f35(A,B,C,D,E,F,G,H) -> f0(A,1 + B,0,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] (?,1) 7. f35(A,B,C,D,E,F,G,H) -> f37(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] (?,1) 8. f35(A,B,C,D,E,F,G,H) -> f37(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] (?,1) 9. f12(A,B,C,D,E,F,G,H) -> f22(A,B,C,D,E,F,G,H) [-1 + A + -1*B >= 0 && D >= 1 + B && E >= 1 + A] (?,1) 10. f12(A,B,C,D,E,F,G,H) -> f22(A,B,C,D,E,F,G,H) [-1 + A + -1*B >= 0 && B >= 1 + D && E >= 1 + A] (?,1) 11. f22(A,B,C,D,E,F,G,H) -> f29(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] (?,1) 12. f37(A,B,C,D,E,F,G,H) -> f0(A,1 + B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] (?,1) 13. f37(A,B,C,D,E,F,G,H) -> f37(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] (?,1) 14. f37(A,B,C,D,E,F,G,H) -> f43(A,B,C,D,E,F,G,J) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D && I >= 1] (?,1) 15. f37(A,B,C,D,E,F,G,H) -> f43(A,B,C,D,E,F,G,J) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D && 0 >= 1 + I] (?,1) 16. f29(A,B,C,D,E,F,G,H) -> f35(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] (?,1) 17. f43(A,B,C,D,E,F,G,H) -> f48(A,B,C,D,E,F,G,H) [-1 + -1*D + E >= 0 (?,1) && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] 18. f48(A,B,C,D,E,F,G,H) -> f37(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 (?,1) && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] Signature: {(f0,8);(f12,8);(f22,8);(f29,8);(f35,8);(f37,8);(f43,8);(f48,8);(f58,8);(start,8)} Flow Graph: [0->{1,2},1->{},2->{3,4,5,9,10},3->{6,7,8},4->{3,4,5,9,10},5->{3,4,5,9,10},6->{1,2},7->{12,13,14,15} ,8->{12,13,14,15},9->{11},10->{11},11->{16},12->{1,2},13->{12,13,14,15},14->{17},15->{17},16->{6,7,8} ,17->{18},18->{12,13,14,15}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,9),(2,10),(4,3),(4,10)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H) -> f0(A,B,C,D,E,F,G,H) True (1,1) 1. f0(A,B,C,D,E,F,G,H) -> f58(A,B,C,D,E,F,G,H) [B >= A] (?,1) 2. f0(A,B,C,D,E,F,G,H) -> f12(A,B,0,B,E,F,G,H) [A >= 1 + B] (?,1) 3. f12(A,B,C,D,E,F,G,H) -> f35(A,B,C,B,E,F,G,H) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] (?,1) 4. f12(A,B,C,D,E,F,G,H) -> f12(A,B,J,E,1 + E,I,K,H) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] (?,1) 5. f12(A,B,C,D,E,F,G,H) -> f12(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] (?,1) 6. f35(A,B,C,D,E,F,G,H) -> f0(A,1 + B,0,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] (?,1) 7. f35(A,B,C,D,E,F,G,H) -> f37(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] (?,1) 8. f35(A,B,C,D,E,F,G,H) -> f37(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] (?,1) 9. f12(A,B,C,D,E,F,G,H) -> f22(A,B,C,D,E,F,G,H) [-1 + A + -1*B >= 0 && D >= 1 + B && E >= 1 + A] (?,1) 10. f12(A,B,C,D,E,F,G,H) -> f22(A,B,C,D,E,F,G,H) [-1 + A + -1*B >= 0 && B >= 1 + D && E >= 1 + A] (?,1) 11. f22(A,B,C,D,E,F,G,H) -> f29(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] (?,1) 12. f37(A,B,C,D,E,F,G,H) -> f0(A,1 + B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] (?,1) 13. f37(A,B,C,D,E,F,G,H) -> f37(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] (?,1) 14. f37(A,B,C,D,E,F,G,H) -> f43(A,B,C,D,E,F,G,J) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D && I >= 1] (?,1) 15. f37(A,B,C,D,E,F,G,H) -> f43(A,B,C,D,E,F,G,J) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D && 0 >= 1 + I] (?,1) 16. f29(A,B,C,D,E,F,G,H) -> f35(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] (?,1) 17. f43(A,B,C,D,E,F,G,H) -> f48(A,B,C,D,E,F,G,H) [-1 + -1*D + E >= 0 (?,1) && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] 18. f48(A,B,C,D,E,F,G,H) -> f37(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 (?,1) && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] Signature: {(f0,8);(f12,8);(f22,8);(f29,8);(f35,8);(f37,8);(f43,8);(f48,8);(f58,8);(start,8)} Flow Graph: [0->{1,2},1->{},2->{3,4,5},3->{6,7,8},4->{4,5,9},5->{3,4,5,9,10},6->{1,2},7->{12,13,14,15},8->{12,13,14 ,15},9->{11},10->{11},11->{16},12->{1,2},13->{12,13,14,15},14->{17},15->{17},16->{6,7,8},17->{18},18->{12,13 ,14,15}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: start(A,B,C,D,E,F,G,H) -> f0(A,B,C,D,E,F,G,H) True f0(A,B,C,D,E,F,G,H) -> f58(A,B,C,D,E,F,G,H) [B >= A] f0(A,B,C,D,E,F,G,H) -> f12(A,B,0,B,E,F,G,H) [A >= 1 + B] f12(A,B,C,D,E,F,G,H) -> f35(A,B,C,B,E,F,G,H) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f12(A,B,C,D,E,F,G,H) -> f12(A,B,J,E,1 + E,I,K,H) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f12(A,B,C,D,E,F,G,H) -> f12(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f35(A,B,C,D,E,F,G,H) -> f0(A,1 + B,0,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] f35(A,B,C,D,E,F,G,H) -> f37(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f35(A,B,C,D,E,F,G,H) -> f37(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f12(A,B,C,D,E,F,G,H) -> f22(A,B,C,D,E,F,G,H) [-1 + A + -1*B >= 0 && D >= 1 + B && E >= 1 + A] f12(A,B,C,D,E,F,G,H) -> f22(A,B,C,D,E,F,G,H) [-1 + A + -1*B >= 0 && B >= 1 + D && E >= 1 + A] f22(A,B,C,D,E,F,G,H) -> f29(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f37(A,B,C,D,E,F,G,H) -> f0(A,1 + B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] f37(A,B,C,D,E,F,G,H) -> f37(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f37(A,B,C,D,E,F,G,H) -> f43(A,B,C,D,E,F,G,J) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D && I >= 1] f37(A,B,C,D,E,F,G,H) -> f43(A,B,C,D,E,F,G,J) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D && 0 >= 1 + I] f29(A,B,C,D,E,F,G,H) -> f35(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f43(A,B,C,D,E,F,G,H) -> f48(A,B,C,D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f48(A,B,C,D,E,F,G,H) -> f37(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] Signature: {(f0,8);(f12,8);(f22,8);(f29,8);(f35,8);(f37,8);(f43,8);(f48,8);(f58,8);(start,8)} Rule Graph: [0->{1,2},1->{},2->{3,4,5},3->{6,7,8},4->{4,5,9},5->{3,4,5,9,10},6->{1,2},7->{12,13,14,15},8->{12,13,14 ,15},9->{11},10->{11},11->{16},12->{1,2},13->{12,13,14,15},14->{17},15->{17},16->{6,7,8},17->{18},18->{12,13 ,14,15}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: start.0(A,B,C,D,E,F,G,H) -> f0.1(A,B,C,D,E,F,G,H) True start.0(A,B,C,D,E,F,G,H) -> f0.2(A,B,C,D,E,F,G,H) True f0.1(A,B,C,D,E,F,G,H) -> f58.19(A,B,C,D,E,F,G,H) [B >= A] f0.2(A,B,C,D,E,F,G,H) -> f12.3(A,B,0,B,E,F,G,H) [A >= 1 + B] f0.2(A,B,C,D,E,F,G,H) -> f12.4(A,B,0,B,E,F,G,H) [A >= 1 + B] f0.2(A,B,C,D,E,F,G,H) -> f12.5(A,B,0,B,E,F,G,H) [A >= 1 + B] f12.3(A,B,C,D,E,F,G,H) -> f35.6(A,B,C,B,E,F,G,H) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f12.3(A,B,C,D,E,F,G,H) -> f35.7(A,B,C,B,E,F,G,H) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f12.3(A,B,C,D,E,F,G,H) -> f35.8(A,B,C,B,E,F,G,H) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f12.4(A,B,C,D,E,F,G,H) -> f12.4(A,B,J,E,1 + E,I,K,H) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f12.4(A,B,C,D,E,F,G,H) -> f12.5(A,B,J,E,1 + E,I,K,H) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f12.4(A,B,C,D,E,F,G,H) -> f12.9(A,B,J,E,1 + E,I,K,H) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f12.5(A,B,C,D,E,F,G,H) -> f12.3(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f12.5(A,B,C,D,E,F,G,H) -> f12.4(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f12.5(A,B,C,D,E,F,G,H) -> f12.5(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f12.5(A,B,C,D,E,F,G,H) -> f12.9(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f12.5(A,B,C,D,E,F,G,H) -> f12.10(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f35.6(A,B,C,D,E,F,G,H) -> f0.1(A,1 + B,0,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] f35.6(A,B,C,D,E,F,G,H) -> f0.2(A,1 + B,0,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] f35.7(A,B,C,D,E,F,G,H) -> f37.12(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f35.7(A,B,C,D,E,F,G,H) -> f37.13(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f35.7(A,B,C,D,E,F,G,H) -> f37.14(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f35.7(A,B,C,D,E,F,G,H) -> f37.15(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f35.8(A,B,C,D,E,F,G,H) -> f37.12(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f35.8(A,B,C,D,E,F,G,H) -> f37.13(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f35.8(A,B,C,D,E,F,G,H) -> f37.14(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f35.8(A,B,C,D,E,F,G,H) -> f37.15(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f12.9(A,B,C,D,E,F,G,H) -> f22.11(A,B,C,D,E,F,G,H) [-1 + A + -1*B >= 0 && D >= 1 + B && E >= 1 + A] f12.10(A,B,C,D,E,F,G,H) -> f22.11(A,B,C,D,E,F,G,H) [-1 + A + -1*B >= 0 && B >= 1 + D && E >= 1 + A] f22.11(A,B,C,D,E,F,G,H) -> f29.16(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f37.12(A,B,C,D,E,F,G,H) -> f0.1(A,1 + B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] f37.12(A,B,C,D,E,F,G,H) -> f0.2(A,1 + B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] f37.13(A,B,C,D,E,F,G,H) -> f37.12(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f37.13(A,B,C,D,E,F,G,H) -> f37.13(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f37.13(A,B,C,D,E,F,G,H) -> f37.14(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f37.13(A,B,C,D,E,F,G,H) -> f37.15(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f37.14(A,B,C,D,E,F,G,H) -> f43.17(A,B,C,D,E,F,G,J) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D && I >= 1] f37.15(A,B,C,D,E,F,G,H) -> f43.17(A,B,C,D,E,F,G,J) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D && 0 >= 1 + I] f29.16(A,B,C,D,E,F,G,H) -> f35.6(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f29.16(A,B,C,D,E,F,G,H) -> f35.7(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f29.16(A,B,C,D,E,F,G,H) -> f35.8(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f43.17(A,B,C,D,E,F,G,H) -> f48.18(A,B,C,D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f48.18(A,B,C,D,E,F,G,H) -> f37.12(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f48.18(A,B,C,D,E,F,G,H) -> f37.13(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f48.18(A,B,C,D,E,F,G,H) -> f37.14(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f48.18(A,B,C,D,E,F,G,H) -> f37.15(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] Signature: {(f0.1,8) ;(f0.2,8) ;(f12.10,8) ;(f12.3,8) ;(f12.4,8) ;(f12.5,8) ;(f12.9,8) ;(f22.11,8) ;(f29.16,8) ;(f35.6,8) ;(f35.7,8) ;(f35.8,8) ;(f37.12,8) ;(f37.13,8) ;(f37.14,8) ;(f37.15,8) ;(f43.17,8) ;(f48.18,8) ;(f58.19,8) ;(start.0,8)} Rule Graph: [0->{2},1->{3,4,5},2->{},3->{6,7,8},4->{9,10,11},5->{12,13,14,15,16},6->{17,18},7->{19,20,21,22},8->{23,24 ,25,26},9->{9,10,11},10->{12,13,14,15,16},11->{27},12->{6,7,8},13->{9,10,11},14->{12,13,14,15,16},15->{27} ,16->{28},17->{2},18->{3,4,5},19->{30,31},20->{32,33,34,35},21->{36},22->{37},23->{30,31},24->{32,33,34,35} ,25->{36},26->{37},27->{29},28->{29},29->{38,39,40},30->{2},31->{3,4,5},32->{30,31},33->{32,33,34,35} ,34->{36},35->{37},36->{41},37->{41},38->{17,18},39->{19,20,21,22},40->{23,24,25,26},41->{42,43,44,45} ,42->{30,31},43->{32,33,34,35},44->{36},45->{37}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose MAYBE + Considered Problem: Rules: start.0(A,B,C,D,E,F,G,H) -> f0.1(A,B,C,D,E,F,G,H) True start.0(A,B,C,D,E,F,G,H) -> f0.2(A,B,C,D,E,F,G,H) True f0.1(A,B,C,D,E,F,G,H) -> f58.19(A,B,C,D,E,F,G,H) [B >= A] f0.2(A,B,C,D,E,F,G,H) -> f12.3(A,B,0,B,E,F,G,H) [A >= 1 + B] f0.2(A,B,C,D,E,F,G,H) -> f12.4(A,B,0,B,E,F,G,H) [A >= 1 + B] f0.2(A,B,C,D,E,F,G,H) -> f12.5(A,B,0,B,E,F,G,H) [A >= 1 + B] f12.3(A,B,C,D,E,F,G,H) -> f35.6(A,B,C,B,E,F,G,H) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f12.3(A,B,C,D,E,F,G,H) -> f35.7(A,B,C,B,E,F,G,H) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f12.3(A,B,C,D,E,F,G,H) -> f35.8(A,B,C,B,E,F,G,H) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f12.4(A,B,C,D,E,F,G,H) -> f12.4(A,B,J,E,1 + E,I,K,H) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f12.4(A,B,C,D,E,F,G,H) -> f12.5(A,B,J,E,1 + E,I,K,H) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f12.4(A,B,C,D,E,F,G,H) -> f12.9(A,B,J,E,1 + E,I,K,H) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f12.5(A,B,C,D,E,F,G,H) -> f12.3(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f12.5(A,B,C,D,E,F,G,H) -> f12.4(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f12.5(A,B,C,D,E,F,G,H) -> f12.5(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f12.5(A,B,C,D,E,F,G,H) -> f12.9(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f12.5(A,B,C,D,E,F,G,H) -> f12.10(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f35.6(A,B,C,D,E,F,G,H) -> f0.1(A,1 + B,0,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] f35.6(A,B,C,D,E,F,G,H) -> f0.2(A,1 + B,0,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] f35.7(A,B,C,D,E,F,G,H) -> f37.12(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f35.7(A,B,C,D,E,F,G,H) -> f37.13(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f35.7(A,B,C,D,E,F,G,H) -> f37.14(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f35.7(A,B,C,D,E,F,G,H) -> f37.15(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f35.8(A,B,C,D,E,F,G,H) -> f37.12(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f35.8(A,B,C,D,E,F,G,H) -> f37.13(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f35.8(A,B,C,D,E,F,G,H) -> f37.14(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f35.8(A,B,C,D,E,F,G,H) -> f37.15(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f12.9(A,B,C,D,E,F,G,H) -> f22.11(A,B,C,D,E,F,G,H) [-1 + A + -1*B >= 0 && D >= 1 + B && E >= 1 + A] f12.10(A,B,C,D,E,F,G,H) -> f22.11(A,B,C,D,E,F,G,H) [-1 + A + -1*B >= 0 && B >= 1 + D && E >= 1 + A] f22.11(A,B,C,D,E,F,G,H) -> f29.16(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f37.12(A,B,C,D,E,F,G,H) -> f0.1(A,1 + B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] f37.12(A,B,C,D,E,F,G,H) -> f0.2(A,1 + B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] f37.13(A,B,C,D,E,F,G,H) -> f37.12(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f37.13(A,B,C,D,E,F,G,H) -> f37.13(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f37.13(A,B,C,D,E,F,G,H) -> f37.14(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f37.13(A,B,C,D,E,F,G,H) -> f37.15(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f37.14(A,B,C,D,E,F,G,H) -> f43.17(A,B,C,D,E,F,G,J) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D && I >= 1] f37.15(A,B,C,D,E,F,G,H) -> f43.17(A,B,C,D,E,F,G,J) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D && 0 >= 1 + I] f29.16(A,B,C,D,E,F,G,H) -> f35.6(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f29.16(A,B,C,D,E,F,G,H) -> f35.7(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f29.16(A,B,C,D,E,F,G,H) -> f35.8(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f43.17(A,B,C,D,E,F,G,H) -> f48.18(A,B,C,D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f48.18(A,B,C,D,E,F,G,H) -> f37.12(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f48.18(A,B,C,D,E,F,G,H) -> f37.13(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f48.18(A,B,C,D,E,F,G,H) -> f37.14(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f48.18(A,B,C,D,E,F,G,H) -> f37.15(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f58.19(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f58.19(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f58.19(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True Signature: {(exitus616,8) ;(f0.1,8) ;(f0.2,8) ;(f12.10,8) ;(f12.3,8) ;(f12.4,8) ;(f12.5,8) ;(f12.9,8) ;(f22.11,8) ;(f29.16,8) ;(f35.6,8) ;(f35.7,8) ;(f35.8,8) ;(f37.12,8) ;(f37.13,8) ;(f37.14,8) ;(f37.15,8) ;(f43.17,8) ;(f48.18,8) ;(f58.19,8) ;(start.0,8)} Rule Graph: [0->{2},1->{3,4,5},2->{46,47,48},3->{6,7,8},4->{9,10,11},5->{12,13,14,15,16},6->{17,18},7->{19,20,21,22} ,8->{23,24,25,26},9->{9,10,11},10->{12,13,14,15,16},11->{27},12->{6,7,8},13->{9,10,11},14->{12,13,14,15,16} ,15->{27},16->{28},17->{2},18->{3,4,5},19->{30,31},20->{32,33,34,35},21->{36},22->{37},23->{30,31},24->{32 ,33,34,35},25->{36},26->{37},27->{29},28->{29},29->{38,39,40},30->{2},31->{3,4,5},32->{30,31},33->{32,33,34 ,35},34->{36},35->{37},36->{41},37->{41},38->{17,18},39->{19,20,21,22},40->{23,24,25,26},41->{42,43,44,45} ,42->{30,31},43->{32,33,34,35},44->{36},45->{37}] + 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] | `- p:[3,18,6,12,5,31,19,7,39,29,27,11,4,9,13,10,14,15,28,16,23,8,40,32,20,24,33,43,41,36,21,25,34,44,37,22,26,35,45,42,38] c: [3,4,5,6,7,8,9,10,11,12,13,14,15,16,18,19,20,21,22,23,24,25,26,27,28,29,31,32,38,39,40,42] | `- p:[33,43,41,36,34,44,37,35,45] c: [33,34,35,36,37,41,43,44,45] * Step 6: AbstractSize MAYBE + Considered Problem: (Rules: start.0(A,B,C,D,E,F,G,H) -> f0.1(A,B,C,D,E,F,G,H) True start.0(A,B,C,D,E,F,G,H) -> f0.2(A,B,C,D,E,F,G,H) True f0.1(A,B,C,D,E,F,G,H) -> f58.19(A,B,C,D,E,F,G,H) [B >= A] f0.2(A,B,C,D,E,F,G,H) -> f12.3(A,B,0,B,E,F,G,H) [A >= 1 + B] f0.2(A,B,C,D,E,F,G,H) -> f12.4(A,B,0,B,E,F,G,H) [A >= 1 + B] f0.2(A,B,C,D,E,F,G,H) -> f12.5(A,B,0,B,E,F,G,H) [A >= 1 + B] f12.3(A,B,C,D,E,F,G,H) -> f35.6(A,B,C,B,E,F,G,H) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f12.3(A,B,C,D,E,F,G,H) -> f35.7(A,B,C,B,E,F,G,H) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f12.3(A,B,C,D,E,F,G,H) -> f35.8(A,B,C,B,E,F,G,H) [-1 + A + -1*B >= 0 && E >= 1 + A && B = D] f12.4(A,B,C,D,E,F,G,H) -> f12.4(A,B,J,E,1 + E,I,K,H) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f12.4(A,B,C,D,E,F,G,H) -> f12.5(A,B,J,E,1 + E,I,K,H) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f12.4(A,B,C,D,E,F,G,H) -> f12.9(A,B,J,E,1 + E,I,K,H) [-1 + A + -1*B >= 0 && A >= E && I >= 1 + K] f12.5(A,B,C,D,E,F,G,H) -> f12.3(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f12.5(A,B,C,D,E,F,G,H) -> f12.4(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f12.5(A,B,C,D,E,F,G,H) -> f12.5(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f12.5(A,B,C,D,E,F,G,H) -> f12.9(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f12.5(A,B,C,D,E,F,G,H) -> f12.10(A,B,C,D,1 + E,J,I,H) [-1 + A + -1*B >= 0 && A >= E && I >= J] f35.6(A,B,C,D,E,F,G,H) -> f0.1(A,1 + B,0,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] f35.6(A,B,C,D,E,F,G,H) -> f0.2(A,1 + B,0,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C = 0] f35.7(A,B,C,D,E,F,G,H) -> f37.12(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f35.7(A,B,C,D,E,F,G,H) -> f37.13(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f35.7(A,B,C,D,E,F,G,H) -> f37.14(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f35.7(A,B,C,D,E,F,G,H) -> f37.15(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && C >= 1] f35.8(A,B,C,D,E,F,G,H) -> f37.12(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f35.8(A,B,C,D,E,F,G,H) -> f37.13(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f35.8(A,B,C,D,E,F,G,H) -> f37.14(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f35.8(A,B,C,D,E,F,G,H) -> f37.15(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + C] f12.9(A,B,C,D,E,F,G,H) -> f22.11(A,B,C,D,E,F,G,H) [-1 + A + -1*B >= 0 && D >= 1 + B && E >= 1 + A] f12.10(A,B,C,D,E,F,G,H) -> f22.11(A,B,C,D,E,F,G,H) [-1 + A + -1*B >= 0 && B >= 1 + D && E >= 1 + A] f22.11(A,B,C,D,E,F,G,H) -> f29.16(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f37.12(A,B,C,D,E,F,G,H) -> f0.1(A,1 + B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] f37.12(A,B,C,D,E,F,G,H) -> f0.2(A,1 + B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && D >= 1 + A] f37.13(A,B,C,D,E,F,G,H) -> f37.12(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f37.13(A,B,C,D,E,F,G,H) -> f37.13(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f37.13(A,B,C,D,E,F,G,H) -> f37.14(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f37.13(A,B,C,D,E,F,G,H) -> f37.15(A,B,C,1 + D,E,F,G,0) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D] f37.14(A,B,C,D,E,F,G,H) -> f43.17(A,B,C,D,E,F,G,J) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D && I >= 1] f37.15(A,B,C,D,E,F,G,H) -> f43.17(A,B,C,D,E,F,G,J) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && A >= D && 0 >= 1 + I] f29.16(A,B,C,D,E,F,G,H) -> f35.6(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f29.16(A,B,C,D,E,F,G,H) -> f35.7(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f29.16(A,B,C,D,E,F,G,H) -> f35.8(A,B,C,D,E,F,G,H) [-2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f43.17(A,B,C,D,E,F,G,H) -> f48.18(A,B,C,D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f48.18(A,B,C,D,E,F,G,H) -> f37.12(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f48.18(A,B,C,D,E,F,G,H) -> f37.13(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f48.18(A,B,C,D,E,F,G,H) -> f37.14(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f48.18(A,B,C,D,E,F,G,H) -> f37.15(A,B,C,1 + D,E,F,G,H) [-1 + -1*D + E >= 0 && -2 + -1*B + E >= 0 && -1 + -1*A + E >= 0 && A + -1*D >= 0 && -1 + A + -1*B >= 0 && E >= 1 + A] f58.19(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f58.19(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f58.19(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True Signature: {(exitus616,8) ;(f0.1,8) ;(f0.2,8) ;(f12.10,8) ;(f12.3,8) ;(f12.4,8) ;(f12.5,8) ;(f12.9,8) ;(f22.11,8) ;(f29.16,8) ;(f35.6,8) ;(f35.7,8) ;(f35.8,8) ;(f37.12,8) ;(f37.13,8) ;(f37.14,8) ;(f37.15,8) ;(f43.17,8) ;(f48.18,8) ;(f58.19,8) ;(start.0,8)} Rule Graph: [0->{2},1->{3,4,5},2->{46,47,48},3->{6,7,8},4->{9,10,11},5->{12,13,14,15,16},6->{17,18},7->{19,20,21,22} ,8->{23,24,25,26},9->{9,10,11},10->{12,13,14,15,16},11->{27},12->{6,7,8},13->{9,10,11},14->{12,13,14,15,16} ,15->{27},16->{28},17->{2},18->{3,4,5},19->{30,31},20->{32,33,34,35},21->{36},22->{37},23->{30,31},24->{32 ,33,34,35},25->{36},26->{37},27->{29},28->{29},29->{38,39,40},30->{2},31->{3,4,5},32->{30,31},33->{32,33,34 ,35},34->{36},35->{37},36->{41},37->{41},38->{17,18},39->{19,20,21,22},40->{23,24,25,26},41->{42,43,44,45} ,42->{30,31},43->{32,33,34,35},44->{36},45->{37}] ,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] | `- p:[3,18,6,12,5,31,19,7,39,29,27,11,4,9,13,10,14,15,28,16,23,8,40,32,20,24,33,43,41,36,21,25,34,44,37,22,26,35,45,42,38] c: [3,4,5,6,7,8,9,10,11,12,13,14,15,16,18,19,20,21,22,23,24,25,26,27,28,29,31,32,38,39,40,42] | `- p:[33,43,41,36,34,44,37,35,45] c: [33,34,35,36,37,41,43,44,45]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,0.0,0.0.0] start.0 ~> f0.1 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] start.0 ~> f0.2 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f0.1 ~> f58.19 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f0.2 ~> f12.3 [A <= A, B <= B, C <= 0*K, D <= B, E <= E, F <= F, G <= G, H <= H] f0.2 ~> f12.4 [A <= A, B <= B, C <= 0*K, D <= B, E <= E, F <= F, G <= G, H <= H] f0.2 ~> f12.5 [A <= A, B <= B, C <= 0*K, D <= B, E <= E, F <= F, G <= G, H <= H] f12.3 ~> f35.6 [A <= A, B <= B, C <= C, D <= B, E <= E, F <= F, G <= G, H <= H] f12.3 ~> f35.7 [A <= A, B <= B, C <= C, D <= B, E <= E, F <= F, G <= G, H <= H] f12.3 ~> f35.8 [A <= A, B <= B, C <= C, D <= B, E <= E, F <= F, G <= G, H <= H] f12.4 ~> f12.4 [A <= A, B <= B, C <= unknown, D <= E, E <= K + E, F <= unknown, G <= unknown, H <= H] f12.4 ~> f12.5 [A <= A, B <= B, C <= unknown, D <= E, E <= K + E, F <= unknown, G <= unknown, H <= H] f12.4 ~> f12.9 [A <= A, B <= B, C <= unknown, D <= E, E <= K + E, F <= unknown, G <= unknown, H <= H] f12.5 ~> f12.3 [A <= A, B <= B, C <= C, D <= D, E <= K + E, F <= unknown, G <= unknown, H <= H] f12.5 ~> f12.4 [A <= A, B <= B, C <= C, D <= D, E <= K + E, F <= unknown, G <= unknown, H <= H] f12.5 ~> f12.5 [A <= A, B <= B, C <= C, D <= D, E <= K + E, F <= unknown, G <= unknown, H <= H] f12.5 ~> f12.9 [A <= A, B <= B, C <= C, D <= D, E <= K + E, F <= unknown, G <= unknown, H <= H] f12.5 ~> f12.10 [A <= A, B <= B, C <= C, D <= D, E <= K + E, F <= unknown, G <= unknown, H <= H] f35.6 ~> f0.1 [A <= A, B <= B + E, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H] f35.6 ~> f0.2 [A <= A, B <= B + E, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H] f35.7 ~> f37.12 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f35.7 ~> f37.13 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f35.7 ~> f37.14 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f35.7 ~> f37.15 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f35.8 ~> f37.12 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f35.8 ~> f37.13 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f35.8 ~> f37.14 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f35.8 ~> f37.15 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f12.9 ~> f22.11 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f12.10 ~> f22.11 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f22.11 ~> f29.16 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f37.12 ~> f0.1 [A <= A, B <= A + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f37.12 ~> f0.2 [A <= A, B <= A + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f37.13 ~> f37.12 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= 0*K] f37.13 ~> f37.13 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= 0*K] f37.13 ~> f37.14 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= 0*K] f37.13 ~> f37.15 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= 0*K] f37.14 ~> f43.17 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown] f37.15 ~> f43.17 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown] f29.16 ~> f35.6 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f29.16 ~> f35.7 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f29.16 ~> f35.8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f43.17 ~> f48.18 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f48.18 ~> f37.12 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= H] f48.18 ~> f37.13 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= H] f48.18 ~> f37.14 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= H] f48.18 ~> f37.15 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= H] f58.19 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f58.19 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f58.19 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] + Loop: [0.0 <= K + A + B + E] f0.2 ~> f12.3 [A <= A, B <= B, C <= 0*K, D <= B, E <= E, F <= F, G <= G, H <= H] f35.6 ~> f0.2 [A <= A, B <= B + E, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H] f12.3 ~> f35.6 [A <= A, B <= B, C <= C, D <= B, E <= E, F <= F, G <= G, H <= H] f12.5 ~> f12.3 [A <= A, B <= B, C <= C, D <= D, E <= K + E, F <= unknown, G <= unknown, H <= H] f0.2 ~> f12.5 [A <= A, B <= B, C <= 0*K, D <= B, E <= E, F <= F, G <= G, H <= H] f37.12 ~> f0.2 [A <= A, B <= A + B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f35.7 ~> f37.12 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f12.3 ~> f35.7 [A <= A, B <= B, C <= C, D <= B, E <= E, F <= F, G <= G, H <= H] f29.16 ~> f35.7 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f22.11 ~> f29.16 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f12.9 ~> f22.11 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f12.4 ~> f12.9 [A <= A, B <= B, C <= unknown, D <= E, E <= K + E, F <= unknown, G <= unknown, H <= H] f0.2 ~> f12.4 [A <= A, B <= B, C <= 0*K, D <= B, E <= E, F <= F, G <= G, H <= H] f12.4 ~> f12.4 [A <= A, B <= B, C <= unknown, D <= E, E <= K + E, F <= unknown, G <= unknown, H <= H] f12.5 ~> f12.4 [A <= A, B <= B, C <= C, D <= D, E <= K + E, F <= unknown, G <= unknown, H <= H] f12.4 ~> f12.5 [A <= A, B <= B, C <= unknown, D <= E, E <= K + E, F <= unknown, G <= unknown, H <= H] f12.5 ~> f12.5 [A <= A, B <= B, C <= C, D <= D, E <= K + E, F <= unknown, G <= unknown, H <= H] f12.5 ~> f12.9 [A <= A, B <= B, C <= C, D <= D, E <= K + E, F <= unknown, G <= unknown, H <= H] f12.10 ~> f22.11 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f12.5 ~> f12.10 [A <= A, B <= B, C <= C, D <= D, E <= K + E, F <= unknown, G <= unknown, H <= H] f35.8 ~> f37.12 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f12.3 ~> f35.8 [A <= A, B <= B, C <= C, D <= B, E <= E, F <= F, G <= G, H <= H] f29.16 ~> f35.8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f37.13 ~> f37.12 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= 0*K] f35.7 ~> f37.13 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f35.8 ~> f37.13 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f37.13 ~> f37.13 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= 0*K] f48.18 ~> f37.13 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= H] f43.17 ~> f48.18 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f37.14 ~> f43.17 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown] f35.7 ~> f37.14 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f35.8 ~> f37.14 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f37.13 ~> f37.14 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= 0*K] f48.18 ~> f37.14 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= H] f37.15 ~> f43.17 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown] f35.7 ~> f37.15 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f35.8 ~> f37.15 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f37.13 ~> f37.15 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= 0*K] f48.18 ~> f37.15 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= H] f48.18 ~> f37.12 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= H] f29.16 ~> f35.6 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] + Loop: [0.0.0 <= K + A + D] f37.13 ~> f37.13 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= 0*K] f48.18 ~> f37.13 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= H] f43.17 ~> f48.18 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] f37.14 ~> f43.17 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown] f37.13 ~> f37.14 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= 0*K] f48.18 ~> f37.14 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= H] f37.15 ~> f43.17 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown] f37.13 ~> f37.15 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= 0*K] f48.18 ~> f37.15 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G, H <= H] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,0.0,0.0.0] start.0 ~> f0.1 [] start.0 ~> f0.2 [] f0.1 ~> f58.19 [] f0.2 ~> f12.3 [B ~=> D,K ~=> C] f0.2 ~> f12.4 [B ~=> D,K ~=> C] f0.2 ~> f12.5 [B ~=> D,K ~=> C] f12.3 ~> f35.6 [B ~=> D] f12.3 ~> f35.7 [B ~=> D] f12.3 ~> f35.8 [B ~=> D] f12.4 ~> f12.4 [E ~=> D,huge ~=> C,huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f12.4 ~> f12.5 [E ~=> D,huge ~=> C,huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f12.4 ~> f12.9 [E ~=> D,huge ~=> C,huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f12.5 ~> f12.3 [huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f12.5 ~> f12.4 [huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f12.5 ~> f12.5 [huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f12.5 ~> f12.9 [huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f12.5 ~> f12.10 [huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f35.6 ~> f0.1 [K ~=> C,B ~+> B,E ~+> B] f35.6 ~> f0.2 [K ~=> C,B ~+> B,E ~+> B] f35.7 ~> f37.12 [] f35.7 ~> f37.13 [] f35.7 ~> f37.14 [] f35.7 ~> f37.15 [] f35.8 ~> f37.12 [] f35.8 ~> f37.13 [] f35.8 ~> f37.14 [] f35.8 ~> f37.15 [] f12.9 ~> f22.11 [] f12.10 ~> f22.11 [] f22.11 ~> f29.16 [] f37.12 ~> f0.1 [A ~+> B,B ~+> B] f37.12 ~> f0.2 [A ~+> B,B ~+> B] f37.13 ~> f37.12 [K ~=> H,D ~+> D,E ~+> D] f37.13 ~> f37.13 [K ~=> H,D ~+> D,E ~+> D] f37.13 ~> f37.14 [K ~=> H,D ~+> D,E ~+> D] f37.13 ~> f37.15 [K ~=> H,D ~+> D,E ~+> D] f37.14 ~> f43.17 [huge ~=> H] f37.15 ~> f43.17 [huge ~=> H] f29.16 ~> f35.6 [] f29.16 ~> f35.7 [] f29.16 ~> f35.8 [] f43.17 ~> f48.18 [] f48.18 ~> f37.12 [D ~+> D,E ~+> D] f48.18 ~> f37.13 [D ~+> D,E ~+> D] f48.18 ~> f37.14 [D ~+> D,E ~+> D] f48.18 ~> f37.15 [D ~+> D,E ~+> D] f58.19 ~> exitus616 [] f58.19 ~> exitus616 [] f58.19 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,E ~+> 0.0,K ~+> 0.0] f0.2 ~> f12.3 [B ~=> D,K ~=> C] f35.6 ~> f0.2 [K ~=> C,B ~+> B,E ~+> B] f12.3 ~> f35.6 [B ~=> D] f12.5 ~> f12.3 [huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f0.2 ~> f12.5 [B ~=> D,K ~=> C] f37.12 ~> f0.2 [A ~+> B,B ~+> B] f35.7 ~> f37.12 [] f12.3 ~> f35.7 [B ~=> D] f29.16 ~> f35.7 [] f22.11 ~> f29.16 [] f12.9 ~> f22.11 [] f12.4 ~> f12.9 [E ~=> D,huge ~=> C,huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f0.2 ~> f12.4 [B ~=> D,K ~=> C] f12.4 ~> f12.4 [E ~=> D,huge ~=> C,huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f12.5 ~> f12.4 [huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f12.4 ~> f12.5 [E ~=> D,huge ~=> C,huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f12.5 ~> f12.5 [huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f12.5 ~> f12.9 [huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f12.10 ~> f22.11 [] f12.5 ~> f12.10 [huge ~=> F,huge ~=> G,E ~+> E,K ~+> E] f35.8 ~> f37.12 [] f12.3 ~> f35.8 [B ~=> D] f29.16 ~> f35.8 [] f37.13 ~> f37.12 [K ~=> H,D ~+> D,E ~+> D] f35.7 ~> f37.13 [] f35.8 ~> f37.13 [] f37.13 ~> f37.13 [K ~=> H,D ~+> D,E ~+> D] f48.18 ~> f37.13 [D ~+> D,E ~+> D] f43.17 ~> f48.18 [] f37.14 ~> f43.17 [huge ~=> H] f35.7 ~> f37.14 [] f35.8 ~> f37.14 [] f37.13 ~> f37.14 [K ~=> H,D ~+> D,E ~+> D] f48.18 ~> f37.14 [D ~+> D,E ~+> D] f37.15 ~> f43.17 [huge ~=> H] f35.7 ~> f37.15 [] f35.8 ~> f37.15 [] f37.13 ~> f37.15 [K ~=> H,D ~+> D,E ~+> D] f48.18 ~> f37.15 [D ~+> D,E ~+> D] f48.18 ~> f37.12 [D ~+> D,E ~+> D] f29.16 ~> f35.6 [] + Loop: [A ~+> 0.0.0,D ~+> 0.0.0,K ~+> 0.0.0] f37.13 ~> f37.13 [K ~=> H,D ~+> D,E ~+> D] f48.18 ~> f37.13 [D ~+> D,E ~+> D] f43.17 ~> f48.18 [] f37.14 ~> f43.17 [huge ~=> H] f37.13 ~> f37.14 [K ~=> H,D ~+> D,E ~+> D] f48.18 ~> f37.14 [D ~+> D,E ~+> D] f37.15 ~> f43.17 [huge ~=> H] f37.13 ~> f37.15 [K ~=> H,D ~+> D,E ~+> D] f48.18 ~> f37.15 [D ~+> D,E ~+> D] + Applied Processor: Lare + Details: start.0 ~> exitus616 [B ~=> D ,E ~=> D ,K ~=> C ,K ~=> H ,huge ~=> C ,huge ~=> F ,huge ~=> G ,huge ~=> H ,A ~+> B ,A ~+> D ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> B ,E ~+> D ,E ~+> E ,E ~+> 0.0 ,E ~+> 0.0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> E ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> E ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,E ~*> B ,E ~*> D ,E ~*> E ,E ~*> 0.0.0 ,E ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> D ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick ,E ~^> D ,E ~^> 0.0.0 ,E ~^> tick ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] + f35.6> [B ~=> D ,E ~=> D ,K ~=> C ,K ~=> H ,huge ~=> C ,huge ~=> F ,huge ~=> G ,huge ~=> H ,A ~+> B ,A ~+> D ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> B ,E ~+> D ,E ~+> E ,E ~+> 0.0 ,E ~+> 0.0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> E ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> E ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,E ~*> B ,E ~*> D ,E ~*> E ,E ~*> 0.0.0 ,E ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> D ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick ,E ~^> D ,E ~^> 0.0.0 ,E ~^> tick ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] f37.12> [B ~=> D ,E ~=> D ,K ~=> C ,K ~=> H ,huge ~=> C ,huge ~=> F ,huge ~=> G ,huge ~=> H ,A ~+> B ,A ~+> D ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> B ,E ~+> D ,E ~+> E ,E ~+> 0.0 ,E ~+> 0.0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> E ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,A ~*> E ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> E ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,E ~*> B ,E ~*> D ,E ~*> E ,E ~*> 0.0.0 ,E ~*> tick ,K ~*> B ,K ~*> D ,K ~*> E ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> D ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick ,E ~^> D ,E ~^> 0.0.0 ,E ~^> tick ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] + f37.13> [K ~=> H ,huge ~=> H ,A ~+> 0.0.0 ,A ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> D ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> D ,D ~*> D ,E ~*> D ,K ~*> D] f48.18> [K ~=> H ,huge ~=> H ,A ~+> 0.0.0 ,A ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> D ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> D ,D ~*> D ,E ~*> D ,K ~*> D] f37.13> [K ~=> H ,huge ~=> H ,A ~+> 0.0.0 ,A ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> D ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> D ,D ~*> D ,E ~*> D ,K ~*> D] f48.18> [K ~=> H ,huge ~=> H ,A ~+> 0.0.0 ,A ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> D ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> D ,D ~*> D ,E ~*> D ,K ~*> D] f37.13> [K ~=> H ,huge ~=> H ,A ~+> 0.0.0 ,A ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> D ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> D ,D ~*> D ,E ~*> D ,K ~*> D] f48.18> [K ~=> H ,huge ~=> H ,A ~+> 0.0.0 ,A ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> D ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> D ,D ~*> D ,E ~*> D ,K ~*> D] YES(?,PRIMREC)