title: Z3 is not able to prove the right-cancellation property in group theory?
body: <p>I am  trying to prove some general properties in group theory.  </p>
  
  <p>For example the left-cancellation property  :  ( x y = x z ) => (y = z) it proved using the following code</p>
  
  <pre><code>(declare-sort S)
  (declare-fun e () S)
  (declare-fun mult (S S) S)
  (declare-fun inv (S) S)
  (assert (forall ((x S) (y S) (z S)) (= (mult (mult x y) z) (mult x (mult y z)))))
  (assert (forall ((x S)) (= (mult e x)  x)))
  (assert (forall ((x S)) (= (mult (inv x) x) e)))
  (assert (forall ((x S)) (= (mult x e)  x)))
  (assert (forall ((x S)) (= (mult x (inv x)) e)))
  (check-sat)
  (assert (not (forall ((x S) (y S) (z S)) (=&gt; (= (mult x y) (mult x z)) (= y z)))))
  (check-sat)
  </code></pre>
  
  <p>and the corresponding output is:</p>
  
  <pre><code>sat
  unsat
  </code></pre>
  
  <p>Now when I try to prove the right-cancellation property: ( y x = z x ) => (y = z) using the following code</p>
  
  <pre><code>(declare-sort S)
  (declare-fun e () S)
  (declare-fun mult (S S) S)
  (declare-fun inv (S) S)
  (assert (forall ((x S) (y S) (z S)) (= (mult (mult x y) z) (mult x (mult y z)))))
  (assert (forall ((x S)) (= (mult e x)  x)))
  (assert (forall ((x S)) (= (mult (inv x) x) e)))
  (assert (forall ((x S)) (= (mult x e)  x)))
  (assert (forall ((x S)) (= (mult x (inv x)) e)))
  
  (check-sat)
  (assert (not (forall ((x S) (y S) (z S)) (=&gt; (= (mult y x) (mult z x)) (= y z)))))
  (check-sat)
  </code></pre>
  
  <p>I am obtaining</p>
  
  <pre><code>timeout
  </code></pre>
  
  <p>Please let me know how to prove the right-cancellation property or it is not possible using Z3 ?</p>