Sample command line:

  ./matitaprover.opt.static -tptppath /home/tassi/TPTP-v3.1.1/ -timeout 600 GRP014-1.p

  or 

  ./matitaprover.opt.static -timeout 600 /home/tassi/TPTP-v3.1.1/Problems/GRP/GRP014-1.p
  
  Note that -tptppath can be omitted only if the file has been expanded (no
  inclusions need to be performed).

Sample output: 

  ........................................
  40 #ACTIVES: 26 #PASSIVES: 1873 #GOALSET: 1(0)
  ........................................
  80 #ACTIVES: 21 #PASSIVES: 271 #GOALSET: 1(0)
  ........................................
  120 #ACTIVES: 35 #PASSIVES: 533 #GOALSET: 1(0)
  ........................................
  160 #ACTIVES: 16 #PASSIVES: 235 #GOALSET: 1(0)
  ........................................
  200 #ACTIVES: 14 #PASSIVES: 250 #GOALSET: 1(0)
  ...................................
  Found a proof in: 42.528698

  <some proofs details here>

  In case of failure: 
  
  "Tactic error: NO proof found: No more time to spend"

Note: 

  the auxiliary files core_notation.moo and matita.conf.xml are needed by matitaprover and 
  must be in the CWD.