The team work method is a concept for distributing automated theorem provers by activating several experts to work on a problem. We have implemented this for pure equational logic using the unfailing Knuth-Bendix completion procedure as basic prover. In this paper we present three classes of experts working in a goal oriented fashion. In general, goal oriented experts perform their job ``unfair'' and so are often unable to solve a given problem alone. However, as team members in the team work method they perform highly efficiently, as we demonstrate by examples, some of which can only be proved using team work.
Generated: 29/10/99