

![0_image_0.png](0_image_0.png)

and the type of the functor RelIncl that is used in proposition A4 (renamed to e7 9 mtest1 by MPTP)). The ATP proof can be visualized in the IDV system by clicking on the palm tree icon in the explanation box.

The second reason for the first use-case is cross-verification. In cases when a bug in the Mizar implementation is suspected, or incompleteness in the ATP translation is suspected, the user may be interested in knowing if the Mizar proof can be done by another system (and how). In this sense the environment is used for gathering additional information and debugging. The cross-verification rates for Mizar justifications are reasonably high [33], which makes this usage realistic.

The second use-case (finding proofs that are too hard for Mizar) is the real
"ATP proof assistance" dream, i.e., using ATP systems to automatically find proofs for ITPs. Users can do this within MizAR by providing a large set of "potentially relevant" Mizar propositions on the right-hand side of the by keyword, and letting the EP system try to find a proof. Note that if EP does not find the problem to be countersatisfiable, the user also has the option to try the SPASS