Logicians' Balladvanced series

The “advanced” problems are not necessarily harder than the “intermediate” ones, but they have been chosen to require slightly more elaborate coding.

This problem requires six constraints each with three literals. The most natural encodings make use of all the binary connectives AND, OR and IMP, or the corresponding logical symbols ∧, ∨ and → . The negation operator NOT (written as ¬ if you like) is also useful.

Logicians, it appears, are liberated but love to do things in traditional style. Five girls escorted five boys to the Logicians’ Ball last year, and:

If Brenda didn’t take Harry, Ian was with either Alice or Emma.
If Emma escorted Ken, then Harry was taken by either Claire or Daphne.
If Claire took neither Gary nor James, Brenda escorted Ken.
If Gary wasn’t with Alice, Brenda took either Ian or Ken.
If Emma didn’t escort James then, if Brenda and Gary weren’t together, Daphne took Ian.
If Claire’s partner was Harry then, if Daphne’s wasn’t James, Alice escorted Ken.

Naturally, they all had a wonderful time. Who with whom?

Notes:

When we say “neither X nor Y” this is the same as saying “not X and not Y”.
Formulae of the form “If X, Y” are written “X → Y”.
Formulae of the form “If X then if Y, Z” can be written “X → (Y → Z)”, or they can be treated as saying the same as “If X and Y, then Z”.
“NOT” can only apply to boolean expressions. So for instance, “NOT (Emma with James)” makes sense, but “NOT (Emma) with James” is a syntax error because Emma is a girl, not a boolean truth value!

Solver

Sorts:

Vocabulary:

Constraints:

Please log in or create an account to use the solver.

Save Title:

Saved Solutions
Name	Time saved
Class Submissions
Name	Time submitted

Number of solutions:

Time limit:

Pretest limit:

Print finder job:

Print solutions:

Print statistics:

Auto Parser Results

No errors found.