Direct finite first-order model generation with negative constraint propagation heuristic. - Olga Shumsky; Ralph W. Wilkerson; William McCune; Fikret Erçal (SAC, 1997)

System Description: IVY. - William McCune; Olga Shumsky (CADE, 2000)