The same argument can propably be used to justify the outcome of the 4th benchmark in both Figures.

-The proof in the last example can be found using just the invertible rules. We don't know

-if there is a deep reason for the difference here.

-%% TODO: check the order in which the rules are applied in Full and FullLS

+The proof in the last example can be found using just the invertible rules. We difference comes from the

+fact that we have implemented an optimized version of the inversion procedure in the FullLS and WeakLS

+provers while we haven't done so in the Full version. Luckily, we can turn this communication mistake into

+an insight into the importance of writing the inversion procedure in an efficient way :-)

\subsubsection{Comparison within the non-deterministic context management group - Figure 3.}

These tools allow one to state a general property, say

- $\m{forall}$ (P Q : $\m{Formula}$), $\m{isProvable}$ ( $ |- P \tensor Q \lolli Q \tensor P) $ == $\m{True}$~~ %% TODO more latex here~~

+ $\m{forall}$ (P Q : $\m{Formula}$), $\m{isProvable}$ ( $ |- P \tensor Q \lolli Q \tensor P) $ == $\m{True}$