;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 21:24:26 1995
;;
;;;;  -> x=x.
;;;; A*B*A*B*A*B=A*A*A*B*B*B, B*B*B*A*A*A=A*A*A*B*B*B -> .
;;;;  -> (x*y)*z=x*y*z.
;;;;  -> x*y*z*u=y*z*u*x.
;;
;; -----> EMPTY CLAUSE at   4.89 sec ----> 462 [hyper,4,412.1,134.1]  -> .
;;
(
(1 (input) ((not (= (* (A) (* (B) (* (A) (* (B) (* (A) (B)))))) (* (A) (* (A) (* (A) (* (B) (* (B) (B)))))))) (not (= (* (B) (* (B) (* (B) (* (A) (* (A) (A)))))) (* (A) (* (A) (* (A) (* (B) (* (B) (B))))))))))
(2 (input) ((= (* (* v0 v1) v2) (* v0 (* v1 v2)))))
(3 (input) ((= (* v0 (* v1 (* v2 v3))) (* v1 (* v2 (* v3 v0))))))
(4 (flip 3 (1)) ((= (* v1 (* v2 (* v3 v0))) (* v0 (* v1 (* v2 v3))))))
(5 (instantiate 3 ((v0 . v66))) ((= (* v66 (* v1 (* v2 v3))) (* v1 (* v2 (* v3 v66))))))
(6 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . (* v1 (* v2 v3))))) ((= (* v64 (* v65 (* v66 (* v1 (* v2 v3))))) (* v65 (* v66 (* (* v1 (* v2 v3)) v64))))))
(7 (paramod 5 (1 1) 6 (1 1 2 2)) ((= (* v64 (* v65 (* v1 (* v2 (* v3 v66))))) (* v65 (* v66 (* (* v1 (* v2 v3)) v64))))))
(8 (instantiate 2 ((v0 . v1)(v1 . (* v2 v3))(v2 . v64))) ((= (* (* v1 (* v2 v3)) v64) (* v1 (* (* v2 v3) v64)))))
(9 (paramod 8 (1 1) 7 (1 2 2 2)) ((= (* v64 (* v65 (* v1 (* v2 (* v3 v66))))) (* v65 (* v66 (* v1 (* (* v2 v3) v64)))))))
(10 (instantiate 2 ((v0 . v2)(v1 . v3)(v2 . v64))) ((= (* (* v2 v3) v64) (* v2 (* v3 v64)))))
(11 (paramod 10 (1 1) 9 (1 2 2 2 2)) ((= (* v64 (* v65 (* v1 (* v2 (* v3 v66))))) (* v65 (* v66 (* v1 (* v2 (* v3 v64))))))))
(12 (instantiate 11 ((v1 . v2)(v2 . v3)(v3 . v4)(v64 . v0)(v65 . v1)(v66 . v5))) ((= (* v0 (* v1 (* v2 (* v3 (* v4 v5))))) (* v1 (* v5 (* v2 (* v3 (* v4 v0))))))))
(13 (instantiate 3 ((v0 . v65)(v1 . v66)(v2 . v67)(v3 . v64))) ((= (* v65 (* v66 (* v67 v64))) (* v66 (* v67 (* v64 v65))))))
(14 (instantiate 4 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) ((= (* v65 (* v66 (* v67 v64))) (* v64 (* v65 (* v66 v67))))))
(15 (paramod 13 (1 1) 14 (1 1)) ((= (* v66 (* v67 (* v64 v65))) (* v64 (* v65 (* v66 v67))))))
(16 (instantiate 15 ((v64 . v2)(v65 . v3)(v66 . v0)(v67 . v1))) ((= (* v0 (* v1 (* v2 v3))) (* v2 (* v3 (* v0 v1))))))
(17 (instantiate 16 ((v0 . v65)(v1 . v66)(v2 . v67)(v3 . (* v68 v69)))) ((= (* v65 (* v66 (* v67 (* v68 v69)))) (* v67 (* (* v68 v69) (* v65 v66))))))
(18 (instantiate 12 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67)(v4 . v68)(v5 . v69))) ((= (* v64 (* v65 (* v66 (* v67 (* v68 v69))))) (* v65 (* v69 (* v66 (* v67 (* v68 v64))))))))
(19 (paramod 17 (1 1) 18 (1 1 2)) ((= (* v64 (* v67 (* (* v68 v69) (* v65 v66)))) (* v65 (* v69 (* v66 (* v67 (* v68 v64))))))))
(20 (instantiate 2 ((v0 . v68)(v1 . v69)(v2 . (* v65 v66)))) ((= (* (* v68 v69) (* v65 v66)) (* v68 (* v69 (* v65 v66))))))
(21 (paramod 20 (1 1) 19 (1 1 2 2)) ((= (* v64 (* v67 (* v68 (* v69 (* v65 v66))))) (* v65 (* v69 (* v66 (* v67 (* v68 v64))))))))
(22 (instantiate 21 ((v64 . v0)(v65 . v4)(v66 . v5)(v67 . v1)(v68 . v2)(v69 . v3))) ((= (* v0 (* v1 (* v2 (* v3 (* v4 v5))))) (* v4 (* v3 (* v5 (* v1 (* v2 v0))))))))
(23 (flip 22 (1)) ((= (* v4 (* v3 (* v5 (* v1 (* v2 v0))))) (* v0 (* v1 (* v2 (* v3 (* v4 v5))))))))
(24 (instantiate 4 ((v0 . (* v66 v64))(v1 . v67)(v2 . v69)(v3 . v65))) ((= (* v67 (* v69 (* v65 (* v66 v64)))) (* (* v66 v64) (* v67 (* v69 v65))))))
(25 (instantiate 23 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67)(v4 . v68)(v5 . v69))) ((= (* v68 (* v67 (* v69 (* v65 (* v66 v64))))) (* v64 (* v65 (* v66 (* v67 (* v68 v69))))))))
(26 (paramod 24 (1 1) 25 (1 1 2)) ((= (* v68 (* (* v66 v64) (* v67 (* v69 v65)))) (* v64 (* v65 (* v66 (* v67 (* v68 v69))))))))
(27 (instantiate 2 ((v0 . v66)(v1 . v64)(v2 . (* v67 (* v69 v65))))) ((= (* (* v66 v64) (* v67 (* v69 v65))) (* v66 (* v64 (* v67 (* v69 v65)))))))
(28 (paramod 27 (1 1) 26 (1 1 2)) ((= (* v68 (* v66 (* v64 (* v67 (* v69 v65))))) (* v64 (* v65 (* v66 (* v67 (* v68 v69))))))))
(29 (instantiate 28 ((v64 . v2)(v65 . v5)(v66 . v1)(v67 . v3)(v68 . v0)(v69 . v4))) ((= (* v0 (* v1 (* v2 (* v3 (* v4 v5))))) (* v2 (* v5 (* v1 (* v3 (* v0 v4))))))))
(30 (flip 29 (1)) ((= (* v2 (* v5 (* v1 (* v3 (* v0 v4))))) (* v0 (* v1 (* v2 (* v3 (* v4 v5))))))))
(31 (instantiate 30 ((v0 . (A))(v1 . (A))(v2 . (A))(v3 . (B))(v4 . (B))(v5 . (B)))) ((= (* (A) (* (B) (* (A) (* (B) (* (A) (B)))))) (* (A) (* (A) (* (A) (* (B) (* (B) (B)))))))))
(32 (resolve 1 (1) 31 (1)) ((not (= (* (B) (* (B) (* (B) (* (A) (* (A) (A)))))) (* (A) (* (A) (* (A) (* (B) (* (B) (B))))))))))
(33 (instantiate 23 ((v0 . (A))(v1 . (A))(v2 . (A))(v3 . (B))(v4 . (B))(v5 . (B)))) ((= (* (B) (* (B) (* (B) (* (A) (* (A) (A)))))) (* (A) (* (A) (* (A) (* (B) (* (B) (B)))))))))
(34 (resolve 32 (1) 33 (1)) ())
)