(
(1 (input) ((not (= (+ v0 v0) v0))))
(2 (input) ((= (+ v0 v1) (+ v1 v0))))
(3 (input) ((= (+ (+ v0 v1) v2) (+ v0 (+ v1 v2)))))
(4 (input) ((= (+ v0 (+ v1 v2)) (+ v1 (+ v0 v2)))))
(5 (input) ((= (+ (C) (D)) (C))))
(6 (input) ((= (n (+ (n (+ v0 v1)) (n (+ v0 (n v1))))) v0)))
(7 (instantiate 3 ((v0 . (C))(v1 . (D))(v2 . v66))) ((= (+ (+ (C) (D)) v66) (+ (C) (+ (D) v66)))))
(8 (paramod 5 (1 1) 7 (1 1 1)) ((= (+ (C) v66) (+ (C) (+ (D) v66)))))
(9 (flip 8 (1)) ((= (+ (C) (+ (D) v66)) (+ (C) v66))))
(10 (instantiate 9 ((v66 . v0))) ((= (+ (C) (+ (D) v0)) (+ (C) v0))))
(11 (instantiate 6 ((v0 . (C))(v1 . (+ (D) v0)))) ((= (n (+ (n (+ (C) (+ (D) v0))) (n (+ (C) (n (+ (D) v0)))))) (C))))
(12 (paramod 10 (1 1) 11 (1 1 1 1 1)) ((= (n (+ (n (+ (C) v0)) (n (+ (C) (n (+ (D) v0)))))) (C))))
(13 (instantiate 4 ((v0 . v64))) ((= (+ v64 (+ v1 v2)) (+ v1 (+ v64 v2)))))
(14 (instantiate 6 ((v0 . v64)(v1 . (+ v1 v2)))) ((= (n (+ (n (+ v64 (+ v1 v2))) (n (+ v64 (n (+ v1 v2)))))) v64)))
(15 (paramod 13 (1 1) 14 (1 1 1 1 1)) ((= (n (+ (n (+ v1 (+ v64 v2))) (n (+ v64 (n (+ v1 v2)))))) v64)))
(16 (instantiate 15 ((v1 . v0)(v64 . v1))) ((= (n (+ (n (+ v0 (+ v1 v2))) (n (+ v1 (n (+ v0 v2)))))) v1)))
(17 (instantiate 2 ((v0 . v64)(v1 . v65))) ((= (+ v64 v65) (+ v65 v64))))
(18 (instantiate 6 ((v0 . v64)(v1 . v65))) ((= (n (+ (n (+ v64 v65)) (n (+ v64 (n v65))))) v64)))
(19 (paramod 17 (1 1) 18 (1 1 1 1 1)) ((= (n (+ (n (+ v65 v64)) (n (+ v64 (n v65))))) v64)))
(20 (instantiate 19 ((v64 . v1)(v65 . v0))) ((= (n (+ (n (+ v0 v1)) (n (+ v1 (n v0))))) v1)))
(21 (instantiate 6 ((v0 . v64)(v1 . (+ (n (+ v0 v1)) (n (+ v0 (n v1))))))) ((= (n (+ (n (+ v64 (+ (n (+ v0 v1)) (n (+ v0 (n v1)))))) (n (+ v64 (n (+ (n (+ v0 v1)) (n (+ v0 (n v1))))))))) v64)))
(22 (paramod 6 (1 1) 21 (1 1 1 2 1 2)) ((= (n (+ (n (+ v64 (+ (n (+ v0 v1)) (n (+ v0 (n v1)))))) (n (+ v64 v0)))) v64)))
(23 (instantiate 2 ((v0 . (n (+ v64 (+ (n (+ v0 v1)) (n (+ v0 (n v1)))))))(v1 . (n (+ v64 v0))))) ((= (+ (n (+ v64 (+ (n (+ v0 v1)) (n (+ v0 (n v1)))))) (n (+ v64 v0))) (+ (n (+ v64 v0)) (n (+ v64 (+ (n (+ v0 v1)) (n (+ v0 (n v1))))))))))
(24 (paramod 23 (1 1) 22 (1 1 1)) ((= (n (+ (n (+ v64 v0)) (n (+ v64 (+ (n (+ v0 v1)) (n (+ v0 (n v1)))))))) v64)))
(25 (instantiate 24 ((v0 . v1)(v1 . v2)(v64 . v0))) ((= (n (+ (n (+ v0 v1)) (n (+ v0 (+ (n (+ v1 v2)) (n (+ v1 (n v2)))))))) v0)))
(26 (instantiate 2 ((v0 . v64)(v1 . (n v65)))) ((= (+ v64 (n v65)) (+ (n v65) v64))))
(27 (instantiate 6 ((v0 . v64)(v1 . v65))) ((= (n (+ (n (+ v64 v65)) (n (+ v64 (n v65))))) v64)))
(28 (paramod 26 (1 1) 27 (1 1 1 2 1)) ((= (n (+ (n (+ v64 v65)) (n (+ (n v65) v64)))) v64)))
(29 (instantiate 28 ((v64 . v0)(v65 . v1))) ((= (n (+ (n (+ v0 v1)) (n (+ (n v1) v0)))) v0)))
(30 (instantiate 2 ((v0 . (C))(v1 . v64))) ((= (+ (C) v64) (+ v64 (C)))))
(31 (instantiate 12 ((v0 . v64))) ((= (n (+ (n (+ (C) v64)) (n (+ (C) (n (+ (D) v64)))))) (C))))
(32 (paramod 30 (1 1) 31 (1 1 1 1 1)) ((= (n (+ (n (+ v64 (C))) (n (+ (C) (n (+ (D) v64)))))) (C))))
(33 (instantiate 32 ((v64 . v0))) ((= (n (+ (n (+ v0 (C))) (n (+ (C) (n (+ (D) v0)))))) (C))))
(34 (instantiate 20 ((v0 . (C))(v1 . (D)))) ((= (n (+ (n (+ (C) (D))) (n (+ (D) (n (C)))))) (D))))
(35 (paramod 5 (1 1) 34 (1 1 1 1 1)) ((= (n (+ (n (C)) (n (+ (D) (n (C)))))) (D))))
(36 (instantiate 2 ((v0 . v65)(v1 . (n v64)))) ((= (+ v65 (n v64)) (+ (n v64) v65))))
(37 (instantiate 20 ((v0 . v64)(v1 . v65))) ((= (n (+ (n (+ v64 v65)) (n (+ v65 (n v64))))) v65)))
(38 (paramod 36 (1 1) 37 (1 1 1 2 1)) ((= (n (+ (n (+ v64 v65)) (n (+ (n v64) v65)))) v65)))
(39 (instantiate 38 ((v64 . v0)(v65 . v1))) ((= (n (+ (n (+ v0 v1)) (n (+ (n v0) v1)))) v1)))
(40 (instantiate 2 ((v0 . (n (+ v64 v65)))(v1 . (n (+ v65 (n v64)))))) ((= (+ (n (+ v64 v65)) (n (+ v65 (n v64)))) (+ (n (+ v65 (n v64))) (n (+ v64 v65))))))
(41 (instantiate 20 ((v0 . v64)(v1 . v65))) ((= (n (+ (n (+ v64 v65)) (n (+ v65 (n v64))))) v65)))
(42 (paramod 40 (1 1) 41 (1 1 1)) ((= (n (+ (n (+ v65 (n v64))) (n (+ v64 v65)))) v65)))
(43 (instantiate 42 ((v64 . v1)(v65 . v0))) ((= (n (+ (n (+ v0 (n v1))) (n (+ v1 v0)))) v0)))
(44 (instantiate 29 ((v0 . v64)(v1 . (+ (n (+ v0 v1)) (n (+ v1 (n v0))))))) ((= (n (+ (n (+ v64 (+ (n (+ v0 v1)) (n (+ v1 (n v0)))))) (n (+ (n (+ (n (+ v0 v1)) (n (+ v1 (n v0))))) v64)))) v64)))
(45 (paramod 20 (1 1) 44 (1 1 1 2 1 1)) ((= (n (+ (n (+ v64 (+ (n (+ v0 v1)) (n (+ v1 (n v0)))))) (n (+ v1 v64)))) v64)))
(46 (instantiate 45 ((v0 . v1)(v1 . v2)(v64 . v0))) ((= (n (+ (n (+ v0 (+ (n (+ v1 v2)) (n (+ v2 (n v1)))))) (n (+ v2 v0)))) v0)))
(47 (instantiate 29 ((v0 . (n (+ (D) (n (C)))))(v1 . (C)))) ((= (n (+ (n (+ (n (+ (D) (n (C)))) (C))) (n (+ (n (C)) (n (+ (D) (n (C)))))))) (n (+ (D) (n (C)))))))
(48 (paramod 35 (1 1) 47 (1 1 1 2)) ((= (n (+ (n (+ (n (+ (D) (n (C)))) (C))) (D))) (n (+ (D) (n (C)))))))
(49 (instantiate 2 ((v0 . (n (+ (D) (n (C)))))(v1 . (C)))) ((= (+ (n (+ (D) (n (C)))) (C)) (+ (C) (n (+ (D) (n (C))))))))
(50 (paramod 49 (1 1) 48 (1 1 1 1 1)) ((= (n (+ (n (+ (C) (n (+ (D) (n (C)))))) (D))) (n (+ (D) (n (C)))))))
(51 (instantiate 2 ((v0 . (n (+ (C) (n (+ (D) (n (C)))))))(v1 . (D)))) ((= (+ (n (+ (C) (n (+ (D) (n (C)))))) (D)) (+ (D) (n (+ (C) (n (+ (D) (n (C))))))))))
(52 (paramod 51 (1 1) 50 (1 1 1)) ((= (n (+ (D) (n (+ (C) (n (+ (D) (n (C)))))))) (n (+ (D) (n (C)))))))
(53 (instantiate 29 ((v0 . (n (+ (n v1) v0)))(v1 . (+ v0 v1)))) ((= (n (+ (n (+ (n (+ (n v1) v0)) (+ v0 v1))) (n (+ (n (+ v0 v1)) (n (+ (n v1) v0)))))) (n (+ (n v1) v0)))))
(54 (paramod 29 (1 1) 53 (1 1 1 2)) ((= (n (+ (n (+ (n (+ (n v1) v0)) (+ v0 v1))) v0)) (n (+ (n v1) v0)))))
(55 (instantiate 4 ((v0 . (n (+ (n v1) v0)))(v1 . v0)(v2 . v1))) ((= (+ (n (+ (n v1) v0)) (+ v0 v1)) (+ v0 (+ (n (+ (n v1) v0)) v1)))))
(56 (paramod 55 (1 1) 54 (1 1 1 1 1)) ((= (n (+ (n (+ v0 (+ (n (+ (n v1) v0)) v1))) v0)) (n (+ (n v1) v0)))))
(57 (instantiate 2 ((v0 . (n (+ (n v1) v0)))(v1 . v1))) ((= (+ (n (+ (n v1) v0)) v1) (+ v1 (n (+ (n v1) v0))))))
(58 (paramod 57 (1 1) 56 (1 1 1 1 1 2)) ((= (n (+ (n (+ v0 (+ v1 (n (+ (n v1) v0))))) v0)) (n (+ (n v1) v0)))))
(59 (instantiate 2 ((v0 . (n (+ v0 (+ v1 (n (+ (n v1) v0))))))(v1 . v0))) ((= (+ (n (+ v0 (+ v1 (n (+ (n v1) v0))))) v0) (+ v0 (n (+ v0 (+ v1 (n (+ (n v1) v0)))))))))
(60 (paramod 59 (1 1) 58 (1 1 1)) ((= (n (+ v0 (n (+ v0 (+ v1 (n (+ (n v1) v0))))))) (n (+ (n v1) v0)))))
(61 (instantiate 3 ((v2 . v65))) ((= (+ (+ v0 v1) v65) (+ v0 (+ v1 v65)))))
(62 (instantiate 39 ((v0 . (+ v0 v1))(v1 . v65))) ((= (n (+ (n (+ (+ v0 v1) v65)) (n (+ (n (+ v0 v1)) v65)))) v65)))
(63 (paramod 61 (1 1) 62 (1 1 1 1 1)) ((= (n (+ (n (+ v0 (+ v1 v65))) (n (+ (n (+ v0 v1)) v65)))) v65)))
(64 (instantiate 63 ((v65 . v2))) ((= (n (+ (n (+ v0 (+ v1 v2))) (n (+ (n (+ v0 v1)) v2)))) v2)))
(65 (instantiate 39 ((v0 . (+ v0 v1))(v1 . (n (+ (n v0) v1))))) ((= (n (+ (n (+ (+ v0 v1) (n (+ (n v0) v1)))) (n (+ (n (+ v0 v1)) (n (+ (n v0) v1)))))) (n (+ (n v0) v1)))))
(66 (paramod 39 (1 1) 65 (1 1 1 2)) ((= (n (+ (n (+ (+ v0 v1) (n (+ (n v0) v1)))) v1)) (n (+ (n v0) v1)))))
(67 (instantiate 3 ((v0 . v0)(v1 . v1)(v2 . (n (+ (n v0) v1))))) ((= (+ (+ v0 v1) (n (+ (n v0) v1))) (+ v0 (+ v1 (n (+ (n v0) v1)))))))
(68 (paramod 67 (1 1) 66 (1 1 1 1 1)) ((= (n (+ (n (+ v0 (+ v1 (n (+ (n v0) v1))))) v1)) (n (+ (n v0) v1)))))
(69 (instantiate 2 ((v0 . (n (+ v0 (+ v1 (n (+ (n v0) v1))))))(v1 . v1))) ((= (+ (n (+ v0 (+ v1 (n (+ (n v0) v1))))) v1) (+ v1 (n (+ v0 (+ v1 (n (+ (n v0) v1)))))))))
(70 (paramod 69 (1 1) 68 (1 1 1)) ((= (n (+ v1 (n (+ v0 (+ v1 (n (+ (n v0) v1))))))) (n (+ (n v0) v1)))))
(71 (instantiate 70 ((v0 . v1)(v1 . v0))) ((= (n (+ v0 (n (+ v1 (+ v0 (n (+ (n v1) v0))))))) (n (+ (n v1) v0)))))
(72 (instantiate 10 ((v0 . v66))) ((= (+ (C) (+ (D) v66)) (+ (C) v66))))
(73 (instantiate 16 ((v0 . (C))(v1 . (D))(v2 . v66))) ((= (n (+ (n (+ (C) (+ (D) v66))) (n (+ (D) (n (+ (C) v66)))))) (D))))
(74 (paramod 72 (1 1) 73 (1 1 1 1 1)) ((= (n (+ (n (+ (C) v66)) (n (+ (D) (n (+ (C) v66)))))) (D))))
(75 (instantiate 74 ((v66 . v0))) ((= (n (+ (n (+ (C) v0)) (n (+ (D) (n (+ (C) v0)))))) (D))))
(76 (instantiate 4 ((v0 . v65))) ((= (+ v65 (+ v1 v2)) (+ v1 (+ v65 v2)))))
(77 (instantiate 43 ((v0 . (+ v1 v2))(v1 . v65))) ((= (n (+ (n (+ (+ v1 v2) (n v65))) (n (+ v65 (+ v1 v2))))) (+ v1 v2))))
(78 (paramod 76 (1 1) 77 (1 1 1 2 1)) ((= (n (+ (n (+ (+ v1 v2) (n v65))) (n (+ v1 (+ v65 v2))))) (+ v1 v2))))
(79 (instantiate 3 ((v0 . v1)(v1 . v2)(v2 . (n v65)))) ((= (+ (+ v1 v2) (n v65)) (+ v1 (+ v2 (n v65))))))
(80 (paramod 79 (1 1) 78 (1 1 1 1 1)) ((= (n (+ (n (+ v1 (+ v2 (n v65)))) (n (+ v1 (+ v65 v2))))) (+ v1 v2))))
(81 (instantiate 80 ((v1 . v0)(v2 . v1)(v65 . v2))) ((= (n (+ (n (+ v0 (+ v1 (n v2)))) (n (+ v0 (+ v2 v1))))) (+ v0 v1))))
(82 (instantiate 3 ((v2 . v64))) ((= (+ (+ v0 v1) v64) (+ v0 (+ v1 v64)))))
(83 (instantiate 43 ((v0 . v64)(v1 . (+ v0 v1)))) ((= (n (+ (n (+ v64 (n (+ v0 v1)))) (n (+ (+ v0 v1) v64)))) v64)))
(84 (paramod 82 (1 1) 83 (1 1 1 2 1)) ((= (n (+ (n (+ v64 (n (+ v0 v1)))) (n (+ v0 (+ v1 v64))))) v64)))
(85 (instantiate 84 ((v0 . v1)(v1 . v2)(v64 . v0))) ((= (n (+ (n (+ v0 (n (+ v1 v2)))) (n (+ v1 (+ v2 v0))))) v0)))
(86 (instantiate 2 ((v0 . (n (+ v64 (C))))(v1 . (n (+ (C) (n (+ (D) v64))))))) ((= (+ (n (+ v64 (C))) (n (+ (C) (n (+ (D) v64))))) (+ (n (+ (C) (n (+ (D) v64)))) (n (+ v64 (C)))))))
(87 (instantiate 33 ((v0 . v64))) ((= (n (+ (n (+ v64 (C))) (n (+ (C) (n (+ (D) v64)))))) (C))))
(88 (paramod 86 (1 1) 87 (1 1 1)) ((= (n (+ (n (+ (C) (n (+ (D) v64)))) (n (+ v64 (C))))) (C))))
(89 (instantiate 88 ((v64 . v0))) ((= (n (+ (n (+ (C) (n (+ (D) v0)))) (n (+ v0 (C))))) (C))))
(90 (instantiate 25 ((v0 . v64)(v1 . (n (+ v0 (n v1))))(v2 . (+ v1 v0)))) ((= (n (+ (n (+ v64 (n (+ v0 (n v1))))) (n (+ v64 (+ (n (+ (n (+ v0 (n v1))) (+ v1 v0))) (n (+ (n (+ v0 (n v1))) (n (+ v1 v0))))))))) v64)))
(91 (paramod 43 (1 1) 90 (1 1 1 2 1 2 2)) ((= (n (+ (n (+ v64 (n (+ v0 (n v1))))) (n (+ v64 (+ (n (+ (n (+ v0 (n v1))) (+ v1 v0))) v0))))) v64)))
(92 (instantiate 4 ((v0 . (n (+ v0 (n v1))))(v1 . v1)(v2 . v0))) ((= (+ (n (+ v0 (n v1))) (+ v1 v0)) (+ v1 (+ (n (+ v0 (n v1))) v0)))))
(93 (paramod 92 (1 1) 91 (1 1 1 2 1 2 1 1)) ((= (n (+ (n (+ v64 (n (+ v0 (n v1))))) (n (+ v64 (+ (n (+ v1 (+ (n (+ v0 (n v1))) v0))) v0))))) v64)))
(94 (instantiate 2 ((v0 . (n (+ v0 (n v1))))(v1 . v0))) ((= (+ (n (+ v0 (n v1))) v0) (+ v0 (n (+ v0 (n v1)))))))
(95 (paramod 94 (1 1) 93 (1 1 1 2 1 2 1 1 2)) ((= (n (+ (n (+ v64 (n (+ v0 (n v1))))) (n (+ v64 (+ (n (+ v1 (+ v0 (n (+ v0 (n v1)))))) v0))))) v64)))
(96 (instantiate 2 ((v0 . (n (+ v1 (+ v0 (n (+ v0 (n v1)))))))(v1 . v0))) ((= (+ (n (+ v1 (+ v0 (n (+ v0 (n v1)))))) v0) (+ v0 (n (+ v1 (+ v0 (n (+ v0 (n v1))))))))))
(97 (paramod 96 (1 1) 95 (1 1 1 2 1 2)) ((= (n (+ (n (+ v64 (n (+ v0 (n v1))))) (n (+ v64 (+ v0 (n (+ v1 (+ v0 (n (+ v0 (n v1))))))))))) v64)))
(98 (instantiate 97 ((v0 . v1)(v1 . v2)(v64 . v0))) ((= (n (+ (n (+ v0 (n (+ v1 (n v2))))) (n (+ v0 (+ v1 (n (+ v2 (+ v1 (n (+ v1 (n v2))))))))))) v0)))
(99 (instantiate 2 ((v0 . (C))(v1 . v64))) ((= (+ (C) v64) (+ v64 (C)))))
(100 (instantiate 75 ((v0 . v64))) ((= (n (+ (n (+ (C) v64)) (n (+ (D) (n (+ (C) v64)))))) (D))))
(101 (paramod 99 (1 1) 100 (1 1 1 1 1)) ((= (n (+ (n (+ v64 (C))) (n (+ (D) (n (+ (C) v64)))))) (D))))
(102 (instantiate 101 ((v64 . v0))) ((= (n (+ (n (+ v0 (C))) (n (+ (D) (n (+ (C) v0)))))) (D))))
(103 (instantiate 2 ((v0 . (n (+ v64 (C))))(v1 . (n (+ (D) (n (+ (C) v64))))))) ((= (+ (n (+ v64 (C))) (n (+ (D) (n (+ (C) v64))))) (+ (n (+ (D) (n (+ (C) v64)))) (n (+ v64 (C)))))))
(104 (instantiate 102 ((v0 . v64))) ((= (n (+ (n (+ v64 (C))) (n (+ (D) (n (+ (C) v64)))))) (D))))
(105 (paramod 103 (1 1) 104 (1 1 1)) ((= (n (+ (n (+ (D) (n (+ (C) v64)))) (n (+ v64 (C))))) (D))))
(106 (instantiate 105 ((v64 . v0))) ((= (n (+ (n (+ (D) (n (+ (C) v0)))) (n (+ v0 (C))))) (D))))
(107 (instantiate 20 ((v0 . (+ (n (+ (D) (n (+ (C) v0)))) (n (+ v0 (C)))))(v1 . v65))) ((= (n (+ (n (+ (+ (n (+ (D) (n (+ (C) v0)))) (n (+ v0 (C)))) v65)) (n (+ v65 (n (+ (n (+ (D) (n (+ (C) v0)))) (n (+ v0 (C))))))))) v65)))
(108 (paramod 106 (1 1) 107 (1 1 1 2 1 2)) ((= (n (+ (n (+ (+ (n (+ (D) (n (+ (C) v0)))) (n (+ v0 (C)))) v65)) (n (+ v65 (D))))) v65)))
(109 (instantiate 3 ((v0 . (n (+ (D) (n (+ (C) v0)))))(v1 . (n (+ v0 (C))))(v2 . v65))) ((= (+ (+ (n (+ (D) (n (+ (C) v0)))) (n (+ v0 (C)))) v65) (+ (n (+ (D) (n (+ (C) v0)))) (+ (n (+ v0 (C))) v65)))))
(110 (paramod 109 (1 1) 108 (1 1 1 1 1)) ((= (n (+ (n (+ (n (+ (D) (n (+ (C) v0)))) (+ (n (+ v0 (C))) v65))) (n (+ v65 (D))))) v65)))
(111 (instantiate 110 ((v65 . v1))) ((= (n (+ (n (+ (n (+ (D) (n (+ (C) v0)))) (+ (n (+ v0 (C))) v1))) (n (+ v1 (D))))) v1)))
(112 (instantiate 4 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (+ v64 (+ v65 v66)) (+ v65 (+ v64 v66)))))
(113 (instantiate 64 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (n (+ (n (+ v64 (+ v65 v66))) (n (+ (n (+ v64 v65)) v66)))) v66)))
(114 (paramod 112 (1 1) 113 (1 1 1 1 1)) ((= (n (+ (n (+ v65 (+ v64 v66))) (n (+ (n (+ v64 v65)) v66)))) v66)))
(115 (instantiate 114 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (n (+ (n (+ v0 (+ v1 v2))) (n (+ (n (+ v1 v0)) v2)))) v2)))
(116 (instantiate 2 ((v0 . v65)(v1 . v66))) ((= (+ v65 v66) (+ v66 v65))))
(117 (instantiate 85 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (n (+ (n (+ v64 (n (+ v65 v66)))) (n (+ v65 (+ v66 v64))))) v64)))
(118 (paramod 116 (1 1) 117 (1 1 1 1 1 2 1)) ((= (n (+ (n (+ v64 (n (+ v66 v65)))) (n (+ v65 (+ v66 v64))))) v64)))
(119 (instantiate 118 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (n (+ (n (+ v0 (n (+ v1 v2)))) (n (+ v2 (+ v1 v0))))) v0)))
(120 (instantiate 119 ((v0 . (+ (D) v0))(v1 . (C))(v2 . v66))) ((= (n (+ (n (+ (+ (D) v0) (n (+ (C) v66)))) (n (+ v66 (+ (C) (+ (D) v0)))))) (+ (D) v0))))
(121 (paramod 10 (1 1) 120 (1 1 1 2 1 2)) ((= (n (+ (n (+ (+ (D) v0) (n (+ (C) v66)))) (n (+ v66 (+ (C) v0))))) (+ (D) v0))))
(122 (instantiate 3 ((v0 . (D))(v1 . v0)(v2 . (n (+ (C) v66))))) ((= (+ (+ (D) v0) (n (+ (C) v66))) (+ (D) (+ v0 (n (+ (C) v66)))))))
(123 (paramod 122 (1 1) 121 (1 1 1 1 1)) ((= (n (+ (n (+ (D) (+ v0 (n (+ (C) v66))))) (n (+ v66 (+ (C) v0))))) (+ (D) v0))))
(124 (instantiate 123 ((v66 . v1))) ((= (n (+ (n (+ (D) (+ v0 (n (+ (C) v1))))) (n (+ v1 (+ (C) v0))))) (+ (D) v0))))
(125 (instantiate 46 ((v0 . (D))(v1 . v65)(v2 . (C)))) ((= (n (+ (n (+ (D) (+ (n (+ v65 (C))) (n (+ (C) (n v65)))))) (n (+ (C) (D))))) (D))))
(126 (paramod 5 (1 1) 125 (1 1 1 2 1)) ((= (n (+ (n (+ (D) (+ (n (+ v65 (C))) (n (+ (C) (n v65)))))) (n (C)))) (D))))
(127 (instantiate 2 ((v0 . (n (+ (D) (+ (n (+ v65 (C))) (n (+ (C) (n v65)))))))(v1 . (n (C))))) ((= (+ (n (+ (D) (+ (n (+ v65 (C))) (n (+ (C) (n v65)))))) (n (C))) (+ (n (C)) (n (+ (D) (+ (n (+ v65 (C))) (n (+ (C) (n v65))))))))))
(128 (paramod 127 (1 1) 126 (1 1 1)) ((= (n (+ (n (C)) (n (+ (D) (+ (n (+ v65 (C))) (n (+ (C) (n v65)))))))) (D))))
(129 (instantiate 128 ((v65 . v0))) ((= (n (+ (n (C)) (n (+ (D) (+ (n (+ v0 (C))) (n (+ (C) (n v0)))))))) (D))))
(130 (instantiate 89 ((v0 . (n (+ (C) (n (+ (D) (n (C))))))))) ((= (n (+ (n (+ (C) (n (+ (D) (n (+ (C) (n (+ (D) (n (C)))))))))) (n (+ (n (+ (C) (n (+ (D) (n (C)))))) (C))))) (C))))
(131 (paramod 52 (1 1) 130 (1 1 1 1 1 2)) ((= (n (+ (n (+ (C) (n (+ (D) (n (C)))))) (n (+ (n (+ (C) (n (+ (D) (n (C)))))) (C))))) (C))))
(132 (instantiate 2 ((v0 . (n (+ (C) (n (+ (D) (n (C)))))))(v1 . (C)))) ((= (+ (n (+ (C) (n (+ (D) (n (C)))))) (C)) (+ (C) (n (+ (C) (n (+ (D) (n (C))))))))))
(133 (paramod 132 (1 1) 131 (1 1 1 2 1)) ((= (n (+ (n (+ (C) (n (+ (D) (n (C)))))) (n (+ (C) (n (+ (C) (n (+ (D) (n (C)))))))))) (C))))
(134 (instantiate 60 ((v0 . (n (+ (D) (n (+ (C) v0)))))(v1 . (+ (C) v0)))) ((= (n (+ (n (+ (D) (n (+ (C) v0)))) (n (+ (n (+ (D) (n (+ (C) v0)))) (+ (+ (C) v0) (n (+ (n (+ (C) v0)) (n (+ (D) (n (+ (C) v0))))))))))) (n (+ (n (+ (C) v0)) (n (+ (D) (n (+ (C) v0)))))))))
(135 (paramod 75 (1 1) 134 (1 1 1 2 1 2 2)) ((= (n (+ (n (+ (D) (n (+ (C) v0)))) (n (+ (n (+ (D) (n (+ (C) v0)))) (+ (+ (C) v0) (D)))))) (n (+ (n (+ (C) v0)) (n (+ (D) (n (+ (C) v0)))))))))
(136 (instantiate 2 ((v0 . (+ (C) v0))(v1 . (D)))) ((= (+ (+ (C) v0) (D)) (+ (D) (+ (C) v0)))))
(137 (paramod 136 (1 1) 135 (1 1 1 2 1 2)) ((= (n (+ (n (+ (D) (n (+ (C) v0)))) (n (+ (n (+ (D) (n (+ (C) v0)))) (+ (D) (+ (C) v0)))))) (n (+ (n (+ (C) v0)) (n (+ (D) (n (+ (C) v0)))))))))
(138 (instantiate 4 ((v0 . (D))(v1 . (C))(v2 . v0))) ((= (+ (D) (+ (C) v0)) (+ (C) (+ (D) v0)))))
(139 (paramod 138 (1 1) 137 (1 1 1 2 1 2)) ((= (n (+ (n (+ (D) (n (+ (C) v0)))) (n (+ (n (+ (D) (n (+ (C) v0)))) (+ (C) (+ (D) v0)))))) (n (+ (n (+ (C) v0)) (n (+ (D) (n (+ (C) v0)))))))))
(140 (paramod 10 (1 1) 139 (1 1 1 2 1 2)) ((= (n (+ (n (+ (D) (n (+ (C) v0)))) (n (+ (n (+ (D) (n (+ (C) v0)))) (+ (C) v0))))) (n (+ (n (+ (C) v0)) (n (+ (D) (n (+ (C) v0)))))))))
(141 (instantiate 2 ((v0 . (n (+ (D) (n (+ (C) v0)))))(v1 . (+ (C) v0)))) ((= (+ (n (+ (D) (n (+ (C) v0)))) (+ (C) v0)) (+ (+ (C) v0) (n (+ (D) (n (+ (C) v0))))))))
(142 (paramod 141 (1 1) 140 (1 1 1 2 1)) ((= (n (+ (n (+ (D) (n (+ (C) v0)))) (n (+ (+ (C) v0) (n (+ (D) (n (+ (C) v0)))))))) (n (+ (n (+ (C) v0)) (n (+ (D) (n (+ (C) v0)))))))))
(143 (instantiate 3 ((v0 . (C))(v1 . v0)(v2 . (n (+ (D) (n (+ (C) v0))))))) ((= (+ (+ (C) v0) (n (+ (D) (n (+ (C) v0))))) (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0)))))))))
(144 (paramod 143 (1 1) 142 (1 1 1 2 1)) ((= (n (+ (n (+ (D) (n (+ (C) v0)))) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))))) (n (+ (n (+ (C) v0)) (n (+ (D) (n (+ (C) v0)))))))))
(145 (paramod 75 (1 1) 144 (1 2)) ((= (n (+ (n (+ (D) (n (+ (C) v0)))) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))))) (D))))
(146 (instantiate 2 ((v0 . v64)(v1 . (+ v65 (n v66))))) ((= (+ v64 (+ v65 (n v66))) (+ (+ v65 (n v66)) v64))))
(147 (instantiate 81 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (n (+ (n (+ v64 (+ v65 (n v66)))) (n (+ v64 (+ v66 v65))))) (+ v64 v65))))
(148 (paramod 146 (1 1) 147 (1 1 1 1 1)) ((= (n (+ (n (+ (+ v65 (n v66)) v64)) (n (+ v64 (+ v66 v65))))) (+ v64 v65))))
(149 (instantiate 3 ((v0 . v65)(v1 . (n v66))(v2 . v64))) ((= (+ (+ v65 (n v66)) v64) (+ v65 (+ (n v66) v64)))))
(150 (paramod 149 (1 1) 148 (1 1 1 1 1)) ((= (n (+ (n (+ v65 (+ (n v66) v64))) (n (+ v64 (+ v66 v65))))) (+ v64 v65))))
(151 (instantiate 150 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (n (+ (n (+ v0 (+ (n v1) v2))) (n (+ v2 (+ v1 v0))))) (+ v2 v0))))
(152 (instantiate 98 ((v0 . (n (+ (C) v0)))(v1 . (D))(v2 . (+ (C) v0)))) ((= (n (+ (n (+ (n (+ (C) v0)) (n (+ (D) (n (+ (C) v0)))))) (n (+ (n (+ (C) v0)) (+ (D) (n (+ (+ (C) v0) (+ (D) (n (+ (D) (n (+ (C) v0)))))))))))) (n (+ (C) v0)))))
(153 (paramod 75 (1 1) 152 (1 1 1 1)) ((= (n (+ (D) (n (+ (n (+ (C) v0)) (+ (D) (n (+ (+ (C) v0) (+ (D) (n (+ (D) (n (+ (C) v0)))))))))))) (n (+ (C) v0)))))
(154 (instantiate 4 ((v0 . (+ (C) v0))(v1 . (D))(v2 . (n (+ (D) (n (+ (C) v0))))))) ((= (+ (+ (C) v0) (+ (D) (n (+ (D) (n (+ (C) v0)))))) (+ (D) (+ (+ (C) v0) (n (+ (D) (n (+ (C) v0)))))))))
(155 (paramod 154 (1 1) 153 (1 1 1 2 1 2 2 1)) ((= (n (+ (D) (n (+ (n (+ (C) v0)) (+ (D) (n (+ (D) (+ (+ (C) v0) (n (+ (D) (n (+ (C) v0)))))))))))) (n (+ (C) v0)))))
(156 (instantiate 3 ((v0 . (C))(v1 . v0)(v2 . (n (+ (D) (n (+ (C) v0))))))) ((= (+ (+ (C) v0) (n (+ (D) (n (+ (C) v0))))) (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0)))))))))
(157 (paramod 156 (1 1) 155 (1 1 1 2 1 2 2 1 2)) ((= (n (+ (D) (n (+ (n (+ (C) v0)) (+ (D) (n (+ (D) (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))))))))) (n (+ (C) v0)))))
(158 (instantiate 4 ((v0 . (D))(v1 . (C))(v2 . (+ v0 (n (+ (D) (n (+ (C) v0)))))))) ((= (+ (D) (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))) (+ (C) (+ (D) (+ v0 (n (+ (D) (n (+ (C) v0))))))))))
(159 (paramod 158 (1 1) 157 (1 1 1 2 1 2 2 1)) ((= (n (+ (D) (n (+ (n (+ (C) v0)) (+ (D) (n (+ (C) (+ (D) (+ v0 (n (+ (D) (n (+ (C) v0))))))))))))) (n (+ (C) v0)))))
(160 (instantiate 10 ((v0 . (+ v0 (n (+ (D) (n (+ (C) v0)))))))) ((= (+ (C) (+ (D) (+ v0 (n (+ (D) (n (+ (C) v0))))))) (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0)))))))))
(161 (paramod 160 (1 1) 159 (1 1 1 2 1 2 2 1)) ((= (n (+ (D) (n (+ (n (+ (C) v0)) (+ (D) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0)))))))))))) (n (+ (C) v0)))))
(162 (instantiate 4 ((v0 . (n (+ (C) v0)))(v1 . (D))(v2 . (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0)))))))))) ((= (+ (n (+ (C) v0)) (+ (D) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))))) (+ (D) (+ (n (+ (C) v0)) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))))))))
(163 (paramod 162 (1 1) 161 (1 1 1 2 1)) ((= (n (+ (D) (n (+ (D) (+ (n (+ (C) v0)) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0)))))))))))) (n (+ (C) v0)))))
(164 (instantiate 115 ((v0 . (n (+ (C) v0)))(v1 . (D))(v2 . (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0)))))))))) ((= (n (+ (n (+ (n (+ (C) v0)) (+ (D) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0)))))))))) (n (+ (n (+ (D) (n (+ (C) v0)))) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))))))) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))))))
(165 (paramod 145 (1 1) 164 (1 1 1 2)) ((= (n (+ (n (+ (n (+ (C) v0)) (+ (D) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0)))))))))) (D))) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))))))
(166 (instantiate 4 ((v0 . (n (+ (C) v0)))(v1 . (D))(v2 . (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0)))))))))) ((= (+ (n (+ (C) v0)) (+ (D) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))))) (+ (D) (+ (n (+ (C) v0)) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))))))))
(167 (paramod 166 (1 1) 165 (1 1 1 1 1)) ((= (n (+ (n (+ (D) (+ (n (+ (C) v0)) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0)))))))))) (D))) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))))))
(168 (instantiate 2 ((v0 . (n (+ (D) (+ (n (+ (C) v0)) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0)))))))))))(v1 . (D)))) ((= (+ (n (+ (D) (+ (n (+ (C) v0)) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0)))))))))) (D)) (+ (D) (n (+ (D) (+ (n (+ (C) v0)) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))))))))))
(169 (paramod 168 (1 1) 167 (1 1 1)) ((= (n (+ (D) (n (+ (D) (+ (n (+ (C) v0)) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0)))))))))))) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))))))
(170 (paramod 163 (1 1) 169 (1 1)) ((= (n (+ (C) v0)) (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))))))
(171 (flip 170 (1)) ((= (n (+ (C) (+ v0 (n (+ (D) (n (+ (C) v0))))))) (n (+ (C) v0)))))
(172 (instantiate 171 ((v0 . (D)))) ((= (n (+ (C) (+ (D) (n (+ (D) (n (+ (C) (D)))))))) (n (+ (C) (D))))))
(173 (paramod 5 (1 1) 172 (1 1 1 2 2 1 2 1)) ((= (n (+ (C) (+ (D) (n (+ (D) (n (C))))))) (n (+ (C) (D))))))
(174 (instantiate 10 ((v0 . (n (+ (D) (n (C))))))) ((= (+ (C) (+ (D) (n (+ (D) (n (C)))))) (+ (C) (n (+ (D) (n (C))))))))
(175 (paramod 174 (1 1) 173 (1 1 1)) ((= (n (+ (C) (n (+ (D) (n (C)))))) (n (+ (C) (D))))))
(176 (paramod 5 (1 1) 175 (1 2 1)) ((= (n (+ (C) (n (+ (D) (n (C)))))) (n (C)))))
(177 (paramod 176 (1 1) 133 (1 1 1 1)) ((= (n (+ (n (C)) (n (+ (C) (n (+ (C) (n (+ (D) (n (C)))))))))) (C))))
(178 (paramod 176 (1 1) 177 (1 1 1 2 1 2)) ((= (n (+ (n (C)) (n (+ (C) (n (C)))))) (C))))
(179 (instantiate 98 ((v0 . (n (C)))(v1 . (C))(v2 . (C)))) ((= (n (+ (n (+ (n (C)) (n (+ (C) (n (C)))))) (n (+ (n (C)) (+ (C) (n (+ (C) (+ (C) (n (+ (C) (n (C)))))))))))) (n (C)))))
(180 (paramod 178 (1 1) 179 (1 1 1 1)) ((= (n (+ (C) (n (+ (n (C)) (+ (C) (n (+ (C) (+ (C) (n (+ (C) (n (C)))))))))))) (n (C)))))
(181 (instantiate 4 ((v0 . (n (C)))(v1 . (C))(v2 . (n (+ (C) (+ (C) (n (+ (C) (n (C)))))))))) ((= (+ (n (C)) (+ (C) (n (+ (C) (+ (C) (n (+ (C) (n (C))))))))) (+ (C) (+ (n (C)) (n (+ (C) (+ (C) (n (+ (C) (n (C))))))))))))
(182 (paramod 181 (1 1) 180 (1 1 1 2 1)) ((= (n (+ (C) (n (+ (C) (+ (n (C)) (n (+ (C) (+ (C) (n (+ (C) (n (C)))))))))))) (n (C)))))
(183 (instantiate 71 ((v0 . (n (+ (C) (n (C)))))(v1 . (C)))) ((= (n (+ (n (+ (C) (n (C)))) (n (+ (C) (+ (n (+ (C) (n (C)))) (n (+ (n (C)) (n (+ (C) (n (C))))))))))) (n (+ (n (C)) (n (+ (C) (n (C)))))))))
(184 (paramod 178 (1 1) 183 (1 1 1 2 1 2 2)) ((= (n (+ (n (+ (C) (n (C)))) (n (+ (C) (+ (n (+ (C) (n (C)))) (C)))))) (n (+ (n (C)) (n (+ (C) (n (C)))))))))
(185 (instantiate 2 ((v0 . (n (+ (C) (n (C)))))(v1 . (C)))) ((= (+ (n (+ (C) (n (C)))) (C)) (+ (C) (n (+ (C) (n (C))))))))
(186 (paramod 185 (1 1) 184 (1 1 1 2 1 2)) ((= (n (+ (n (+ (C) (n (C)))) (n (+ (C) (+ (C) (n (+ (C) (n (C))))))))) (n (+ (n (C)) (n (+ (C) (n (C)))))))))
(187 (paramod 178 (1 1) 186 (1 2)) ((= (n (+ (n (+ (C) (n (C)))) (n (+ (C) (+ (C) (n (+ (C) (n (C))))))))) (C))))
(188 (instantiate 115 ((v0 . (n (C)))(v1 . (C))(v2 . (n (+ (C) (+ (C) (n (+ (C) (n (C)))))))))) ((= (n (+ (n (+ (n (C)) (+ (C) (n (+ (C) (+ (C) (n (+ (C) (n (C)))))))))) (n (+ (n (+ (C) (n (C)))) (n (+ (C) (+ (C) (n (+ (C) (n (C))))))))))) (n (+ (C) (+ (C) (n (+ (C) (n (C))))))))))
(189 (paramod 187 (1 1) 188 (1 1 1 2)) ((= (n (+ (n (+ (n (C)) (+ (C) (n (+ (C) (+ (C) (n (+ (C) (n (C)))))))))) (C))) (n (+ (C) (+ (C) (n (+ (C) (n (C))))))))))
(190 (instantiate 4 ((v0 . (n (C)))(v1 . (C))(v2 . (n (+ (C) (+ (C) (n (+ (C) (n (C)))))))))) ((= (+ (n (C)) (+ (C) (n (+ (C) (+ (C) (n (+ (C) (n (C))))))))) (+ (C) (+ (n (C)) (n (+ (C) (+ (C) (n (+ (C) (n (C))))))))))))
(191 (paramod 190 (1 1) 189 (1 1 1 1 1)) ((= (n (+ (n (+ (C) (+ (n (C)) (n (+ (C) (+ (C) (n (+ (C) (n (C)))))))))) (C))) (n (+ (C) (+ (C) (n (+ (C) (n (C))))))))))
(192 (instantiate 2 ((v0 . (n (+ (C) (+ (n (C)) (n (+ (C) (+ (C) (n (+ (C) (n (C)))))))))))(v1 . (C)))) ((= (+ (n (+ (C) (+ (n (C)) (n (+ (C) (+ (C) (n (+ (C) (n (C)))))))))) (C)) (+ (C) (n (+ (C) (+ (n (C)) (n (+ (C) (+ (C) (n (+ (C) (n (C))))))))))))))
(193 (paramod 192 (1 1) 191 (1 1 1)) ((= (n (+ (C) (n (+ (C) (+ (n (C)) (n (+ (C) (+ (C) (n (+ (C) (n (C)))))))))))) (n (+ (C) (+ (C) (n (+ (C) (n (C))))))))))
(194 (paramod 182 (1 1) 193 (1 1)) ((= (n (C)) (n (+ (C) (+ (C) (n (+ (C) (n (C))))))))))
(195 (flip 194 (1)) ((= (n (+ (C) (+ (C) (n (+ (C) (n (C))))))) (n (C)))))
(196 (instantiate 124 ((v0 . (n (+ (C) (n (C)))))(v1 . (C)))) ((= (n (+ (n (+ (D) (+ (n (+ (C) (n (C)))) (n (+ (C) (C)))))) (n (+ (C) (+ (C) (n (+ (C) (n (C))))))))) (+ (D) (n (+ (C) (n (C))))))))
(197 (paramod 195 (1 1) 196 (1 1 1 2)) ((= (n (+ (n (+ (D) (+ (n (+ (C) (n (C)))) (n (+ (C) (C)))))) (n (C)))) (+ (D) (n (+ (C) (n (C))))))))
(198 (instantiate 2 ((v0 . (n (+ (C) (n (C)))))(v1 . (n (+ (C) (C)))))) ((= (+ (n (+ (C) (n (C)))) (n (+ (C) (C)))) (+ (n (+ (C) (C))) (n (+ (C) (n (C))))))))
(199 (paramod 198 (1 1) 197 (1 1 1 1 1 2)) ((= (n (+ (n (+ (D) (+ (n (+ (C) (C))) (n (+ (C) (n (C))))))) (n (C)))) (+ (D) (n (+ (C) (n (C))))))))
(200 (instantiate 2 ((v0 . (n (+ (D) (+ (n (+ (C) (C))) (n (+ (C) (n (C))))))))(v1 . (n (C))))) ((= (+ (n (+ (D) (+ (n (+ (C) (C))) (n (+ (C) (n (C))))))) (n (C))) (+ (n (C)) (n (+ (D) (+ (n (+ (C) (C))) (n (+ (C) (n (C)))))))))))
(201 (paramod 200 (1 1) 199 (1 1 1)) ((= (n (+ (n (C)) (n (+ (D) (+ (n (+ (C) (C))) (n (+ (C) (n (C))))))))) (+ (D) (n (+ (C) (n (C))))))))
(202 (instantiate 129 ((v0 . (C)))) ((= (n (+ (n (C)) (n (+ (D) (+ (n (+ (C) (C))) (n (+ (C) (n (C))))))))) (D))))
(203 (paramod 202 (1 1) 201 (1 1)) ((= (D) (+ (D) (n (+ (C) (n (C))))))))
(204 (flip 203 (1)) ((= (+ (D) (n (+ (C) (n (C))))) (D))))
(205 (instantiate 111 ((v0 . (n (C)))(v1 . v65))) ((= (n (+ (n (+ (n (+ (D) (n (+ (C) (n (C)))))) (+ (n (+ (n (C)) (C))) v65))) (n (+ v65 (D))))) v65)))
(206 (paramod 204 (1 1) 205 (1 1 1 1 1 1 1)) ((= (n (+ (n (+ (n (D)) (+ (n (+ (n (C)) (C))) v65))) (n (+ v65 (D))))) v65)))
(207 (instantiate 2 ((v0 . (n (C)))(v1 . (C)))) ((= (+ (n (C)) (C)) (+ (C) (n (C))))))
(208 (paramod 207 (1 1) 206 (1 1 1 1 1 2 1 1)) ((= (n (+ (n (+ (n (D)) (+ (n (+ (C) (n (C)))) v65))) (n (+ v65 (D))))) v65)))
(209 (instantiate 208 ((v65 . v0))) ((= (n (+ (n (+ (n (D)) (+ (n (+ (C) (n (C)))) v0))) (n (+ v0 (D))))) v0)))
(210 (instantiate 151 ((v0 . (n (+ (C) (n (C)))))(v1 . (D))(v2 . v66))) ((= (n (+ (n (+ (n (+ (C) (n (C)))) (+ (n (D)) v66))) (n (+ v66 (+ (D) (n (+ (C) (n (C))))))))) (+ v66 (n (+ (C) (n (C))))))))
(211 (paramod 204 (1 1) 210 (1 1 1 2 1 2)) ((= (n (+ (n (+ (n (+ (C) (n (C)))) (+ (n (D)) v66))) (n (+ v66 (D))))) (+ v66 (n (+ (C) (n (C))))))))
(212 (instantiate 4 ((v0 . (n (+ (C) (n (C)))))(v1 . (n (D)))(v2 . v66))) ((= (+ (n (+ (C) (n (C)))) (+ (n (D)) v66)) (+ (n (D)) (+ (n (+ (C) (n (C)))) v66)))))
(213 (paramod 212 (1 1) 211 (1 1 1 1 1)) ((= (n (+ (n (+ (n (D)) (+ (n (+ (C) (n (C)))) v66))) (n (+ v66 (D))))) (+ v66 (n (+ (C) (n (C))))))))
(214 (instantiate 209 ((v0 . v66))) ((= (n (+ (n (+ (n (D)) (+ (n (+ (C) (n (C)))) v66))) (n (+ v66 (D))))) v66)))
(215 (paramod 214 (1 1) 213 (1 1)) ((= v66 (+ v66 (n (+ (C) (n (C))))))))
(216 (flip 215 (1)) ((= (+ v66 (n (+ (C) (n (C))))) v66)))
(217 (instantiate 216 ((v66 . v0))) ((= (+ v0 (n (+ (C) (n (C))))) v0)))
(218 (instantiate 1 ((v0 . (n (+ (C) (n (C))))))) ((not (= (+ (n (+ (C) (n (C)))) (n (+ (C) (n (C))))) (n (+ (C) (n (C))))))))
(219 (instantiate 217 ((v0 . (n (+ (C) (n (C))))))) ((= (+ (n (+ (C) (n (C)))) (n (+ (C) (n (C))))) (n (+ (C) (n (C)))))))
(220 (resolve 218 (1) 219 (1)) ())
)