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