Work log 2016-08-11

Turned cluster and explore results into multipl-output derivations, along with time calculations. Pushed to see what fails. Turns out, 1 success extra!

THOUGHT:

Proof search looks at all combinations of terms until one is a valid proof. Levin (program) search runs those terms for longer and longer times. Turing-complete proof languages are semi-checkable?