;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 21:24:40 1995
;;
;;;;  -> x=x.
;;;; A*B*A*B*A*B*A*B=A*A*A*A*B*B*B*B, B*B*B*B*A*A*A*A=A*A*A*A*B*B*B*B -> .
;;;;  -> (x*y)*z=x*y*z.
;;;;  -> x*y*z*u*v=y*z*u*v*x.
;;
;; -----> EMPTY CLAUSE at 269.12 sec ----> 3136 [hyper,4,2799.1,2779.1]  -> .
;;
(
(1 (input) ((not (= (* (A) (* (B) (* (A) (* (B) (* (A) (* (B) (* (A) (B)))))))) (* (A) (* (A) (* (A) (* (A) (* (B) (* (B) (* (B) (B)))))))))) (not (= (* (B) (* (B) (* (B) (* (B) (* (A) (* (A) (* (A) (A)))))))) (* (A) (* (A) (* (A) (* (A) (* (B) (* (B) (* (B) (B))))))))))))
(2 (input) ((= (* (* v0 v1) v2) (* v0 (* v1 v2)))))
(3 (input) ((= (* v0 (* v1 (* v2 (* v3 v4)))) (* v1 (* v2 (* v3 (* v4 v0)))))))
(4 (flip 3 (1)) ((= (* v1 (* v2 (* v3 (* v4 v0)))) (* v0 (* v1 (* v2 (* v3 v4)))))))
(5 (instantiate 3 ((v0 . v67))) ((= (* v67 (* v1 (* v2 (* v3 v4)))) (* v1 (* v2 (* v3 (* v4 v67)))))))
(6 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67)(v4 . (* v1 (* v2 (* v3 v4)))))) ((= (* v64 (* v65 (* v66 (* v67 (* v1 (* v2 (* v3 v4))))))) (* v65 (* v66 (* v67 (* (* v1 (* v2 (* v3 v4))) v64)))))))
(7 (paramod 5 (1 1) 6 (1 1 2 2 2)) ((= (* v64 (* v65 (* v66 (* v1 (* v2 (* v3 (* v4 v67))))))) (* v65 (* v66 (* v67 (* (* v1 (* v2 (* v3 v4))) v64)))))))
(8 (instantiate 2 ((v0 . v1)(v1 . (* v2 (* v3 v4)))(v2 . v64))) ((= (* (* v1 (* v2 (* v3 v4))) v64) (* v1 (* (* v2 (* v3 v4)) v64)))))
(9 (paramod 8 (1 1) 7 (1 2 2 2 2)) ((= (* v64 (* v65 (* v66 (* v1 (* v2 (* v3 (* v4 v67))))))) (* v65 (* v66 (* v67 (* v1 (* (* v2 (* v3 v4)) v64))))))))
(10 (instantiate 2 ((v0 . v2)(v1 . (* v3 v4))(v2 . v64))) ((= (* (* v2 (* v3 v4)) v64) (* v2 (* (* v3 v4) v64)))))
(11 (paramod 10 (1 1) 9 (1 2 2 2 2 2)) ((= (* v64 (* v65 (* v66 (* v1 (* v2 (* v3 (* v4 v67))))))) (* v65 (* v66 (* v67 (* v1 (* v2 (* (* v3 v4) v64)))))))))
(12 (instantiate 2 ((v0 . v3)(v1 . v4)(v2 . v64))) ((= (* (* v3 v4) v64) (* v3 (* v4 v64)))))
(13 (paramod 12 (1 1) 11 (1 2 2 2 2 2 2)) ((= (* v64 (* v65 (* v66 (* v1 (* v2 (* v3 (* v4 v67))))))) (* v65 (* v66 (* v67 (* v1 (* v2 (* v3 (* v4 v64))))))))))
(14 (instantiate 13 ((v1 . v3)(v2 . v4)(v3 . v5)(v4 . v6)(v64 . v0)(v65 . v1)(v66 . v2)(v67 . v7))) ((= (* v0 (* v1 (* v2 (* v3 (* v4 (* v5 (* v6 v7))))))) (* v1 (* v2 (* v7 (* v3 (* v4 (* v5 (* v6 v0))))))))))
(15 (instantiate 2 ((v2 . (* v65 (* v66 (* v67 v68)))))) ((= (* (* v0 v1) (* v65 (* v66 (* v67 v68)))) (* v0 (* v1 (* v65 (* v66 (* v67 v68))))))))
(16 (instantiate 3 ((v0 . (* v0 v1))(v1 . v65)(v2 . v66)(v3 . v67)(v4 . v68))) ((= (* (* v0 v1) (* v65 (* v66 (* v67 v68)))) (* v65 (* v66 (* v67 (* v68 (* v0 v1))))))))
(17 (paramod 15 (1 1) 16 (1 1)) ((= (* v0 (* v1 (* v65 (* v66 (* v67 v68))))) (* v65 (* v66 (* v67 (* v68 (* v0 v1))))))))
(18 (instantiate 17 ((v65 . v2)(v66 . v3)(v67 . v4)(v68 . v5))) ((= (* v0 (* v1 (* v2 (* v3 (* v4 v5))))) (* v2 (* v3 (* v4 (* v5 (* v0 v1))))))))
(19 (flip 14 (1)) ((= (* v1 (* v2 (* v7 (* v3 (* v4 (* v5 (* v6 v0))))))) (* v0 (* v1 (* v2 (* v3 (* v4 (* v5 (* v6 v7))))))))))
(20 (instantiate 4 ((v1 . v65)(v2 . v66)(v3 . v67))) ((= (* v65 (* v66 (* v67 (* v4 v0)))) (* v0 (* v65 (* v66 (* v67 v4)))))))
(21 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67)(v4 . (* v4 v0)))) ((= (* v64 (* v65 (* v66 (* v67 (* v4 v0))))) (* v65 (* v66 (* v67 (* (* v4 v0) v64)))))))
(22 (paramod 20 (1 1) 21 (1 1 2)) ((= (* v64 (* v0 (* v65 (* v66 (* v67 v4))))) (* v65 (* v66 (* v67 (* (* v4 v0) v64)))))))
(23 (instantiate 2 ((v0 . v4)(v1 . v0)(v2 . v64))) ((= (* (* v4 v0) v64) (* v4 (* v0 v64)))))
(24 (paramod 23 (1 1) 22 (1 2 2 2 2)) ((= (* v64 (* v0 (* v65 (* v66 (* v67 v4))))) (* v65 (* v66 (* v67 (* v4 (* v0 v64))))))))
(25 (instantiate 24 ((v0 . v1)(v4 . v5)(v64 . v0)(v65 . v2)(v66 . v3)(v67 . v4))) ((= (* v0 (* v1 (* v2 (* v3 (* v4 v5))))) (* v2 (* v3 (* v4 (* v5 (* v1 v0))))))))
(26 (flip 25 (1)) ((= (* v2 (* v3 (* v4 (* v5 (* v1 v0))))) (* v0 (* v1 (* v2 (* v3 (* v4 v5))))))))
(27 (instantiate 26 ((v2 . v66)(v3 . v67)(v4 . v68))) ((= (* v66 (* v67 (* v68 (* v5 (* v1 v0))))) (* v0 (* v1 (* v66 (* v67 (* v68 v5))))))))
(28 (instantiate 18 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67)(v4 . v68)(v5 . (* v5 (* v1 v0))))) ((= (* v64 (* v65 (* v66 (* v67 (* v68 (* v5 (* v1 v0))))))) (* v66 (* v67 (* v68 (* (* v5 (* v1 v0)) (* v64 v65))))))))
(29 (paramod 27 (1 1) 28 (1 1 2 2)) ((= (* v64 (* v65 (* v0 (* v1 (* v66 (* v67 (* v68 v5))))))) (* v66 (* v67 (* v68 (* (* v5 (* v1 v0)) (* v64 v65))))))))
(30 (instantiate 2 ((v0 . v5)(v1 . (* v1 v0))(v2 . (* v64 v65)))) ((= (* (* v5 (* v1 v0)) (* v64 v65)) (* v5 (* (* v1 v0) (* v64 v65))))))
(31 (paramod 30 (1 1) 29 (1 2 2 2 2)) ((= (* v64 (* v65 (* v0 (* v1 (* v66 (* v67 (* v68 v5))))))) (* v66 (* v67 (* v68 (* v5 (* (* v1 v0) (* v64 v65)))))))))
(32 (instantiate 2 ((v0 . v1)(v1 . v0)(v2 . (* v64 v65)))) ((= (* (* v1 v0) (* v64 v65)) (* v1 (* v0 (* v64 v65))))))
(33 (paramod 32 (1 1) 31 (1 2 2 2 2 2)) ((= (* v64 (* v65 (* v0 (* v1 (* v66 (* v67 (* v68 v5))))))) (* v66 (* v67 (* v68 (* v5 (* v1 (* v0 (* v64 v65))))))))))
(34 (instantiate 33 ((v0 . v2)(v1 . v3)(v5 . v7)(v64 . v0)(v65 . v1)(v66 . v4)(v67 . v5)(v68 . v6))) ((= (* v0 (* v1 (* v2 (* v3 (* v4 (* v5 (* v6 v7))))))) (* v4 (* v5 (* v6 (* v7 (* v3 (* v2 (* v0 v1))))))))))
(35 (instantiate 26 ((v0 . (* v70 v64))(v1 . v69)(v2 . v66)(v3 . v71)(v4 . v67)(v5 . v68))) ((= (* v66 (* v71 (* v67 (* v68 (* v69 (* v70 v64)))))) (* (* v70 v64) (* v69 (* v66 (* v71 (* v67 v68))))))))
(36 (instantiate 19 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67)(v4 . v68)(v5 . v69)(v6 . v70)(v7 . v71))) ((= (* v65 (* v66 (* v71 (* v67 (* v68 (* v69 (* v70 v64))))))) (* v64 (* v65 (* v66 (* v67 (* v68 (* v69 (* v70 v71))))))))))
(37 (paramod 35 (1 1) 36 (1 1 2)) ((= (* v65 (* (* v70 v64) (* v69 (* v66 (* v71 (* v67 v68)))))) (* v64 (* v65 (* v66 (* v67 (* v68 (* v69 (* v70 v71))))))))))
(38 (instantiate 2 ((v0 . v70)(v1 . v64)(v2 . (* v69 (* v66 (* v71 (* v67 v68))))))) ((= (* (* v70 v64) (* v69 (* v66 (* v71 (* v67 v68))))) (* v70 (* v64 (* v69 (* v66 (* v71 (* v67 v68)))))))))
(39 (paramod 38 (1 1) 37 (1 1 2)) ((= (* v65 (* v70 (* v64 (* v69 (* v66 (* v71 (* v67 v68))))))) (* v64 (* v65 (* v66 (* v67 (* v68 (* v69 (* v70 v71))))))))))
(40 (instantiate 39 ((v64 . v2)(v65 . v0)(v66 . v4)(v67 . v6)(v68 . v7)(v69 . v3)(v70 . v1)(v71 . v5))) ((= (* v0 (* v1 (* v2 (* v3 (* v4 (* v5 (* v6 v7))))))) (* v2 (* v0 (* v4 (* v6 (* v7 (* v3 (* v1 v5))))))))))
(41 (instantiate 40 ((v0 . (A))(v1 . (B))(v2 . (A))(v3 . (B))(v4 . (A))(v5 . (B))(v6 . (A))(v7 . (B)))) ((= (* (A) (* (B) (* (A) (* (B) (* (A) (* (B) (* (A) (B)))))))) (* (A) (* (A) (* (A) (* (A) (* (B) (* (B) (* (B) (B)))))))))))
(42 (resolve 1 (1) 41 (1)) ((not (= (* (B) (* (B) (* (B) (* (B) (* (A) (* (A) (* (A) (A)))))))) (* (A) (* (A) (* (A) (* (A) (* (B) (* (B) (* (B) (B))))))))))))
(43 (instantiate 34 ((v0 . (B))(v1 . (B))(v2 . (B))(v3 . (B))(v4 . (A))(v5 . (A))(v6 . (A))(v7 . (A)))) ((= (* (B) (* (B) (* (B) (* (B) (* (A) (* (A) (* (A) (A)))))))) (* (A) (* (A) (* (A) (* (A) (* (B) (* (B) (* (B) (B)))))))))))
(44 (resolve 42 (1) 43 (1)) ())
)