;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 21:58:17 1995
;;
;;;;  -> x=x.
;;;; B*B@ =A*A@ , A* (B*B@ )=A, (A*B)*C=A* (B*C) -> .
;;;;  -> x* (x@ *y)=y.
;;;;  -> (y*x@ )*x=y.
;;;;  -> (x*y)* ((u*u@ )*z)= (x* (v@ *v))* (y*z).
;;
;; ----> UNIT CONFLICT at   0.52 sec ----> 126 [binary,125.1,121.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 v1) (* (* v2 (@ v2)) v3)) (* (* v0 (* (@ v4) v4)) (* v1 v3)))))
(6 (flip 5 (1)) ((= (* (* v0 (* (@ v4) v4)) (* v1 v3)) (* (* v0 v1) (* (* v2 (@ v2)) v3)))))
(7 (instantiate 3 ((v0 . (@ v64)))) ((= (* (@ v64) (* (@ (@ v64)) v1)) v1)))
(8 (instantiate 3 ((v0 . v64)(v1 . (* (@ (@ v64)) v1)))) ((= (* v64 (* (@ v64) (* (@ (@ v64)) v1))) (* (@ (@ v64)) v1))))
(9 (paramod 7 (1 1) 8 (1 1 2)) ((= (* v64 v1) (* (@ (@ v64)) v1))))
(10 (flip 9 (1)) ((= (* (@ (@ v64)) v1) (* v64 v1))))
(11 (instantiate 10 ((v64 . v0))) ((= (* (@ (@ v0)) v1) (* v0 v1))))
(12 (instantiate 11 ((v1 . (@ v65)))) ((= (* (@ (@ v0)) (@ v65)) (* v0 (@ v65)))))
(13 (instantiate 4 ((v0 . (@ (@ v0)))(v1 . v65))) ((= (* (* (@ (@ v0)) (@ v65)) v65) (@ (@ v0)))))
(14 (paramod 12 (1 1) 13 (1 1 1)) ((= (* (* v0 (@ v65)) v65) (@ (@ v0)))))
(15 (instantiate 4 ((v0 . v0)(v1 . v65))) ((= (* (* v0 (@ v65)) v65) v0)))
(16 (paramod 15 (1 1) 14 (1 1)) ((= v0 (@ (@ v0)))))
(17 (flip 16 (1)) ((= (@ (@ v0)) v0)))
(18 (instantiate 11 ((v1 . v65))) ((= (* (@ (@ v0)) v65) (* v0 v65))))
(19 (instantiate 3 ((v0 . (@ v0))(v1 . v65))) ((= (* (@ v0) (* (@ (@ v0)) v65)) v65)))
(20 (paramod 18 (1 1) 19 (1 1 2)) ((= (* (@ v0) (* v0 v65)) v65)))
(21 (instantiate 20 ((v65 . v1))) ((= (* (@ v0) (* v0 v1)) v1)))
(22 (instantiate 4 ((v0 . v64)(v1 . (@ v0)))) ((= (* (* v64 (@ (@ v0))) (@ v0)) v64)))
(23 (paramod 17 (1 1) 22 (1 1 1 2)) ((= (* (* v64 v0) (@ v0)) v64)))
(24 (instantiate 23 ((v0 . v1)(v64 . v0))) ((= (* (* v0 v1) (@ v1)) v0)))
(25 (instantiate 4 ((v0 . v67)(v1 . v67))) ((= (* (* v67 (@ v67)) v67) v67)))
(26 (instantiate 5 ((v0 . v64)(v1 . v65)(v2 . v67)(v3 . v67)(v4 . v68))) ((= (* (* v64 v65) (* (* v67 (@ v67)) v67)) (* (* v64 (* (@ v68) v68)) (* v65 v67)))))
(27 (paramod 25 (1 1) 26 (1 1 2)) ((= (* (* v64 v65) v67) (* (* v64 (* (@ v68) v68)) (* v65 v67)))))
(28 (instantiate 27 ((v64 . v0)(v65 . v1)(v67 . v2)(v68 . v3))) ((= (* (* v0 v1) v2) (* (* v0 (* (@ v3) v3)) (* v1 v2)))))
(29 (flip 28 (1)) ((= (* (* v0 (* (@ v3) v3)) (* v1 v2)) (* (* v0 v1) v2))))
(30 (instantiate 24 ((v0 . (@ v0))(v1 . (* v0 v1)))) ((= (* (* (@ v0) (* v0 v1)) (@ (* v0 v1))) (@ v0))))
(31 (paramod 21 (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 24 (1 1) 33 (1 1 2 1)) ((= (* (@ v1) (@ v0)) (@ (* v0 v1)))))
(35 (flip 34 (1)) ((= (@ (* v0 v1)) (* (@ v1) (@ v0)))))
(36 (instantiate 24 ((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 38 ((v0 . v64)(v1 . (* v0 v1))(v2 . v66))) ((= (* (* v64 (* (* v0 v1) v66)) (* (@ v66) (@ (* v0 v1)))) v64)))
(40 (paramod 35 (1 1) 39 (1 1 2 2)) ((= (* (* v64 (* (* v0 v1) v66)) (* (@ v66) (* (@ v1) (@ v0)))) v64)))
(41 (instantiate 40 ((v0 . v1)(v1 . v2)(v64 . v0)(v66 . v3))) ((= (* (* v0 (* (* v1 v2) v3)) (* (@ v3) (* (@ v2) (@ v1)))) v0)))
(42 (instantiate 21 ((v0 . (@ v68))(v1 . v68))) ((= (* (@ (@ v68)) (* (@ v68) v68)) v68)))
(43 (instantiate 6 ((v0 . (@ (@ v68)))(v1 . v65)(v2 . v66)(v3 . v67)(v4 . v68))) ((= (* (* (@ (@ v68)) (* (@ v68) v68)) (* v65 v67)) (* (* (@ (@ v68)) v65) (* (* v66 (@ v66)) v67)))))
(44 (paramod 42 (1 1) 43 (1 1 1)) ((= (* v68 (* v65 v67)) (* (* (@ (@ v68)) v65) (* (* v66 (@ v66)) v67)))))
(45 (instantiate 17 ((v0 . v68))) ((= (@ (@ v68)) v68)))
(46 (paramod 45 (1 1) 44 (1 2 1 1)) ((= (* v68 (* v65 v67)) (* (* v68 v65) (* (* v66 (@ v66)) v67)))))
(47 (flip 46 (1)) ((= (* (* v68 v65) (* (* v66 (@ v66)) v67)) (* v68 (* v65 v67)))))
(48 (instantiate 47 ((v65 . v1)(v66 . v2)(v67 . v3)(v68 . v0))) ((= (* (* v0 v1) (* (* v2 (@ v2)) v3)) (* v0 (* v1 v3)))))
(49 (instantiate 38 ((v0 . v64)(v1 . (@ v68))(v2 . v68))) ((= (* (* v64 (* (@ v68) v68)) (* (@ v68) (@ (@ v68)))) v64)))
(50 (instantiate 6 ((v0 . v64)(v1 . (@ v68))(v2 . v66)(v3 . (@ (@ v68)))(v4 . v68))) ((= (* (* v64 (* (@ v68) v68)) (* (@ v68) (@ (@ v68)))) (* (* v64 (@ v68)) (* (* v66 (@ v66)) (@ (@ v68)))))))
(51 (paramod 49 (1 1) 50 (1 1)) ((= v64 (* (* v64 (@ v68)) (* (* v66 (@ v66)) (@ (@ v68)))))))
(52 (instantiate 17 ((v0 . v68))) ((= (@ (@ v68)) v68)))
(53 (paramod 52 (1 1) 51 (1 2 2 2)) ((= v64 (* (* v64 (@ v68)) (* (* v66 (@ v66)) v68)))))
(54 (instantiate 48 ((v0 . v64)(v1 . (@ v68))(v2 . v66)(v3 . v68))) ((= (* (* v64 (@ v68)) (* (* v66 (@ v66)) v68)) (* v64 (* (@ v68) v68)))))
(55 (paramod 54 (1 1) 53 (1 2)) ((= v64 (* v64 (* (@ v68) v68)))))
(56 (flip 55 (1)) ((= (* v64 (* (@ v68) v68)) v64)))
(57 (instantiate 56 ((v64 . v0)(v68 . v1))) ((= (* v0 (* (@ v1) v1)) v0)))
(58 (instantiate 57 ((v0 . v0)(v1 . v3))) ((= (* v0 (* (@ v3) v3)) v0)))
(59 (paramod 58 (1 1) 29 (1 1 1)) ((= (* v0 (* v1 v2)) (* (* v0 v1) v2))))
(60 (flip 59 (1)) ((= (* (* v0 v1) v2) (* v0 (* v1 v2)))))
(61 (instantiate 60 ((v0 . v1)(v1 . v2)(v2 . v3))) ((= (* (* v1 v2) v3) (* v1 (* v2 v3)))))
(62 (paramod 61 (1 1) 41 (1 1 1 2)) ((= (* (* v0 (* v1 (* v2 v3))) (* (@ v3) (* (@ v2) (@ v1)))) v0)))
(63 (instantiate 60 ((v0 . v0)(v1 . (* v1 (* v2 v3)))(v2 . (* (@ v3) (* (@ v2) (@ v1)))))) ((= (* (* v0 (* v1 (* v2 v3))) (* (@ v3) (* (@ v2) (@ v1)))) (* v0 (* (* v1 (* v2 v3)) (* (@ v3) (* (@ v2) (@ v1))))))))
(64 (paramod 63 (1 1) 62 (1 1)) ((= (* v0 (* (* v1 (* v2 v3)) (* (@ v3) (* (@ v2) (@ v1))))) v0)))
(65 (instantiate 60 ((v0 . v1)(v1 . (* v2 v3))(v2 . (* (@ v3) (* (@ v2) (@ v1)))))) ((= (* (* v1 (* v2 v3)) (* (@ v3) (* (@ v2) (@ v1)))) (* v1 (* (* v2 v3) (* (@ v3) (* (@ v2) (@ v1))))))))
(66 (paramod 65 (1 1) 64 (1 1 2)) ((= (* v0 (* v1 (* (* v2 v3) (* (@ v3) (* (@ v2) (@ v1)))))) v0)))
(67 (instantiate 60 ((v0 . v2)(v1 . v3)(v2 . (* (@ v3) (* (@ v2) (@ v1)))))) ((= (* (* v2 v3) (* (@ v3) (* (@ v2) (@ v1)))) (* v2 (* v3 (* (@ v3) (* (@ v2) (@ v1))))))))
(68 (paramod 67 (1 1) 66 (1 1 2 2)) ((= (* v0 (* v1 (* v2 (* v3 (* (@ v3) (* (@ v2) (@ v1))))))) v0)))
(69 (instantiate 3 ((v0 . v3)(v1 . (* (@ v2) (@ v1))))) ((= (* v3 (* (@ v3) (* (@ v2) (@ v1)))) (* (@ v2) (@ v1)))))
(70 (paramod 69 (1 1) 68 (1 1 2 2 2)) ((= (* v0 (* v1 (* v2 (* (@ v2) (@ v1))))) v0)))
(71 (instantiate 3 ((v0 . v2)(v1 . (@ v1)))) ((= (* v2 (* (@ v2) (@ v1))) (@ v1))))
(72 (paramod 71 (1 1) 70 (1 1 2 2)) ((= (* v0 (* v1 (@ v1))) v0)))
(73 (instantiate 72 ((v0 . (A))(v1 . (B)))) ((= (* (A) (* (B) (@ (B)))) (A))))
(74 (paramod 73 (1 1) 2 (2 1 1)) ((not (= (* (B) (@ (B))) (* (A) (@ (A))))) (not (= (A) (A))) (not (= (* (* (A) (B)) (C)) (* (A) (* (B) (C)))))))
(75 (instantiate 60 ((v0 . (A))(v1 . (B))(v2 . (C)))) ((= (* (* (A) (B)) (C)) (* (A) (* (B) (C))))))
(76 (paramod 75 (1 1) 74 (3 1 1)) ((not (= (* (B) (@ (B))) (* (A) (@ (A))))) (not (= (A) (A))) (not (= (* (A) (* (B) (C))) (* (A) (* (B) (C)))))))
(77 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(78 (resolve 76 (2) 77 (1)) ((not (= (* (B) (@ (B))) (* (A) (@ (A))))) (not (= (* (A) (* (B) (C))) (* (A) (* (B) (C)))))))
(79 (instantiate 1 ((v0 . (* (A) (* (B) (C)))))) ((= (* (A) (* (B) (C))) (* (A) (* (B) (C))))))
(80 (resolve 78 (2) 79 (1)) ((not (= (* (B) (@ (B))) (* (A) (@ (A)))))))
(81 (instantiate 72 ((v0 . (@ v64)))) ((= (* (@ v64) (* v1 (@ v1))) (@ v64))))
(82 (instantiate 3 ((v0 . v64)(v1 . (* v1 (@ v1))))) ((= (* v64 (* (@ v64) (* v1 (@ v1)))) (* v1 (@ v1)))))
(83 (paramod 81 (1 1) 82 (1 1 2)) ((= (* v64 (@ v64)) (* v1 (@ v1)))))
(84 (instantiate 83 ((v64 . v0))) ((= (* v0 (@ v0)) (* v1 (@ v1)))))
(85 (instantiate 84 ((v0 . (B))(v1 . (A)))) ((= (* (B) (@ (B))) (* (A) (@ (A))))))
(86 (resolve 80 (1) 85 (1)) ())
)