Ok but if you read the actual solutions they aren't a bizarre mess of brute force.
They look like what a human would write if they were trying to come up with a formal proof (albeit it does some steps in a weird order).
They look like what a human would write if they were trying to come up with a formal proof (albeit it does some steps in a weird order).