Saturation-based satisfiability checking without CNF conversion

We ask if conversion to clausal normal form (CNF) is a precondition to do efficient saturation-based propositional theorem proving as is suggested by currently available systems like SATO [4]. Founded on examples from modelling and consistency checking tasks in automotive product data management we argue that in this case CNF conversion is inadequate if not in general impossible while a saturation-style algorithm still seems to be a good choice. We sketch our approach to solve this problem and give experimental results