Ptest filters before finding the common prefix and ungrounded terms can no longer be proved.
Adding tests and fixing a parsing bug.