The application profile has major impacts on the problem solving process and requires an open system architecture in which different deductive engines work in combination because the proof problems are too difficult for a single monolithic system. We describe our system architecture, a pipeline of filters of increasing deductive strength, and concentrate on the final filter, in which theorem provers are applied. Here, we use the Ilf -system as a control and integration shell to combine different provers. We support two different combination styles, competition and cooperation.
Experiments confirm our approach.