;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  9 15:39:27 1995
;;
;;;;  -> x=x.
;;;; z1*x=u, z2*y=u, z1*z=w, z3*y=w -> z2*z=z3*x.
;;;; f(B,A)=f(A,B), f(f(A,B),C)=f(A,f(B,C)), f(e,A)=A, f(y,A)=e -> .
;;;;  -> x* (y*x)=y.
;;;;  -> x*e=e*x.
;;;;  -> f(x,y)=e* (y*x).
;;
;; ----> UNIT CONFLICT at   2.15 sec ----> 350 [binary,349.1,115.1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((not (= (* v0 v1) v2)) (not (= (* v3 v4) v2)) (not (= (* v0 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v1))))
(3 (input) ((not (= (f (B) (A)) (f (A) (B)))) (not (= (f (f (A) (B)) (C)) (f (A) (f (B) (C))))) (not (= (f (e) (A)) (A))) (not (= (f v0 (A)) (e)))))
(4 (input) ((= (* v0 (* v1 v0)) v1)))
(5 (input) ((= (* v0 (e)) (* (e) v0))))
(6 (input) ((= (f v0 v1) (* (e) (* v1 v0)))))
(7 (instantiate 6 ((v0 . (B))(v1 . (A)))) ((= (f (B) (A)) (* (e) (* (A) (B))))))
(8 (paramod 7 (1 1) 3 (1 1 1)) ((not (= (* (e) (* (A) (B))) (f (A) (B)))) (not (= (f (f (A) (B)) (C)) (f (A) (f (B) (C))))) (not (= (f (e) (A)) (A))) (not (= (f v0 (A)) (e)))))
(9 (instantiate 6 ((v0 . (A))(v1 . (B)))) ((= (f (A) (B)) (* (e) (* (B) (A))))))
(10 (paramod 9 (1 1) 8 (1 1 2)) ((not (= (* (e) (* (A) (B))) (* (e) (* (B) (A))))) (not (= (f (f (A) (B)) (C)) (f (A) (f (B) (C))))) (not (= (f (e) (A)) (A))) (not (= (f v0 (A)) (e)))))
(11 (instantiate 6 ((v0 . (A))(v1 . (B)))) ((= (f (A) (B)) (* (e) (* (B) (A))))))
(12 (paramod 11 (1 1) 10 (2 1 1 1)) ((not (= (* (e) (* (A) (B))) (* (e) (* (B) (A))))) (not (= (f (* (e) (* (B) (A))) (C)) (f (A) (f (B) (C))))) (not (= (f (e) (A)) (A))) (not (= (f v0 (A)) (e)))))
(13 (instantiate 6 ((v0 . (* (e) (* (B) (A))))(v1 . (C)))) ((= (f (* (e) (* (B) (A))) (C)) (* (e) (* (C) (* (e) (* (B) (A))))))))
(14 (paramod 13 (1 1) 12 (2 1 1)) ((not (= (* (e) (* (A) (B))) (* (e) (* (B) (A))))) (not (= (* (e) (* (C) (* (e) (* (B) (A))))) (f (A) (f (B) (C))))) (not (= (f (e) (A)) (A))) (not (= (f v0 (A)) (e)))))
(15 (instantiate 6 ((v0 . (B))(v1 . (C)))) ((= (f (B) (C)) (* (e) (* (C) (B))))))
(16 (paramod 15 (1 1) 14 (2 1 2 2)) ((not (= (* (e) (* (A) (B))) (* (e) (* (B) (A))))) (not (= (* (e) (* (C) (* (e) (* (B) (A))))) (f (A) (* (e) (* (C) (B)))))) (not (= (f (e) (A)) (A))) (not (= (f v0 (A)) (e)))))
(17 (instantiate 6 ((v0 . (A))(v1 . (* (e) (* (C) (B)))))) ((= (f (A) (* (e) (* (C) (B)))) (* (e) (* (* (e) (* (C) (B))) (A))))))
(18 (paramod 17 (1 1) 16 (2 1 2)) ((not (= (* (e) (* (A) (B))) (* (e) (* (B) (A))))) (not (= (* (e) (* (C) (* (e) (* (B) (A))))) (* (e) (* (* (e) (* (C) (B))) (A))))) (not (= (f (e) (A)) (A))) (not (= (f v0 (A)) (e)))))
(19 (instantiate 6 ((v0 . (e))(v1 . (A)))) ((= (f (e) (A)) (* (e) (* (A) (e))))))
(20 (paramod 19 (1 1) 18 (3 1 1)) ((not (= (* (e) (* (A) (B))) (* (e) (* (B) (A))))) (not (= (* (e) (* (C) (* (e) (* (B) (A))))) (* (e) (* (* (e) (* (C) (B))) (A))))) (not (= (* (e) (* (A) (e))) (A))) (not (= (f v0 (A)) (e)))))
(21 (instantiate 4 ((v0 . (e))(v1 . (A)))) ((= (* (e) (* (A) (e))) (A))))
(22 (paramod 21 (1 1) 20 (3 1 1)) ((not (= (* (e) (* (A) (B))) (* (e) (* (B) (A))))) (not (= (* (e) (* (C) (* (e) (* (B) (A))))) (* (e) (* (* (e) (* (C) (B))) (A))))) (not (= (A) (A))) (not (= (f v0 (A)) (e)))))
(23 (instantiate 6 ((v0 . v0)(v1 . (A)))) ((= (f v0 (A)) (* (e) (* (A) v0)))))
(24 (paramod 23 (1 1) 22 (4 1 1)) ((not (= (* (e) (* (A) (B))) (* (e) (* (B) (A))))) (not (= (* (e) (* (C) (* (e) (* (B) (A))))) (* (e) (* (* (e) (* (C) (B))) (A))))) (not (= (A) (A))) (not (= (* (e) (* (A) v0)) (e)))))
(25 (flip 24 (1)) ((not (= (* (e) (* (B) (A))) (* (e) (* (A) (B))))) (not (= (* (e) (* (C) (* (e) (* (B) (A))))) (* (e) (* (* (e) (* (C) (B))) (A))))) (not (= (A) (A))) (not (= (* (e) (* (A) v0)) (e)))))
(26 (flip 25 (2)) ((not (= (* (e) (* (B) (A))) (* (e) (* (A) (B))))) (not (= (* (e) (* (* (e) (* (C) (B))) (A))) (* (e) (* (C) (* (e) (* (B) (A))))))) (not (= (A) (A))) (not (= (* (e) (* (A) v0)) (e)))))
(27 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(28 (resolve 26 (3) 27 (1)) ((not (= (* (e) (* (B) (A))) (* (e) (* (A) (B))))) (not (= (* (e) (* (* (e) (* (C) (B))) (A))) (* (e) (* (C) (* (e) (* (B) (A))))))) (not (= (* (e) (* (A) v0)) (e)))))
(29 (instantiate 4 ((v0 . v65))) ((= (* v65 (* v1 v65)) v1)))
(30 (instantiate 4 ((v0 . (* v1 v65))(v1 . v65))) ((= (* (* v1 v65) (* v65 (* v1 v65))) v65)))
(31 (paramod 29 (1 1) 30 (1 1 2)) ((= (* (* v1 v65) v1) v65)))
(32 (instantiate 31 ((v1 . v0)(v65 . v1))) ((= (* (* v0 v1) v0) v1)))
(33 (instantiate 2 ((v0 . v64)(v1 . (* v65 v64))(v2 . v65))) ((not (= (* v64 (* v65 v64)) v65)) (not (= (* v3 v4) v65)) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* v65 v64)))))
(34 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) v65)))
(35 (resolve 33 (1) 34 (1)) ((not (= (* v3 v4) v65)) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* v65 v64)))))
(36 (instantiate 35 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v3)(v65 . v2))) ((not (= (* v0 v1) v2)) (not (= (* v3 v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 (* v2 v3)))))
(37 (instantiate 36 ((v0 . v64)(v1 . (e))(v2 . (* (e) v64)))) ((not (= (* v64 (e)) (* (e) v64))) (not (= (* v3 v4) v5)) (not (= (* v6 (e)) v5)) (= (* v64 v4) (* v6 (* (* (e) v64) v3)))))
(38 (instantiate 5 ((v0 . v64))) ((= (* v64 (e)) (* (e) v64))))
(39 (resolve 37 (1) 38 (1)) ((not (= (* v3 v4) v5)) (not (= (* v6 (e)) v5)) (= (* v64 v4) (* v6 (* (* (e) v64) v3)))))
(40 (instantiate 39 ((v3 . v0)(v4 . v1)(v5 . v2)(v6 . v3)(v64 . v4))) ((not (= (* v0 v1) v2)) (not (= (* v3 (e)) v2)) (= (* v4 v1) (* v3 (* (* (e) v4) v0)))))
(41 (instantiate 40 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v3 (e)) (* v0 v1))) (= (* v4 v1) (* v3 (* (* (e) v4) v0)))))
(42 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(43 (resolve 41 (1) 42 (1)) ((not (= (* v3 (e)) (* v0 v1))) (= (* v4 v1) (* v3 (* (* (e) v4) v0)))))
(44 (instantiate 43 ((v0 . v1)(v1 . v2)(v3 . v0)(v4 . v3))) ((not (= (* v0 (e)) (* v1 v2))) (= (* v3 v2) (* v0 (* (* (e) v3) v1)))))
(45 (instantiate 44 ((v0 . v64)(v1 . (e))(v2 . v64))) ((not (= (* v64 (e)) (* (e) v64))) (= (* v3 v64) (* v64 (* (* (e) v3) (e))))))
(46 (instantiate 5 ((v0 . v64))) ((= (* v64 (e)) (* (e) v64))))
(47 (resolve 45 (1) 46 (1)) ((= (* v3 v64) (* v64 (* (* (e) v3) (e))))))
(48 (instantiate 47 ((v3 . v0)(v64 . v1))) ((= (* v0 v1) (* v1 (* (* (e) v0) (e))))))
(49 (instantiate 32 ((v0 . (e))(v1 . v0))) ((= (* (* (e) v0) (e)) v0)))
(50 (paramod 49 (1 1) 48 (1 2 2)) ((= (* v0 v1) (* v1 v0))))
(51 (instantiate 32 ((v0 . v65))) ((= (* (* v65 v1) v65) v1)))
(52 (instantiate 50 ((v0 . (* v65 v1))(v1 . v65))) ((= (* (* v65 v1) v65) (* v65 (* v65 v1)))))
(53 (paramod 51 (1 1) 52 (1 1)) ((= v1 (* v65 (* v65 v1)))))
(54 (flip 53 (1)) ((= (* v65 (* v65 v1)) v1)))
(55 (instantiate 54 ((v65 . v0))) ((= (* v0 (* v0 v1)) v1)))
(56 (instantiate 4 ((v0 . v64))) ((= (* v64 (* v1 v64)) v1)))
(57 (instantiate 50 ((v0 . v64)(v1 . (* v1 v64)))) ((= (* v64 (* v1 v64)) (* (* v1 v64) v64))))
(58 (paramod 56 (1 1) 57 (1 1)) ((= v1 (* (* v1 v64) v64))))
(59 (flip 58 (1)) ((= (* (* v1 v64) v64) v1)))
(60 (instantiate 59 ((v1 . v0)(v64 . v1))) ((= (* (* v0 v1) v1) v0)))
(61 (instantiate 2 ((v0 . v64)(v1 . (* v64 v65))(v2 . v65))) ((not (= (* v64 (* v64 v65)) v65)) (not (= (* v3 v4) v65)) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* v64 v65)))))
(62 (instantiate 55 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v64 v65)) v65)))
(63 (resolve 61 (1) 62 (1)) ((not (= (* v3 v4) v65)) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* v64 v65)))))
(64 (instantiate 63 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v3)(v65 . v2))) ((not (= (* v0 v1) v2)) (not (= (* v3 v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 (* v3 v2)))))
(65 (instantiate 64 ((v0 . v64)(v1 . (* v64 v65))(v2 . v65))) ((not (= (* v64 (* v64 v65)) v65)) (not (= (* v3 v4) v5)) (not (= (* v6 (* v64 v65)) v5)) (= (* v64 v4) (* v6 (* v3 v65)))))
(66 (instantiate 55 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v64 v65)) v65)))
(67 (resolve 65 (1) 66 (1)) ((not (= (* v3 v4) v5)) (not (= (* v6 (* v64 v65)) v5)) (= (* v64 v4) (* v6 (* v3 v65)))))
(68 (instantiate 67 ((v3 . v0)(v4 . v1)(v5 . v2)(v6 . v3)(v64 . v4)(v65 . v5))) ((not (= (* v0 v1) v2)) (not (= (* v3 (* v4 v5)) v2)) (= (* v4 v1) (* v3 (* v0 v5)))))
(69 (instantiate 68 ((v0 . v64)(v1 . (* v65 v64))(v2 . v65))) ((not (= (* v64 (* v65 v64)) v65)) (not (= (* v3 (* v4 v5)) v65)) (= (* v4 (* v65 v64)) (* v3 (* v64 v5)))))
(70 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) v65)))
(71 (resolve 69 (1) 70 (1)) ((not (= (* v3 (* v4 v5)) v65)) (= (* v4 (* v65 v64)) (* v3 (* v64 v5)))))
(72 (instantiate 71 ((v3 . v0)(v4 . v1)(v5 . v2)(v64 . v4)(v65 . v3))) ((not (= (* v0 (* v1 v2)) v3)) (= (* v1 (* v3 v4)) (* v0 (* v4 v2)))))
(73 (instantiate 72 ((v0 . v64)(v1 . v64)(v2 . v65)(v3 . v65))) ((not (= (* v64 (* v64 v65)) v65)) (= (* v64 (* v65 v4)) (* v64 (* v4 v65)))))
(74 (instantiate 55 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v64 v65)) v65)))
(75 (resolve 73 (1) 74 (1)) ((= (* v64 (* v65 v4)) (* v64 (* v4 v65)))))
(76 (instantiate 75 ((v4 . v2)(v64 . v0)(v65 . v1))) ((= (* v0 (* v1 v2)) (* v0 (* v2 v1)))))
(77 (instantiate 2 ((v0 . (* v64 v65))(v1 . v65)(v2 . v64))) ((not (= (* (* v64 v65) v65) v64)) (not (= (* v3 v4) v64)) (not (= (* (* v64 v65) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v65))))
(78 (instantiate 60 ((v0 . v64)(v1 . v65))) ((= (* (* v64 v65) v65) v64)))
(79 (resolve 77 (1) 78 (1)) ((not (= (* v3 v4) v64)) (not (= (* (* v64 v65) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v65))))
(80 (instantiate 79 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v2)(v65 . v3))) ((not (= (* v0 v1) v2)) (not (= (* (* v2 v3) v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 v3))))
(81 (instantiate 80 ((v0 . v64)(v1 . (* v64 v65))(v2 . v65))) ((not (= (* v64 (* v64 v65)) v65)) (not (= (* (* v65 v3) v4) v5)) (not (= (* v6 (* v64 v65)) v5)) (= (* v64 v4) (* v6 v3))))
(82 (instantiate 55 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v64 v65)) v65)))
(83 (resolve 81 (1) 82 (1)) ((not (= (* (* v65 v3) v4) v5)) (not (= (* v6 (* v64 v65)) v5)) (= (* v64 v4) (* v6 v3))))
(84 (instantiate 83 ((v3 . v1)(v4 . v2)(v5 . v3)(v6 . v4)(v64 . v5)(v65 . v0))) ((not (= (* (* v0 v1) v2) v3)) (not (= (* v4 (* v5 v0)) v3)) (= (* v5 v2) (* v4 v1))))
(85 (instantiate 84 ((v2 . (* v65 (* v0 v1)))(v3 . v65))) ((not (= (* (* v0 v1) (* v65 (* v0 v1))) v65)) (not (= (* v4 (* v5 v0)) v65)) (= (* v5 (* v65 (* v0 v1))) (* v4 v1))))
(86 (instantiate 4 ((v0 . (* v0 v1))(v1 . v65))) ((= (* (* v0 v1) (* v65 (* v0 v1))) v65)))
(87 (resolve 85 (1) 86 (1)) ((not (= (* v4 (* v5 v0)) v65)) (= (* v5 (* v65 (* v0 v1))) (* v4 v1))))
(88 (instantiate 87 ((v0 . v2)(v1 . v4)(v4 . v0)(v5 . v1)(v65 . v3))) ((not (= (* v0 (* v1 v2)) v3)) (= (* v1 (* v3 (* v2 v4))) (* v0 v4))))
(89 (instantiate 88 ((v0 . (* v64 (* v1 v2)))(v3 . v64))) ((not (= (* (* v64 (* v1 v2)) (* v1 v2)) v64)) (= (* v1 (* v64 (* v2 v4))) (* (* v64 (* v1 v2)) v4))))
(90 (instantiate 60 ((v0 . v64)(v1 . (* v1 v2)))) ((= (* (* v64 (* v1 v2)) (* v1 v2)) v64)))
(91 (resolve 89 (1) 90 (1)) ((= (* v1 (* v64 (* v2 v4))) (* (* v64 (* v1 v2)) v4))))
(92 (instantiate 91 ((v1 . v0)(v4 . v3)(v64 . v1))) ((= (* v0 (* v1 (* v2 v3))) (* (* v1 (* v0 v2)) v3))))
(93 (flip 92 (1)) ((= (* (* v1 (* v0 v2)) v3) (* v0 (* v1 (* v2 v3))))))
(94 (instantiate 93 ((v0 . v1)(v1 . v0))) ((= (* (* v0 (* v1 v2)) v3) (* v1 (* v0 (* v2 v3))))))
(95 (instantiate 94 ((v0 . (e))(v1 . (C))(v2 . (B))(v3 . (A)))) ((= (* (* (e) (* (C) (B))) (A)) (* (C) (* (e) (* (B) (A)))))))
(96 (paramod 95 (1 1) 28 (2 1 1 2)) ((not (= (* (e) (* (B) (A))) (* (e) (* (A) (B))))) (not (= (* (e) (* (C) (* (e) (* (B) (A))))) (* (e) (* (C) (* (e) (* (B) (A))))))) (not (= (* (e) (* (A) v0)) (e)))))
(97 (instantiate 76 ((v0 . (e))(v1 . (B))(v2 . (A)))) ((= (* (e) (* (B) (A))) (* (e) (* (A) (B))))))
(98 (resolve 96 (1) 97 (1)) ((not (= (* (e) (* (C) (* (e) (* (B) (A))))) (* (e) (* (C) (* (e) (* (B) (A))))))) (not (= (* (e) (* (A) v0)) (e)))))
(99 (instantiate 1 ((v0 . (* (e) (* (C) (* (e) (* (B) (A)))))))) ((= (* (e) (* (C) (* (e) (* (B) (A))))) (* (e) (* (C) (* (e) (* (B) (A))))))))
(100 (resolve 98 (1) 99 (1)) ((not (= (* (e) (* (A) v0)) (e)))))
(101 (instantiate 55 ((v0 . (A)))) ((= (* (A) (* (A) v1)) v1)))
(102 (instantiate 100 ((v0 . (* (A) v1)))) ((not (= (* (e) (* (A) (* (A) v1))) (e)))))
(103 (paramod 101 (1 1) 102 (1 1 1 2)) ((not (= (* (e) v1) (e)))))
(104 (instantiate 103 ((v1 . v0))) ((not (= (* (e) v0) (e)))))
(105 (instantiate 104 ((v0 . (* (e) (e))))) ((not (= (* (e) (* (e) (e))) (e)))))
(106 (instantiate 55 ((v0 . (e))(v1 . (e)))) ((= (* (e) (* (e) (e))) (e))))
(107 (resolve 105 (1) 106 (1)) ())
)