I'm a "hard core PLer" and I am skeptical. I don't like automated solvers where there is no way to manually include a proof (to be checked).