;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:02:18 1995
;;
;;;;  -> x=x.
;;;; A* ((((A*B@ )*B)@ *C)* ((alpha*D)@ * (beta*D)))=C -> .
;;;;  -> beta=alpha.
;;;;  -> x@ *x=y@ *y.
;;;;  -> x@ * (x*y)=y.
;;;;  -> (x*y)*y@ =x.
;;
;; ----> UNIT CONFLICT at   0.12 sec ----> 43 [binary,41.1,32.1]  -> .
;;
(
(1 (input) ((not (= (* (A) (* (* (@ (* (* (A) (@ (B))) (B))) (C)) (* (@ (* (alpha) (D))) (* (beta) (D))))) (C)))))
(2 (input) ((= (beta) (alpha))))
(3 (input) ((= (* (@ v0) v0) (* (@ v1) v1))))
(4 (input) ((= (* (@ v0) (* v0 v1)) v1)))
(5 (input) ((= (* (* v0 v1) (@ v1)) v0)))
(6 (paramod 2 (1 1) 1 (1 1 1 2 2 2 1)) ((not (= (* (A) (* (* (@ (* (* (A) (@ (B))) (B))) (C)) (* (@ (* (alpha) (D))) (* (alpha) (D))))) (C)))))
(7 (instantiate 4 ((v0 . (@ v0))(v1 . (* v0 v1)))) ((= (* (@ (@ v0)) (* (@ v0) (* v0 v1))) (* v0 v1))))
(8 (paramod 4 (1 1) 7 (1 1 2)) ((= (* (@ (@ v0)) v1) (* v0 v1))))
(9 (instantiate 5 ((v0 . (@ v0))(v1 . (* v0 v1)))) ((= (* (* (@ v0) (* v0 v1)) (@ (* v0 v1))) (@ v0))))
(10 (paramod 4 (1 1) 9 (1 1 1)) ((= (* v1 (@ (* v0 v1))) (@ v0))))
(11 (instantiate 10 ((v0 . v1)(v1 . v0))) ((= (* v0 (@ (* v1 v0))) (@ v1))))
(12 (instantiate 3 ((v0 . v65))) ((= (* (@ v65) v65) (* (@ v1) v1))))
(13 (instantiate 4 ((v0 . (@ v65))(v1 . v65))) ((= (* (@ (@ v65)) (* (@ v65) v65)) v65)))
(14 (paramod 12 (1 1) 13 (1 1 2)) ((= (* (@ (@ v65)) (* (@ v1) v1)) v65)))
(15 (instantiate 8 ((v0 . v65)(v1 . (* (@ v1) v1)))) ((= (* (@ (@ v65)) (* (@ v1) v1)) (* v65 (* (@ v1) v1)))))
(16 (paramod 15 (1 1) 14 (1 1)) ((= (* v65 (* (@ v1) v1)) v65)))
(17 (instantiate 16 ((v65 . v0))) ((= (* v0 (* (@ v1) v1)) v0)))
(18 (instantiate 17 ((v0 . (* (@ (* (* (A) (@ (B))) (B))) (C)))(v1 . (* (alpha) (D))))) ((= (* (* (@ (* (* (A) (@ (B))) (B))) (C)) (* (@ (* (alpha) (D))) (* (alpha) (D)))) (* (@ (* (* (A) (@ (B))) (B))) (C)))))
(19 (paramod 18 (1 1) 6 (1 1 1 2)) ((not (= (* (A) (* (@ (* (* (A) (@ (B))) (B))) (C))) (C)))))
(20 (instantiate 4 ((v0 . (@ v65))(v1 . v65))) ((= (* (@ (@ v65)) (* (@ v65) v65)) v65)))
(21 (instantiate 17 ((v0 . (@ (@ v65)))(v1 . v65))) ((= (* (@ (@ v65)) (* (@ v65) v65)) (@ (@ v65)))))
(22 (paramod 20 (1 1) 21 (1 1)) ((= v65 (@ (@ v65)))))
(23 (flip 22 (1)) ((= (@ (@ v65)) v65)))
(24 (instantiate 23 ((v65 . v0))) ((= (@ (@ v0)) v0)))
(25 (instantiate 11 ((v0 . (@ v1))(v1 . (* v0 v1)))) ((= (* (@ v1) (@ (* (* v0 v1) (@ v1)))) (@ (* v0 v1)))))
(26 (paramod 5 (1 1) 25 (1 1 2 1)) ((= (* (@ v1) (@ v0)) (@ (* v0 v1)))))
(27 (flip 26 (1)) ((= (@ (* v0 v1)) (* (@ v1) (@ v0)))))
(28 (instantiate 27 ((v0 . (* (A) (@ (B))))(v1 . (B)))) ((= (@ (* (* (A) (@ (B))) (B))) (* (@ (B)) (@ (* (A) (@ (B))))))))
(29 (paramod 28 (1 1) 19 (1 1 1 2 1)) ((not (= (* (A) (* (* (@ (B)) (@ (* (A) (@ (B))))) (C))) (C)))))
(30 (instantiate 27 ((v0 . (A))(v1 . (@ (B))))) ((= (@ (* (A) (@ (B)))) (* (@ (@ (B))) (@ (A))))))
(31 (paramod 30 (1 1) 29 (1 1 1 2 1 2)) ((not (= (* (A) (* (* (@ (B)) (* (@ (@ (B))) (@ (A)))) (C))) (C)))))
(32 (instantiate 24 ((v0 . (B)))) ((= (@ (@ (B))) (B))))
(33 (paramod 32 (1 1) 31 (1 1 1 2 1 2 1)) ((not (= (* (A) (* (* (@ (B)) (* (B) (@ (A)))) (C))) (C)))))
(34 (instantiate 4 ((v0 . (B))(v1 . (@ (A))))) ((= (* (@ (B)) (* (B) (@ (A)))) (@ (A)))))
(35 (paramod 34 (1 1) 33 (1 1 1 2 1)) ((not (= (* (A) (* (@ (A)) (C))) (C)))))
(36 (instantiate 4 ((v0 . (@ v0))(v1 . v65))) ((= (* (@ (@ v0)) (* (@ v0) v65)) v65)))
(37 (paramod 24 (1 1) 36 (1 1 1)) ((= (* v0 (* (@ v0) v65)) v65)))
(38 (instantiate 37 ((v65 . v1))) ((= (* v0 (* (@ v0) v1)) v1)))
(39 (instantiate 38 ((v0 . (A))(v1 . (C)))) ((= (* (A) (* (@ (A)) (C))) (C))))
(40 (resolve 35 (1) 39 (1)) ())
)