Building complex derived inference rules: a decider for the class of prenex universal-existential formulas