NO * Step 1: UnsatPaths NO + Considered Problem: Rules: 0. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= A] 1. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A >= 2] 2. f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] 3. f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [-1 + D + -1*F >= 0 (?,1) && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 255 >= C] 4. f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [-1 + -1*D + F >= 0 (?,1) && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 0] 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) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] 7. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= E && D >= 1 + F] 8. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 2 && D >= 1 + F] 9. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && D >= 1 + F && E = 1] 10. f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D >= 1 + F && B = 0 && E = 1] 11. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 1 >= E && F >= 1 + D] 12. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 3 && F >= 1 + D] 13. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && F >= 1 + D && E = 2] 14. f9(A,B,C,D,E,F) -> f25(-1 + A,1,1 + -1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && F >= 1 + D && B = 0 && E = 2] 15. f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A = 1] 16. f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [-1 + D + -1*F >= 0 (?,1) && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 256] 17. f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [-1 + -1*D + F >= 0 (?,1) && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= 1 + C] 18. f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D = F] Signature: {(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Flow Graph: [0->{2,6},1->{2,6},2->{7,8,9,10,11,12,13,14,18},3->{0,1,15},4->{0,1,15},5->{0,1,15},6->{7,8,9,10,11,12,13 ,14,18},7->{3,16},8->{3,16},9->{3,16},10->{3,16},11->{4,17},12->{4,17},13->{4,17},14->{4,17},15->{},16->{} ,17->{},18->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,9),(2,13),(5,0),(5,15),(6,10),(6,14)] * Step 2: FromIts NO + Considered Problem: Rules: 0. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= A] 1. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A >= 2] 2. f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] 3. f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [-1 + D + -1*F >= 0 (?,1) && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 255 >= C] 4. f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [-1 + -1*D + F >= 0 (?,1) && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 0] 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) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] 7. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= E && D >= 1 + F] 8. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 2 && D >= 1 + F] 9. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && D >= 1 + F && E = 1] 10. f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D >= 1 + F && B = 0 && E = 1] 11. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 1 >= E && F >= 1 + D] 12. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 3 && F >= 1 + D] 13. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && F >= 1 + D && E = 2] 14. f9(A,B,C,D,E,F) -> f25(-1 + A,1,1 + -1*A + C,D,1,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && F >= 1 + D && B = 0 && E = 2] 15. f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A = 1] 16. f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [-1 + D + -1*F >= 0 (?,1) && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 256] 17. f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [-1 + -1*D + F >= 0 (?,1) && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= 1 + C] 18. f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [E >= 0 (?,1) && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D = F] Signature: {(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Flow Graph: [0->{2,6},1->{2,6},2->{7,8,10,11,12,14,18},3->{0,1,15},4->{0,1,15},5->{1},6->{7,8,9,11,12,13,18},7->{3,16} ,8->{3,16},9->{3,16},10->{3,16},11->{4,17},12->{4,17},13->{4,17},14->{4,17},15->{},16->{},17->{},18->{}] + 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) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= A] f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A >= 2] f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B = 0] f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [-1 + D + -1*F >= 0 && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 255 >= C] f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [-1 + -1*D + F >= 0 && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 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) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1] f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= E && D >= 1 + F] f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 2 && D >= 1 + F] f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && B >= 1 && D >= 1 + F && E = 1] f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D >= 1 + F && B = 0 && E = 1] f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 1 >= E && F >= 1 + D] f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && E >= 3 && F >= 1 + D] f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 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) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && F >= 1 + D && B = 0 && E = 2] f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && A = 1] f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [-1 + D + -1*F >= 0 && 2 + -1*E >= 0 && 2 + B + -1*E >= 0 && 6 + -1*A + -1*E >= 0 && -2 + E >= 0 && -2 + B + E >= 0 && 2 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && C >= 256] f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [-1 + -1*D + F >= 0 && 1 + -1*E >= 0 && 1 + B + -1*E >= 0 && 5 + -1*A + -1*E >= 0 && -1 + E >= 0 && -1 + B + E >= 0 && 3 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && 0 >= 1 + C] f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [E >= 0 && B + E >= 0 && 4 + -1*A + E >= 0 && 4 + -1*A + -1*B >= 0 && B >= 0 && 4 + -1*A + B >= 0 && 4 + -1*A >= 0 && D = F] Signature: {(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Rule Graph: [0->{2,6},1->{2,6},2->{7,8,10,11,12,14,18},3->{0,1,15},4->{0,1,15},5->{1},6->{7,8,9,11,12,13,18},7->{3,16} ,8->{3,16},9->{3,16},10->{3,16},11->{4,17},12->{4,17},13->{4,17},14->{4,17},15->{},16->{},17->{},18->{}] + Applied Processor: CloseWith False + Details: () NO