%------------------------------------------------------------------------------
include('S5=S1-0M6S3M9B.sys').
include('PCAxiomDefns.ax').
include('ModalAxiomDefns.ax',[axiom_K,axiom_M,axiom_5]).
include('ModalRuleDefns.ax',[necessitation]).
%------------------------------------------------------------------------------
%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(modus_ponens,conjecture,modus_ponens).

%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(modus_tollens,conjecture,modus_tollens).

%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(implies_1,conjecture,implies_1).

%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(implies_2,conjecture,implies_2).

%----E---0.82dev070 says Theorem - CPU = 5.0 on Walkabout
fof(and_1,conjecture,and_1).

%----E---0.82dev070 says Theorem - CPU = 6.0 on Walkabout
fof(and_2,conjecture,and_2).

%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(and_3,conjecture,and_3).

%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(or_1,conjecture,or_1).

%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(or_2,conjecture,or_2).

%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(or_3,conjecture,or_3).

%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(equivalence_1,conjecture,equivalence_1).

%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(equivalence_2,conjecture,equivalence_2).

%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(equivalence_3,conjecture,equivalence_3).

%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(not_is_idempotent,conjecture,not_is_idempotent).

%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(axiom_K,conjecture,axiom_K).

%----E---0.82dev070 says Theorem - CPU = 6.0 on Walkabout
fof(axiom_M,conjecture,axiom_M).

%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(axiom_5,conjecture,axiom_5).

%----E---0.82dev070 says Timeout - CPU = 600.0 on Walkabout
fof(necessitation,conjecture,necessitation).

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