z3 - Why the unstable branch is not able to prove a theorem but the master branch is able? -

i trying prove theorem in group theory using following z3 smt-lib code

 (declare-sort s) (declare-fun identity () s) (declare-fun product (s s s) bool) (declare-fun inverse (s) s) (declare-fun multiply (s s) s)  (assert (forall ((x s)) (product identity x x) )) (assert (forall ((x s)) (product x identity x) )) (assert (forall ((x s)) (product (inverse x) x identity) )) (assert (forall ((x s)) (product x (inverse x) identity) )) (assert (forall ((x s) (y s)) (product x y (multiply x y)) )) ;;(assert (forall ((x s) (y s) (z s) (w s)) (or (not (product x y z))  ;;                                              (not (product x y w)) ;;                                              (= z w))))   (assert (forall ((x s) (y s) (z s) (u s) (v s) (w s)) (or (not (product x y u))                                                (not (product y z v))                                               (not (product u z w) )                                               (product x v w))))  (assert (forall ((x s) (y s) (z s) (u s) (v s) (w s)) (or (not (product x y u))                                                (not (product y z v))                                               (not (product x v w) )                                               (product u z w))))    (check-sat)   (push) ;; file     : grp001-1 : tptp v6.0.0. released v1.0.0. ;; domain   : group theory ;; problem  : x^2 = identity => commutativity ;; version  : [mow76] axioms. ;; english  : if square of every element identity, system ;;            commutative. (declare-fun () s) (declare-fun b () s) (declare-fun c () s) (assert (forall ((x s)) (product x x identity) )) (assert (product b c)) (assert (not (product b c))) (check-sat) (pop) 

please run code online here.

the master branch z3 able prove such theorem unstable branch not able. please let me know why. many thanks.