;; ----- Otter 3.0.4c, May 1996 ----- ;; The job was started by mccune on cosmo.mcs.anl.gov, Thu Jan 23 15:36:28 1997 ;; ;;;; x=x. ;;;; x+y=y+x. ;;;; (x+y)+z=x+y+z. ;;;; x+y!=x. ;;;; n(n(n(x)+y)+n(x+y))=y. ;;;; (x+y)+z=x+y+z. ;; ;; ----> UNIT CONFLICT at 24.80 sec ----> 3039 [binary,3038.1,51.1] $F. ;; ( (1 (input) ((= (+ v0 v1) (+ v1 v0)))) (2 (input) ((= (+ (+ v0 v1) v2) (+ v0 (+ v1 v2))))) (3 (input) ((not (= (+ v0 v1) v0)))) (4 (input) ((= (n (+ (n (+ (n v0) v1)) (n (+ v0 v1)))) v1))) (5 (input) ((= (+ (+ v0 v1) v2) (+ v0 (+ v1 v2))))) (6 (instantiate 1 ((v0 . v64)(v1 . v65))) ((= (+ v64 v65) (+ v65 v64)))) (7 (instantiate 2 ((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 5 ((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 2 ((v2 . v65))) ((= (+ (+ v0 v1) v65) (+ v0 (+ v1 v65))))) (13 (instantiate 1 ((v0 . (+ v0 v1))(v1 . v65))) ((= (+ (+ v0 v1) v65) (+ v65 (+ v0 v1))))) (14 (paramod 12 (1 1) 13 (1 1)) ((= (+ v0 (+ v1 v65)) (+ v65 (+ v0 v1))))) (15 (instantiate 14 ((v65 . v2))) ((= (+ v0 (+ v1 v2)) (+ v2 (+ v0 v1))))) (16 (instantiate 1 ((v0 . v64)(v1 . v65))) ((= (+ v64 v65) (+ v65 v64)))) (17 (instantiate 3 ((v0 . v64)(v1 . v65))) ((not (= (+ v64 v65) v64)))) (18 (paramod 16 (1 1) 17 (1 1 1)) ((not (= (+ v65 v64) v64)))) (19 (instantiate 18 ((v64 . v1)(v65 . v0))) ((not (= (+ v0 v1) v1)))) (20 (instantiate 1 ((v0 . (n v64))(v1 . v65))) ((= (+ (n v64) v65) (+ v65 (n v64))))) (21 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (n (+ (n (+ (n v64) v65)) (n (+ v64 v65)))) v65))) (22 (paramod 20 (1 1) 21 (1 1 1 1 1)) ((= (n (+ (n (+ v65 (n v64))) (n (+ v64 v65)))) v65))) (23 (instantiate 22 ((v64 . v1)(v65 . v0))) ((= (n (+ (n (+ v0 (n v1))) (n (+ v1 v0)))) v0))) (24 (instantiate 2 ((v2 . v65))) ((= (+ (+ v0 v1) v65) (+ v0 (+ v1 v65))))) (25 (instantiate 4 ((v0 . (+ v0 v1))(v1 . v65))) ((= (n (+ (n (+ (n (+ v0 v1)) v65)) (n (+ (+ v0 v1) v65)))) v65))) (26 (paramod 24 (1 1) 25 (1 1 1 2 1)) ((= (n (+ (n (+ (n (+ v0 v1)) v65)) (n (+ v0 (+ v1 v65))))) v65))) (27 (instantiate 26 ((v65 . v2))) ((= (n (+ (n (+ (n (+ v0 v1)) v2)) (n (+ v0 (+ v1 v2))))) v2))) (28 (instantiate 1 ((v0 . v64)(v1 . v65))) ((= (+ v64 v65) (+ v65 v64)))) (29 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (n (+ (n (+ (n v64) v65)) (n (+ v64 v65)))) v65))) (30 (paramod 28 (1 1) 29 (1 1 1 2 1)) ((= (n (+ (n (+ (n v64) v65)) (n (+ v65 v64)))) v65))) (31 (instantiate 30 ((v64 . v0)(v65 . v1))) ((= (n (+ (n (+ (n v0) v1)) (n (+ v1 v0)))) v1))) (32 (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)))))) (33 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (n (+ (n (+ (n v64) v65)) (n (+ v64 v65)))) v65))) (34 (paramod 32 (1 1) 33 (1 1 1)) ((= (n (+ (n (+ v64 v65)) (n (+ (n v64) v65)))) v65))) (35 (instantiate 34 ((v64 . v0)(v65 . v1))) ((= (n (+ (n (+ v0 v1)) (n (+ (n v0) v1)))) v1))) (36 (instantiate 11 ((v0 . (n v64)))) ((= (+ (n v64) (+ v1 v2)) (+ v1 (+ (n v64) v2))))) (37 (instantiate 4 ((v0 . v64)(v1 . (+ v1 v2)))) ((= (n (+ (n (+ (n v64) (+ v1 v2))) (n (+ v64 (+ v1 v2))))) (+ v1 v2)))) (38 (paramod 36 (1 1) 37 (1 1 1 1 1)) ((= (n (+ (n (+ v1 (+ (n v64) v2))) (n (+ v64 (+ v1 v2))))) (+ v1 v2)))) (39 (instantiate 38 ((v1 . v0)(v64 . v1))) ((= (n (+ (n (+ v0 (+ (n v1) v2))) (n (+ v1 (+ v0 v2))))) (+ v0 v2)))) (40 (instantiate 2 ((v2 . v66))) ((= (+ (+ v0 v1) v66) (+ v0 (+ v1 v66))))) (41 (instantiate 15 ((v0 . v64)(v1 . (+ v0 v1))(v2 . v66))) ((= (+ v64 (+ (+ v0 v1) v66)) (+ v66 (+ v64 (+ v0 v1)))))) (42 (paramod 40 (1 1) 41 (1 1 2)) ((= (+ v64 (+ v0 (+ v1 v66))) (+ v66 (+ v64 (+ v0 v1)))))) (43 (instantiate 42 ((v0 . v1)(v1 . v2)(v64 . v0)(v66 . v3))) ((= (+ v0 (+ v1 (+ v2 v3))) (+ v3 (+ v0 (+ v1 v2)))))) (44 (instantiate 2 ((v2 . v65))) ((= (+ (+ v0 v1) v65) (+ v0 (+ v1 v65))))) (45 (instantiate 27 ((v0 . (+ v0 v1))(v1 . v65)(v2 . v66))) ((= (n (+ (n (+ (n (+ (+ v0 v1) v65)) v66)) (n (+ (+ v0 v1) (+ v65 v66))))) v66))) (46 (paramod 44 (1 1) 45 (1 1 1 1 1 1 1)) ((= (n (+ (n (+ (n (+ v0 (+ v1 v65))) v66)) (n (+ (+ v0 v1) (+ v65 v66))))) v66))) (47 (instantiate 5 ((v0 . v0)(v1 . v1)(v2 . (+ v65 v66)))) ((= (+ (+ v0 v1) (+ v65 v66)) (+ v0 (+ v1 (+ v65 v66)))))) (48 (paramod 47 (1 1) 46 (1 1 1 2 1)) ((= (n (+ (n (+ (n (+ v0 (+ v1 v65))) v66)) (n (+ v0 (+ v1 (+ v65 v66)))))) v66))) (49 (instantiate 48 ((v65 . v2)(v66 . v3))) ((= (n (+ (n (+ (n (+ v0 (+ v1 v2))) v3)) (n (+ v0 (+ v1 (+ v2 v3)))))) v3))) (50 (instantiate 31 ((v0 . (+ (n (+ (n v0) v1)) (n (+ v0 v1))))(v1 . v65))) ((= (n (+ (n (+ (n (+ (n (+ (n v0) v1)) (n (+ v0 v1)))) v65)) (n (+ v65 (+ (n (+ (n v0) v1)) (n (+ v0 v1))))))) v65))) (51 (paramod 4 (1 1) 50 (1 1 1 1 1 1)) ((= (n (+ (n (+ v1 v65)) (n (+ v65 (+ (n (+ (n v0) v1)) (n (+ v0 v1))))))) v65))) (52 (instantiate 51 ((v0 . v2)(v1 . v0)(v65 . v1))) ((= (n (+ (n (+ v0 v1)) (n (+ v1 (+ (n (+ (n v2) v0)) (n (+ v2 v0))))))) v1))) (53 (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)))))) (54 (instantiate 31 ((v0 . v64)(v1 . v65))) ((= (n (+ (n (+ (n v64) v65)) (n (+ v65 v64)))) v65))) (55 (paramod 53 (1 1) 54 (1 1 1)) ((= (n (+ (n (+ v65 v64)) (n (+ (n v64) v65)))) v65))) (56 (instantiate 55 ((v64 . v1)(v65 . v0))) ((= (n (+ (n (+ v0 v1)) (n (+ (n v1) v0)))) v0))) (57 (instantiate 2 ((v2 . v66))) ((= (+ (+ v0 v1) v66) (+ v0 (+ v1 v66))))) (58 (instantiate 49 ((v0 . v64)(v1 . (+ v0 v1))(v2 . v66)(v3 . v67))) ((= (n (+ (n (+ (n (+ v64 (+ (+ v0 v1) v66))) v67)) (n (+ v64 (+ (+ v0 v1) (+ v66 v67)))))) v67))) (59 (paramod 57 (1 1) 58 (1 1 1 1 1 1 1 2)) ((= (n (+ (n (+ (n (+ v64 (+ v0 (+ v1 v66)))) v67)) (n (+ v64 (+ (+ v0 v1) (+ v66 v67)))))) v67))) (60 (instantiate 5 ((v0 . v0)(v1 . v1)(v2 . (+ v66 v67)))) ((= (+ (+ v0 v1) (+ v66 v67)) (+ v0 (+ v1 (+ v66 v67)))))) (61 (paramod 60 (1 1) 59 (1 1 1 2 1 2)) ((= (n (+ (n (+ (n (+ v64 (+ v0 (+ v1 v66)))) v67)) (n (+ v64 (+ v0 (+ v1 (+ v66 v67))))))) v67))) (62 (instantiate 61 ((v0 . v1)(v1 . v2)(v64 . v0)(v66 . v3)(v67 . v4))) ((= (n (+ (n (+ (n (+ v0 (+ v1 (+ v2 v3)))) v4)) (n (+ v0 (+ v1 (+ v2 (+ v3 v4))))))) v4))) (63 (instantiate 56 ((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))))) (64 (paramod 56 (1 1) 63 (1 1 1 2)) ((= (n (+ (n (+ (n (+ (n v1) v0)) (+ v0 v1))) v0)) (n (+ (n v1) v0))))) (65 (instantiate 64 ((v0 . v1)(v1 . v0))) ((= (n (+ (n (+ (n (+ (n v0) v1)) (+ v1 v0))) v1)) (n (+ (n v0) v1))))) (66 (instantiate 56 ((v0 . (n (+ v1 (+ v0 v2))))(v1 . (+ v0 (+ (n v1) v2))))) ((= (n (+ (n (+ (n (+ v1 (+ v0 v2))) (+ v0 (+ (n v1) v2)))) (n (+ (n (+ v0 (+ (n v1) v2))) (n (+ v1 (+ v0 v2))))))) (n (+ v1 (+ v0 v2)))))) (67 (paramod 39 (1 1) 66 (1 1 1 2)) ((= (n (+ (n (+ (n (+ v1 (+ v0 v2))) (+ v0 (+ (n v1) v2)))) (+ v0 v2))) (n (+ v1 (+ v0 v2)))))) (68 (instantiate 67 ((v0 . v1)(v1 . v0))) ((= (n (+ (n (+ (n (+ v0 (+ v1 v2))) (+ v1 (+ (n v0) v2)))) (+ v1 v2))) (n (+ v0 (+ v1 v2)))))) (69 (instantiate 56 ((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))))) (70 (paramod 35 (1 1) 69 (1 1 1 2)) ((= (n (+ (n (+ (n (+ (n v0) v1)) (+ v0 v1))) v1)) (n (+ (n v0) v1))))) (71 (instantiate 2 ((v2 . v67))) ((= (+ (+ v0 v1) v67) (+ v0 (+ v1 v67))))) (72 (instantiate 62 ((v0 . v64)(v1 . v65)(v2 . (+ v0 v1))(v3 . v67)(v4 . v68))) ((= (n (+ (n (+ (n (+ v64 (+ v65 (+ (+ v0 v1) v67)))) v68)) (n (+ v64 (+ v65 (+ (+ v0 v1) (+ v67 v68))))))) v68))) (73 (paramod 71 (1 1) 72 (1 1 1 1 1 1 1 2 2)) ((= (n (+ (n (+ (n (+ v64 (+ v65 (+ v0 (+ v1 v67))))) v68)) (n (+ v64 (+ v65 (+ (+ v0 v1) (+ v67 v68))))))) v68))) (74 (instantiate 5 ((v0 . v0)(v1 . v1)(v2 . (+ v67 v68)))) ((= (+ (+ v0 v1) (+ v67 v68)) (+ v0 (+ v1 (+ v67 v68)))))) (75 (paramod 74 (1 1) 73 (1 1 1 2 1 2 2)) ((= (n (+ (n (+ (n (+ v64 (+ v65 (+ v0 (+ v1 v67))))) v68)) (n (+ v64 (+ v65 (+ v0 (+ v1 (+ v67 v68)))))))) v68))) (76 (instantiate 75 ((v0 . v2)(v1 . v3)(v64 . v0)(v65 . v1)(v67 . v4)(v68 . v5))) ((= (n (+ (n (+ (n (+ v0 (+ v1 (+ v2 (+ v3 v4))))) v5)) (n (+ v0 (+ v1 (+ v2 (+ v3 (+ v4 v5)))))))) v5))) (77 (instantiate 65 ((v1 . v64))) ((= (n (+ (n (+ (n (+ (n v0) v64)) (+ v64 v0))) v64)) (n (+ (n v0) v64))))) (78 (instantiate 52 ((v0 . v64)(v1 . v65)(v2 . (+ (n (+ (n v0) v64)) (+ v64 v0))))) ((= (n (+ (n (+ v64 v65)) (n (+ v65 (+ (n (+ (n (+ (n (+ (n v0) v64)) (+ v64 v0))) v64)) (n (+ (+ (n (+ (n v0) v64)) (+ v64 v0)) v64))))))) v65))) (79 (paramod 77 (1 1) 78 (1 1 1 2 1 2 1)) ((= (n (+ (n (+ v64 v65)) (n (+ v65 (+ (n (+ (n v0) v64)) (n (+ (+ (n (+ (n v0) v64)) (+ v64 v0)) v64))))))) v65))) (80 (instantiate 5 ((v0 . (n (+ (n v0) v64)))(v1 . (+ v64 v0))(v2 . v64))) ((= (+ (+ (n (+ (n v0) v64)) (+ v64 v0)) v64) (+ (n (+ (n v0) v64)) (+ (+ v64 v0) v64))))) (81 (paramod 80 (1 1) 79 (1 1 1 2 1 2 2 1)) ((= (n (+ (n (+ v64 v65)) (n (+ v65 (+ (n (+ (n v0) v64)) (n (+ (n (+ (n v0) v64)) (+ (+ v64 v0) v64)))))))) v65))) (82 (instantiate 5 ((v0 . v64)(v1 . v0)(v2 . v64))) ((= (+ (+ v64 v0) v64) (+ v64 (+ v0 v64))))) (83 (paramod 82 (1 1) 81 (1 1 1 2 1 2 2 1 2)) ((= (n (+ (n (+ v64 v65)) (n (+ v65 (+ (n (+ (n v0) v64)) (n (+ (n (+ (n v0) v64)) (+ v64 (+ v0 v64))))))))) v65))) (84 (instantiate 83 ((v0 . v2)(v64 . v0)(v65 . v1))) ((= (n (+ (n (+ v0 v1)) (n (+ v1 (+ (n (+ (n v2) v0)) (n (+ (n (+ (n v2) v0)) (+ v0 (+ v2 v0))))))))) v1))) (85 (instantiate 11 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (+ v64 (+ v65 v66)) (+ v65 (+ v64 v66))))) (86 (instantiate 68 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (n (+ (n (+ (n (+ v64 (+ v65 v66))) (+ v65 (+ (n v64) v66)))) (+ v65 v66))) (n (+ v64 (+ v65 v66)))))) (87 (paramod 85 (1 1) 86 (1 1 1 1 1 1 1)) ((= (n (+ (n (+ (n (+ v65 (+ v64 v66))) (+ v65 (+ (n v64) v66)))) (+ v65 v66))) (n (+ v64 (+ v65 v66)))))) (88 (instantiate 87 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (n (+ (n (+ (n (+ v0 (+ v1 v2))) (+ v0 (+ (n v1) v2)))) (+ v0 v2))) (n (+ v1 (+ v0 v2)))))) (89 (instantiate 2 ((v2 . v65))) ((= (+ (+ v0 v1) v65) (+ v0 (+ v1 v65))))) (90 (instantiate 70 ((v0 . (+ v0 v1))(v1 . v65))) ((= (n (+ (n (+ (n (+ (n (+ v0 v1)) v65)) (+ (+ v0 v1) v65))) v65)) (n (+ (n (+ v0 v1)) v65))))) (91 (paramod 89 (1 1) 90 (1 1 1 1 1 2)) ((= (n (+ (n (+ (n (+ (n (+ v0 v1)) v65)) (+ v0 (+ v1 v65)))) v65)) (n (+ (n (+ v0 v1)) v65))))) (92 (instantiate 91 ((v65 . v2))) ((= (n (+ (n (+ (n (+ (n (+ v0 v1)) v2)) (+ v0 (+ v1 v2)))) v2)) (n (+ (n (+ v0 v1)) v2))))) (93 (instantiate 70 ((v1 . v65))) ((= (n (+ (n (+ (n (+ (n v0) v65)) (+ v0 v65))) v65)) (n (+ (n v0) v65))))) (94 (instantiate 35 ((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))) (95 (paramod 93 (1 1) 94 (1 1 1 2)) ((= (n (+ (n (+ (+ (n (+ (n v0) v65)) (+ v0 v65)) v65)) (n (+ (n v0) v65)))) v65))) (96 (instantiate 5 ((v0 . (n (+ (n v0) v65)))(v1 . (+ v0 v65))(v2 . v65))) ((= (+ (+ (n (+ (n v0) v65)) (+ v0 v65)) v65) (+ (n (+ (n v0) v65)) (+ (+ v0 v65) v65))))) (97 (paramod 96 (1 1) 95 (1 1 1 1 1)) ((= (n (+ (n (+ (n (+ (n v0) v65)) (+ (+ v0 v65) v65))) (n (+ (n v0) v65)))) v65))) (98 (instantiate 5 ((v0 . v0)(v1 . v65)(v2 . v65))) ((= (+ (+ v0 v65) v65) (+ v0 (+ v65 v65))))) (99 (paramod 98 (1 1) 97 (1 1 1 1 1 2)) ((= (n (+ (n (+ (n (+ (n v0) v65)) (+ v0 (+ v65 v65)))) (n (+ (n v0) v65)))) v65))) (100 (instantiate 99 ((v65 . v1))) ((= (n (+ (n (+ (n (+ (n v0) v1)) (+ v0 (+ v1 v1)))) (n (+ (n v0) v1)))) v1))) (101 (instantiate 1 ((v0 . v64)(v1 . v65))) ((= (+ v64 v65) (+ v65 v64)))) (102 (instantiate 84 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (n (+ (n (+ v64 v65)) (n (+ v65 (+ (n (+ (n v66) v64)) (n (+ (n (+ (n v66) v64)) (+ v64 (+ v66 v64))))))))) v65))) (103 (paramod 101 (1 1) 102 (1 1 1 1 1)) ((= (n (+ (n (+ v65 v64)) (n (+ v65 (+ (n (+ (n v66) v64)) (n (+ (n (+ (n v66) v64)) (+ v64 (+ v66 v64))))))))) v65))) (104 (instantiate 103 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (n (+ (n (+ v0 v1)) (n (+ v0 (+ (n (+ (n v2) v1)) (n (+ (n (+ (n v2) v1)) (+ v1 (+ v2 v1))))))))) v0))) (105 (instantiate 1 ((v0 . v64)(v1 . v66))) ((= (+ v64 v66) (+ v66 v64)))) (106 (instantiate 88 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (n (+ (n (+ (n (+ v64 (+ v65 v66))) (+ v64 (+ (n v65) v66)))) (+ v64 v66))) (n (+ v65 (+ v64 v66)))))) (107 (paramod 105 (1 1) 106 (1 1 1 2)) ((= (n (+ (n (+ (n (+ v64 (+ v65 v66))) (+ v64 (+ (n v65) v66)))) (+ v66 v64))) (n (+ v65 (+ v64 v66)))))) (108 (instantiate 107 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (n (+ (n (+ (n (+ v0 (+ v1 v2))) (+ v0 (+ (n v1) v2)))) (+ v2 v0))) (n (+ v1 (+ v0 v2)))))) (109 (instantiate 2 ((v2 . v65))) ((= (+ (+ v0 v1) v65) (+ v0 (+ v1 v65))))) (110 (instantiate 92 ((v0 . (+ v0 v1))(v1 . v65)(v2 . v66))) ((= (n (+ (n (+ (n (+ (n (+ (+ v0 v1) v65)) v66)) (+ (+ v0 v1) (+ v65 v66)))) v66)) (n (+ (n (+ (+ v0 v1) v65)) v66))))) (111 (paramod 109 (1 1) 110 (1 1 1 1 1 1 1 1 1)) ((= (n (+ (n (+ (n (+ (n (+ v0 (+ v1 v65))) v66)) (+ (+ v0 v1) (+ v65 v66)))) v66)) (n (+ (n (+ (+ v0 v1) v65)) v66))))) (112 (instantiate 5 ((v0 . v0)(v1 . v1)(v2 . (+ v65 v66)))) ((= (+ (+ v0 v1) (+ v65 v66)) (+ v0 (+ v1 (+ v65 v66)))))) (113 (paramod 112 (1 1) 111 (1 1 1 1 1 2)) ((= (n (+ (n (+ (n (+ (n (+ v0 (+ v1 v65))) v66)) (+ v0 (+ v1 (+ v65 v66))))) v66)) (n (+ (n (+ (+ v0 v1) v65)) v66))))) (114 (instantiate 5 ((v0 . v0)(v1 . v1)(v2 . v65))) ((= (+ (+ v0 v1) v65) (+ v0 (+ v1 v65))))) (115 (paramod 114 (1 1) 113 (1 2 1 1 1)) ((= (n (+ (n (+ (n (+ (n (+ v0 (+ v1 v65))) v66)) (+ v0 (+ v1 (+ v65 v66))))) v66)) (n (+ (n (+ v0 (+ v1 v65))) v66))))) (116 (instantiate 115 ((v65 . v2)(v66 . v3))) ((= (n (+ (n (+ (n (+ (n (+ v0 (+ v1 v2))) v3)) (+ v0 (+ v1 (+ v2 v3))))) v3)) (n (+ (n (+ v0 (+ v1 v2))) v3))))) (117 (instantiate 35 ((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))) (118 (paramod 100 (1 1) 117 (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))) (119 (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))))) (120 (paramod 119 (1 1) 118 (1 1 1 1 1)) ((= (n (+ (n (+ (n (+ (n (+ (n v0) v1)) (+ v0 (+ v1 v1)))) (+ (n (+ (n v0) v1)) v65))) (n (+ v1 v65)))) v65))) (121 (instantiate 120 ((v65 . v2))) ((= (n (+ (n (+ (n (+ (n (+ (n v0) v1)) (+ v0 (+ v1 v1)))) (+ (n (+ (n v0) v1)) v2))) (n (+ v1 v2)))) v2))) (122 (instantiate 1 ((v0 . v66)(v1 . v65))) ((= (+ v66 v65) (+ v65 v66)))) (123 (instantiate 104 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (n (+ (n (+ v64 v65)) (n (+ v64 (+ (n (+ (n v66) v65)) (n (+ (n (+ (n v66) v65)) (+ v65 (+ v66 v65))))))))) v64))) (124 (paramod 122 (1 1) 123 (1 1 1 2 1 2 2 1 2 2)) ((= (n (+ (n (+ v64 v65)) (n (+ v64 (+ (n (+ (n v66) v65)) (n (+ (n (+ (n v66) v65)) (+ v65 (+ v65 v66))))))))) v64))) (125 (instantiate 124 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (n (+ (n (+ v0 v1)) (n (+ v0 (+ (n (+ (n v2) v1)) (n (+ (n (+ (n v2) v1)) (+ v1 (+ v1 v2))))))))) v0))) (126 (instantiate 35 ((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))))) (127 (paramod 121 (1 1) 126 (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))))) (128 (instantiate 5 ((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))))))) (129 (paramod 128 (1 1) 127 (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))))) (130 (instantiate 5 ((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))))))) (131 (paramod 130 (1 1) 129 (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))))) (132 (instantiate 1 ((v0 . v66)(v1 . (n (+ v65 v66))))) ((= (+ v66 (n (+ v65 v66))) (+ (n (+ v65 v66)) v66)))) (133 (instantiate 131 ((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))))) (134 (paramod 132 (1 1) 133 (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))))) (135 (instantiate 134 ((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))))) (136 (instantiate 35 ((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))) (137 (paramod 135 (1 1) 136 (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))) (138 (instantiate 5 ((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))))) (139 (paramod 138 (1 1) 137 (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))) (140 (instantiate 139 ((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))) (141 (instantiate 108 ((v0 . (n (+ (n (+ v65 (+ v65 v65))) v65)))(v1 . (+ v65 (+ v65 v65)))(v2 . (+ v65 v65)))) ((= (n (+ (n (+ (n (+ (n (+ (n (+ v65 (+ v65 v65))) v65)) (+ (+ v65 (+ v65 v65)) (+ v65 v65)))) (+ (n (+ (n (+ v65 (+ v65 v65))) v65)) (+ (n (+ v65 (+ v65 v65))) (+ v65 v65))))) (+ (+ v65 v65) (n (+ (n (+ v65 (+ v65 v65))) v65))))) (n (+ (+ v65 (+ v65 v65)) (+ (n (+ (n (+ v65 (+ v65 v65))) v65)) (+ v65 v65))))))) (142 (instantiate 140 ((v0 . (+ v65 (+ v65 v65)))(v1 . v65)(v2 . (+ v65 v65))(v3 . (n (+ (n (+ v65 (+ v65 v65))) v65))))) ((= (n (+ (n (+ (n (+ (n (+ (n (+ (n (+ v65 (+ v65 v65))) v65)) (+ (+ v65 (+ v65 v65)) (+ v65 v65)))) (+ (n (+ (n (+ v65 (+ v65 v65))) v65)) (+ (n (+ v65 (+ v65 v65))) (+ v65 v65))))) (+ (+ v65 v65) (n (+ (n (+ v65 (+ v65 v65))) v65))))) (n (+ (n (+ v65 (+ v65 v65))) (n (+ (n (+ v65 (+ v65 v65))) v65)))))) (n (+ (n (+ v65 (+ v65 v65))) v65))))) (143 (paramod 141 (1 1) 142 (1 1 1 1)) ((= (n (+ (n (+ (+ v65 (+ v65 v65)) (+ (n (+ (n (+ v65 (+ v65 v65))) v65)) (+ v65 v65)))) (n (+ (n (+ v65 (+ v65 v65))) (n (+ (n (+ v65 (+ v65 v65))) v65)))))) (n (+ (n (+ v65 (+ v65 v65))) v65))))) (144 (instantiate 5 ((v0 . v65)(v1 . (+ v65 v65))(v2 . (+ (n (+ (n (+ v65 (+ v65 v65))) v65)) (+ v65 v65))))) ((= (+ (+ v65 (+ v65 v65)) (+ (n (+ (n (+ v65 (+ v65 v65))) v65)) (+ v65 v65))) (+ v65 (+ (+ v65 v65) (+ (n (+ (n (+ v65 (+ v65 v65))) v65)) (+ v65 v65))))))) (145 (paramod 144 (1 1) 143 (1 1 1 1 1)) ((= (n (+ (n (+ v65 (+ (+ v65 v65) (+ (n (+ (n (+ v65 (+ v65 v65))) v65)) (+ v65 v65))))) (n (+ (n (+ v65 (+ v65 v65))) (n (+ (n (+ v65 (+ v65 v65))) v65)))))) (n (+ (n (+ v65 (+ v65 v65))) v65))))) (146 (instantiate 5 ((v0 . v65)(v1 . v65)(v2 . (+ (n (+ (n (+ v65 (+ v65 v65))) v65)) (+ v65 v65))))) ((= (+ (+ v65 v65) (+ (n (+ (n (+ v65 (+ v65 v65))) v65)) (+ v65 v65))) (+ v65 (+ v65 (+ (n (+ (n (+ v65 (+ v65 v65))) v65)) (+ v65 v65))))))) (147 (paramod 146 (1 1) 145 (1 1 1 1 1 2)) ((= (n (+ (n (+ v65 (+ v65 (+ v65 (+ (n (+ (n (+ v65 (+ v65 v65))) v65)) (+ v65 v65)))))) (n (+ (n (+ v65 (+ v65 v65))) (n (+ (n (+ v65 (+ v65 v65))) v65)))))) (n (+ (n (+ v65 (+ v65 v65))) v65))))) (148 (instantiate 147 ((v65 . v0))) ((= (n (+ (n (+ v0 (+ v0 (+ v0 (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0)))))) (n (+ (n (+ v0 (+ v0 v0))) (n (+ (n (+ v0 (+ v0 v0))) v0)))))) (n (+ (n (+ v0 (+ v0 v0))) v0))))) (149 (instantiate 23 ((v0 . (n (+ v0 (+ v0 (+ v0 (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0)))))))(v1 . (+ (n (+ v0 (+ v0 v0))) (n (+ (n (+ v0 (+ v0 v0))) v0)))))) ((= (n (+ (n (+ (n (+ v0 (+ v0 (+ v0 (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0)))))) (n (+ (n (+ v0 (+ v0 v0))) (n (+ (n (+ v0 (+ v0 v0))) v0)))))) (n (+ (+ (n (+ v0 (+ v0 v0))) (n (+ (n (+ v0 (+ v0 v0))) v0))) (n (+ v0 (+ v0 (+ v0 (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0)))))))))) (n (+ v0 (+ v0 (+ v0 (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0))))))))) (150 (paramod 148 (1 1) 149 (1 1 1 1)) ((= (n (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (n (+ (+ (n (+ v0 (+ v0 v0))) (n (+ (n (+ v0 (+ v0 v0))) v0))) (n (+ v0 (+ v0 (+ v0 (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0)))))))))) (n (+ v0 (+ v0 (+ v0 (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0))))))))) (151 (instantiate 5 ((v0 . (n (+ v0 (+ v0 v0))))(v1 . (n (+ (n (+ v0 (+ v0 v0))) v0)))(v2 . (n (+ v0 (+ v0 (+ v0 (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0))))))))) ((= (+ (+ (n (+ v0 (+ v0 v0))) (n (+ (n (+ v0 (+ v0 v0))) v0))) (n (+ v0 (+ v0 (+ v0 (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0))))))) (+ (n (+ v0 (+ v0 v0))) (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (n (+ v0 (+ v0 (+ v0 (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0))))))))))) (152 (paramod 151 (1 1) 150 (1 1 1 2 1)) ((= (n (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (n (+ (n (+ v0 (+ v0 v0))) (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (n (+ v0 (+ v0 (+ v0 (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0))))))))))) (n (+ v0 (+ v0 (+ v0 (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0))))))))) (153 (instantiate 43 ((v0 . v64)(v1 . v64)(v2 . v64)(v3 . (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64))))) ((= (+ v64 (+ v64 (+ v64 (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64))))) (+ (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64)) (+ v64 (+ v64 v64)))))) (154 (instantiate 152 ((v0 . v64))) ((= (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (n (+ (n (+ v64 (+ v64 v64))) (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (n (+ v64 (+ v64 (+ v64 (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64))))))))))) (n (+ v64 (+ v64 (+ v64 (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64))))))))) (155 (paramod 153 (1 1) 154 (1 1 1 2 1 2 2 1)) ((= (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (n (+ (n (+ v64 (+ v64 v64))) (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (n (+ (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64)) (+ v64 (+ v64 v64))))))))) (n (+ v64 (+ v64 (+ v64 (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64))))))))) (156 (instantiate 5 ((v0 . (n (+ (n (+ v64 (+ v64 v64))) v64)))(v1 . (+ v64 v64))(v2 . (+ v64 (+ v64 v64))))) ((= (+ (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64)) (+ v64 (+ v64 v64))) (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ (+ v64 v64) (+ v64 (+ v64 v64))))))) (157 (paramod 156 (1 1) 155 (1 1 1 2 1 2 2 1)) ((= (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (n (+ (n (+ v64 (+ v64 v64))) (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ (+ v64 v64) (+ v64 (+ v64 v64)))))))))) (n (+ v64 (+ v64 (+ v64 (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64))))))))) (158 (instantiate 5 ((v0 . v64)(v1 . v64)(v2 . (+ v64 (+ v64 v64))))) ((= (+ (+ v64 v64) (+ v64 (+ v64 v64))) (+ v64 (+ v64 (+ v64 (+ v64 v64))))))) (159 (paramod 158 (1 1) 157 (1 1 1 2 1 2 2 1 2)) ((= (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (n (+ (n (+ v64 (+ v64 v64))) (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 (+ v64 (+ v64 (+ v64 v64))))))))))) (n (+ v64 (+ v64 (+ v64 (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64))))))))) (160 (instantiate 159 ((v64 . v0))) ((= (n (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (n (+ (n (+ v0 (+ v0 v0))) (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (n (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 (+ v0 (+ v0 (+ v0 v0))))))))))) (n (+ v0 (+ v0 (+ v0 (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0))))))))) (161 (instantiate 125 ((v0 . (n (+ v64 (+ v64 v64))))(v1 . v64)(v2 . (+ v64 (+ v64 v64))))) ((= (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (n (+ (n (+ v64 (+ v64 v64))) (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 (+ v64 (+ v64 (+ v64 v64))))))))))) (n (+ v64 (+ v64 v64)))))) (162 (instantiate 160 ((v0 . v64))) ((= (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (n (+ (n (+ v64 (+ v64 v64))) (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 (+ v64 (+ v64 (+ v64 v64))))))))))) (n (+ v64 (+ v64 (+ v64 (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64))))))))) (163 (paramod 161 (1 1) 162 (1 1)) ((= (n (+ v64 (+ v64 v64))) (n (+ v64 (+ v64 (+ v64 (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64))))))))) (164 (flip 163 (1)) ((= (n (+ v64 (+ v64 (+ v64 (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64)))))) (n (+ v64 (+ v64 v64)))))) (165 (instantiate 164 ((v64 . v0))) ((= (n (+ v0 (+ v0 (+ v0 (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0)))))) (n (+ v0 (+ v0 v0)))))) (166 (instantiate 43 ((v0 . v64)(v1 . v64)(v2 . v64)(v3 . (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64))))) ((= (+ v64 (+ v64 (+ v64 (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64))))) (+ (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64)) (+ v64 (+ v64 v64)))))) (167 (instantiate 165 ((v0 . v64))) ((= (n (+ v64 (+ v64 (+ v64 (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64)))))) (n (+ v64 (+ v64 v64)))))) (168 (paramod 166 (1 1) 167 (1 1 1)) ((= (n (+ (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64)) (+ v64 (+ v64 v64)))) (n (+ v64 (+ v64 v64)))))) (169 (instantiate 5 ((v0 . (n (+ (n (+ v64 (+ v64 v64))) v64)))(v1 . (+ v64 v64))(v2 . (+ v64 (+ v64 v64))))) ((= (+ (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64)) (+ v64 (+ v64 v64))) (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ (+ v64 v64) (+ v64 (+ v64 v64))))))) (170 (paramod 169 (1 1) 168 (1 1 1)) ((= (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ (+ v64 v64) (+ v64 (+ v64 v64))))) (n (+ v64 (+ v64 v64)))))) (171 (instantiate 5 ((v0 . v64)(v1 . v64)(v2 . (+ v64 (+ v64 v64))))) ((= (+ (+ v64 v64) (+ v64 (+ v64 v64))) (+ v64 (+ v64 (+ v64 (+ v64 v64))))))) (172 (paramod 171 (1 1) 170 (1 1 1 2)) ((= (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 (+ v64 (+ v64 (+ v64 v64)))))) (n (+ v64 (+ v64 v64)))))) (173 (instantiate 172 ((v64 . v0))) ((= (n (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 (+ v0 (+ v0 (+ v0 v0)))))) (n (+ v0 (+ v0 v0)))))) (174 (instantiate 165 ((v0 . v66))) ((= (n (+ v66 (+ v66 (+ v66 (+ (n (+ (n (+ v66 (+ v66 v66))) v66)) (+ v66 v66)))))) (n (+ v66 (+ v66 v66)))))) (175 (instantiate 49 ((v0 . v66)(v1 . v66)(v2 . v66)(v3 . (+ (n (+ (n (+ v66 (+ v66 v66))) v66)) (+ v66 v66))))) ((= (n (+ (n (+ (n (+ v66 (+ v66 v66))) (+ (n (+ (n (+ v66 (+ v66 v66))) v66)) (+ v66 v66)))) (n (+ v66 (+ v66 (+ v66 (+ (n (+ (n (+ v66 (+ v66 v66))) v66)) (+ v66 v66)))))))) (+ (n (+ (n (+ v66 (+ v66 v66))) v66)) (+ v66 v66))))) (176 (paramod 174 (1 1) 175 (1 1 1 2)) ((= (n (+ (n (+ (n (+ v66 (+ v66 v66))) (+ (n (+ (n (+ v66 (+ v66 v66))) v66)) (+ v66 v66)))) (n (+ v66 (+ v66 v66))))) (+ (n (+ (n (+ v66 (+ v66 v66))) v66)) (+ v66 v66))))) (177 (instantiate 176 ((v66 . v0))) ((= (n (+ (n (+ (n (+ v0 (+ v0 v0))) (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0)))) (n (+ v0 (+ v0 v0))))) (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0))))) (178 (instantiate 173 ((v0 . v69))) ((= (n (+ (n (+ (n (+ v69 (+ v69 v69))) v69)) (+ v69 (+ v69 (+ v69 (+ v69 v69)))))) (n (+ v69 (+ v69 v69)))))) (179 (instantiate 76 ((v0 . (n (+ (n (+ v69 (+ v69 v69))) v69)))(v1 . v69)(v2 . v69)(v3 . v69)(v4 . v69)(v5 . v69))) ((= (n (+ (n (+ (n (+ (n (+ (n (+ v69 (+ v69 v69))) v69)) (+ v69 (+ v69 (+ v69 v69))))) v69)) (n (+ (n (+ (n (+ v69 (+ v69 v69))) v69)) (+ v69 (+ v69 (+ v69 (+ v69 v69)))))))) v69))) (180 (paramod 178 (1 1) 179 (1 1 1 2)) ((= (n (+ (n (+ (n (+ (n (+ (n (+ v69 (+ v69 v69))) v69)) (+ v69 (+ v69 (+ v69 v69))))) v69)) (n (+ v69 (+ v69 v69))))) v69))) (181 (instantiate 180 ((v69 . v0))) ((= (n (+ (n (+ (n (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 (+ v0 (+ v0 v0))))) v0)) (n (+ v0 (+ v0 v0))))) v0))) (182 (instantiate 116 ((v0 . v64)(v1 . v64)(v2 . v64)(v3 . v64))) ((= (n (+ (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 (+ v64 (+ v64 v64))))) v64)) (n (+ (n (+ v64 (+ v64 v64))) v64))))) (183 (instantiate 181 ((v0 . v64))) ((= (n (+ (n (+ (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 (+ v64 (+ v64 v64))))) v64)) (n (+ v64 (+ v64 v64))))) v64))) (184 (paramod 182 (1 1) 183 (1 1 1 1)) ((= (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (n (+ v64 (+ v64 v64))))) v64))) (185 (instantiate 184 ((v64 . v0))) ((= (n (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (n (+ v0 (+ v0 v0))))) v0))) (186 (instantiate 35 ((v0 . (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (n (+ v0 (+ v0 v0)))))(v1 . v65))) ((= (n (+ (n (+ (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (n (+ v0 (+ v0 v0)))) v65)) (n (+ (n (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (n (+ v0 (+ v0 v0))))) v65)))) v65))) (187 (paramod 185 (1 1) 186 (1 1 1 2 1 1)) ((= (n (+ (n (+ (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (n (+ v0 (+ v0 v0)))) v65)) (n (+ v0 v65)))) v65))) (188 (instantiate 5 ((v0 . (n (+ (n (+ v0 (+ v0 v0))) v0)))(v1 . (n (+ v0 (+ v0 v0))))(v2 . v65))) ((= (+ (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (n (+ v0 (+ v0 v0)))) v65) (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ (n (+ v0 (+ v0 v0))) v65))))) (189 (paramod 188 (1 1) 187 (1 1 1 1 1)) ((= (n (+ (n (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ (n (+ v0 (+ v0 v0))) v65))) (n (+ v0 v65)))) v65))) (190 (instantiate 189 ((v65 . v1))) ((= (n (+ (n (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ (n (+ v0 (+ v0 v0))) v1))) (n (+ v0 v1)))) v1))) (191 (instantiate 11 ((v0 . (n (+ (n (+ v64 (+ v64 v64))) v64)))(v1 . (n (+ v64 (+ v64 v64))))(v2 . v65))) ((= (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ (n (+ v64 (+ v64 v64))) v65)) (+ (n (+ v64 (+ v64 v64))) (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) v65))))) (192 (instantiate 190 ((v0 . v64)(v1 . v65))) ((= (n (+ (n (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ (n (+ v64 (+ v64 v64))) v65))) (n (+ v64 v65)))) v65))) (193 (paramod 191 (1 1) 192 (1 1 1 1 1)) ((= (n (+ (n (+ (n (+ v64 (+ v64 v64))) (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) v65))) (n (+ v64 v65)))) v65))) (194 (instantiate 193 ((v64 . v0)(v65 . v1))) ((= (n (+ (n (+ (n (+ v0 (+ v0 v0))) (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) v1))) (n (+ v0 v1)))) v1))) (195 (instantiate 177 ((v0 . v64))) ((= (n (+ (n (+ (n (+ v64 (+ v64 v64))) (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64)))) (n (+ v64 (+ v64 v64))))) (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64))))) (196 (instantiate 194 ((v0 . v64)(v1 . (+ v64 v64)))) ((= (n (+ (n (+ (n (+ v64 (+ v64 v64))) (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64)))) (n (+ v64 (+ v64 v64))))) (+ v64 v64)))) (197 (paramod 195 (1 1) 196 (1 1)) ((= (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64)) (+ v64 v64)))) (198 (instantiate 197 ((v64 . v0))) ((= (+ (n (+ (n (+ v0 (+ v0 v0))) v0)) (+ v0 v0)) (+ v0 v0)))) (199 (instantiate 19 ((v0 . (n (+ (n (+ v64 (+ v64 v64))) v64)))(v1 . (+ v64 v64)))) ((not (= (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64)) (+ v64 v64))))) (200 (instantiate 198 ((v0 . v64))) ((= (+ (n (+ (n (+ v64 (+ v64 v64))) v64)) (+ v64 v64)) (+ v64 v64)))) (201 (resolve 199 (1) 200 (1)) ()) )