The nondeterminism introduced by parallelism gives rise to the question of how
repeatable the experiments are. It is indeed true that ROO, unlike OTTER,
does not run the same way every time, even with the exact same input file and
the same number of processes. In this section we report on some experiments
to measure, at least on a limited sample of examples, the extent of this
problem. We do this by running the very same problem ten times with the same
number of processes, and comparing the results.