En esta práctica se repetirá la práctica 2-2002, resolviendo con Otter el problema concreto que allí se plantea.

Además también se resolverá con Otter este problema:

María y José tienen, entre los dos, dos trabajos. Cada uno tiene un trabajo. Los trabajos son profesor y abogado.
El trabajo de abogado lo tiene un varón. ¿Qué trabajo tiene cada uno?
 

El lenguaje FOL que se utiliza tendrá un predicado binario tienetrabajo(x, y), "x tiene el trabajo y", y los predicados unarios varón, hembra. La prueba se hara por refutación.