https://sicstus.sics.se/sicstus/docs/4.3.1/html/sicstus/CLPB...
This of course requires a slightly different way to encode the task, using logical variables:
?- sat(School*Study*Exercise),
sat(Exercise =< Healthy),
sat(Study + Sick),
sat(~Rain),
sat(Study * ( Gym + Coffee)),
sat(Rain + (Exercise * Study)),
sat(Healthy =< (Happy + Fit)).
As an answer, we get: School = Study, Study = Exercise, Exercise = Healthy, Healthy = 1,
Rain = 0,
sat(Sick=:=Sick),
sat(Gym=\=Gym*Coffee#Coffee),
sat(Happy=\=Happy*Fit#Fit).
Since CLP(B) is complete, these are all the consequences that can be derived from the initial knowledge. Note that for example `Gym = 1` is consistent with the initial assumptions, it just doesn't follow from them.To obtain ground solutions, you can use labeling/1 on the remaining free variables, showing all possible ways in which truth values can be assigned to them.