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