Fix solvers

[Jengamon]

Fix the solvers to formally use modus ponens/tollens to solve the program rather than our best guess

Given:
$P \implies Q$
Tollens:
$\neg Q \therefore \neg P$
Ponens:
$P \therefore Q$

where $Q = D_1 \vee D_2 \vee D_3 \vee \dots$