straylight straylight is a (WIP) Lambda-superposition automated theorem prover. elaboration unification derived KBO main loop clausify THF parser system description dependent types unification?