Menu options: a: Add a pre- or user-defined axiom to the logic. b: Specify a formula to fail in the matrices found. c: Define a connective. E.g. + defined ~a -> b. d: Delete either an axiom or the chosen bad guy. e: Exit from MAGIC. f: Choose fragment (pre-defined connectives). g: Search for matrices. h: Display this page. i: Change the output formats. j: Set a condition on which to jump out of the search. k: Re-initialise everything. l: Change your mind about your favourite logic.