;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Sun Feb 11 18:41:31 1996
;;
;;;;  -> x=x.
;;;; A+ (B*C)= (A+B)* (A+C), (A*B)+B=B, B*B@ =A*A@  -> .
;;;;  -> (x+y)*y=y.
;;;;  -> x* (y+z)= (x*y)+ (x*z).
;;;;  -> x+x@ =1.
;;;;  -> p(x,y,z)= (x*y@ )+ ((x*z)+ (y@ *z)).
;;;;  -> p(x,x,y)=y.
;;;;  -> p(x,y,y)=x.
;;;;  -> p(x,y,x)=x.
;;
;; ----> UNIT CONFLICT at   3.81 sec ----> 240 [binary,239.1,226.1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((not (= (+ (A) (* (B) (C))) (* (+ (A) (B)) (+ (A) (C))))) (not (= (+ (* (A) (B)) (B)) (B))) (not (= (* (B) (@ (B))) (* (A) (@ (A)))))))
(3 (input) ((= (* (+ v0 v1) v1) v1)))
(4 (input) ((= (* v0 (+ v1 v2)) (+ (* v0 v1) (* v0 v2)))))
(5 (flip 4 (1)) ((= (+ (* v0 v1) (* v0 v2)) (* v0 (+ v1 v2)))))
(6 (input) ((= (+ v0 (@ v0)) (1))))
(7 (input) ((= (p v0 v1 v2) (+ (* v0 (@ v1)) (+ (* v0 v2) (* (@ v1) v2))))))
(8 (input) ((= (p v0 v0 v1) v1)))
(9 (instantiate 7 ((v0 . v0)(v1 . v0)(v2 . v1))) ((= (p v0 v0 v1) (+ (* v0 (@ v0)) (+ (* v0 v1) (* (@ v0) v1))))))
(10 (paramod 9 (1 1) 8 (1 1)) ((= (+ (* v0 (@ v0)) (+ (* v0 v1) (* (@ v0) v1))) v1)))
(11 (input) ((= (p v0 v1 v1) v0)))
(12 (instantiate 7 ((v0 . v0)(v1 . v1)(v2 . v1))) ((= (p v0 v1 v1) (+ (* v0 (@ v1)) (+ (* v0 v1) (* (@ v1) v1))))))
(13 (paramod 12 (1 1) 11 (1 1)) ((= (+ (* v0 (@ v1)) (+ (* v0 v1) (* (@ v1) v1))) v0)))
(14 (instantiate 6 ((v0 . v64))) ((= (+ v64 (@ v64)) (1))))
(15 (instantiate 3 ((v0 . v64)(v1 . (@ v64)))) ((= (* (+ v64 (@ v64)) (@ v64)) (@ v64))))
(16 (paramod 14 (1 1) 15 (1 1 1)) ((= (* (1) (@ v64)) (@ v64))))
(17 (instantiate 16 ((v64 . v0))) ((= (* (1) (@ v0)) (@ v0))))
(18 (instantiate 5 ((v0 . (1))(v1 . (@ v0))(v2 . v66))) ((= (+ (* (1) (@ v0)) (* (1) v66)) (* (1) (+ (@ v0) v66)))))
(19 (paramod 17 (1 1) 18 (1 1 1)) ((= (+ (@ v0) (* (1) v66)) (* (1) (+ (@ v0) v66)))))
(20 (instantiate 19 ((v66 . v1))) ((= (+ (@ v0) (* (1) v1)) (* (1) (+ (@ v0) v1)))))
(21 (instantiate 3 ((v1 . v65))) ((= (* (+ v0 v65) v65) v65)))
(22 (instantiate 5 ((v0 . (+ v0 v65))(v1 . v65)(v2 . v66))) ((= (+ (* (+ v0 v65) v65) (* (+ v0 v65) v66)) (* (+ v0 v65) (+ v65 v66)))))
(23 (paramod 21 (1 1) 22 (1 1 1)) ((= (+ v65 (* (+ v0 v65) v66)) (* (+ v0 v65) (+ v65 v66)))))
(24 (instantiate 23 ((v0 . v1)(v65 . v0)(v66 . v2))) ((= (+ v0 (* (+ v1 v0) v2)) (* (+ v1 v0) (+ v0 v2)))))
(25 (instantiate 3 ((v1 . v66))) ((= (* (+ v0 v66) v66) v66)))
(26 (instantiate 5 ((v0 . (+ v0 v66))(v1 . v65)(v2 . v66))) ((= (+ (* (+ v0 v66) v65) (* (+ v0 v66) v66)) (* (+ v0 v66) (+ v65 v66)))))
(27 (paramod 25 (1 1) 26 (1 1 2)) ((= (+ (* (+ v0 v66) v65) v66) (* (+ v0 v66) (+ v65 v66)))))
(28 (instantiate 27 ((v65 . v2)(v66 . v1))) ((= (+ (* (+ v0 v1) v2) v1) (* (+ v0 v1) (+ v2 v1)))))
(29 (instantiate 3 ((v0 . (* v0 v1))(v1 . (* v0 v2)))) ((= (* (+ (* v0 v1) (* v0 v2)) (* v0 v2)) (* v0 v2))))
(30 (paramod 5 (1 1) 29 (1 1 1)) ((= (* (* v0 (+ v1 v2)) (* v0 v2)) (* v0 v2))))
(31 (instantiate 20 ((v0 . v64)(v1 . (@ v0)))) ((= (+ (@ v64) (* (1) (@ v0))) (* (1) (+ (@ v64) (@ v0))))))
(32 (paramod 17 (1 1) 31 (1 1 2)) ((= (+ (@ v64) (@ v0)) (* (1) (+ (@ v64) (@ v0))))))
(33 (flip 32 (1)) ((= (* (1) (+ (@ v64) (@ v0))) (+ (@ v64) (@ v0)))))
(34 (instantiate 33 ((v0 . v1)(v64 . v0))) ((= (* (1) (+ (@ v0) (@ v1))) (+ (@ v0) (@ v1)))))
(35 (instantiate 3 ((v0 . v65)(v1 . v66))) ((= (* (+ v65 v66) v66) v66)))
(36 (instantiate 24 ((v0 . v66)(v1 . v65)(v2 . v66))) ((= (+ v66 (* (+ v65 v66) v66)) (* (+ v65 v66) (+ v66 v66)))))
(37 (paramod 35 (1 1) 36 (1 1 2)) ((= (+ v66 v66) (* (+ v65 v66) (+ v66 v66)))))
(38 (flip 37 (1)) ((= (* (+ v65 v66) (+ v66 v66)) (+ v66 v66))))
(39 (instantiate 38 ((v65 . v0)(v66 . v1))) ((= (* (+ v0 v1) (+ v1 v1)) (+ v1 v1))))
(40 (instantiate 28 ((v1 . v65))) ((= (+ (* (+ v0 v65) v2) v65) (* (+ v0 v65) (+ v2 v65)))))
(41 (instantiate 3 ((v0 . (* (+ v0 v65) v2))(v1 . v65))) ((= (* (+ (* (+ v0 v65) v2) v65) v65) v65)))
(42 (paramod 40 (1 1) 41 (1 1 1)) ((= (* (* (+ v0 v65) (+ v2 v65)) v65) v65)))
(43 (instantiate 42 ((v65 . v1))) ((= (* (* (+ v0 v1) (+ v2 v1)) v1) v1)))
(44 (instantiate 6 ((v0 . (@ v64)))) ((= (+ (@ v64) (@ (@ v64))) (1))))
(45 (instantiate 34 ((v0 . v64)(v1 . (@ v64)))) ((= (* (1) (+ (@ v64) (@ (@ v64)))) (+ (@ v64) (@ (@ v64))))))
(46 (paramod 44 (1 1) 45 (1 1 2)) ((= (* (1) (1)) (+ (@ v64) (@ (@ v64))))))
(47 (instantiate 6 ((v0 . (@ v64)))) ((= (+ (@ v64) (@ (@ v64))) (1))))
(48 (paramod 47 (1 1) 46 (1 2)) ((= (* (1) (1)) (1))))
(49 (instantiate 6 ((v0 . v66))) ((= (+ v66 (@ v66)) (1))))
(50 (instantiate 43 ((v0 . v64)(v1 . (@ v66))(v2 . v66))) ((= (* (* (+ v64 (@ v66)) (+ v66 (@ v66))) (@ v66)) (@ v66))))
(51 (paramod 49 (1 1) 50 (1 1 1 2)) ((= (* (* (+ v64 (@ v66)) (1)) (@ v66)) (@ v66))))
(52 (instantiate 51 ((v64 . v0)(v66 . v1))) ((= (* (* (+ v0 (@ v1)) (1)) (@ v1)) (@ v1))))
(53 (instantiate 20 ((v0 . v64)(v1 . (1)))) ((= (+ (@ v64) (* (1) (1))) (* (1) (+ (@ v64) (1))))))
(54 (paramod 48 (1 1) 53 (1 1 2)) ((= (+ (@ v64) (1)) (* (1) (+ (@ v64) (1))))))
(55 (flip 54 (1)) ((= (* (1) (+ (@ v64) (1))) (+ (@ v64) (1)))))
(56 (instantiate 55 ((v64 . v0))) ((= (* (1) (+ (@ v0) (1))) (+ (@ v0) (1)))))
(57 (instantiate 30 ((v0 . (1))(v1 . v65)(v2 . (1)))) ((= (* (* (1) (+ v65 (1))) (* (1) (1))) (* (1) (1)))))
(58 (paramod 48 (1 1) 57 (1 1 2)) ((= (* (* (1) (+ v65 (1))) (1)) (* (1) (1)))))
(59 (paramod 48 (1 1) 58 (1 2)) ((= (* (* (1) (+ v65 (1))) (1)) (1))))
(60 (instantiate 59 ((v65 . v0))) ((= (* (* (1) (+ v0 (1))) (1)) (1))))
(61 (instantiate 5 ((v0 . (1))(v1 . v65)(v2 . (1)))) ((= (+ (* (1) v65) (* (1) (1))) (* (1) (+ v65 (1))))))
(62 (paramod 48 (1 1) 61 (1 1 2)) ((= (+ (* (1) v65) (1)) (* (1) (+ v65 (1))))))
(63 (instantiate 62 ((v65 . v0))) ((= (+ (* (1) v0) (1)) (* (1) (+ v0 (1))))))
(64 (instantiate 10 ((v0 . (1))(v1 . (1)))) ((= (+ (* (1) (@ (1))) (+ (* (1) (1)) (* (@ (1)) (1)))) (1))))
(65 (paramod 48 (1 1) 64 (1 1 2 1)) ((= (+ (* (1) (@ (1))) (+ (1) (* (@ (1)) (1)))) (1))))
(66 (instantiate 17 ((v0 . (1)))) ((= (* (1) (@ (1))) (@ (1)))))
(67 (paramod 66 (1 1) 65 (1 1 1)) ((= (+ (@ (1)) (+ (1) (* (@ (1)) (1)))) (1))))
(68 (instantiate 3 ((v1 . (@ v65)))) ((= (* (+ v0 (@ v65)) (@ v65)) (@ v65))))
(69 (instantiate 13 ((v0 . (+ v0 (@ v65)))(v1 . v65))) ((= (+ (* (+ v0 (@ v65)) (@ v65)) (+ (* (+ v0 (@ v65)) v65) (* (@ v65) v65))) (+ v0 (@ v65)))))
(70 (paramod 68 (1 1) 69 (1 1 1)) ((= (+ (@ v65) (+ (* (+ v0 (@ v65)) v65) (* (@ v65) v65))) (+ v0 (@ v65)))))
(71 (instantiate 70 ((v0 . v1)(v65 . v0))) ((= (+ (@ v0) (+ (* (+ v1 (@ v0)) v0) (* (@ v0) v0))) (+ v1 (@ v0)))))
(72 (instantiate 5 ((v0 . (@ v65))(v1 . v65)(v2 . v65))) ((= (+ (* (@ v65) v65) (* (@ v65) v65)) (* (@ v65) (+ v65 v65)))))
(73 (instantiate 13 ((v0 . (@ v65))(v1 . v65))) ((= (+ (* (@ v65) (@ v65)) (+ (* (@ v65) v65) (* (@ v65) v65))) (@ v65))))
(74 (paramod 72 (1 1) 73 (1 1 2)) ((= (+ (* (@ v65) (@ v65)) (* (@ v65) (+ v65 v65))) (@ v65))))
(75 (instantiate 5 ((v0 . (@ v65))(v1 . (@ v65))(v2 . (+ v65 v65)))) ((= (+ (* (@ v65) (@ v65)) (* (@ v65) (+ v65 v65))) (* (@ v65) (+ (@ v65) (+ v65 v65))))))
(76 (paramod 75 (1 1) 74 (1 1)) ((= (* (@ v65) (+ (@ v65) (+ v65 v65))) (@ v65))))
(77 (instantiate 76 ((v65 . v0))) ((= (* (@ v0) (+ (@ v0) (+ v0 v0))) (@ v0))))
(78 (instantiate 28 ((v0 . (* v0 (@ v1)))(v1 . (+ (* v0 v1) (* (@ v1) v1)))(v2 . v66))) ((= (+ (* (+ (* v0 (@ v1)) (+ (* v0 v1) (* (@ v1) v1))) v66) (+ (* v0 v1) (* (@ v1) v1))) (* (+ (* v0 (@ v1)) (+ (* v0 v1) (* (@ v1) v1))) (+ v66 (+ (* v0 v1) (* (@ v1) v1)))))))
(79 (paramod 13 (1 1) 78 (1 1 1 1)) ((= (+ (* v0 v66) (+ (* v0 v1) (* (@ v1) v1))) (* (+ (* v0 (@ v1)) (+ (* v0 v1) (* (@ v1) v1))) (+ v66 (+ (* v0 v1) (* (@ v1) v1)))))))
(80 (paramod 13 (1 1) 79 (1 2 1)) ((= (+ (* v0 v66) (+ (* v0 v1) (* (@ v1) v1))) (* v0 (+ v66 (+ (* v0 v1) (* (@ v1) v1)))))))
(81 (instantiate 80 ((v1 . v2)(v66 . v1))) ((= (+ (* v0 v1) (+ (* v0 v2) (* (@ v2) v2))) (* v0 (+ v1 (+ (* v0 v2) (* (@ v2) v2)))))))
(82 (instantiate 3 ((v0 . (* v0 (@ v1)))(v1 . (+ (* v0 v1) (* (@ v1) v1))))) ((= (* (+ (* v0 (@ v1)) (+ (* v0 v1) (* (@ v1) v1))) (+ (* v0 v1) (* (@ v1) v1))) (+ (* v0 v1) (* (@ v1) v1)))))
(83 (paramod 13 (1 1) 82 (1 1 1)) ((= (* v0 (+ (* v0 v1) (* (@ v1) v1))) (+ (* v0 v1) (* (@ v1) v1)))))
(84 (instantiate 81 ((v0 . v0)(v1 . (@ v1))(v2 . v1))) ((= (+ (* v0 (@ v1)) (+ (* v0 v1) (* (@ v1) v1))) (* v0 (+ (@ v1) (+ (* v0 v1) (* (@ v1) v1)))))))
(85 (paramod 84 (1 1) 13 (1 1)) ((= (* v0 (+ (@ v1) (+ (* v0 v1) (* (@ v1) v1)))) v0)))
(86 (instantiate 39 ((v0 . (* (1) v0))(v1 . (1)))) ((= (* (+ (* (1) v0) (1)) (+ (1) (1))) (+ (1) (1)))))
(87 (paramod 63 (1 1) 86 (1 1 1)) ((= (* (* (1) (+ v0 (1))) (+ (1) (1))) (+ (1) (1)))))
(88 (instantiate 5 ((v0 . (@ v0))(v1 . v65)(v2 . (+ (@ v0) (+ v0 v0))))) ((= (+ (* (@ v0) v65) (* (@ v0) (+ (@ v0) (+ v0 v0)))) (* (@ v0) (+ v65 (+ (@ v0) (+ v0 v0)))))))
(89 (paramod 77 (1 1) 88 (1 1 2)) ((= (+ (* (@ v0) v65) (@ v0)) (* (@ v0) (+ v65 (+ (@ v0) (+ v0 v0)))))))
(90 (instantiate 89 ((v65 . v1))) ((= (+ (* (@ v0) v1) (@ v0)) (* (@ v0) (+ v1 (+ (@ v0) (+ v0 v0)))))))
(91 (instantiate 85 ((v0 . (* (1) (+ v0 (1))))(v1 . (1)))) ((= (* (* (1) (+ v0 (1))) (+ (@ (1)) (+ (* (* (1) (+ v0 (1))) (1)) (* (@ (1)) (1))))) (* (1) (+ v0 (1))))))
(92 (paramod 60 (1 1) 91 (1 1 2 2 1)) ((= (* (* (1) (+ v0 (1))) (+ (@ (1)) (+ (1) (* (@ (1)) (1))))) (* (1) (+ v0 (1))))))
(93 (paramod 67 (1 1) 92 (1 1 2)) ((= (* (* (1) (+ v0 (1))) (1)) (* (1) (+ v0 (1))))))
(94 (paramod 60 (1 1) 93 (1 1)) ((= (1) (* (1) (+ v0 (1))))))
(95 (flip 94 (1)) ((= (* (1) (+ v0 (1))) (1))))
(96 (paramod 95 (1 1) 87 (1 1 1)) ((= (* (1) (+ (1) (1))) (+ (1) (1)))))
(97 (instantiate 95 ((v0 . (1)))) ((= (* (1) (+ (1) (1))) (1))))
(98 (paramod 97 (1 1) 96 (1 1)) ((= (1) (+ (1) (1)))))
(99 (flip 98 (1)) ((= (+ (1) (1)) (1))))
(100 (instantiate 95 ((v0 . (@ v0)))) ((= (* (1) (+ (@ v0) (1))) (1))))
(101 (paramod 100 (1 1) 56 (1 1)) ((= (1) (+ (@ v0) (1)))))
(102 (flip 101 (1)) ((= (+ (@ v0) (1)) (1))))
(103 (instantiate 77 ((v0 . (1)))) ((= (* (@ (1)) (+ (@ (1)) (+ (1) (1)))) (@ (1)))))
(104 (paramod 99 (1 1) 103 (1 1 2 2)) ((= (* (@ (1)) (+ (@ (1)) (1))) (@ (1)))))
(105 (instantiate 102 ((v0 . (1)))) ((= (+ (@ (1)) (1)) (1))))
(106 (paramod 105 (1 1) 104 (1 1 2)) ((= (* (@ (1)) (1)) (@ (1)))))
(107 (instantiate 71 ((v0 . (1))(v1 . v65))) ((= (+ (@ (1)) (+ (* (+ v65 (@ (1))) (1)) (* (@ (1)) (1)))) (+ v65 (@ (1))))))
(108 (paramod 106 (1 1) 107 (1 1 2 2)) ((= (+ (@ (1)) (+ (* (+ v65 (@ (1))) (1)) (@ (1)))) (+ v65 (@ (1))))))
(109 (instantiate 28 ((v0 . v65)(v1 . (@ (1)))(v2 . (1)))) ((= (+ (* (+ v65 (@ (1))) (1)) (@ (1))) (* (+ v65 (@ (1))) (+ (1) (@ (1)))))))
(110 (paramod 109 (1 1) 108 (1 1 2)) ((= (+ (@ (1)) (* (+ v65 (@ (1))) (+ (1) (@ (1))))) (+ v65 (@ (1))))))
(111 (instantiate 6 ((v0 . (1)))) ((= (+ (1) (@ (1))) (1))))
(112 (paramod 111 (1 1) 110 (1 1 2 2)) ((= (+ (@ (1)) (* (+ v65 (@ (1))) (1))) (+ v65 (@ (1))))))
(113 (instantiate 24 ((v0 . (@ (1)))(v1 . v65)(v2 . (1)))) ((= (+ (@ (1)) (* (+ v65 (@ (1))) (1))) (* (+ v65 (@ (1))) (+ (@ (1)) (1))))))
(114 (paramod 113 (1 1) 112 (1 1)) ((= (* (+ v65 (@ (1))) (+ (@ (1)) (1))) (+ v65 (@ (1))))))
(115 (instantiate 102 ((v0 . (1)))) ((= (+ (@ (1)) (1)) (1))))
(116 (paramod 115 (1 1) 114 (1 1 2)) ((= (* (+ v65 (@ (1))) (1)) (+ v65 (@ (1))))))
(117 (instantiate 116 ((v65 . v0))) ((= (* (+ v0 (@ (1))) (1)) (+ v0 (@ (1))))))
(118 (instantiate 85 ((v0 . v64)(v1 . (1)))) ((= (* v64 (+ (@ (1)) (+ (* v64 (1)) (* (@ (1)) (1))))) v64)))
(119 (paramod 106 (1 1) 118 (1 1 2 2 2)) ((= (* v64 (+ (@ (1)) (+ (* v64 (1)) (@ (1))))) v64)))
(120 (instantiate 119 ((v64 . v0))) ((= (* v0 (+ (@ (1)) (+ (* v0 (1)) (@ (1))))) v0)))
(121 (instantiate 83 ((v0 . v64)(v1 . (1)))) ((= (* v64 (+ (* v64 (1)) (* (@ (1)) (1)))) (+ (* v64 (1)) (* (@ (1)) (1))))))
(122 (paramod 106 (1 1) 121 (1 1 2 2)) ((= (* v64 (+ (* v64 (1)) (@ (1)))) (+ (* v64 (1)) (* (@ (1)) (1))))))
(123 (paramod 106 (1 1) 122 (1 2 2)) ((= (* v64 (+ (* v64 (1)) (@ (1)))) (+ (* v64 (1)) (@ (1))))))
(124 (instantiate 123 ((v64 . v0))) ((= (* v0 (+ (* v0 (1)) (@ (1)))) (+ (* v0 (1)) (@ (1))))))
(125 (instantiate 90 ((v0 . (1))(v1 . (1)))) ((= (+ (* (@ (1)) (1)) (@ (1))) (* (@ (1)) (+ (1) (+ (@ (1)) (+ (1) (1))))))))
(126 (paramod 106 (1 1) 125 (1 1 1)) ((= (+ (@ (1)) (@ (1))) (* (@ (1)) (+ (1) (+ (@ (1)) (+ (1) (1))))))))
(127 (paramod 99 (1 1) 126 (1 2 2 2 2)) ((= (+ (@ (1)) (@ (1))) (* (@ (1)) (+ (1) (+ (@ (1)) (1)))))))
(128 (instantiate 102 ((v0 . (1)))) ((= (+ (@ (1)) (1)) (1))))
(129 (paramod 128 (1 1) 127 (1 2 2 2)) ((= (+ (@ (1)) (@ (1))) (* (@ (1)) (+ (1) (1))))))
(130 (paramod 99 (1 1) 129 (1 2 2)) ((= (+ (@ (1)) (@ (1))) (* (@ (1)) (1)))))
(131 (paramod 106 (1 1) 130 (1 2)) ((= (+ (@ (1)) (@ (1))) (@ (1)))))
(132 (instantiate 81 ((v0 . (@ (1)))(v1 . v65)(v2 . (1)))) ((= (+ (* (@ (1)) v65) (+ (* (@ (1)) (1)) (* (@ (1)) (1)))) (* (@ (1)) (+ v65 (+ (* (@ (1)) (1)) (* (@ (1)) (1))))))))
(133 (paramod 106 (1 1) 132 (1 1 2 1)) ((= (+ (* (@ (1)) v65) (+ (@ (1)) (* (@ (1)) (1)))) (* (@ (1)) (+ v65 (+ (* (@ (1)) (1)) (* (@ (1)) (1))))))))
(134 (paramod 106 (1 1) 133 (1 1 2 2)) ((= (+ (* (@ (1)) v65) (+ (@ (1)) (@ (1)))) (* (@ (1)) (+ v65 (+ (* (@ (1)) (1)) (* (@ (1)) (1))))))))
(135 (paramod 131 (1 1) 134 (1 1 2)) ((= (+ (* (@ (1)) v65) (@ (1))) (* (@ (1)) (+ v65 (+ (* (@ (1)) (1)) (* (@ (1)) (1))))))))
(136 (instantiate 90 ((v0 . (1))(v1 . v65))) ((= (+ (* (@ (1)) v65) (@ (1))) (* (@ (1)) (+ v65 (+ (@ (1)) (+ (1) (1))))))))
(137 (paramod 136 (1 1) 135 (1 1)) ((= (* (@ (1)) (+ v65 (+ (@ (1)) (+ (1) (1))))) (* (@ (1)) (+ v65 (+ (* (@ (1)) (1)) (* (@ (1)) (1))))))))
(138 (paramod 99 (1 1) 137 (1 1 2 2 2)) ((= (* (@ (1)) (+ v65 (+ (@ (1)) (1)))) (* (@ (1)) (+ v65 (+ (* (@ (1)) (1)) (* (@ (1)) (1))))))))
(139 (instantiate 102 ((v0 . (1)))) ((= (+ (@ (1)) (1)) (1))))
(140 (paramod 139 (1 1) 138 (1 1 2 2)) ((= (* (@ (1)) (+ v65 (1))) (* (@ (1)) (+ v65 (+ (* (@ (1)) (1)) (* (@ (1)) (1))))))))
(141 (paramod 106 (1 1) 140 (1 2 2 2 1)) ((= (* (@ (1)) (+ v65 (1))) (* (@ (1)) (+ v65 (+ (@ (1)) (* (@ (1)) (1))))))))
(142 (paramod 106 (1 1) 141 (1 2 2 2 2)) ((= (* (@ (1)) (+ v65 (1))) (* (@ (1)) (+ v65 (+ (@ (1)) (@ (1))))))))
(143 (paramod 131 (1 1) 142 (1 2 2 2)) ((= (* (@ (1)) (+ v65 (1))) (* (@ (1)) (+ v65 (@ (1)))))))
(144 (flip 143 (1)) ((= (* (@ (1)) (+ v65 (@ (1)))) (* (@ (1)) (+ v65 (1))))))
(145 (instantiate 144 ((v65 . v0))) ((= (* (@ (1)) (+ v0 (@ (1)))) (* (@ (1)) (+ v0 (1))))))
(146 (instantiate 117 ((v0 . v65))) ((= (* (+ v65 (@ (1))) (1)) (+ v65 (@ (1))))))
(147 (instantiate 24 ((v0 . (@ (1)))(v1 . v65)(v2 . (1)))) ((= (+ (@ (1)) (* (+ v65 (@ (1))) (1))) (* (+ v65 (@ (1))) (+ (@ (1)) (1))))))
(148 (paramod 146 (1 1) 147 (1 1 2)) ((= (+ (@ (1)) (+ v65 (@ (1)))) (* (+ v65 (@ (1))) (+ (@ (1)) (1))))))
(149 (instantiate 102 ((v0 . (1)))) ((= (+ (@ (1)) (1)) (1))))
(150 (paramod 149 (1 1) 148 (1 2 2)) ((= (+ (@ (1)) (+ v65 (@ (1)))) (* (+ v65 (@ (1))) (1)))))
(151 (instantiate 117 ((v0 . v65))) ((= (* (+ v65 (@ (1))) (1)) (+ v65 (@ (1))))))
(152 (paramod 151 (1 1) 150 (1 2)) ((= (+ (@ (1)) (+ v65 (@ (1)))) (+ v65 (@ (1))))))
(153 (instantiate 152 ((v65 . v0))) ((= (+ (@ (1)) (+ v0 (@ (1)))) (+ v0 (@ (1))))))
(154 (instantiate 153 ((v0 . (* v0 (1))))) ((= (+ (@ (1)) (+ (* v0 (1)) (@ (1)))) (+ (* v0 (1)) (@ (1))))))
(155 (paramod 154 (1 1) 120 (1 1 2)) ((= (* v0 (+ (* v0 (1)) (@ (1)))) v0)))
(156 (paramod 124 (1 1) 155 (1 1)) ((= (+ (* v0 (1)) (@ (1))) v0)))
(157 (paramod 156 (1 1) 124 (1 1 2)) ((= (* v0 v0) (+ (* v0 (1)) (@ (1))))))
(158 (paramod 156 (1 1) 157 (1 2)) ((= (* v0 v0) v0)))
(159 (instantiate 3 ((v1 . (1)))) ((= (* (+ v0 (1)) (1)) (1))))
(160 (instantiate 156 ((v0 . (+ v0 (1))))) ((= (+ (* (+ v0 (1)) (1)) (@ (1))) (+ v0 (1)))))
(161 (paramod 159 (1 1) 160 (1 1 1)) ((= (+ (1) (@ (1))) (+ v0 (1)))))
(162 (instantiate 6 ((v0 . (1)))) ((= (+ (1) (@ (1))) (1))))
(163 (paramod 162 (1 1) 161 (1 1)) ((= (1) (+ v0 (1)))))
(164 (flip 163 (1)) ((= (+ v0 (1)) (1))))
(165 (paramod 164 (1 1) 145 (1 2 2)) ((= (* (@ (1)) (+ v0 (@ (1)))) (* (@ (1)) (1)))))
(166 (paramod 106 (1 1) 165 (1 2)) ((= (* (@ (1)) (+ v0 (@ (1)))) (@ (1)))))
(167 (instantiate 153 ((v0 . (* v0 (1))))) ((= (+ (@ (1)) (+ (* v0 (1)) (@ (1)))) (+ (* v0 (1)) (@ (1))))))
(168 (paramod 156 (1 1) 167 (1 1 2)) ((= (+ (@ (1)) v0) (+ (* v0 (1)) (@ (1))))))
(169 (paramod 156 (1 1) 168 (1 2)) ((= (+ (@ (1)) v0) v0)))
(170 (instantiate 117 ((v0 . (* v0 (1))))) ((= (* (+ (* v0 (1)) (@ (1))) (1)) (+ (* v0 (1)) (@ (1))))))
(171 (paramod 156 (1 1) 170 (1 1 1)) ((= (* v0 (1)) (+ (* v0 (1)) (@ (1))))))
(172 (paramod 156 (1 1) 171 (1 2)) ((= (* v0 (1)) v0)))
(173 (instantiate 52 ((v0 . (* v0 (1)))(v1 . (1)))) ((= (* (* (+ (* v0 (1)) (@ (1))) (1)) (@ (1))) (@ (1)))))
(174 (paramod 156 (1 1) 173 (1 1 1 1)) ((= (* (* v0 (1)) (@ (1))) (@ (1)))))
(175 (paramod 172 (1 1) 174 (1 1 1)) ((= (* v0 (@ (1))) (@ (1)))))
(176 (paramod 172 (1 1) 156 (1 1 1)) ((= (+ v0 (@ (1))) v0)))
(177 (paramod 176 (1 1) 166 (1 1 2)) ((= (* (@ (1)) v0) (@ (1)))))
(178 (instantiate 158 ((v0 . v66))) ((= (* v66 v66) v66)))
(179 (instantiate 5 ((v0 . v66)(v1 . v65)(v2 . v66))) ((= (+ (* v66 v65) (* v66 v66)) (* v66 (+ v65 v66)))))
(180 (paramod 178 (1 1) 179 (1 1 2)) ((= (+ (* v66 v65) v66) (* v66 (+ v65 v66)))))
(181 (instantiate 180 ((v65 . v1)(v66 . v0))) ((= (+ (* v0 v1) v0) (* v0 (+ v1 v0)))))
(182 (instantiate 158 ((v0 . v65))) ((= (* v65 v65) v65)))
(183 (instantiate 5 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (+ (* v65 v65) (* v65 v66)) (* v65 (+ v65 v66)))))
(184 (paramod 182 (1 1) 183 (1 1 1)) ((= (+ v65 (* v65 v66)) (* v65 (+ v65 v66)))))
(185 (instantiate 184 ((v65 . v0)(v66 . v1))) ((= (+ v0 (* v0 v1)) (* v0 (+ v0 v1)))))
(186 (instantiate 172 ((v0 . v64))) ((= (* v64 (1)) v64)))
(187 (instantiate 5 ((v0 . v64)(v1 . v65)(v2 . (1)))) ((= (+ (* v64 v65) (* v64 (1))) (* v64 (+ v65 (1))))))
(188 (paramod 186 (1 1) 187 (1 1 2)) ((= (+ (* v64 v65) v64) (* v64 (+ v65 (1))))))
(189 (instantiate 181 ((v0 . v64)(v1 . v65))) ((= (+ (* v64 v65) v64) (* v64 (+ v65 v64)))))
(190 (paramod 189 (1 1) 188 (1 1)) ((= (* v64 (+ v65 v64)) (* v64 (+ v65 (1))))))
(191 (instantiate 164 ((v0 . v65))) ((= (+ v65 (1)) (1))))
(192 (paramod 191 (1 1) 190 (1 2 2)) ((= (* v64 (+ v65 v64)) (* v64 (1)))))
(193 (instantiate 172 ((v0 . v64))) ((= (* v64 (1)) v64)))
(194 (paramod 193 (1 1) 192 (1 2)) ((= (* v64 (+ v65 v64)) v64)))
(195 (instantiate 194 ((v64 . v0)(v65 . v1))) ((= (* v0 (+ v1 v0)) v0)))
(196 (instantiate 172 ((v0 . v64))) ((= (* v64 (1)) v64)))
(197 (instantiate 5 ((v0 . v64)(v1 . (1))(v2 . v66))) ((= (+ (* v64 (1)) (* v64 v66)) (* v64 (+ (1) v66)))))
(198 (paramod 196 (1 1) 197 (1 1 1)) ((= (+ v64 (* v64 v66)) (* v64 (+ (1) v66)))))
(199 (instantiate 185 ((v0 . v64)(v1 . v66))) ((= (+ v64 (* v64 v66)) (* v64 (+ v64 v66)))))
(200 (paramod 199 (1 1) 198 (1 1)) ((= (* v64 (+ v64 v66)) (* v64 (+ (1) v66)))))
(201 (instantiate 200 ((v64 . v0)(v66 . v1))) ((= (* v0 (+ v0 v1)) (* v0 (+ (1) v1)))))
(202 (paramod 195 (1 1) 181 (1 2)) ((= (+ (* v0 v1) v0) v0)))
(203 (instantiate 175 ((v0 . (@ v64)))) ((= (* (@ v64) (@ (1))) (@ (1)))))
(204 (instantiate 10 ((v0 . v64)(v1 . (@ (1))))) ((= (+ (* v64 (@ v64)) (+ (* v64 (@ (1))) (* (@ v64) (@ (1))))) (@ (1)))))
(205 (paramod 203 (1 1) 204 (1 1 2 2)) ((= (+ (* v64 (@ v64)) (+ (* v64 (@ (1))) (@ (1)))) (@ (1)))))
(206 (instantiate 175 ((v0 . v64))) ((= (* v64 (@ (1))) (@ (1)))))
(207 (paramod 206 (1 1) 205 (1 1 2 1)) ((= (+ (* v64 (@ v64)) (+ (@ (1)) (@ (1)))) (@ (1)))))
(208 (instantiate 176 ((v0 . (@ (1))))) ((= (+ (@ (1)) (@ (1))) (@ (1)))))
(209 (paramod 208 (1 1) 207 (1 1 2)) ((= (+ (* v64 (@ v64)) (@ (1))) (@ (1)))))
(210 (instantiate 176 ((v0 . (* v64 (@ v64))))) ((= (+ (* v64 (@ v64)) (@ (1))) (* v64 (@ v64)))))
(211 (paramod 210 (1 1) 209 (1 1)) ((= (* v64 (@ v64)) (@ (1)))))
(212 (instantiate 211 ((v64 . v0))) ((= (* v0 (@ v0)) (@ (1)))))
(213 (flip 212 (1)) ((= (@ (1)) (* v0 (@ v0)))))
(214 (instantiate 83 ((v0 . (@ (1))))) ((= (* (@ (1)) (+ (* (@ (1)) v1) (* (@ v1) v1))) (+ (* (@ (1)) v1) (* (@ v1) v1)))))
(215 (instantiate 177 ((v0 . (+ (* (@ (1)) v1) (* (@ v1) v1))))) ((= (* (@ (1)) (+ (* (@ (1)) v1) (* (@ v1) v1))) (@ (1)))))
(216 (paramod 214 (1 1) 215 (1 1)) ((= (+ (* (@ (1)) v1) (* (@ v1) v1)) (@ (1)))))
(217 (instantiate 177 ((v0 . v1))) ((= (* (@ (1)) v1) (@ (1)))))
(218 (paramod 217 (1 1) 216 (1 1 1)) ((= (+ (@ (1)) (* (@ v1) v1)) (@ (1)))))
(219 (instantiate 169 ((v0 . (* (@ v1) v1)))) ((= (+ (@ (1)) (* (@ v1) v1)) (* (@ v1) v1))))
(220 (paramod 219 (1 1) 218 (1 1)) ((= (* (@ v1) v1) (@ (1)))))
(221 (instantiate 220 ((v1 . v0))) ((= (* (@ v0) v0) (@ (1)))))
(222 (instantiate 195 ((v0 . v64))) ((= (* v64 (+ v1 v64)) v64)))
(223 (instantiate 5 ((v0 . v64)(v1 . (+ v1 v64))(v2 . v66))) ((= (+ (* v64 (+ v1 v64)) (* v64 v66)) (* v64 (+ (+ v1 v64) v66)))))
(224 (paramod 222 (1 1) 223 (1 1 1)) ((= (+ v64 (* v64 v66)) (* v64 (+ (+ v1 v64) v66)))))
(225 (instantiate 185 ((v0 . v64)(v1 . v66))) ((= (+ v64 (* v64 v66)) (* v64 (+ v64 v66)))))
(226 (paramod 225 (1 1) 224 (1 1)) ((= (* v64 (+ v64 v66)) (* v64 (+ (+ v1 v64) v66)))))
(227 (flip 226 (1)) ((= (* v64 (+ (+ v1 v64) v66)) (* v64 (+ v64 v66)))))
(228 (instantiate 227 ((v64 . v0)(v66 . v2))) ((= (* v0 (+ (+ v1 v0) v2)) (* v0 (+ v0 v2)))))
(229 (instantiate 6 ((v0 . v64))) ((= (+ v64 (@ v64)) (1))))
(230 (instantiate 201 ((v0 . v64)(v1 . (@ v64)))) ((= (* v64 (+ v64 (@ v64))) (* v64 (+ (1) (@ v64))))))
(231 (paramod 229 (1 1) 230 (1 1 2)) ((= (* v64 (1)) (* v64 (+ (1) (@ v64))))))
(232 (instantiate 172 ((v0 . v64))) ((= (* v64 (1)) v64)))
(233 (paramod 232 (1 1) 231 (1 1)) ((= v64 (* v64 (+ (1) (@ v64))))))
(234 (flip 233 (1)) ((= (* v64 (+ (1) (@ v64))) v64)))
(235 (instantiate 234 ((v64 . v0))) ((= (* v0 (+ (1) (@ v0))) v0)))
(236 (instantiate 212 ((v0 . (@ v64)))) ((= (* (@ v64) (@ (@ v64))) (@ (1)))))
(237 (instantiate 10 ((v0 . v64)(v1 . (@ (@ v64))))) ((= (+ (* v64 (@ v64)) (+ (* v64 (@ (@ v64))) (* (@ v64) (@ (@ v64))))) (@ (@ v64)))))
(238 (paramod 236 (1 1) 237 (1 1 2 2)) ((= (+ (* v64 (@ v64)) (+ (* v64 (@ (@ v64))) (@ (1)))) (@ (@ v64)))))
(239 (instantiate 176 ((v0 . (* v64 (@ (@ v64)))))) ((= (+ (* v64 (@ (@ v64))) (@ (1))) (* v64 (@ (@ v64))))))
(240 (paramod 239 (1 1) 238 (1 1 2)) ((= (+ (* v64 (@ v64)) (* v64 (@ (@ v64)))) (@ (@ v64)))))
(241 (instantiate 5 ((v0 . v64)(v1 . (@ v64))(v2 . (@ (@ v64))))) ((= (+ (* v64 (@ v64)) (* v64 (@ (@ v64)))) (* v64 (+ (@ v64) (@ (@ v64)))))))
(242 (paramod 241 (1 1) 240 (1 1)) ((= (* v64 (+ (@ v64) (@ (@ v64)))) (@ (@ v64)))))
(243 (instantiate 6 ((v0 . (@ v64)))) ((= (+ (@ v64) (@ (@ v64))) (1))))
(244 (paramod 243 (1 1) 242 (1 1 2)) ((= (* v64 (1)) (@ (@ v64)))))
(245 (instantiate 172 ((v0 . v64))) ((= (* v64 (1)) v64)))
(246 (paramod 245 (1 1) 244 (1 1)) ((= v64 (@ (@ v64)))))
(247 (flip 246 (1)) ((= (@ (@ v64)) v64)))
(248 (instantiate 247 ((v64 . v0))) ((= (@ (@ v0)) v0)))
(249 (instantiate 212 ((v0 . v64))) ((= (* v64 (@ v64)) (@ (1)))))
(250 (instantiate 10 ((v0 . v64)(v1 . v65))) ((= (+ (* v64 (@ v64)) (+ (* v64 v65) (* (@ v64) v65))) v65)))
(251 (paramod 249 (1 1) 250 (1 1 1)) ((= (+ (@ (1)) (+ (* v64 v65) (* (@ v64) v65))) v65)))
(252 (instantiate 169 ((v0 . (+ (* v64 v65) (* (@ v64) v65))))) ((= (+ (@ (1)) (+ (* v64 v65) (* (@ v64) v65))) (+ (* v64 v65) (* (@ v64) v65)))))
(253 (paramod 252 (1 1) 251 (1 1)) ((= (+ (* v64 v65) (* (@ v64) v65)) v65)))
(254 (instantiate 253 ((v64 . v0)(v65 . v1))) ((= (+ (* v0 v1) (* (@ v0) v1)) v1)))
(255 (instantiate 213 ((v0 . v64))) ((= (@ (1)) (* v64 (@ v64)))))
(256 (paramod 213 (1 1) 255 (1 1)) ((= (* v0 (@ v0)) (* v64 (@ v64)))))
(257 (instantiate 256 ((v64 . v1))) ((= (* v0 (@ v0)) (* v1 (@ v1)))))
(258 (instantiate 221 ((v0 . v66))) ((= (* (@ v66) v66) (@ (1)))))
(259 (instantiate 5 ((v0 . (@ v66))(v1 . v65)(v2 . v66))) ((= (+ (* (@ v66) v65) (* (@ v66) v66)) (* (@ v66) (+ v65 v66)))))
(260 (paramod 258 (1 1) 259 (1 1 2)) ((= (+ (* (@ v66) v65) (@ (1))) (* (@ v66) (+ v65 v66)))))
(261 (instantiate 176 ((v0 . (* (@ v66) v65)))) ((= (+ (* (@ v66) v65) (@ (1))) (* (@ v66) v65))))
(262 (paramod 261 (1 1) 260 (1 1)) ((= (* (@ v66) v65) (* (@ v66) (+ v65 v66)))))
(263 (flip 262 (1)) ((= (* (@ v66) (+ v65 v66)) (* (@ v66) v65))))
(264 (instantiate 263 ((v65 . v1)(v66 . v0))) ((= (* (@ v0) (+ v1 v0)) (* (@ v0) v1))))
(265 (instantiate 221 ((v0 . v65))) ((= (* (@ v65) v65) (@ (1)))))
(266 (instantiate 5 ((v0 . (@ v65))(v1 . v65)(v2 . v66))) ((= (+ (* (@ v65) v65) (* (@ v65) v66)) (* (@ v65) (+ v65 v66)))))
(267 (paramod 265 (1 1) 266 (1 1 1)) ((= (+ (@ (1)) (* (@ v65) v66)) (* (@ v65) (+ v65 v66)))))
(268 (instantiate 169 ((v0 . (* (@ v65) v66)))) ((= (+ (@ (1)) (* (@ v65) v66)) (* (@ v65) v66))))
(269 (paramod 268 (1 1) 267 (1 1)) ((= (* (@ v65) v66) (* (@ v65) (+ v65 v66)))))
(270 (flip 269 (1)) ((= (* (@ v65) (+ v65 v66)) (* (@ v65) v66))))
(271 (instantiate 270 ((v65 . v0)(v66 . v1))) ((= (* (@ v0) (+ v0 v1)) (* (@ v0) v1))))
(272 (instantiate 201 ((v0 . v64))) ((= (* v64 (+ v64 v1)) (* v64 (+ (1) v1)))))
(273 (instantiate 254 ((v0 . v64)(v1 . (+ v64 v1)))) ((= (+ (* v64 (+ v64 v1)) (* (@ v64) (+ v64 v1))) (+ v64 v1))))
(274 (paramod 272 (1 1) 273 (1 1 1)) ((= (+ (* v64 (+ (1) v1)) (* (@ v64) (+ v64 v1))) (+ v64 v1))))
(275 (instantiate 271 ((v0 . v64)(v1 . v1))) ((= (* (@ v64) (+ v64 v1)) (* (@ v64) v1))))
(276 (paramod 275 (1 1) 274 (1 1 2)) ((= (+ (* v64 (+ (1) v1)) (* (@ v64) v1)) (+ v64 v1))))
(277 (instantiate 276 ((v64 . v0))) ((= (+ (* v0 (+ (1) v1)) (* (@ v0) v1)) (+ v0 v1))))
(278 (instantiate 235 ((v0 . (@ v64)))) ((= (* (@ v64) (+ (1) (@ (@ v64)))) (@ v64))))
(279 (instantiate 254 ((v0 . v64)(v1 . (+ (1) (@ (@ v64)))))) ((= (+ (* v64 (+ (1) (@ (@ v64)))) (* (@ v64) (+ (1) (@ (@ v64))))) (+ (1) (@ (@ v64))))))
(280 (paramod 278 (1 1) 279 (1 1 2)) ((= (+ (* v64 (+ (1) (@ (@ v64)))) (@ v64)) (+ (1) (@ (@ v64))))))
(281 (instantiate 248 ((v0 . v64))) ((= (@ (@ v64)) v64)))
(282 (paramod 281 (1 1) 280 (1 1 1 2 2)) ((= (+ (* v64 (+ (1) v64)) (@ v64)) (+ (1) (@ (@ v64))))))
(283 (instantiate 195 ((v0 . v64)(v1 . (1)))) ((= (* v64 (+ (1) v64)) v64)))
(284 (paramod 283 (1 1) 282 (1 1 1)) ((= (+ v64 (@ v64)) (+ (1) (@ (@ v64))))))
(285 (instantiate 6 ((v0 . v64))) ((= (+ v64 (@ v64)) (1))))
(286 (paramod 285 (1 1) 284 (1 1)) ((= (1) (+ (1) (@ (@ v64))))))
(287 (instantiate 248 ((v0 . v64))) ((= (@ (@ v64)) v64)))
(288 (paramod 287 (1 1) 286 (1 2 2)) ((= (1) (+ (1) v64))))
(289 (flip 288 (1)) ((= (+ (1) v64) (1))))
(290 (instantiate 289 ((v64 . v0))) ((= (+ (1) v0) (1))))
(291 (instantiate 290 ((v0 . v1))) ((= (+ (1) v1) (1))))
(292 (paramod 291 (1 1) 277 (1 1 1 2)) ((= (+ (* v0 (1)) (* (@ v0) v1)) (+ v0 v1))))
(293 (paramod 172 (1 1) 292 (1 1 1)) ((= (+ v0 (* (@ v0) v1)) (+ v0 v1))))
(294 (instantiate 290 ((v0 . v1))) ((= (+ (1) v1) (1))))
(295 (paramod 294 (1 1) 201 (1 2 2)) ((= (* v0 (+ v0 v1)) (* v0 (1)))))
(296 (paramod 172 (1 1) 295 (1 2)) ((= (* v0 (+ v0 v1)) v0)))
(297 (instantiate 296 ((v0 . v0)(v1 . v2))) ((= (* v0 (+ v0 v2)) v0)))
(298 (paramod 297 (1 1) 228 (1 2)) ((= (* v0 (+ (+ v1 v0) v2)) v0)))
(299 (paramod 296 (1 1) 185 (1 2)) ((= (+ v0 (* v0 v1)) v0)))
(300 (instantiate 5 ((v0 . (@ v0))(v1 . (+ v1 v0))(v2 . v66))) ((= (+ (* (@ v0) (+ v1 v0)) (* (@ v0) v66)) (* (@ v0) (+ (+ v1 v0) v66)))))
(301 (paramod 264 (1 1) 300 (1 1 1)) ((= (+ (* (@ v0) v1) (* (@ v0) v66)) (* (@ v0) (+ (+ v1 v0) v66)))))
(302 (instantiate 5 ((v0 . (@ v0))(v1 . v1)(v2 . v66))) ((= (+ (* (@ v0) v1) (* (@ v0) v66)) (* (@ v0) (+ v1 v66)))))
(303 (paramod 302 (1 1) 301 (1 1)) ((= (* (@ v0) (+ v1 v66)) (* (@ v0) (+ (+ v1 v0) v66)))))
(304 (flip 303 (1)) ((= (* (@ v0) (+ (+ v1 v0) v66)) (* (@ v0) (+ v1 v66)))))
(305 (instantiate 304 ((v66 . v2))) ((= (* (@ v0) (+ (+ v1 v0) v2)) (* (@ v0) (+ v1 v2)))))
(306 (instantiate 271 ((v0 . v64))) ((= (* (@ v64) (+ v64 v1)) (* (@ v64) v1))))
(307 (instantiate 293 ((v0 . v64)(v1 . (+ v64 v1)))) ((= (+ v64 (* (@ v64) (+ v64 v1))) (+ v64 (+ v64 v1)))))
(308 (paramod 306 (1 1) 307 (1 1 2)) ((= (+ v64 (* (@ v64) v1)) (+ v64 (+ v64 v1)))))
(309 (instantiate 293 ((v0 . v64)(v1 . v1))) ((= (+ v64 (* (@ v64) v1)) (+ v64 v1))))
(310 (paramod 309 (1 1) 308 (1 1)) ((= (+ v64 v1) (+ v64 (+ v64 v1)))))
(311 (flip 310 (1)) ((= (+ v64 (+ v64 v1)) (+ v64 v1))))
(312 (instantiate 311 ((v64 . v0))) ((= (+ v0 (+ v0 v1)) (+ v0 v1))))
(313 (instantiate 298 ((v0 . v64))) ((= (* v64 (+ (+ v1 v64) v2)) v64)))
(314 (instantiate 254 ((v0 . v64)(v1 . (+ (+ v1 v64) v2)))) ((= (+ (* v64 (+ (+ v1 v64) v2)) (* (@ v64) (+ (+ v1 v64) v2))) (+ (+ v1 v64) v2))))
(315 (paramod 313 (1 1) 314 (1 1 1)) ((= (+ v64 (* (@ v64) (+ (+ v1 v64) v2))) (+ (+ v1 v64) v2))))
(316 (instantiate 305 ((v0 . v64)(v1 . v1)(v2 . v2))) ((= (* (@ v64) (+ (+ v1 v64) v2)) (* (@ v64) (+ v1 v2)))))
(317 (paramod 316 (1 1) 315 (1 1 2)) ((= (+ v64 (* (@ v64) (+ v1 v2))) (+ (+ v1 v64) v2))))
(318 (instantiate 293 ((v0 . v64)(v1 . (+ v1 v2)))) ((= (+ v64 (* (@ v64) (+ v1 v2))) (+ v64 (+ v1 v2)))))
(319 (paramod 318 (1 1) 317 (1 1)) ((= (+ v64 (+ v1 v2)) (+ (+ v1 v64) v2))))
(320 (flip 319 (1)) ((= (+ (+ v1 v64) v2) (+ v64 (+ v1 v2)))))
(321 (instantiate 320 ((v1 . v0)(v64 . v1))) ((= (+ (+ v0 v1) v2) (+ v1 (+ v0 v2)))))
(322 (instantiate 312 ((v0 . (* v0 v1))(v1 . (* (@ v0) v1)))) ((= (+ (* v0 v1) (+ (* v0 v1) (* (@ v0) v1))) (+ (* v0 v1) (* (@ v0) v1)))))
(323 (paramod 254 (1 1) 322 (1 1 2)) ((= (+ (* v0 v1) v1) (+ (* v0 v1) (* (@ v0) v1)))))
(324 (paramod 254 (1 1) 323 (1 2)) ((= (+ (* v0 v1) v1) v1)))
(325 (instantiate 324 ((v0 . (A))(v1 . (B)))) ((= (+ (* (A) (B)) (B)) (B))))
(326 (paramod 325 (1 1) 2 (2 1 1)) ((not (= (+ (A) (* (B) (C))) (* (+ (A) (B)) (+ (A) (C))))) (not (= (B) (B))) (not (= (* (B) (@ (B))) (* (A) (@ (A)))))))
(327 (instantiate 1 ((v0 . (B)))) ((= (B) (B))))
(328 (resolve 326 (2) 327 (1)) ((not (= (+ (A) (* (B) (C))) (* (+ (A) (B)) (+ (A) (C))))) (not (= (* (B) (@ (B))) (* (A) (@ (A)))))))
(329 (instantiate 257 ((v0 . (B))(v1 . (A)))) ((= (* (B) (@ (B))) (* (A) (@ (A))))))
(330 (resolve 328 (2) 329 (1)) ((not (= (+ (A) (* (B) (C))) (* (+ (A) (B)) (+ (A) (C)))))))
(331 (instantiate 324 ((v1 . v65))) ((= (+ (* v0 v65) v65) v65)))
(332 (instantiate 321 ((v0 . (* v0 v65))(v1 . v65)(v2 . v66))) ((= (+ (+ (* v0 v65) v65) v66) (+ v65 (+ (* v0 v65) v66)))))
(333 (paramod 331 (1 1) 332 (1 1 1)) ((= (+ v65 v66) (+ v65 (+ (* v0 v65) v66)))))
(334 (flip 333 (1)) ((= (+ v65 (+ (* v0 v65) v66)) (+ v65 v66))))
(335 (instantiate 334 ((v0 . v1)(v65 . v0)(v66 . v2))) ((= (+ v0 (+ (* v1 v0) v2)) (+ v0 v2))))
(336 (instantiate 176 ((v0 . (* v65 v64)))) ((= (+ (* v65 v64) (@ (1))) (* v65 v64))))
(337 (instantiate 335 ((v0 . v64)(v1 . v65)(v2 . (@ (1))))) ((= (+ v64 (+ (* v65 v64) (@ (1)))) (+ v64 (@ (1))))))
(338 (paramod 336 (1 1) 337 (1 1 2)) ((= (+ v64 (* v65 v64)) (+ v64 (@ (1))))))
(339 (instantiate 176 ((v0 . v64))) ((= (+ v64 (@ (1))) v64)))
(340 (paramod 339 (1 1) 338 (1 2)) ((= (+ v64 (* v65 v64)) v64)))
(341 (instantiate 340 ((v64 . v0)(v65 . v1))) ((= (+ v0 (* v1 v0)) v0)))
(342 (instantiate 5 ((v0 . v65)(v1 . v64))) ((= (+ (* v65 v64) (* v65 v2)) (* v65 (+ v64 v2)))))
(343 (instantiate 335 ((v0 . v64)(v1 . v65)(v2 . (* v65 v2)))) ((= (+ v64 (+ (* v65 v64) (* v65 v2))) (+ v64 (* v65 v2)))))
(344 (paramod 342 (1 1) 343 (1 1 2)) ((= (+ v64 (* v65 (+ v64 v2))) (+ v64 (* v65 v2)))))
(345 (instantiate 344 ((v64 . v0)(v65 . v1))) ((= (+ v0 (* v1 (+ v0 v2))) (+ v0 (* v1 v2)))))
(346 (instantiate 341 ((v0 . v65))) ((= (+ v65 (* v1 v65)) v65)))
(347 (instantiate 24 ((v0 . (* v1 v65))(v1 . v65)(v2 . v66))) ((= (+ (* v1 v65) (* (+ v65 (* v1 v65)) v66)) (* (+ v65 (* v1 v65)) (+ (* v1 v65) v66)))))
(348 (paramod 346 (1 1) 347 (1 1 2 1)) ((= (+ (* v1 v65) (* v65 v66)) (* (+ v65 (* v1 v65)) (+ (* v1 v65) v66)))))
(349 (instantiate 341 ((v0 . v65)(v1 . v1))) ((= (+ v65 (* v1 v65)) v65)))
(350 (paramod 349 (1 1) 348 (1 2 1)) ((= (+ (* v1 v65) (* v65 v66)) (* v65 (+ (* v1 v65) v66)))))
(351 (instantiate 350 ((v1 . v0)(v65 . v1)(v66 . v2))) ((= (+ (* v0 v1) (* v1 v2)) (* v1 (+ (* v0 v1) v2)))))
(352 (instantiate 341 ((v0 . v64))) ((= (+ v64 (* v1 v64)) v64)))
(353 (instantiate 28 ((v0 . v64)(v1 . (* v1 v64))(v2 . v66))) ((= (+ (* (+ v64 (* v1 v64)) v66) (* v1 v64)) (* (+ v64 (* v1 v64)) (+ v66 (* v1 v64))))))
(354 (paramod 352 (1 1) 353 (1 1 1 1)) ((= (+ (* v64 v66) (* v1 v64)) (* (+ v64 (* v1 v64)) (+ v66 (* v1 v64))))))
(355 (instantiate 341 ((v0 . v64)(v1 . v1))) ((= (+ v64 (* v1 v64)) v64)))
(356 (paramod 355 (1 1) 354 (1 2 1)) ((= (+ (* v64 v66) (* v1 v64)) (* v64 (+ v66 (* v1 v64))))))
(357 (instantiate 356 ((v1 . v2)(v64 . v0)(v66 . v1))) ((= (+ (* v0 v1) (* v2 v0)) (* v0 (+ v1 (* v2 v0))))))
(358 (instantiate 296 ((v0 . v64))) ((= (* v64 (+ v64 v1)) v64)))
(359 (instantiate 351 ((v0 . v64)(v1 . (+ v64 v1))(v2 . v66))) ((= (+ (* v64 (+ v64 v1)) (* (+ v64 v1) v66)) (* (+ v64 v1) (+ (* v64 (+ v64 v1)) v66)))))
(360 (paramod 358 (1 1) 359 (1 1 1)) ((= (+ v64 (* (+ v64 v1) v66)) (* (+ v64 v1) (+ (* v64 (+ v64 v1)) v66)))))
(361 (instantiate 296 ((v0 . v64)(v1 . v1))) ((= (* v64 (+ v64 v1)) v64)))
(362 (paramod 361 (1 1) 360 (1 2 2 1)) ((= (+ v64 (* (+ v64 v1) v66)) (* (+ v64 v1) (+ v64 v66)))))
(363 (instantiate 362 ((v64 . v0)(v66 . v2))) ((= (+ v0 (* (+ v0 v1) v2)) (* (+ v0 v1) (+ v0 v2)))))
(364 (instantiate 351 ((v0 . v64)(v1 . v66)(v2 . v64))) ((= (+ (* v64 v66) (* v66 v64)) (* v66 (+ (* v64 v66) v64)))))
(365 (instantiate 357 ((v0 . v64)(v1 . v66)(v2 . v66))) ((= (+ (* v64 v66) (* v66 v64)) (* v64 (+ v66 (* v66 v64))))))
(366 (paramod 364 (1 1) 365 (1 1)) ((= (* v66 (+ (* v64 v66) v64)) (* v64 (+ v66 (* v66 v64))))))
(367 (instantiate 202 ((v0 . v64)(v1 . v66))) ((= (+ (* v64 v66) v64) v64)))
(368 (paramod 367 (1 1) 366 (1 1 2)) ((= (* v66 v64) (* v64 (+ v66 (* v66 v64))))))
(369 (instantiate 299 ((v0 . v66)(v1 . v64))) ((= (+ v66 (* v66 v64)) v66)))
(370 (paramod 369 (1 1) 368 (1 2 2)) ((= (* v66 v64) (* v64 v66))))
(371 (instantiate 370 ((v64 . v1)(v66 . v0))) ((= (* v0 v1) (* v1 v0))))
(372 (instantiate 371 ((v0 . v65)(v1 . (+ v64 v66)))) ((= (* v65 (+ v64 v66)) (* (+ v64 v66) v65))))
(373 (instantiate 345 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (+ v64 (* v65 (+ v64 v66))) (+ v64 (* v65 v66)))))
(374 (paramod 372 (1 1) 373 (1 1 2)) ((= (+ v64 (* (+ v64 v66) v65)) (+ v64 (* v65 v66)))))
(375 (instantiate 363 ((v0 . v64)(v1 . v66)(v2 . v65))) ((= (+ v64 (* (+ v64 v66) v65)) (* (+ v64 v66) (+ v64 v65)))))
(376 (paramod 375 (1 1) 374 (1 1)) ((= (* (+ v64 v66) (+ v64 v65)) (+ v64 (* v65 v66)))))
(377 (flip 376 (1)) ((= (+ v64 (* v65 v66)) (* (+ v64 v66) (+ v64 v65)))))
(378 (instantiate 377 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (+ v0 (* v1 v2)) (* (+ v0 v2) (+ v0 v1)))))
(379 (instantiate 378 ((v0 . (A))(v1 . (B))(v2 . (C)))) ((= (+ (A) (* (B) (C))) (* (+ (A) (C)) (+ (A) (B))))))
(380 (paramod 379 (1 1) 330 (1 1 1)) ((not (= (* (+ (A) (C)) (+ (A) (B))) (* (+ (A) (B)) (+ (A) (C)))))))
(381 (instantiate 371 ((v0 . (+ (A) (C)))(v1 . (+ (A) (B))))) ((= (* (+ (A) (C)) (+ (A) (B))) (* (+ (A) (B)) (+ (A) (C))))))
(382 (resolve 380 (1) 381 (1)) ())
)