Fixed bugs, now properly implemented

Around 10x slower and 100x as much memory as the old version with naive
clause handling.  Profiling to find the cause