The Irredundant form item (menu Presentation) finds an irredundant expression by deleting terms in such a way that this does not change the function. It is based on satisfiability (or refutability) algorithm of Davies and Putnam.