MAYBE * Step 1: UnsatRules MAYBE + Considered Problem: Rules: 0. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] (?,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,10,20,1,20,0,0,H,I,J,K) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [D >= E && G = 0] (?,1) 3. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [1 + D >= E && E >= 2 + D && G = 0] (?,1) 4. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,H,I,J,K) [E = 1 + D && G = 0] (?,1) 5. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,N,I,J,K) [L >= 1 + M && E = 1 + D && G = 0] (?,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K) -> f40(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] (?,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,0,G,H,I,1 + J,K) [F = 0] (?,1) 10. f43(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,F,G,H,I,1 + J,K) [K >= 1 + N] (?,1) 11. f48(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 12. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 13. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 14. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,0,G,N,I,J,K) [F = 0] (?,1) 15. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 16. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,-1 + A,F,G,H,I,J,K) [A >= B] (?,1) 17. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,J,E,F,G,H,I,J,K) [B >= A] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,F,G,H,I,J,K) [A >= J] (?,1) 19. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,1,G,H,I,J,K) [J >= 1 + A] (?,1) 20. f43(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 21. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + G] (?,1) 22. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [G >= 1] (?,1) Signature: {(f0,11);(f11,11);(f40,11);(f43,11);(f48,11);(f54,11);(f59,11);(f63,11);(f69,11)} Flow Graph: [0->{2,3,4,5,6,21,22},1->{2,3,4,5,6,21,22},2->{2,3,4,5,6,21,22},3->{2,3,4,5,6,21,22},4->{2,3,4,5,6,21,22} ,5->{2,3,4,5,6,21,22},6->{7,8,9},7->{15,16},8->{15,16},9->{10,20},10->{10,20},11->{11,18,19},12->{7,8,9} ,13->{7,8,9},14->{7,8,9},15->{0,17},16->{0,17},17->{2,3,4,5,6,21,22},18->{12,13,14},19->{12,13,14},20->{11 ,18,19},21->{},22->{}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [3] * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] (?,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,10,20,1,20,0,0,H,I,J,K) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [D >= E && G = 0] (?,1) 4. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,H,I,J,K) [E = 1 + D && G = 0] (?,1) 5. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,N,I,J,K) [L >= 1 + M && E = 1 + D && G = 0] (?,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K) -> f40(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] (?,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,0,G,H,I,1 + J,K) [F = 0] (?,1) 10. f43(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,F,G,H,I,1 + J,K) [K >= 1 + N] (?,1) 11. f48(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 12. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 13. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 14. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,0,G,N,I,J,K) [F = 0] (?,1) 15. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 16. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,-1 + A,F,G,H,I,J,K) [A >= B] (?,1) 17. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,J,E,F,G,H,I,J,K) [B >= A] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,F,G,H,I,J,K) [A >= J] (?,1) 19. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,1,G,H,I,J,K) [J >= 1 + A] (?,1) 20. f43(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 21. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + G] (?,1) 22. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [G >= 1] (?,1) Signature: {(f0,11);(f11,11);(f40,11);(f43,11);(f48,11);(f54,11);(f59,11);(f63,11);(f69,11)} Flow Graph: [0->{2,4,5,6,21,22},1->{2,4,5,6,21,22},2->{2,4,5,6,21,22},4->{2,4,5,6,21,22},5->{2,4,5,6,21,22},6->{7,8,9} ,7->{15,16},8->{15,16},9->{10,20},10->{10,20},11->{11,18,19},12->{7,8,9},13->{7,8,9},14->{7,8,9},15->{0,17} ,16->{0,17},17->{2,4,5,6,21,22},18->{12,13,14},19->{12,13,14},20->{11,18,19},21->{},22->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,2) ,(1,4) ,(1,5) ,(1,21) ,(1,22) ,(2,2) ,(2,4) ,(2,5) ,(2,6) ,(2,21) ,(4,2) ,(4,4) ,(4,5) ,(4,6) ,(4,21) ,(5,2) ,(5,4) ,(5,5) ,(5,6) ,(5,21) ,(12,8) ,(12,9) ,(13,7) ,(13,9) ,(14,7) ,(14,8) ,(15,0) ,(19,12) ,(19,14)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] (?,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,10,20,1,20,0,0,H,I,J,K) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [D >= E && G = 0] (?,1) 4. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,H,I,J,K) [E = 1 + D && G = 0] (?,1) 5. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,N,I,J,K) [L >= 1 + M && E = 1 + D && G = 0] (?,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K) -> f40(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] (?,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,0,G,H,I,1 + J,K) [F = 0] (?,1) 10. f43(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,F,G,H,I,1 + J,K) [K >= 1 + N] (?,1) 11. f48(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 12. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 13. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 14. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,0,G,N,I,J,K) [F = 0] (?,1) 15. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 16. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,-1 + A,F,G,H,I,J,K) [A >= B] (?,1) 17. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,J,E,F,G,H,I,J,K) [B >= A] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,F,G,H,I,J,K) [A >= J] (?,1) 19. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,1,G,H,I,J,K) [J >= 1 + A] (?,1) 20. f43(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 21. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + G] (?,1) 22. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [G >= 1] (?,1) Signature: {(f0,11);(f11,11);(f40,11);(f43,11);(f48,11);(f54,11);(f59,11);(f63,11);(f69,11)} Flow Graph: [0->{2,4,5,6,21,22},1->{6},2->{22},4->{22},5->{22},6->{7,8,9},7->{15,16},8->{15,16},9->{10,20},10->{10,20} ,11->{11,18,19},12->{7},13->{8},14->{9},15->{17},16->{0,17},17->{2,4,5,6,21,22},18->{12,13,14},19->{13} ,20->{11,18,19},21->{},22->{}] + Applied Processor: FromIts + Details: () * Step 4: Unfold MAYBE + Considered Problem: Rules: f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] f0(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,10,20,1,20,0,0,H,I,J,K) True f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [D >= E && G = 0] f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,H,I,J,K) [E = 1 + D && G = 0] f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,N,I,J,K) [L >= 1 + M && E = 1 + D && G = 0] f11(A,B,C,D,E,F,G,H,I,J,K) -> f40(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] f40(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,0,G,H,I,1 + J,K) [F = 0] f43(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,F,G,H,I,1 + J,K) [K >= 1 + N] f48(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,0,G,N,I,J,K) [F = 0] f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,-1 + A,F,G,H,I,J,K) [A >= B] f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,J,E,F,G,H,I,J,K) [B >= A] f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,F,G,H,I,J,K) [A >= J] f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,1,G,H,I,J,K) [J >= 1 + A] f43(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + G] f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [G >= 1] Signature: {(f0,11);(f11,11);(f40,11);(f43,11);(f48,11);(f54,11);(f59,11);(f63,11);(f69,11)} Rule Graph: [0->{2,4,5,6,21,22},1->{6},2->{22},4->{22},5->{22},6->{7,8,9},7->{15,16},8->{15,16},9->{10,20},10->{10,20} ,11->{11,18,19},12->{7},13->{8},14->{9},15->{17},16->{0,17},17->{2,4,5,6,21,22},18->{12,13,14},19->{13} ,20->{11,18,19},21->{},22->{}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: f63.0(A,B,C,D,E,F,G,H,I,J,K) -> f11.2(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] f63.0(A,B,C,D,E,F,G,H,I,J,K) -> f11.4(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] f63.0(A,B,C,D,E,F,G,H,I,J,K) -> f11.5(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] f63.0(A,B,C,D,E,F,G,H,I,J,K) -> f11.6(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] f63.0(A,B,C,D,E,F,G,H,I,J,K) -> f11.21(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] f63.0(A,B,C,D,E,F,G,H,I,J,K) -> f11.22(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] f0.1(A,B,C,D,E,F,G,H,I,J,K) -> f11.6(A,10,20,1,20,0,0,H,I,J,K) True f11.2(A,B,C,D,E,F,G,H,I,J,K) -> f11.22(A,B,C,D,E,F,1,H,I,J,K) [D >= E && G = 0] f11.4(A,B,C,D,E,F,G,H,I,J,K) -> f11.22(A,B,C,D,1 + D,F,1,H,I,J,K) [E = 1 + D && G = 0] f11.5(A,B,C,D,E,F,G,H,I,J,K) -> f11.22(A,B,C,D,1 + D,F,1,N,I,J,K) [L >= 1 + M && E = 1 + D && G = 0] f11.6(A,B,C,D,E,F,G,H,I,J,K) -> f40.7(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] f11.6(A,B,C,D,E,F,G,H,I,J,K) -> f40.8(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] f11.6(A,B,C,D,E,F,G,H,I,J,K) -> f40.9(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] f40.7(A,B,C,D,E,F,G,H,I,J,K) -> f59.15(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] f40.7(A,B,C,D,E,F,G,H,I,J,K) -> f59.16(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] f40.8(A,B,C,D,E,F,G,H,I,J,K) -> f59.15(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] f40.8(A,B,C,D,E,F,G,H,I,J,K) -> f59.16(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] f40.9(A,B,C,D,E,F,G,H,I,J,K) -> f43.10(A,B,C,D,E,0,G,H,I,1 + J,K) [F = 0] f40.9(A,B,C,D,E,F,G,H,I,J,K) -> f43.20(A,B,C,D,E,0,G,H,I,1 + J,K) [F = 0] f43.10(A,B,C,D,E,F,G,H,I,J,K) -> f43.10(A,B,C,D,E,F,G,H,I,1 + J,K) [K >= 1 + N] f43.10(A,B,C,D,E,F,G,H,I,J,K) -> f43.20(A,B,C,D,E,F,G,H,I,1 + J,K) [K >= 1 + N] f48.11(A,B,C,D,E,F,G,H,I,J,K) -> f48.11(-1 + A,B,C,D,E,F,G,H,I,J,K) True f48.11(A,B,C,D,E,F,G,H,I,J,K) -> f48.18(-1 + A,B,C,D,E,F,G,H,I,J,K) True f48.11(A,B,C,D,E,F,G,H,I,J,K) -> f48.19(-1 + A,B,C,D,E,F,G,H,I,J,K) True f54.12(A,B,C,D,E,F,G,H,I,J,K) -> f40.7(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] f54.13(A,B,C,D,E,F,G,H,I,J,K) -> f40.8(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] f54.14(A,B,C,D,E,F,G,H,I,J,K) -> f40.9(A,B,C,D,E,0,G,N,I,J,K) [F = 0] f59.15(A,B,C,D,E,F,G,H,I,J,K) -> f63.17(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] f59.16(A,B,C,D,E,F,G,H,I,J,K) -> f63.0(A,B,C,D,-1 + A,F,G,H,I,J,K) [A >= B] f59.16(A,B,C,D,E,F,G,H,I,J,K) -> f63.17(A,B,C,D,-1 + A,F,G,H,I,J,K) [A >= B] f63.17(A,B,C,D,E,F,G,H,I,J,K) -> f11.2(A,B,C,J,E,F,G,H,I,J,K) [B >= A] f63.17(A,B,C,D,E,F,G,H,I,J,K) -> f11.4(A,B,C,J,E,F,G,H,I,J,K) [B >= A] f63.17(A,B,C,D,E,F,G,H,I,J,K) -> f11.5(A,B,C,J,E,F,G,H,I,J,K) [B >= A] f63.17(A,B,C,D,E,F,G,H,I,J,K) -> f11.6(A,B,C,J,E,F,G,H,I,J,K) [B >= A] f63.17(A,B,C,D,E,F,G,H,I,J,K) -> f11.21(A,B,C,J,E,F,G,H,I,J,K) [B >= A] f63.17(A,B,C,D,E,F,G,H,I,J,K) -> f11.22(A,B,C,J,E,F,G,H,I,J,K) [B >= A] f48.18(A,B,C,D,E,F,G,H,I,J,K) -> f54.12(A,B,C,D,E,F,G,H,I,J,K) [A >= J] f48.18(A,B,C,D,E,F,G,H,I,J,K) -> f54.13(A,B,C,D,E,F,G,H,I,J,K) [A >= J] f48.18(A,B,C,D,E,F,G,H,I,J,K) -> f54.14(A,B,C,D,E,F,G,H,I,J,K) [A >= J] f48.19(A,B,C,D,E,F,G,H,I,J,K) -> f54.13(A,B,C,D,E,1,G,H,I,J,K) [J >= 1 + A] f43.20(A,B,C,D,E,F,G,H,I,J,K) -> f48.11(-1 + A,B,C,D,E,F,G,H,I,J,K) True f43.20(A,B,C,D,E,F,G,H,I,J,K) -> f48.18(-1 + A,B,C,D,E,F,G,H,I,J,K) True f43.20(A,B,C,D,E,F,G,H,I,J,K) -> f48.19(-1 + A,B,C,D,E,F,G,H,I,J,K) True f11.21(A,B,C,D,E,F,G,H,I,J,K) -> f69.23(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + G] f11.22(A,B,C,D,E,F,G,H,I,J,K) -> f69.23(A,B,C,D,E,F,G,H,I,J,K) [G >= 1] Signature: {(f0.1,11) ;(f11.2,11) ;(f11.21,11) ;(f11.22,11) ;(f11.4,11) ;(f11.5,11) ;(f11.6,11) ;(f40.7,11) ;(f40.8,11) ;(f40.9,11) ;(f43.10,11) ;(f43.20,11) ;(f48.11,11) ;(f48.18,11) ;(f48.19,11) ;(f54.12,11) ;(f54.13,11) ;(f54.14,11) ;(f59.15,11) ;(f59.16,11) ;(f63.0,11) ;(f63.17,11) ;(f69.23,11)} Rule Graph: [0->{7},1->{8},2->{9},3->{10,11,12},4->{43},5->{44},6->{10,11,12},7->{44},8->{44},9->{44},10->{13,14} ,11->{15,16},12->{17,18},13->{27},14->{28,29},15->{27},16->{28,29},17->{19,20},18->{40,41,42},19->{19,20} ,20->{40,41,42},21->{21,22,23},22->{36,37,38},23->{39},24->{13,14},25->{15,16},26->{17,18},27->{30,31,32,33 ,34,35},28->{0,1,2,3,4,5},29->{30,31,32,33,34,35},30->{7},31->{8},32->{9},33->{10,11,12},34->{43},35->{44} ,36->{24},37->{25},38->{26},39->{25},40->{21,22,23},41->{36,37,38},42->{39},43->{},44->{}] + Applied Processor: AddSinks + Details: () * Step 6: Failure MAYBE + Considered Problem: Rules: f63.0(A,B,C,D,E,F,G,H,I,J,K) -> f11.2(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] f63.0(A,B,C,D,E,F,G,H,I,J,K) -> f11.4(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] f63.0(A,B,C,D,E,F,G,H,I,J,K) -> f11.5(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] f63.0(A,B,C,D,E,F,G,H,I,J,K) -> f11.6(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] f63.0(A,B,C,D,E,F,G,H,I,J,K) -> f11.21(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] f63.0(A,B,C,D,E,F,G,H,I,J,K) -> f11.22(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] f0.1(A,B,C,D,E,F,G,H,I,J,K) -> f11.6(A,10,20,1,20,0,0,H,I,J,K) True f11.2(A,B,C,D,E,F,G,H,I,J,K) -> f11.22(A,B,C,D,E,F,1,H,I,J,K) [D >= E && G = 0] f11.4(A,B,C,D,E,F,G,H,I,J,K) -> f11.22(A,B,C,D,1 + D,F,1,H,I,J,K) [E = 1 + D && G = 0] f11.5(A,B,C,D,E,F,G,H,I,J,K) -> f11.22(A,B,C,D,1 + D,F,1,N,I,J,K) [L >= 1 + M && E = 1 + D && G = 0] f11.6(A,B,C,D,E,F,G,H,I,J,K) -> f40.7(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] f11.6(A,B,C,D,E,F,G,H,I,J,K) -> f40.8(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] f11.6(A,B,C,D,E,F,G,H,I,J,K) -> f40.9(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] f40.7(A,B,C,D,E,F,G,H,I,J,K) -> f59.15(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] f40.7(A,B,C,D,E,F,G,H,I,J,K) -> f59.16(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] f40.8(A,B,C,D,E,F,G,H,I,J,K) -> f59.15(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] f40.8(A,B,C,D,E,F,G,H,I,J,K) -> f59.16(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] f40.9(A,B,C,D,E,F,G,H,I,J,K) -> f43.10(A,B,C,D,E,0,G,H,I,1 + J,K) [F = 0] f40.9(A,B,C,D,E,F,G,H,I,J,K) -> f43.20(A,B,C,D,E,0,G,H,I,1 + J,K) [F = 0] f43.10(A,B,C,D,E,F,G,H,I,J,K) -> f43.10(A,B,C,D,E,F,G,H,I,1 + J,K) [K >= 1 + N] f43.10(A,B,C,D,E,F,G,H,I,J,K) -> f43.20(A,B,C,D,E,F,G,H,I,1 + J,K) [K >= 1 + N] f48.11(A,B,C,D,E,F,G,H,I,J,K) -> f48.11(-1 + A,B,C,D,E,F,G,H,I,J,K) True f48.11(A,B,C,D,E,F,G,H,I,J,K) -> f48.18(-1 + A,B,C,D,E,F,G,H,I,J,K) True f48.11(A,B,C,D,E,F,G,H,I,J,K) -> f48.19(-1 + A,B,C,D,E,F,G,H,I,J,K) True f54.12(A,B,C,D,E,F,G,H,I,J,K) -> f40.7(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] f54.13(A,B,C,D,E,F,G,H,I,J,K) -> f40.8(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] f54.14(A,B,C,D,E,F,G,H,I,J,K) -> f40.9(A,B,C,D,E,0,G,N,I,J,K) [F = 0] f59.15(A,B,C,D,E,F,G,H,I,J,K) -> f63.17(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] f59.16(A,B,C,D,E,F,G,H,I,J,K) -> f63.0(A,B,C,D,-1 + A,F,G,H,I,J,K) [A >= B] f59.16(A,B,C,D,E,F,G,H,I,J,K) -> f63.17(A,B,C,D,-1 + A,F,G,H,I,J,K) [A >= B] f63.17(A,B,C,D,E,F,G,H,I,J,K) -> f11.2(A,B,C,J,E,F,G,H,I,J,K) [B >= A] f63.17(A,B,C,D,E,F,G,H,I,J,K) -> f11.4(A,B,C,J,E,F,G,H,I,J,K) [B >= A] f63.17(A,B,C,D,E,F,G,H,I,J,K) -> f11.5(A,B,C,J,E,F,G,H,I,J,K) [B >= A] f63.17(A,B,C,D,E,F,G,H,I,J,K) -> f11.6(A,B,C,J,E,F,G,H,I,J,K) [B >= A] f63.17(A,B,C,D,E,F,G,H,I,J,K) -> f11.21(A,B,C,J,E,F,G,H,I,J,K) [B >= A] f63.17(A,B,C,D,E,F,G,H,I,J,K) -> f11.22(A,B,C,J,E,F,G,H,I,J,K) [B >= A] f48.18(A,B,C,D,E,F,G,H,I,J,K) -> f54.12(A,B,C,D,E,F,G,H,I,J,K) [A >= J] f48.18(A,B,C,D,E,F,G,H,I,J,K) -> f54.13(A,B,C,D,E,F,G,H,I,J,K) [A >= J] f48.18(A,B,C,D,E,F,G,H,I,J,K) -> f54.14(A,B,C,D,E,F,G,H,I,J,K) [A >= J] f48.19(A,B,C,D,E,F,G,H,I,J,K) -> f54.13(A,B,C,D,E,1,G,H,I,J,K) [J >= 1 + A] f43.20(A,B,C,D,E,F,G,H,I,J,K) -> f48.11(-1 + A,B,C,D,E,F,G,H,I,J,K) True f43.20(A,B,C,D,E,F,G,H,I,J,K) -> f48.18(-1 + A,B,C,D,E,F,G,H,I,J,K) True f43.20(A,B,C,D,E,F,G,H,I,J,K) -> f48.19(-1 + A,B,C,D,E,F,G,H,I,J,K) True f11.21(A,B,C,D,E,F,G,H,I,J,K) -> f69.23(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + G] f11.22(A,B,C,D,E,F,G,H,I,J,K) -> f69.23(A,B,C,D,E,F,G,H,I,J,K) [G >= 1] f69.23(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True f69.23(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True f69.23(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True f69.23(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True f69.23(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True f69.23(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True f69.23(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True f69.23(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True f69.23(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True f69.23(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True Signature: {(exitus616,11) ;(f0.1,11) ;(f11.2,11) ;(f11.21,11) ;(f11.22,11) ;(f11.4,11) ;(f11.5,11) ;(f11.6,11) ;(f40.7,11) ;(f40.8,11) ;(f40.9,11) ;(f43.10,11) ;(f43.20,11) ;(f48.11,11) ;(f48.18,11) ;(f48.19,11) ;(f54.12,11) ;(f54.13,11) ;(f54.14,11) ;(f59.15,11) ;(f59.16,11) ;(f63.0,11) ;(f63.17,11) ;(f69.23,11)} Rule Graph: [0->{7},1->{8},2->{9},3->{10,11,12},4->{43},5->{44},6->{10,11,12},7->{44},8->{44},9->{44},10->{13,14} ,11->{15,16},12->{17,18},13->{27},14->{28,29},15->{27},16->{28,29},17->{19,20},18->{40,41,42},19->{19,20} ,20->{40,41,42},21->{21,22,23},22->{36,37,38},23->{39},24->{13,14},25->{15,16},26->{17,18},27->{30,31,32,33 ,34,35},28->{0,1,2,3,4,5},29->{30,31,32,33,34,35},30->{7},31->{8},32->{9},33->{10,11,12},34->{43},35->{44} ,36->{24},37->{25},38->{26},39->{25},40->{21,22,23},41->{36,37,38},42->{39},43->{46,48},44->{45,47,49,50,51 ,52,53,54}] + Applied Processor: Decompose Greedy + 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,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54] | `- p:[3,28,14,10,33,27,13,24,36,22,21,40,18,12,26,38,41,20,17,19,15,11,25,37,39,23,42,29,16] c: [] MAYBE