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