MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,0) True (1,1) 1. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f11(1 + A,B,C,D,1,F,U,V,W,X,D,U,U,U,P,P,1,1,0,T) [-1*C >= 0 (?,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && 0 >= U && B >= 1 + A] 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f35(A,B,C,D,Y,F,U,V,W,X,D,U,U,U,P,0,Y,Y,0,T) [-1*C >= 0 (?,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && B >= 1 + A && 0 >= U && 0 >= Y] 3. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f35(A,B,C,D,Y,F,U,V,W,X,D,U,U,U,P,0,Y,Y,0,T) [-1*C >= 0 (?,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && B >= 1 + A && 0 >= U && Y >= 2] 4. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,U,V,W,X,D,U,U,N,O,P,Q,R,S,T) [-1*C >= 0 (?,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && U >= 1 && B >= 1 + A] 5. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*C >= 0 (?,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && A >= B] 6. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && 1 >= E] 7. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && E = 2] 8. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && E >= 3] 9. f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D >= 0 (?,1) && C + -1*D >= 0 && -1*C + -1*D >= 0 && -1*D + T >= 0 && -1*D + -1*T >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && D + T >= 0 && D + -1*T >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0] Signature: {(f0,20);(f11,20);(f35,20);(f49,20)} Flow Graph: [0->{1,2,3,4,5},1->{1,2,3,4,5},2->{6,7,8},3->{6,7,8},4->{9},5->{9},6->{9},7->{9},8->{9},9->{9}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,7),(2,8),(3,6)] * Step 2: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,0) True (1,1) 1. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f11(1 + A,B,C,D,1,F,U,V,W,X,D,U,U,U,P,P,1,1,0,T) [-1*C >= 0 (?,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && 0 >= U && B >= 1 + A] 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f35(A,B,C,D,Y,F,U,V,W,X,D,U,U,U,P,0,Y,Y,0,T) [-1*C >= 0 (?,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && B >= 1 + A && 0 >= U && 0 >= Y] 3. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f35(A,B,C,D,Y,F,U,V,W,X,D,U,U,U,P,0,Y,Y,0,T) [-1*C >= 0 (?,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && B >= 1 + A && 0 >= U && Y >= 2] 4. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,U,V,W,X,D,U,U,N,O,P,Q,R,S,T) [-1*C >= 0 (?,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && U >= 1 && B >= 1 + A] 5. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*C >= 0 (?,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && A >= B] 6. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && 1 >= E] 7. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && E = 2] 8. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 (?,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && E >= 3] 9. f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D >= 0 (?,1) && C + -1*D >= 0 && -1*C + -1*D >= 0 && -1*D + T >= 0 && -1*D + -1*T >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && D + T >= 0 && D + -1*T >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0] Signature: {(f0,20);(f11,20);(f35,20);(f49,20)} Flow Graph: [0->{1,2,3,4,5},1->{1,2,3,4,5},2->{6},3->{7,8},4->{9},5->{9},6->{9},7->{9},8->{9},9->{9}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: PolyRank MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,0) True (1,1) 1. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f11(1 + A,B,C,D,1,F,U,V,W,X,D,U,U,U,P,P,1,1,0,T) [-1*C >= 0 (?,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && 0 >= U && B >= 1 + A] 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f35(A,B,C,D,Y,F,U,V,W,X,D,U,U,U,P,0,Y,Y,0,T) [-1*C >= 0 (1,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && B >= 1 + A && 0 >= U && 0 >= Y] 3. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f35(A,B,C,D,Y,F,U,V,W,X,D,U,U,U,P,0,Y,Y,0,T) [-1*C >= 0 (1,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && B >= 1 + A && 0 >= U && Y >= 2] 4. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,U,V,W,X,D,U,U,N,O,P,Q,R,S,T) [-1*C >= 0 (1,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && U >= 1 && B >= 1 + A] 5. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*C >= 0 (1,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && A >= B] 6. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 (1,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && 1 >= E] 7. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 (1,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && E = 2] 8. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 (1,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && E >= 3] 9. f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D >= 0 (?,1) && C + -1*D >= 0 && -1*C + -1*D >= 0 && -1*D + T >= 0 && -1*D + -1*T >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && D + T >= 0 && D + -1*T >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0] Signature: {(f0,20);(f11,20);(f35,20);(f49,20)} Flow Graph: [0->{1,2,3,4,5},1->{1,2,3,4,5},2->{6},3->{7,8},4->{9},5->{9},6->{9},7->{9},8->{9},9->{9}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = -1*x1 + x2 p(f11) = -1*x1 + x2 p(f35) = -1*x1 + x2 p(f49) = -1*x1 + x2 Following rules are strictly oriented: [-1*C >= 0 ==> && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && 0 >= U && B >= 1 + A] f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) = -1*A + B > -1 + -1*A + B = f11(1 + A,B,C,D,1,F,U,V,W,X,D,U,U,U,P,P,1,1,0,T) Following rules are weakly oriented: True ==> f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) = -1*A + B >= -1*A + B = f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,0) [-1*C >= 0 ==> && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && B >= 1 + A && 0 >= U && 0 >= Y] f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) = -1*A + B >= -1*A + B = f35(A,B,C,D,Y,F,U,V,W,X,D,U,U,U,P,0,Y,Y,0,T) [-1*C >= 0 ==> && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && B >= 1 + A && 0 >= U && Y >= 2] f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) = -1*A + B >= -1*A + B = f35(A,B,C,D,Y,F,U,V,W,X,D,U,U,U,P,0,Y,Y,0,T) [-1*C >= 0 ==> && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && U >= 1 && B >= 1 + A] f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) = -1*A + B >= -1*A + B = f49(A,B,0,0,E,F,U,V,W,X,D,U,U,N,O,P,Q,R,S,T) [-1*C >= 0 ==> && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && A >= B] f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) = -1*A + B >= -1*A + B = f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 ==> && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && 1 >= E] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) = -1*A + B >= -1*A + B = f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 ==> && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && E = 2] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) = -1*A + B >= -1*A + B = f49(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 ==> && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && E >= 3] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) = -1*A + B >= -1*A + B = f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D >= 0 ==> && C + -1*D >= 0 && -1*C + -1*D >= 0 && -1*D + T >= 0 && -1*D + -1*T >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && D + T >= 0 && D + -1*T >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0] f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) = -1*A + B >= -1*A + B = f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) * Step 4: Failure MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,0) True (1,1) 1. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f11(1 + A,B,C,D,1,F,U,V,W,X,D,U,U,U,P,P,1,1,0,T) [-1*C >= 0 (A + B,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && 0 >= U && B >= 1 + A] 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f35(A,B,C,D,Y,F,U,V,W,X,D,U,U,U,P,0,Y,Y,0,T) [-1*C >= 0 (1,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && B >= 1 + A && 0 >= U && 0 >= Y] 3. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f35(A,B,C,D,Y,F,U,V,W,X,D,U,U,U,P,0,Y,Y,0,T) [-1*C >= 0 (1,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && B >= 1 + A && 0 >= U && Y >= 2] 4. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,U,V,W,X,D,U,U,N,O,P,Q,R,S,T) [-1*C >= 0 (1,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && U >= 1 && B >= 1 + A] 5. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*C >= 0 (1,1) && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0 && A >= B] 6. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 (1,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && 1 >= E] 7. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 (1,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && E = 2] 8. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D + K >= 0 (1,1) && D + -1*K >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && -1*C + S >= 0 && -1*C + -1*S >= 0 && -1*C + P >= 0 && -1*C + -1*P >= 0 && -1*C + -1*N >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && C + S >= 0 && C + -1*S >= 0 && C + P >= 0 && C + -1*P >= 0 && C + -1*N >= 0 && -1*T >= 0 && S + -1*T >= 0 && -1*S + -1*T >= 0 && P + -1*T >= 0 && -1*P + -1*T >= 0 && -1*N + -1*T >= 0 && T >= 0 && S + T >= 0 && -1*S + T >= 0 && P + T >= 0 && -1*P + T >= 0 && -1*N + T >= 0 && -1 + -1*A + B >= 0 && -1*S >= 0 && P + -1*S >= 0 && -1*P + -1*S >= 0 && -1*N + -1*S >= 0 && S >= 0 && P + S >= 0 && -1*P + S >= 0 && -1*N + S >= 0 && -1*P >= 0 && -1*N + -1*P >= 0 && P >= 0 && -1*N + P >= 0 && -1*N >= 0 && E >= 3] 9. f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [-1*D >= 0 (?,1) && C + -1*D >= 0 && -1*C + -1*D >= 0 && -1*D + T >= 0 && -1*D + -1*T >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && D + T >= 0 && D + -1*T >= 0 && -1*C >= 0 && -1*C + T >= 0 && -1*C + -1*T >= 0 && C >= 0 && C + T >= 0 && C + -1*T >= 0 && -1*T >= 0 && T >= 0] Signature: {(f0,20);(f11,20);(f35,20);(f49,20)} Flow Graph: [0->{1,2,3,4,5},1->{1,2,3,4,5},2->{6},3->{7,8},4->{9},5->{9},6->{9},7->{9},8->{9},9->{9}] + Applied Processor: Failing "Open problems left." + Details: Open problems left. MAYBE