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