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