It works will prove stuff given the axioms in axioms.lisp