Please choose one of the examples below, or enter your own sequent
according to the syntax on the left. Then click "Prove!". If you
want to see what the prover did then turn on the trace option by
pressing the Trace On/Off button. This will print out the rules
applied by the prover and will allow you to extract a
proof/counter-model if the sequent is provable/unprovable.