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