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