Spracherkennung für: .out vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
Non-discriminated database
Unfoldable variable definitions: none
Unfoldable constant definitions: none
Unfoldable projection definitions: none
Cut: emp
For any goal -> (*external*) (idtac "second"; fail) (cost 1, id 0)
(*external*) (idtac "first"; fail) (cost 1, id 0)
(*external*) (idtac "fourth"; fail) (cost 2, id 0)
(*external*) (idtac "third"; fail) (cost 2, id 0)
(* info auto: *)
second
first
fourth
third
fifth, different hintDb
idtac.
(* info eauto: *)
second
first
fifth, different hintDb
fourth
third
idtac.
second
first
fifth, different hintDb
fourth
third
File "./output/auto_order.v", line 16, characters 5-45:
The command has indeed failed with message:
Tactic failure: Proof search failed.
[Dauer der Verarbeitung: 0.15 Sekunden, vorverarbeitet 2026-06-04]
