178 "The prover derived \"False\"" ^ from_lemmas ss ^ |
172 "The prover derived \"False\"" ^ from_lemmas ss ^ |
179 "; specify a sound type encoding or omit the \"type_enc\" option" |
173 "; specify a sound type encoding or omit the \"type_enc\" option" |
180 | string_of_atp_failure (UnsoundProof (true, ss)) = |
174 | string_of_atp_failure (UnsoundProof (true, ss)) = |
181 "The prover derived \"False\"" ^ from_lemmas ss ^ |
175 "The prover derived \"False\"" ^ from_lemmas ss ^ |
182 ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)" |
176 ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)" |
183 | string_of_atp_failure CantConnect = "Cannot connect to server" |
|
184 | string_of_atp_failure TimedOut = "Timed out" |
177 | string_of_atp_failure TimedOut = "Timed out" |
185 | string_of_atp_failure Inappropriate = |
178 | string_of_atp_failure Inappropriate = |
186 "The generated problem lies outside the prover's scope" |
179 "The generated problem lies outside the prover's scope" |
187 | string_of_atp_failure OutOfResources = "The prover ran out of resources" |
180 | string_of_atp_failure OutOfResources = "The prover ran out of resources" |
188 | string_of_atp_failure NoPerl = "Perl" ^ missing_message_tail |
|
189 | string_of_atp_failure NoLibwwwPerl = |
|
190 "The Perl module \"libwww-perl\"" ^ missing_message_tail |
|
191 | string_of_atp_failure MalformedInput = "The generated problem is malformed" |
181 | string_of_atp_failure MalformedInput = "The generated problem is malformed" |
192 | string_of_atp_failure MalformedOutput = "The prover output is malformed" |
182 | string_of_atp_failure MalformedOutput = "The prover output is malformed" |
193 | string_of_atp_failure Interrupted = "The prover was interrupted" |
183 | string_of_atp_failure Interrupted = "The prover was interrupted" |
194 | string_of_atp_failure Crashed = "The prover crashed" |
184 | string_of_atp_failure Crashed = "The prover crashed" |
195 | string_of_atp_failure InternalError = "An internal prover error occurred" |
185 | string_of_atp_failure InternalError = "An internal prover error occurred" |