src/HOL/ATP_Linkup.thy
changeset 29587 96599d8d8268
parent 28594 ed3351ff3f1b
child 29588 6cccea7c94d4
equal deleted inserted replaced
29452:b81ae415873d 29587:96599d8d8268
   111 text {* on some problems better results *}
   111 text {* on some problems better results *}
   112 setup {* AtpManager.add_prover "spass_no_tc" (AtpWrapper.spass_opts 40 false) *}
   112 setup {* AtpManager.add_prover "spass_no_tc" (AtpWrapper.spass_opts 40 false) *}
   113 
   113 
   114 text {* remote provers via SystemOnTPTP *}
   114 text {* remote provers via SystemOnTPTP *}
   115 setup {* AtpManager.add_prover "remote_vamp9"
   115 setup {* AtpManager.add_prover "remote_vamp9"
   116   (AtpWrapper.remote_prover "Vampire---9.0" "jumpirefix --output_syntax tptp --mode casc -t 3600") *}
   116   (AtpWrapper.remote_prover "Vampire---9.0" 90) *}
   117 setup {* AtpManager.add_prover "remote_vamp10"
   117 setup {* AtpManager.add_prover "remote_spass"
   118   (AtpWrapper.remote_prover "Vampire---10.0" "drakosha.pl 60") *}
   118   (AtpWrapper.remote_prover "SPASS---3.01" 90) *}
       
   119 setup {* AtpManager.add_prover "remote_metis"
       
   120   (AtpWrapper.remote_prover "Metis---2.1" 90) *}
       
   121 setup {* AtpManager.add_prover "remote_snark"
       
   122   (AtpWrapper.remote_prover "SNARK---20080805r005" 90) *}
       
   123 setup {* AtpManager.add_prover "remote_otter"
       
   124   (AtpWrapper.remote_prover "Otter---3.3" 90) *}
       
   125 setup {* AtpManager.add_prover "remote_e"
       
   126   (AtpWrapper.remote_prover "EP---1.0" 90) *}
       
   127 setup {* AtpManager.add_prover "remote_sos"
       
   128   (AtpWrapper.remote_prover "SOS---2.0" 90) *}
       
   129   
   119 
   130 
   120 
   131 
   121 subsection {* The Metis prover *}
   132 subsection {* The Metis prover *}
   122 
   133 
   123 use "Tools/metis_tools.ML"
   134 use "Tools/metis_tools.ML"