NO * Step 1: UnsatRules NO + 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 NO + 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 NO + 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: CloseWith NO + 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: CloseWith False + Details: () NO