Introducing SimpSolver
Added model dump command
Working K-induction