Remove `lia_generic`

This rule is a legacy macro rule. It is hard to reconstruct and essentially needs an integer solver to be reconstructed.

In veriT this rule is generated by LA_xx_conflict_proof_z in src/arith/LA-xx.c.tpl which is only called if LA_solve_z returns the status UNSAT. LA_solve_z is a simple search for integer solutions with bounds.

Instead of having one lia_generic step for all of this we should have multiple la_generic steps for the bounds and then resolutions for the final clause which is currently produced by lia_generic.

We should also check how this is handled in CVC4.