Future directions of automated deduction: Strategy analysis for theorem proving