see

In a group, the inverse of an element is unique.

Insight

The compiled query selected 2 fact(s) after the rule closure was computed.
Main conclusion: :result :sameInverse (:x :j :i).

Selected conclusions:

• :result :sameInverse (:x :j :i) .
• :result :sameInverse (:x :i :j) .

Explanation

The generated JavaScript starts from 6 compiled source fact(s), applies 6 compiled rule(s), and stops only after a fixpoint is reached.
After saturation, the compiled log:query directive projects only the matching facts shown in the insight, rather than dumping the whole graph.

A compact derivation path is:

• Rule 3: if ?a :inG true, then (:e ?a) :mul ?a. This produced (:e :x) :mul :x .
  • Premises used:
    • :x :inG true . (source fact)
• Rule 3: if ?a :inG true, then (:e ?a) :mul ?a. This produced (:e :i) :mul :i .
  • Premises used:
    • :i :inG true . (source fact)
• Rule 3: if ?a :inG true, then (:e ?a) :mul ?a. This produced (:e :j) :mul :j .
  • Premises used:
    • :j :inG true . (source fact)
• Rule 3: if ?a :inG true, then (:e ?a) :mul ?a. This produced (:e :e) :mul :e .
  • Premises used:
    • :e :inG true . (source fact)
• Rule 4: if ?a :inG true, then (?a :e) :mul ?a. This produced (:x :e) :mul :x .
  • Premises used:
    • :x :inG true . (source fact)
• Rule 4: if ?a :inG true, then (?a :e) :mul ?a. This produced (:i :e) :mul :i .
  • Premises used:
    • :i :inG true . (source fact)
• Rule 4: if ?a :inG true, then (?a :e) :mul ?a. This produced (:j :e) :mul :j .
  • Premises used:
    • :j :inG true . (source fact)
• Rule 5: if ?x :inG true; ?y :inG true; ?y :inverseOf ?x, then (?x ?y) :mul :e; (?y ?x) :mul :e. This produced (:x :i) :mul :e ., (:i :x) :mul :e .
  • Premises used:
    • :x :inG true . (source fact)
    • :i :inG true . (source fact)
    • :i :inverseOf :x . (source fact)

Evidence

These are the facts selected by the query projection.

:result :sameInverse (:x :i :j) .  
:result :sameInverse (:x :j :i) .