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