The same argument can probably 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 ru~~le~~s~~. ~~W~~e difference comes from the

+Inversion by itself is sufficient to find the proof in the last example. The 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 lazy splitting group - Figure 4.}

-The full focusing prover always beats its less deterministic version, the weak focusing prover, as we expected,

-there is nothing to deep analysis.

+An we expected, the full focusing prover always beats its less deterministic version, the weak focusing prover.

+No deep thinking is required here.

-More interesting are differences to naive prover, which we suppose to be much wors~~t~~ than other provers.

+More interesting are differences to naive prover, which we suppose to be much worse than other provers.

As mentioned in previous sections the tests Tensor with zeros and With with zeros are hard for our

algorithms with lazy splitting due to non-deterministic choices.

However, this disadvantage of basic lazy splitting does not explain why the Naive prover is almost twice

better than the FullLS prover at the test Tensor commutativity. It shows defect of our implementation.

-The FullLS (and the WeakLS) prover tries to make possible inversions after each recursive call, but

-context is fully decomposed into atoms at beginning. It means that after each step whole context would be

-analyzed for possible inversions. We can solve this problem by splitting input resources into two sets,

-one for already inverted hypotheses and second for not.

+The FullLS (and the WeakLS) prover tries to make all possible inversions after each recursive call, but here

+the context is fully decomposed into atoms at the beginning. It means that after each step whole context would be

+analyzed for possible inversions. We could solve this problem by splitting input resources into two sets,

+one for already inverted hypotheses and another for the remaiming ones.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%