;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:02:16 1995
;;
;;;;  -> x=x.
;;;;  -> beta=alpha.
;;;;  -> x* ((((x*y@ )*y)@ *z)* ((alpha*u)@ * (beta*u)))=z.
;;;; A@ *A=B@ *B -> .
;;
;; ----> UNIT CONFLICT at   1.28 sec ----> 175 [binary,174.1,1.1]  -> .
;;
(
(1 (input) ((not (= (* (@ (A)) (A)) (* (@ (B)) (B))))))
(2 (input) ((= (beta) (alpha))))
(3 (input) ((= (* v0 (* (* (@ (* (* v0 (@ v1)) v1)) v2) (* (@ (* (alpha) v3)) (* (beta) v3)))) v2)))
(4 (paramod 2 (1 1) 3 (1 1 2 2 2 1)) ((= (* v0 (* (* (@ (* (* v0 (@ v1)) v1)) v2) (* (@ (* (alpha) v3)) (* (alpha) v3)))) v2)))
(5 (instantiate 4 ((v0 . (alpha)))) ((= (* (alpha) (* (* (@ (* (* (alpha) (@ v1)) v1)) v2) (* (@ (* (alpha) v3)) (* (alpha) v3)))) v2)))
(6 (instantiate 4 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . (* (* (@ (* (* (alpha) (@ v1)) v1)) v2) (* (@ (* (alpha) v3)) (* (alpha) v3)))))) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) v66) (* (@ (* (alpha) (* (* (@ (* (* (alpha) (@ v1)) v1)) v2) (* (@ (* (alpha) v3)) (* (alpha) v3))))) (* (alpha) (* (* (@ (* (* (alpha) (@ v1)) v1)) v2) (* (@ (* (alpha) v3)) (* (alpha) v3))))))) v66)))
(7 (paramod 5 (1 1) 6 (1 1 2 2 1 1)) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) v66) (* (@ v2) (* (alpha) (* (* (@ (* (* (alpha) (@ v1)) v1)) v2) (* (@ (* (alpha) v3)) (* (alpha) v3))))))) v66)))
(8 (instantiate 4 ((v0 . (alpha))(v1 . v1)(v2 . v2)(v3 . v3))) ((= (* (alpha) (* (* (@ (* (* (alpha) (@ v1)) v1)) v2) (* (@ (* (alpha) v3)) (* (alpha) v3)))) v2)))
(9 (paramod 8 (1 1) 7 (1 1 2 2 2)) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) v66) (* (@ v2) v2))) v66)))
(10 (instantiate 9 ((v2 . v3)(v64 . v0)(v65 . v1)(v66 . v2))) ((= (* v0 (* (* (@ (* (* v0 (@ v1)) v1)) v2) (* (@ v3) v3))) v2)))
(11 (instantiate 10 ((v0 . (@ (* (* v64 (@ v65)) v65))))) ((= (* (@ (* (* v64 (@ v65)) v65)) (* (* (@ (* (* (@ (* (* v64 (@ v65)) v65)) (@ v1)) v1)) v2) (* (@ v3) v3))) v2)))
(12 (instantiate 10 ((v0 . v64)(v1 . v65)(v2 . (* (* (@ (* (* (@ (* (* v64 (@ v65)) v65)) (@ v1)) v1)) v2) (* (@ v3) v3)))(v3 . v67))) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) (* (* (@ (* (* (@ (* (* v64 (@ v65)) v65)) (@ v1)) v1)) v2) (* (@ v3) v3))) (* (@ v67) v67))) (* (* (@ (* (* (@ (* (* v64 (@ v65)) v65)) (@ v1)) v1)) v2) (* (@ v3) v3)))))
(13 (paramod 11 (1 1) 12 (1 1 2 1)) ((= (* v64 (* v2 (* (@ v67) v67))) (* (* (@ (* (* (@ (* (* v64 (@ v65)) v65)) (@ v1)) v1)) v2) (* (@ v3) v3)))))
(14 (instantiate 13 ((v1 . v4)(v2 . v1)(v3 . v5)(v64 . v0)(v65 . v3)(v67 . v2))) ((= (* v0 (* v1 (* (@ v2) v2))) (* (* (@ (* (* (@ (* (* v0 (@ v3)) v3)) (@ v4)) v4)) v1) (* (@ v5) v5)))))
(15 (flip 14 (1)) ((= (* (* (@ (* (* (@ (* (* v0 (@ v3)) v3)) (@ v4)) v4)) v1) (* (@ v5) v5)) (* v0 (* v1 (* (@ v2) v2))))))
(16 (instantiate 15 ((v0 . v64)(v1 . v65)(v3 . v67)(v4 . v68)(v5 . v69))) ((= (* (* (@ (* (* (@ (* (* v64 (@ v67)) v67)) (@ v68)) v68)) v65) (* (@ v69) v69)) (* v64 (* v65 (* (@ v2) v2))))))
(17 (instantiate 15 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67)(v4 . v68)(v5 . v69))) ((= (* (* (@ (* (* (@ (* (* v64 (@ v67)) v67)) (@ v68)) v68)) v65) (* (@ v69) v69)) (* v64 (* v65 (* (@ v66) v66))))))
(18 (paramod 16 (1 1) 17 (1 1)) ((= (* v64 (* v65 (* (@ v2) v2))) (* v64 (* v65 (* (@ v66) v66))))))
(19 (instantiate 18 ((v64 . v0)(v65 . v1)(v66 . v3))) ((= (* v0 (* v1 (* (@ v2) v2))) (* v0 (* v1 (* (@ v3) v3))))))
(20 (instantiate 19 ((v0 . (@ (* (* v64 (@ v65)) v65))))) ((= (* (@ (* (* v64 (@ v65)) v65)) (* v1 (* (@ v2) v2))) (* (@ (* (* v64 (@ v65)) v65)) (* v1 (* (@ v3) v3))))))
(21 (instantiate 10 ((v0 . v64)(v1 . v65)(v2 . (* v1 (* (@ v2) v2)))(v3 . v67))) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) (* v1 (* (@ v2) v2))) (* (@ v67) v67))) (* v1 (* (@ v2) v2)))))
(22 (paramod 20 (1 1) 21 (1 1 2 1)) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) (* v1 (* (@ v3) v3))) (* (@ v67) v67))) (* v1 (* (@ v2) v2)))))
(23 (instantiate 10 ((v0 . v64)(v1 . v65)(v2 . (* v1 (* (@ v3) v3)))(v3 . v67))) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) (* v1 (* (@ v3) v3))) (* (@ v67) v67))) (* v1 (* (@ v3) v3)))))
(24 (paramod 23 (1 1) 22 (1 1)) ((= (* v1 (* (@ v3) v3)) (* v1 (* (@ v2) v2)))))
(25 (instantiate 24 ((v1 . v0)(v3 . v1))) ((= (* v0 (* (@ v1) v1)) (* v0 (* (@ v2) v2)))))
(26 (instantiate 25 ((v0 . (@ (* (* v64 (@ v65)) v65))))) ((= (* (@ (* (* v64 (@ v65)) v65)) (* (@ v1) v1)) (* (@ (* (* v64 (@ v65)) v65)) (* (@ v2) v2)))))
(27 (instantiate 10 ((v0 . v64)(v1 . v65)(v2 . (* (@ v1) v1))(v3 . v67))) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) (* (@ v1) v1)) (* (@ v67) v67))) (* (@ v1) v1))))
(28 (paramod 26 (1 1) 27 (1 1 2 1)) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) (* (@ v2) v2)) (* (@ v67) v67))) (* (@ v1) v1))))
(29 (instantiate 10 ((v0 . v64)(v1 . v65)(v2 . (* (@ v2) v2))(v3 . v67))) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) (* (@ v2) v2)) (* (@ v67) v67))) (* (@ v2) v2))))
(30 (paramod 29 (1 1) 28 (1 1)) ((= (* (@ v2) v2) (* (@ v1) v1))))
(31 (instantiate 30 ((v2 . v0))) ((= (* (@ v0) v0) (* (@ v1) v1))))
(32 (instantiate 31 ((v0 . (A))(v1 . (B)))) ((= (* (@ (A)) (A)) (* (@ (B)) (B)))))
(33 (resolve 1 (1) 32 (1)) ())
)