263 % |
263 % |
264 Sledgehammer: ``\textit{remote\_waldmeister}'' on goal \\ |
264 Sledgehammer: ``\textit{remote\_waldmeister}'' on goal \\ |
265 $[a] = [b] \,\Longrightarrow\, a = b$ \\ |
265 $[a] = [b] \,\Longrightarrow\, a = b$ \\ |
266 Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount] |
266 Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount] |
267 % |
267 % |
|
268 Sledgehammer: ``\textit{remote\_e\_sine}'' on goal \\ |
|
269 $[a] = [b] \,\Longrightarrow\, a = b$ \\ |
|
270 Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). \\[3\smallskipamount] |
|
271 % |
268 Sledgehammer: ``\textit{remote\_z3}'' on goal \\ |
272 Sledgehammer: ``\textit{remote\_z3}'' on goal \\ |
269 $[a] = [b] \,\Longrightarrow\, a = b$ \\ |
273 $[a] = [b] \,\Longrightarrow\, a = b$ \\ |
270 Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). |
274 Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). |
271 \postw |
275 \postw |
272 |
276 |
273 Sledgehammer ran E, SPASS, Vampire, Waldmeister, and Z3 in parallel. |
277 Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel. |
274 Depending on which provers are installed and how many processor cores are |
278 Depending on which provers are installed and how many processor cores are |
275 available, some of the provers might be missing or present with a |
279 available, some of the provers might be missing or present with a |
276 \textit{remote\_} prefix. Waldmeister is run only for unit equational problems, |
280 \textit{remote\_} prefix. Waldmeister is run only for unit equational problems, |
277 where the goal's conclusion is a (universally quantified) equation. |
281 where the goal's conclusion is a (universally quantified) equation. |
278 |
282 |
812 |
816 |
813 \item[$\bullet$] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3 |
817 \item[$\bullet$] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3 |
814 with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers. |
818 with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers. |
815 \end{enum} |
819 \end{enum} |
816 |
820 |
817 By default, Sledgehammer runs E, SPASS, Vampire, Z3 (or whatever |
821 By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever |
818 the SMT module's \textit{smt\_solver} configuration option is set to), and (if |
822 the SMT module's \textit{smt\_solver} configuration option is set to), and (if |
819 appropriate) Waldmeister in parallel---either locally or remotely, depending on |
823 appropriate) Waldmeister in parallel---either locally or remotely, depending on |
820 the number of processor cores available. For historical reasons, the default |
824 the number of processor cores available. For historical reasons, the default |
821 value of this option can be overridden using the option ``Sledgehammer: |
825 value of this option can be overridden using the option ``Sledgehammer: |
822 Provers'' in Proof General's ``Isabelle'' menu. |
826 Provers'' in Proof General's ``Isabelle'' menu. |