;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:22:04 1995
;;
;;;;  -> x=x.
;;;; z1*x=u, z2*y=u, z1*z=w, z3*y=w -> z2*z=z3*x.
;;;;  -> e*e=e.
;;;;  -> e*x=x*e.
;;;;  -> x* (y*x)=y.
;;;; (A* (((A*B)*C)* (B*e)))* (e*e)=C -> .
;;
;; ----> UNIT CONFLICT at   0.64 sec ----> 133 [binary,132.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) ((= (* (e) v0) (* v0 (e)))))
(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 . (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))))
(9 (instantiate 4 ((v0 . v64))) ((= (* (e) v64) (* v64 (e)))))
(10 (resolve 8 (1) 9 (1)) ((not (= (* v3 v4) (* v64 (e)))) (not (= (* (e) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v64))))
(11 (instantiate 10 ((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))))
(12 (instantiate 11 ((v1 . (e))(v2 . v0))) ((not (= (* v0 (e)) (* v0 (e)))) (not (= (* (e) v3) v4)) (not (= (* v5 (e)) v4)) (= (* v0 v3) (* v5 v0))))
(13 (instantiate 1 ((v0 . (* v0 (e))))) ((= (* v0 (e)) (* v0 (e)))))
(14 (resolve 12 (1) 13 (1)) ((not (= (* (e) v3) v4)) (not (= (* v5 (e)) v4)) (= (* v0 v3) (* v5 v0))))
(15 (instantiate 14 ((v0 . v3)(v3 . v0)(v4 . v1)(v5 . v2))) ((not (= (* (e) v0) v1)) (not (= (* v2 (e)) v1)) (= (* v3 v0) (* v2 v3))))
(16 (instantiate 15 ((v0 . v64)(v1 . (* v64 (e))))) ((not (= (* (e) v64) (* v64 (e)))) (not (= (* v2 (e)) (* v64 (e)))) (= (* v3 v64) (* v2 v3))))
(17 (instantiate 4 ((v0 . v64))) ((= (* (e) v64) (* v64 (e)))))
(18 (resolve 16 (1) 17 (1)) ((not (= (* v2 (e)) (* v64 (e)))) (= (* v3 v64) (* v2 v3))))
(19 (instantiate 18 ((v2 . v0)(v3 . v2)(v64 . v1))) ((not (= (* v0 (e)) (* v1 (e)))) (= (* v2 v1) (* v0 v2))))
(20 (instantiate 19 ((v1 . v0))) ((not (= (* v0 (e)) (* v0 (e)))) (= (* v2 v0) (* v0 v2))))
(21 (instantiate 1 ((v0 . (* v0 (e))))) ((= (* v0 (e)) (* v0 (e)))))
(22 (resolve 20 (1) 21 (1)) ((= (* v2 v0) (* v0 v2))))
(23 (instantiate 22 ((v0 . v1)(v2 . v0))) ((= (* v0 v1) (* v1 v0))))
(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 5 ((v0 . v64))) ((= (* v64 (* v1 v64)) v1)))
(29 (instantiate 23 ((v0 . v64)(v1 . (* v1 v64)))) ((= (* v64 (* v1 v64)) (* (* v1 v64) v64))))
(30 (paramod 28 (1 1) 29 (1 1)) ((= v1 (* (* v1 v64) v64))))
(31 (flip 30 (1)) ((= (* (* v1 v64) v64) v1)))
(32 (instantiate 31 ((v1 . v0)(v64 . v1))) ((= (* (* v0 v1) v1) v0)))
(33 (instantiate 23 ((v0 . v65)(v1 . v64))) ((= (* v65 v64) (* v64 v65))))
(34 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) v65)))
(35 (paramod 33 (1 1) 34 (1 1 2)) ((= (* v64 (* v64 v65)) v65)))
(36 (instantiate 35 ((v64 . v0)(v65 . v1))) ((= (* v0 (* v0 v1)) v1)))
(37 (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)))))
(38 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) v65)))
(39 (resolve 37 (1) 38 (1)) ((not (= (* v3 v4) v65)) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* v65 v64)))))
(40 (instantiate 39 ((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)))))
(41 (instantiate 40 ((v0 . v64)(v1 . (* v65 v64))(v2 . v65))) ((not (= (* v64 (* v65 v64)) v65)) (not (= (* v3 v4) v5)) (not (= (* v6 (* v65 v64)) v5)) (= (* v64 v4) (* v6 (* v65 v3)))))
(42 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) v65)))
(43 (resolve 41 (1) 42 (1)) ((not (= (* v3 v4) v5)) (not (= (* v6 (* v65 v64)) v5)) (= (* v64 v4) (* v6 (* v65 v3)))))
(44 (instantiate 43 ((v3 . v0)(v4 . v1)(v5 . v2)(v6 . v3)(v64 . v5)(v65 . v4))) ((not (= (* v0 v1) v2)) (not (= (* v3 (* v4 v5)) v2)) (= (* v5 v1) (* v3 (* v4 v0)))))
(45 (instantiate 44 ((v0 . v64)(v1 . (* v65 v64))(v2 . v65))) ((not (= (* v64 (* v65 v64)) v65)) (not (= (* v3 (* v4 v5)) v65)) (= (* v5 (* v65 v64)) (* v3 (* v4 v64)))))
(46 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) v65)))
(47 (resolve 45 (1) 46 (1)) ((not (= (* v3 (* v4 v5)) v65)) (= (* v5 (* v65 v64)) (* v3 (* v4 v64)))))
(48 (instantiate 47 ((v3 . v0)(v4 . v1)(v5 . v2)(v64 . v4)(v65 . v3))) ((not (= (* v0 (* v1 v2)) v3)) (= (* v2 (* v3 v4)) (* v0 (* v1 v4)))))
(49 (instantiate 48 ((v0 . (* (* v1 v2) v65))(v3 . v65))) ((not (= (* (* (* v1 v2) v65) (* v1 v2)) v65)) (= (* v2 (* v65 v4)) (* (* (* v1 v2) v65) (* v1 v4)))))
(50 (instantiate 27 ((v0 . (* v1 v2))(v1 . v65))) ((= (* (* (* v1 v2) v65) (* v1 v2)) v65)))
(51 (resolve 49 (1) 50 (1)) ((= (* v2 (* v65 v4)) (* (* (* v1 v2) v65) (* v1 v4)))))
(52 (instantiate 51 ((v1 . v3)(v2 . v0)(v4 . v2)(v65 . v1))) ((= (* v0 (* v1 v2)) (* (* (* v3 v0) v1) (* v3 v2)))))
(53 (flip 52 (1)) ((= (* (* (* v3 v0) v1) (* v3 v2)) (* v0 (* v1 v2)))))
(54 (instantiate 53 ((v0 . v1)(v1 . v2)(v2 . v3)(v3 . v0))) ((= (* (* (* v0 v1) v2) (* v0 v3)) (* v1 (* v2 v3)))))
(55 (instantiate 23 ((v0 . (A))(v1 . (B)))) ((= (* (A) (B)) (* (B) (A)))))
(56 (paramod 55 (1 1) 7 (1 1 1 1 2 1 1)) ((not (= (* (* (A) (* (* (* (B) (A)) (C)) (* (B) (e)))) (e)) (C)))))
(57 (instantiate 54 ((v0 . (B))(v1 . (A))(v2 . (C))(v3 . (e)))) ((= (* (* (* (B) (A)) (C)) (* (B) (e))) (* (A) (* (C) (e))))))
(58 (paramod 57 (1 1) 56 (1 1 1 1 2)) ((not (= (* (* (A) (* (A) (* (C) (e)))) (e)) (C)))))
(59 (instantiate 36 ((v0 . (A))(v1 . (* (C) (e))))) ((= (* (A) (* (A) (* (C) (e)))) (* (C) (e)))))
(60 (paramod 59 (1 1) 58 (1 1 1 1)) ((not (= (* (* (C) (e)) (e)) (C)))))
(61 (instantiate 32 ((v0 . (C))(v1 . (e)))) ((= (* (* (C) (e)) (e)) (C))))
(62 (paramod 61 (1 1) 60 (1 1 1)) ((not (= (C) (C)))))
(63 (instantiate 1 ((v0 . (C)))) ((= (C) (C))))
(64 (resolve 62 (1) 63 (1)) ())
)