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