%------------------------------------------------------------------------------
include('S5=KM4B.sys').
include('ModalAxiomDefns.ax',[axiom_5]).
%------------------------------------------------------------------------------
%----E---0.82dev070 says Timeout - CPU = 601.0 on Walkabout
fof(axiom_5,conjecture,
    axiom_5 ).

%------------------------------------------------------------------------------