Separation logic + superposition calculus = heap theorem prover