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