NO * Step 1: UnsatPaths NO + 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: 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 2: FromIts NO + 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,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: FromIts + Details: () * Step 3: CloseWith NO + Considered Problem: Rules: f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [0 >= A] f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [A >= 2] f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [B = 0] f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [255 >= C] f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [C >= 0] f0(A,B,C,D,E,F) -> f5(4,0,C,G,0,F) True f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [B >= 1] f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= E && D >= 1 + F] f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 2 && D >= 1 + F] f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= 1 + B && D >= 1 + F && E = 1] f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [B >= 1 && D >= 1 + F && E = 1] f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [D >= 1 + F && B = 0 && E = 1] f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [1 >= E && F >= 1 + D] f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 3 && F >= 1 + D] f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [0 >= 1 + B && F >= 1 + D && E = 2] f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [B >= 1 && F >= 1 + D && E = 2] 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] f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [A = 1] f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [C >= 256] f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [0 >= 1 + C] f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [D = F] Signature: {(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Rule 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: CloseWith False + Details: () NO