MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) 1. f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A >= B] (?,1) 3. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [D >= 3] (?,1) 4. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [1 >= D] (?,1) 5. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,2,F,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [D = 2] (?,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,U,V,W,X,C,U,U,M,N,O,P,Q,R,S,T) [U >= 1 && B >= 1 + A] (?,1) 7. 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,Y,E,U,V,W,X,C,U,U,U,O,0,Y,Y,0,S,T) [B >= 1 + A && 0 >= U && Y >= 2] (?,1) 8. 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,Y,E,U,V,W,X,C,U,U,U,O,0,Y,Y,0,S,T) [B >= 1 + A && 0 >= U && 0 >= Y] (?,1) 9. 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,1,E,U,V,W,X,C,U,U,U,O,O,1,1,0,S,T) [0 >= U && B >= 1 + A] (?,1) 10. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0,0) True (1,1) Signature: {(f0,20);(f11,20);(f35,20);(f47,20);(f49,20);(f52,20)} Flow Graph: [0->{0},1->{},2->{0},3->{0},4->{0},5->{0},6->{0},7->{3,4,5},8->{3,4,5},9->{2,6,7,8,9},10->{2,6,7,8,9}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) 1. f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A >= B] (1,1) 3. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [D >= 3] (1,1) 4. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [1 >= D] (1,1) 5. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,2,F,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [D = 2] (1,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,U,V,W,X,C,U,U,M,N,O,P,Q,R,S,T) [U >= 1 && B >= 1 + A] (1,1) 7. 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,Y,E,U,V,W,X,C,U,U,U,O,0,Y,Y,0,S,T) [B >= 1 + A && 0 >= U && Y >= 2] (1,1) 8. 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,Y,E,U,V,W,X,C,U,U,U,O,0,Y,Y,0,S,T) [B >= 1 + A && 0 >= U && 0 >= Y] (1,1) 9. 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,1,E,U,V,W,X,C,U,U,U,O,O,1,1,0,S,T) [0 >= U && B >= 1 + A] (?,1) 10. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0,0) True (1,1) Signature: {(f0,20);(f11,20);(f35,20);(f47,20);(f49,20);(f52,20)} Flow Graph: [0->{0},1->{},2->{0},3->{0},4->{0},5->{0},6->{0},7->{3,4,5},8->{3,4,5},9->{2,6,7,8,9},10->{2,6,7,8,9}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(7,4),(8,3),(8,5)] * Step 3: UnreachableRules MAYBE + Considered Problem: Rules: 0. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) 1. f49(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A >= B] (1,1) 3. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [D >= 3] (1,1) 4. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [1 >= D] (1,1) 5. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,2,F,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [D = 2] (1,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,U,V,W,X,C,U,U,M,N,O,P,Q,R,S,T) [U >= 1 && B >= 1 + A] (1,1) 7. 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,Y,E,U,V,W,X,C,U,U,U,O,0,Y,Y,0,S,T) [B >= 1 + A && 0 >= U && Y >= 2] (1,1) 8. 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,Y,E,U,V,W,X,C,U,U,U,O,0,Y,Y,0,S,T) [B >= 1 + A && 0 >= U && 0 >= Y] (1,1) 9. 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,1,E,U,V,W,X,C,U,U,U,O,O,1,1,0,S,T) [0 >= U && B >= 1 + A] (?,1) 10. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0,0) True (1,1) Signature: {(f0,20);(f11,20);(f35,20);(f47,20);(f49,20);(f52,20)} Flow Graph: [0->{0},1->{},2->{0},3->{0},4->{0},5->{0},6->{0},7->{3,5},8->{4},9->{2,6,7,8,9},10->{2,6,7,8,9}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [1] * Step 4: AddSinks MAYBE + Considered Problem: Rules: 0. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A >= B] (1,1) 3. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [D >= 3] (1,1) 4. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [1 >= D] (1,1) 5. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,2,F,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [D = 2] (1,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,U,V,W,X,C,U,U,M,N,O,P,Q,R,S,T) [U >= 1 && B >= 1 + A] (1,1) 7. 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,Y,E,U,V,W,X,C,U,U,U,O,0,Y,Y,0,S,T) [B >= 1 + A && 0 >= U && Y >= 2] (1,1) 8. 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,Y,E,U,V,W,X,C,U,U,U,O,0,Y,Y,0,S,T) [B >= 1 + A && 0 >= U && 0 >= Y] (1,1) 9. 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,1,E,U,V,W,X,C,U,U,U,O,O,1,1,0,S,T) [0 >= U && B >= 1 + A] (?,1) 10. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0,0) True (1,1) Signature: {(f0,20);(f11,20);(f35,20);(f47,20);(f49,20);(f52,20)} Flow Graph: [0->{0},2->{0},3->{0},4->{0},5->{0},6->{0},7->{3,5},8->{4},9->{2,6,7,8,9},10->{2,6,7,8,9}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths MAYBE + Considered Problem: Rules: 0. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A >= B] (?,1) 3. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [D >= 3] (?,1) 4. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [1 >= D] (?,1) 5. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,2,F,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [D = 2] (?,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,U,V,W,X,C,U,U,M,N,O,P,Q,R,S,T) [U >= 1 && B >= 1 + A] (?,1) 7. 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,Y,E,U,V,W,X,C,U,U,U,O,0,Y,Y,0,S,T) [B >= 1 + A && 0 >= U && Y >= 2] (?,1) 8. 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,Y,E,U,V,W,X,C,U,U,U,O,0,Y,Y,0,S,T) [B >= 1 + A && 0 >= U && 0 >= Y] (?,1) 9. 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,1,E,U,V,W,X,C,U,U,U,O,O,1,1,0,S,T) [0 >= U && B >= 1 + A] (?,1) 10. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0,0) True (1,1) 11. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) Signature: {(exitus616,20);(f0,20);(f11,20);(f35,20);(f47,20);(f49,20);(f52,20)} Flow Graph: [0->{0,11},2->{0,11},3->{0,11},4->{0,11},5->{0,11},6->{0,11},7->{3,4,5},8->{3,4,5},9->{2,6,7,8,9},10->{2,6 ,7,8,9},11->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(7,4),(8,3),(8,5)] * Step 6: Failure MAYBE + Considered Problem: Rules: 0. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A >= B] (?,1) 3. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [D >= 3] (?,1) 4. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [1 >= D] (?,1) 5. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,2,F,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [D = 2] (?,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f47(A,B,0,D,E,U,V,W,X,C,U,U,M,N,O,P,Q,R,S,T) [U >= 1 && B >= 1 + A] (?,1) 7. 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,Y,E,U,V,W,X,C,U,U,U,O,0,Y,Y,0,S,T) [B >= 1 + A && 0 >= U && Y >= 2] (?,1) 8. 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,Y,E,U,V,W,X,C,U,U,U,O,0,Y,Y,0,S,T) [B >= 1 + A && 0 >= U && 0 >= Y] (?,1) 9. 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,1,E,U,V,W,X,C,U,U,U,O,O,1,1,0,S,T) [0 >= U && B >= 1 + A] (?,1) 10. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0,0) True (1,1) 11. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) Signature: {(exitus616,20);(f0,20);(f11,20);(f35,20);(f47,20);(f49,20);(f52,20)} Flow Graph: [0->{0,11},2->{0,11},3->{0,11},4->{0,11},5->{0,11},6->{0,11},7->{3,5},8->{4},9->{2,6,7,8,9},10->{2,6,7,8 ,9},11->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,2,3,4,5,6,7,8,9,10,11] | +- p:[9] c: [9] | `- p:[0] c: [] MAYBE