Remove old substitution

[sankalpgambhir]

• removed old substitution
• the only breaking change is SimpleTautology in lisa-examples, we will retcon and fix it later
• removed the old UnificationUtils2
• removed the old FirstOrderUnifier
• we did not use actual unification anywhere, and so we do not have a new implementation of it. Tests for unification have been commented out for now
• removed SecondOrderUnifier as we never used or needed it in the end (we didn't even have the functions implemented :raised_eyebrow: )
• adapted theory files to accommodate changes above