;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 21:57:51 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@ *x=y*y@ .
;;;;  -> ((x* (alpha*y))*beta)*z=x* (alpha* ((y*beta)*z)).
;;
;; ----> UNIT CONFLICT at   3.38 sec ----> 565 [binary,563.1,20.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) v0) (* v1 (@ v1)))))
(6 (input) ((= (* (* (* v0 (* (alpha) v1)) (beta)) v2) (* v0 (* (alpha) (* (* v1 (beta)) v2))))))
(7 (instantiate 5 ((v0 . v64))) ((= (* (@ v64) v64) (* v1 (@ v1)))))
(8 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (* (@ v64) v64) (* v65 (@ v65)))))
(9 (paramod 7 (1 1) 8 (1 1)) ((= (* v1 (@ v1)) (* v65 (@ v65)))))
(10 (instantiate 9 ((v1 . v0)(v65 . v1))) ((= (* v0 (@ v0)) (* v1 (@ v1)))))
(11 (instantiate 5 ((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 1)) ((= (* (* v1 (@ v1)) v65) (@ (@ v65)))))
(14 (instantiate 13 ((v1 . v0)(v65 . v1))) ((= (* (* v0 (@ v0)) v1) (@ (@ v1)))))
(15 (instantiate 5 ((v0 . v65))) ((= (* (@ v65) v65) (* v1 (@ v1)))))
(16 (instantiate 3 ((v0 . v65)(v1 . v65))) ((= (* v65 (* (@ v65) v65)) v65)))
(17 (paramod 15 (1 1) 16 (1 1 2)) ((= (* v65 (* v1 (@ v1))) v65)))
(18 (instantiate 17 ((v65 . v0))) ((= (* v0 (* v1 (@ v1))) v0)))
(19 (flip 14 (1)) ((= (@ (@ v1)) (* (* v0 (@ v0)) v1))))
(20 (instantiate 18 ((v0 . (A))(v1 . (B)))) ((= (* (A) (* (B) (@ (B)))) (A))))
(21 (paramod 20 (1 1) 2 (2 1 1)) ((not (= (* (B) (@ (B))) (* (A) (@ (A))))) (not (= (A) (A))) (not (= (* (* (A) (B)) (C)) (* (A) (* (B) (C)))))))
(22 (instantiate 10 ((v0 . (B))(v1 . (A)))) ((= (* (B) (@ (B))) (* (A) (@ (A))))))
(23 (resolve 21 (1) 22 (1)) ((not (= (A) (A))) (not (= (* (* (A) (B)) (C)) (* (A) (* (B) (C)))))))
(24 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(25 (resolve 23 (1) 24 (1)) ((not (= (* (* (A) (B)) (C)) (* (A) (* (B) (C)))))))
(26 (instantiate 3 ((v0 . v64)(v1 . (@ (@ v64))))) ((= (* v64 (* (@ v64) (@ (@ v64)))) (@ (@ v64)))))
(27 (instantiate 18 ((v0 . v64)(v1 . (@ v64)))) ((= (* v64 (* (@ v64) (@ (@ v64)))) v64)))
(28 (paramod 26 (1 1) 27 (1 1)) ((= (@ (@ v64)) v64)))
(29 (instantiate 28 ((v64 . v0))) ((= (@ (@ v0)) v0)))
(30 (instantiate 29 ((v0 . v1))) ((= (@ (@ v1)) v1)))
(31 (paramod 30 (1 1) 19 (1 1)) ((= v1 (* (* v0 (@ v0)) v1))))
(32 (flip 31 (1)) ((= (* (* v0 (@ v0)) v1) v1)))
(33 (instantiate 4 ((v0 . v64)(v1 . (@ v0)))) ((= (* (* v64 (@ (@ v0))) (@ v0)) v64)))
(34 (paramod 29 (1 1) 33 (1 1 1 2)) ((= (* (* v64 v0) (@ v0)) v64)))
(35 (instantiate 34 ((v0 . v1)(v64 . v0))) ((= (* (* v0 v1) (@ v1)) v0)))
(36 (instantiate 3 ((v0 . (@ v0))(v1 . v65))) ((= (* (@ v0) (* (@ (@ v0)) v65)) v65)))
(37 (paramod 29 (1 1) 36 (1 1 2 1)) ((= (* (@ v0) (* v0 v65)) v65)))
(38 (instantiate 37 ((v65 . v1))) ((= (* (@ v0) (* v0 v1)) v1)))
(39 (instantiate 3 ((v0 . (alpha)))) ((= (* (alpha) (* (@ (alpha)) v1)) v1)))
(40 (instantiate 6 ((v0 . v64)(v1 . (* (@ (alpha)) v1))(v2 . v66))) ((= (* (* (* v64 (* (alpha) (* (@ (alpha)) v1))) (beta)) v66) (* v64 (* (alpha) (* (* (* (@ (alpha)) v1) (beta)) v66))))))
(41 (paramod 39 (1 1) 40 (1 1 1 1 2)) ((= (* (* (* v64 v1) (beta)) v66) (* v64 (* (alpha) (* (* (* (@ (alpha)) v1) (beta)) v66))))))
(42 (instantiate 41 ((v64 . v0)(v66 . v2))) ((= (* (* (* v0 v1) (beta)) v2) (* v0 (* (alpha) (* (* (* (@ (alpha)) v1) (beta)) v2))))))
(43 (instantiate 18 ((v0 . v64)(v1 . (alpha)))) ((= (* v64 (* (alpha) (@ (alpha)))) v64)))
(44 (instantiate 6 ((v0 . v64)(v1 . (@ (alpha)))(v2 . v66))) ((= (* (* (* v64 (* (alpha) (@ (alpha)))) (beta)) v66) (* v64 (* (alpha) (* (* (@ (alpha)) (beta)) v66))))))
(45 (paramod 43 (1 1) 44 (1 1 1 1)) ((= (* (* v64 (beta)) v66) (* v64 (* (alpha) (* (* (@ (alpha)) (beta)) v66))))))
(46 (instantiate 45 ((v64 . v0)(v66 . v1))) ((= (* (* v0 (beta)) v1) (* v0 (* (alpha) (* (* (@ (alpha)) (beta)) v1))))))
(47 (flip 46 (1)) ((= (* v0 (* (alpha) (* (* (@ (alpha)) (beta)) v1))) (* (* v0 (beta)) v1))))
(48 (instantiate 32 ((v0 . (@ v0))(v1 . v65))) ((= (* (* (@ v0) (@ (@ v0))) v65) v65)))
(49 (paramod 29 (1 1) 48 (1 1 1 2)) ((= (* (* (@ v0) v0) v65) v65)))
(50 (instantiate 49 ((v65 . v1))) ((= (* (* (@ v0) v0) v1) v1)))
(51 (instantiate 38 ((v0 . (* v0 v1))(v1 . (@ v1)))) ((= (* (@ (* v0 v1)) (* (* v0 v1) (@ v1))) (@ v1))))
(52 (paramod 35 (1 1) 51 (1 1 2)) ((= (* (@ (* v0 v1)) v0) (@ v1))))
(53 (instantiate 52 ((v0 . (@ v0))(v1 . (* v0 v1)))) ((= (* (@ (* (@ v0) (* v0 v1))) (@ v0)) (@ (* v0 v1)))))
(54 (paramod 38 (1 1) 53 (1 1 1 1)) ((= (* (@ v1) (@ v0)) (@ (* v0 v1)))))
(55 (flip 54 (1)) ((= (@ (* v0 v1)) (* (@ v1) (@ v0)))))
(56 (instantiate 38 ((v0 . (* v0 v1))(v1 . v65))) ((= (* (@ (* v0 v1)) (* (* v0 v1) v65)) v65)))
(57 (paramod 55 (1 1) 56 (1 1 1)) ((= (* (* (@ v1) (@ v0)) (* (* v0 v1) v65)) v65)))
(58 (instantiate 57 ((v0 . v1)(v1 . v0)(v65 . v2))) ((= (* (* (@ v0) (@ v1)) (* (* v1 v0) v2)) v2)))
(59 (instantiate 50 ((v1 . v65))) ((= (* (* (@ v0) v0) v65) v65)))
(60 (instantiate 42 ((v0 . (* (@ v0) v0))(v1 . v65)(v2 . v66))) ((= (* (* (* (* (@ v0) v0) v65) (beta)) v66) (* (* (@ v0) v0) (* (alpha) (* (* (* (@ (alpha)) v65) (beta)) v66))))))
(61 (paramod 59 (1 1) 60 (1 1 1 1)) ((= (* (* v65 (beta)) v66) (* (* (@ v0) v0) (* (alpha) (* (* (* (@ (alpha)) v65) (beta)) v66))))))
(62 (instantiate 50 ((v0 . v0)(v1 . (* (alpha) (* (* (* (@ (alpha)) v65) (beta)) v66))))) ((= (* (* (@ v0) v0) (* (alpha) (* (* (* (@ (alpha)) v65) (beta)) v66))) (* (alpha) (* (* (* (@ (alpha)) v65) (beta)) v66)))))
(63 (paramod 62 (1 1) 61 (1 2)) ((= (* (* v65 (beta)) v66) (* (alpha) (* (* (* (@ (alpha)) v65) (beta)) v66)))))
(64 (flip 63 (1)) ((= (* (alpha) (* (* (* (@ (alpha)) v65) (beta)) v66)) (* (* v65 (beta)) v66))))
(65 (instantiate 64 ((v65 . v0)(v66 . v1))) ((= (* (alpha) (* (* (* (@ (alpha)) v0) (beta)) v1)) (* (* v0 (beta)) v1))))
(66 (instantiate 10 ((v0 . v64))) ((= (* v64 (@ v64)) (* v1 (@ v1)))))
(67 (instantiate 42 ((v0 . v64)(v1 . (@ v64))(v2 . v66))) ((= (* (* (* v64 (@ v64)) (beta)) v66) (* v64 (* (alpha) (* (* (* (@ (alpha)) (@ v64)) (beta)) v66))))))
(68 (paramod 66 (1 1) 67 (1 1 1 1)) ((= (* (* (* v1 (@ v1)) (beta)) v66) (* v64 (* (alpha) (* (* (* (@ (alpha)) (@ v64)) (beta)) v66))))))
(69 (instantiate 32 ((v0 . v1)(v1 . (beta)))) ((= (* (* v1 (@ v1)) (beta)) (beta))))
(70 (paramod 69 (1 1) 68 (1 1 1)) ((= (* (beta) v66) (* v64 (* (alpha) (* (* (* (@ (alpha)) (@ v64)) (beta)) v66))))))
(71 (instantiate 65 ((v0 . (@ v64))(v1 . v66))) ((= (* (alpha) (* (* (* (@ (alpha)) (@ v64)) (beta)) v66)) (* (* (@ v64) (beta)) v66))))
(72 (paramod 71 (1 1) 70 (1 2 2)) ((= (* (beta) v66) (* v64 (* (* (@ v64) (beta)) v66)))))
(73 (flip 72 (1)) ((= (* v64 (* (* (@ v64) (beta)) v66)) (* (beta) v66))))
(74 (instantiate 73 ((v64 . v0)(v66 . v1))) ((= (* v0 (* (* (@ v0) (beta)) v1)) (* (beta) v1))))
(75 (instantiate 3 ((v0 . v64))) ((= (* v64 (* (@ v64) v1)) v1)))
(76 (instantiate 42 ((v0 . v64)(v1 . (* (@ v64) v1))(v2 . v66))) ((= (* (* (* v64 (* (@ v64) v1)) (beta)) v66) (* v64 (* (alpha) (* (* (* (@ (alpha)) (* (@ v64) v1)) (beta)) v66))))))
(77 (paramod 75 (1 1) 76 (1 1 1 1)) ((= (* (* v1 (beta)) v66) (* v64 (* (alpha) (* (* (* (@ (alpha)) (* (@ v64) v1)) (beta)) v66))))))
(78 (instantiate 65 ((v0 . (* (@ v64) v1))(v1 . v66))) ((= (* (alpha) (* (* (* (@ (alpha)) (* (@ v64) v1)) (beta)) v66)) (* (* (* (@ v64) v1) (beta)) v66))))
(79 (paramod 78 (1 1) 77 (1 2 2)) ((= (* (* v1 (beta)) v66) (* v64 (* (* (* (@ v64) v1) (beta)) v66)))))
(80 (flip 79 (1)) ((= (* v64 (* (* (* (@ v64) v1) (beta)) v66)) (* (* v1 (beta)) v66))))
(81 (instantiate 80 ((v64 . v0)(v66 . v2))) ((= (* v0 (* (* (* (@ v0) v1) (beta)) v2)) (* (* v1 (beta)) v2))))
(82 (instantiate 3 ((v0 . (* (* v64 v65) (beta))))) ((= (* (* (* v64 v65) (beta)) (* (@ (* (* v64 v65) (beta))) v1)) v1)))
(83 (instantiate 42 ((v0 . v64)(v1 . v65)(v2 . (* (@ (* (* v64 v65) (beta))) v1)))) ((= (* (* (* v64 v65) (beta)) (* (@ (* (* v64 v65) (beta))) v1)) (* v64 (* (alpha) (* (* (* (@ (alpha)) v65) (beta)) (* (@ (* (* v64 v65) (beta))) v1)))))))
(84 (paramod 82 (1 1) 83 (1 1)) ((= v1 (* v64 (* (alpha) (* (* (* (@ (alpha)) v65) (beta)) (* (@ (* (* v64 v65) (beta))) v1)))))))
(85 (instantiate 55 ((v0 . (* v64 v65))(v1 . (beta)))) ((= (@ (* (* v64 v65) (beta))) (* (@ (beta)) (@ (* v64 v65))))))
(86 (paramod 85 (1 1) 84 (1 2 2 2 2 1)) ((= v1 (* v64 (* (alpha) (* (* (* (@ (alpha)) v65) (beta)) (* (* (@ (beta)) (@ (* v64 v65))) v1)))))))
(87 (instantiate 55 ((v0 . v64)(v1 . v65))) ((= (@ (* v64 v65)) (* (@ v65) (@ v64)))))
(88 (paramod 87 (1 1) 86 (1 2 2 2 2 1 2)) ((= v1 (* v64 (* (alpha) (* (* (* (@ (alpha)) v65) (beta)) (* (* (@ (beta)) (* (@ v65) (@ v64))) v1)))))))
(89 (instantiate 81 ((v0 . (alpha))(v1 . v65)(v2 . (* (* (@ (beta)) (* (@ v65) (@ v64))) v1)))) ((= (* (alpha) (* (* (* (@ (alpha)) v65) (beta)) (* (* (@ (beta)) (* (@ v65) (@ v64))) v1))) (* (* v65 (beta)) (* (* (@ (beta)) (* (@ v65) (@ v64))) v1)))))
(90 (paramod 89 (1 1) 88 (1 2 2)) ((= v1 (* v64 (* (* v65 (beta)) (* (* (@ (beta)) (* (@ v65) (@ v64))) v1))))))
(91 (flip 90 (1)) ((= (* v64 (* (* v65 (beta)) (* (* (@ (beta)) (* (@ v65) (@ v64))) v1))) v1)))
(92 (instantiate 91 ((v1 . v2)(v64 . v0)(v65 . v1))) ((= (* v0 (* (* v1 (beta)) (* (* (@ (beta)) (* (@ v1) (@ v0))) v2))) v2)))
(93 (instantiate 74 ((v0 . (alpha))(v1 . v1))) ((= (* (alpha) (* (* (@ (alpha)) (beta)) v1)) (* (beta) v1))))
(94 (paramod 93 (1 1) 47 (1 1 2)) ((= (* v0 (* (beta) v1)) (* (* v0 (beta)) v1))))
(95 (flip 94 (1)) ((= (* (* v0 (beta)) v1) (* v0 (* (beta) v1)))))
(96 (instantiate 95 ((v0 . v1)(v1 . (* (* (@ (beta)) (* (@ v1) (@ v0))) v2)))) ((= (* (* v1 (beta)) (* (* (@ (beta)) (* (@ v1) (@ v0))) v2)) (* v1 (* (beta) (* (* (@ (beta)) (* (@ v1) (@ v0))) v2))))))
(97 (paramod 96 (1 1) 92 (1 1 2)) ((= (* v0 (* v1 (* (beta) (* (* (@ (beta)) (* (@ v1) (@ v0))) v2)))) v2)))
(98 (instantiate 3 ((v0 . (* v64 (beta))))) ((= (* (* v64 (beta)) (* (@ (* v64 (beta))) v1)) v1)))
(99 (instantiate 95 ((v0 . v64)(v1 . (* (@ (* v64 (beta))) v1)))) ((= (* (* v64 (beta)) (* (@ (* v64 (beta))) v1)) (* v64 (* (beta) (* (@ (* v64 (beta))) v1))))))
(100 (paramod 98 (1 1) 99 (1 1)) ((= v1 (* v64 (* (beta) (* (@ (* v64 (beta))) v1))))))
(101 (instantiate 55 ((v0 . v64)(v1 . (beta)))) ((= (@ (* v64 (beta))) (* (@ (beta)) (@ v64)))))
(102 (paramod 101 (1 1) 100 (1 2 2 2 1)) ((= v1 (* v64 (* (beta) (* (* (@ (beta)) (@ v64)) v1))))))
(103 (flip 102 (1)) ((= (* v64 (* (beta) (* (* (@ (beta)) (@ v64)) v1))) v1)))
(104 (instantiate 103 ((v64 . v0))) ((= (* v0 (* (beta) (* (* (@ (beta)) (@ v0)) v1))) v1)))
(105 (instantiate 58 ((v0 . v64)(v1 . (@ v0))(v2 . v66))) ((= (* (* (@ v64) (@ (@ v0))) (* (* (@ v0) v64) v66)) v66)))
(106 (paramod 29 (1 1) 105 (1 1 1 2)) ((= (* (* (@ v64) v0) (* (* (@ v0) v64) v66)) v66)))
(107 (instantiate 106 ((v0 . v1)(v64 . v0)(v66 . v2))) ((= (* (* (@ v0) v1) (* (* (@ v1) v0) v2)) v2)))
(108 (instantiate 104 ((v0 . (@ v64)))) ((= (* (@ v64) (* (beta) (* (* (@ (beta)) (@ (@ v64))) v1))) v1)))
(109 (instantiate 3 ((v0 . v64)(v1 . (* (beta) (* (* (@ (beta)) (@ (@ v64))) v1))))) ((= (* v64 (* (@ v64) (* (beta) (* (* (@ (beta)) (@ (@ v64))) v1)))) (* (beta) (* (* (@ (beta)) (@ (@ v64))) v1)))))
(110 (paramod 108 (1 1) 109 (1 1 2)) ((= (* v64 v1) (* (beta) (* (* (@ (beta)) (@ (@ v64))) v1)))))
(111 (instantiate 29 ((v0 . v64))) ((= (@ (@ v64)) v64)))
(112 (paramod 111 (1 1) 110 (1 2 2 1 2)) ((= (* v64 v1) (* (beta) (* (* (@ (beta)) v64) v1)))))
(113 (flip 112 (1)) ((= (* (beta) (* (* (@ (beta)) v64) v1)) (* v64 v1))))
(114 (instantiate 113 ((v64 . v0))) ((= (* (beta) (* (* (@ (beta)) v0) v1)) (* v0 v1))))
(115 (instantiate 114 ((v0 . (* (@ v1) (@ v0)))(v1 . v2))) ((= (* (beta) (* (* (@ (beta)) (* (@ v1) (@ v0))) v2)) (* (* (@ v1) (@ v0)) v2))))
(116 (paramod 115 (1 1) 97 (1 1 2 2)) ((= (* v0 (* v1 (* (* (@ v1) (@ v0)) v2))) v2)))
(117 (instantiate 107 ((v0 . v65)(v1 . (@ v64)))) ((= (* (* (@ v65) (@ v64)) (* (* (@ (@ v64)) v65) v2)) v2)))
(118 (instantiate 116 ((v0 . v64)(v1 . v65)(v2 . (* (* (@ (@ v64)) v65) v2)))) ((= (* v64 (* v65 (* (* (@ v65) (@ v64)) (* (* (@ (@ v64)) v65) v2)))) (* (* (@ (@ v64)) v65) v2))))
(119 (paramod 117 (1 1) 118 (1 1 2 2)) ((= (* v64 (* v65 v2)) (* (* (@ (@ v64)) v65) v2))))
(120 (instantiate 29 ((v0 . v64))) ((= (@ (@ v64)) v64)))
(121 (paramod 120 (1 1) 119 (1 2 1 1)) ((= (* v64 (* v65 v2)) (* (* v64 v65) v2))))
(122 (flip 121 (1)) ((= (* (* v64 v65) v2) (* v64 (* v65 v2)))))
(123 (instantiate 122 ((v64 . v0)(v65 . v1))) ((= (* (* v0 v1) v2) (* v0 (* v1 v2)))))
(124 (instantiate 123 ((v0 . (A))(v1 . (B))(v2 . (C)))) ((= (* (* (A) (B)) (C)) (* (A) (* (B) (C))))))
(125 (resolve 25 (1) 124 (1)) ())
)