This report is no longer available (in any form) because all of its files were lost due to a botched disk back-up. I could have tried to reconstruct the report from some surviving draft files, but I never bothered because it became soon subsumed by later work of mine on DPLL(T). I would recommend that work instead (In particular, see entry [NOT06] at http://www.cs.uiowa.edu/~tinelli/html/publications.html). -CT