;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:20:30 1995
;;
;;;;  -> x=x.
;;;;  -> ((x*x)*y)* (z* (y*x))=z.
;;;; B*A=A*B, A*A=A, (A*B)*A=B -> .
;;
;; ----> UNIT CONFLICT at   0.22 sec ----> 83 [binary,82.1,79.1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((= (* (* (* v0 v0) v1) (* v2 (* v1 v0))) v2)))
(3 (input) ((not (= (* (B) (A)) (* (A) (B)))) (not (= (* (A) (A)) (A))) (not (= (* (* (A) (B)) (A)) (B)))))
(4 (instantiate 2 ((v1 . (* v0 v0)))) ((= (* (* (* v0 v0) (* v0 v0)) (* v2 (* (* v0 v0) v0))) v2)))
(5 (instantiate 2 ((v0 . (* v0 v0))(v1 . (* v2 (* (* v0 v0) v0)))(v2 . v66))) ((= (* (* (* (* v0 v0) (* v0 v0)) (* v2 (* (* v0 v0) v0))) (* v66 (* (* v2 (* (* v0 v0) v0)) (* v0 v0)))) v66)))
(6 (paramod 4 (1 1) 5 (1 1 1)) ((= (* v2 (* v66 (* (* v2 (* (* v0 v0) v0)) (* v0 v0)))) v66)))
(7 (instantiate 6 ((v0 . v2)(v2 . v0)(v66 . v1))) ((= (* v0 (* v1 (* (* v0 (* (* v2 v2) v2)) (* v2 v2)))) v1)))
(8 (instantiate 2 ((v2 . v65))) ((= (* (* (* v0 v0) v1) (* v65 (* v1 v0))) v65)))
(9 (instantiate 2 ((v0 . (* v1 v0))(v1 . v65)(v2 . (* (* v0 v0) v1)))) ((= (* (* (* (* v1 v0) (* v1 v0)) v65) (* (* (* v0 v0) v1) (* v65 (* v1 v0)))) (* (* v0 v0) v1))))
(10 (paramod 8 (1 1) 9 (1 1 2)) ((= (* (* (* (* v1 v0) (* v1 v0)) v65) v65) (* (* v0 v0) v1))))
(11 (instantiate 10 ((v0 . v1)(v1 . v0)(v65 . v2))) ((= (* (* (* (* v0 v1) (* v0 v1)) v2) v2) (* (* v1 v1) v0))))
(12 (instantiate 2 ((v0 . v66)(v1 . v66)(v2 . (* v64 (* (* v66 v66) v66))))) ((= (* (* (* v66 v66) v66) (* (* v64 (* (* v66 v66) v66)) (* v66 v66))) (* v64 (* (* v66 v66) v66)))))
(13 (instantiate 7 ((v0 . v64)(v1 . (* (* v66 v66) v66))(v2 . v66))) ((= (* v64 (* (* (* v66 v66) v66) (* (* v64 (* (* v66 v66) v66)) (* v66 v66)))) (* (* v66 v66) v66))))
(14 (paramod 12 (1 1) 13 (1 1 2)) ((= (* v64 (* v64 (* (* v66 v66) v66))) (* (* v66 v66) v66))))
(15 (instantiate 14 ((v64 . v0)(v66 . v1))) ((= (* v0 (* v0 (* (* v1 v1) v1))) (* (* v1 v1) v1))))
(16 (instantiate 2 ((v0 . v65)(v1 . (* v65 v65))(v2 . (* (* v65 v65) (* v65 v65))))) ((= (* (* (* v65 v65) (* v65 v65)) (* (* (* v65 v65) (* v65 v65)) (* (* v65 v65) v65))) (* (* v65 v65) (* v65 v65)))))
(17 (instantiate 15 ((v0 . (* (* v65 v65) (* v65 v65)))(v1 . v65))) ((= (* (* (* v65 v65) (* v65 v65)) (* (* (* v65 v65) (* v65 v65)) (* (* v65 v65) v65))) (* (* v65 v65) v65))))
(18 (paramod 16 (1 1) 17 (1 1)) ((= (* (* v65 v65) (* v65 v65)) (* (* v65 v65) v65))))
(19 (instantiate 18 ((v65 . v0))) ((= (* (* v0 v0) (* v0 v0)) (* (* v0 v0) v0))))
(20 (instantiate 15 ((v0 . v65))) ((= (* v65 (* v65 (* (* v1 v1) v1))) (* (* v1 v1) v1))))
(21 (instantiate 2 ((v0 . (* (* v1 v1) v1))(v1 . v65)(v2 . v65))) ((= (* (* (* (* (* v1 v1) v1) (* (* v1 v1) v1)) v65) (* v65 (* v65 (* (* v1 v1) v1)))) v65)))
(22 (paramod 20 (1 1) 21 (1 1 2)) ((= (* (* (* (* (* v1 v1) v1) (* (* v1 v1) v1)) v65) (* (* v1 v1) v1)) v65)))
(23 (instantiate 22 ((v1 . v0)(v65 . v1))) ((= (* (* (* (* (* v0 v0) v0) (* (* v0 v0) v0)) v1) (* (* v0 v0) v0)) v1)))
(24 (instantiate 19 ((v0 . (* v0 v0)))) ((= (* (* (* v0 v0) (* v0 v0)) (* (* v0 v0) (* v0 v0))) (* (* (* v0 v0) (* v0 v0)) (* v0 v0)))))
(25 (paramod 19 (1 1) 24 (1 1 1)) ((= (* (* (* v0 v0) v0) (* (* v0 v0) (* v0 v0))) (* (* (* v0 v0) (* v0 v0)) (* v0 v0)))))
(26 (paramod 19 (1 1) 25 (1 1 2)) ((= (* (* (* v0 v0) v0) (* (* v0 v0) v0)) (* (* (* v0 v0) (* v0 v0)) (* v0 v0)))))
(27 (paramod 19 (1 1) 26 (1 2 1)) ((= (* (* (* v0 v0) v0) (* (* v0 v0) v0)) (* (* (* v0 v0) v0) (* v0 v0)))))
(28 (paramod 27 (1 1) 23 (1 1 1 1)) ((= (* (* (* (* (* v0 v0) v0) (* v0 v0)) v1) (* (* v0 v0) v0)) v1)))
(29 (instantiate 15 ((v0 . v64)(v1 . (* v0 v0)))) ((= (* v64 (* v64 (* (* (* v0 v0) (* v0 v0)) (* v0 v0)))) (* (* (* v0 v0) (* v0 v0)) (* v0 v0)))))
(30 (paramod 19 (1 1) 29 (1 1 2 2 1)) ((= (* v64 (* v64 (* (* (* v0 v0) v0) (* v0 v0)))) (* (* (* v0 v0) (* v0 v0)) (* v0 v0)))))
(31 (paramod 19 (1 1) 30 (1 2 1)) ((= (* v64 (* v64 (* (* (* v0 v0) v0) (* v0 v0)))) (* (* (* v0 v0) v0) (* v0 v0)))))
(32 (instantiate 31 ((v0 . v1)(v64 . v0))) ((= (* v0 (* v0 (* (* (* v1 v1) v1) (* v1 v1)))) (* (* (* v1 v1) v1) (* v1 v1)))))
(33 (instantiate 19 ((v0 . v64))) ((= (* (* v64 v64) (* v64 v64)) (* (* v64 v64) v64))))
(34 (instantiate 2 ((v0 . v64)(v1 . v64)(v2 . (* v64 v64)))) ((= (* (* (* v64 v64) v64) (* (* v64 v64) (* v64 v64))) (* v64 v64))))
(35 (paramod 33 (1 1) 34 (1 1 2)) ((= (* (* (* v64 v64) v64) (* (* v64 v64) v64)) (* v64 v64))))
(36 (instantiate 27 ((v0 . v64))) ((= (* (* (* v64 v64) v64) (* (* v64 v64) v64)) (* (* (* v64 v64) v64) (* v64 v64)))))
(37 (paramod 36 (1 1) 35 (1 1)) ((= (* (* (* v64 v64) v64) (* v64 v64)) (* v64 v64))))
(38 (instantiate 37 ((v64 . v0))) ((= (* (* (* v0 v0) v0) (* v0 v0)) (* v0 v0))))
(39 (instantiate 38 ((v0 . v1))) ((= (* (* (* v1 v1) v1) (* v1 v1)) (* v1 v1))))
(40 (paramod 39 (1 1) 32 (1 1 2 2)) ((= (* v0 (* v0 (* v1 v1))) (* (* (* v1 v1) v1) (* v1 v1)))))
(41 (instantiate 38 ((v0 . v1))) ((= (* (* (* v1 v1) v1) (* v1 v1)) (* v1 v1))))
(42 (paramod 41 (1 1) 40 (1 2)) ((= (* v0 (* v0 (* v1 v1))) (* v1 v1))))
(43 (paramod 38 (1 1) 28 (1 1 1 1)) ((= (* (* (* v0 v0) v1) (* (* v0 v0) v0)) v1)))
(44 (instantiate 43 ((v0 . v0)(v1 . v0))) ((= (* (* (* v0 v0) v0) (* (* v0 v0) v0)) v0)))
(45 (paramod 44 (1 1) 27 (1 1)) ((= v0 (* (* (* v0 v0) v0) (* v0 v0)))))
(46 (paramod 38 (1 1) 45 (1 2)) ((= v0 (* v0 v0))))
(47 (flip 46 (1)) ((= (* v0 v0) v0)))
(48 (paramod 47 (1 1) 43 (1 1 1 1)) ((= (* (* v0 v1) (* (* v0 v0) v0)) v1)))
(49 (paramod 47 (1 1) 48 (1 1 2 1)) ((= (* (* v0 v1) (* v0 v0)) v1)))
(50 (paramod 47 (1 1) 49 (1 1 2)) ((= (* (* v0 v1) v0) v1)))
(51 (instantiate 47 ((v0 . v1))) ((= (* v1 v1) v1)))
(52 (paramod 51 (1 1) 42 (1 1 2 2)) ((= (* v0 (* v0 v1)) (* v1 v1))))
(53 (instantiate 47 ((v0 . v1))) ((= (* v1 v1) v1)))
(54 (paramod 53 (1 1) 52 (1 2)) ((= (* v0 (* v0 v1)) v1)))
(55 (instantiate 47 ((v0 . (* v0 v1)))) ((= (* (* v0 v1) (* v0 v1)) (* v0 v1))))
(56 (paramod 55 (1 1) 11 (1 1 1 1)) ((= (* (* (* v0 v1) v2) v2) (* (* v1 v1) v0))))
(57 (instantiate 47 ((v0 . v1))) ((= (* v1 v1) v1)))
(58 (paramod 57 (1 1) 56 (1 2 1)) ((= (* (* (* v0 v1) v2) v2) (* v1 v0))))
(59 (instantiate 47 ((v0 . (A)))) ((= (* (A) (A)) (A))))
(60 (paramod 59 (1 1) 3 (2 1 1)) ((not (= (* (B) (A)) (* (A) (B)))) (not (= (A) (A))) (not (= (* (* (A) (B)) (A)) (B)))))
(61 (instantiate 50 ((v0 . (A))(v1 . (B)))) ((= (* (* (A) (B)) (A)) (B))))
(62 (paramod 61 (1 1) 60 (3 1 1)) ((not (= (* (B) (A)) (* (A) (B)))) (not (= (A) (A))) (not (= (B) (B)))))
(63 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(64 (resolve 62 (2) 63 (1)) ((not (= (* (B) (A)) (* (A) (B)))) (not (= (B) (B)))))
(65 (instantiate 1 ((v0 . (B)))) ((= (B) (B))))
(66 (resolve 64 (2) 65 (1)) ((not (= (* (B) (A)) (* (A) (B))))))
(67 (instantiate 50 ((v0 . v65))) ((= (* (* v65 v1) v65) v1)))
(68 (instantiate 54 ((v0 . (* v65 v1))(v1 . v65))) ((= (* (* v65 v1) (* (* v65 v1) v65)) v65)))
(69 (paramod 67 (1 1) 68 (1 1 2)) ((= (* (* v65 v1) v1) v65)))
(70 (instantiate 69 ((v65 . v0))) ((= (* (* v0 v1) v1) v0)))
(71 (instantiate 70 ((v0 . (* v0 v1))(v1 . v2))) ((= (* (* (* v0 v1) v2) v2) (* v0 v1))))
(72 (paramod 71 (1 1) 58 (1 1)) ((= (* v0 v1) (* v1 v0))))
(73 (instantiate 72 ((v0 . (B))(v1 . (A)))) ((= (* (B) (A)) (* (A) (B)))))
(74 (resolve 66 (1) 73 (1)) ())
)