;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 21:15:00 1995
;;
;;;;  -> x=x.
;;;; e*e=e, e*A=A*e, A* (B*A)=B -> .
;;;;  -> (x* ((z* (x*y))* (e*y)))* (e*e)=z.
;;
;; -----> EMPTY CLAUSE at   0.56 sec ----> 112 [back_demod,46,demod,109,unit_del,77,1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((not (= (* (e) (e)) (e))) (not (= (* (e) (A)) (* (A) (e)))) (not (= (* (A) (* (B) (A))) (B)))))
(3 (input) ((= (* (* v0 (* (* v1 (* v0 v2)) (* (e) v2))) (* (e) (e))) v1)))
(4 (instantiate 3 ((v0 . (e))(v1 . (* v0 (* (* v1 (* v0 v2)) (* (e) v2))))(v2 . (e)))) ((= (* (* (e) (* (* (* v0 (* (* v1 (* v0 v2)) (* (e) v2))) (* (e) (e))) (* (e) (e)))) (* (e) (e))) (* v0 (* (* v1 (* v0 v2)) (* (e) v2))))))
(5 (paramod 3 (1 1) 4 (1 1 1 2 1)) ((= (* (* (e) (* v1 (* (e) (e)))) (* (e) (e))) (* v0 (* (* v1 (* v0 v2)) (* (e) v2))))))
(6 (instantiate 5 ((v0 . v1)(v1 . v0))) ((= (* (* (e) (* v0 (* (e) (e)))) (* (e) (e))) (* v1 (* (* v0 (* v1 v2)) (* (e) v2))))))
(7 (instantiate 6 ((v0 . v64))) ((= (* (* (e) (* v64 (* (e) (e)))) (* (e) (e))) (* v1 (* (* v64 (* v1 v2)) (* (e) v2))))))
(8 (instantiate 6 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (* (* (e) (* v64 (* (e) (e)))) (* (e) (e))) (* v65 (* (* v64 (* v65 v66)) (* (e) v66))))))
(9 (paramod 7 (1 1) 8 (1 1)) ((= (* v1 (* (* v64 (* v1 v2)) (* (e) v2))) (* v65 (* (* v64 (* v65 v66)) (* (e) v66))))))
(10 (instantiate 9 ((v1 . v0)(v64 . v1)(v65 . v3)(v66 . v4))) ((= (* v0 (* (* v1 (* v0 v2)) (* (e) v2))) (* v3 (* (* v1 (* v3 v4)) (* (e) v4))))))
(11 (instantiate 3 ((v0 . (e))(v2 . (e)))) ((= (* (* (e) (* (* v1 (* (e) (e))) (* (e) (e)))) (* (e) (e))) v1)))
(12 (instantiate 6 ((v0 . (* v1 (* (e) (e))))(v1 . v65)(v2 . v66))) ((= (* (* (e) (* (* v1 (* (e) (e))) (* (e) (e)))) (* (e) (e))) (* v65 (* (* (* v1 (* (e) (e))) (* v65 v66)) (* (e) v66))))))
(13 (paramod 11 (1 1) 12 (1 1)) ((= v1 (* v65 (* (* (* v1 (* (e) (e))) (* v65 v66)) (* (e) v66))))))
(14 (flip 13 (1)) ((= (* v65 (* (* (* v1 (* (e) (e))) (* v65 v66)) (* (e) v66))) v1)))
(15 (instantiate 14 ((v65 . v0)(v66 . v2))) ((= (* v0 (* (* (* v1 (* (e) (e))) (* v0 v2)) (* (e) v2))) v1)))
(16 (instantiate 3 ((v0 . (e))(v1 . (* (e) (* v0 (* (e) (e)))))(v2 . (e)))) ((= (* (* (e) (* (* (* (e) (* v0 (* (e) (e)))) (* (e) (e))) (* (e) (e)))) (* (e) (e))) (* (e) (* v0 (* (e) (e)))))))
(17 (paramod 6 (1 1) 16 (1 1 1 2 1)) ((= (* (* (e) (* (* v1 (* (* v0 (* v1 v2)) (* (e) v2))) (* (e) (e)))) (* (e) (e))) (* (e) (* v0 (* (e) (e)))))))
(18 (instantiate 3 ((v0 . v1)(v1 . v0)(v2 . v2))) ((= (* (* v1 (* (* v0 (* v1 v2)) (* (e) v2))) (* (e) (e))) v0)))
(19 (paramod 18 (1 1) 17 (1 1 1 2)) ((= (* (* (e) v0) (* (e) (e))) (* (e) (* v0 (* (e) (e)))))))
(20 (instantiate 3 ((v0 . (e)))) ((= (* (* (e) (* (* v1 (* (e) v2)) (* (e) v2))) (* (e) (e))) v1)))
(21 (instantiate 19 ((v0 . (* (* v1 (* (e) v2)) (* (e) v2))))) ((= (* (* (e) (* (* v1 (* (e) v2)) (* (e) v2))) (* (e) (e))) (* (e) (* (* (* v1 (* (e) v2)) (* (e) v2)) (* (e) (e)))))))
(22 (paramod 20 (1 1) 21 (1 1)) ((= v1 (* (e) (* (* (* v1 (* (e) v2)) (* (e) v2)) (* (e) (e)))))))
(23 (flip 22 (1)) ((= (* (e) (* (* (* v1 (* (e) v2)) (* (e) v2)) (* (e) (e)))) v1)))
(24 (instantiate 23 ((v1 . v0)(v2 . v1))) ((= (* (e) (* (* (* v0 (* (e) v1)) (* (e) v1)) (* (e) (e)))) v0)))
(25 (instantiate 19 ((v0 . (* v64 (e))))) ((= (* (* (e) (* v64 (e))) (* (e) (e))) (* (e) (* (* v64 (e)) (* (e) (e)))))))
(26 (instantiate 3 ((v0 . v64)(v1 . (e))(v2 . (e)))) ((= (* (* v64 (* (* (e) (* v64 (e))) (* (e) (e)))) (* (e) (e))) (e))))
(27 (paramod 25 (1 1) 26 (1 1 1 2)) ((= (* (* v64 (* (e) (* (* v64 (e)) (* (e) (e))))) (* (e) (e))) (e))))
(28 (instantiate 27 ((v64 . v0))) ((= (* (* v0 (* (e) (* (* v0 (e)) (* (e) (e))))) (* (e) (e))) (e))))
(29 (instantiate 19 ((v0 . (* (e) (e))))) ((= (* (* (e) (* (e) (e))) (* (e) (e))) (* (e) (* (* (e) (e)) (* (e) (e)))))))
(30 (instantiate 15 ((v0 . (e))(v1 . (e))(v2 . (e)))) ((= (* (e) (* (* (* (e) (* (e) (e))) (* (e) (e))) (* (e) (e)))) (e))))
(31 (paramod 29 (1 1) 30 (1 1 2 1)) ((= (* (e) (* (* (e) (* (* (e) (e)) (* (e) (e)))) (* (e) (e)))) (e))))
(32 (instantiate 19 ((v0 . (e)))) ((= (* (* (e) (e)) (* (e) (e))) (* (e) (* (e) (* (e) (e)))))))
(33 (paramod 32 (1 1) 31 (1 1 2 1 2)) ((= (* (e) (* (* (e) (* (e) (* (e) (* (e) (e))))) (* (e) (e)))) (e))))
(34 (instantiate 19 ((v0 . (* (e) (* (e) (* (e) (e))))))) ((= (* (* (e) (* (e) (* (e) (* (e) (e))))) (* (e) (e))) (* (e) (* (* (e) (* (e) (* (e) (e)))) (* (e) (e)))))))
(35 (paramod 34 (1 1) 33 (1 1 2)) ((= (* (e) (* (e) (* (* (e) (* (e) (* (e) (e)))) (* (e) (e))))) (e))))
(36 (instantiate 19 ((v0 . (* (e) (* (e) (e)))))) ((= (* (* (e) (* (e) (* (e) (e)))) (* (e) (e))) (* (e) (* (* (e) (* (e) (e))) (* (e) (e)))))))
(37 (paramod 36 (1 1) 35 (1 1 2 2)) ((= (* (e) (* (e) (* (e) (* (* (e) (* (e) (e))) (* (e) (e)))))) (e))))
(38 (instantiate 19 ((v0 . (* (e) (e))))) ((= (* (* (e) (* (e) (e))) (* (e) (e))) (* (e) (* (* (e) (e)) (* (e) (e)))))))
(39 (paramod 38 (1 1) 37 (1 1 2 2 2)) ((= (* (e) (* (e) (* (e) (* (e) (* (* (e) (e)) (* (e) (e))))))) (e))))
(40 (instantiate 19 ((v0 . (e)))) ((= (* (* (e) (e)) (* (e) (e))) (* (e) (* (e) (* (e) (e)))))))
(41 (paramod 40 (1 1) 39 (1 1 2 2 2 2)) ((= (* (e) (* (e) (* (e) (* (e) (* (e) (* (e) (* (e) (e)))))))) (e))))
(42 (instantiate 24 ((v0 . v64)(v1 . (* (* (* v0 (* (e) v1)) (* (e) v1)) (* (e) (e)))))) ((= (* (e) (* (* (* v64 (* (e) (* (* (* v0 (* (e) v1)) (* (e) v1)) (* (e) (e))))) (* (e) (* (* (* v0 (* (e) v1)) (* (e) v1)) (* (e) (e))))) (* (e) (e)))) v64)))
(43 (paramod 24 (1 1) 42 (1 1 2 1 1 2)) ((= (* (e) (* (* (* v64 v0) (* (e) (* (* (* v0 (* (e) v1)) (* (e) v1)) (* (e) (e))))) (* (e) (e)))) v64)))
(44 (paramod 24 (1 1) 43 (1 1 2 1 2)) ((= (* (e) (* (* (* v64 v0) v0) (* (e) (e)))) v64)))
(45 (instantiate 44 ((v0 . v1)(v64 . v0))) ((= (* (e) (* (* (* v0 v1) v1) (* (e) (e)))) v0)))
(46 (instantiate 15 ((v0 . (e))(v1 . v65)(v2 . (* (* (* v0 v1) v1) (* (e) (e)))))) ((= (* (e) (* (* (* v65 (* (e) (e))) (* (e) (* (* (* v0 v1) v1) (* (e) (e))))) (* (e) (* (* (* v0 v1) v1) (* (e) (e)))))) v65)))
(47 (paramod 45 (1 1) 46 (1 1 2 1 2)) ((= (* (e) (* (* (* v65 (* (e) (e))) v0) (* (e) (* (* (* v0 v1) v1) (* (e) (e)))))) v65)))
(48 (paramod 45 (1 1) 47 (1 1 2 2)) ((= (* (e) (* (* (* v65 (* (e) (e))) v0) v0)) v65)))
(49 (instantiate 48 ((v0 . v1)(v65 . v0))) ((= (* (e) (* (* (* v0 (* (e) (e))) v1) v1)) v0)))
(50 (instantiate 45 ((v1 . (e)))) ((= (* (e) (* (* (* v0 (e)) (e)) (* (e) (e)))) v0)))
(51 (instantiate 28 ((v0 . (* v0 (e))))) ((= (* (* (* v0 (e)) (* (e) (* (* (* v0 (e)) (e)) (* (e) (e))))) (* (e) (e))) (e))))
(52 (paramod 50 (1 1) 51 (1 1 1 2)) ((= (* (* (* v0 (e)) v0) (* (e) (e))) (e))))
(53 (instantiate 52 ((v0 . (e)))) ((= (* (* (* (e) (e)) (e)) (* (e) (e))) (e))))
(54 (instantiate 52 ((v0 . (* (e) (e))))) ((= (* (* (* (* (e) (e)) (e)) (* (e) (e))) (* (e) (e))) (e))))
(55 (paramod 53 (1 1) 54 (1 1 1)) ((= (* (e) (* (e) (e))) (e))))
(56 (paramod 55 (1 1) 41 (1 1 2 2 2 2 2)) ((= (* (e) (* (e) (* (e) (* (e) (* (e) (e)))))) (e))))
(57 (paramod 55 (1 1) 56 (1 1 2 2 2)) ((= (* (e) (* (e) (* (e) (e)))) (e))))
(58 (paramod 55 (1 1) 57 (1 1 2)) ((= (* (e) (e)) (e))))
(59 (paramod 58 (1 1) 52 (1 1 2)) ((= (* (* (* v0 (e)) v0) (e)) (e))))
(60 (paramod 58 (1 1) 49 (1 1 2 1 1 2)) ((= (* (e) (* (* (* v0 (e)) v1) v1)) v0)))
(61 (paramod 58 (1 1) 45 (1 1 2 2)) ((= (* (e) (* (* (* v0 v1) v1) (e))) v0)))
(62 (paramod 58 (1 1) 19 (1 1 2)) ((= (* (* (e) v0) (e)) (* (e) (* v0 (* (e) (e)))))))
(63 (paramod 58 (1 1) 62 (1 2 2 2)) ((= (* (* (e) v0) (e)) (* (e) (* v0 (e))))))
(64 (paramod 58 (1 1) 3 (1 1 2)) ((= (* (* v0 (* (* v1 (* v0 v2)) (* (e) v2))) (e)) v1)))
(65 (paramod 58 (1 1) 2 (1 1 1)) ((not (= (e) (e))) (not (= (* (e) (A)) (* (A) (e)))) (not (= (* (A) (* (B) (A))) (B)))))
(66 (instantiate 1 ((v0 . (e)))) ((= (e) (e))))
(67 (resolve 65 (1) 66 (1)) ((not (= (* (e) (A)) (* (A) (e)))) (not (= (* (A) (* (B) (A))) (B)))))
(68 (instantiate 60 ((v0 . (* (* v0 (e)) v0))(v1 . v65))) ((= (* (e) (* (* (* (* (* v0 (e)) v0) (e)) v65) v65)) (* (* v0 (e)) v0))))
(69 (paramod 59 (1 1) 68 (1 1 2 1 1)) ((= (* (e) (* (* (e) v65) v65)) (* (* v0 (e)) v0))))
(70 (instantiate 69 ((v0 . v1)(v65 . v0))) ((= (* (e) (* (* (e) v0) v0)) (* (* v1 (e)) v1))))
(71 (instantiate 60 ((v0 . (e))(v1 . v65))) ((= (* (e) (* (* (* (e) (e)) v65) v65)) (e))))
(72 (paramod 58 (1 1) 71 (1 1 2 1 1)) ((= (* (e) (* (* (e) v65) v65)) (e))))
(73 (instantiate 72 ((v65 . v0))) ((= (* (e) (* (* (e) v0) v0)) (e))))
(74 (paramod 73 (1 1) 70 (1 1)) ((= (e) (* (* v1 (e)) v1))))
(75 (flip 74 (1)) ((= (* (* v1 (e)) v1) (e))))
(76 (instantiate 75 ((v1 . v0))) ((= (* (* v0 (e)) v0) (e))))
(77 (instantiate 76 ((v0 . v65))) ((= (* (* v65 (e)) v65) (e))))
(78 (instantiate 60 ((v0 . v65)(v1 . v65))) ((= (* (e) (* (* (* v65 (e)) v65) v65)) v65)))
(79 (paramod 77 (1 1) 78 (1 1 2 1)) ((= (* (e) (* (e) v65)) v65)))
(80 (instantiate 79 ((v65 . v0))) ((= (* (e) (* (e) v0)) v0)))
(81 (instantiate 80 ((v0 . (* (* (* v0 (e)) v1) v1)))) ((= (* (e) (* (e) (* (* (* v0 (e)) v1) v1))) (* (* (* v0 (e)) v1) v1))))
(82 (paramod 60 (1 1) 81 (1 1 2)) ((= (* (e) v0) (* (* (* v0 (e)) v1) v1))))
(83 (flip 82 (1)) ((= (* (* (* v0 (e)) v1) v1) (* (e) v0))))
(84 (instantiate 80 ((v0 . (* (* (e) v0) v0)))) ((= (* (e) (* (e) (* (* (e) v0) v0))) (* (* (e) v0) v0))))
(85 (paramod 73 (1 1) 84 (1 1 2)) ((= (* (e) (e)) (* (* (e) v0) v0))))
(86 (paramod 58 (1 1) 85 (1 1)) ((= (e) (* (* (e) v0) v0))))
(87 (flip 86 (1)) ((= (* (* (e) v0) v0) (e))))
(88 (instantiate 87 ((v0 . (* (e) v0)))) ((= (* (* (e) (* (e) v0)) (* (e) v0)) (e))))
(89 (paramod 80 (1 1) 88 (1 1 1)) ((= (* v0 (* (e) v0)) (e))))
(90 (instantiate 89 ((v0 . v66))) ((= (* v66 (* (e) v66)) (e))))
(91 (instantiate 10 ((v0 . (e))(v1 . v66)(v2 . v66)(v3 . v67)(v4 . v68))) ((= (* (e) (* (* v66 (* (e) v66)) (* (e) v66))) (* v67 (* (* v66 (* v67 v68)) (* (e) v68))))))
(92 (paramod 90 (1 1) 91 (1 1 2 1)) ((= (* (e) (* (e) (* (e) v66))) (* v67 (* (* v66 (* v67 v68)) (* (e) v68))))))
(93 (instantiate 80 ((v0 . v66))) ((= (* (e) (* (e) v66)) v66)))
(94 (paramod 93 (1 1) 92 (1 1 2)) ((= (* (e) v66) (* v67 (* (* v66 (* v67 v68)) (* (e) v68))))))
(95 (flip 94 (1)) ((= (* v67 (* (* v66 (* v67 v68)) (* (e) v68))) (* (e) v66))))
(96 (instantiate 95 ((v66 . v1)(v67 . v0)(v68 . v2))) ((= (* v0 (* (* v1 (* v0 v2)) (* (e) v2))) (* (e) v1))))
(97 (instantiate 89 ((v0 . v64))) ((= (* v64 (* (e) v64)) (e))))
(98 (instantiate 10 ((v0 . v64)(v1 . v65)(v2 . (* (e) v64))(v3 . v67)(v4 . v68))) ((= (* v64 (* (* v65 (* v64 (* (e) v64))) (* (e) (* (e) v64)))) (* v67 (* (* v65 (* v67 v68)) (* (e) v68))))))
(99 (paramod 97 (1 1) 98 (1 1 2 1 2)) ((= (* v64 (* (* v65 (e)) (* (e) (* (e) v64)))) (* v67 (* (* v65 (* v67 v68)) (* (e) v68))))))
(100 (instantiate 80 ((v0 . v64))) ((= (* (e) (* (e) v64)) v64)))
(101 (paramod 100 (1 1) 99 (1 1 2 2)) ((= (* v64 (* (* v65 (e)) v64)) (* v67 (* (* v65 (* v67 v68)) (* (e) v68))))))
(102 (instantiate 96 ((v0 . v67)(v1 . v65)(v2 . v68))) ((= (* v67 (* (* v65 (* v67 v68)) (* (e) v68))) (* (e) v65))))
(103 (paramod 102 (1 1) 101 (1 2)) ((= (* v64 (* (* v65 (e)) v64)) (* (e) v65))))
(104 (instantiate 103 ((v64 . v0)(v65 . v1))) ((= (* v0 (* (* v1 (e)) v0)) (* (e) v1))))
(105 (paramod 96 (1 1) 64 (1 1 1)) ((= (* (* (e) v1) (e)) v1)))
(106 (instantiate 63 ((v0 . v1))) ((= (* (* (e) v1) (e)) (* (e) (* v1 (e))))))
(107 (paramod 106 (1 1) 105 (1 1)) ((= (* (e) (* v1 (e))) v1)))
(108 (instantiate 107 ((v1 . v0))) ((= (* (e) (* v0 (e))) v0)))
(109 (instantiate 108 ((v0 . (* (* v0 v1) v1)))) ((= (* (e) (* (* (* v0 v1) v1) (e))) (* (* v0 v1) v1))))
(110 (paramod 109 (1 1) 61 (1 1)) ((= (* (* v0 v1) v1) v0)))
(111 (instantiate 110 ((v0 . (* v0 (e)))(v1 . v1))) ((= (* (* (* v0 (e)) v1) v1) (* v0 (e)))))
(112 (paramod 111 (1 1) 83 (1 1)) ((= (* v0 (e)) (* (e) v0))))
(113 (flip 112 (1)) ((= (* (e) v0) (* v0 (e)))))
(114 (instantiate 110 ((v1 . (e)))) ((= (* (* v0 (e)) (e)) v0)))
(115 (instantiate 104 ((v0 . v64)(v1 . (* v0 (e))))) ((= (* v64 (* (* (* v0 (e)) (e)) v64)) (* (e) (* v0 (e))))))
(116 (paramod 114 (1 1) 115 (1 1 2 1)) ((= (* v64 (* v0 v64)) (* (e) (* v0 (e))))))
(117 (paramod 108 (1 1) 116 (1 2)) ((= (* v64 (* v0 v64)) v0)))
(118 (instantiate 117 ((v0 . v1)(v64 . v0))) ((= (* v0 (* v1 v0)) v1)))
(119 (instantiate 118 ((v0 . (A))(v1 . (B)))) ((= (* (A) (* (B) (A))) (B))))
(120 (paramod 119 (1 1) 67 (2 1 1)) ((not (= (* (e) (A)) (* (A) (e)))) (not (= (B) (B)))))
(121 (instantiate 113 ((v0 . (A)))) ((= (* (e) (A)) (* (A) (e)))))
(122 (resolve 120 (1) 121 (1)) ((not (= (B) (B)))))
(123 (instantiate 1 ((v0 . (B)))) ((= (B) (B))))
(124 (resolve 122 (1) 123 (1)) ())
)