Automated proofs in Lukasiewicz logic