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