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