YES * Step 1: FromIts YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J) -> f17(0,K,L,0,E,F,G,H,I,J) True (1,1) 1. f17(A,B,C,D,E,F,G,H,I,J) -> f17(A,B,C,1 + D,E,F,G,H,I,J) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 1 + D] (?,1) 2. f27(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,E,-1 + F,G,H,I,J) [-1 + E + -1*F >= 0 (?,1) && -1 + D + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && F >= 0] 3. f37(A,B,C,D,E,F,G,H,I,J) -> f37(A,B,C,D,E,F,1 + G,H,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && -1 + -1*A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 1 + G] 4. f45(A,B,C,D,E,F,G,H,I,J) -> f45(1 + A,B,C,D,E,F,G,H,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && E >= 1 + A] 5. f55(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,F,G,1 + H,I,J) [G + -1*H >= 0 (?,1) && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && E >= 1 + H] 6. f65(A,B,C,D,E,F,G,H,I,J) -> f65(A,B,C,D,E,F,G,H,-1 + I,J) [-1 + H + -1*I >= 0 (?,1) && -1 + G + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && I >= 0] 7. f75(A,B,C,D,E,F,G,H,I,J) -> f75(A,B,C,D,E,F,G,H,I,1 + J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && A + D >= 0 && -1*A + D >= 0 && A + -1*J >= 0 && J >= 0 && A + J >= 0 && A >= 0 && E >= 1 + J] 8. f83(A,B,C,D,E,F,G,H,I,J) -> f83(-1 + A,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && -1 + -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && A + -1*F >= 0 && D + -1*E >= 0 && -1*E + J >= 0 && -1 + -1*A + E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && -1 + -1*A + D >= 0 && J >= 0 && -1 + -1*A + J >= 0 && A >= 0] 9. f83(A,B,C,D,E,F,G,H,I,J) -> f93(A,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && -1 + -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && A + -1*F >= 0 && D + -1*E >= 0 && -1*E + J >= 0 && -1 + -1*A + E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && -1 + -1*A + D >= 0 && J >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + A] 10. f75(A,B,C,D,E,F,G,H,I,J) -> f83(-1 + E,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && A + D >= 0 && -1*A + D >= 0 && A + -1*J >= 0 && J >= 0 && A + J >= 0 && A >= 0 && J >= E] 11. f65(A,B,C,D,E,F,G,H,I,J) -> f75(A,B,C,D,E,F,G,H,I,0) [-1 + H + -1*I >= 0 (?,1) && -1 + G + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && 0 >= 1 + I] 12. f55(A,B,C,D,E,F,G,H,I,J) -> f65(A,B,C,D,E,F,G,H,-1 + E,J) [G + -1*H >= 0 (?,1) && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && H >= E] 13. f45(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,F,G,0,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && A >= E] 14. f37(A,B,C,D,E,F,G,H,I,J) -> f45(0,B,C,D,E,F,G,H,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && -1 + -1*A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && G >= E] 15. f27(A,B,C,D,E,F,G,H,I,J) -> f37(A,B,C,D,E,F,0,H,I,J) [-1 + E + -1*F >= 0 (?,1) && -1 + D + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 0 >= 1 + F] 16. f17(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,E,-1 + E,G,H,I,J) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && D >= E] (?,1) Signature: {(f0,10);(f17,10);(f27,10);(f37,10);(f45,10);(f55,10);(f65,10);(f75,10);(f83,10);(f93,10)} Flow Graph: [0->{1,16},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8,9} ,11->{7,10},12->{6,11},13->{5,12},14->{4,13},15->{3,14},16->{2,15}] + Applied Processor: FromIts + Details: () * Step 2: Decompose YES + Considered Problem: Rules: f0(A,B,C,D,E,F,G,H,I,J) -> f17(0,K,L,0,E,F,G,H,I,J) True f17(A,B,C,D,E,F,G,H,I,J) -> f17(A,B,C,1 + D,E,F,G,H,I,J) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 1 + D] f27(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,E,-1 + F,G,H,I,J) [-1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && F >= 0] f37(A,B,C,D,E,F,G,H,I,J) -> f37(A,B,C,D,E,F,1 + G,H,I,J) [D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && -1 + -1*A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 1 + G] f45(A,B,C,D,E,F,G,H,I,J) -> f45(1 + A,B,C,D,E,F,G,H,I,J) [D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && E >= 1 + A] f55(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,F,G,1 + H,I,J) [G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && E >= 1 + H] f65(A,B,C,D,E,F,G,H,I,J) -> f65(A,B,C,D,E,F,G,H,-1 + I,J) [-1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && I >= 0] f75(A,B,C,D,E,F,G,H,I,J) -> f75(A,B,C,D,E,F,G,H,I,1 + J) [-1 + -1*I >= 0 && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && A + D >= 0 && -1*A + D >= 0 && A + -1*J >= 0 && J >= 0 && A + J >= 0 && A >= 0 && E >= 1 + J] f83(A,B,C,D,E,F,G,H,I,J) -> f83(-1 + A,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && -1 + -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && A + -1*F >= 0 && D + -1*E >= 0 && -1*E + J >= 0 && -1 + -1*A + E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && -1 + -1*A + D >= 0 && J >= 0 && -1 + -1*A + J >= 0 && A >= 0] f83(A,B,C,D,E,F,G,H,I,J) -> f93(A,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && -1 + -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && A + -1*F >= 0 && D + -1*E >= 0 && -1*E + J >= 0 && -1 + -1*A + E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && -1 + -1*A + D >= 0 && J >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + A] f75(A,B,C,D,E,F,G,H,I,J) -> f83(-1 + E,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && A + D >= 0 && -1*A + D >= 0 && A + -1*J >= 0 && J >= 0 && A + J >= 0 && A >= 0 && J >= E] f65(A,B,C,D,E,F,G,H,I,J) -> f75(A,B,C,D,E,F,G,H,I,0) [-1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && 0 >= 1 + I] f55(A,B,C,D,E,F,G,H,I,J) -> f65(A,B,C,D,E,F,G,H,-1 + E,J) [G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && H >= E] f45(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,F,G,0,I,J) [D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && A >= E] f37(A,B,C,D,E,F,G,H,I,J) -> f45(0,B,C,D,E,F,G,H,I,J) [D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && -1 + -1*A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && G >= E] f27(A,B,C,D,E,F,G,H,I,J) -> f37(A,B,C,D,E,F,0,H,I,J) [-1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 0 >= 1 + F] f17(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,E,-1 + E,G,H,I,J) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && D >= E] Signature: {(f0,10);(f17,10);(f27,10);(f37,10);(f45,10);(f55,10);(f65,10);(f75,10);(f83,10);(f93,10)} Rule Graph: [0->{1,16},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8,9} ,11->{7,10},12->{6,11},13->{5,12},14->{4,13},15->{3,14},16->{2,15}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] | +- p:[1] c: [1] | +- p:[2] c: [2] | +- p:[3] c: [3] | +- p:[4] c: [4] | +- p:[5] c: [5] | +- p:[6] c: [6] | +- p:[7] c: [7] | `- p:[8] c: [8] * Step 3: CloseWith YES + Considered Problem: (Rules: f0(A,B,C,D,E,F,G,H,I,J) -> f17(0,K,L,0,E,F,G,H,I,J) True f17(A,B,C,D,E,F,G,H,I,J) -> f17(A,B,C,1 + D,E,F,G,H,I,J) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 1 + D] f27(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,E,-1 + F,G,H,I,J) [-1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && F >= 0] f37(A,B,C,D,E,F,G,H,I,J) -> f37(A,B,C,D,E,F,1 + G,H,I,J) [D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && -1 + -1*A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 1 + G] f45(A,B,C,D,E,F,G,H,I,J) -> f45(1 + A,B,C,D,E,F,G,H,I,J) [D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && E >= 1 + A] f55(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,F,G,1 + H,I,J) [G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && E >= 1 + H] f65(A,B,C,D,E,F,G,H,I,J) -> f65(A,B,C,D,E,F,G,H,-1 + I,J) [-1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && I >= 0] f75(A,B,C,D,E,F,G,H,I,J) -> f75(A,B,C,D,E,F,G,H,I,1 + J) [-1 + -1*I >= 0 && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && A + D >= 0 && -1*A + D >= 0 && A + -1*J >= 0 && J >= 0 && A + J >= 0 && A >= 0 && E >= 1 + J] f83(A,B,C,D,E,F,G,H,I,J) -> f83(-1 + A,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && -1 + -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && A + -1*F >= 0 && D + -1*E >= 0 && -1*E + J >= 0 && -1 + -1*A + E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && -1 + -1*A + D >= 0 && J >= 0 && -1 + -1*A + J >= 0 && A >= 0] f83(A,B,C,D,E,F,G,H,I,J) -> f93(A,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && -1 + -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && A + -1*F >= 0 && D + -1*E >= 0 && -1*E + J >= 0 && -1 + -1*A + E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && -1 + -1*A + D >= 0 && J >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + A] f75(A,B,C,D,E,F,G,H,I,J) -> f83(-1 + E,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && A + D >= 0 && -1*A + D >= 0 && A + -1*J >= 0 && J >= 0 && A + J >= 0 && A >= 0 && J >= E] f65(A,B,C,D,E,F,G,H,I,J) -> f75(A,B,C,D,E,F,G,H,I,0) [-1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && 0 >= 1 + I] f55(A,B,C,D,E,F,G,H,I,J) -> f65(A,B,C,D,E,F,G,H,-1 + E,J) [G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && H >= E] f45(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,F,G,0,I,J) [D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && A >= E] f37(A,B,C,D,E,F,G,H,I,J) -> f45(0,B,C,D,E,F,G,H,I,J) [D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && -1 + -1*A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && G >= E] f27(A,B,C,D,E,F,G,H,I,J) -> f37(A,B,C,D,E,F,0,H,I,J) [-1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 0 >= 1 + F] f17(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,E,-1 + E,G,H,I,J) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && D >= E] Signature: {(f0,10);(f17,10);(f27,10);(f37,10);(f45,10);(f55,10);(f65,10);(f75,10);(f83,10);(f93,10)} Rule Graph: [0->{1,16},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8,9} ,11->{7,10},12->{6,11},13->{5,12},14->{4,13},15->{3,14},16->{2,15}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] | +- p:[1] c: [1] | +- p:[2] c: [2] | +- p:[3] c: [3] | +- p:[4] c: [4] | +- p:[5] c: [5] | +- p:[6] c: [6] | +- p:[7] c: [7] | `- p:[8] c: [8]) + Applied Processor: CloseWith True + Details: () YES