MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f38(A,B,C,D,E,F,G) -> f11(A,A,C,D,E,F,G) [A = B] (?,1) 1. f0(A,B,C,D,E,F,G) -> f11(0,0,H,0,1,I,I) [H >= 0 && I >= 1] (1,1) 2. f11(A,B,C,D,E,F,G) -> f34(0,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && 0 >= D] (?,1) 3. f11(A,B,C,D,E,F,G) -> f34(1,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && D = 1] (?,1) 4. f11(A,B,C,D,E,F,G) -> f34(0,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && D = 2] (?,1) 5. f11(A,B,C,D,E,F,G) -> f34(I,J,H,0,1 + E,F,G) [J >= 0 && 1 >= J && I >= 0 && 1 >= I && H >= 0 && G >= 1 && 0 >= C && D >= 3] (?,1) 6. f11(A,B,C,D,E,F,G) -> f34(H,I,-1 + C,D,E,F,G) [I >= 0 && 1 >= I && H >= 0 && 1 >= H && C >= 1 && G >= 1] (?,1) 7. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [0 >= B && 0 >= C && 0 >= D] (?,1) 8. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [B >= 1 && 0 >= C && D = 1] (?,1) 9. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [0 >= B && 0 >= C && D = 2] (?,1) 10. f34(A,B,C,D,E,F,G) -> f38(A,B,H,0,1 + E,F,G) [H >= 0 && 0 >= C && D >= 3] (?,1) 11. f34(A,B,C,D,E,F,G) -> f38(A,B,-1 + C,D,E,F,G) [C >= 1] (?,1) 12. f38(A,B,C,D,E,F,G) -> f11(A,B,C,D,E,F,-1 + G) [B >= 1 + A] (?,1) 13. f38(A,B,C,D,E,F,G) -> f11(A,B,C,D,E,F,-1 + G) [A >= 1 + B] (?,1) 14. f11(A,B,C,D,E,F,G) -> f53(A,B,C,D,E,F,G) [0 >= G] (?,1) Signature: {(f0,7);(f11,7);(f34,7);(f38,7);(f53,7)} Flow Graph: [0->{2,3,4,5,6,14},1->{2,3,4,5,6,14},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{7,8,9,10,11} ,6->{7,8,9,10,11},7->{0,12,13},8->{0,12,13},9->{0,12,13},10->{0,12,13},11->{0,12,13},12->{2,3,4,5,6,14} ,13->{2,3,4,5,6,14},14->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f38(A,B,C,D,E,F,G) -> f11(A,A,C,D,E,F,G) [A = B] (?,1) 1. f0(A,B,C,D,E,F,G) -> f11(0,0,H,0,1,I,I) [H >= 0 && I >= 1] (1,1) 2. f11(A,B,C,D,E,F,G) -> f34(0,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && 0 >= D] (?,1) 3. f11(A,B,C,D,E,F,G) -> f34(1,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && D = 1] (?,1) 4. f11(A,B,C,D,E,F,G) -> f34(0,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && D = 2] (?,1) 5. f11(A,B,C,D,E,F,G) -> f34(I,J,H,0,1 + E,F,G) [J >= 0 && 1 >= J && I >= 0 && 1 >= I && H >= 0 && G >= 1 && 0 >= C && D >= 3] (?,1) 6. f11(A,B,C,D,E,F,G) -> f34(H,I,-1 + C,D,E,F,G) [I >= 0 && 1 >= I && H >= 0 && 1 >= H && C >= 1 && G >= 1] (?,1) 7. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [0 >= B && 0 >= C && 0 >= D] (?,1) 8. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [B >= 1 && 0 >= C && D = 1] (?,1) 9. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [0 >= B && 0 >= C && D = 2] (?,1) 10. f34(A,B,C,D,E,F,G) -> f38(A,B,H,0,1 + E,F,G) [H >= 0 && 0 >= C && D >= 3] (?,1) 11. f34(A,B,C,D,E,F,G) -> f38(A,B,-1 + C,D,E,F,G) [C >= 1] (?,1) 12. f38(A,B,C,D,E,F,G) -> f11(A,B,C,D,E,F,-1 + G) [B >= 1 + A] (?,1) 13. f38(A,B,C,D,E,F,G) -> f11(A,B,C,D,E,F,-1 + G) [A >= 1 + B] (?,1) 14. f11(A,B,C,D,E,F,G) -> f53(A,B,C,D,E,F,G) [0 >= G] (1,1) Signature: {(f0,7);(f11,7);(f34,7);(f38,7);(f53,7)} Flow Graph: [0->{2,3,4,5,6,14},1->{2,3,4,5,6,14},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{7,8,9,10,11} ,6->{7,8,9,10,11},7->{0,12,13},8->{0,12,13},9->{0,12,13},10->{0,12,13},11->{0,12,13},12->{2,3,4,5,6,14} ,13->{2,3,4,5,6,14},14->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,3) ,(1,4) ,(1,5) ,(1,14) ,(2,9) ,(2,10) ,(2,11) ,(3,7) ,(3,8) ,(3,10) ,(3,11) ,(4,7) ,(4,8) ,(4,9) ,(4,11) ,(5,8) ,(5,9) ,(5,10)] * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. f38(A,B,C,D,E,F,G) -> f11(A,A,C,D,E,F,G) [A = B] (?,1) 1. f0(A,B,C,D,E,F,G) -> f11(0,0,H,0,1,I,I) [H >= 0 && I >= 1] (1,1) 2. f11(A,B,C,D,E,F,G) -> f34(0,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && 0 >= D] (?,1) 3. f11(A,B,C,D,E,F,G) -> f34(1,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && D = 1] (?,1) 4. f11(A,B,C,D,E,F,G) -> f34(0,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && D = 2] (?,1) 5. f11(A,B,C,D,E,F,G) -> f34(I,J,H,0,1 + E,F,G) [J >= 0 && 1 >= J && I >= 0 && 1 >= I && H >= 0 && G >= 1 && 0 >= C && D >= 3] (?,1) 6. f11(A,B,C,D,E,F,G) -> f34(H,I,-1 + C,D,E,F,G) [I >= 0 && 1 >= I && H >= 0 && 1 >= H && C >= 1 && G >= 1] (?,1) 7. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [0 >= B && 0 >= C && 0 >= D] (?,1) 8. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [B >= 1 && 0 >= C && D = 1] (?,1) 9. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [0 >= B && 0 >= C && D = 2] (?,1) 10. f34(A,B,C,D,E,F,G) -> f38(A,B,H,0,1 + E,F,G) [H >= 0 && 0 >= C && D >= 3] (?,1) 11. f34(A,B,C,D,E,F,G) -> f38(A,B,-1 + C,D,E,F,G) [C >= 1] (?,1) 12. f38(A,B,C,D,E,F,G) -> f11(A,B,C,D,E,F,-1 + G) [B >= 1 + A] (?,1) 13. f38(A,B,C,D,E,F,G) -> f11(A,B,C,D,E,F,-1 + G) [A >= 1 + B] (?,1) 14. f11(A,B,C,D,E,F,G) -> f53(A,B,C,D,E,F,G) [0 >= G] (1,1) Signature: {(f0,7);(f11,7);(f34,7);(f38,7);(f53,7)} Flow Graph: [0->{2,3,4,5,6,14},1->{2,6},2->{7,8},3->{9},4->{10},5->{7,11},6->{7,8,9,10,11},7->{0,12,13},8->{0,12,13} ,9->{0,12,13},10->{0,12,13},11->{0,12,13},12->{2,3,4,5,6,14},13->{2,3,4,5,6,14},14->{}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths MAYBE + Considered Problem: Rules: 0. f38(A,B,C,D,E,F,G) -> f11(A,A,C,D,E,F,G) [A = B] (?,1) 1. f0(A,B,C,D,E,F,G) -> f11(0,0,H,0,1,I,I) [H >= 0 && I >= 1] (1,1) 2. f11(A,B,C,D,E,F,G) -> f34(0,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && 0 >= D] (?,1) 3. f11(A,B,C,D,E,F,G) -> f34(1,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && D = 1] (?,1) 4. f11(A,B,C,D,E,F,G) -> f34(0,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && D = 2] (?,1) 5. f11(A,B,C,D,E,F,G) -> f34(I,J,H,0,1 + E,F,G) [J >= 0 && 1 >= J && I >= 0 && 1 >= I && H >= 0 && G >= 1 && 0 >= C && D >= 3] (?,1) 6. f11(A,B,C,D,E,F,G) -> f34(H,I,-1 + C,D,E,F,G) [I >= 0 && 1 >= I && H >= 0 && 1 >= H && C >= 1 && G >= 1] (?,1) 7. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [0 >= B && 0 >= C && 0 >= D] (?,1) 8. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [B >= 1 && 0 >= C && D = 1] (?,1) 9. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [0 >= B && 0 >= C && D = 2] (?,1) 10. f34(A,B,C,D,E,F,G) -> f38(A,B,H,0,1 + E,F,G) [H >= 0 && 0 >= C && D >= 3] (?,1) 11. f34(A,B,C,D,E,F,G) -> f38(A,B,-1 + C,D,E,F,G) [C >= 1] (?,1) 12. f38(A,B,C,D,E,F,G) -> f11(A,B,C,D,E,F,-1 + G) [B >= 1 + A] (?,1) 13. f38(A,B,C,D,E,F,G) -> f11(A,B,C,D,E,F,-1 + G) [A >= 1 + B] (?,1) 14. f11(A,B,C,D,E,F,G) -> f53(A,B,C,D,E,F,G) [0 >= G] (?,1) 15. f11(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True (?,1) Signature: {(exitus616,7);(f0,7);(f11,7);(f34,7);(f38,7);(f53,7)} Flow Graph: [0->{2,3,4,5,6,14,15},1->{2,3,4,5,6,14,15},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{7,8,9,10 ,11},6->{7,8,9,10,11},7->{0,12,13},8->{0,12,13},9->{0,12,13},10->{0,12,13},11->{0,12,13},12->{2,3,4,5,6,14 ,15},13->{2,3,4,5,6,14,15},14->{},15->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,3) ,(1,4) ,(1,5) ,(1,14) ,(2,9) ,(2,10) ,(2,11) ,(3,7) ,(3,8) ,(3,10) ,(3,11) ,(4,7) ,(4,8) ,(4,9) ,(4,11) ,(5,8) ,(5,9) ,(5,10)] * Step 5: Failure MAYBE + Considered Problem: Rules: 0. f38(A,B,C,D,E,F,G) -> f11(A,A,C,D,E,F,G) [A = B] (?,1) 1. f0(A,B,C,D,E,F,G) -> f11(0,0,H,0,1,I,I) [H >= 0 && I >= 1] (1,1) 2. f11(A,B,C,D,E,F,G) -> f34(0,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && 0 >= D] (?,1) 3. f11(A,B,C,D,E,F,G) -> f34(1,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && D = 1] (?,1) 4. f11(A,B,C,D,E,F,G) -> f34(0,H,C,1 + D,E,F,G) [H >= 0 && 1 >= H && G >= 1 && 0 >= C && D = 2] (?,1) 5. f11(A,B,C,D,E,F,G) -> f34(I,J,H,0,1 + E,F,G) [J >= 0 && 1 >= J && I >= 0 && 1 >= I && H >= 0 && G >= 1 && 0 >= C && D >= 3] (?,1) 6. f11(A,B,C,D,E,F,G) -> f34(H,I,-1 + C,D,E,F,G) [I >= 0 && 1 >= I && H >= 0 && 1 >= H && C >= 1 && G >= 1] (?,1) 7. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [0 >= B && 0 >= C && 0 >= D] (?,1) 8. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [B >= 1 && 0 >= C && D = 1] (?,1) 9. f34(A,B,C,D,E,F,G) -> f38(A,B,C,1 + D,E,F,G) [0 >= B && 0 >= C && D = 2] (?,1) 10. f34(A,B,C,D,E,F,G) -> f38(A,B,H,0,1 + E,F,G) [H >= 0 && 0 >= C && D >= 3] (?,1) 11. f34(A,B,C,D,E,F,G) -> f38(A,B,-1 + C,D,E,F,G) [C >= 1] (?,1) 12. f38(A,B,C,D,E,F,G) -> f11(A,B,C,D,E,F,-1 + G) [B >= 1 + A] (?,1) 13. f38(A,B,C,D,E,F,G) -> f11(A,B,C,D,E,F,-1 + G) [A >= 1 + B] (?,1) 14. f11(A,B,C,D,E,F,G) -> f53(A,B,C,D,E,F,G) [0 >= G] (?,1) 15. f11(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True (?,1) Signature: {(exitus616,7);(f0,7);(f11,7);(f34,7);(f38,7);(f53,7)} Flow Graph: [0->{2,3,4,5,6,14,15},1->{2,6,15},2->{7,8},3->{9},4->{10},5->{7,11},6->{7,8,9,10,11},7->{0,12,13},8->{0,12 ,13},9->{0,12,13},10->{0,12,13},11->{0,12,13},12->{2,3,4,5,6,14,15},13->{2,3,4,5,6,14,15},14->{},15->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15] | `- p:[0,7,2,12,8,6,13,9,3,10,4,11,5] c: [] MAYBE