Proof obligations (POs) arise when applying formal methods (FMs). The undischarged POs can become a bottleneck
in the use of FMs in industry. The work we proposed here, as a part of AI4FM project, aims at increasing the proportion
of discharged POs by analysing failed proofs and related patches to classify POs as families and construct proof strategies,
which can be used to guide proof search for the POs in the same families.