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