;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 21:51:22 1995
;;
;;;;  -> x=x.
;;;; B*A=A*B, (A*B)*C=A* (B*C) -> .
;;;;  -> (x+y)*y=y.
;;;;  -> x* (y+z)= (y*x)+ (z*x).
;;;;  -> x+x@ =1.
;;;;  -> (x*y)+y=y.
;;;;  -> x+ (y*z)= (y+x)* (z+x).
;;;;  -> x*x@ =0.
;;
;; -----> EMPTY CLAUSE at  28.95 sec ----> 6098 [back_demod,2,demod,5275,unit_del,31,1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((not (= (* (B) (A)) (* (A) (B)))) (not (= (* (* (A) (B)) (C)) (* (A) (* (B) (C)))))))
(3 (input) ((= (* (+ v0 v1) v1) v1)))
(4 (input) ((= (* v0 (+ v1 v2)) (+ (* v1 v0) (* v2 v0)))))
(5 (flip 4 (1)) ((= (+ (* v1 v0) (* v2 v0)) (* v0 (+ v1 v2)))))
(6 (instantiate 5 ((v0 . v1)(v1 . v0))) ((= (+ (* v0 v1) (* v2 v1)) (* v1 (+ v0 v2)))))
(7 (input) ((= (+ v0 (@ v0)) (1))))
(8 (input) ((= (+ (* v0 v1) v1) v1)))
(9 (input) ((= (+ v0 (* v1 v2)) (* (+ v1 v0) (+ v2 v0)))))
(10 (input) ((= (* v0 (@ v0)) (0))))
(11 (flip 9 (1)) ((= (* (+ v1 v0) (+ v2 v0)) (+ v0 (* v1 v2)))))
(12 (instantiate 10 ((v0 . v64))) ((= (* v64 (@ v64)) (0))))
(13 (instantiate 8 ((v0 . v64)(v1 . (@ v64)))) ((= (+ (* v64 (@ v64)) (@ v64)) (@ v64))))
(14 (paramod 12 (1 1) 13 (1 1 1)) ((= (+ (0) (@ v64)) (@ v64))))
(15 (instantiate 14 ((v64 . v0))) ((= (+ (0) (@ v0)) (@ v0))))
(16 (instantiate 3 ((v1 . v65))) ((= (* (+ v0 v65) v65) v65)))
(17 (instantiate 8 ((v0 . (+ v0 v65))(v1 . v65))) ((= (+ (* (+ v0 v65) v65) v65) v65)))
(18 (paramod 16 (1 1) 17 (1 1 1)) ((= (+ v65 v65) v65)))
(19 (instantiate 18 ((v65 . v0))) ((= (+ v0 v0) v0)))
(20 (instantiate 8 ((v1 . v65))) ((= (+ (* v0 v65) v65) v65)))
(21 (instantiate 3 ((v0 . (* v0 v65))(v1 . v65))) ((= (* (+ (* v0 v65) v65) v65) v65)))
(22 (paramod 20 (1 1) 21 (1 1 1)) ((= (* v65 v65) v65)))
(23 (instantiate 22 ((v65 . v0))) ((= (* v0 v0) v0)))
(24 (instantiate 3 ((v1 . v65))) ((= (* (+ v0 v65) v65) v65)))
(25 (instantiate 6 ((v0 . v64)(v1 . v65)(v2 . (+ v0 v65)))) ((= (+ (* v64 v65) (* (+ v0 v65) v65)) (* v65 (+ v64 (+ v0 v65))))))
(26 (paramod 24 (1 1) 25 (1 1 2)) ((= (+ (* v64 v65) v65) (* v65 (+ v64 (+ v0 v65))))))
(27 (instantiate 8 ((v0 . v64)(v1 . v65))) ((= (+ (* v64 v65) v65) v65)))
(28 (paramod 27 (1 1) 26 (1 1)) ((= v65 (* v65 (+ v64 (+ v0 v65))))))
(29 (flip 28 (1)) ((= (* v65 (+ v64 (+ v0 v65))) v65)))
(30 (instantiate 29 ((v0 . v2)(v64 . v1)(v65 . v0))) ((= (* v0 (+ v1 (+ v2 v0))) v0)))
(31 (instantiate 19 ((v0 . (* v66 v65)))) ((= (+ (* v66 v65) (* v66 v65)) (* v66 v65))))
(32 (instantiate 6 ((v0 . v66)(v1 . v65)(v2 . v66))) ((= (+ (* v66 v65) (* v66 v65)) (* v65 (+ v66 v66)))))
(33 (paramod 31 (1 1) 32 (1 1)) ((= (* v66 v65) (* v65 (+ v66 v66)))))
(34 (instantiate 19 ((v0 . v66))) ((= (+ v66 v66) v66)))
(35 (paramod 34 (1 1) 33 (1 2 2)) ((= (* v66 v65) (* v65 v66))))
(36 (instantiate 35 ((v65 . v1)(v66 . v0))) ((= (* v0 v1) (* v1 v0))))
(37 (instantiate 23 ((v0 . v65))) ((= (* v65 v65) v65)))
(38 (instantiate 6 ((v0 . v64)(v1 . v65)(v2 . v65))) ((= (+ (* v64 v65) (* v65 v65)) (* v65 (+ v64 v65)))))
(39 (paramod 37 (1 1) 38 (1 1 2)) ((= (+ (* v64 v65) v65) (* v65 (+ v64 v65)))))
(40 (instantiate 8 ((v0 . v64)(v1 . v65))) ((= (+ (* v64 v65) v65) v65)))
(41 (paramod 40 (1 1) 39 (1 1)) ((= v65 (* v65 (+ v64 v65)))))
(42 (flip 41 (1)) ((= (* v65 (+ v64 v65)) v65)))
(43 (instantiate 42 ((v64 . v1)(v65 . v0))) ((= (* v0 (+ v1 v0)) v0)))
(44 (instantiate 23 ((v0 . v65))) ((= (* v65 v65) v65)))
(45 (instantiate 6 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (+ (* v65 v65) (* v66 v65)) (* v65 (+ v65 v66)))))
(46 (paramod 44 (1 1) 45 (1 1 1)) ((= (+ v65 (* v66 v65)) (* v65 (+ v65 v66)))))
(47 (instantiate 46 ((v65 . v0)(v66 . v1))) ((= (+ v0 (* v1 v0)) (* v0 (+ v0 v1)))))
(48 (instantiate 23 ((v0 . v66))) ((= (* v66 v66) v66)))
(49 (instantiate 9 ((v0 . v64)(v1 . v66)(v2 . v66))) ((= (+ v64 (* v66 v66)) (* (+ v66 v64) (+ v66 v64)))))
(50 (paramod 48 (1 1) 49 (1 1 2)) ((= (+ v64 v66) (* (+ v66 v64) (+ v66 v64)))))
(51 (instantiate 23 ((v0 . (+ v66 v64)))) ((= (* (+ v66 v64) (+ v66 v64)) (+ v66 v64))))
(52 (paramod 51 (1 1) 50 (1 2)) ((= (+ v64 v66) (+ v66 v64))))
(53 (instantiate 52 ((v64 . v0)(v66 . v1))) ((= (+ v0 v1) (+ v1 v0))))
(54 (instantiate 7 ((v0 . (0)))) ((= (+ (0) (@ (0))) (1))))
(55 (instantiate 15 ((v0 . (0)))) ((= (+ (0) (@ (0))) (@ (0)))))
(56 (paramod 54 (1 1) 55 (1 1)) ((= (1) (@ (0)))))
(57 (flip 56 (1)) ((= (@ (0)) (1))))
(58 (instantiate 10 ((v0 . (0)))) ((= (* (0) (@ (0))) (0))))
(59 (paramod 57 (1 1) 58 (1 1 2)) ((= (* (0) (1)) (0))))
(60 (instantiate 19 ((v0 . v64))) ((= (+ v64 v64) v64)))
(61 (instantiate 11 ((v0 . v64)(v1 . v65)(v2 . v64))) ((= (* (+ v65 v64) (+ v64 v64)) (+ v64 (* v65 v64)))))
(62 (paramod 60 (1 1) 61 (1 1 2)) ((= (* (+ v65 v64) v64) (+ v64 (* v65 v64)))))
(63 (instantiate 3 ((v0 . v65)(v1 . v64))) ((= (* (+ v65 v64) v64) v64)))
(64 (paramod 63 (1 1) 62 (1 1)) ((= v64 (+ v64 (* v65 v64)))))
(65 (instantiate 47 ((v0 . v64)(v1 . v65))) ((= (+ v64 (* v65 v64)) (* v64 (+ v64 v65)))))
(66 (paramod 65 (1 1) 64 (1 2)) ((= v64 (* v64 (+ v64 v65)))))
(67 (flip 66 (1)) ((= (* v64 (+ v64 v65)) v64)))
(68 (instantiate 67 ((v64 . v0)(v65 . v1))) ((= (* v0 (+ v0 v1)) v0)))
(69 (instantiate 8 ((v1 . v64))) ((= (+ (* v0 v64) v64) v64)))
(70 (instantiate 11 ((v0 . v64)(v1 . v65)(v2 . (* v0 v64)))) ((= (* (+ v65 v64) (+ (* v0 v64) v64)) (+ v64 (* v65 (* v0 v64))))))
(71 (paramod 69 (1 1) 70 (1 1 2)) ((= (* (+ v65 v64) v64) (+ v64 (* v65 (* v0 v64))))))
(72 (instantiate 3 ((v0 . v65)(v1 . v64))) ((= (* (+ v65 v64) v64) v64)))
(73 (paramod 72 (1 1) 71 (1 1)) ((= v64 (+ v64 (* v65 (* v0 v64))))))
(74 (flip 73 (1)) ((= (+ v64 (* v65 (* v0 v64))) v64)))
(75 (instantiate 74 ((v0 . v2)(v64 . v0)(v65 . v1))) ((= (+ v0 (* v1 (* v2 v0))) v0)))
(76 (paramod 68 (1 1) 47 (1 2)) ((= (+ v0 (* v1 v0)) v0)))
(77 (instantiate 9 ((v0 . v64)(v1 . (0))(v2 . (1)))) ((= (+ v64 (* (0) (1))) (* (+ (0) v64) (+ (1) v64)))))
(78 (paramod 59 (1 1) 77 (1 1 2)) ((= (+ v64 (0)) (* (+ (0) v64) (+ (1) v64)))))
(79 (instantiate 78 ((v64 . v0))) ((= (+ v0 (0)) (* (+ (0) v0) (+ (1) v0)))))
(80 (flip 79 (1)) ((= (* (+ (0) v0) (+ (1) v0)) (+ v0 (0)))))
(81 (instantiate 10 ((v0 . v64))) ((= (* v64 (@ v64)) (0))))
(82 (instantiate 36 ((v0 . v64)(v1 . (@ v64)))) ((= (* v64 (@ v64)) (* (@ v64) v64))))
(83 (paramod 81 (1 1) 82 (1 1)) ((= (0) (* (@ v64) v64))))
(84 (flip 83 (1)) ((= (* (@ v64) v64) (0))))
(85 (instantiate 84 ((v64 . v0))) ((= (* (@ v0) v0) (0))))
(86 (instantiate 85 ((v0 . v66))) ((= (* (@ v66) v66) (0))))
(87 (instantiate 9 ((v0 . v64)(v1 . (@ v66))(v2 . v66))) ((= (+ v64 (* (@ v66) v66)) (* (+ (@ v66) v64) (+ v66 v64)))))
(88 (paramod 86 (1 1) 87 (1 1 2)) ((= (+ v64 (0)) (* (+ (@ v66) v64) (+ v66 v64)))))
(89 (instantiate 88 ((v64 . v0)(v66 . v1))) ((= (+ v0 (0)) (* (+ (@ v1) v0) (+ v1 v0)))))
(90 (instantiate 85 ((v0 . v65))) ((= (* (@ v65) v65) (0))))
(91 (instantiate 8 ((v0 . (@ v65))(v1 . v65))) ((= (+ (* (@ v65) v65) v65) v65)))
(92 (paramod 90 (1 1) 91 (1 1 1)) ((= (+ (0) v65) v65)))
(93 (instantiate 92 ((v65 . v0))) ((= (+ (0) v0) v0)))
(94 (instantiate 85 ((v0 . v65))) ((= (* (@ v65) v65) (0))))
(95 (instantiate 6 ((v0 . (@ v65))(v1 . v65)(v2 . v66))) ((= (+ (* (@ v65) v65) (* v66 v65)) (* v65 (+ (@ v65) v66)))))
(96 (paramod 94 (1 1) 95 (1 1 1)) ((= (+ (0) (* v66 v65)) (* v65 (+ (@ v65) v66)))))
(97 (instantiate 93 ((v0 . (* v66 v65)))) ((= (+ (0) (* v66 v65)) (* v66 v65))))
(98 (paramod 97 (1 1) 96 (1 1)) ((= (* v66 v65) (* v65 (+ (@ v65) v66)))))
(99 (flip 98 (1)) ((= (* v65 (+ (@ v65) v66)) (* v66 v65))))
(100 (instantiate 99 ((v65 . v0)(v66 . v1))) ((= (* v0 (+ (@ v0) v1)) (* v1 v0))))
(101 (flip 89 (1)) ((= (* (+ (@ v1) v0) (+ v1 v0)) (+ v0 (0)))))
(102 (paramod 93 (1 1) 80 (1 1 1)) ((= (* v0 (+ (1) v0)) (+ v0 (0)))))
(103 (instantiate 43 ((v0 . v0)(v1 . (1)))) ((= (* v0 (+ (1) v0)) v0)))
(104 (paramod 103 (1 1) 102 (1 1)) ((= v0 (+ v0 (0)))))
(105 (flip 104 (1)) ((= (+ v0 (0)) v0)))
(106 (paramod 105 (1 1) 101 (1 2)) ((= (* (+ (@ v1) v0) (+ v1 v0)) v0)))
(107 (instantiate 106 ((v0 . v1)(v1 . v0))) ((= (* (+ (@ v0) v1) (+ v0 v1)) v1)))
(108 (instantiate 9 ((v0 . v64))) ((= (+ v64 (* v1 v2)) (* (+ v1 v64) (+ v2 v64)))))
(109 (instantiate 53 ((v0 . v64)(v1 . (* v1 v2)))) ((= (+ v64 (* v1 v2)) (+ (* v1 v2) v64))))
(110 (paramod 108 (1 1) 109 (1 1)) ((= (* (+ v1 v64) (+ v2 v64)) (+ (* v1 v2) v64))))
(111 (flip 110 (1)) ((= (+ (* v1 v2) v64) (* (+ v1 v64) (+ v2 v64)))))
(112 (instantiate 111 ((v1 . v0)(v2 . v1)(v64 . v2))) ((= (+ (* v0 v1) v2) (* (+ v0 v2) (+ v1 v2)))))
(113 (instantiate 7 ((v0 . v64))) ((= (+ v64 (@ v64)) (1))))
(114 (instantiate 53 ((v0 . v64)(v1 . (@ v64)))) ((= (+ v64 (@ v64)) (+ (@ v64) v64))))
(115 (paramod 113 (1 1) 114 (1 1)) ((= (1) (+ (@ v64) v64))))
(116 (flip 115 (1)) ((= (+ (@ v64) v64) (1))))
(117 (instantiate 116 ((v64 . v0))) ((= (+ (@ v0) v0) (1))))
(118 (instantiate 117 ((v0 . (+ v66 v64)))) ((= (+ (@ (+ v66 v64)) (+ v66 v64)) (1))))
(119 (instantiate 30 ((v0 . v64)(v1 . (@ (+ v66 v64)))(v2 . v66))) ((= (* v64 (+ (@ (+ v66 v64)) (+ v66 v64))) v64)))
(120 (paramod 118 (1 1) 119 (1 1 2)) ((= (* v64 (1)) v64)))
(121 (instantiate 120 ((v64 . v0))) ((= (* v0 (1)) v0)))
(122 (instantiate 68 ((v0 . v65))) ((= (* v65 (+ v65 v1)) v65)))
(123 (instantiate 76 ((v0 . (+ v65 v1))(v1 . v65))) ((= (+ (+ v65 v1) (* v65 (+ v65 v1))) (+ v65 v1))))
(124 (paramod 122 (1 1) 123 (1 1 2)) ((= (+ (+ v65 v1) v65) (+ v65 v1))))
(125 (instantiate 124 ((v65 . v0))) ((= (+ (+ v0 v1) v0) (+ v0 v1))))
(126 (instantiate 53 ((v0 . (+ v64 v65))(v1 . v64))) ((= (+ (+ v64 v65) v64) (+ v64 (+ v64 v65)))))
(127 (instantiate 125 ((v0 . v64)(v1 . v65))) ((= (+ (+ v64 v65) v64) (+ v64 v65))))
(128 (paramod 126 (1 1) 127 (1 1)) ((= (+ v64 (+ v64 v65)) (+ v64 v65))))
(129 (instantiate 128 ((v64 . v0)(v65 . v1))) ((= (+ v0 (+ v0 v1)) (+ v0 v1))))
(130 (instantiate 129 ((v0 . (@ v64)))) ((= (+ (@ v64) (+ (@ v64) v1)) (+ (@ v64) v1))))
(131 (instantiate 100 ((v0 . v64)(v1 . (+ (@ v64) v1)))) ((= (* v64 (+ (@ v64) (+ (@ v64) v1))) (* (+ (@ v64) v1) v64))))
(132 (paramod 130 (1 1) 131 (1 1 2)) ((= (* v64 (+ (@ v64) v1)) (* (+ (@ v64) v1) v64))))
(133 (instantiate 100 ((v0 . v64)(v1 . v1))) ((= (* v64 (+ (@ v64) v1)) (* v1 v64))))
(134 (paramod 133 (1 1) 132 (1 1)) ((= (* v1 v64) (* (+ (@ v64) v1) v64))))
(135 (flip 134 (1)) ((= (* (+ (@ v64) v1) v64) (* v1 v64))))
(136 (instantiate 135 ((v64 . v0))) ((= (* (+ (@ v0) v1) v0) (* v1 v0))))
(137 (instantiate 53 ((v0 . (@ v64))(v1 . v65))) ((= (+ (@ v64) v65) (+ v65 (@ v64)))))
(138 (instantiate 107 ((v0 . v64)(v1 . v65))) ((= (* (+ (@ v64) v65) (+ v64 v65)) v65)))
(139 (paramod 137 (1 1) 138 (1 1 1)) ((= (* (+ v65 (@ v64)) (+ v64 v65)) v65)))
(140 (instantiate 139 ((v64 . v1)(v65 . v0))) ((= (* (+ v0 (@ v1)) (+ v1 v0)) v0)))
(141 (instantiate 9 ((v0 . (@ v64)))) ((= (+ (@ v64) (* v1 v2)) (* (+ v1 (@ v64)) (+ v2 (@ v64))))))
(142 (instantiate 136 ((v0 . v64)(v1 . (* v1 v2)))) ((= (* (+ (@ v64) (* v1 v2)) v64) (* (* v1 v2) v64))))
(143 (paramod 141 (1 1) 142 (1 1 1)) ((= (* (* (+ v1 (@ v64)) (+ v2 (@ v64))) v64) (* (* v1 v2) v64))))
(144 (instantiate 143 ((v1 . v0)(v64 . v1))) ((= (* (* (+ v0 (@ v1)) (+ v2 (@ v1))) v1) (* (* v0 v2) v1))))
(145 (instantiate 75 ((v0 . v65))) ((= (+ v65 (* v1 (* v2 v65))) v65)))
(146 (instantiate 140 ((v0 . (* v1 (* v2 v65)))(v1 . v65))) ((= (* (+ (* v1 (* v2 v65)) (@ v65)) (+ v65 (* v1 (* v2 v65)))) (* v1 (* v2 v65)))))
(147 (paramod 145 (1 1) 146 (1 1 2)) ((= (* (+ (* v1 (* v2 v65)) (@ v65)) v65) (* v1 (* v2 v65)))))
(148 (instantiate 112 ((v0 . v1)(v1 . (* v2 v65))(v2 . (@ v65)))) ((= (+ (* v1 (* v2 v65)) (@ v65)) (* (+ v1 (@ v65)) (+ (* v2 v65) (@ v65))))))
(149 (paramod 148 (1 1) 147 (1 1 1)) ((= (* (* (+ v1 (@ v65)) (+ (* v2 v65) (@ v65))) v65) (* v1 (* v2 v65)))))
(150 (instantiate 112 ((v0 . v2)(v1 . v65)(v2 . (@ v65)))) ((= (+ (* v2 v65) (@ v65)) (* (+ v2 (@ v65)) (+ v65 (@ v65))))))
(151 (paramod 150 (1 1) 149 (1 1 1 2)) ((= (* (* (+ v1 (@ v65)) (* (+ v2 (@ v65)) (+ v65 (@ v65)))) v65) (* v1 (* v2 v65)))))
(152 (instantiate 7 ((v0 . v65))) ((= (+ v65 (@ v65)) (1))))
(153 (paramod 152 (1 1) 151 (1 1 1 2 2)) ((= (* (* (+ v1 (@ v65)) (* (+ v2 (@ v65)) (1))) v65) (* v1 (* v2 v65)))))
(154 (instantiate 121 ((v0 . (+ v2 (@ v65))))) ((= (* (+ v2 (@ v65)) (1)) (+ v2 (@ v65)))))
(155 (paramod 154 (1 1) 153 (1 1 1 2)) ((= (* (* (+ v1 (@ v65)) (+ v2 (@ v65))) v65) (* v1 (* v2 v65)))))
(156 (instantiate 144 ((v0 . v1)(v1 . v65)(v2 . v2))) ((= (* (* (+ v1 (@ v65)) (+ v2 (@ v65))) v65) (* (* v1 v2) v65))))
(157 (paramod 156 (1 1) 155 (1 1)) ((= (* (* v1 v2) v65) (* v1 (* v2 v65)))))
(158 (instantiate 157 ((v1 . v0)(v2 . v1)(v65 . v2))) ((= (* (* v0 v1) v2) (* v0 (* v1 v2)))))
(159 (instantiate 158 ((v0 . (A))(v1 . (B))(v2 . (C)))) ((= (* (* (A) (B)) (C)) (* (A) (* (B) (C))))))
(160 (paramod 159 (1 1) 2 (2 1 1)) ((not (= (* (B) (A)) (* (A) (B)))) (not (= (* (A) (* (B) (C))) (* (A) (* (B) (C)))))))
(161 (instantiate 36 ((v0 . (B))(v1 . (A)))) ((= (* (B) (A)) (* (A) (B)))))
(162 (resolve 160 (1) 161 (1)) ((not (= (* (A) (* (B) (C))) (* (A) (* (B) (C)))))))
(163 (instantiate 1 ((v0 . (* (A) (* (B) (C)))))) ((= (* (A) (* (B) (C))) (* (A) (* (B) (C))))))
(164 (resolve 162 (1) 163 (1)) ())
)