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