Convert many examples to java backend

**do not review yet**
The unification procedure should be able to detect two problems all by itself, without any smt involvement:
1) equalities of the form X = T[X]; and
2) equalities of the form f(...) = g(...), with f different from g
In both cases it should fail, smoothly.  If that is not the case, then we have a problem with our unification procedure.

I think @andreistefanescu should also say something about this.