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