;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 21:56:33 1995
;;
;;;;  -> x=x.
;;;; B+B@ =A+A@ , B*B@ =A*A@  -> .
;;;;  -> (x*y)+ ((y*z)+ (z*x))= (x+y)* ((y+z)* (z+x)).
;;;;  -> y+ (x* (y*z))=y.
;;;;  -> ((x*y)+ (y*z))+y=y.
;;;;  -> (x+x@ )*y=y.
;;;;  -> y* (x+ (y+z))=y.
;;;;  -> ((x+y)* (y+z))*y=y.
;;;;  -> (x*x@ )+y=y.
;;
;; -----> EMPTY CLAUSE at   2.82 sec ----> 726 [hyper,2,286.1,293.1]  -> .
;;
(
(1 (input) ((not (= (+ (B) (@ (B))) (+ (A) (@ (A))))) (not (= (* (B) (@ (B))) (* (A) (@ (A)))))))
(2 (input) ((= (+ (* v0 v1) (+ (* v1 v2) (* v2 v0))) (* (+ v0 v1) (* (+ v1 v2) (+ v2 v0))))))
(3 (input) ((= (+ v0 (* v1 (* v0 v2))) v0)))
(4 (input) ((= (+ (+ (* v0 v1) (* v1 v2)) v1) v1)))
(5 (input) ((= (* (+ v0 (@ v0)) v1) v1)))
(6 (input) ((= (* v0 (+ v1 (+ v0 v2))) v0)))
(7 (input) ((= (+ (* v0 (@ v0)) v1) v1)))
(8 (instantiate 7 ((v1 . (@ (* v0 (@ v0)))))) ((= (+ (* v0 (@ v0)) (@ (* v0 (@ v0)))) (@ (* v0 (@ v0))))))
(9 (instantiate 5 ((v0 . (* v0 (@ v0)))(v1 . v65))) ((= (* (+ (* v0 (@ v0)) (@ (* v0 (@ v0)))) v65) v65)))
(10 (paramod 8 (1 1) 9 (1 1 1)) ((= (* (@ (* v0 (@ v0))) v65) v65)))
(11 (instantiate 10 ((v65 . v1))) ((= (* (@ (* v0 (@ v0))) v1) v1)))
(12 (instantiate 5 ((v1 . (* v64 v66)))) ((= (* (+ v0 (@ v0)) (* v64 v66)) (* v64 v66))))
(13 (instantiate 3 ((v0 . v64)(v1 . (+ v0 (@ v0)))(v2 . v66))) ((= (+ v64 (* (+ v0 (@ v0)) (* v64 v66))) v64)))
(14 (paramod 12 (1 1) 13 (1 1 2)) ((= (+ v64 (* v64 v66)) v64)))
(15 (instantiate 14 ((v64 . v0)(v66 . v1))) ((= (+ v0 (* v0 v1)) v0)))
(16 (instantiate 5 ((v1 . v65))) ((= (* (+ v0 (@ v0)) v65) v65)))
(17 (instantiate 4 ((v0 . (+ v0 (@ v0)))(v1 . v65)(v2 . v66))) ((= (+ (+ (* (+ v0 (@ v0)) v65) (* v65 v66)) v65) v65)))
(18 (paramod 16 (1 1) 17 (1 1 1 1)) ((= (+ (+ v65 (* v65 v66)) v65) v65)))
(19 (instantiate 15 ((v0 . v65)(v1 . v66))) ((= (+ v65 (* v65 v66)) v65)))
(20 (paramod 19 (1 1) 18 (1 1 1)) ((= (+ v65 v65) v65)))
(21 (instantiate 20 ((v65 . v0))) ((= (+ v0 v0) v0)))
(22 (instantiate 3 ((v0 . (* v64 v65))(v1 . v65))) ((= (+ (* v64 v65) (* v65 (* (* v64 v65) v2))) (* v64 v65))))
(23 (instantiate 4 ((v0 . v64)(v1 . v65)(v2 . (* (* v64 v65) v2)))) ((= (+ (+ (* v64 v65) (* v65 (* (* v64 v65) v2))) v65) v65)))
(24 (paramod 22 (1 1) 23 (1 1 1)) ((= (+ (* v64 v65) v65) v65)))
(25 (instantiate 24 ((v64 . v0)(v65 . v1))) ((= (+ (* v0 v1) v1) v1)))
(26 (instantiate 21 ((v0 . v66))) ((= (+ v66 v66) v66)))
(27 (instantiate 6 ((v0 . v66)(v1 . v65)(v2 . v66))) ((= (* v66 (+ v65 (+ v66 v66))) v66)))
(28 (paramod 26 (1 1) 27 (1 1 2 2)) ((= (* v66 (+ v65 v66)) v66)))
(29 (instantiate 28 ((v65 . v1)(v66 . v0))) ((= (* v0 (+ v1 v0)) v0)))
(30 (instantiate 25 ((v1 . (+ v64 v66)))) ((= (+ (* v0 (+ v64 v66)) (+ v64 v66)) (+ v64 v66))))
(31 (instantiate 6 ((v0 . v64)(v1 . (* v0 (+ v64 v66)))(v2 . v66))) ((= (* v64 (+ (* v0 (+ v64 v66)) (+ v64 v66))) v64)))
(32 (paramod 30 (1 1) 31 (1 1 2)) ((= (* v64 (+ v64 v66)) v64)))
(33 (instantiate 32 ((v64 . v0)(v66 . v1))) ((= (* v0 (+ v0 v1)) v0)))
(34 (instantiate 15 ((v0 . v65))) ((= (+ v65 (* v65 v1)) v65)))
(35 (instantiate 29 ((v0 . (* v65 v1))(v1 . v65))) ((= (* (* v65 v1) (+ v65 (* v65 v1))) (* v65 v1))))
(36 (paramod 34 (1 1) 35 (1 1 2)) ((= (* (* v65 v1) v65) (* v65 v1))))
(37 (instantiate 36 ((v65 . v0))) ((= (* (* v0 v1) v0) (* v0 v1))))
(38 (instantiate 33 ((v0 . (@ (* v64 (@ v64)))))) ((= (* (@ (* v64 (@ v64))) (+ (@ (* v64 (@ v64))) v1)) (@ (* v64 (@ v64))))))
(39 (instantiate 11 ((v0 . v64)(v1 . (+ (@ (* v64 (@ v64))) v1)))) ((= (* (@ (* v64 (@ v64))) (+ (@ (* v64 (@ v64))) v1)) (+ (@ (* v64 (@ v64))) v1))))
(40 (paramod 38 (1 1) 39 (1 1)) ((= (@ (* v64 (@ v64))) (+ (@ (* v64 (@ v64))) v1))))
(41 (flip 40 (1)) ((= (+ (@ (* v64 (@ v64))) v1) (@ (* v64 (@ v64))))))
(42 (instantiate 41 ((v64 . v0))) ((= (+ (@ (* v0 (@ v0))) v1) (@ (* v0 (@ v0))))))
(43 (instantiate 29 ((v0 . (@ (* v64 (@ v64)))))) ((= (* (@ (* v64 (@ v64))) (+ v1 (@ (* v64 (@ v64))))) (@ (* v64 (@ v64))))))
(44 (instantiate 11 ((v0 . v64)(v1 . (+ v1 (@ (* v64 (@ v64))))))) ((= (* (@ (* v64 (@ v64))) (+ v1 (@ (* v64 (@ v64))))) (+ v1 (@ (* v64 (@ v64)))))))
(45 (paramod 43 (1 1) 44 (1 1)) ((= (@ (* v64 (@ v64))) (+ v1 (@ (* v64 (@ v64)))))))
(46 (flip 45 (1)) ((= (+ v1 (@ (* v64 (@ v64)))) (@ (* v64 (@ v64))))))
(47 (instantiate 46 ((v1 . v0)(v64 . v1))) ((= (+ v0 (@ (* v1 (@ v1)))) (@ (* v1 (@ v1))))))
(48 (instantiate 11 ((v1 . v66))) ((= (* (@ (* v0 (@ v0))) v66) v66)))
(49 (instantiate 2 ((v0 . v64)(v1 . (@ (* v0 (@ v0))))(v2 . v66))) ((= (+ (* v64 (@ (* v0 (@ v0)))) (+ (* (@ (* v0 (@ v0))) v66) (* v66 v64))) (* (+ v64 (@ (* v0 (@ v0)))) (* (+ (@ (* v0 (@ v0))) v66) (+ v66 v64))))))
(50 (paramod 48 (1 1) 49 (1 1 2 1)) ((= (+ (* v64 (@ (* v0 (@ v0)))) (+ v66 (* v66 v64))) (* (+ v64 (@ (* v0 (@ v0)))) (* (+ (@ (* v0 (@ v0))) v66) (+ v66 v64))))))
(51 (instantiate 15 ((v0 . v66)(v1 . v64))) ((= (+ v66 (* v66 v64)) v66)))
(52 (paramod 51 (1 1) 50 (1 1 2)) ((= (+ (* v64 (@ (* v0 (@ v0)))) v66) (* (+ v64 (@ (* v0 (@ v0)))) (* (+ (@ (* v0 (@ v0))) v66) (+ v66 v64))))))
(53 (instantiate 47 ((v0 . v64)(v1 . v0))) ((= (+ v64 (@ (* v0 (@ v0)))) (@ (* v0 (@ v0))))))
(54 (paramod 53 (1 1) 52 (1 2 1)) ((= (+ (* v64 (@ (* v0 (@ v0)))) v66) (* (@ (* v0 (@ v0))) (* (+ (@ (* v0 (@ v0))) v66) (+ v66 v64))))))
(55 (instantiate 42 ((v0 . v0)(v1 . v66))) ((= (+ (@ (* v0 (@ v0))) v66) (@ (* v0 (@ v0))))))
(56 (paramod 55 (1 1) 54 (1 2 2 1)) ((= (+ (* v64 (@ (* v0 (@ v0)))) v66) (* (@ (* v0 (@ v0))) (* (@ (* v0 (@ v0))) (+ v66 v64))))))
(57 (instantiate 11 ((v0 . v0)(v1 . (+ v66 v64)))) ((= (* (@ (* v0 (@ v0))) (+ v66 v64)) (+ v66 v64))))
(58 (paramod 57 (1 1) 56 (1 2 2)) ((= (+ (* v64 (@ (* v0 (@ v0)))) v66) (* (@ (* v0 (@ v0))) (+ v66 v64)))))
(59 (instantiate 11 ((v0 . v0)(v1 . (+ v66 v64)))) ((= (* (@ (* v0 (@ v0))) (+ v66 v64)) (+ v66 v64))))
(60 (paramod 59 (1 1) 58 (1 2)) ((= (+ (* v64 (@ (* v0 (@ v0)))) v66) (+ v66 v64))))
(61 (instantiate 60 ((v0 . v1)(v64 . v0)(v66 . v2))) ((= (+ (* v0 (@ (* v1 (@ v1)))) v2) (+ v2 v0))))
(62 (flip 61 (1)) ((= (+ v2 v0) (+ (* v0 (@ (* v1 (@ v1)))) v2))))
(63 (instantiate 11 ((v1 . v65))) ((= (* (@ (* v0 (@ v0))) v65) v65)))
(64 (instantiate 37 ((v0 . (@ (* v0 (@ v0))))(v1 . v65))) ((= (* (* (@ (* v0 (@ v0))) v65) (@ (* v0 (@ v0)))) (* (@ (* v0 (@ v0))) v65))))
(65 (paramod 63 (1 1) 64 (1 1 1)) ((= (* v65 (@ (* v0 (@ v0)))) (* (@ (* v0 (@ v0))) v65))))
(66 (instantiate 11 ((v0 . v0)(v1 . v65))) ((= (* (@ (* v0 (@ v0))) v65) v65)))
(67 (paramod 66 (1 1) 65 (1 2)) ((= (* v65 (@ (* v0 (@ v0)))) v65)))
(68 (instantiate 67 ((v0 . v1)(v65 . v0))) ((= (* v0 (@ (* v1 (@ v1)))) v0)))
(69 (instantiate 5 ((v1 . v65))) ((= (* (+ v0 (@ v0)) v65) v65)))
(70 (instantiate 37 ((v0 . (+ v0 (@ v0)))(v1 . v65))) ((= (* (* (+ v0 (@ v0)) v65) (+ v0 (@ v0))) (* (+ v0 (@ v0)) v65))))
(71 (paramod 69 (1 1) 70 (1 1 1)) ((= (* v65 (+ v0 (@ v0))) (* (+ v0 (@ v0)) v65))))
(72 (instantiate 5 ((v0 . v0)(v1 . v65))) ((= (* (+ v0 (@ v0)) v65) v65)))
(73 (paramod 72 (1 1) 71 (1 2)) ((= (* v65 (+ v0 (@ v0))) v65)))
(74 (instantiate 73 ((v0 . v1)(v65 . v0))) ((= (* v0 (+ v1 (@ v1))) v0)))
(75 (paramod 68 (1 1) 62 (1 2 1)) ((= (+ v2 v0) (+ v0 v2))))
(76 (instantiate 75 ((v0 . v1)(v2 . v0))) ((= (+ v0 v1) (+ v1 v0))))
(77 (instantiate 7 ((v1 . v65))) ((= (+ (* v0 (@ v0)) v65) v65)))
(78 (instantiate 76 ((v0 . (* v0 (@ v0)))(v1 . v65))) ((= (+ (* v0 (@ v0)) v65) (+ v65 (* v0 (@ v0))))))
(79 (paramod 77 (1 1) 78 (1 1)) ((= v65 (+ v65 (* v0 (@ v0))))))
(80 (flip 79 (1)) ((= (+ v65 (* v0 (@ v0))) v65)))
(81 (instantiate 80 ((v0 . v1)(v65 . v0))) ((= (+ v0 (* v1 (@ v1))) v0)))
(82 (instantiate 5 ((v1 . (+ v65 (@ v65))))) ((= (* (+ v0 (@ v0)) (+ v65 (@ v65))) (+ v65 (@ v65)))))
(83 (instantiate 74 ((v0 . (+ v0 (@ v0)))(v1 . v65))) ((= (* (+ v0 (@ v0)) (+ v65 (@ v65))) (+ v0 (@ v0)))))
(84 (paramod 82 (1 1) 83 (1 1)) ((= (+ v65 (@ v65)) (+ v0 (@ v0)))))
(85 (instantiate 84 ((v0 . v1)(v65 . v0))) ((= (+ v0 (@ v0)) (+ v1 (@ v1)))))
(86 (instantiate 7 ((v1 . (* v65 (@ v65))))) ((= (+ (* v0 (@ v0)) (* v65 (@ v65))) (* v65 (@ v65)))))
(87 (instantiate 81 ((v0 . (* v0 (@ v0)))(v1 . v65))) ((= (+ (* v0 (@ v0)) (* v65 (@ v65))) (* v0 (@ v0)))))
(88 (paramod 86 (1 1) 87 (1 1)) ((= (* v65 (@ v65)) (* v0 (@ v0)))))
(89 (instantiate 88 ((v0 . v1)(v65 . v0))) ((= (* v0 (@ v0)) (* v1 (@ v1)))))
(90 (instantiate 85 ((v0 . (B))(v1 . (A)))) ((= (+ (B) (@ (B))) (+ (A) (@ (A))))))
(91 (resolve 1 (1) 90 (1)) ((not (= (* (B) (@ (B))) (* (A) (@ (A)))))))
(92 (instantiate 89 ((v0 . (B))(v1 . (A)))) ((= (* (B) (@ (B))) (* (A) (@ (A))))))
(93 (resolve 91 (1) 92 (1)) ())
)