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