MAYBE * Step 1: ArgumentFilter MAYBE + 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: ArgumentFilter [6,8,9,10,11,12,14,15] + Details: We remove following argument positions: [6,8,9,10,11,12,14,15]. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,H,N,Q,R) -> f9(A,1 + B,1 + C,S,E,F,H,N,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,H,N,Q,R) -> f0(A,B,C,D,E,F,G,N,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,H,N,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,0,V,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,H,N,Q,R) -> f12(A,B,C,D,E,F,0,0,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,H,N,Q,R) -> f5(A,B,C,D,1,-3 + C + T,0,X,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,H,N,Q,R) -> f9(17,1,0,S,E,F,H,N,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 3: FromIts MAYBE + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,H,N,Q,R) -> f9(A,1 + B,1 + C,S,E,F,H,N,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,H,N,Q,R) -> f0(A,B,C,D,E,F,G,N,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,H,N,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,0,V,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,H,N,Q,R) -> f12(A,B,C,D,E,F,0,0,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,H,N,Q,R) -> f5(A,B,C,D,1,-3 + C + T,0,X,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,H,N,Q,R) -> f9(17,1,0,S,E,F,H,N,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 4: Unfold MAYBE + Considered Problem: Rules: f9(A,B,C,D,E,F,H,N,Q,R) -> f9(A,1 + B,1 + C,S,E,F,H,N,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,H,N,Q,R) -> f0(A,B,C,D,E,F,G,N,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,H,N,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,0,V,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,H,N,Q,R) -> f12(A,B,C,D,E,F,0,0,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,H,N,Q,R) -> f5(A,B,C,D,1,-3 + C + T,0,X,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,H,N,Q,R) -> f9(17,1,0,S,E,F,H,N,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: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: f9.0(A,B,C,D,E,F,H,N,Q,R) -> f9.0(A,1 + B,1 + C,S,E,F,H,N,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] f9.0(A,B,C,D,E,F,H,N,Q,R) -> f9.4(A,1 + B,1 + C,S,E,F,H,N,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.1(A,B,C,D,E,F,H,N,Q,R) -> f0.6(A,B,C,D,E,F,G,N,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.2(A,B,C,D,E,F,H,N,Q,R) -> f5.1(A,B,C,D,1 + E,-1 + F,0,V,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.2(A,B,C,D,E,F,H,N,Q,R) -> f5.2(A,B,C,D,1 + E,-1 + F,0,V,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.2(A,B,C,D,E,F,H,N,Q,R) -> f5.3(A,B,C,D,1 + E,-1 + F,0,V,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.3(A,B,C,D,E,F,H,N,Q,R) -> f12.6(A,B,C,D,E,F,0,0,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.4(A,B,C,D,E,F,H,N,Q,R) -> f5.1(A,B,C,D,1,-3 + C + T,0,X,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] f9.4(A,B,C,D,E,F,H,N,Q,R) -> f5.2(A,B,C,D,1,-3 + C + T,0,X,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] f9.4(A,B,C,D,E,F,H,N,Q,R) -> f5.3(A,B,C,D,1,-3 + C + T,0,X,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.5(A,B,C,D,E,F,H,N,Q,R) -> f9.0(17,1,0,S,E,F,H,N,Q,R) True Signature: {(f0.6,10);(f12.6,10);(f5.1,10);(f5.2,10);(f5.3,10);(f6.5,10);(f9.0,10);(f9.4,10)} Rule Graph: [0->{0,1},1->{7,8,9},2->{},3->{2},4->{3,4,5},5->{6},6->{},7->{2},8->{3,4,5},9->{6},10->{0,1}] + Applied Processor: AddSinks + Details: () * Step 6: Decompose MAYBE + Considered Problem: Rules: f9.0(A,B,C,D,E,F,H,N,Q,R) -> f9.0(A,1 + B,1 + C,S,E,F,H,N,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] f9.0(A,B,C,D,E,F,H,N,Q,R) -> f9.4(A,1 + B,1 + C,S,E,F,H,N,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.1(A,B,C,D,E,F,H,N,Q,R) -> f0.6(A,B,C,D,E,F,G,N,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.2(A,B,C,D,E,F,H,N,Q,R) -> f5.1(A,B,C,D,1 + E,-1 + F,0,V,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.2(A,B,C,D,E,F,H,N,Q,R) -> f5.2(A,B,C,D,1 + E,-1 + F,0,V,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.2(A,B,C,D,E,F,H,N,Q,R) -> f5.3(A,B,C,D,1 + E,-1 + F,0,V,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.3(A,B,C,D,E,F,H,N,Q,R) -> f12.6(A,B,C,D,E,F,0,0,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.4(A,B,C,D,E,F,H,N,Q,R) -> f5.1(A,B,C,D,1,-3 + C + T,0,X,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] f9.4(A,B,C,D,E,F,H,N,Q,R) -> f5.2(A,B,C,D,1,-3 + C + T,0,X,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] f9.4(A,B,C,D,E,F,H,N,Q,R) -> f5.3(A,B,C,D,1,-3 + C + T,0,X,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.5(A,B,C,D,E,F,H,N,Q,R) -> f9.0(17,1,0,S,E,F,H,N,Q,R) True f12.6(A,B,C,D,E,F,H,N,Q,R) -> exitus616(A,B,C,D,E,F,H,N,Q,R) True f12.6(A,B,C,D,E,F,H,N,Q,R) -> exitus616(A,B,C,D,E,F,H,N,Q,R) True f0.6(A,B,C,D,E,F,H,N,Q,R) -> exitus616(A,B,C,D,E,F,H,N,Q,R) True f0.6(A,B,C,D,E,F,H,N,Q,R) -> exitus616(A,B,C,D,E,F,H,N,Q,R) True Signature: {(exitus616,10);(f0.6,10);(f12.6,10);(f5.1,10);(f5.2,10);(f5.3,10);(f6.5,10);(f9.0,10);(f9.4,10)} Rule Graph: [0->{0,1},1->{7,8,9},2->{13,14},3->{2},4->{3,4,5},5->{6},6->{11,12},7->{2},8->{3,4,5},9->{6},10->{0,1}] + 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] | +- p:[0] c: [0] | `- p:[4] c: [4] * Step 7: AbstractSize MAYBE + Considered Problem: (Rules: f9.0(A,B,C,D,E,F,H,N,Q,R) -> f9.0(A,1 + B,1 + C,S,E,F,H,N,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] f9.0(A,B,C,D,E,F,H,N,Q,R) -> f9.4(A,1 + B,1 + C,S,E,F,H,N,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.1(A,B,C,D,E,F,H,N,Q,R) -> f0.6(A,B,C,D,E,F,G,N,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.2(A,B,C,D,E,F,H,N,Q,R) -> f5.1(A,B,C,D,1 + E,-1 + F,0,V,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.2(A,B,C,D,E,F,H,N,Q,R) -> f5.2(A,B,C,D,1 + E,-1 + F,0,V,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.2(A,B,C,D,E,F,H,N,Q,R) -> f5.3(A,B,C,D,1 + E,-1 + F,0,V,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.3(A,B,C,D,E,F,H,N,Q,R) -> f12.6(A,B,C,D,E,F,0,0,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.4(A,B,C,D,E,F,H,N,Q,R) -> f5.1(A,B,C,D,1,-3 + C + T,0,X,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] f9.4(A,B,C,D,E,F,H,N,Q,R) -> f5.2(A,B,C,D,1,-3 + C + T,0,X,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] f9.4(A,B,C,D,E,F,H,N,Q,R) -> f5.3(A,B,C,D,1,-3 + C + T,0,X,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.5(A,B,C,D,E,F,H,N,Q,R) -> f9.0(17,1,0,S,E,F,H,N,Q,R) True f12.6(A,B,C,D,E,F,H,N,Q,R) -> exitus616(A,B,C,D,E,F,H,N,Q,R) True f12.6(A,B,C,D,E,F,H,N,Q,R) -> exitus616(A,B,C,D,E,F,H,N,Q,R) True f0.6(A,B,C,D,E,F,H,N,Q,R) -> exitus616(A,B,C,D,E,F,H,N,Q,R) True f0.6(A,B,C,D,E,F,H,N,Q,R) -> exitus616(A,B,C,D,E,F,H,N,Q,R) True Signature: {(exitus616,10);(f0.6,10);(f12.6,10);(f5.1,10);(f5.2,10);(f5.3,10);(f6.5,10);(f9.0,10);(f9.4,10)} Rule Graph: [0->{0,1},1->{7,8,9},2->{13,14},3->{2},4->{3,4,5},5->{6},6->{11,12},7->{2},8->{3,4,5},9->{6},10->{0,1}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14] | +- p:[0] c: [0] | `- p:[4] c: [4]) + Applied Processor: AbstractSize Minimize + Details: () * Step 8: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,F,H,N,Q,R,0.0,0.1] f9.0 ~> f9.0 [A <= A, B <= 17*K, C <= 16*K, D <= unknown, E <= E, F <= F, H <= H, N <= N, Q <= Q, R <= R] f9.0 ~> f9.4 [A <= A, B <= 17*K, C <= 16*K, D <= unknown, E <= E, F <= F, H <= H, N <= N, Q <= Q, R <= R] f5.1 ~> f0.6 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, H <= unknown, N <= N, Q <= Q, R <= R] f5.2 ~> f5.1 [A <= A, B <= B, C <= C, D <= D, E <= B + E, F <= K + F, H <= 0*K, N <= unknown, Q <= Q, R <= R] f5.2 ~> f5.2 [A <= A, B <= B, C <= C, D <= D, E <= B + E, F <= K + F, H <= 0*K, N <= unknown, Q <= Q, R <= R] f5.2 ~> f5.3 [A <= A, B <= B, C <= C, D <= D, E <= B + E, F <= K + F, H <= 0*K, N <= unknown, Q <= Q, R <= R] f5.3 ~> f12.6 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, H <= 0*K, N <= 0*K, Q <= unknown, R <= R] f9.4 ~> f5.1 [A <= A, B <= B, C <= C, D <= D, E <= K, F <= unknown, H <= 0*K, N <= unknown, Q <= D, R <= B] f9.4 ~> f5.2 [A <= A, B <= B, C <= C, D <= D, E <= K, F <= unknown, H <= 0*K, N <= unknown, Q <= D, R <= B] f9.4 ~> f5.3 [A <= A, B <= B, C <= C, D <= D, E <= K, F <= unknown, H <= 0*K, N <= unknown, Q <= D, R <= B] f6.5 ~> f9.0 [A <= 17*K, B <= K, C <= 0*K, D <= unknown, E <= E, F <= F, H <= H, N <= N, Q <= Q, R <= R] f12.6 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, H <= H, N <= N, Q <= Q, R <= R] f12.6 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, H <= H, N <= N, Q <= Q, R <= R] f0.6 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, H <= H, N <= N, Q <= Q, R <= R] f0.6 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, H <= H, N <= N, Q <= Q, R <= R] + Loop: [0.0 <= K + A + B] f9.0 ~> f9.0 [A <= A, B <= 17*K, C <= 16*K, D <= unknown, E <= E, F <= F, H <= H, N <= N, Q <= Q, R <= R] + Loop: [0.1 <= F] f5.2 ~> f5.2 [A <= A, B <= B, C <= C, D <= D, E <= B + E, F <= K + F, H <= 0*K, N <= unknown, Q <= Q, R <= R] + Applied Processor: AbstractFlow + Details: () * Step 9: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,H,N,Q,R,0.0,0.1] f9.0 ~> f9.0 [K ~=> B,K ~=> C,huge ~=> D] f9.0 ~> f9.4 [K ~=> B,K ~=> C,huge ~=> D] f5.1 ~> f0.6 [huge ~=> H] f5.2 ~> f5.1 [K ~=> H,huge ~=> N,B ~+> E,E ~+> E,F ~+> F,K ~+> F] f5.2 ~> f5.2 [K ~=> H,huge ~=> N,B ~+> E,E ~+> E,F ~+> F,K ~+> F] f5.2 ~> f5.3 [K ~=> H,huge ~=> N,B ~+> E,E ~+> E,F ~+> F,K ~+> F] f5.3 ~> f12.6 [K ~=> H,K ~=> N,huge ~=> Q] f9.4 ~> f5.1 [B ~=> R,D ~=> Q,K ~=> E,K ~=> H,huge ~=> F,huge ~=> N] f9.4 ~> f5.2 [B ~=> R,D ~=> Q,K ~=> E,K ~=> H,huge ~=> F,huge ~=> N] f9.4 ~> f5.3 [B ~=> R,D ~=> Q,K ~=> E,K ~=> H,huge ~=> F,huge ~=> N] f6.5 ~> f9.0 [K ~=> A,K ~=> B,K ~=> C,huge ~=> D] f12.6 ~> exitus616 [] f12.6 ~> exitus616 [] f0.6 ~> exitus616 [] f0.6 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f9.0 ~> f9.0 [K ~=> B,K ~=> C,huge ~=> D] + Loop: [F ~=> 0.1] f5.2 ~> f5.2 [K ~=> H,huge ~=> N,B ~+> E,E ~+> E,F ~+> F,K ~+> F] + Applied Processor: Lare + Details: Unknown bound. MAYBE