%=============================================================
%
% THE "FULL" JOBS PUZZLE -- CLAUSAL FORM
% version by Selmer Bringsjord
%
%     Intro to Logic Programming & AI
%     Spring 1998
%
% There are four people:  Roberta, Thelma, Steve, and Pete.
% Among them, they hold eight different jobs.  Each holds
% exactly two jobs.  The jobs are chef, guard, nurse, clerk,
% police officer (gender open), teacher, actor, and boxer.
% The husband of te chef is the clerk.  Roberta is not a boxer.
% Pete has no education poast the ninth grade.  Roberta, the
% chef, and the police officer went golfing together.
%
%=============================================================


set(ur_res).
set(back_demod).
set(dynamic_demod_all).
assign(max_proofs,1).

weight_list(pick_and_purge).
weight(roberta,1).
weight(thelma,2).
weight(steve,3).
weight(pete,4).
end_of_list.

list(usable).

Female(x) | Male(x).
-Female(x) | -Male(x).

-HasJob(x,nurse) | Male(x).
-HasJob(x,actor) | Male(x).
HasJob(x,job1(x)).
HasJob(x,job2(x)).

HasJob(jobholder(y),y).

-Husband(x,jobholder(chef)) | HasJob(x,clerk).
-HasJob(x,clerk) | Husband(x,jobholder(chef)).

Female(jobholder(chef)).

-Husband(x,y) | Male(x).
-Husband(x,y) | Female(y).

-HasJob(x,nurse) | GreaterThan(ed-level(x),9).
-HasJob(x,policeofficer) | GreaterThan(ed-level(x),9).
-HasJob(x,teacher) | GreaterThan(ed-level(x),9).

-HasJob(x,chef) | -HasJob(x,policeofficer).

-Equalp(roberta,thelma).
-Equalp(roberta,steve).
-Equalp(roberta,pete).
-Equalp(thelma,steve).
-Equalp(thelma,pete).
-Equalp(pete,steve).

-Equalj(job1(x),job2(x)).

Equalp(x,x).
Equalj(x,x).
Equal(x,x).

Equalj(y,job2(x)) | Equalj(y,job1(x)).

Equalp(x,x) | -HasJob(x,y) | -HasJob(z,y).

-Female(jobholder(y)) | HasJob(roberta,y) | HasJob(thelma,y).

-Male(jobholder(y)) | HasJob(steve,y) | HasJob(pete,y).


%=============================================================
%
% INFO FOR TABLE SIMULATION
%
PossJobs(l(pj(roberta,chef),l(pj(roberta,guard),l(pj(roberta,nurse),
l(pj(roberta,clerk),l(pj(roberta,policeofficer),l(pj(roberta,teacher),
l(pj(roberta,actor),l(pj(roberta,boxer),end))))))))).

PossJobs(l(pj(thelma,chef),l(pj(thelma,guard),l(pj(thelma,nurse),
l(pj(thelma,clerk),l(pj(thelma,policeofficer),l(pj(thelma,teacher),
l(pj(thelma,actor),l(pj(thelma,boxer),end))))))))).

PossJobs(l(pj(steve,chef),l(pj(steve,guard),l(pj(steve,nurse),
l(pj(steve,clerk),l(pj(steve,policeofficer),l(pj(steve,teacher),
l(pj(steve,actor),l(pj(steve,boxer),end))))))))).

PossJobs(l(pj(pete,chef),l(pj(pete,guard),l(pj(pete,nurse),
l(pj(pete,clerk),l(pj(pete,policeofficer),l(pj(pete,teacher),
l(pj(pete,actor),l(pj(pete,boxer),end))))))))).

PossPeople(l(pj(roberta,chef),l(pj(steve,chef),l(pj(thelma,chef),
l(pj(pete,chef),end))))).

PossPeople(l(pj(roberta,guard),l(pj(steve,guard),l(pj(thelma,guard),
l(pj(pete,guard),end))))).

PossPeople(l(pj(roberta,nurse),l(pj(steve,nurse),l(pj(thelma,nurse),
l(pj(pete,nurse),end))))).

PossPeople(l(pj(roberta,clerk),l(pj(steve,clerk),l(pj(thelma,clerk),
l(pj(pete,clerk),end))))).

PossPeople(l(pj(roberta,policeofficer),l(pj(steve,policeofficer),
l(pj(thelma,policeofficer),l(pj(pete,policeofficer),end))))).

PossPeople(l(pj(roberta,teacher),l(pj(steve,teacher),l(pj(thelma,teacher),
l(pj(pete,teacher),end))))).

PossPeople(l(pj(roberta,actor),l(pj(steve,actor),l(pj(thelma,actor),
l(pj(pete,actor),end))))).

PossPeople(l(pj(roberta,boxer),l(pj(steve,boxer),l(pj(thelma,boxer),
l(pj(pete,boxer),end))))).

HasJob(x,y) | Equal(pj(x,y),crossed).

Equal(l(crossed,x),x).

-PossJobs(l(pj(x,y),l(pj(x,z),end))) | Equalp(x,w) |
Equal(pj(w,y),crossed).

-PossJobs(l(pj(x,y),l(pj(x,z),end))) | HasJob(x,y).

-PossJobs(l(pj(x,y),l(pj(x,z),end))) | HasJob(x,z).

-PossPeople(l(pj(x,y),end)) | HasJob(x,y).

StillDo(l(jobsof(roberta),l(jobsof(steve),l(jobsof(thelma),
l(jobsof(pete),end))))).

-PossJobs(l(pj(x,y),l(pj(x,z),end))) | Equal(jobsof(x),crossed).

-StillDo(end).

-HasJob(x,y) | Equal(pj(x,y),j(x,y)).

Equal(l(pj(x,y),l(j(x,z),w)),l(j(x,z),l(pj(x,y),w))).

Equal(l(j(x,y),l(j(x,z),l(v,w))),l(j(x,y),l(j(x,z),end))).

-PossJobs(l(j(x,y),l(j(x,z),end))) | Equal(jobsof(x),crossed).

-PossJobs(l(j(x,y),l(pj(x,z),end))) | HasJob(x,z).

end_of_list.

list(sos).
Female(roberta).
Female(thelma).
Male(steve).
Male(pete).
-HasJob(roberta,boxer).
-GreaterThan(ed-level(pete),9).
-HasJob(roberta,chef).
-HasJob(roberta,policeofficer).
end_of_list.

list(demodulators).
Equal(l(crossed,x),x).
end_of_list.