;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 21:16:48 1995
;;
;;;; x=x.
;;;; (x*y)*z=x*y*z.
;;;; x*y*y=y*y*x.
;;;; A*B*A*B*A*B*A*B!=A*A*A*A*B*B*B*B.
;;
;; ----> UNIT CONFLICT at 187.41 sec ----> 4009 [binary,4008.1,1.1] $F.
;;
(
(1 (input) ((not (= (* (A) (* (B) (* (A) (* (B) (* (A) (* (B) (* (A) (B)))))))) (* (A) (* (A) (* (A) (* (A) (* (B) (* (B) (* (B) (B))))))))))))
(2 (input) ((= (* (* v0 v1) v2) (* v0 (* v1 v2)))))
(3 (input) ((= (* v0 (* v1 v1)) (* v1 (* v1 v0)))))
(4 (instantiate 2 ((v2 . (* v0 v1)))) ((= (* (* v0 v1) (* v0 v1)) (* v0 (* v1 (* v0 v1))))))
(5 (instantiate 3 ((v0 . v64)(v1 . (* v0 v1)))) ((= (* v64 (* (* v0 v1) (* v0 v1))) (* (* v0 v1) (* (* v0 v1) v64)))))
(6 (paramod 4 (1 1) 5 (1 1 2)) ((= (* v64 (* v0 (* v1 (* v0 v1)))) (* (* v0 v1) (* (* v0 v1) v64)))))
(7 (instantiate 2 ((v0 . v0)(v1 . v1)(v2 . v64))) ((= (* (* v0 v1) v64) (* v0 (* v1 v64)))))
(8 (paramod 7 (1 1) 6 (1 2 2)) ((= (* v64 (* v0 (* v1 (* v0 v1)))) (* (* v0 v1) (* v0 (* v1 v64))))))
(9 (instantiate 2 ((v0 . v0)(v1 . v1)(v2 . (* v0 (* v1 v64))))) ((= (* (* v0 v1) (* v0 (* v1 v64))) (* v0 (* v1 (* v0 (* v1 v64)))))))
(10 (paramod 9 (1 1) 8 (1 2)) ((= (* v64 (* v0 (* v1 (* v0 v1)))) (* v0 (* v1 (* v0 (* v1 v64)))))))
(11 (instantiate 10 ((v0 . v1)(v1 . v2)(v64 . v0))) ((= (* v0 (* v1 (* v2 (* v1 v2)))) (* v1 (* v2 (* v1 (* v2 v0)))))))
(12 (instantiate 3 ((v0 . v64))) ((= (* v64 (* v1 v1)) (* v1 (* v1 v64)))))
(13 (instantiate 2 ((v0 . v64)(v1 . (* v1 v1))(v2 . v66))) ((= (* (* v64 (* v1 v1)) v66) (* v64 (* (* v1 v1) v66)))))
(14 (paramod 12 (1 1) 13 (1 1 1)) ((= (* (* v1 (* v1 v64)) v66) (* v64 (* (* v1 v1) v66)))))
(15 (instantiate 2 ((v0 . v1)(v1 . (* v1 v64))(v2 . v66))) ((= (* (* v1 (* v1 v64)) v66) (* v1 (* (* v1 v64) v66)))))
(16 (paramod 15 (1 1) 14 (1 1)) ((= (* v1 (* (* v1 v64) v66)) (* v64 (* (* v1 v1) v66)))))
(17 (instantiate 2 ((v0 . v1)(v1 . v64)(v2 . v66))) ((= (* (* v1 v64) v66) (* v1 (* v64 v66)))))
(18 (paramod 17 (1 1) 16 (1 1 2)) ((= (* v1 (* v1 (* v64 v66))) (* v64 (* (* v1 v1) v66)))))
(19 (instantiate 2 ((v0 . v1)(v1 . v1)(v2 . v66))) ((= (* (* v1 v1) v66) (* v1 (* v1 v66)))))
(20 (paramod 19 (1 1) 18 (1 2 2)) ((= (* v1 (* v1 (* v64 v66))) (* v64 (* v1 (* v1 v66))))))
(21 (instantiate 20 ((v1 . v0)(v64 . v1)(v66 . v2))) ((= (* v0 (* v0 (* v1 v2))) (* v1 (* v0 (* v0 v2))))))
(22 (flip 21 (1)) ((= (* v1 (* v0 (* v0 v2))) (* v0 (* v0 (* v1 v2))))))
(23 (instantiate 11 ((v0 . v64))) ((= (* v64 (* v1 (* v2 (* v1 v2)))) (* v1 (* v2 (* v1 (* v2 v64)))))))
(24 (instantiate 2 ((v0 . v64)(v1 . (* v1 (* v2 (* v1 v2))))(v2 . v66))) ((= (* (* v64 (* v1 (* v2 (* v1 v2)))) v66) (* v64 (* (* v1 (* v2 (* v1 v2))) v66)))))
(25 (paramod 23 (1 1) 24 (1 1 1)) ((= (* (* v1 (* v2 (* v1 (* v2 v64)))) v66) (* v64 (* (* v1 (* v2 (* v1 v2))) v66)))))
(26 (instantiate 2 ((v0 . v1)(v1 . (* v2 (* v1 (* v2 v64))))(v2 . v66))) ((= (* (* v1 (* v2 (* v1 (* v2 v64)))) v66) (* v1 (* (* v2 (* v1 (* v2 v64))) v66)))))
(27 (paramod 26 (1 1) 25 (1 1)) ((= (* v1 (* (* v2 (* v1 (* v2 v64))) v66)) (* v64 (* (* v1 (* v2 (* v1 v2))) v66)))))
(28 (instantiate 2 ((v0 . v2)(v1 . (* v1 (* v2 v64)))(v2 . v66))) ((= (* (* v2 (* v1 (* v2 v64))) v66) (* v2 (* (* v1 (* v2 v64)) v66)))))
(29 (paramod 28 (1 1) 27 (1 1 2)) ((= (* v1 (* v2 (* (* v1 (* v2 v64)) v66))) (* v64 (* (* v1 (* v2 (* v1 v2))) v66)))))
(30 (instantiate 2 ((v0 . v1)(v1 . (* v2 v64))(v2 . v66))) ((= (* (* v1 (* v2 v64)) v66) (* v1 (* (* v2 v64) v66)))))
(31 (paramod 30 (1 1) 29 (1 1 2 2)) ((= (* v1 (* v2 (* v1 (* (* v2 v64) v66)))) (* v64 (* (* v1 (* v2 (* v1 v2))) v66)))))
(32 (instantiate 2 ((v0 . v2)(v1 . v64)(v2 . v66))) ((= (* (* v2 v64) v66) (* v2 (* v64 v66)))))
(33 (paramod 32 (1 1) 31 (1 1 2 2 2)) ((= (* v1 (* v2 (* v1 (* v2 (* v64 v66))))) (* v64 (* (* v1 (* v2 (* v1 v2))) v66)))))
(34 (instantiate 2 ((v0 . v1)(v1 . (* v2 (* v1 v2)))(v2 . v66))) ((= (* (* v1 (* v2 (* v1 v2))) v66) (* v1 (* (* v2 (* v1 v2)) v66)))))
(35 (paramod 34 (1 1) 33 (1 2 2)) ((= (* v1 (* v2 (* v1 (* v2 (* v64 v66))))) (* v64 (* v1 (* (* v2 (* v1 v2)) v66))))))
(36 (instantiate 2 ((v0 . v2)(v1 . (* v1 v2))(v2 . v66))) ((= (* (* v2 (* v1 v2)) v66) (* v2 (* (* v1 v2) v66)))))
(37 (paramod 36 (1 1) 35 (1 2 2 2)) ((= (* v1 (* v2 (* v1 (* v2 (* v64 v66))))) (* v64 (* v1 (* v2 (* (* v1 v2) v66)))))))
(38 (instantiate 2 ((v0 . v1)(v1 . v2)(v2 . v66))) ((= (* (* v1 v2) v66) (* v1 (* v2 v66)))))
(39 (paramod 38 (1 1) 37 (1 2 2 2 2)) ((= (* v1 (* v2 (* v1 (* v2 (* v64 v66))))) (* v64 (* v1 (* v2 (* v1 (* v2 v66))))))))
(40 (instantiate 39 ((v1 . v0)(v2 . v1)(v64 . v2)(v66 . v3))) ((= (* v0 (* v1 (* v0 (* v1 (* v2 v3))))) (* v2 (* v0 (* v1 (* v0 (* v1 v3))))))))
(41 (flip 40 (1)) ((= (* v2 (* v0 (* v1 (* v0 (* v1 v3))))) (* v0 (* v1 (* v0 (* v1 (* v2 v3))))))))
(42 (instantiate 22 ((v1 . v64))) ((= (* v64 (* v0 (* v0 v2))) (* v0 (* v0 (* v64 v2))))))
(43 (instantiate 22 ((v0 . v64)(v1 . v65)(v2 . (* v0 (* v0 v2))))) ((= (* v65 (* v64 (* v64 (* v0 (* v0 v2))))) (* v64 (* v64 (* v65 (* v0 (* v0 v2))))))))
(44 (paramod 42 (1 1) 43 (1 1 2 2)) ((= (* v65 (* v64 (* v0 (* v0 (* v64 v2))))) (* v64 (* v64 (* v65 (* v0 (* v0 v2))))))))
(45 (instantiate 44 ((v0 . v2)(v2 . v3)(v64 . v1)(v65 . v0))) ((= (* v0 (* v1 (* v2 (* v2 (* v1 v3))))) (* v1 (* v1 (* v0 (* v2 (* v2 v3))))))))
(46 (instantiate 45 ((v0 . v65)(v1 . v64)(v2 . v65))) ((= (* v65 (* v64 (* v65 (* v65 (* v64 v3))))) (* v64 (* v64 (* v65 (* v65 (* v65 v3))))))))
(47 (instantiate 41 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . (* v65 (* v64 v3))))) ((= (* v66 (* v64 (* v65 (* v64 (* v65 (* v65 (* v64 v3))))))) (* v64 (* v65 (* v64 (* v65 (* v66 (* v65 (* v64 v3))))))))))
(48 (paramod 46 (1 1) 47 (1 1 2 2)) ((= (* v66 (* v64 (* v64 (* v64 (* v65 (* v65 (* v65 v3))))))) (* v64 (* v65 (* v64 (* v65 (* v66 (* v65 (* v64 v3))))))))))
(49 (instantiate 48 ((v64 . v1)(v65 . v2)(v66 . v0))) ((= (* v0 (* v1 (* v1 (* v1 (* v2 (* v2 (* v2 v3))))))) (* v1 (* v2 (* v1 (* v2 (* v0 (* v2 (* v1 v3))))))))))
(50 (flip 49 (1)) ((= (* v1 (* v2 (* v1 (* v2 (* v0 (* v2 (* v1 v3))))))) (* v0 (* v1 (* v1 (* v1 (* v2 (* v2 (* v2 v3))))))))))
(51 (instantiate 50 ((v0 . (A))(v1 . (A))(v2 . (B))(v3 . (B)))) ((= (* (A) (* (B) (* (A) (* (B) (* (A) (* (B) (* (A) (B)))))))) (* (A) (* (A) (* (A) (* (A) (* (B) (* (B) (* (B) (B)))))))))))
(52 (resolve 1 (1) 51 (1)) ())
)