src/HOL/ATP_Linkup.thy
changeset 28594 ed3351ff3f1b
parent 28592 824f8390aaa2
child 29580 117b88da143c
child 29587 96599d8d8268
equal deleted inserted replaced
28593:f087237af65d 28594:ed3351ff3f1b
   107 text {* provers with stuctured output *}
   107 text {* provers with stuctured output *}
   108 setup {* AtpManager.add_prover "vampire_full" AtpWrapper.vampire_full *}
   108 setup {* AtpManager.add_prover "vampire_full" AtpWrapper.vampire_full *}
   109 setup {* AtpManager.add_prover "e_full" AtpWrapper.eprover_full *}
   109 setup {* AtpManager.add_prover "e_full" AtpWrapper.eprover_full *}
   110 
   110 
   111 text {* on some problems better results *}
   111 text {* on some problems better results *}
   112 setup {* AtpManager.add_prover "spass_no_tc" (AtpWrapper.spass_filter_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" "jumpirefix --output_syntax tptp --mode casc -t 3600") *}
   117 setup {* AtpManager.add_prover "remote_vamp10"
   117 setup {* AtpManager.add_prover "remote_vamp10"