My "value" error trace when there's a solution (the /= Goal is violated) is the following State (num = 1) (small :> 0 @@ big :> 0) State (num = 2) (small :> 0 @@ big :> 5) State (num = 3) (small :> 3 @@ big :> 2) State (num = 4) (small :> 0 @@ big :> 2) State (num = 5) (small :> -2 @@ big :> 4) I'm confused as to why "small" is ever negative as it is in state 5 -- any ideas?