;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:20:04 1995
;;
;;;;  -> x=x.
;;;;  -> ((x*x)*y)* (z* (x*y))=z.
;;;; A*A=A, (A*B)*A=B -> .
;;
;; -----> EMPTY CLAUSE at   0.49 sec ----> 143 [back_demod,4,demod,138,142,unit_del,1,1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((= (* (* (* v0 v0) v1) (* v2 (* v0 v1))) v2)))
(3 (input) ((not (= (* (A) (A)) (A))) (not (= (* (* (A) (B)) (A)) (B)))))
(4 (instantiate 2 ((v2 . v64))) ((= (* (* (* v0 v0) v1) (* v64 (* v0 v1))) v64)))
(5 (instantiate 2 ((v0 . v64)(v1 . (* v0 v1))(v2 . (* (* v0 v0) v1)))) ((= (* (* (* v64 v64) (* v0 v1)) (* (* (* v0 v0) v1) (* v64 (* v0 v1)))) (* (* v0 v0) v1))))
(6 (paramod 4 (1 1) 5 (1 1 2)) ((= (* (* (* v64 v64) (* v0 v1)) v64) (* (* v0 v0) v1))))
(7 (instantiate 6 ((v0 . v1)(v1 . v2)(v64 . v0))) ((= (* (* (* v0 v0) (* v1 v2)) v0) (* (* v1 v1) v2))))
(8 (instantiate 2 ((v1 . (* v0 v0))(v2 . v65))) ((= (* (* (* v0 v0) (* v0 v0)) (* v65 (* v0 (* v0 v0)))) v65)))
(9 (instantiate 7 ((v0 . (* v0 v0))(v1 . v65)(v2 . (* v0 (* v0 v0))))) ((= (* (* (* (* v0 v0) (* v0 v0)) (* v65 (* v0 (* v0 v0)))) (* v0 v0)) (* (* v65 v65) (* v0 (* v0 v0))))))
(10 (paramod 8 (1 1) 9 (1 1 1)) ((= (* v65 (* v0 v0)) (* (* v65 v65) (* v0 (* v0 v0))))))
(11 (flip 10 (1)) ((= (* (* v65 v65) (* v0 (* v0 v0))) (* v65 (* v0 v0)))))
(12 (instantiate 11 ((v0 . v1)(v65 . v0))) ((= (* (* v0 v0) (* v1 (* v1 v1))) (* v0 (* v1 v1)))))
(13 (instantiate 12 ((v0 . v64)(v1 . v65))) ((= (* (* v64 v64) (* v65 (* v65 v65))) (* v64 (* v65 v65)))))
(14 (instantiate 7 ((v0 . v64)(v1 . v65)(v2 . (* v65 v65)))) ((= (* (* (* v64 v64) (* v65 (* v65 v65))) v64) (* (* v65 v65) (* v65 v65)))))
(15 (paramod 13 (1 1) 14 (1 1 1)) ((= (* (* v64 (* v65 v65)) v64) (* (* v65 v65) (* v65 v65)))))
(16 (instantiate 15 ((v64 . v0)(v65 . v1))) ((= (* (* v0 (* v1 v1)) v0) (* (* v1 v1) (* v1 v1)))))
(17 (instantiate 12 ((v1 . v64))) ((= (* (* v0 v0) (* v64 (* v64 v64))) (* v0 (* v64 v64)))))
(18 (instantiate 2 ((v0 . v64)(v1 . (* v64 v64))(v2 . (* v0 v0)))) ((= (* (* (* v64 v64) (* v64 v64)) (* (* v0 v0) (* v64 (* v64 v64)))) (* v0 v0))))
(19 (paramod 17 (1 1) 18 (1 1 2)) ((= (* (* (* v64 v64) (* v64 v64)) (* v0 (* v64 v64))) (* v0 v0))))
(20 (instantiate 19 ((v0 . v1)(v64 . v0))) ((= (* (* (* v0 v0) (* v0 v0)) (* v1 (* v0 v0))) (* v1 v1))))
(21 (flip 20 (1)) ((= (* v1 v1) (* (* (* v0 v0) (* v0 v0)) (* v1 (* v0 v0))))))
(22 (instantiate 16 ((v0 . (* v66 v66))(v1 . v66))) ((= (* (* (* v66 v66) (* v66 v66)) (* v66 v66)) (* (* v66 v66) (* v66 v66)))))
(23 (instantiate 7 ((v0 . (* v66 v66))(v1 . v66)(v2 . v66))) ((= (* (* (* (* v66 v66) (* v66 v66)) (* v66 v66)) (* v66 v66)) (* (* v66 v66) v66))))
(24 (paramod 22 (1 1) 23 (1 1 1)) ((= (* (* (* v66 v66) (* v66 v66)) (* v66 v66)) (* (* v66 v66) v66))))
(25 (instantiate 16 ((v0 . (* v66 v66))(v1 . v66))) ((= (* (* (* v66 v66) (* v66 v66)) (* v66 v66)) (* (* v66 v66) (* v66 v66)))))
(26 (paramod 25 (1 1) 24 (1 1)) ((= (* (* v66 v66) (* v66 v66)) (* (* v66 v66) v66))))
(27 (instantiate 26 ((v66 . v0))) ((= (* (* v0 v0) (* v0 v0)) (* (* v0 v0) v0))))
(28 (paramod 27 (1 1) 21 (1 2 1)) ((= (* v1 v1) (* (* (* v0 v0) v0) (* v1 (* v0 v0))))))
(29 (instantiate 2 ((v0 . v0)(v1 . v0)(v2 . v1))) ((= (* (* (* v0 v0) v0) (* v1 (* v0 v0))) v1)))
(30 (paramod 29 (1 1) 28 (1 2)) ((= (* v1 v1) v1)))
(31 (instantiate 30 ((v1 . v0))) ((= (* v0 v0) v0)))
(32 (instantiate 31 ((v0 . v1))) ((= (* v1 v1) v1)))
(33 (paramod 32 (1 1) 16 (1 1 1 2)) ((= (* (* v0 v1) v0) (* (* v1 v1) (* v1 v1)))))
(34 (instantiate 31 ((v0 . v1))) ((= (* v1 v1) v1)))
(35 (paramod 34 (1 1) 33 (1 2 1)) ((= (* (* v0 v1) v0) (* v1 (* v1 v1)))))
(36 (instantiate 31 ((v0 . v1))) ((= (* v1 v1) v1)))
(37 (paramod 36 (1 1) 35 (1 2 2)) ((= (* (* v0 v1) v0) (* v1 v1))))
(38 (instantiate 31 ((v0 . v1))) ((= (* v1 v1) v1)))
(39 (paramod 38 (1 1) 37 (1 2)) ((= (* (* v0 v1) v0) v1)))
(40 (instantiate 31 ((v0 . (A)))) ((= (* (A) (A)) (A))))
(41 (paramod 40 (1 1) 3 (1 1 1)) ((not (= (A) (A))) (not (= (* (* (A) (B)) (A)) (B)))))
(42 (instantiate 39 ((v0 . (A))(v1 . (B)))) ((= (* (* (A) (B)) (A)) (B))))
(43 (paramod 42 (1 1) 41 (2 1 1)) ((not (= (A) (A))) (not (= (B) (B)))))
(44 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(45 (resolve 43 (1) 44 (1)) ((not (= (B) (B)))))
(46 (instantiate 1 ((v0 . (B)))) ((= (B) (B))))
(47 (resolve 45 (1) 46 (1)) ())
)