There are four levels of proof available.
(1) The definite level. 

This level only uses rules with > in them.
To prove x at this level, type
+d x
(2) The plausible with ambiguity propagation (likely) level. 

This level uses all the rules and the priority (> )
information. To prove x at this level type
+l x
(3) The plausible level without ambiguity propagation. 

This level uses all the rules and the priority (> )
information. To prove x at this level type
+p x
(4) The supported level. 

This level uses all the rules and the priority (> )
information. To prove x at this level type
+s x
This system can also prove that formulas cannot be proved.
To prove that +d x cannot be proved, type
d x
To prove that +l x cannot be proved, type
l x
To prove that +p x cannot be proved, type
p x
To prove that +s x cannot be proved, type
s x
The positive (+ ) and negative ( ) kinds of
proof are related as follows.
Let a be one of d , l ,
p , s .
If +a x then not a x .
If a x then not +a x .
The levels of proof are related as follows.
If +d x then +l x .
If +l x then +p x .
If +p x then +s x .
If s x then p x .
If d x then l x .
If l x then d x .
