Comment by __atx__

I checked and the solution is unique (at least within some reasonable bounds in terms of runtime etc, it's possible there is a 1000 bits long special solution hidden somewhere, but due to the relatively small amount of flops I doubt it).