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