# No proof found in 31 steps (3100000 steps/sec) using 1 engine (84 triples)