  I argue that the most interesting goal facing researchers in automated
reasoning is being able to solve problems that cannot currently be solved by
existing tools and methods. This may appear obvious, and is clearly not an
original thought, but focusing on this as a primary goal allows us to examine
other goals in a new light. Many successful theorem provers employ a portfolio
of different methods for solving problems. This changes the landscape on which
we perform our research: solving problems that can already be solved may not
improve the state of the art and a method that can solve a handful of problems
unsolvable by current methods, but generally performs poorly on most problems,
can be very useful. We acknowledge that forcing new methods to compete against
portfolio solvers can stifle innovation. However, this is only the case when
comparisons are made at the level of total problems solved. We propose a
movement towards focussing on unique solutions in evaluation and competitions
i.e. measuring the potential contribution to a portfolio solver. This state of
affairs is particularly prominent in first-order logic, which is undecidable.
When reasoning in a decidable logic there can be a focus on optimising a
decision procedure and measuring average solving times. But in a setting where
solutions are difficult to find, average solving times lose meaning, and whilst
improving the efficiency of a technique can move potential solutions within
acceptable time limits, in general, complementary strategies may be more
successful.
