Z3 is not able to prove the right-cancellation property in group theory?

Question

I am trying to prove some general properties in group theory.

For example the left-cancellation property : ( x y = x z ) => (y = z) it proved using the following 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)) (=> (= (mult x y) (mult x z)) (= y z)))))
(check-sat)

and the corresponding output is:

sat
unsat

Now when I try to prove the right-cancellation property: ( y x = z x ) => (y = z) using the following 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)) (=> (= (mult y x) (mult z x)) (= y z)))))
(check-sat)

I am obtaining

timeout

Please let me know how to prove the right-cancellation property or it is not possible using Z3 ?

Answer 1

As far as I know this style of theorems are better handled by super-position inference engines. Older versions of Z3 contains a superposition engine, but it is removed from newer versions as we have seen few uses overall for solving problems in universal algebra. There are several theorem provers specializing in super-position inferences, such as Vampire, E, SPASS and you can use the tools available from www.TPTP.org to try out these engines.

Answer 2

A possible proof of the right cancellation property using Z3 is as follows.

(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) (y S) (z S)) (= (mult x (mult y z)) (mult (mult x 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)

(push)
(assert (not (forall ((x S) (y S) (z S)) (=> (= (mult (mult y x) (inv x)) 
                                                (mult (mult z x) (inv x) )) (= y z)))))
(check-sat)
(pop)

and the respective output is

sat
unsat