src/HOL/Tools/ATP/atp_systems.ML

       ("% SZS output start Proof", "% SZS output end Proof")],
    known_failures =
      [(Unprovable, "UNPROVABLE"),
       (IncompleteUnprovable, "CANNOT PROVE"),
       (IncompleteUnprovable, "SZS status GaveUp"),
-      (ProofMissing, "predicate_definition_introduction,[]"),
+      (ProofIncomplete, "predicate_definition_introduction,[]"),
       (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),
       (VampireTooOld, "not a valid option"),
       (Interrupted, "Aborted by signal SIGINT")],