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