;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 23:50:11 1995
;;
;;;; x=x.
;;;; x+y=y+x.
;;;; (x+y)+z=x+ (y+z).
;;;; n(n(x+y)+n(x+n(y)))=x.
;;;; c+c=c.
;;;; n(A+n(B))+n(n(A)+n(B))!=B.
;;
;; ----> UNIT CONFLICT at  21.99 sec ----> 2178 [binary,2177.1,1.1] $F.
;;
(
(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 (+ (A) (n (B)))) (n (+ (n (A)) (n (B))))) (B)))))
(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) (n (B)))))(v1 . (n (+ (n (A)) (n (B))))))) ((= (+ (n (+ (A) (n (B)))) (n (+ (n (A)) (n (B))))) (+ (n (+ (n (A)) (n (B)))) (n (+ (A) (n (B))))))))
(52 (paramod 51 (1 1) 6 (1 1 1)) ((not (= (+ (n (+ (n (A)) (n (B)))) (n (+ (A) (n (B))))) (B)))))
(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 55 ((v0 . (c)))) ((= (n (+ (n (+ (c) (+ (n (+ (c) (n (c)))) (n (c))))) (n (+ (c) (c))))) (c))))
(102 (paramod 5 (1 1) 101 (1 1 1 2 1)) ((= (n (+ (n (+ (c) (+ (n (+ (c) (n (c)))) (n (c))))) (n (c)))) (c))))
(103 (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)))
(104 (paramod 21 (1 1) 103 (1 1 1 1 1 2)) ((= (n (+ (n (+ v64 (c))) (n (+ (n (+ (c) (n (c)))) (+ v64 (n (c))))))) v64)))
(105 (instantiate 104 ((v64 . v0))) ((= (n (+ (n (+ v0 (c))) (n (+ (n (+ (c) (n (c)))) (+ v0 (n (c))))))) v0)))
(106 (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))))))))
(107 (paramod 100 (1 1) 106 (1 1 1 2)) ((= (n (+ (n (+ (c) (+ (n (+ (c) (n (c)))) (n (c))))) (n (c)))) (+ (c) (n (+ (c) (n (c))))))))
(108 (paramod 102 (1 1) 107 (1 1)) ((= (c) (+ (c) (n (+ (c) (n (c))))))))
(109 (flip 108 (1)) ((= (+ (c) (n (+ (c) (n (c))))) (c))))
(110 (instantiate 2 ((v0 . (c))(v1 . (n (+ (c) (n (c))))))) ((= (+ (c) (n (+ (c) (n (c))))) (+ (n (+ (c) (n (c)))) (c)))))
(111 (paramod 110 (1 1) 109 (1 1)) ((= (+ (n (+ (c) (n (c)))) (c)) (c))))
(112 (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))))
(113 (paramod 111 (1 1) 112 (1 1 1 1 1 2)) ((= (n (+ (n (+ v64 (c))) (n (+ (n (+ (c) (n (c)))) (+ v64 (n (c))))))) (+ (n (+ (c) (n (c)))) v64))))
(114 (instantiate 105 ((v0 . v64))) ((= (n (+ (n (+ v64 (c))) (n (+ (n (+ (c) (n (c)))) (+ v64 (n (c))))))) v64)))
(115 (paramod 114 (1 1) 113 (1 1)) ((= v64 (+ (n (+ (c) (n (c)))) v64))))
(116 (flip 115 (1)) ((= (+ (n (+ (c) (n (c)))) v64) v64)))
(117 (instantiate 116 ((v64 . v0))) ((= (+ (n (+ (c) (n (c)))) v0) v0)))
(118 (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))))))))
(119 (paramod 111 (1 1) 118 (1 1 1 1 1 2)) ((= (n (+ (n (+ v64 (c))) (n (+ v64 (+ (n (+ (c) (n (c)))) (n (c))))))) (+ v64 (n (+ (c) (n (c))))))))
(120 (instantiate 117 ((v0 . (n (c))))) ((= (+ (n (+ (c) (n (c)))) (n (c))) (n (c)))))
(121 (paramod 120 (1 1) 119 (1 1 1 2 1 2)) ((= (n (+ (n (+ v64 (c))) (n (+ v64 (n (c)))))) (+ v64 (n (+ (c) (n (c))))))))
(122 (instantiate 4 ((v0 . v64)(v1 . (c)))) ((= (n (+ (n (+ v64 (c))) (n (+ v64 (n (c)))))) v64)))
(123 (paramod 122 (1 1) 121 (1 1)) ((= v64 (+ v64 (n (+ (c) (n (c))))))))
(124 (flip 123 (1)) ((= (+ v64 (n (+ (c) (n (c))))) v64)))
(125 (instantiate 124 ((v64 . v0))) ((= (+ v0 (n (+ (c) (n (c))))) v0)))
(126 (instantiate 117 ((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)))))))
(127 (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)))))))
(128 (paramod 126 (1 1) 127 (1 1 1 1 1)) ((= (n (+ (n (+ (n (+ v65 v66)) (n (+ v65 (n v66))))) (n (+ (n (+ (c) (n (c)))) v65)))) (n (+ (c) (n (c)))))))
(129 (instantiate 4 ((v0 . v65)(v1 . v66))) ((= (n (+ (n (+ v65 v66)) (n (+ v65 (n v66))))) v65)))
(130 (paramod 129 (1 1) 128 (1 1 1 1)) ((= (n (+ v65 (n (+ (n (+ (c) (n (c)))) v65)))) (n (+ (c) (n (c)))))))
(131 (instantiate 117 ((v0 . v65))) ((= (+ (n (+ (c) (n (c)))) v65) v65)))
(132 (paramod 131 (1 1) 130 (1 1 1 2 1)) ((= (n (+ v65 (n v65))) (n (+ (c) (n (c)))))))
(133 (instantiate 132 ((v65 . v0))) ((= (n (+ v0 (n v0))) (n (+ (c) (n (c)))))))
(134 (instantiate 133 ((v0 . (n v64)))) ((= (n (+ (n v64) (n (n v64)))) (n (+ (c) (n (c)))))))
(135 (instantiate 73 ((v0 . v64)(v1 . (n (n v64))))) ((= (n (+ (n (+ (n v64) (n (n v64)))) (n (+ (n (n v64)) v64)))) (n (n v64)))))
(136 (paramod 134 (1 1) 135 (1 1 1 1)) ((= (n (+ (n (+ (c) (n (c)))) (n (+ (n (n v64)) v64)))) (n (n v64)))))
(137 (instantiate 117 ((v0 . (n (+ (n (n v64)) v64))))) ((= (+ (n (+ (c) (n (c)))) (n (+ (n (n v64)) v64))) (n (+ (n (n v64)) v64)))))
(138 (paramod 137 (1 1) 136 (1 1 1)) ((= (n (n (+ (n (n v64)) v64))) (n (n v64)))))
(139 (instantiate 138 ((v64 . v0))) ((= (n (n (+ (n (n v0)) v0))) (n (n v0)))))
(140 (instantiate 133 ((v0 . v65))) ((= (n (+ v65 (n v65))) (n (+ (c) (n (c)))))))
(141 (instantiate 73 ((v0 . (n v65))(v1 . v65))) ((= (n (+ (n (+ (n (n v65)) v65)) (n (+ v65 (n v65))))) v65)))
(142 (paramod 140 (1 1) 141 (1 1 1 2)) ((= (n (+ (n (+ (n (n v65)) v65)) (n (+ (c) (n (c)))))) v65)))
(143 (instantiate 125 ((v0 . (n (+ (n (n v65)) v65))))) ((= (+ (n (+ (n (n v65)) v65)) (n (+ (c) (n (c))))) (n (+ (n (n v65)) v65)))))
(144 (paramod 143 (1 1) 142 (1 1 1)) ((= (n (n (+ (n (n v65)) v65))) v65)))
(145 (instantiate 139 ((v0 . v65))) ((= (n (n (+ (n (n v65)) v65))) (n (n v65)))))
(146 (paramod 145 (1 1) 144 (1 1)) ((= (n (n v65)) v65)))
(147 (instantiate 146 ((v65 . v0))) ((= (n (n v0)) v0)))
(148 (instantiate 147 ((v0 . (+ (n (+ (n v0) v1)) (n (+ v0 v1)))))) ((= (n (n (+ (n (+ (n v0) v1)) (n (+ v0 v1))))) (+ (n (+ (n v0) v1)) (n (+ v0 v1))))))
(149 (paramod 83 (1 1) 148 (1 1 1)) ((= (n v1) (+ (n (+ (n v0) v1)) (n (+ v0 v1))))))
(150 (flip 149 (1)) ((= (+ (n (+ (n v0) v1)) (n (+ v0 v1))) (n v1))))
(151 (instantiate 150 ((v0 . (A))(v1 . (n (B))))) ((= (+ (n (+ (n (A)) (n (B)))) (n (+ (A) (n (B))))) (n (n (B))))))
(152 (paramod 151 (1 1) 52 (1 1 1)) ((not (= (n (n (B))) (B)))))
(153 (instantiate 147 ((v0 . (B)))) ((= (n (n (B))) (B))))
(154 (paramod 153 (1 1) 152 (1 1 1)) ((not (= (B) (B)))))
(155 (instantiate 1 ((v0 . (B)))) ((= (B) (B))))
(156 (resolve 154 (1) 155 (1)) ())
)