tff(student_type,type,student: $tType).

tff(teacher_type,type,teacher: $tType).

tff(joe_decl,type,joe: student).

tff(geoff_decl,type,geoff: teacher).

tff(teacher_of_decl,type,teacher_of: student > teacher).

tff(failed_decl,type,failed: student > $o).

tff(stupid_decl,type,stupid: student > $o).

%----Geoff is the __only__ teacher of Joe.
tff(geoff_teaches_joe,axiom,
    teacher_of(joe) = geoff ).

%----Joe is not stupid but Joe failed.
tff(joe_failed,axiom,
    ( ~ stupid(joe)
    & failed(joe) ) ).

%----If a student failed then either the student is stupid or there is
%----is some other student with the same teacher who also failed.
tff(someone_stupid,axiom,
    ! [S: student] : 
      ( failed(S) 
     => ( stupid(S)
        | ? [C: student] :
            ( C != S
            & teacher_of(S) = teacher_of(C)
            & failed(C) ) ) ) ).

%----Therefore there is some student other then Joe and also taught by Geoff,
%----who failed.
tff(some_other_student_failed,conjecture,
    ? [S: student] :
      ( S != joe
      & teacher_of(S) = geoff
      & failed(S) ) ).