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