YES * Step 1: TrivialSCCs YES + Considered Problem: Rules: 0. f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) [A >= B] (?,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) True (1,1) 2. f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] (?,1) 3. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) True (1,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,A,M,N,O,P) [A = B] (?,1) 5. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,B,M,N,O,P) True (1,1) 6. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,M,N,M,N,K,L) True (1,1) 7. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,A,B,I,J,K,L) True (1,1) 8. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] (?,1) 9. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [A >= 1 + B] (?,1) 10. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) 11. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) 12. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) Signature: {(f0,12);(f3,12);(f4,12);(f8,12)} Flow Graph: [0->{4,8,9},1->{4,8,9},2->{4,8,9},3->{4,8,9},4->{},5->{},6->{4,8,9},7->{4,8,9},8->{0,2},9->{0,2},10->{} ,11->{0,2},12->{4,8,9}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths YES + Considered Problem: Rules: 0. f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) [A >= B] (?,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) True (1,1) 2. f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] (?,1) 3. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) True (1,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,A,M,N,O,P) [A = B] (1,1) 5. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,B,M,N,O,P) True (1,1) 6. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,M,N,M,N,K,L) True (1,1) 7. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,A,B,I,J,K,L) True (1,1) 8. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] (?,1) 9. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [A >= 1 + B] (?,1) 10. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) 11. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) 12. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) Signature: {(f0,12);(f3,12);(f4,12);(f8,12)} Flow Graph: [0->{4,8,9},1->{4,8,9},2->{4,8,9},3->{4,8,9},4->{},5->{},6->{4,8,9},7->{4,8,9},8->{0,2},9->{0,2},10->{} ,11->{0,2},12->{4,8,9}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,9),(8,0),(9,2)] * Step 3: Looptree YES + Considered Problem: Rules: 0. f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) [A >= B] (?,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) True (1,1) 2. f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] (?,1) 3. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) True (1,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,A,M,N,O,P) [A = B] (1,1) 5. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,B,M,N,O,P) True (1,1) 6. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,M,N,M,N,K,L) True (1,1) 7. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,A,B,I,J,K,L) True (1,1) 8. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] (?,1) 9. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [A >= 1 + B] (?,1) 10. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) 11. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) 12. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) Signature: {(f0,12);(f3,12);(f4,12);(f8,12)} Flow Graph: [0->{4,8,9},1->{4,8,9},2->{4,8},3->{4,8,9},4->{},5->{},6->{4,8,9},7->{4,8,9},8->{2},9->{0},10->{},11->{0 ,2},12->{4,8,9}] + Applied Processor: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | +- p:[0,9] c: [9] | `- p:[8,2] c: [8] YES