;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:43:14 1995
;;
;;;; x=x.
;;;; x* (x\y)=y.
;;;; x\ (x*y)=y.
;;;; (x/y)*y=x.
;;;; (x*y)/y=x.
;;;; x* (y* (y*x))=y*x.
;;;; A* (A*B)!=B*A.
;;
;; ----> UNIT CONFLICT at   0.47 sec ----> 133 [binary,132.1,13.1] $F.
;;
(
(1 (input) ((= (\ v0 (* v0 v1)) v1)))
(2 (input) ((= (* (/ v0 v1) v1) v0)))
(3 (input) ((= (/ (* v0 v1) v1) v0)))
(4 (input) ((= (* v0 (* v1 (* v1 v0))) (* v1 v0))))
(5 (input) ((not (= (* (A) (* (A) (B))) (* (B) (A))))))
(6 (flip 5 (1)) ((not (= (* (B) (A)) (* (A) (* (A) (B)))))))
(7 (instantiate 2 ((v1 . v65))) ((= (* (/ v0 v65) v65) v0)))
(8 (instantiate 1 ((v0 . (/ v0 v65))(v1 . v65))) ((= (\ (/ v0 v65) (* (/ v0 v65) v65)) v65)))
(9 (paramod 7 (1 1) 8 (1 1 2)) ((= (\ (/ v0 v65) v0) v65)))
(10 (instantiate 9 ((v65 . v1))) ((= (\ (/ v0 v1) v0) v1)))
(11 (instantiate 2 ((v1 . v64))) ((= (* (/ v0 v64) v64) v0)))
(12 (instantiate 4 ((v0 . v64)(v1 . (/ v0 v64)))) ((= (* v64 (* (/ v0 v64) (* (/ v0 v64) v64))) (* (/ v0 v64) v64))))
(13 (paramod 11 (1 1) 12 (1 1 2 2)) ((= (* v64 (* (/ v0 v64) v0)) (* (/ v0 v64) v64))))
(14 (instantiate 2 ((v0 . v0)(v1 . v64))) ((= (* (/ v0 v64) v64) v0)))
(15 (paramod 14 (1 1) 13 (1 2)) ((= (* v64 (* (/ v0 v64) v0)) v0)))
(16 (instantiate 15 ((v0 . v1)(v64 . v0))) ((= (* v0 (* (/ v1 v0) v1)) v1)))
(17 (instantiate 16 ((v0 . v65))) ((= (* v65 (* (/ v1 v65) v1)) v1)))
(18 (instantiate 4 ((v0 . (* (/ v1 v65) v1))(v1 . v65))) ((= (* (* (/ v1 v65) v1) (* v65 (* v65 (* (/ v1 v65) v1)))) (* v65 (* (/ v1 v65) v1)))))
(19 (paramod 17 (1 1) 18 (1 1 2 2)) ((= (* (* (/ v1 v65) v1) (* v65 v1)) (* v65 (* (/ v1 v65) v1)))))
(20 (instantiate 16 ((v0 . v65)(v1 . v1))) ((= (* v65 (* (/ v1 v65) v1)) v1)))
(21 (paramod 20 (1 1) 19 (1 2)) ((= (* (* (/ v1 v65) v1) (* v65 v1)) v1)))
(22 (instantiate 21 ((v1 . v0)(v65 . v1))) ((= (* (* (/ v0 v1) v0) (* v1 v0)) v0)))
(23 (instantiate 16 ((v0 . v64))) ((= (* v64 (* (/ v1 v64) v1)) v1)))
(24 (instantiate 3 ((v0 . v64)(v1 . (* (/ v1 v64) v1)))) ((= (/ (* v64 (* (/ v1 v64) v1)) (* (/ v1 v64) v1)) v64)))
(25 (paramod 23 (1 1) 24 (1 1 1)) ((= (/ v1 (* (/ v1 v64) v1)) v64)))
(26 (instantiate 25 ((v1 . v0)(v64 . v1))) ((= (/ v0 (* (/ v0 v1) v0)) v1)))
(27 (instantiate 16 ((v0 . v64))) ((= (* v64 (* (/ v1 v64) v1)) v1)))
(28 (instantiate 1 ((v0 . v64)(v1 . (* (/ v1 v64) v1)))) ((= (\ v64 (* v64 (* (/ v1 v64) v1))) (* (/ v1 v64) v1))))
(29 (paramod 27 (1 1) 28 (1 1 2)) ((= (\ v64 v1) (* (/ v1 v64) v1))))
(30 (instantiate 29 ((v64 . v0))) ((= (\ v0 v1) (* (/ v1 v0) v1))))
(31 (instantiate 30 ((v0 . (/ v0 v1))(v1 . v0))) ((= (\ (/ v0 v1) v0) (* (/ v0 (/ v0 v1)) v0))))
(32 (paramod 31 (1 1) 10 (1 1)) ((= (* (/ v0 (/ v0 v1)) v0) v1)))
(33 (instantiate 26 ((v0 . v64))) ((= (/ v64 (* (/ v64 v1) v64)) v1)))
(34 (instantiate 26 ((v0 . v64)(v1 . (* (/ v64 v1) v64)))) ((= (/ v64 (* (/ v64 (* (/ v64 v1) v64)) v64)) (* (/ v64 v1) v64))))
(35 (paramod 33 (1 1) 34 (1 1 2 1)) ((= (/ v64 (* v1 v64)) (* (/ v64 v1) v64))))
(36 (instantiate 35 ((v64 . v0))) ((= (/ v0 (* v1 v0)) (* (/ v0 v1) v0))))
(37 (instantiate 32 ((v0 . v65))) ((= (* (/ v65 (/ v65 v1)) v65) v1)))
(38 (instantiate 3 ((v0 . (/ v65 (/ v65 v1)))(v1 . v65))) ((= (/ (* (/ v65 (/ v65 v1)) v65) v65) (/ v65 (/ v65 v1)))))
(39 (paramod 37 (1 1) 38 (1 1 1)) ((= (/ v1 v65) (/ v65 (/ v65 v1)))))
(40 (instantiate 39 ((v1 . v0)(v65 . v1))) ((= (/ v0 v1) (/ v1 (/ v1 v0)))))
(41 (flip 40 (1)) ((= (/ v1 (/ v1 v0)) (/ v0 v1))))
(42 (instantiate 3 ((v1 . v64))) ((= (/ (* v0 v64) v64) v0)))
(43 (instantiate 41 ((v0 . v64)(v1 . (* v0 v64)))) ((= (/ (* v0 v64) (/ (* v0 v64) v64)) (/ v64 (* v0 v64)))))
(44 (paramod 42 (1 1) 43 (1 1 2)) ((= (/ (* v0 v64) v0) (/ v64 (* v0 v64)))))
(45 (instantiate 36 ((v0 . v64)(v1 . v0))) ((= (/ v64 (* v0 v64)) (* (/ v64 v0) v64))))
(46 (paramod 45 (1 1) 44 (1 2)) ((= (/ (* v0 v64) v0) (* (/ v64 v0) v64))))
(47 (instantiate 46 ((v64 . v1))) ((= (/ (* v0 v1) v0) (* (/ v1 v0) v1))))
(48 (instantiate 41 ((v1 . v64))) ((= (/ v64 (/ v64 v0)) (/ v0 v64))))
(49 (instantiate 2 ((v0 . v64)(v1 . (/ v64 v0)))) ((= (* (/ v64 (/ v64 v0)) (/ v64 v0)) v64)))
(50 (paramod 48 (1 1) 49 (1 1 1)) ((= (* (/ v0 v64) (/ v64 v0)) v64)))
(51 (instantiate 50 ((v64 . v1))) ((= (* (/ v0 v1) (/ v1 v0)) v1)))
(52 (instantiate 3 ((v1 . v64))) ((= (/ (* v0 v64) v64) v0)))
(53 (instantiate 51 ((v0 . v64)(v1 . (* v0 v64)))) ((= (* (/ v64 (* v0 v64)) (/ (* v0 v64) v64)) (* v0 v64))))
(54 (paramod 52 (1 1) 53 (1 1 2)) ((= (* (/ v64 (* v0 v64)) v0) (* v0 v64))))
(55 (instantiate 36 ((v0 . v64)(v1 . v0))) ((= (/ v64 (* v0 v64)) (* (/ v64 v0) v64))))
(56 (paramod 55 (1 1) 54 (1 1 1)) ((= (* (* (/ v64 v0) v64) v0) (* v0 v64))))
(57 (instantiate 56 ((v0 . v1)(v64 . v0))) ((= (* (* (/ v0 v1) v0) v1) (* v1 v0))))
(58 (instantiate 47 ((v0 . v65))) ((= (/ (* v65 v1) v65) (* (/ v1 v65) v1))))
(59 (instantiate 57 ((v0 . (* v65 v1))(v1 . v65))) ((= (* (* (/ (* v65 v1) v65) (* v65 v1)) v65) (* v65 (* v65 v1)))))
(60 (paramod 58 (1 1) 59 (1 1 1 1)) ((= (* (* (* (/ v1 v65) v1) (* v65 v1)) v65) (* v65 (* v65 v1)))))
(61 (instantiate 22 ((v0 . v1)(v1 . v65))) ((= (* (* (/ v1 v65) v1) (* v65 v1)) v1)))
(62 (paramod 61 (1 1) 60 (1 1 1)) ((= (* v1 v65) (* v65 (* v65 v1)))))
(63 (instantiate 62 ((v1 . v0)(v65 . v1))) ((= (* v0 v1) (* v1 (* v1 v0)))))
(64 (instantiate 63 ((v0 . (B))(v1 . (A)))) ((= (* (B) (A)) (* (A) (* (A) (B))))))
(65 (resolve 6 (1) 64 (1)) ())
)