Here, I have translated your axioms into DC Proof format. Download my software, enter these axioms (the "@" is mapped to epsilon) and see what you can do with them. You have to construct your own proofs one line at a time, but the software will not let you make mistakes. Instant feedback is provided with each line you enter it. You might start by proving the associativity and commutativity of + and * as you have defined them. You can get started using with the tutorial or user manual.