;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:01:55 1995
;;
;;;;  -> x=x.
;;;;  -> x* ((((x*y@ )*y)@ *z)* (u@ *u))=z.
;;;; A@ *A=B@ *B -> .
;;
;; ----> UNIT CONFLICT at   0.46 sec ----> 85 [binary,84.1,1.1]  -> .
;;
(
(1 (input) ((not (= (* (@ (A)) (A)) (* (@ (B)) (B))))))
(2 (input) ((= (* v0 (* (* (@ (* (* v0 (@ v1)) v1)) v2) (* (@ v3) v3))) v2)))
(3 (instantiate 2 ((v0 . (@ (* (* v64 (@ v65)) v65))))) ((= (* (@ (* (* v64 (@ v65)) v65)) (* (* (@ (* (* (@ (* (* v64 (@ v65)) v65)) (@ v1)) v1)) v2) (* (@ v3) v3))) v2)))
(4 (instantiate 2 ((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)))))
(5 (paramod 3 (1 1) 4 (1 1 2 1)) ((= (* v64 (* v2 (* (@ v67) v67))) (* (* (@ (* (* (@ (* (* v64 (@ v65)) v65)) (@ v1)) v1)) v2) (* (@ v3) v3)))))
(6 (instantiate 5 ((v1 . v4)(v2 . v1)(v3 . v5)(v64 . v0)(v65 . v3)(v67 . v2))) ((= (* v0 (* v1 (* (@ v2) v2))) (* (* (@ (* (* (@ (* (* v0 (@ v3)) v3)) (@ v4)) v4)) v1) (* (@ v5) v5)))))
(7 (flip 6 (1)) ((= (* (* (@ (* (* (@ (* (* v0 (@ v3)) v3)) (@ v4)) v4)) v1) (* (@ v5) v5)) (* v0 (* v1 (* (@ v2) v2))))))
(8 (instantiate 7 ((v0 . v64)(v1 . v65)(v3 . v67)(v4 . v68)(v5 . v69))) ((= (* (* (@ (* (* (@ (* (* v64 (@ v67)) v67)) (@ v68)) v68)) v65) (* (@ v69) v69)) (* v64 (* v65 (* (@ v2) v2))))))
(9 (instantiate 7 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67)(v4 . v68)(v5 . v69))) ((= (* (* (@ (* (* (@ (* (* v64 (@ v67)) v67)) (@ v68)) v68)) v65) (* (@ v69) v69)) (* v64 (* v65 (* (@ v66) v66))))))
(10 (paramod 8 (1 1) 9 (1 1)) ((= (* v64 (* v65 (* (@ v2) v2))) (* v64 (* v65 (* (@ v66) v66))))))
(11 (instantiate 10 ((v64 . v0)(v65 . v1)(v66 . v3))) ((= (* v0 (* v1 (* (@ v2) v2))) (* v0 (* v1 (* (@ v3) v3))))))
(12 (instantiate 11 ((v0 . (@ (* (* v64 (@ v65)) v65))))) ((= (* (@ (* (* v64 (@ v65)) v65)) (* v1 (* (@ v2) v2))) (* (@ (* (* v64 (@ v65)) v65)) (* v1 (* (@ v3) v3))))))
(13 (instantiate 2 ((v0 . v64)(v1 . v65)(v2 . (* v1 (* (@ v2) v2)))(v3 . v67))) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) (* v1 (* (@ v2) v2))) (* (@ v67) v67))) (* v1 (* (@ v2) v2)))))
(14 (paramod 12 (1 1) 13 (1 1 2 1)) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) (* v1 (* (@ v3) v3))) (* (@ v67) v67))) (* v1 (* (@ v2) v2)))))
(15 (instantiate 2 ((v0 . v64)(v1 . v65)(v2 . (* v1 (* (@ v3) v3)))(v3 . v67))) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) (* v1 (* (@ v3) v3))) (* (@ v67) v67))) (* v1 (* (@ v3) v3)))))
(16 (paramod 15 (1 1) 14 (1 1)) ((= (* v1 (* (@ v3) v3)) (* v1 (* (@ v2) v2)))))
(17 (instantiate 16 ((v1 . v0)(v3 . v1))) ((= (* v0 (* (@ v1) v1)) (* v0 (* (@ v2) v2)))))
(18 (instantiate 17 ((v0 . (@ (* (* v64 (@ v65)) v65))))) ((= (* (@ (* (* v64 (@ v65)) v65)) (* (@ v1) v1)) (* (@ (* (* v64 (@ v65)) v65)) (* (@ v2) v2)))))
(19 (instantiate 2 ((v0 . v64)(v1 . v65)(v2 . (* (@ v1) v1))(v3 . v67))) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) (* (@ v1) v1)) (* (@ v67) v67))) (* (@ v1) v1))))
(20 (paramod 18 (1 1) 19 (1 1 2 1)) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) (* (@ v2) v2)) (* (@ v67) v67))) (* (@ v1) v1))))
(21 (instantiate 2 ((v0 . v64)(v1 . v65)(v2 . (* (@ v2) v2))(v3 . v67))) ((= (* v64 (* (* (@ (* (* v64 (@ v65)) v65)) (* (@ v2) v2)) (* (@ v67) v67))) (* (@ v2) v2))))
(22 (paramod 21 (1 1) 20 (1 1)) ((= (* (@ v2) v2) (* (@ v1) v1))))
(23 (instantiate 22 ((v2 . v0))) ((= (* (@ v0) v0) (* (@ v1) v1))))
(24 (instantiate 23 ((v0 . (A))(v1 . (B)))) ((= (* (@ (A)) (A)) (* (@ (B)) (B)))))
(25 (resolve 1 (1) 24 (1)) ())
)