Description
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, telephone operator, police officer (either gender), teacher, actor, and boxer.
The job of a nurse is held by a male. The husband of the chef is the telephone operator. Roberta is not a boxer. Pete has no education past the ninth grade. Roberta, the chef and the police officer went golfing together.
Who holds which job?
ProverBox Specification (download file)
CONST OBJ : TYPE
educated : PRED[OBJ]
equal_jobs : PRED[OBJ,OBJ]
equal_people : PRED[OBJ,OBJ]
female : PRED[OBJ]
has_job : PRED[OBJ,OBJ]
husband : PRED[OBJ,OBJ]
male : PRED[OBJ]
actor : OBJ
boxer : OBJ
chef : OBJ
guard : OBJ
nurse : OBJ
operator : OBJ
pete : OBJ
police : OBJ
roberta : OBJ
steve : OBJ
teacher : OBJ
thelma : OBJ
VAR U : OBJ
X : OBJ
Y : OBJ
Z : OBJ
AXIOM reflexivity_for_equal_people: equal_people(X,X)
AXIOM reflexivity_for_equal_jobs: equal_jobs(X,X)
AXIOM symmetry_of_equal_people: not equal_people(X,Y) or equal_people(Y,X)
AXIOM symmetry_of_equal_jobs: not equal_jobs(X,Y) or equal_jobs(Y,X)
AXIOM roberta_not_thelma: not equal_people(roberta,thelma)
AXIOM roberta_not_pete: not equal_people(roberta,pete)
AXIOM roberta_not_steve: not equal_people(roberta,steve)
AXIOM pete_not_thelma: not equal_people(pete,thelma)
AXIOM pete_not_steve: not equal_people(pete,steve)
AXIOM chef_not_guard: not equal_jobs(chef,guard)
AXIOM chef_not_nurse: not equal_jobs(chef,nurse)
AXIOM chef_not_operator: not equal_jobs(chef,operator)
AXIOM chef_not_police: not equal_jobs(chef,police)
AXIOM chef_not_actor: not equal_jobs(chef,actor)
AXIOM chef_not_boxer: not equal_jobs(chef,boxer)
AXIOM chef_not_teacher: not equal_jobs(chef,teacher)
AXIOM guard_not_nurse: not equal_jobs(guard,nurse)
AXIOM guard_not_operator: not equal_jobs(guard,operator)
AXIOM guard_not_police: not equal_jobs(guard,police)
AXIOM guard_not_actor: not equal_jobs(guard,actor)
AXIOM guard_not_boxer: not equal_jobs(guard,boxer)
AXIOM guard_not_teacher: not equal_jobs(guard,teacher)
AXIOM nurse_not_operator: not equal_jobs(nurse,operator)
AXIOM nurse_not_police: not equal_jobs(nurse,police)
AXIOM nurse_not_actor: not equal_jobs(nurse,actor)
AXIOM nurse_not_boxer: not equal_jobs(nurse,boxer)
AXIOM nurse_not_teacher: not equal_jobs(nurse,teacher)
AXIOM operator_not_police: not equal_jobs(operator,police)
AXIOM operator_not_actor: not equal_jobs(operator,actor)
AXIOM operator_not_boxer: not equal_jobs(operator,boxer)
AXIOM operator_not_teacher: not equal_jobs(operator,teacher)
AXIOM police_not_actor: not equal_jobs(police,actor)
AXIOM police_not_boxer: not equal_jobs(police,boxer)
AXIOM police_not_teacher: not equal_jobs(police,teacher)
AXIOM actor_not_boxer: not equal_jobs(actor,boxer)
AXIOM actor_not_teacher: not equal_jobs(actor,teacher)
AXIOM boxer_not_teacher: not equal_jobs(boxer,teacher)
AXIOM nurse_is_male: not has_job(X,nurse) or male(X)
AXIOM actor_is_male: not has_job(X,actor) or male(X)
AXIOM chef_is_female: not has_job(X,chef) or female(X)
AXIOM nurse_is_educated: not has_job(X,nurse) or educated(X)
AXIOM teacher_is_educated: not has_job(X,teacher) or educated(X)
AXIOM police_is_educated: not has_job(X,police) or educated(X)
AXIOM chef_is_not_also_police: not has_job(X,chef)
or not has_job(X,police)
AXIOM males_are_not_female: not male(X) or not female(X)
AXIOM everyone_male_or_female: male(X) or female(X)
AXIOM husband_is_male: not husband(X,Y) or male(Y)
AXIOM wife_is_female: not husband(X,Y) or female(X)
AXIOM husband_of_chef_is_operator1: not has_job(X,chef)
or not has_job(Y,operator) or husband(X,Y)
AXIOM husband_of_chef_is_operator2: not has_job(X,chef)
or has_job(Y,operator) or not husband(X,Y)
AXIOM each_job_held_once: not has_job(X,Z) or not has_job(Y,Z)
or equal_people(X,Y)
AXIOM each_has_maximum_of_two_jobs: not has_job(Z,U) or not has_job(Z,X)
or not has_job(Z,Y) or equal_jobs(U,X) or equal_jobs(U,Y)
or equal_jobs(X,Y)
AXIOM every_job_is_used: has_job(roberta,X) or has_job(thelma,X)
or has_job(pete,X) or has_job(steve,X)
AXIOM everyone_works: has_job(X,chef) or has_job(X,guard)
or has_job(X,nurse) or has_job(X,operator) or has_job(X,police)
or has_job(X,teacher) or has_job(X,actor) or has_job(X,boxer)
AXIOM pete_is_not_educated: not educated(pete)
AXIOM roberta_is_not_chef: not has_job(roberta,chef)
AXIOM roberta_is_not_boxer: not has_job(roberta,boxer)
AXIOM roberta_is_not_police: not has_job(roberta,police)
AXIOM steve_is_male: male(steve)
AXIOM pete_is_male: male(pete)
AXIOM roberta_is_female: female(roberta)
AXIOM thelma_is_female: female(thelma)
THEOREM find_who_has_each_job: Exists X1:OBJ,X2:OBJ,X3:OBJ,X4:OBJ,X5:OBJ,
X6:OBJ,X7:OBJ,X8:OBJ.
(has_job(X1,chef) and has_job(X2,guard) and has_job(X3,nurse)
and has_job(X4,operator) and has_job(X5,police)
and has_job(X6,teacher) and has_job(X7,actor)
and has_job(X8,boxer))