This paper presents an improvement of A-SATCHMORE (SATCHMORE withAvailability) . A-SATCHMORE incorporates relevancy testing and availability checking into SATCHMOto prune away irrelevant forward chaining. However, considering every consequent atom of thosenon-Horn clauses being derivable, A-SATCHMORE may suffer from a potential explosion of thesearch space when some of such consequent atoms are actually underivable. This paper introducesa solution for this problem and shows its correctness.