MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [0 >= A] (?,1) 1. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [A >= 2] (?,1) 2. f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [B = 0] (?,1) 3. f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [255 >= C] (?,1) 4. f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [C >= 0] (?,1) 5. f0(A,B,C,D,E,F) -> f5(4,0,C,G,0,F) True (1,1) 6. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [0 >= 1 + B] (?,1) 7. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [B >= 1] (?,1) 8. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= E && D >= 1 + F] (?,1) 9. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 2 && D >= 1 + F] (?,1) 10. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= 1 + B && D >= 1 + F && E = 1] (?,1) 11. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [B >= 1 && D >= 1 + F && E = 1] (?,1) 12. f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [D >= 1 + F && B = 0 && E = 1] (?,1) 13. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [1 >= E && F >= 1 + D] (?,1) 14. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 3 && F >= 1 + D] (?,1) 15. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [0 >= 1 + B && F >= 1 + D && E = 2] (?,1) 16. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [B >= 1 && F >= 1 + D && E = 2] (?,1) 17. f9(A,B,C,D,E,F) -> f25(-1 + A,1,1 + -1*A + C,D,1,F) [F >= 1 + D && B = 0 && E = 2] (?,1) 18. f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [A = 1] (?,1) 19. f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [C >= 256] (?,1) 20. f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [0 >= 1 + C] (?,1) 21. f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [D = F] (?,1) Signature: {(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Flow Graph: [0->{2,6,7},1->{2,6,7},2->{8,9,10,11,12,13,14,15,16,17,21},3->{0,1,18},4->{0,1,18},5->{0,1,18},6->{8,9,10 ,11,12,13,14,15,16,17,21},7->{8,9,10,11,12,13,14,15,16,17,21},8->{3,19},9->{3,19},10->{3,19},11->{3,19} ,12->{3,19},13->{4,20},14->{4,20},15->{4,20},16->{4,20},17->{4,20},18->{},19->{},20->{},21->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [0 >= A] (?,1) 1. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [A >= 2] (?,1) 2. f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [B = 0] (?,1) 3. f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [255 >= C] (?,1) 4. f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [C >= 0] (?,1) 5. f0(A,B,C,D,E,F) -> f5(4,0,C,G,0,F) True (1,1) 6. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [0 >= 1 + B] (?,1) 7. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [B >= 1] (?,1) 8. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= E && D >= 1 + F] (?,1) 9. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 2 && D >= 1 + F] (?,1) 10. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= 1 + B && D >= 1 + F && E = 1] (?,1) 11. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [B >= 1 && D >= 1 + F && E = 1] (?,1) 12. f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [D >= 1 + F && B = 0 && E = 1] (?,1) 13. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [1 >= E && F >= 1 + D] (?,1) 14. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 3 && F >= 1 + D] (?,1) 15. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [0 >= 1 + B && F >= 1 + D && E = 2] (?,1) 16. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [B >= 1 && F >= 1 + D && E = 2] (?,1) 17. f9(A,B,C,D,E,F) -> f25(-1 + A,1,1 + -1*A + C,D,1,F) [F >= 1 + D && B = 0 && E = 2] (?,1) 18. f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [A = 1] (1,1) 19. f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [C >= 256] (1,1) 20. f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [0 >= 1 + C] (1,1) 21. f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [D = F] (1,1) Signature: {(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Flow Graph: [0->{2,6,7},1->{2,6,7},2->{8,9,10,11,12,13,14,15,16,17,21},3->{0,1,18},4->{0,1,18},5->{0,1,18},6->{8,9,10 ,11,12,13,14,15,16,17,21},7->{8,9,10,11,12,13,14,15,16,17,21},8->{3,19},9->{3,19},10->{3,19},11->{3,19} ,12->{3,19},13->{4,20},14->{4,20},15->{4,20},16->{4,20},17->{4,20},18->{},19->{},20->{},21->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,10) ,(2,11) ,(2,15) ,(2,16) ,(5,0) ,(5,18) ,(6,11) ,(6,12) ,(6,16) ,(6,17) ,(7,10) ,(7,12) ,(7,15) ,(7,17)] * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [0 >= A] (?,1) 1. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [A >= 2] (?,1) 2. f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [B = 0] (?,1) 3. f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [255 >= C] (?,1) 4. f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [C >= 0] (?,1) 5. f0(A,B,C,D,E,F) -> f5(4,0,C,G,0,F) True (1,1) 6. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [0 >= 1 + B] (?,1) 7. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [B >= 1] (?,1) 8. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= E && D >= 1 + F] (?,1) 9. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 2 && D >= 1 + F] (?,1) 10. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= 1 + B && D >= 1 + F && E = 1] (?,1) 11. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [B >= 1 && D >= 1 + F && E = 1] (?,1) 12. f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [D >= 1 + F && B = 0 && E = 1] (?,1) 13. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [1 >= E && F >= 1 + D] (?,1) 14. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 3 && F >= 1 + D] (?,1) 15. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [0 >= 1 + B && F >= 1 + D && E = 2] (?,1) 16. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [B >= 1 && F >= 1 + D && E = 2] (?,1) 17. f9(A,B,C,D,E,F) -> f25(-1 + A,1,1 + -1*A + C,D,1,F) [F >= 1 + D && B = 0 && E = 2] (?,1) 18. f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [A = 1] (1,1) 19. f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [C >= 256] (1,1) 20. f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [0 >= 1 + C] (1,1) 21. f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [D = F] (1,1) Signature: {(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Flow Graph: [0->{2,6,7},1->{2,6,7},2->{8,9,12,13,14,17,21},3->{0,1,18},4->{0,1,18},5->{1},6->{8,9,10,13,14,15,21} ,7->{8,9,11,13,14,16,21},8->{3,19},9->{3,19},10->{3,19},11->{3,19},12->{3,19},13->{4,20},14->{4,20},15->{4 ,20},16->{4,20},17->{4,20},18->{},19->{},20->{},21->{}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths MAYBE + Considered Problem: Rules: 0. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [0 >= A] (?,1) 1. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [A >= 2] (?,1) 2. f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [B = 0] (?,1) 3. f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [255 >= C] (?,1) 4. f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [C >= 0] (?,1) 5. f0(A,B,C,D,E,F) -> f5(4,0,C,G,0,F) True (1,1) 6. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [0 >= 1 + B] (?,1) 7. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [B >= 1] (?,1) 8. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= E && D >= 1 + F] (?,1) 9. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 2 && D >= 1 + F] (?,1) 10. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= 1 + B && D >= 1 + F && E = 1] (?,1) 11. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [B >= 1 && D >= 1 + F && E = 1] (?,1) 12. f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [D >= 1 + F && B = 0 && E = 1] (?,1) 13. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [1 >= E && F >= 1 + D] (?,1) 14. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 3 && F >= 1 + D] (?,1) 15. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [0 >= 1 + B && F >= 1 + D && E = 2] (?,1) 16. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [B >= 1 && F >= 1 + D && E = 2] (?,1) 17. f9(A,B,C,D,E,F) -> f25(-1 + A,1,1 + -1*A + C,D,1,F) [F >= 1 + D && B = 0 && E = 2] (?,1) 18. f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [A = 1] (?,1) 19. f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [C >= 256] (?,1) 20. f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [0 >= 1 + C] (?,1) 21. f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [D = F] (?,1) 22. f9(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True (?,1) 23. f25(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True (?,1) 24. f5(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True (?,1) 25. f16(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True (?,1) Signature: {(exitus616,6);(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Flow Graph: [0->{2,6,7},1->{2,6,7},2->{8,9,10,11,12,13,14,15,16,17,21,22},3->{0,1,18,24},4->{0,1,18,24},5->{0,1,18,24} ,6->{8,9,10,11,12,13,14,15,16,17,21,22},7->{8,9,10,11,12,13,14,15,16,17,21,22},8->{3,19,25},9->{3,19,25} ,10->{3,19,25},11->{3,19,25},12->{3,19,25},13->{4,20,23},14->{4,20,23},15->{4,20,23},16->{4,20,23},17->{4,20 ,23},18->{},19->{},20->{},21->{},22->{},23->{},24->{},25->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,10) ,(2,11) ,(2,15) ,(2,16) ,(5,0) ,(5,18) ,(6,11) ,(6,12) ,(6,16) ,(6,17) ,(7,10) ,(7,12) ,(7,15) ,(7,17)] * Step 5: Failure MAYBE + Considered Problem: Rules: 0. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [0 >= A] (?,1) 1. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [A >= 2] (?,1) 2. f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [B = 0] (?,1) 3. f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [255 >= C] (?,1) 4. f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [C >= 0] (?,1) 5. f0(A,B,C,D,E,F) -> f5(4,0,C,G,0,F) True (1,1) 6. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [0 >= 1 + B] (?,1) 7. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [B >= 1] (?,1) 8. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= E && D >= 1 + F] (?,1) 9. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 2 && D >= 1 + F] (?,1) 10. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= 1 + B && D >= 1 + F && E = 1] (?,1) 11. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [B >= 1 && D >= 1 + F && E = 1] (?,1) 12. f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [D >= 1 + F && B = 0 && E = 1] (?,1) 13. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [1 >= E && F >= 1 + D] (?,1) 14. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 3 && F >= 1 + D] (?,1) 15. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [0 >= 1 + B && F >= 1 + D && E = 2] (?,1) 16. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [B >= 1 && F >= 1 + D && E = 2] (?,1) 17. f9(A,B,C,D,E,F) -> f25(-1 + A,1,1 + -1*A + C,D,1,F) [F >= 1 + D && B = 0 && E = 2] (?,1) 18. f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [A = 1] (?,1) 19. f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [C >= 256] (?,1) 20. f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [0 >= 1 + C] (?,1) 21. f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [D = F] (?,1) 22. f9(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True (?,1) 23. f25(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True (?,1) 24. f5(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True (?,1) 25. f16(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True (?,1) Signature: {(exitus616,6);(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Flow Graph: [0->{2,6,7},1->{2,6,7},2->{8,9,12,13,14,17,21,22},3->{0,1,18,24},4->{0,1,18,24},5->{1,24},6->{8,9,10,13,14 ,15,21,22},7->{8,9,11,13,14,16,21,22},8->{3,19,25},9->{3,19,25},10->{3,19,25},11->{3,19,25},12->{3,19,25} ,13->{4,20,23},14->{4,20,23},15->{4,20,23},16->{4,20,23},17->{4,20,23},18->{},19->{},20->{},21->{},22->{} ,23->{},24->{},25->{}] + 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,16,17,18,19,20,21,22,23,24,25] | `- p:[0,3,8,2,1,4,13,6,7,14,15,16,17,9,10,11,12] c: [17] | `- p:[0,3,8,2,1,4,13,6,7,14,15,16,9,10,11,12] c: [12] | `- p:[0,3,8,2,1,4,13,6,7,14,15,16,9,10,11] c: [] MAYBE