tmp commit, rewriting stuff
equalities containing functions are added sent to the congruence closure algorithm right away. this cleans up the propositional skeleton computation a lot as well.