(Contributed by William McCune and Ewing Lusk)
We were able to port our parallel distributed-memory theorem prover dac (distributed associative-commutative theorem prover) to the SP1 with no problems. We initially developed dac on the Symmetry and a Sun network using p4, so once p4 itself was ported to the SP1, we needed only to recompile and link the program. Single-node performance was excellent, despite the lack of floating-point operations in dac.