metit foo.tptp
metit -m foo.tptp
metit --smt foo.tptp
metit --strategy 1 foo.tptp
metit -p --strategy 1 tan-1-1var-weak.tptp > tan-1-1var-weak.proof
yields the following MetiTarski proof of the problem tan-1-1var-weak.tptp: tan-1-1var-weak.proof.
This process produces a log file with a name of the form STATUS-Metit-‹DATE›-‹TIME_LIMIT›--‹OPTIONS›.log.
For instance, if run on 28-Feb-2012, the above command would generate a log file named STATUS-Metit-2012-02-28-120--strategy_1.log.
The script metis-rcf/scripts/compare-logfiles.pl can be used to compare multiple log files, reporting, for each considered theorem, which log file contains the fastest proof of the theorem by at least some specified margin. This is how the bar graphs in Fig. 2 were created.