Automated Reasoning for Mizar

Mizar article (example article)
Local article file to upload
URL to fetch article from
Optional vocabulary file to upload (its name will be kept)
Article name (must not be in the current MML):


Generate ATP problems
Allow ATP calls for hard problems
Call ATP onload on all Mizar-unsolved (only first 10 are attempted)
Do not call ATP onload on Mizar-unsolved
Mizar-unsolved positions (10 at most) to call ATP onload (list of line:column numbers like: 23:7,456:3,789:22)
HTML mode
TEXT mode