# In a group, the inverse of an element is unique.
@prefix : <https://eyereasoner.github.io/eye/reasoning#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.

{ (?a ?b) :mul ?ab. (?ab ?c) :mul ?left. (?b ?c) :mul ?bc. (?a ?bc) :mul ?right. } => { (?left ?right) :sameTerm true. }.
{ (?a ?b) :sameTerm true. } => { (?b ?a) :sameTerm true. }.
{ ?a :inG true. } => { (:e ?a) :mul ?a. }.
{ ?a :inG true. } => { (?a :e) :mul ?a. }.
{ ?x :inG true. ?y :inG true. ?y :inverseOf ?x. } => { (?x ?y) :mul :e. (?y ?x) :mul :e. }.
{ ?y :inverseOf ?x. ?z :inverseOf ?x. (?y ?z) :sameTerm true. } => { (?x ?y ?z) :sameInverse true. }.

:x :inG true.
:i :inG true.
:j :inG true.
:e :inG true.
:i :inverseOf :x.
:j :inverseOf :x.

{ (?x ?y ?z) :sameInverse true. ?y log:notEqualTo ?z. } log:query { :result :sameInverse (?x ?y ?z). }.