CS157 Contest: Category 5 -- Group Theory

The problems in this category are drawn from Group Theory. You are given the axioms shown below, and you may assume whatever equality axioms you deem appropriate. We will provide no additional premises. The conclusion in each case is a conjecture about Group Theory (which may, in some cases, be false).

Your solution will contain the following:

Background Axioms 

   (= (* (* ?x ?y) ?z) (* ?x (* ?y ?z)))
   (= (* ?x e) ?x)
   (= (* ?x (inv ?x)) e)

Sample Premises 

There will be no sample premises

Sample Conclusion 

   (= (* (inv a) a) e)