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))