Order of branches: sort all branches with short premises first but then from longest premise. Sort branches in numerical abduction from shortest premise to longest.
Small fixes.