  Earlier work on machine learning for automated reasoning mostly relied on
simple, syntactic features combined with sophisticated learning techniques.
Using ideas adopted in the software verification community, we propose the
investigation of more complex, structural features to learn from. These may be
exploited to either learn beneficial strategies for tools, or build a portfolio
solver that chooses the most suitable tool for a given problem. We present some
ideas for features of term rewrite systems and theorem proving problems.
