;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 21:56:45 1995
;;
;;;;  -> x=x.
;;;; (A*B)+ (A*C)=A* (B+C), (A*B)+B=B -> .
;;;;  -> (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.
;;;;  -> x+x@ =1.
;;;;  -> x*x@ =0.
;;;;  -> (x+y)+z=x+ (y+z).
;;;;  -> (x*y)*z=x* (y*z).
;;
;; ----> UNIT CONFLICT at  24.59 sec ----> 4972 [binary,4971.1,134.1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((not (= (+ (* (A) (B)) (* (A) (C))) (* (A) (+ (B) (C))))) (not (= (+ (* (A) (B)) (B)) (B)))))
(3 (input) ((= (+ (* v0 v1) (+ (* v1 v2) (* v2 v0))) (* (+ v0 v1) (* (+ v1 v2) (+ v2 v0))))))
(4 (input) ((= (+ v0 (* v1 (* v0 v2))) v0)))
(5 (input) ((= (+ (+ (* v0 v1) (* v1 v2)) v1) v1)))
(6 (input) ((= (* (+ v0 (@ v0)) v1) v1)))
(7 (input) ((= (* v0 (+ v1 (+ v0 v2))) v0)))
(8 (input) ((= (+ (* v0 (@ v0)) v1) v1)))
(9 (input) ((= (+ v0 (@ v0)) (1))))
(10 (input) ((= (* v0 (@ v0)) (0))))
(11 (input) ((= (+ (+ v0 v1) v2) (+ v0 (+ v1 v2)))))
(12 (input) ((= (* (* v0 v1) v2) (* v0 (* v1 v2)))))
(13 (paramod 9 (1 1) 6 (1 1 1)) ((= (* (1) v1) v1)))
(14 (instantiate 13 ((v1 . v0))) ((= (* (1) v0) v0)))
(15 (paramod 10 (1 1) 8 (1 1 1)) ((= (+ (0) v1) v1)))
(16 (instantiate 15 ((v1 . v0))) ((= (+ (0) v0) v0)))
(17 (instantiate 11 ((v0 . (* v0 v1))(v1 . (* v1 v2))(v2 . v1))) ((= (+ (+ (* v0 v1) (* v1 v2)) v1) (+ (* v0 v1) (+ (* v1 v2) v1)))))
(18 (paramod 17 (1 1) 5 (1 1)) ((= (+ (* v0 v1) (+ (* v1 v2) v1)) v1)))
(19 (instantiate 14 ((v0 . v66))) ((= (* (1) v66) v66)))
(20 (instantiate 3 ((v0 . v64)(v1 . (1))(v2 . v66))) ((= (+ (* v64 (1)) (+ (* (1) v66) (* v66 v64))) (* (+ v64 (1)) (* (+ (1) v66) (+ v66 v64))))))
(21 (paramod 19 (1 1) 20 (1 1 2 1)) ((= (+ (* v64 (1)) (+ v66 (* v66 v64))) (* (+ v64 (1)) (* (+ (1) v66) (+ v66 v64))))))
(22 (instantiate 21 ((v64 . v0)(v66 . v1))) ((= (+ (* v0 (1)) (+ v1 (* v1 v0))) (* (+ v0 (1)) (* (+ (1) v1) (+ v1 v0))))))
(23 (instantiate 16 ((v0 . (@ (0))))) ((= (+ (0) (@ (0))) (@ (0)))))
(24 (instantiate 9 ((v0 . (0)))) ((= (+ (0) (@ (0))) (1))))
(25 (paramod 23 (1 1) 24 (1 1)) ((= (@ (0)) (1))))
(26 (instantiate 14 ((v0 . v66))) ((= (* (1) v66) v66)))
(27 (instantiate 4 ((v0 . (1))(v1 . v65)(v2 . v66))) ((= (+ (1) (* v65 (* (1) v66))) (1))))
(28 (paramod 26 (1 1) 27 (1 1 2 2)) ((= (+ (1) (* v65 v66)) (1))))
(29 (instantiate 28 ((v65 . v0)(v66 . v1))) ((= (+ (1) (* v0 v1)) (1))))
(30 (instantiate 14 ((v0 . (* v64 v66)))) ((= (* (1) (* v64 v66)) (* v64 v66))))
(31 (instantiate 4 ((v0 . v64)(v1 . (1))(v2 . v66))) ((= (+ v64 (* (1) (* 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 16 ((v0 . (* v65 (* (0) v66))))) ((= (+ (0) (* v65 (* (0) v66))) (* v65 (* (0) v66)))))
(35 (instantiate 4 ((v0 . (0))(v1 . v65)(v2 . v66))) ((= (+ (0) (* v65 (* (0) v66))) (0))))
(36 (paramod 34 (1 1) 35 (1 1)) ((= (* v65 (* (0) v66)) (0))))
(37 (instantiate 36 ((v65 . v0)(v66 . v1))) ((= (* v0 (* (0) v1)) (0))))
(38 (instantiate 33 ((v0 . v1)(v1 . v0))) ((= (+ v1 (* v1 v0)) v1)))
(39 (paramod 38 (1 1) 22 (1 1 2)) ((= (+ (* v0 (1)) v1) (* (+ v0 (1)) (* (+ (1) v1) (+ v1 v0))))))
(40 (instantiate 10 ((v0 . (0)))) ((= (* (0) (@ (0))) (0))))
(41 (paramod 25 (1 1) 40 (1 1 2)) ((= (* (0) (1)) (0))))
(42 (instantiate 14 ((v0 . (@ (1))))) ((= (* (1) (@ (1))) (@ (1)))))
(43 (instantiate 10 ((v0 . (1)))) ((= (* (1) (@ (1))) (0))))
(44 (paramod 42 (1 1) 43 (1 1)) ((= (@ (1)) (0))))
(45 (instantiate 10 ((v0 . v65))) ((= (* v65 (@ v65)) (0))))
(46 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . (@ v65)))) ((= (+ (* v64 v65) (+ (* v65 (@ v65)) (* (@ v65) v64))) (* (+ v64 v65) (* (+ v65 (@ v65)) (+ (@ v65) v64))))))
(47 (paramod 45 (1 1) 46 (1 1 2 1)) ((= (+ (* v64 v65) (+ (0) (* (@ v65) v64))) (* (+ v64 v65) (* (+ v65 (@ v65)) (+ (@ v65) v64))))))
(48 (instantiate 16 ((v0 . (* (@ v65) v64)))) ((= (+ (0) (* (@ v65) v64)) (* (@ v65) v64))))
(49 (paramod 48 (1 1) 47 (1 1 2)) ((= (+ (* v64 v65) (* (@ v65) v64)) (* (+ v64 v65) (* (+ v65 (@ v65)) (+ (@ v65) v64))))))
(50 (instantiate 9 ((v0 . v65))) ((= (+ v65 (@ v65)) (1))))
(51 (paramod 50 (1 1) 49 (1 2 2 1)) ((= (+ (* v64 v65) (* (@ v65) v64)) (* (+ v64 v65) (* (1) (+ (@ v65) v64))))))
(52 (instantiate 14 ((v0 . (+ (@ v65) v64)))) ((= (* (1) (+ (@ v65) v64)) (+ (@ v65) v64))))
(53 (paramod 52 (1 1) 51 (1 2 2)) ((= (+ (* v64 v65) (* (@ v65) v64)) (* (+ v64 v65) (+ (@ v65) v64)))))
(54 (instantiate 53 ((v64 . v0)(v65 . v1))) ((= (+ (* v0 v1) (* (@ v1) v0)) (* (+ v0 v1) (+ (@ v1) v0)))))
(55 (instantiate 10 ((v0 . v64))) ((= (* v64 (@ v64)) (0))))
(56 (instantiate 3 ((v0 . v64)(v1 . (@ v64))(v2 . v66))) ((= (+ (* v64 (@ v64)) (+ (* (@ v64) v66) (* v66 v64))) (* (+ v64 (@ v64)) (* (+ (@ v64) v66) (+ v66 v64))))))
(57 (paramod 55 (1 1) 56 (1 1 1)) ((= (+ (0) (+ (* (@ v64) v66) (* v66 v64))) (* (+ v64 (@ v64)) (* (+ (@ v64) v66) (+ v66 v64))))))
(58 (instantiate 16 ((v0 . (+ (* (@ v64) v66) (* v66 v64))))) ((= (+ (0) (+ (* (@ v64) v66) (* v66 v64))) (+ (* (@ v64) v66) (* v66 v64)))))
(59 (paramod 58 (1 1) 57 (1 1)) ((= (+ (* (@ v64) v66) (* v66 v64)) (* (+ v64 (@ v64)) (* (+ (@ v64) v66) (+ v66 v64))))))
(60 (instantiate 9 ((v0 . v64))) ((= (+ v64 (@ v64)) (1))))
(61 (paramod 60 (1 1) 59 (1 2 1)) ((= (+ (* (@ v64) v66) (* v66 v64)) (* (1) (* (+ (@ v64) v66) (+ v66 v64))))))
(62 (instantiate 14 ((v0 . (* (+ (@ v64) v66) (+ v66 v64))))) ((= (* (1) (* (+ (@ v64) v66) (+ v66 v64))) (* (+ (@ v64) v66) (+ v66 v64)))))
(63 (paramod 62 (1 1) 61 (1 2)) ((= (+ (* (@ v64) v66) (* v66 v64)) (* (+ (@ v64) v66) (+ v66 v64)))))
(64 (instantiate 63 ((v64 . v0)(v66 . v1))) ((= (+ (* (@ v0) v1) (* v1 v0)) (* (+ (@ v0) v1) (+ v1 v0)))))
(65 (flip 54 (1)) ((= (* (+ v0 v1) (+ (@ v1) v0)) (+ (* v0 v1) (* (@ v1) v0)))))
(66 (instantiate 9 ((v0 . (1)))) ((= (+ (1) (@ (1))) (1))))
(67 (paramod 44 (1 1) 66 (1 1 2)) ((= (+ (1) (0)) (1))))
(68 (instantiate 3 ((v0 . (0))(v1 . (1))(v2 . v66))) ((= (+ (* (0) (1)) (+ (* (1) v66) (* v66 (0)))) (* (+ (0) (1)) (* (+ (1) v66) (+ v66 (0)))))))
(69 (paramod 41 (1 1) 68 (1 1 1)) ((= (+ (0) (+ (* (1) v66) (* v66 (0)))) (* (+ (0) (1)) (* (+ (1) v66) (+ v66 (0)))))))
(70 (instantiate 14 ((v0 . v66))) ((= (* (1) v66) v66)))
(71 (paramod 70 (1 1) 69 (1 1 2 1)) ((= (+ (0) (+ v66 (* v66 (0)))) (* (+ (0) (1)) (* (+ (1) v66) (+ v66 (0)))))))
(72 (instantiate 33 ((v0 . v66)(v1 . (0)))) ((= (+ v66 (* v66 (0))) v66)))
(73 (paramod 72 (1 1) 71 (1 1 2)) ((= (+ (0) v66) (* (+ (0) (1)) (* (+ (1) v66) (+ v66 (0)))))))
(74 (instantiate 16 ((v0 . v66))) ((= (+ (0) v66) v66)))
(75 (paramod 74 (1 1) 73 (1 1)) ((= v66 (* (+ (0) (1)) (* (+ (1) v66) (+ v66 (0)))))))
(76 (instantiate 16 ((v0 . (1)))) ((= (+ (0) (1)) (1))))
(77 (paramod 76 (1 1) 75 (1 2 1)) ((= v66 (* (1) (* (+ (1) v66) (+ v66 (0)))))))
(78 (instantiate 14 ((v0 . (* (+ (1) v66) (+ v66 (0)))))) ((= (* (1) (* (+ (1) v66) (+ v66 (0)))) (* (+ (1) v66) (+ v66 (0))))))
(79 (paramod 78 (1 1) 77 (1 2)) ((= v66 (* (+ (1) v66) (+ v66 (0))))))
(80 (flip 79 (1)) ((= (* (+ (1) v66) (+ v66 (0))) v66)))
(81 (instantiate 80 ((v66 . v0))) ((= (* (+ (1) v0) (+ v0 (0))) v0)))
(82 (instantiate 7 ((v0 . (1))(v1 . v65)(v2 . (0)))) ((= (* (1) (+ v65 (+ (1) (0)))) (1))))
(83 (paramod 67 (1 1) 82 (1 1 2 2)) ((= (* (1) (+ v65 (1))) (1))))
(84 (instantiate 14 ((v0 . (+ v65 (1))))) ((= (* (1) (+ v65 (1))) (+ v65 (1)))))
(85 (paramod 84 (1 1) 83 (1 1)) ((= (+ v65 (1)) (1))))
(86 (instantiate 85 ((v65 . v0))) ((= (+ v0 (1)) (1))))
(87 (instantiate 9 ((v0 . v64))) ((= (+ v64 (@ v64)) (1))))
(88 (instantiate 7 ((v0 . v64)(v1 . v65)(v2 . (@ v64)))) ((= (* v64 (+ v65 (+ v64 (@ v64)))) v64)))
(89 (paramod 87 (1 1) 88 (1 1 2 2)) ((= (* v64 (+ v65 (1))) v64)))
(90 (instantiate 86 ((v0 . v65))) ((= (+ v65 (1)) (1))))
(91 (paramod 90 (1 1) 89 (1 1 2)) ((= (* v64 (1)) v64)))
(92 (instantiate 91 ((v64 . v0))) ((= (* v0 (1)) v0)))
(93 (instantiate 4 ((v0 . v64))) ((= (+ v64 (* v1 (* v64 v2))) v64)))
(94 (instantiate 7 ((v0 . v64)(v1 . v65)(v2 . (* v1 (* v64 v2))))) ((= (* v64 (+ v65 (+ v64 (* v1 (* v64 v2))))) v64)))
(95 (paramod 93 (1 1) 94 (1 1 2 2)) ((= (* v64 (+ v65 v64)) v64)))
(96 (instantiate 95 ((v64 . v0)(v65 . v1))) ((= (* v0 (+ v1 v0)) v0)))
(97 (instantiate 16 ((v0 . (+ v64 v66)))) ((= (+ (0) (+ v64 v66)) (+ v64 v66))))
(98 (instantiate 7 ((v0 . v64)(v1 . (0))(v2 . v66))) ((= (* v64 (+ (0) (+ v64 v66))) v64)))
(99 (paramod 97 (1 1) 98 (1 1 2)) ((= (* v64 (+ v64 v66)) v64)))
(100 (instantiate 99 ((v64 . v0)(v66 . v1))) ((= (* v0 (+ v0 v1)) v0)))
(101 (paramod 92 (1 1) 39 (1 1 1)) ((= (+ v0 v1) (* (+ v0 (1)) (* (+ (1) v1) (+ v1 v0))))))
(102 (paramod 86 (1 1) 101 (1 2 1)) ((= (+ v0 v1) (* (1) (* (+ (1) v1) (+ v1 v0))))))
(103 (instantiate 14 ((v0 . (* (+ (1) v1) (+ v1 v0))))) ((= (* (1) (* (+ (1) v1) (+ v1 v0))) (* (+ (1) v1) (+ v1 v0)))))
(104 (paramod 103 (1 1) 102 (1 2)) ((= (+ v0 v1) (* (+ (1) v1) (+ v1 v0)))))
(105 (instantiate 7 ((v0 . v64))) ((= (* v64 (+ v1 (+ v64 v2))) v64)))
(106 (instantiate 4 ((v0 . v64)(v1 . v65)(v2 . (+ v1 (+ v64 v2))))) ((= (+ v64 (* v65 (* v64 (+ v1 (+ v64 v2))))) v64)))
(107 (paramod 105 (1 1) 106 (1 1 2 2)) ((= (+ v64 (* v65 v64)) v64)))
(108 (instantiate 107 ((v64 . v0)(v65 . v1))) ((= (+ v0 (* v1 v0)) v0)))
(109 (instantiate 92 ((v0 . v64))) ((= (* v64 (1)) v64)))
(110 (instantiate 29 ((v0 . v64)(v1 . (1)))) ((= (+ (1) (* v64 (1))) (1))))
(111 (paramod 109 (1 1) 110 (1 1 2)) ((= (+ (1) v64) (1))))
(112 (instantiate 111 ((v64 . v0))) ((= (+ (1) v0) (1))))
(113 (instantiate 112 ((v0 . v1))) ((= (+ (1) v1) (1))))
(114 (paramod 113 (1 1) 104 (1 2 1)) ((= (+ v0 v1) (* (1) (+ v1 v0)))))
(115 (instantiate 14 ((v0 . (+ v1 v0)))) ((= (* (1) (+ v1 v0)) (+ v1 v0))))
(116 (paramod 115 (1 1) 114 (1 2)) ((= (+ v0 v1) (+ v1 v0))))
(117 (paramod 112 (1 1) 81 (1 1 1)) ((= (* (1) (+ v0 (0))) v0)))
(118 (instantiate 14 ((v0 . (+ v0 (0))))) ((= (* (1) (+ v0 (0))) (+ v0 (0)))))
(119 (paramod 118 (1 1) 117 (1 1)) ((= (+ v0 (0)) v0)))
(120 (instantiate 4 ((v0 . v64))) ((= (+ v64 (* v1 (* v64 v2))) v64)))
(121 (instantiate 11 ((v0 . v64)(v1 . (* v1 (* v64 v2)))(v2 . v66))) ((= (+ (+ v64 (* v1 (* v64 v2))) v66) (+ v64 (+ (* v1 (* v64 v2)) v66)))))
(122 (paramod 120 (1 1) 121 (1 1 1)) ((= (+ v64 v66) (+ v64 (+ (* v1 (* v64 v2)) v66)))))
(123 (flip 122 (1)) ((= (+ v64 (+ (* v1 (* v64 v2)) v66)) (+ v64 v66))))
(124 (instantiate 123 ((v64 . v0)(v66 . v3))) ((= (+ v0 (+ (* v1 (* v0 v2)) v3)) (+ v0 v3))))
(125 (instantiate 92 ((v0 . v64))) ((= (* v64 (1)) v64)))
(126 (instantiate 33 ((v0 . v64)(v1 . (1)))) ((= (+ v64 (* v64 (1))) v64)))
(127 (paramod 125 (1 1) 126 (1 1 2)) ((= (+ v64 v64) v64)))
(128 (instantiate 127 ((v64 . v0))) ((= (+ v0 v0) v0)))
(129 (instantiate 16 ((v0 . (* (0) v65)))) ((= (+ (0) (* (0) v65)) (* (0) v65))))
(130 (instantiate 33 ((v0 . (0))(v1 . v65))) ((= (+ (0) (* (0) v65)) (0))))
(131 (paramod 129 (1 1) 130 (1 1)) ((= (* (0) v65) (0))))
(132 (instantiate 131 ((v65 . v0))) ((= (* (0) v0) (0))))
(133 (instantiate 132 ((v0 . v1))) ((= (* (0) v1) (0))))
(134 (paramod 133 (1 1) 37 (1 1 2)) ((= (* v0 (0)) (0))))
(135 (instantiate 33 ((v0 . v64))) ((= (+ v64 (* v64 v1)) v64)))
(136 (instantiate 11 ((v0 . v64)(v1 . (* v64 v1))(v2 . v66))) ((= (+ (+ v64 (* v64 v1)) v66) (+ v64 (+ (* v64 v1) v66)))))
(137 (paramod 135 (1 1) 136 (1 1 1)) ((= (+ v64 v66) (+ v64 (+ (* v64 v1) v66)))))
(138 (flip 137 (1)) ((= (+ v64 (+ (* v64 v1) v66)) (+ v64 v66))))
(139 (instantiate 138 ((v64 . v0)(v66 . v2))) ((= (+ v0 (+ (* v0 v1) v2)) (+ v0 v2))))
(140 (instantiate 132 ((v0 . v66))) ((= (* (0) v66) (0))))
(141 (instantiate 3 ((v0 . v64)(v1 . (0))(v2 . v66))) ((= (+ (* v64 (0)) (+ (* (0) v66) (* v66 v64))) (* (+ v64 (0)) (* (+ (0) v66) (+ v66 v64))))))
(142 (paramod 140 (1 1) 141 (1 1 2 1)) ((= (+ (* v64 (0)) (+ (0) (* v66 v64))) (* (+ v64 (0)) (* (+ (0) v66) (+ v66 v64))))))
(143 (instantiate 134 ((v0 . v64))) ((= (* v64 (0)) (0))))
(144 (paramod 143 (1 1) 142 (1 1 1)) ((= (+ (0) (+ (0) (* v66 v64))) (* (+ v64 (0)) (* (+ (0) v66) (+ v66 v64))))))
(145 (instantiate 16 ((v0 . (* v66 v64)))) ((= (+ (0) (* v66 v64)) (* v66 v64))))
(146 (paramod 145 (1 1) 144 (1 1 2)) ((= (+ (0) (* v66 v64)) (* (+ v64 (0)) (* (+ (0) v66) (+ v66 v64))))))
(147 (instantiate 16 ((v0 . (* v66 v64)))) ((= (+ (0) (* v66 v64)) (* v66 v64))))
(148 (paramod 147 (1 1) 146 (1 1)) ((= (* v66 v64) (* (+ v64 (0)) (* (+ (0) v66) (+ v66 v64))))))
(149 (instantiate 119 ((v0 . v64))) ((= (+ v64 (0)) v64)))
(150 (paramod 149 (1 1) 148 (1 2 1)) ((= (* v66 v64) (* v64 (* (+ (0) v66) (+ v66 v64))))))
(151 (instantiate 16 ((v0 . v66))) ((= (+ (0) v66) v66)))
(152 (paramod 151 (1 1) 150 (1 2 2 1)) ((= (* v66 v64) (* v64 (* v66 (+ v66 v64))))))
(153 (instantiate 100 ((v0 . v66)(v1 . v64))) ((= (* v66 (+ v66 v64)) v66)))
(154 (paramod 153 (1 1) 152 (1 2 2)) ((= (* v66 v64) (* v64 v66))))
(155 (instantiate 154 ((v64 . v1)(v66 . v0))) ((= (* v0 v1) (* v1 v0))))
(156 (instantiate 10 ((v0 . v64))) ((= (* v64 (@ v64)) (0))))
(157 (instantiate 12 ((v0 . v64)(v1 . (@ v64))(v2 . v66))) ((= (* (* v64 (@ v64)) v66) (* v64 (* (@ v64) v66)))))
(158 (paramod 156 (1 1) 157 (1 1 1)) ((= (* (0) v66) (* v64 (* (@ v64) v66)))))
(159 (instantiate 132 ((v0 . v66))) ((= (* (0) v66) (0))))
(160 (paramod 159 (1 1) 158 (1 1)) ((= (0) (* v64 (* (@ v64) v66)))))
(161 (flip 160 (1)) ((= (* v64 (* (@ v64) v66)) (0))))
(162 (instantiate 161 ((v64 . v0)(v66 . v1))) ((= (* v0 (* (@ v0) v1)) (0))))
(163 (instantiate 128 ((v0 . v64))) ((= (+ v64 v64) v64)))
(164 (instantiate 96 ((v0 . v64)(v1 . v64))) ((= (* v64 (+ v64 v64)) v64)))
(165 (paramod 163 (1 1) 164 (1 1 2)) ((= (* v64 v64) v64)))
(166 (instantiate 165 ((v64 . v0))) ((= (* v0 v0) v0)))
(167 (instantiate 96 ((v0 . v64))) ((= (* v64 (+ v1 v64)) v64)))
(168 (instantiate 12 ((v0 . v64)(v1 . (+ v1 v64))(v2 . v66))) ((= (* (* v64 (+ v1 v64)) v66) (* v64 (* (+ v1 v64) v66)))))
(169 (paramod 167 (1 1) 168 (1 1 1)) ((= (* v64 v66) (* v64 (* (+ v1 v64) v66)))))
(170 (flip 169 (1)) ((= (* v64 (* (+ v1 v64) v66)) (* v64 v66))))
(171 (instantiate 170 ((v64 . v0)(v66 . v2))) ((= (* v0 (* (+ v1 v0) v2)) (* v0 v2))))
(172 (instantiate 166 ((v0 . v64))) ((= (* v64 v64) v64)))
(173 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . v64))) ((= (+ (* v64 v65) (+ (* v65 v64) (* v64 v64))) (* (+ v64 v65) (* (+ v65 v64) (+ v64 v64))))))
(174 (paramod 172 (1 1) 173 (1 1 2 2)) ((= (+ (* v64 v65) (+ (* v65 v64) v64)) (* (+ v64 v65) (* (+ v65 v64) (+ v64 v64))))))
(175 (instantiate 128 ((v0 . v64))) ((= (+ v64 v64) v64)))
(176 (paramod 175 (1 1) 174 (1 2 2 2)) ((= (+ (* v64 v65) (+ (* v65 v64) v64)) (* (+ v64 v65) (* (+ v65 v64) v64)))))
(177 (instantiate 176 ((v64 . v0)(v65 . v1))) ((= (+ (* v0 v1) (+ (* v1 v0) v0)) (* (+ v0 v1) (* (+ v1 v0) v0)))))
(178 (instantiate 166 ((v0 . v66))) ((= (* v66 v66) v66)))
(179 (instantiate 3 ((v0 . v64)(v1 . v66)(v2 . v66))) ((= (+ (* v64 v66) (+ (* v66 v66) (* v66 v64))) (* (+ v64 v66) (* (+ v66 v66) (+ v66 v64))))))
(180 (paramod 178 (1 1) 179 (1 1 2 1)) ((= (+ (* v64 v66) (+ v66 (* v66 v64))) (* (+ v64 v66) (* (+ v66 v66) (+ v66 v64))))))
(181 (instantiate 33 ((v0 . v66)(v1 . v64))) ((= (+ v66 (* v66 v64)) v66)))
(182 (paramod 181 (1 1) 180 (1 1 2)) ((= (+ (* v64 v66) v66) (* (+ v64 v66) (* (+ v66 v66) (+ v66 v64))))))
(183 (instantiate 128 ((v0 . v66))) ((= (+ v66 v66) v66)))
(184 (paramod 183 (1 1) 182 (1 2 2 1)) ((= (+ (* v64 v66) v66) (* (+ v64 v66) (* v66 (+ v66 v64))))))
(185 (instantiate 100 ((v0 . v66)(v1 . v64))) ((= (* v66 (+ v66 v64)) v66)))
(186 (paramod 185 (1 1) 184 (1 2 2)) ((= (+ (* v64 v66) v66) (* (+ v64 v66) v66))))
(187 (instantiate 186 ((v64 . v0)(v66 . v1))) ((= (+ (* v0 v1) v1) (* (+ v0 v1) v1))))
(188 (instantiate 166 ((v0 . v65))) ((= (* v65 v65) v65)))
(189 (instantiate 12 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (* (* v65 v65) v66) (* v65 (* v65 v66)))))
(190 (paramod 188 (1 1) 189 (1 1 1)) ((= (* v65 v66) (* v65 (* v65 v66)))))
(191 (flip 190 (1)) ((= (* v65 (* v65 v66)) (* v65 v66))))
(192 (instantiate 191 ((v65 . v0)(v66 . v1))) ((= (* v0 (* v0 v1)) (* v0 v1))))
(193 (instantiate 187 ((v0 . v1)(v1 . v0))) ((= (+ (* v1 v0) v0) (* (+ v1 v0) v0))))
(194 (paramod 193 (1 1) 177 (1 1 2)) ((= (+ (* v0 v1) (* (+ v1 v0) v0)) (* (+ v0 v1) (* (+ v1 v0) v0)))))
(195 (instantiate 187 ((v0 . (A))(v1 . (B)))) ((= (+ (* (A) (B)) (B)) (* (+ (A) (B)) (B)))))
(196 (paramod 195 (1 1) 2 (2 1 1)) ((not (= (+ (* (A) (B)) (* (A) (C))) (* (A) (+ (B) (C))))) (not (= (* (+ (A) (B)) (B)) (B)))))
(197 (instantiate 100 ((v0 . (* v0 v1))(v1 . (+ (* v1 v2) (* v2 v0))))) ((= (* (* v0 v1) (+ (* v0 v1) (+ (* v1 v2) (* v2 v0)))) (* v0 v1))))
(198 (paramod 3 (1 1) 197 (1 1 2)) ((= (* (* v0 v1) (* (+ v0 v1) (* (+ v1 v2) (+ v2 v0)))) (* v0 v1))))
(199 (instantiate 12 ((v0 . v0)(v1 . v1)(v2 . (* (+ v0 v1) (* (+ v1 v2) (+ v2 v0)))))) ((= (* (* v0 v1) (* (+ v0 v1) (* (+ v1 v2) (+ v2 v0)))) (* v0 (* v1 (* (+ v0 v1) (* (+ v1 v2) (+ v2 v0))))))))
(200 (paramod 199 (1 1) 198 (1 1)) ((= (* v0 (* v1 (* (+ v0 v1) (* (+ v1 v2) (+ v2 v0))))) (* v0 v1))))
(201 (instantiate 171 ((v0 . v1)(v1 . v0)(v2 . (* (+ v1 v2) (+ v2 v0))))) ((= (* v1 (* (+ v0 v1) (* (+ v1 v2) (+ v2 v0)))) (* v1 (* (+ v1 v2) (+ v2 v0))))))
(202 (paramod 201 (1 1) 200 (1 1 2)) ((= (* v0 (* v1 (* (+ v1 v2) (+ v2 v0)))) (* v0 v1))))
(203 (instantiate 100 ((v0 . v64))) ((= (* v64 (+ v64 v1)) v64)))
(204 (instantiate 12 ((v0 . v64)(v1 . (+ v64 v1))(v2 . v66))) ((= (* (* v64 (+ v64 v1)) v66) (* v64 (* (+ v64 v1) v66)))))
(205 (paramod 203 (1 1) 204 (1 1 1)) ((= (* v64 v66) (* v64 (* (+ v64 v1) v66)))))
(206 (flip 205 (1)) ((= (* v64 (* (+ v64 v1) v66)) (* v64 v66))))
(207 (instantiate 206 ((v64 . v0)(v66 . v2))) ((= (* v0 (* (+ v0 v1) v2)) (* v0 v2))))
(208 (instantiate 207 ((v0 . v1)(v1 . v2)(v2 . (+ v2 v0)))) ((= (* v1 (* (+ v1 v2) (+ v2 v0))) (* v1 (+ v2 v0)))))
(209 (paramod 208 (1 1) 202 (1 1 2)) ((= (* v0 (* v1 (+ v2 v0))) (* v0 v1))))
(210 (instantiate 132 ((v0 . v65))) ((= (* (0) v65) (0))))
(211 (instantiate 18 ((v0 . (0))(v1 . v65)(v2 . v66))) ((= (+ (* (0) v65) (+ (* v65 v66) v65)) v65)))
(212 (paramod 210 (1 1) 211 (1 1 1)) ((= (+ (0) (+ (* v65 v66) v65)) v65)))
(213 (instantiate 16 ((v0 . (+ (* v65 v66) v65)))) ((= (+ (0) (+ (* v65 v66) v65)) (+ (* v65 v66) v65))))
(214 (paramod 213 (1 1) 212 (1 1)) ((= (+ (* v65 v66) v65) v65)))
(215 (instantiate 214 ((v65 . v0)(v66 . v1))) ((= (+ (* v0 v1) v0) v0)))
(216 (instantiate 96 ((v0 . v64))) ((= (* v64 (+ v1 v64)) v64)))
(217 (instantiate 18 ((v0 . v64)(v1 . (+ v1 v64))(v2 . v66))) ((= (+ (* v64 (+ v1 v64)) (+ (* (+ v1 v64) v66) (+ v1 v64))) (+ v1 v64))))
(218 (paramod 216 (1 1) 217 (1 1 1)) ((= (+ v64 (+ (* (+ v1 v64) v66) (+ v1 v64))) (+ v1 v64))))
(219 (instantiate 215 ((v0 . (+ v1 v64))(v1 . v66))) ((= (+ (* (+ v1 v64) v66) (+ v1 v64)) (+ v1 v64))))
(220 (paramod 219 (1 1) 218 (1 1 2)) ((= (+ v64 (+ v1 v64)) (+ v1 v64))))
(221 (instantiate 220 ((v64 . v0))) ((= (+ v0 (+ v1 v0)) (+ v1 v0))))
(222 (instantiate 166 ((v0 . v66))) ((= (* v66 v66) v66)))
(223 (instantiate 18 ((v0 . v64)(v1 . v66)(v2 . v66))) ((= (+ (* v64 v66) (+ (* v66 v66) v66)) v66)))
(224 (paramod 222 (1 1) 223 (1 1 2 1)) ((= (+ (* v64 v66) (+ v66 v66)) v66)))
(225 (instantiate 128 ((v0 . v66))) ((= (+ v66 v66) v66)))
(226 (paramod 225 (1 1) 224 (1 1 2)) ((= (+ (* v64 v66) v66) v66)))
(227 (instantiate 187 ((v0 . v64)(v1 . v66))) ((= (+ (* v64 v66) v66) (* (+ v64 v66) v66))))
(228 (paramod 227 (1 1) 226 (1 1)) ((= (* (+ v64 v66) v66) v66)))
(229 (instantiate 228 ((v64 . v0)(v66 . v1))) ((= (* (+ v0 v1) v1) v1)))
(230 (instantiate 229 ((v0 . (A))(v1 . (B)))) ((= (* (+ (A) (B)) (B)) (B))))
(231 (paramod 230 (1 1) 196 (2 1 1)) ((not (= (+ (* (A) (B)) (* (A) (C))) (* (A) (+ (B) (C))))) (not (= (B) (B)))))
(232 (instantiate 1 ((v0 . (B)))) ((= (B) (B))))
(233 (resolve 231 (2) 232 (1)) ((not (= (+ (* (A) (B)) (* (A) (C))) (* (A) (+ (B) (C)))))))
(234 (instantiate 229 ((v0 . v1)(v1 . v0))) ((= (* (+ v1 v0) v0) v0)))
(235 (paramod 234 (1 1) 194 (1 1 2)) ((= (+ (* v0 v1) v0) (* (+ v0 v1) (* (+ v1 v0) v0)))))
(236 (paramod 215 (1 1) 235 (1 1)) ((= v0 (* (+ v0 v1) (* (+ v1 v0) v0)))))
(237 (instantiate 229 ((v0 . v1)(v1 . v0))) ((= (* (+ v1 v0) v0) v0)))
(238 (paramod 237 (1 1) 236 (1 2 2)) ((= v0 (* (+ v0 v1) v0))))
(239 (flip 238 (1)) ((= (* (+ v0 v1) v0) v0)))
(240 (paramod 229 (1 1) 187 (1 2)) ((= (+ (* v0 v1) v1) v1)))
(241 (instantiate 11 ((v2 . (* v65 (+ v0 v1))))) ((= (+ (+ v0 v1) (* v65 (+ v0 v1))) (+ v0 (+ v1 (* v65 (+ v0 v1)))))))
(242 (instantiate 108 ((v0 . (+ v0 v1))(v1 . v65))) ((= (+ (+ v0 v1) (* v65 (+ v0 v1))) (+ v0 v1))))
(243 (paramod 241 (1 1) 242 (1 1)) ((= (+ v0 (+ v1 (* v65 (+ v0 v1)))) (+ v0 v1))))
(244 (instantiate 243 ((v65 . v2))) ((= (+ v0 (+ v1 (* v2 (+ v0 v1)))) (+ v0 v1))))
(245 (instantiate 108 ((v0 . v64))) ((= (+ v64 (* v1 v64)) v64)))
(246 (instantiate 11 ((v0 . v64)(v1 . (* v1 v64))(v2 . v66))) ((= (+ (+ v64 (* v1 v64)) v66) (+ v64 (+ (* v1 v64) v66)))))
(247 (paramod 245 (1 1) 246 (1 1 1)) ((= (+ v64 v66) (+ v64 (+ (* v1 v64) v66)))))
(248 (flip 247 (1)) ((= (+ v64 (+ (* v1 v64) v66)) (+ v64 v66))))
(249 (instantiate 248 ((v64 . v0)(v66 . v2))) ((= (+ v0 (+ (* v1 v0) v2)) (+ v0 v2))))
(250 (instantiate 11 ((v2 . v65))) ((= (+ (+ v0 v1) v65) (+ v0 (+ v1 v65)))))
(251 (instantiate 116 ((v0 . (+ v0 v1))(v1 . v65))) ((= (+ (+ v0 v1) v65) (+ v65 (+ v0 v1)))))
(252 (paramod 250 (1 1) 251 (1 1)) ((= (+ v0 (+ v1 v65)) (+ v65 (+ v0 v1)))))
(253 (instantiate 252 ((v65 . v2))) ((= (+ v0 (+ v1 v2)) (+ v2 (+ v0 v1)))))
(254 (instantiate 9 ((v0 . v64))) ((= (+ v64 (@ v64)) (1))))
(255 (instantiate 116 ((v0 . v64)(v1 . (@ v64)))) ((= (+ v64 (@ v64)) (+ (@ v64) v64))))
(256 (paramod 254 (1 1) 255 (1 1)) ((= (1) (+ (@ v64) v64))))
(257 (flip 256 (1)) ((= (+ (@ v64) v64) (1))))
(258 (instantiate 257 ((v64 . v0))) ((= (+ (@ v0) v0) (1))))
(259 (instantiate 4 ((v0 . v64))) ((= (+ v64 (* v1 (* v64 v2))) v64)))
(260 (instantiate 116 ((v0 . v64)(v1 . (* v1 (* v64 v2))))) ((= (+ v64 (* v1 (* v64 v2))) (+ (* v1 (* v64 v2)) v64))))
(261 (paramod 259 (1 1) 260 (1 1)) ((= v64 (+ (* v1 (* v64 v2)) v64))))
(262 (flip 261 (1)) ((= (+ (* v1 (* v64 v2)) v64) v64)))
(263 (instantiate 262 ((v1 . v0)(v64 . v1))) ((= (+ (* v0 (* v1 v2)) v1) v1)))
(264 (flip 253 (1)) ((= (+ v2 (+ v0 v1)) (+ v0 (+ v1 v2)))))
(265 (instantiate 12 ((v2 . v65))) ((= (* (* v0 v1) v65) (* v0 (* v1 v65)))))
(266 (instantiate 155 ((v0 . (* v0 v1))(v1 . v65))) ((= (* (* v0 v1) v65) (* v65 (* v0 v1)))))
(267 (paramod 265 (1 1) 266 (1 1)) ((= (* v0 (* v1 v65)) (* v65 (* v0 v1)))))
(268 (instantiate 267 ((v65 . v2))) ((= (* v0 (* v1 v2)) (* v2 (* v0 v1)))))
(269 (instantiate 7 ((v0 . v64))) ((= (* v64 (+ v1 (+ v64 v2))) v64)))
(270 (instantiate 155 ((v0 . v64)(v1 . (+ v1 (+ v64 v2))))) ((= (* v64 (+ v1 (+ v64 v2))) (* (+ v1 (+ v64 v2)) v64))))
(271 (paramod 269 (1 1) 270 (1 1)) ((= v64 (* (+ v1 (+ v64 v2)) v64))))
(272 (flip 271 (1)) ((= (* (+ v1 (+ v64 v2)) v64) v64)))
(273 (instantiate 272 ((v1 . v0)(v64 . v1))) ((= (* (+ v0 (+ v1 v2)) v1) v1)))
(274 (instantiate 155 ((v0 . v66)(v1 . v64))) ((= (* v66 v64) (* v64 v66))))
(275 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (+ (* v64 v65) (+ (* v65 v66) (* v66 v64))) (* (+ v64 v65) (* (+ v65 v66) (+ v66 v64))))))
(276 (paramod 274 (1 1) 275 (1 1 2 2)) ((= (+ (* v64 v65) (+ (* v65 v66) (* v64 v66))) (* (+ v64 v65) (* (+ v65 v66) (+ v66 v64))))))
(277 (instantiate 276 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (+ (* v0 v1) (+ (* v1 v2) (* v0 v2))) (* (+ v0 v1) (* (+ v1 v2) (+ v2 v0))))))
(278 (instantiate 10 ((v0 . v64))) ((= (* v64 (@ v64)) (0))))
(279 (instantiate 54 ((v0 . v64)(v1 . (@ v64)))) ((= (+ (* v64 (@ v64)) (* (@ (@ v64)) v64)) (* (+ v64 (@ v64)) (+ (@ (@ v64)) v64)))))
(280 (paramod 278 (1 1) 279 (1 1 1)) ((= (+ (0) (* (@ (@ v64)) v64)) (* (+ v64 (@ v64)) (+ (@ (@ v64)) v64)))))
(281 (instantiate 16 ((v0 . (* (@ (@ v64)) v64)))) ((= (+ (0) (* (@ (@ v64)) v64)) (* (@ (@ v64)) v64))))
(282 (paramod 281 (1 1) 280 (1 1)) ((= (* (@ (@ v64)) v64) (* (+ v64 (@ v64)) (+ (@ (@ v64)) v64)))))
(283 (instantiate 9 ((v0 . v64))) ((= (+ v64 (@ v64)) (1))))
(284 (paramod 283 (1 1) 282 (1 2 1)) ((= (* (@ (@ v64)) v64) (* (1) (+ (@ (@ v64)) v64)))))
(285 (instantiate 14 ((v0 . (+ (@ (@ v64)) v64)))) ((= (* (1) (+ (@ (@ v64)) v64)) (+ (@ (@ v64)) v64))))
(286 (paramod 285 (1 1) 284 (1 2)) ((= (* (@ (@ v64)) v64) (+ (@ (@ v64)) v64))))
(287 (flip 286 (1)) ((= (+ (@ (@ v64)) v64) (* (@ (@ v64)) v64))))
(288 (instantiate 287 ((v64 . v0))) ((= (+ (@ (@ v0)) v0) (* (@ (@ v0)) v0))))
(289 (instantiate 155 ((v0 . (@ v65))(v1 . v64))) ((= (* (@ v65) v64) (* v64 (@ v65)))))
(290 (instantiate 54 ((v0 . v64)(v1 . v65))) ((= (+ (* v64 v65) (* (@ v65) v64)) (* (+ v64 v65) (+ (@ v65) v64)))))
(291 (paramod 289 (1 1) 290 (1 1 2)) ((= (+ (* v64 v65) (* v64 (@ v65))) (* (+ v64 v65) (+ (@ v65) v64)))))
(292 (instantiate 291 ((v64 . v0)(v65 . v1))) ((= (+ (* v0 v1) (* v0 (@ v1))) (* (+ v0 v1) (+ (@ v1) v0)))))
(293 (instantiate 96 ((v0 . (@ v65)))) ((= (* (@ v65) (+ v1 (@ v65))) (@ v65))))
(294 (instantiate 54 ((v0 . (+ v1 (@ v65)))(v1 . v65))) ((= (+ (* (+ v1 (@ v65)) v65) (* (@ v65) (+ v1 (@ v65)))) (* (+ (+ v1 (@ v65)) v65) (+ (@ v65) (+ v1 (@ v65)))))))
(295 (paramod 293 (1 1) 294 (1 1 2)) ((= (+ (* (+ v1 (@ v65)) v65) (@ v65)) (* (+ (+ v1 (@ v65)) v65) (+ (@ v65) (+ v1 (@ v65)))))))
(296 (instantiate 11 ((v0 . v1)(v1 . (@ v65))(v2 . v65))) ((= (+ (+ v1 (@ v65)) v65) (+ v1 (+ (@ v65) v65)))))
(297 (paramod 296 (1 1) 295 (1 2 1)) ((= (+ (* (+ v1 (@ v65)) v65) (@ v65)) (* (+ v1 (+ (@ v65) v65)) (+ (@ v65) (+ v1 (@ v65)))))))
(298 (instantiate 258 ((v0 . v65))) ((= (+ (@ v65) v65) (1))))
(299 (paramod 298 (1 1) 297 (1 2 1 2)) ((= (+ (* (+ v1 (@ v65)) v65) (@ v65)) (* (+ v1 (1)) (+ (@ v65) (+ v1 (@ v65)))))))
(300 (instantiate 86 ((v0 . v1))) ((= (+ v1 (1)) (1))))
(301 (paramod 300 (1 1) 299 (1 2 1)) ((= (+ (* (+ v1 (@ v65)) v65) (@ v65)) (* (1) (+ (@ v65) (+ v1 (@ v65)))))))
(302 (instantiate 221 ((v0 . (@ v65))(v1 . v1))) ((= (+ (@ v65) (+ v1 (@ v65))) (+ v1 (@ v65)))))
(303 (paramod 302 (1 1) 301 (1 2 2)) ((= (+ (* (+ v1 (@ v65)) v65) (@ v65)) (* (1) (+ v1 (@ v65))))))
(304 (instantiate 14 ((v0 . (+ v1 (@ v65))))) ((= (* (1) (+ v1 (@ v65))) (+ v1 (@ v65)))))
(305 (paramod 304 (1 1) 303 (1 2)) ((= (+ (* (+ v1 (@ v65)) v65) (@ v65)) (+ v1 (@ v65)))))
(306 (instantiate 305 ((v1 . v0)(v65 . v1))) ((= (+ (* (+ v0 (@ v1)) v1) (@ v1)) (+ v0 (@ v1)))))
(307 (flip 292 (1)) ((= (* (+ v0 v1) (+ (@ v1) v0)) (+ (* v0 v1) (* v0 (@ v1))))))
(308 (instantiate 229 ((v1 . v65))) ((= (* (+ v0 v65) v65) v65)))
(309 (instantiate 3 ((v0 . (+ v0 v65))(v1 . v65)(v2 . v66))) ((= (+ (* (+ v0 v65) v65) (+ (* v65 v66) (* v66 (+ v0 v65)))) (* (+ (+ v0 v65) v65) (* (+ v65 v66) (+ v66 (+ v0 v65)))))))
(310 (paramod 308 (1 1) 309 (1 1 1)) ((= (+ v65 (+ (* v65 v66) (* v66 (+ v0 v65)))) (* (+ (+ v0 v65) v65) (* (+ v65 v66) (+ v66 (+ v0 v65)))))))
(311 (instantiate 139 ((v0 . v65)(v1 . v66)(v2 . (* v66 (+ v0 v65))))) ((= (+ v65 (+ (* v65 v66) (* v66 (+ v0 v65)))) (+ v65 (* v66 (+ v0 v65))))))
(312 (paramod 311 (1 1) 310 (1 1)) ((= (+ v65 (* v66 (+ v0 v65))) (* (+ (+ v0 v65) v65) (* (+ v65 v66) (+ v66 (+ v0 v65)))))))
(313 (instantiate 11 ((v0 . v0)(v1 . v65)(v2 . v65))) ((= (+ (+ v0 v65) v65) (+ v0 (+ v65 v65)))))
(314 (paramod 313 (1 1) 312 (1 2 1)) ((= (+ v65 (* v66 (+ v0 v65))) (* (+ v0 (+ v65 v65)) (* (+ v65 v66) (+ v66 (+ v0 v65)))))))
(315 (instantiate 128 ((v0 . v65))) ((= (+ v65 v65) v65)))
(316 (paramod 315 (1 1) 314 (1 2 1 2)) ((= (+ v65 (* v66 (+ v0 v65))) (* (+ v0 v65) (* (+ v65 v66) (+ v66 (+ v0 v65)))))))
(317 (instantiate 209 ((v0 . (+ v0 v65))(v1 . (+ v65 v66))(v2 . v66))) ((= (* (+ v0 v65) (* (+ v65 v66) (+ v66 (+ v0 v65)))) (* (+ v0 v65) (+ v65 v66)))))
(318 (paramod 317 (1 1) 316 (1 2)) ((= (+ v65 (* v66 (+ v0 v65))) (* (+ v0 v65) (+ v65 v66)))))
(319 (instantiate 318 ((v0 . v2)(v65 . v0)(v66 . v1))) ((= (+ v0 (* v1 (+ v2 v0))) (* (+ v2 v0) (+ v0 v1)))))
(320 (instantiate 319 ((v0 . v1)(v1 . v2)(v2 . v0))) ((= (+ v1 (* v2 (+ v0 v1))) (* (+ v0 v1) (+ v1 v2)))))
(321 (paramod 320 (1 1) 244 (1 1 2)) ((= (+ v0 (* (+ v0 v1) (+ v1 v2))) (+ v0 v1))))
(322 (instantiate 116 ((v0 . (* (@ v64) v65))(v1 . (* v65 v64)))) ((= (+ (* (@ v64) v65) (* v65 v64)) (+ (* v65 v64) (* (@ v64) v65)))))
(323 (instantiate 64 ((v0 . v64)(v1 . v65))) ((= (+ (* (@ v64) v65) (* v65 v64)) (* (+ (@ v64) v65) (+ v65 v64)))))
(324 (paramod 322 (1 1) 323 (1 1)) ((= (+ (* v65 v64) (* (@ v64) v65)) (* (+ (@ v64) v65) (+ v65 v64)))))
(325 (instantiate 324 ((v64 . v1)(v65 . v0))) ((= (+ (* v0 v1) (* (@ v1) v0)) (* (+ (@ v1) v0) (+ v0 v1)))))
(326 (instantiate 155 ((v0 . (@ v64))(v1 . v65))) ((= (* (@ v64) v65) (* v65 (@ v64)))))
(327 (instantiate 162 ((v0 . v64)(v1 . v65))) ((= (* v64 (* (@ v64) v65)) (0))))
(328 (paramod 326 (1 1) 327 (1 1 2)) ((= (* v64 (* v65 (@ v64))) (0))))
(329 (instantiate 328 ((v64 . v0)(v65 . v1))) ((= (* v0 (* v1 (@ v0))) (0))))
(330 (instantiate 155 ((v0 . v64)(v1 . (* (@ v64) v65)))) ((= (* v64 (* (@ v64) v65)) (* (* (@ v64) v65) v64))))
(331 (instantiate 162 ((v0 . v64)(v1 . v65))) ((= (* v64 (* (@ v64) v65)) (0))))
(332 (paramod 330 (1 1) 331 (1 1)) ((= (* (* (@ v64) v65) v64) (0))))
(333 (instantiate 12 ((v0 . (@ v64))(v1 . v65)(v2 . v64))) ((= (* (* (@ v64) v65) v64) (* (@ v64) (* v65 v64)))))
(334 (paramod 333 (1 1) 332 (1 1)) ((= (* (@ v64) (* v65 v64)) (0))))
(335 (instantiate 334 ((v64 . v0)(v65 . v1))) ((= (* (@ v0) (* v1 v0)) (0))))
(336 (instantiate 116 ((v0 . (@ v65))(v1 . v64))) ((= (+ (@ v65) v64) (+ v64 (@ v65)))))
(337 (instantiate 65 ((v0 . v64)(v1 . v65))) ((= (* (+ v64 v65) (+ (@ v65) v64)) (+ (* v64 v65) (* (@ v65) v64)))))
(338 (paramod 336 (1 1) 337 (1 1 2)) ((= (* (+ v64 v65) (+ v64 (@ v65))) (+ (* v64 v65) (* (@ v65) v64)))))
(339 (flip 338 (1)) ((= (+ (* v64 v65) (* (@ v65) v64)) (* (+ v64 v65) (+ v64 (@ v65))))))
(340 (instantiate 339 ((v64 . v0)(v65 . v1))) ((= (+ (* v0 v1) (* (@ v1) v0)) (* (+ v0 v1) (+ v0 (@ v1))))))
(341 (paramod 340 (1 1) 325 (1 1)) ((= (* (+ v0 v1) (+ v0 (@ v1))) (* (+ (@ v1) v0) (+ v0 v1)))))
(342 (paramod 340 (1 1) 54 (1 1)) ((= (* (+ v0 v1) (+ v0 (@ v1))) (* (+ v0 v1) (+ (@ v1) v0)))))
(343 (instantiate 335 ((v0 . v64))) ((= (* (@ v64) (* v1 v64)) (0))))
(344 (instantiate 64 ((v0 . v64)(v1 . (* v1 v64)))) ((= (+ (* (@ v64) (* v1 v64)) (* (* v1 v64) v64)) (* (+ (@ v64) (* v1 v64)) (+ (* v1 v64) v64)))))
(345 (paramod 343 (1 1) 344 (1 1 1)) ((= (+ (0) (* (* v1 v64) v64)) (* (+ (@ v64) (* v1 v64)) (+ (* v1 v64) v64)))))
(346 (instantiate 12 ((v0 . v1)(v1 . v64)(v2 . v64))) ((= (* (* v1 v64) v64) (* v1 (* v64 v64)))))
(347 (paramod 346 (1 1) 345 (1 1 2)) ((= (+ (0) (* v1 (* v64 v64))) (* (+ (@ v64) (* v1 v64)) (+ (* v1 v64) v64)))))
(348 (instantiate 166 ((v0 . v64))) ((= (* v64 v64) v64)))
(349 (paramod 348 (1 1) 347 (1 1 2 2)) ((= (+ (0) (* v1 v64)) (* (+ (@ v64) (* v1 v64)) (+ (* v1 v64) v64)))))
(350 (instantiate 16 ((v0 . (* v1 v64)))) ((= (+ (0) (* v1 v64)) (* v1 v64))))
(351 (paramod 350 (1 1) 349 (1 1)) ((= (* v1 v64) (* (+ (@ v64) (* v1 v64)) (+ (* v1 v64) v64)))))
(352 (instantiate 240 ((v0 . v1)(v1 . v64))) ((= (+ (* v1 v64) v64) v64)))
(353 (paramod 352 (1 1) 351 (1 2 2)) ((= (* v1 v64) (* (+ (@ v64) (* v1 v64)) v64))))
(354 (flip 353 (1)) ((= (* (+ (@ v64) (* v1 v64)) v64) (* v1 v64))))
(355 (instantiate 354 ((v64 . v0))) ((= (* (+ (@ v0) (* v1 v0)) v0) (* v1 v0))))
(356 (instantiate 192 ((v0 . v64))) ((= (* v64 (* v64 v1)) (* v64 v1))))
(357 (instantiate 3 ((v0 . v64)(v1 . (* v64 v1))(v2 . v66))) ((= (+ (* v64 (* v64 v1)) (+ (* (* v64 v1) v66) (* v66 v64))) (* (+ v64 (* v64 v1)) (* (+ (* v64 v1) v66) (+ v66 v64))))))
(358 (paramod 356 (1 1) 357 (1 1 1)) ((= (+ (* v64 v1) (+ (* (* v64 v1) v66) (* v66 v64))) (* (+ v64 (* v64 v1)) (* (+ (* v64 v1) v66) (+ v66 v64))))))
(359 (instantiate 12 ((v0 . v64)(v1 . v1)(v2 . v66))) ((= (* (* v64 v1) v66) (* v64 (* v1 v66)))))
(360 (paramod 359 (1 1) 358 (1 1 2 1)) ((= (+ (* v64 v1) (+ (* v64 (* v1 v66)) (* v66 v64))) (* (+ v64 (* v64 v1)) (* (+ (* v64 v1) v66) (+ v66 v64))))))
(361 (instantiate 33 ((v0 . v64)(v1 . v1))) ((= (+ v64 (* v64 v1)) v64)))
(362 (paramod 361 (1 1) 360 (1 2 1)) ((= (+ (* v64 v1) (+ (* v64 (* v1 v66)) (* v66 v64))) (* v64 (* (+ (* v64 v1) v66) (+ v66 v64))))))
(363 (instantiate 209 ((v0 . v64)(v1 . (+ (* v64 v1) v66))(v2 . v66))) ((= (* v64 (* (+ (* v64 v1) v66) (+ v66 v64))) (* v64 (+ (* v64 v1) v66)))))
(364 (paramod 363 (1 1) 362 (1 2)) ((= (+ (* v64 v1) (+ (* v64 (* v1 v66)) (* v66 v64))) (* v64 (+ (* v64 v1) v66)))))
(365 (instantiate 364 ((v64 . v0)(v66 . v2))) ((= (+ (* v0 v1) (+ (* v0 (* v1 v2)) (* v2 v0))) (* v0 (+ (* v0 v1) v2)))))
(366 (instantiate 263 ((v1 . v66))) ((= (+ (* v0 (* v66 v2)) v66) v66)))
(367 (instantiate 273 ((v0 . v64)(v1 . (* v0 (* v66 v2)))(v2 . v66))) ((= (* (+ v64 (+ (* v0 (* v66 v2)) v66)) (* v0 (* v66 v2))) (* v0 (* v66 v2)))))
(368 (paramod 366 (1 1) 367 (1 1 1 2)) ((= (* (+ v64 v66) (* v0 (* v66 v2))) (* v0 (* v66 v2)))))
(369 (instantiate 368 ((v0 . v2)(v2 . v3)(v64 . v0)(v66 . v1))) ((= (* (+ v0 v1) (* v2 (* v1 v3))) (* v2 (* v1 v3)))))
(370 (instantiate 124 ((v0 . v64)(v3 . v66))) ((= (+ v64 (+ (* v1 (* v64 v2)) v66)) (+ v64 v66))))
(371 (instantiate 273 ((v0 . v64)(v1 . (* v1 (* v64 v2)))(v2 . v66))) ((= (* (+ v64 (+ (* v1 (* v64 v2)) v66)) (* v1 (* v64 v2))) (* v1 (* v64 v2)))))
(372 (paramod 370 (1 1) 371 (1 1 1)) ((= (* (+ v64 v66) (* v1 (* v64 v2))) (* v1 (* v64 v2)))))
(373 (instantiate 372 ((v1 . v2)(v2 . v3)(v64 . v0)(v66 . v1))) ((= (* (+ v0 v1) (* v2 (* v0 v3))) (* v2 (* v0 v3)))))
(374 (instantiate 273 ((v0 . (* v0 v1))(v1 . (* v1 v2))(v2 . (* v2 v0)))) ((= (* (+ (* v0 v1) (+ (* v1 v2) (* v2 v0))) (* v1 v2)) (* v1 v2))))
(375 (paramod 3 (1 1) 374 (1 1 1)) ((= (* (* (+ v0 v1) (* (+ v1 v2) (+ v2 v0))) (* v1 v2)) (* v1 v2))))
(376 (instantiate 12 ((v0 . (+ v0 v1))(v1 . (* (+ v1 v2) (+ v2 v0)))(v2 . (* v1 v2)))) ((= (* (* (+ v0 v1) (* (+ v1 v2) (+ v2 v0))) (* v1 v2)) (* (+ v0 v1) (* (* (+ v1 v2) (+ v2 v0)) (* v1 v2))))))
(377 (paramod 376 (1 1) 375 (1 1)) ((= (* (+ v0 v1) (* (* (+ v1 v2) (+ v2 v0)) (* v1 v2))) (* v1 v2))))
(378 (instantiate 12 ((v0 . (+ v1 v2))(v1 . (+ v2 v0))(v2 . (* v1 v2)))) ((= (* (* (+ v1 v2) (+ v2 v0)) (* v1 v2)) (* (+ v1 v2) (* (+ v2 v0) (* v1 v2))))))
(379 (paramod 378 (1 1) 377 (1 1 2)) ((= (* (+ v0 v1) (* (+ v1 v2) (* (+ v2 v0) (* v1 v2)))) (* v1 v2))))
(380 (instantiate 373 ((v0 . v1)(v1 . v2)(v2 . (+ v2 v0))(v3 . v2))) ((= (* (+ v1 v2) (* (+ v2 v0) (* v1 v2))) (* (+ v2 v0) (* v1 v2)))))
(381 (paramod 380 (1 1) 379 (1 1 2)) ((= (* (+ v0 v1) (* (+ v2 v0) (* v1 v2))) (* v1 v2))))
(382 (instantiate 369 ((v0 . v0)(v1 . v1)(v2 . (+ v2 v0))(v3 . v2))) ((= (* (+ v0 v1) (* (+ v2 v0) (* v1 v2))) (* (+ v2 v0) (* v1 v2)))))
(383 (paramod 382 (1 1) 381 (1 1)) ((= (* (+ v2 v0) (* v1 v2)) (* v1 v2))))
(384 (instantiate 383 ((v0 . v1)(v1 . v2)(v2 . v0))) ((= (* (+ v0 v1) (* v2 v0)) (* v2 v0))))
(385 (instantiate 12 ((v2 . v65))) ((= (* (* v0 v1) v65) (* v0 (* v1 v65)))))
(386 (instantiate 139 ((v0 . (* v0 v1))(v1 . v65)(v2 . v66))) ((= (+ (* v0 v1) (+ (* (* v0 v1) v65) v66)) (+ (* v0 v1) v66))))
(387 (paramod 385 (1 1) 386 (1 1 2 1)) ((= (+ (* v0 v1) (+ (* v0 (* v1 v65)) v66)) (+ (* v0 v1) v66))))
(388 (instantiate 387 ((v65 . v2)(v66 . v3))) ((= (+ (* v0 v1) (+ (* v0 (* v1 v2)) v3)) (+ (* v0 v1) v3))))
(389 (instantiate 64 ((v1 . v65))) ((= (+ (* (@ v0) v65) (* v65 v0)) (* (+ (@ v0) v65) (+ v65 v0)))))
(390 (instantiate 139 ((v0 . (@ v0))(v1 . v65)(v2 . (* v65 v0)))) ((= (+ (@ v0) (+ (* (@ v0) v65) (* v65 v0))) (+ (@ v0) (* v65 v0)))))
(391 (paramod 389 (1 1) 390 (1 1 2)) ((= (+ (@ v0) (* (+ (@ v0) v65) (+ v65 v0))) (+ (@ v0) (* v65 v0)))))
(392 (instantiate 321 ((v0 . (@ v0))(v1 . v65)(v2 . v0))) ((= (+ (@ v0) (* (+ (@ v0) v65) (+ v65 v0))) (+ (@ v0) v65))))
(393 (paramod 392 (1 1) 391 (1 1)) ((= (+ (@ v0) v65) (+ (@ v0) (* v65 v0)))))
(394 (flip 393 (1)) ((= (+ (@ v0) (* v65 v0)) (+ (@ v0) v65))))
(395 (instantiate 394 ((v65 . v1))) ((= (+ (@ v0) (* v1 v0)) (+ (@ v0) v1))))
(396 (instantiate 388 ((v0 . v0)(v1 . v1)(v2 . v2)(v3 . (* v2 v0)))) ((= (+ (* v0 v1) (+ (* v0 (* v1 v2)) (* v2 v0))) (+ (* v0 v1) (* v2 v0)))))
(397 (paramod 396 (1 1) 365 (1 1)) ((= (+ (* v0 v1) (* v2 v0)) (* v0 (+ (* v0 v1) v2)))))
(398 (paramod 395 (1 1) 355 (1 1 1)) ((= (* (+ (@ v0) v1) v0) (* v1 v0))))
(399 (instantiate 397 ((v0 . v0)(v1 . v1)(v2 . (@ v1)))) ((= (+ (* v0 v1) (* (@ v1) v0)) (* v0 (+ (* v0 v1) (@ v1))))))
(400 (paramod 399 (1 1) 340 (1 1)) ((= (* v0 (+ (* v0 v1) (@ v1))) (* (+ v0 v1) (+ v0 (@ v1))))))
(401 (instantiate 116 ((v0 . (@ v64))(v1 . v65))) ((= (+ (@ v64) v65) (+ v65 (@ v64)))))
(402 (instantiate 398 ((v0 . v64)(v1 . v65))) ((= (* (+ (@ v64) v65) v64) (* v65 v64))))
(403 (paramod 401 (1 1) 402 (1 1 1)) ((= (* (+ v65 (@ v64)) v64) (* v65 v64))))
(404 (instantiate 403 ((v64 . v1)(v65 . v0))) ((= (* (+ v0 (@ v1)) v1) (* v0 v1))))
(405 (instantiate 9 ((v0 . (@ v64)))) ((= (+ (@ v64) (@ (@ v64))) (1))))
(406 (instantiate 398 ((v0 . v64)(v1 . (@ (@ v64))))) ((= (* (+ (@ v64) (@ (@ v64))) v64) (* (@ (@ v64)) v64))))
(407 (paramod 405 (1 1) 406 (1 1 1)) ((= (* (1) v64) (* (@ (@ v64)) v64))))
(408 (instantiate 14 ((v0 . v64))) ((= (* (1) v64) v64)))
(409 (paramod 408 (1 1) 407 (1 1)) ((= v64 (* (@ (@ v64)) v64))))
(410 (flip 409 (1)) ((= (* (@ (@ v64)) v64) v64)))
(411 (instantiate 410 ((v64 . v0))) ((= (* (@ (@ v0)) v0) v0)))
(412 (paramod 404 (1 1) 306 (1 1 1)) ((= (+ (* v0 v1) (@ v1)) (+ v0 (@ v1)))))
(413 (paramod 411 (1 1) 288 (1 2)) ((= (+ (@ (@ v0)) v0) v0)))
(414 (paramod 412 (1 1) 400 (1 1 2)) ((= (* v0 (+ v0 (@ v1))) (* (+ v0 v1) (+ v0 (@ v1))))))
(415 (instantiate 100 ((v0 . v0)(v1 . (@ v1)))) ((= (* v0 (+ v0 (@ v1))) v0)))
(416 (paramod 415 (1 1) 414 (1 1)) ((= v0 (* (+ v0 v1) (+ v0 (@ v1))))))
(417 (flip 416 (1)) ((= (* (+ v0 v1) (+ v0 (@ v1))) v0)))
(418 (paramod 417 (1 1) 342 (1 1)) ((= v0 (* (+ v0 v1) (+ (@ v1) v0)))))
(419 (flip 418 (1)) ((= (* (+ v0 v1) (+ (@ v1) v0)) v0)))
(420 (paramod 417 (1 1) 341 (1 1)) ((= v0 (* (+ (@ v1) v0) (+ v0 v1)))))
(421 (flip 420 (1)) ((= (* (+ (@ v1) v0) (+ v0 v1)) v0)))
(422 (instantiate 421 ((v0 . v1)(v1 . v0))) ((= (* (+ (@ v0) v1) (+ v1 v0)) v1)))
(423 (paramod 419 (1 1) 307 (1 1)) ((= v0 (+ (* v0 v1) (* v0 (@ v1))))))
(424 (flip 423 (1)) ((= (+ (* v0 v1) (* v0 (@ v1))) v0)))
(425 (instantiate 411 ((v0 . v65))) ((= (* (@ (@ v65)) v65) v65)))
(426 (instantiate 33 ((v0 . (@ (@ v65)))(v1 . v65))) ((= (+ (@ (@ v65)) (* (@ (@ v65)) v65)) (@ (@ v65)))))
(427 (paramod 425 (1 1) 426 (1 1 2)) ((= (+ (@ (@ v65)) v65) (@ (@ v65)))))
(428 (instantiate 413 ((v0 . v65))) ((= (+ (@ (@ v65)) v65) v65)))
(429 (paramod 428 (1 1) 427 (1 1)) ((= v65 (@ (@ v65)))))
(430 (flip 429 (1)) ((= (@ (@ v65)) v65)))
(431 (instantiate 430 ((v65 . v0))) ((= (@ (@ v0)) v0)))
(432 (instantiate 398 ((v0 . (@ v0))(v1 . v65))) ((= (* (+ (@ (@ v0)) v65) (@ v0)) (* v65 (@ v0)))))
(433 (paramod 431 (1 1) 432 (1 1 1 1)) ((= (* (+ v0 v65) (@ v0)) (* v65 (@ v0)))))
(434 (instantiate 433 ((v65 . v1))) ((= (* (+ v0 v1) (@ v0)) (* v1 (@ v0)))))
(435 (instantiate 116 ((v0 . v65)(v1 . v64))) ((= (+ v65 v64) (+ v64 v65))))
(436 (instantiate 422 ((v0 . v64)(v1 . v65))) ((= (* (+ (@ v64) v65) (+ v65 v64)) v65)))
(437 (paramod 435 (1 1) 436 (1 1 2)) ((= (* (+ (@ v64) v65) (+ v64 v65)) v65)))
(438 (instantiate 437 ((v64 . v0)(v65 . v1))) ((= (* (+ (@ v0) v1) (+ v0 v1)) v1)))
(439 (instantiate 239 ((v0 . v65))) ((= (* (+ v65 v1) v65) v65)))
(440 (instantiate 424 ((v0 . (+ v65 v1))(v1 . v65))) ((= (+ (* (+ v65 v1) v65) (* (+ v65 v1) (@ v65))) (+ v65 v1))))
(441 (paramod 439 (1 1) 440 (1 1 1)) ((= (+ v65 (* (+ v65 v1) (@ v65))) (+ v65 v1))))
(442 (instantiate 434 ((v0 . v65)(v1 . v1))) ((= (* (+ v65 v1) (@ v65)) (* v1 (@ v65)))))
(443 (paramod 442 (1 1) 441 (1 1 2)) ((= (+ v65 (* v1 (@ v65))) (+ v65 v1))))
(444 (instantiate 443 ((v65 . v0))) ((= (+ v0 (* v1 (@ v0))) (+ v0 v1))))
(445 (instantiate 155 ((v0 . (A))(v1 . (C)))) ((= (* (A) (C)) (* (C) (A)))))
(446 (paramod 445 (1 1) 233 (1 1 1 2)) ((not (= (+ (* (A) (B)) (* (C) (A))) (* (A) (+ (B) (C)))))))
(447 (instantiate 397 ((v0 . (A))(v1 . (B))(v2 . (C)))) ((= (+ (* (A) (B)) (* (C) (A))) (* (A) (+ (* (A) (B)) (C))))))
(448 (paramod 447 (1 1) 446 (1 1 1)) ((not (= (* (A) (+ (* (A) (B)) (C))) (* (A) (+ (B) (C)))))))
(449 (instantiate 249 ((v0 . (@ v64)))) ((= (+ (@ v64) (+ (* v1 (@ v64)) v2)) (+ (@ v64) v2))))
(450 (instantiate 438 ((v0 . v64)(v1 . (+ (* v1 (@ v64)) v2)))) ((= (* (+ (@ v64) (+ (* v1 (@ v64)) v2)) (+ v64 (+ (* v1 (@ v64)) v2))) (+ (* v1 (@ v64)) v2))))
(451 (paramod 449 (1 1) 450 (1 1 1)) ((= (* (+ (@ v64) v2) (+ v64 (+ (* v1 (@ v64)) v2))) (+ (* v1 (@ v64)) v2))))
(452 (instantiate 451 ((v1 . v2)(v2 . v1)(v64 . v0))) ((= (* (+ (@ v0) v1) (+ v0 (+ (* v2 (@ v0)) v1))) (+ (* v2 (@ v0)) v1))))
(453 (instantiate 12 ((v2 . (@ v64)))) ((= (* (* v0 v1) (@ v64)) (* v0 (* v1 (@ v64))))))
(454 (instantiate 444 ((v0 . v64)(v1 . (* v0 v1)))) ((= (+ v64 (* (* v0 v1) (@ v64))) (+ v64 (* v0 v1)))))
(455 (paramod 453 (1 1) 454 (1 1 2)) ((= (+ v64 (* v0 (* v1 (@ v64)))) (+ v64 (* v0 v1)))))
(456 (instantiate 455 ((v0 . v1)(v1 . v2)(v64 . v0))) ((= (+ v0 (* v1 (* v2 (@ v0)))) (+ v0 (* v1 v2)))))
(457 (instantiate 444 ((v0 . v64))) ((= (+ v64 (* v1 (@ v64))) (+ v64 v1))))
(458 (instantiate 11 ((v0 . v64)(v1 . (* v1 (@ v64)))(v2 . v66))) ((= (+ (+ v64 (* v1 (@ v64))) v66) (+ v64 (+ (* v1 (@ v64)) v66)))))
(459 (paramod 457 (1 1) 458 (1 1 1)) ((= (+ (+ v64 v1) v66) (+ v64 (+ (* v1 (@ v64)) v66)))))
(460 (instantiate 11 ((v0 . v64)(v1 . v1)(v2 . v66))) ((= (+ (+ v64 v1) v66) (+ v64 (+ v1 v66)))))
(461 (paramod 460 (1 1) 459 (1 1)) ((= (+ v64 (+ v1 v66)) (+ v64 (+ (* v1 (@ v64)) v66)))))
(462 (flip 461 (1)) ((= (+ v64 (+ (* v1 (@ v64)) v66)) (+ v64 (+ v1 v66)))))
(463 (instantiate 462 ((v64 . v0)(v66 . v2))) ((= (+ v0 (+ (* v1 (@ v0)) v2)) (+ v0 (+ v1 v2)))))
(464 (instantiate 463 ((v0 . v0)(v1 . v2)(v2 . v1))) ((= (+ v0 (+ (* v2 (@ v0)) v1)) (+ v0 (+ v2 v1)))))
(465 (paramod 464 (1 1) 452 (1 1 2)) ((= (* (+ (@ v0) v1) (+ v0 (+ v2 v1))) (+ (* v2 (@ v0)) v1))))
(466 (flip 465 (1)) ((= (+ (* v2 (@ v0)) v1) (* (+ (@ v0) v1) (+ v0 (+ v2 v1))))))
(467 (instantiate 466 ((v0 . v1)(v1 . v2)(v2 . v0))) ((= (+ (* v0 (@ v1)) v2) (* (+ (@ v1) v2) (+ v1 (+ v0 v2))))))
(468 (instantiate 264 ((v2 . v66))) ((= (+ v66 (+ v0 v1)) (+ v0 (+ v1 v66)))))
(469 (instantiate 209 ((v0 . (+ v0 v1))(v1 . v65)(v2 . v66))) ((= (* (+ v0 v1) (* v65 (+ v66 (+ v0 v1)))) (* (+ v0 v1) v65))))
(470 (paramod 468 (1 1) 469 (1 1 2 2)) ((= (* (+ v0 v1) (* v65 (+ v0 (+ v1 v66)))) (* (+ v0 v1) v65))))
(471 (instantiate 470 ((v65 . v2)(v66 . v3))) ((= (* (+ v0 v1) (* v2 (+ v0 (+ v1 v3)))) (* (+ v0 v1) v2))))
(472 (instantiate 268 ((v0 . v64)(v1 . (+ (@ v0) v1))(v2 . (+ v1 v0)))) ((= (* v64 (* (+ (@ v0) v1) (+ v1 v0))) (* (+ v1 v0) (* v64 (+ (@ v0) v1))))))
(473 (paramod 422 (1 1) 472 (1 1 2)) ((= (* v64 v1) (* (+ v1 v0) (* v64 (+ (@ v0) v1))))))
(474 (flip 473 (1)) ((= (* (+ v1 v0) (* v64 (+ (@ v0) v1))) (* v64 v1))))
(475 (instantiate 474 ((v0 . v1)(v1 . v0)(v64 . v2))) ((= (* (+ v0 v1) (* v2 (+ (@ v1) v0))) (* v2 v0))))
(476 (instantiate 192 ((v0 . v64))) ((= (* v64 (* v64 v1)) (* v64 v1))))
(477 (instantiate 277 ((v0 . v64)(v1 . (* v64 v1))(v2 . v66))) ((= (+ (* v64 (* v64 v1)) (+ (* (* v64 v1) v66) (* v64 v66))) (* (+ v64 (* v64 v1)) (* (+ (* v64 v1) v66) (+ v66 v64))))))
(478 (paramod 476 (1 1) 477 (1 1 1)) ((= (+ (* v64 v1) (+ (* (* v64 v1) v66) (* v64 v66))) (* (+ v64 (* v64 v1)) (* (+ (* v64 v1) v66) (+ v66 v64))))))
(479 (instantiate 12 ((v0 . v64)(v1 . v1)(v2 . v66))) ((= (* (* v64 v1) v66) (* v64 (* v1 v66)))))
(480 (paramod 479 (1 1) 478 (1 1 2 1)) ((= (+ (* v64 v1) (+ (* v64 (* v1 v66)) (* v64 v66))) (* (+ v64 (* v64 v1)) (* (+ (* v64 v1) v66) (+ v66 v64))))))
(481 (instantiate 388 ((v0 . v64)(v1 . v1)(v2 . v66)(v3 . (* v64 v66)))) ((= (+ (* v64 v1) (+ (* v64 (* v1 v66)) (* v64 v66))) (+ (* v64 v1) (* v64 v66)))))
(482 (paramod 481 (1 1) 480 (1 1)) ((= (+ (* v64 v1) (* v64 v66)) (* (+ v64 (* v64 v1)) (* (+ (* v64 v1) v66) (+ v66 v64))))))
(483 (instantiate 33 ((v0 . v64)(v1 . v1))) ((= (+ v64 (* v64 v1)) v64)))
(484 (paramod 483 (1 1) 482 (1 2 1)) ((= (+ (* v64 v1) (* v64 v66)) (* v64 (* (+ (* v64 v1) v66) (+ v66 v64))))))
(485 (instantiate 209 ((v0 . v64)(v1 . (+ (* v64 v1) v66))(v2 . v66))) ((= (* v64 (* (+ (* v64 v1) v66) (+ v66 v64))) (* v64 (+ (* v64 v1) v66)))))
(486 (paramod 485 (1 1) 484 (1 2)) ((= (+ (* v64 v1) (* v64 v66)) (* v64 (+ (* v64 v1) v66)))))
(487 (instantiate 486 ((v64 . v0)(v66 . v2))) ((= (+ (* v0 v1) (* v0 v2)) (* v0 (+ (* v0 v1) v2)))))
(488 (instantiate 329 ((v0 . v65))) ((= (* v65 (* v1 (@ v65))) (0))))
(489 (instantiate 277 ((v0 . v64)(v1 . v65)(v2 . (* v1 (@ v65))))) ((= (+ (* v64 v65) (+ (* v65 (* v1 (@ v65))) (* v64 (* v1 (@ v65))))) (* (+ v64 v65) (* (+ v65 (* v1 (@ v65))) (+ (* v1 (@ v65)) v64))))))
(490 (paramod 488 (1 1) 489 (1 1 2 1)) ((= (+ (* v64 v65) (+ (0) (* v64 (* v1 (@ v65))))) (* (+ v64 v65) (* (+ v65 (* v1 (@ v65))) (+ (* v1 (@ v65)) v64))))))
(491 (instantiate 16 ((v0 . (* v64 (* v1 (@ v65)))))) ((= (+ (0) (* v64 (* v1 (@ v65)))) (* v64 (* v1 (@ v65))))))
(492 (paramod 491 (1 1) 490 (1 1 2)) ((= (+ (* v64 v65) (* v64 (* v1 (@ v65)))) (* (+ v64 v65) (* (+ v65 (* v1 (@ v65))) (+ (* v1 (@ v65)) v64))))))
(493 (instantiate 487 ((v0 . v64)(v1 . v65)(v2 . (* v1 (@ v65))))) ((= (+ (* v64 v65) (* v64 (* v1 (@ v65)))) (* v64 (+ (* v64 v65) (* v1 (@ v65)))))))
(494 (paramod 493 (1 1) 492 (1 1)) ((= (* v64 (+ (* v64 v65) (* v1 (@ v65)))) (* (+ v64 v65) (* (+ v65 (* v1 (@ v65))) (+ (* v1 (@ v65)) v64))))))
(495 (instantiate 444 ((v0 . v65)(v1 . v1))) ((= (+ v65 (* v1 (@ v65))) (+ v65 v1))))
(496 (paramod 495 (1 1) 494 (1 2 2 1)) ((= (* v64 (+ (* v64 v65) (* v1 (@ v65)))) (* (+ v64 v65) (* (+ v65 v1) (+ (* v1 (@ v65)) v64))))))
(497 (instantiate 467 ((v0 . v1)(v1 . v65)(v2 . v64))) ((= (+ (* v1 (@ v65)) v64) (* (+ (@ v65) v64) (+ v65 (+ v1 v64))))))
(498 (paramod 497 (1 1) 496 (1 2 2 2)) ((= (* v64 (+ (* v64 v65) (* v1 (@ v65)))) (* (+ v64 v65) (* (+ v65 v1) (* (+ (@ v65) v64) (+ v65 (+ v1 v64))))))))
(499 (instantiate 471 ((v0 . v65)(v1 . v1)(v2 . (+ (@ v65) v64))(v3 . v64))) ((= (* (+ v65 v1) (* (+ (@ v65) v64) (+ v65 (+ v1 v64)))) (* (+ v65 v1) (+ (@ v65) v64)))))
(500 (paramod 499 (1 1) 498 (1 2 2)) ((= (* v64 (+ (* v64 v65) (* v1 (@ v65)))) (* (+ v64 v65) (* (+ v65 v1) (+ (@ v65) v64))))))
(501 (instantiate 475 ((v0 . v64)(v1 . v65)(v2 . (+ v65 v1)))) ((= (* (+ v64 v65) (* (+ v65 v1) (+ (@ v65) v64))) (* (+ v65 v1) v64))))
(502 (paramod 501 (1 1) 500 (1 2)) ((= (* v64 (+ (* v64 v65) (* v1 (@ v65)))) (* (+ v65 v1) v64))))
(503 (instantiate 502 ((v1 . v2)(v64 . v0)(v65 . v1))) ((= (* v0 (+ (* v0 v1) (* v2 (@ v1)))) (* (+ v1 v2) v0))))
(504 (instantiate 192 ((v0 . v64))) ((= (* v64 (* v64 v1)) (* v64 v1))))
(505 (instantiate 277 ((v0 . v64)(v1 . v65)(v2 . (* v64 v1)))) ((= (+ (* v64 v65) (+ (* v65 (* v64 v1)) (* v64 (* v64 v1)))) (* (+ v64 v65) (* (+ v65 (* v64 v1)) (+ (* v64 v1) v64))))))
(506 (paramod 504 (1 1) 505 (1 1 2 2)) ((= (+ (* v64 v65) (+ (* v65 (* v64 v1)) (* v64 v1))) (* (+ v64 v65) (* (+ v65 (* v64 v1)) (+ (* v64 v1) v64))))))
(507 (instantiate 240 ((v0 . v65)(v1 . (* v64 v1)))) ((= (+ (* v65 (* v64 v1)) (* v64 v1)) (* v64 v1))))
(508 (paramod 507 (1 1) 506 (1 1 2)) ((= (+ (* v64 v65) (* v64 v1)) (* (+ v64 v65) (* (+ v65 (* v64 v1)) (+ (* v64 v1) v64))))))
(509 (instantiate 487 ((v0 . v64)(v1 . v65)(v2 . v1))) ((= (+ (* v64 v65) (* v64 v1)) (* v64 (+ (* v64 v65) v1)))))
(510 (paramod 509 (1 1) 508 (1 1)) ((= (* v64 (+ (* v64 v65) v1)) (* (+ v64 v65) (* (+ v65 (* v64 v1)) (+ (* v64 v1) v64))))))
(511 (instantiate 215 ((v0 . v64)(v1 . v1))) ((= (+ (* v64 v1) v64) v64)))
(512 (paramod 511 (1 1) 510 (1 2 2 2)) ((= (* v64 (+ (* v64 v65) v1)) (* (+ v64 v65) (* (+ v65 (* v64 v1)) v64)))))
(513 (instantiate 384 ((v0 . v64)(v1 . v65)(v2 . (+ v65 (* v64 v1))))) ((= (* (+ v64 v65) (* (+ v65 (* v64 v1)) v64)) (* (+ v65 (* v64 v1)) v64))))
(514 (paramod 513 (1 1) 512 (1 2)) ((= (* v64 (+ (* v64 v65) v1)) (* (+ v65 (* v64 v1)) v64))))
(515 (instantiate 514 ((v1 . v2)(v64 . v0)(v65 . v1))) ((= (* v0 (+ (* v0 v1) v2)) (* (+ v1 (* v0 v2)) v0))))
(516 (instantiate 515 ((v0 . v0)(v1 . v1)(v2 . (* v2 (@ v1))))) ((= (* v0 (+ (* v0 v1) (* v2 (@ v1)))) (* (+ v1 (* v0 (* v2 (@ v1)))) v0))))
(517 (paramod 516 (1 1) 503 (1 1)) ((= (* (+ v1 (* v0 (* v2 (@ v1)))) v0) (* (+ v1 v2) v0))))
(518 (instantiate 456 ((v0 . v1)(v1 . v0)(v2 . v2))) ((= (+ v1 (* v0 (* v2 (@ v1)))) (+ v1 (* v0 v2)))))
(519 (paramod 518 (1 1) 517 (1 1 1)) ((= (* (+ v1 (* v0 v2)) v0) (* (+ v1 v2) v0))))
(520 (instantiate 519 ((v0 . v1)(v1 . v0))) ((= (* (+ v0 (* v1 v2)) v1) (* (+ v0 v2) v1))))
(521 (instantiate 515 ((v0 . (A))(v1 . (B))(v2 . (C)))) ((= (* (A) (+ (* (A) (B)) (C))) (* (+ (B) (* (A) (C))) (A)))))
(522 (paramod 521 (1 1) 448 (1 1 1)) ((not (= (* (+ (B) (* (A) (C))) (A)) (* (A) (+ (B) (C)))))))
(523 (instantiate 520 ((v0 . (B))(v1 . (A))(v2 . (C)))) ((= (* (+ (B) (* (A) (C))) (A)) (* (+ (B) (C)) (A)))))
(524 (paramod 523 (1 1) 522 (1 1 1)) ((not (= (* (+ (B) (C)) (A)) (* (A) (+ (B) (C)))))))
(525 (instantiate 155 ((v0 . (+ (B) (C)))(v1 . (A)))) ((= (* (+ (B) (C)) (A)) (* (A) (+ (B) (C))))))
(526 (resolve 524 (1) 525 (1)) ())
)