Hello; I am writing a parallel theorem prover using Haskell, and I am trying to do several things. As a first cut, I want to try using the par construct to attempt right and left rules simultaneously, and to evaluate both branches of an and clause in parallel. My code (attached) does not seem to generate sparks, however. When I run ./proposition +RTS -N2 -sstderr I get that no sparks are created. What am I doing wrong? Also, I was wondering if something akin to a "parallel or" exists. By this, I mean I am looking for a function which, given x : a , y : a, returns either, whichever computation returns first. Can I use strategies to code up something like this? I suppose this doesn't play nicely with the idea of determinism, but thought it might be worth asking anyway. Thanks, -Jamie