formulas(assumptions).  
 L1 | L2 | L3 |L4 | L5 | L6 |L7 |L8 |L9.  %at least one lady
 %T1 | T2 | T3 |T4 | T5 | T6 |T7 |T8 |T9.  %at least one tiger
 %E1 | E2 | E3 |E4 | E5 | E6 |E7 |E8 |E9.  %at least one empty

 %at most one lady
 L1 -> -(L2 | L3 | L4 | L5 | L6 | L7 | L8 | L9).
 L2 -> -(L1 | L3 | L4 | L5 | L6 | L7 | L8 | L9).
 L3 -> -(L2 | L1 | L4 | L5 | L6 | L7 | L8 | L9).
 L4 -> -(L2 | L3 | L1 | L5 | L6 | L7 | L8 | L9).
 L5 -> -(L2 | L3 | L4 | L1 | L6 | L7 | L8 | L9).
 L6 -> -(L2 | L3 | L4 | L5 | L1 | L7 | L8 | L9).
 L7 -> -(L2 | L3 | L4 | L5 | L6 | L1 | L8 | L9).
 L8 -> -(L2 | L3 | L4 | L5 | L6 | L7 | L1 | L9).
 L9 -> -(L2 | L3 | L4 | L5 | L6 | L7 | L8 | L1).

 %lady is true
 (L1 -> R1) & (L2 -> R2) & (L3 -> R3) & (L4 -> R4) & (L5 -> R5).
 (L6 -> R6) & (L7 -> R7) & (L8 -> R8) & (L9 -> R9).

 %tiger is false
 (T1 -> -R1) & (T2 -> -R2) & (T3 -> -R3) & (T4 -> -R4) & (T5 -> -R5).
 (T6 -> -R6) & (T7 -> -R7) & (T8 -> -R8) & (T9 -> -R9).

 %lady, tiger or empty 
 (L1 | T1 | E1) & (L2 | T2 | E2) & (L3 | T3 | E3) & (L4 | T4 | E4) &
 (L5 | T5 | E5) & (L6 | T6 | E6) & (L7 | T7 | E7) & (L8 | T8 | E8) & 
 (L9 | T9 | E9).

 %single occupant
 (L1 -> -T1 & -E1) & (L2 -> -T2 & -E2) & (L3 -> -T3 & -E3).
 (L4 -> -T4 & -E4) & (L5 -> -T5 & -E5) & (L6 -> -T6 & -E6).
 (L7 -> -T7 & -E7) & (L8 -> -T8 & -E8) & (L9 -> -T9 & -E9).
  
 (T1 -> -L1 & -E1) & (T2 -> -L2 & -E2) & (T3 -> -L3 & -E3).
 (T4 -> -L4 & -E4) & (T5 -> -L5 & -E5) & (T6 -> -L6 & -E6). 
 (T7 -> -L7 & -E7) & (T8 -> -L8 & -E8) & (T9 -> -L9 & -E9). 
 
 (E1 -> -L1 & -T1) & (E2 -> -L2 & -T2) & (E3 -> -L3 & -T3).
 (E4 -> -L4 & -T4) & (E5 -> -L5 & -T5) & (E6 -> -L6 & -T6). 
 (E7 -> -L7 & -T7) & (E8 -> -L8 & -T8) & (E9 -> -L9 & -T9). 

 R1 <-> (L1 | L3 | L5 | L7 | L9).
 R2 <->  E2.
 R3 <-> (R5 | -R7). 
 R4 <-> -R1.
 R5 <-> (R2 |  R4). 
 R6 <-> -R3.
 R7 <-> -L1.
 R8 <->  T8 &  E9.
 R9 <->  T9 & -R6.
 
-E8. %extra clue
end_of_list.

formulas(goals).
  L7.
end_of_list.
 
