;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 21:24:10 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*y*y*y=y*y*y*y*x.
;;;; B*A*B*A*B*A*B*A=A*B*A*B*A*B*A*B -> .
;;
;; ----> UNIT CONFLICT at   4.67 sec ----> 212 [binary,211.1,1.1]  -> .
;;
(
(1 (input) ((not (= (* (B) (* (A) (* (B) (* (A) (* (B) (* (A) (* (B) (A)))))))) (* (A) (* (B) (* (A) (* (B) (* (A) (* (B) (* (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 (* v1 (* v1 v1)))) (* v1 (* v1 (* v1 (* v1 v0)))))))
(6 (instantiate 4 ((v2 . (* v0 v1)))) ((= (* (* v0 v1) (* v0 v1)) (* v0 (* v1 (* v0 v1))))))
(7 (instantiate 5 ((v0 . v64)(v1 . (* v0 v1)))) ((= (* v64 (* (* v0 v1) (* (* v0 v1) (* (* v0 v1) (* v0 v1))))) (* (* v0 v1) (* (* v0 v1) (* (* v0 v1) (* (* v0 v1) v64)))))))
(8 (paramod 6 (1 1) 7 (1 1 2 2 2)) ((= (* v64 (* (* v0 v1) (* (* v0 v1) (* v0 (* v1 (* v0 v1)))))) (* (* v0 v1) (* (* v0 v1) (* (* v0 v1) (* (* v0 v1) v64)))))))
(9 (instantiate 4 ((v0 . v0)(v1 . v1)(v2 . (* v0 (* v1 (* v0 v1)))))) ((= (* (* v0 v1) (* v0 (* v1 (* v0 v1)))) (* v0 (* v1 (* v0 (* v1 (* v0 v1))))))))
(10 (paramod 9 (1 1) 8 (1 1 2 2)) ((= (* v64 (* (* v0 v1) (* v0 (* v1 (* v0 (* v1 (* v0 v1))))))) (* (* v0 v1) (* (* v0 v1) (* (* v0 v1) (* (* v0 v1) v64)))))))
(11 (instantiate 4 ((v0 . v0)(v1 . v1)(v2 . (* v0 (* v1 (* v0 (* v1 (* v0 v1)))))))) ((= (* (* v0 v1) (* v0 (* v1 (* v0 (* v1 (* v0 v1)))))) (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 (* v0 v1))))))))))
(12 (paramod 11 (1 1) 10 (1 1 2)) ((= (* v64 (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 (* v0 v1)))))))) (* (* v0 v1) (* (* v0 v1) (* (* v0 v1) (* (* v0 v1) v64)))))))
(13 (instantiate 4 ((v0 . v0)(v1 . v1)(v2 . v64))) ((= (* (* v0 v1) v64) (* v0 (* v1 v64)))))
(14 (paramod 13 (1 1) 12 (1 2 2 2 2)) ((= (* v64 (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 (* v0 v1)))))))) (* (* v0 v1) (* (* v0 v1) (* (* v0 v1) (* v0 (* v1 v64))))))))
(15 (instantiate 4 ((v0 . v0)(v1 . v1)(v2 . (* v0 (* v1 v64))))) ((= (* (* v0 v1) (* v0 (* v1 v64))) (* v0 (* v1 (* v0 (* v1 v64)))))))
(16 (paramod 15 (1 1) 14 (1 2 2 2)) ((= (* v64 (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 (* v0 v1)))))))) (* (* v0 v1) (* (* v0 v1) (* v0 (* v1 (* v0 (* v1 v64)))))))))
(17 (instantiate 4 ((v0 . v0)(v1 . v1)(v2 . (* v0 (* v1 (* v0 (* v1 v64))))))) ((= (* (* v0 v1) (* v0 (* v1 (* v0 (* v1 v64))))) (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 v64)))))))))
(18 (paramod 17 (1 1) 16 (1 2 2)) ((= (* v64 (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 (* v0 v1)))))))) (* (* v0 v1) (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 v64))))))))))
(19 (instantiate 4 ((v0 . v0)(v1 . v1)(v2 . (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 v64))))))))) ((= (* (* v0 v1) (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 v64))))))) (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 v64)))))))))))
(20 (paramod 19 (1 1) 18 (1 2)) ((= (* v64 (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 (* v0 v1)))))))) (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 v64)))))))))))
(21 (instantiate 20 ((v0 . v1)(v1 . v2)(v64 . v0))) ((= (* v0 (* v1 (* v2 (* v1 (* v2 (* v1 (* v2 (* v1 v2)))))))) (* v1 (* v2 (* v1 (* v2 (* v1 (* v2 (* v1 (* v2 v0)))))))))))
(22 (instantiate 3 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(23 (instantiate 2 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(24 (resolve 22 (1) 23 (1)) ((not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(25 (instantiate 24 ((v1 . v2)(v3 . v1))) ((not (= (* v0 v1) (* v0 v2))) (= v2 v1)))
(26 (instantiate 25 ((v0 . v65)(v1 . (* v65 (* v66 (* v65 (* v66 (* v65 (* v66 (* v65 v66))))))))(v2 . (* v66 (* v65 (* v66 (* v65 (* v66 (* v65 (* v66 v65)))))))))) ((not (= (* v65 (* v65 (* v66 (* v65 (* v66 (* v65 (* v66 (* v65 v66)))))))) (* v65 (* v66 (* v65 (* v66 (* v65 (* v66 (* v65 (* v66 v65)))))))))) (= (* v66 (* v65 (* v66 (* v65 (* v66 (* v65 (* v66 v65))))))) (* v65 (* v66 (* v65 (* v66 (* v65 (* v66 (* v65 v66))))))))))
(27 (instantiate 21 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (* v65 (* v65 (* v66 (* v65 (* v66 (* v65 (* v66 (* v65 v66)))))))) (* v65 (* v66 (* v65 (* v66 (* v65 (* v66 (* v65 (* v66 v65)))))))))))
(28 (resolve 26 (1) 27 (1)) ((= (* v66 (* v65 (* v66 (* v65 (* v66 (* v65 (* v66 v65))))))) (* v65 (* v66 (* v65 (* v66 (* v65 (* v66 (* v65 v66))))))))))
(29 (instantiate 28 ((v65 . v1)(v66 . v0))) ((= (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 (* v0 v1))))))) (* v1 (* v0 (* v1 (* v0 (* v1 (* v0 (* v1 v0))))))))))
(30 (instantiate 29 ((v0 . (B))(v1 . (A)))) ((= (* (B) (* (A) (* (B) (* (A) (* (B) (* (A) (* (B) (A)))))))) (* (A) (* (B) (* (A) (* (B) (* (A) (* (B) (* (A) (B)))))))))))
(31 (resolve 1 (1) 30 (1)) ())
)