YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && A >= 1 + B] 1. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && U >= 1 + T && E >= 1 && F >= 0] 2. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && T >= U && E >= 0 && F >= 0 && H = 0] 3. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && C >= 2 && B >= A && Y >= Z] 5. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R) True (1,1) Signature: {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)} Flow Graph: [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0,4}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(5,4)] * Step 2: FromIts YES + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && A >= 1 + B] 1. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && U >= 1 + T && E >= 1 && F >= 0] 2. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && T >= U && E >= 0 && F >= 0 && H = 0] 3. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R) [-1*H >= 0 (?,1) && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C) [-1 + B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && C >= 2 && B >= A && Y >= Z] 5. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R) True (1,1) Signature: {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)} Flow Graph: [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0}] + Applied Processor: FromIts + Details: () * Step 3: Decompose YES + Considered Problem: Rules: f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && A >= 1 + B] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R) [-1*H >= 0 && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && U >= 1 + T && E >= 1 && F >= 0] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R) [-1*H >= 0 && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && T >= U && E >= 0 && F >= 0 && H = 0] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R) [-1*H >= 0 && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && C >= 2 && B >= A && Y >= Z] f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R) True Signature: {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)} Rule Graph: [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5] | +- p:[0] c: [0] | `- p:[2] c: [2] * Step 4: CloseWith YES + Considered Problem: (Rules: f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && A >= 1 + B] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R) [-1*H >= 0 && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && U >= 1 + T && E >= 1 && F >= 0] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R) [-1*H >= 0 && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && T >= U && E >= 0 && F >= 0 && H = 0] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R) [-1*H >= 0 && -1 + E + -1*H >= 0 && -16 + C + -1*H >= 0 && -17 + B + -1*H >= 0 && -14 + -1*H + R >= 0 && -17 + A + -1*H >= 0 && 17 + -1*A + -1*H >= 0 && H >= 0 && -1 + E + H >= 0 && -16 + C + H >= 0 && -17 + B + H >= 0 && -14 + H + R >= 0 && -17 + A + H >= 0 && 17 + -1*A + H >= 0 && -1 + E >= 0 && -17 + C + E >= 0 && -18 + B + E >= 0 && -15 + E + R >= 0 && -18 + A + E >= 0 && 16 + -1*A + E >= 0 && -1*D + Q >= 0 && D + -1*Q >= 0 && -1 + B + -1*C >= 0 && 2 + -1*C + R >= 0 && -16 + C >= 0 && -33 + B + C >= 0 && 1 + -1*B + C >= 0 && -30 + C + R >= 0 && -2 + C + -1*R >= 0 && -33 + A + C >= 0 && 1 + -1*A + C >= 0 && 3 + -1*B + R >= 0 && -17 + B >= 0 && -31 + B + R >= 0 && -3 + B + -1*R >= 0 && -34 + A + B >= 0 && -1*A + B >= 0 && -14 + R >= 0 && -31 + A + R >= 0 && 3 + -1*A + R >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C) [-1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && 1 + -1*B + C >= 0 && -17 + A + C >= 0 && 17 + -1*A + C >= 0 && -1 + B >= 0 && -18 + A + B >= 0 && 16 + -1*A + B >= 0 && 17 + -1*A >= 0 && -17 + A >= 0 && C >= 2 && B >= A && Y >= Z] f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R) True Signature: {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)} Rule Graph: [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0}] ,We construct a looptree: P: [0,1,2,3,4,5] | +- p:[0] c: [0] | `- p:[2] c: [2]) + Applied Processor: CloseWith True + Details: () YES