Using hundreds of workstations to solve first-order logic problems

This paper describes a distributed, adaptive, first-order logic engine with exceptional performance characteristics. The system combines serial search reduction techniques such as bounded-overhead subgoal caching and intelligent backtracking with a novel parallelization strategy particularly well-suited to coarse-grained parallel execution on a network of workstations. We present empirical results that demonstrate our system's performance using 100 workstations on over 1400 first-order logic problems drawn from the "Thousands of Problems for Theorem Provers" collection.