title: I want to prove some theorem using Prolog, however, it always returns "Out of global stack"
body: <p>I'm doing AI homework of proving the group theory in algebra.</p>
  
  <p>The theorem can be represented as follows:</p>
  
  <pre><code>A1. i(e,X) = X                   (identity)
  A2. i(X, e) = X                  (identity)
  A3. i(comp(X),X) = e             (complement)
  A4. i(X, comp(X)) = e            (complement)
  A5. i(X, i(Y,Z)) = i(i(X,Y),Z)   (associativity)
  
  THEOREM: If G is a group such that for every X,
  A6. i(X,X) = e,
  then G is commutative, i.e., for every X; Y ,
  i(X,Y) = i(Y,X):
  
  and the commutative part can be represented as 
  A7. i(a, b, c)                          clause derived from negated conclusion
  A8. -i(b, a, c)                         clause derived from negated conclusion
  </code></pre>
  
  <p>And I converted them into Prolog format as follows:</p>
  
  <pre><code>% A7
  i(a, b, c).
  % A1
  i(e, X, X) .
  %A2
  i(X, e, X).
  % A3
  i(comp(X), X, e).
  % A4
  i(X, comp(X), e).
  % A51
  i(U, Z, W) :- i(X, Y, U), i(Y, Z, V), i(X, V, W).
  % A52
  i(X, V, W) :- i(X, Y, U), i(Y, Z, V), i(U, Z, W).
  % A6
  i(X, X, e).
  </code></pre>
  
  <p>Then I wanted to prove the theorem, so i typed "i(b,a,c)" in Prolog console, and I got following error message:</p>
  
  <pre><code>?- i(b,a,c).
  ERROR: Out of global-stack.
  ERROR: No room for exception term.  Aborting.
  ERROR: Out of global-stack.
  ERROR: No room for exception term.  Aborting.
  ERROR: Out of global-stack.
  ERROR: No room for exception term.  Aborting.
  % Execution Aborted
  </code></pre>
  
  <p>Please help me, thank you very much! </p>