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