MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= A] 1. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A >= 2] 2. f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] 3. f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [-1 + D + -1*F >= 0 (?,1) && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 255 >= C] 4. f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [-1 + -1*D + F >= 0 (?,1) && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 0] 5. f0(A,B,C,D,E,F) -> f5(4,0,C,G,0,F) True (1,1) 6. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] 7. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= E && D >= 1 + F] 8. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 2 && D >= 1 + F] 9. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && D >= 1 + F && E = 1] 10. f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D >= 1 + F && B = 0 && E = 1] 11. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 1 >= E && F >= 1 + D] 12. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 3 && F >= 1 + D] 13. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && F >= 1 + D && E = 2] 14. f9(A,B,C,D,E,F) -> f25(-1 + A,1,1 + -1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && F >= 1 + D && B = 0 && E = 2] 15. f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A = 1] 16. f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [-1 + D + -1*F >= 0 (?,1) && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 256] 17. f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [-1 + -1*D + F >= 0 (?,1) && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= 1 + C] 18. f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D = F] Signature: {(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Flow Graph: [0->{2,6},1->{2,6},2->{7,8,9,10,11,12,13,14,18},3->{0,1,15},4->{0,1,15},5->{0,1,15},6->{7,8,9,10,11,12,13 ,14,18},7->{3,16},8->{3,16},9->{3,16},10->{3,16},11->{4,17},12->{4,17},13->{4,17},14->{4,17},15->{},16->{} ,17->{},18->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,9),(2,13),(5,0),(5,15),(6,10),(6,14)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= A] 1. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A >= 2] 2. f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] 3. f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [-1 + D + -1*F >= 0 (?,1) && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 255 >= C] 4. f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [-1 + -1*D + F >= 0 (?,1) && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 0] 5. f0(A,B,C,D,E,F) -> f5(4,0,C,G,0,F) True (1,1) 6. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] 7. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= E && D >= 1 + F] 8. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 2 && D >= 1 + F] 9. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && D >= 1 + F && E = 1] 10. f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D >= 1 + F && B = 0 && E = 1] 11. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 1 >= E && F >= 1 + D] 12. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 3 && F >= 1 + D] 13. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && F >= 1 + D && E = 2] 14. f9(A,B,C,D,E,F) -> f25(-1 + A,1,1 + -1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && F >= 1 + D && B = 0 && E = 2] 15. f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A = 1] 16. f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [-1 + D + -1*F >= 0 (?,1) && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 256] 17. f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [-1 + -1*D + F >= 0 (?,1) && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= 1 + C] 18. f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D = F] Signature: {(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Flow Graph: [0->{2,6},1->{2,6},2->{7,8,10,11,12,14,18},3->{0,1,15},4->{0,1,15},5->{1},6->{7,8,9,11,12,13,18},7->{3,16} ,8->{3,16},9->{3,16},10->{3,16},11->{4,17},12->{4,17},13->{4,17},14->{4,17},15->{},16->{},17->{},18->{}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= A] f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A >= 2] f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [-1 + D + -1*F >= 0 && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 255 >= C] f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [-1 + -1*D + F >= 0 && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 0] f0(A,B,C,D,E,F) -> f5(4,0,C,G,0,F) True f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= E && D >= 1 + F] f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 2 && D >= 1 + F] f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && D >= 1 + F && E = 1] f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D >= 1 + F && B = 0 && E = 1] f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 1 >= E && F >= 1 + D] f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 3 && F >= 1 + D] f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && F >= 1 + D && E = 2] f9(A,B,C,D,E,F) -> f25(-1 + A,1,1 + -1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && F >= 1 + D && B = 0 && E = 2] f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A = 1] f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [-1 + D + -1*F >= 0 && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 256] f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [-1 + -1*D + F >= 0 && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= 1 + C] f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D = F] Signature: {(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Rule Graph: [0->{2,6},1->{2,6},2->{7,8,10,11,12,14,18},3->{0,1,15},4->{0,1,15},5->{1},6->{7,8,9,11,12,13,18},7->{3,16} ,8->{3,16},9->{3,16},10->{3,16},11->{4,17},12->{4,17},13->{4,17},14->{4,17},15->{},16->{},17->{},18->{}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: f5.0(A,B,C,D,E,F) -> f7.2(A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= A] f5.0(A,B,C,D,E,F) -> f7.6(A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= A] f5.1(A,B,C,D,E,F) -> f7.2(A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A >= 2] f5.1(A,B,C,D,E,F) -> f7.6(A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A >= 2] f7.2(A,B,C,D,E,F) -> f9.7(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f7.2(A,B,C,D,E,F) -> f9.8(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f7.2(A,B,C,D,E,F) -> f9.10(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f7.2(A,B,C,D,E,F) -> f9.11(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f7.2(A,B,C,D,E,F) -> f9.12(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f7.2(A,B,C,D,E,F) -> f9.14(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f7.2(A,B,C,D,E,F) -> f9.18(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f16.3(A,B,C,D,E,F) -> f5.0(A,B,C,G,E,F) [-1 + D + -1*F >= 0 && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 255 >= C] f16.3(A,B,C,D,E,F) -> f5.1(A,B,C,G,E,F) [-1 + D + -1*F >= 0 && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 255 >= C] f16.3(A,B,C,D,E,F) -> f5.15(A,B,C,G,E,F) [-1 + D + -1*F >= 0 && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 255 >= C] f25.4(A,B,C,D,E,F) -> f5.0(A,B,C,G,E,F) [-1 + -1*D + F >= 0 && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 0] f25.4(A,B,C,D,E,F) -> f5.1(A,B,C,G,E,F) [-1 + -1*D + F >= 0 && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 0] f25.4(A,B,C,D,E,F) -> f5.15(A,B,C,G,E,F) [-1 + -1*D + F >= 0 && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 0] f0.5(A,B,C,D,E,F) -> f5.1(4,0,C,G,0,F) True f7.6(A,B,C,D,E,F) -> f9.7(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f7.6(A,B,C,D,E,F) -> f9.8(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f7.6(A,B,C,D,E,F) -> f9.9(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f7.6(A,B,C,D,E,F) -> f9.11(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f7.6(A,B,C,D,E,F) -> f9.12(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f7.6(A,B,C,D,E,F) -> f9.13(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f7.6(A,B,C,D,E,F) -> f9.18(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f9.7(A,B,C,D,E,F) -> f16.3(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= E && D >= 1 + F] f9.7(A,B,C,D,E,F) -> f16.16(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= E && D >= 1 + F] f9.8(A,B,C,D,E,F) -> f16.3(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 2 && D >= 1 + F] f9.8(A,B,C,D,E,F) -> f16.16(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 2 && D >= 1 + F] f9.9(A,B,C,D,E,F) -> f16.3(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && D >= 1 + F && E = 1] f9.9(A,B,C,D,E,F) -> f16.16(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && D >= 1 + F && E = 1] f9.10(A,B,C,D,E,F) -> f16.3(-1 + A,1,-1 + A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D >= 1 + F && B = 0 && E = 1] f9.10(A,B,C,D,E,F) -> f16.16(-1 + A,1,-1 + A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D >= 1 + F && B = 0 && E = 1] f9.11(A,B,C,D,E,F) -> f25.4(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 1 >= E && F >= 1 + D] f9.11(A,B,C,D,E,F) -> f25.17(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 1 >= E && F >= 1 + D] f9.12(A,B,C,D,E,F) -> f25.4(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 3 && F >= 1 + D] f9.12(A,B,C,D,E,F) -> f25.17(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 3 && F >= 1 + D] f9.13(A,B,C,D,E,F) -> f25.4(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && F >= 1 + D && E = 2] f9.13(A,B,C,D,E,F) -> f25.17(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && F >= 1 + D && E = 2] f9.14(A,B,C,D,E,F) -> f25.4(-1 + A,1,1 + -1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && F >= 1 + D && B = 0 && E = 2] f9.14(A,B,C,D,E,F) -> f25.17(-1 + A,1,1 + -1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && F >= 1 + D && B = 0 && E = 2] f5.15(A,B,C,D,E,F) -> f30.19(1,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A = 1] f16.16(A,B,C,D,E,F) -> f30.19(A,B,C,D,E,F) [-1 + D + -1*F >= 0 && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 256] f25.17(A,B,C,D,E,F) -> f30.19(A,B,C,D,E,F) [-1 + -1*D + F >= 0 && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= 1 + C] f9.18(A,B,C,D,E,F) -> f30.19(A,B,C,D,E,D) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D = F] Signature: {(f0.5,6) ;(f16.16,6) ;(f16.3,6) ;(f25.17,6) ;(f25.4,6) ;(f30.19,6) ;(f5.0,6) ;(f5.1,6) ;(f5.15,6) ;(f7.2,6) ;(f7.6,6) ;(f9.10,6) ;(f9.11,6) ;(f9.12,6) ;(f9.13,6) ;(f9.14,6) ;(f9.18,6) ;(f9.7,6) ;(f9.8,6) ;(f9.9,6)} Rule Graph: [0->{4,5,6,7,8,9,10},1->{18,19,20,21,22,23,24},2->{4,5,6,7,8,9,10},3->{18,19,20,21,22,23,24},4->{25,26} ,5->{27,28},6->{31,32},7->{33,34},8->{35,36},9->{39,40},10->{44},11->{0,1},12->{2,3},13->{41},14->{0,1} ,15->{2,3},16->{41},17->{2,3},18->{25,26},19->{27,28},20->{29,30},21->{33,34},22->{35,36},23->{37,38} ,24->{44},25->{11,12,13},26->{42},27->{11,12,13},28->{42},29->{11,12,13},30->{42},31->{11,12,13},32->{42} ,33->{14,15,16},34->{43},35->{14,15,16},36->{43},37->{14,15,16},38->{43},39->{14,15,16},40->{43},41->{} ,42->{},43->{},44->{}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: f5.0(A,B,C,D,E,F) -> f7.2(A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= A] f5.0(A,B,C,D,E,F) -> f7.6(A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= A] f5.1(A,B,C,D,E,F) -> f7.2(A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A >= 2] f5.1(A,B,C,D,E,F) -> f7.6(A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A >= 2] f7.2(A,B,C,D,E,F) -> f9.7(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f7.2(A,B,C,D,E,F) -> f9.8(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f7.2(A,B,C,D,E,F) -> f9.10(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f7.2(A,B,C,D,E,F) -> f9.11(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f7.2(A,B,C,D,E,F) -> f9.12(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f7.2(A,B,C,D,E,F) -> f9.14(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f7.2(A,B,C,D,E,F) -> f9.18(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f16.3(A,B,C,D,E,F) -> f5.0(A,B,C,G,E,F) [-1 + D + -1*F >= 0 && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 255 >= C] f16.3(A,B,C,D,E,F) -> f5.1(A,B,C,G,E,F) [-1 + D + -1*F >= 0 && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 255 >= C] f16.3(A,B,C,D,E,F) -> f5.15(A,B,C,G,E,F) [-1 + D + -1*F >= 0 && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 255 >= C] f25.4(A,B,C,D,E,F) -> f5.0(A,B,C,G,E,F) [-1 + -1*D + F >= 0 && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 0] f25.4(A,B,C,D,E,F) -> f5.1(A,B,C,G,E,F) [-1 + -1*D + F >= 0 && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 0] f25.4(A,B,C,D,E,F) -> f5.15(A,B,C,G,E,F) [-1 + -1*D + F >= 0 && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 0] f0.5(A,B,C,D,E,F) -> f5.1(4,0,C,G,0,F) True f7.6(A,B,C,D,E,F) -> f9.7(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f7.6(A,B,C,D,E,F) -> f9.8(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f7.6(A,B,C,D,E,F) -> f9.9(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f7.6(A,B,C,D,E,F) -> f9.11(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f7.6(A,B,C,D,E,F) -> f9.12(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f7.6(A,B,C,D,E,F) -> f9.13(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f7.6(A,B,C,D,E,F) -> f9.18(-1 + A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f9.7(A,B,C,D,E,F) -> f16.3(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= E && D >= 1 + F] f9.7(A,B,C,D,E,F) -> f16.16(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= E && D >= 1 + F] f9.8(A,B,C,D,E,F) -> f16.3(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 2 && D >= 1 + F] f9.8(A,B,C,D,E,F) -> f16.16(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 2 && D >= 1 + F] f9.9(A,B,C,D,E,F) -> f16.3(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && D >= 1 + F && E = 1] f9.9(A,B,C,D,E,F) -> f16.16(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && D >= 1 + F && E = 1] f9.10(A,B,C,D,E,F) -> f16.3(-1 + A,1,-1 + A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D >= 1 + F && B = 0 && E = 1] f9.10(A,B,C,D,E,F) -> f16.16(-1 + A,1,-1 + A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D >= 1 + F && B = 0 && E = 1] f9.11(A,B,C,D,E,F) -> f25.4(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 1 >= E && F >= 1 + D] f9.11(A,B,C,D,E,F) -> f25.17(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 1 >= E && F >= 1 + D] f9.12(A,B,C,D,E,F) -> f25.4(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 3 && F >= 1 + D] f9.12(A,B,C,D,E,F) -> f25.17(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 3 && F >= 1 + D] f9.13(A,B,C,D,E,F) -> f25.4(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && F >= 1 + D && E = 2] f9.13(A,B,C,D,E,F) -> f25.17(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && F >= 1 + D && E = 2] f9.14(A,B,C,D,E,F) -> f25.4(-1 + A,1,1 + -1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && F >= 1 + D && B = 0 && E = 2] f9.14(A,B,C,D,E,F) -> f25.17(-1 + A,1,1 + -1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && F >= 1 + D && B = 0 && E = 2] f5.15(A,B,C,D,E,F) -> f30.19(1,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A = 1] f16.16(A,B,C,D,E,F) -> f30.19(A,B,C,D,E,F) [-1 + D + -1*F >= 0 && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 256] f25.17(A,B,C,D,E,F) -> f30.19(A,B,C,D,E,F) [-1 + -1*D + F >= 0 && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= 1 + C] f9.18(A,B,C,D,E,F) -> f30.19(A,B,C,D,E,D) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D = F] f30.19(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.19(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.19(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.19(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.19(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.19(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.19(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.19(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.19(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.19(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.19(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.19(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True Signature: {(exitus616,6) ;(f0.5,6) ;(f16.16,6) ;(f16.3,6) ;(f25.17,6) ;(f25.4,6) ;(f30.19,6) ;(f5.0,6) ;(f5.1,6) ;(f5.15,6) ;(f7.2,6) ;(f7.6,6) ;(f9.10,6) ;(f9.11,6) ;(f9.12,6) ;(f9.13,6) ;(f9.14,6) ;(f9.18,6) ;(f9.7,6) ;(f9.8,6) ;(f9.9,6)} Rule Graph: [0->{4,5,6,7,8,9,10},1->{18,19,20,21,22,23,24},2->{4,5,6,7,8,9,10},3->{18,19,20,21,22,23,24},4->{25,26} ,5->{27,28},6->{31,32},7->{33,34},8->{35,36},9->{39,40},10->{44},11->{0,1},12->{2,3},13->{41},14->{0,1} ,15->{2,3},16->{41},17->{2,3},18->{25,26},19->{27,28},20->{29,30},21->{33,34},22->{35,36},23->{37,38} ,24->{44},25->{11,12,13},26->{42},27->{11,12,13},28->{42},29->{11,12,13},30->{42},31->{11,12,13},32->{42} ,33->{14,15,16},34->{43},35->{14,15,16},36->{43},37->{14,15,16},38->{43},39->{14,15,16},40->{43},41->{50,54} ,42->{52,53,55,56},43->{46,48,49,51},44->{45,47}] + 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] | `- p:[0,11,25,4,2,12,27,5,19,1,14,33,7,21,3,15,35,8,22,37,23,39,9,29,20,31,6,18] c: [3,6,9,31,39] | `- p:[0,11,25,4,2,12,27,5,19,1,14,33,7,21,35,8,22,37,23,29,20,15,18] c: [] MAYBE