4 colors suffice

4 color can be difficult to solve, here’s a solution using clingo: