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