YES * Step 1: TrivialSCCs YES + Considered Problem: Rules: 0. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) 1. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 2. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] 3. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] 4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] (?,1) 5. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 6. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] Signature: {(f1,24);(f10,24);(f3,24);(f4,24)} Flow Graph: [0->{2,3,4},1->{},2->{5,6,7,8,9},3->{5,6,7,8,9},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9} ,8->{5,6,7,8,9},9->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths YES + Considered Problem: Rules: 0. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) 1. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 2. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [A + -1*B >= 0 (1,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] 3. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [A + -1*B >= 0 (1,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] 4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] (?,1) 5. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 6. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [O + -1*U >= 0 (1,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] Signature: {(f1,24);(f10,24);(f3,24);(f4,24)} Flow Graph: [0->{2,3,4},1->{},2->{5,6,7,8,9},3->{5,6,7,8,9},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9} ,8->{5,6,7,8,9},9->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,9),(3,9)] * Step 3: Looptree YES + Considered Problem: Rules: 0. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) 1. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 2. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [A + -1*B >= 0 (1,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] 3. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [A + -1*B >= 0 (1,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] 4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] (?,1) 5. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 6. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [O + -1*U >= 0 (1,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] Signature: {(f1,24);(f10,24);(f3,24);(f4,24)} Flow Graph: [0->{2,3,4},1->{},2->{5,6,7,8},3->{5,6,7,8},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9},8->{5 ,6,7,8,9},9->{}] + Applied Processor: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9] | +- p:[4] c: [4] | `- p:[5,6,7,8] c: [8] | `- p:[5,6,7] c: [7] | `- p:[5,6] c: [6] | `- p:[5] c: [5] YES