Congruence closure state.
This may be considered to be a set of expressions and an equivalence class over this set.
The equivalence class is generated by the equational rules that are added to the cc_state and congruence,
that is, if
a = b then
f(a) = f(b) and so on.
"Modification Time". The field m_mt is used to implement the mod-time optimization introduce by the Simplify theorem prover. The basic idea is to introduce a counter gmt that records the number of heuristic instantiation that have occurred in the current branch. It is incremented after each round of heuristic instantiation. The field m_mt records the last time any proper descendant of of thie entry was involved in a merge.