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