;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:24:59 1995
;;
;;;;  -> x=x.
;;;;  -> 1*x=x.
;;;;  -> x@ *x=1.
;;;;  -> ((x*y)*z)*y=x* (y* (z*y)).
;;;; A*1=A, B*B@ =1, C*x=D, y*E=F -> .
;;
;; -----> EMPTY CLAUSE at   7.45 sec ----> 995 [hyper,56,207.1,909.1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((= (* (1) v0) v0)))
(3 (input) ((= (* (@ v0) v0) (1))))
(4 (input) ((= (* (* (* v0 v1) v2) v1) (* v0 (* v1 (* v2 v1))))))
(5 (input) ((not (= (* (A) (1)) (A))) (not (= (* (B) (@ (B))) (1))) (not (= (* (C) v0) (D))) (not (= (* v1 (E)) (F)))))
(6 (instantiate 3 ((v0 . v65))) ((= (* (@ v65) v65) (1))))
(7 (instantiate 4 ((v0 . (@ v65))(v1 . v65)(v2 . v66))) ((= (* (* (* (@ v65) v65) v66) v65) (* (@ v65) (* v65 (* v66 v65))))))
(8 (paramod 6 (1 1) 7 (1 1 1 1)) ((= (* (* (1) v66) v65) (* (@ v65) (* v65 (* v66 v65))))))
(9 (instantiate 2 ((v0 . v66))) ((= (* (1) v66) v66)))
(10 (paramod 9 (1 1) 8 (1 1 1)) ((= (* v66 v65) (* (@ v65) (* v65 (* v66 v65))))))
(11 (flip 10 (1)) ((= (* (@ v65) (* v65 (* v66 v65))) (* v66 v65))))
(12 (instantiate 11 ((v65 . v0)(v66 . v1))) ((= (* (@ v0) (* v0 (* v1 v0))) (* v1 v0))))
(13 (instantiate 2 ((v0 . v65))) ((= (* (1) v65) v65)))
(14 (instantiate 4 ((v0 . (1))(v1 . v65)(v2 . v66))) ((= (* (* (* (1) v65) v66) v65) (* (1) (* v65 (* v66 v65))))))
(15 (paramod 13 (1 1) 14 (1 1 1 1)) ((= (* (* v65 v66) v65) (* (1) (* v65 (* v66 v65))))))
(16 (instantiate 2 ((v0 . (* v65 (* v66 v65))))) ((= (* (1) (* v65 (* v66 v65))) (* v65 (* v66 v65)))))
(17 (paramod 16 (1 1) 15 (1 2)) ((= (* (* v65 v66) v65) (* v65 (* v66 v65)))))
(18 (instantiate 17 ((v65 . v0)(v66 . v1))) ((= (* (* v0 v1) v0) (* v0 (* v1 v0)))))
(19 (instantiate 4 ((v1 . v66)(v2 . v65))) ((= (* (* (* v0 v66) v65) v66) (* v0 (* v66 (* v65 v66))))))
(20 (instantiate 4 ((v0 . (* v0 v66))(v1 . v65)(v2 . v66))) ((= (* (* (* (* v0 v66) v65) v66) v65) (* (* v0 v66) (* v65 (* v66 v65))))))
(21 (paramod 19 (1 1) 20 (1 1 1)) ((= (* (* v0 (* v66 (* v65 v66))) v65) (* (* v0 v66) (* v65 (* v66 v65))))))
(22 (instantiate 21 ((v65 . v2)(v66 . v1))) ((= (* (* v0 (* v1 (* v2 v1))) v2) (* (* v0 v1) (* v2 (* v1 v2))))))
(23 (instantiate 3 ((v0 . v65))) ((= (* (@ v65) v65) (1))))
(24 (instantiate 18 ((v0 . (@ v65))(v1 . v65))) ((= (* (* (@ v65) v65) (@ v65)) (* (@ v65) (* v65 (@ v65))))))
(25 (paramod 23 (1 1) 24 (1 1 1)) ((= (* (1) (@ v65)) (* (@ v65) (* v65 (@ v65))))))
(26 (instantiate 2 ((v0 . (@ v65)))) ((= (* (1) (@ v65)) (@ v65))))
(27 (paramod 26 (1 1) 25 (1 1)) ((= (@ v65) (* (@ v65) (* v65 (@ v65))))))
(28 (flip 27 (1)) ((= (* (@ v65) (* v65 (@ v65))) (@ v65))))
(29 (instantiate 28 ((v65 . v0))) ((= (* (@ v0) (* v0 (@ v0))) (@ v0))))
(30 (instantiate 18 ((v0 . v66)(v1 . v65))) ((= (* (* v66 v65) v66) (* v66 (* v65 v66)))))
(31 (instantiate 4 ((v0 . v66)(v1 . v65)(v2 . v66))) ((= (* (* (* v66 v65) v66) v65) (* v66 (* v65 (* v66 v65))))))
(32 (paramod 30 (1 1) 31 (1 1 1)) ((= (* (* v66 (* v65 v66)) v65) (* v66 (* v65 (* v66 v65))))))
(33 (instantiate 32 ((v65 . v1)(v66 . v0))) ((= (* (* v0 (* v1 v0)) v1) (* v0 (* v1 (* v0 v1))))))
(34 (instantiate 18 ((v0 . v64))) ((= (* (* v64 v1) v64) (* v64 (* v1 v64)))))
(35 (instantiate 12 ((v0 . v64)(v1 . (* v64 v1)))) ((= (* (@ v64) (* v64 (* (* v64 v1) v64))) (* (* v64 v1) v64))))
(36 (paramod 34 (1 1) 35 (1 1 2 2)) ((= (* (@ v64) (* v64 (* v64 (* v1 v64)))) (* (* v64 v1) v64))))
(37 (instantiate 18 ((v0 . v64)(v1 . v1))) ((= (* (* v64 v1) v64) (* v64 (* v1 v64)))))
(38 (paramod 37 (1 1) 36 (1 2)) ((= (* (@ v64) (* v64 (* v64 (* v1 v64)))) (* v64 (* v1 v64)))))
(39 (instantiate 38 ((v64 . v0))) ((= (* (@ v0) (* v0 (* v0 (* v1 v0)))) (* v0 (* v1 v0)))))
(40 (instantiate 4 ((v1 . v64))) ((= (* (* (* v0 v64) v2) v64) (* v0 (* v64 (* v2 v64))))))
(41 (instantiate 12 ((v0 . v64)(v1 . (* (* v0 v64) v2)))) ((= (* (@ v64) (* v64 (* (* (* v0 v64) v2) v64))) (* (* (* v0 v64) v2) v64))))
(42 (paramod 40 (1 1) 41 (1 1 2 2)) ((= (* (@ v64) (* v64 (* v0 (* v64 (* v2 v64))))) (* (* (* v0 v64) v2) v64))))
(43 (instantiate 4 ((v0 . v0)(v1 . v64)(v2 . v2))) ((= (* (* (* v0 v64) v2) v64) (* v0 (* v64 (* v2 v64))))))
(44 (paramod 43 (1 1) 42 (1 2)) ((= (* (@ v64) (* v64 (* v0 (* v64 (* v2 v64))))) (* v0 (* v64 (* v2 v64))))))
(45 (instantiate 44 ((v0 . v1)(v64 . v0))) ((= (* (@ v0) (* v0 (* v1 (* v0 (* v2 v0))))) (* v1 (* v0 (* v2 v0))))))
(46 (instantiate 2 ((v0 . v64))) ((= (* (1) v64) v64)))
(47 (instantiate 12 ((v0 . v64)(v1 . (1)))) ((= (* (@ v64) (* v64 (* (1) v64))) (* (1) v64))))
(48 (paramod 46 (1 1) 47 (1 1 2 2)) ((= (* (@ v64) (* v64 v64)) (* (1) v64))))
(49 (instantiate 2 ((v0 . v64))) ((= (* (1) v64) v64)))
(50 (paramod 49 (1 1) 48 (1 2)) ((= (* (@ v64) (* v64 v64)) v64)))
(51 (instantiate 50 ((v64 . v0))) ((= (* (@ v0) (* v0 v0)) v0)))
(52 (instantiate 29 ((v0 . v65))) ((= (* (@ v65) (* v65 (@ v65))) (@ v65))))
(53 (instantiate 12 ((v0 . (@ v65))(v1 . v65))) ((= (* (@ (@ v65)) (* (@ v65) (* v65 (@ v65)))) (* v65 (@ v65)))))
(54 (paramod 52 (1 1) 53 (1 1 2)) ((= (* (@ (@ v65)) (@ v65)) (* v65 (@ v65)))))
(55 (instantiate 3 ((v0 . (@ v65)))) ((= (* (@ (@ v65)) (@ v65)) (1))))
(56 (paramod 55 (1 1) 54 (1 1)) ((= (1) (* v65 (@ v65)))))
(57 (flip 56 (1)) ((= (* v65 (@ v65)) (1))))
(58 (instantiate 57 ((v65 . v0))) ((= (* v0 (@ v0)) (1))))
(59 (instantiate 58 ((v0 . (B)))) ((= (* (B) (@ (B))) (1))))
(60 (paramod 59 (1 1) 5 (2 1 1)) ((not (= (* (A) (1)) (A))) (not (= (1) (1))) (not (= (* (C) v0) (D))) (not (= (* v1 (E)) (F)))))
(61 (instantiate 1 ((v0 . (1)))) ((= (1) (1))))
(62 (resolve 60 (2) 61 (1)) ((not (= (* (A) (1)) (A))) (not (= (* (C) v0) (D))) (not (= (* v1 (E)) (F)))))
(63 (instantiate 58 ((v0 . (* v64 v65)))) ((= (* (* v64 v65) (@ (* v64 v65))) (1))))
(64 (instantiate 4 ((v0 . v64)(v1 . v65)(v2 . (@ (* v64 v65))))) ((= (* (* (* v64 v65) (@ (* v64 v65))) v65) (* v64 (* v65 (* (@ (* v64 v65)) v65))))))
(65 (paramod 63 (1 1) 64 (1 1 1)) ((= (* (1) v65) (* v64 (* v65 (* (@ (* v64 v65)) v65))))))
(66 (instantiate 2 ((v0 . v65))) ((= (* (1) v65) v65)))
(67 (paramod 66 (1 1) 65 (1 1)) ((= v65 (* v64 (* v65 (* (@ (* v64 v65)) v65))))))
(68 (flip 67 (1)) ((= (* v64 (* v65 (* (@ (* v64 v65)) v65))) v65)))
(69 (instantiate 68 ((v64 . v0)(v65 . v1))) ((= (* v0 (* v1 (* (@ (* v0 v1)) v1))) v1)))
(70 (instantiate 58 ((v0 . v64))) ((= (* v64 (@ v64)) (1))))
(71 (instantiate 18 ((v0 . v64)(v1 . (@ v64)))) ((= (* (* v64 (@ v64)) v64) (* v64 (* (@ v64) v64)))))
(72 (paramod 70 (1 1) 71 (1 1 1)) ((= (* (1) v64) (* v64 (* (@ v64) v64)))))
(73 (instantiate 2 ((v0 . v64))) ((= (* (1) v64) v64)))
(74 (paramod 73 (1 1) 72 (1 1)) ((= v64 (* v64 (* (@ v64) v64)))))
(75 (instantiate 3 ((v0 . v64))) ((= (* (@ v64) v64) (1))))
(76 (paramod 75 (1 1) 74 (1 2 2)) ((= v64 (* v64 (1)))))
(77 (flip 76 (1)) ((= (* v64 (1)) v64)))
(78 (instantiate 77 ((v64 . v0))) ((= (* v0 (1)) v0)))
(79 (instantiate 58 ((v0 . v64))) ((= (* v64 (@ v64)) (1))))
(80 (instantiate 4 ((v0 . v64)(v1 . (@ v64))(v2 . v66))) ((= (* (* (* v64 (@ v64)) v66) (@ v64)) (* v64 (* (@ v64) (* v66 (@ v64)))))))
(81 (paramod 79 (1 1) 80 (1 1 1 1)) ((= (* (* (1) v66) (@ v64)) (* v64 (* (@ v64) (* v66 (@ v64)))))))
(82 (instantiate 2 ((v0 . v66))) ((= (* (1) v66) v66)))
(83 (paramod 82 (1 1) 81 (1 1 1)) ((= (* v66 (@ v64)) (* v64 (* (@ v64) (* v66 (@ v64)))))))
(84 (flip 83 (1)) ((= (* v64 (* (@ v64) (* v66 (@ v64)))) (* v66 (@ v64)))))
(85 (instantiate 84 ((v64 . v0)(v66 . v1))) ((= (* v0 (* (@ v0) (* v1 (@ v0)))) (* v1 (@ v0)))))
(86 (instantiate 78 ((v0 . (A)))) ((= (* (A) (1)) (A))))
(87 (paramod 86 (1 1) 62 (1 1 1)) ((not (= (A) (A))) (not (= (* (C) v0) (D))) (not (= (* v1 (E)) (F)))))
(88 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(89 (resolve 87 (1) 88 (1)) ((not (= (* (C) v0) (D))) (not (= (* v1 (E)) (F)))))
(90 (instantiate 2 ((v0 . v65))) ((= (* (1) v65) v65)))
(91 (instantiate 22 ((v0 . v64)(v1 . v65)(v2 . (1)))) ((= (* (* v64 (* v65 (* (1) v65))) (1)) (* (* v64 v65) (* (1) (* v65 (1)))))))
(92 (paramod 90 (1 1) 91 (1 1 1 2 2)) ((= (* (* v64 (* v65 v65)) (1)) (* (* v64 v65) (* (1) (* v65 (1)))))))
(93 (instantiate 78 ((v0 . (* v64 (* v65 v65))))) ((= (* (* v64 (* v65 v65)) (1)) (* v64 (* v65 v65)))))
(94 (paramod 93 (1 1) 92 (1 1)) ((= (* v64 (* v65 v65)) (* (* v64 v65) (* (1) (* v65 (1)))))))
(95 (instantiate 78 ((v0 . v65))) ((= (* v65 (1)) v65)))
(96 (paramod 95 (1 1) 94 (1 2 2 2)) ((= (* v64 (* v65 v65)) (* (* v64 v65) (* (1) v65)))))
(97 (instantiate 2 ((v0 . v65))) ((= (* (1) v65) v65)))
(98 (paramod 97 (1 1) 96 (1 2 2)) ((= (* v64 (* v65 v65)) (* (* v64 v65) v65))))
(99 (flip 98 (1)) ((= (* (* v64 v65) v65) (* v64 (* v65 v65)))))
(100 (instantiate 99 ((v64 . v0)(v65 . v1))) ((= (* (* v0 v1) v1) (* v0 (* v1 v1)))))
(101 (instantiate 18 ((v0 . (@ v0))(v1 . (* v0 v0)))) ((= (* (* (@ v0) (* v0 v0)) (@ v0)) (* (@ v0) (* (* v0 v0) (@ v0))))))
(102 (paramod 51 (1 1) 101 (1 1 1)) ((= (* v0 (@ v0)) (* (@ v0) (* (* v0 v0) (@ v0))))))
(103 (paramod 58 (1 1) 102 (1 1)) ((= (1) (* (@ v0) (* (* v0 v0) (@ v0))))))
(104 (flip 103 (1)) ((= (* (@ v0) (* (* v0 v0) (@ v0))) (1))))
(105 (instantiate 58 ((v0 . v64))) ((= (* v64 (@ v64)) (1))))
(106 (instantiate 100 ((v0 . v64)(v1 . (@ v64)))) ((= (* (* v64 (@ v64)) (@ v64)) (* v64 (* (@ v64) (@ v64))))))
(107 (paramod 105 (1 1) 106 (1 1 1)) ((= (* (1) (@ v64)) (* v64 (* (@ v64) (@ v64))))))
(108 (instantiate 2 ((v0 . (@ v64)))) ((= (* (1) (@ v64)) (@ v64))))
(109 (paramod 108 (1 1) 107 (1 1)) ((= (@ v64) (* v64 (* (@ v64) (@ v64))))))
(110 (flip 109 (1)) ((= (* v64 (* (@ v64) (@ v64))) (@ v64))))
(111 (instantiate 110 ((v64 . v0))) ((= (* v0 (* (@ v0) (@ v0))) (@ v0))))
(112 (instantiate 111 ((v0 . v64))) ((= (* v64 (* (@ v64) (@ v64))) (@ v64))))
(113 (instantiate 18 ((v0 . v64)(v1 . (* (@ v64) (@ v64))))) ((= (* (* v64 (* (@ v64) (@ v64))) v64) (* v64 (* (* (@ v64) (@ v64)) v64)))))
(114 (paramod 112 (1 1) 113 (1 1 1)) ((= (* (@ v64) v64) (* v64 (* (* (@ v64) (@ v64)) v64)))))
(115 (instantiate 3 ((v0 . v64))) ((= (* (@ v64) v64) (1))))
(116 (paramod 115 (1 1) 114 (1 1)) ((= (1) (* v64 (* (* (@ v64) (@ v64)) v64)))))
(117 (flip 116 (1)) ((= (* v64 (* (* (@ v64) (@ v64)) v64)) (1))))
(118 (instantiate 117 ((v64 . v0))) ((= (* v0 (* (* (@ v0) (@ v0)) v0)) (1))))
(119 (instantiate 12 ((v0 . (@ v0))(v1 . (* v0 v0)))) ((= (* (@ (@ v0)) (* (@ v0) (* (* v0 v0) (@ v0)))) (* (* v0 v0) (@ v0)))))
(120 (paramod 104 (1 1) 119 (1 1 2)) ((= (* (@ (@ v0)) (1)) (* (* v0 v0) (@ v0)))))
(121 (instantiate 78 ((v0 . (@ (@ v0))))) ((= (* (@ (@ v0)) (1)) (@ (@ v0)))))
(122 (paramod 121 (1 1) 120 (1 1)) ((= (@ (@ v0)) (* (* v0 v0) (@ v0)))))
(123 (instantiate 22 ((v0 . v64)(v1 . (@ v0))(v2 . (* v0 v0)))) ((= (* (* v64 (* (@ v0) (* (* v0 v0) (@ v0)))) (* v0 v0)) (* (* v64 (@ v0)) (* (* v0 v0) (* (@ v0) (* v0 v0)))))))
(124 (paramod 104 (1 1) 123 (1 1 1 2)) ((= (* (* v64 (1)) (* v0 v0)) (* (* v64 (@ v0)) (* (* v0 v0) (* (@ v0) (* v0 v0)))))))
(125 (instantiate 78 ((v0 . v64))) ((= (* v64 (1)) v64)))
(126 (paramod 125 (1 1) 124 (1 1 1)) ((= (* v64 (* v0 v0)) (* (* v64 (@ v0)) (* (* v0 v0) (* (@ v0) (* v0 v0)))))))
(127 (paramod 51 (1 1) 126 (1 2 2 2)) ((= (* v64 (* v0 v0)) (* (* v64 (@ v0)) (* (* v0 v0) v0)))))
(128 (instantiate 18 ((v0 . v0)(v1 . v0))) ((= (* (* v0 v0) v0) (* v0 (* v0 v0)))))
(129 (paramod 128 (1 1) 127 (1 2 2)) ((= (* v64 (* v0 v0)) (* (* v64 (@ v0)) (* v0 (* v0 v0))))))
(130 (flip 129 (1)) ((= (* (* v64 (@ v0)) (* v0 (* v0 v0))) (* v64 (* v0 v0)))))
(131 (instantiate 130 ((v0 . v1)(v64 . v0))) ((= (* (* v0 (@ v1)) (* v1 (* v1 v1))) (* v0 (* v1 v1)))))
(132 (instantiate 3 ((v0 . (@ v0)))) ((= (* (@ (@ v0)) (@ v0)) (1))))
(133 (paramod 122 (1 1) 132 (1 1 1)) ((= (* (* (* v0 v0) (@ v0)) (@ v0)) (1))))
(134 (instantiate 100 ((v0 . (* v0 v0))(v1 . (@ v0)))) ((= (* (* (* v0 v0) (@ v0)) (@ v0)) (* (* v0 v0) (* (@ v0) (@ v0))))))
(135 (paramod 134 (1 1) 133 (1 1)) ((= (* (* v0 v0) (* (@ v0) (@ v0))) (1))))
(136 (instantiate 118 ((v0 . v64))) ((= (* v64 (* (* (@ v64) (@ v64)) v64)) (1))))
(137 (instantiate 12 ((v0 . v64)(v1 . (* (@ v64) (@ v64))))) ((= (* (@ v64) (* v64 (* (* (@ v64) (@ v64)) v64))) (* (* (@ v64) (@ v64)) v64))))
(138 (paramod 136 (1 1) 137 (1 1 2)) ((= (* (@ v64) (1)) (* (* (@ v64) (@ v64)) v64))))
(139 (instantiate 78 ((v0 . (@ v64)))) ((= (* (@ v64) (1)) (@ v64))))
(140 (paramod 139 (1 1) 138 (1 1)) ((= (@ v64) (* (* (@ v64) (@ v64)) v64))))
(141 (flip 140 (1)) ((= (* (* (@ v64) (@ v64)) v64) (@ v64))))
(142 (instantiate 141 ((v64 . v0))) ((= (* (* (@ v0) (@ v0)) v0) (@ v0))))
(143 (instantiate 69 ((v0 . v64))) ((= (* v64 (* v1 (* (@ (* v64 v1)) v1))) v1)))
(144 (instantiate 18 ((v0 . v64)(v1 . (* v1 (* (@ (* v64 v1)) v1))))) ((= (* (* v64 (* v1 (* (@ (* v64 v1)) v1))) v64) (* v64 (* (* v1 (* (@ (* v64 v1)) v1)) v64)))))
(145 (paramod 143 (1 1) 144 (1 1 1)) ((= (* v1 v64) (* v64 (* (* v1 (* (@ (* v64 v1)) v1)) v64)))))
(146 (flip 145 (1)) ((= (* v64 (* (* v1 (* (@ (* v64 v1)) v1)) v64)) (* v1 v64))))
(147 (instantiate 146 ((v64 . v0))) ((= (* v0 (* (* v1 (* (@ (* v0 v1)) v1)) v0)) (* v1 v0))))
(148 (instantiate 142 ((v0 . (@ v64)))) ((= (* (* (@ (@ v64)) (@ (@ v64))) (@ v64)) (@ (@ v64)))))
(149 (instantiate 85 ((v0 . v64)(v1 . (* (@ (@ v64)) (@ (@ v64)))))) ((= (* v64 (* (@ v64) (* (* (@ (@ v64)) (@ (@ v64))) (@ v64)))) (* (* (@ (@ v64)) (@ (@ v64))) (@ v64)))))
(150 (paramod 148 (1 1) 149 (1 1 2 2)) ((= (* v64 (* (@ v64) (@ (@ v64)))) (* (* (@ (@ v64)) (@ (@ v64))) (@ v64)))))
(151 (instantiate 122 ((v0 . v64))) ((= (@ (@ v64)) (* (* v64 v64) (@ v64)))))
(152 (paramod 151 (1 1) 150 (1 1 2 2)) ((= (* v64 (* (@ v64) (* (* v64 v64) (@ v64)))) (* (* (@ (@ v64)) (@ (@ v64))) (@ v64)))))
(153 (instantiate 104 ((v0 . v64))) ((= (* (@ v64) (* (* v64 v64) (@ v64))) (1))))
(154 (paramod 153 (1 1) 152 (1 1 2)) ((= (* v64 (1)) (* (* (@ (@ v64)) (@ (@ v64))) (@ v64)))))
(155 (instantiate 78 ((v0 . v64))) ((= (* v64 (1)) v64)))
(156 (paramod 155 (1 1) 154 (1 1)) ((= v64 (* (* (@ (@ v64)) (@ (@ v64))) (@ v64)))))
(157 (instantiate 122 ((v0 . v64))) ((= (@ (@ v64)) (* (* v64 v64) (@ v64)))))
(158 (paramod 157 (1 1) 156 (1 2 1 1)) ((= v64 (* (* (* (* v64 v64) (@ v64)) (@ (@ v64))) (@ v64)))))
(159 (instantiate 122 ((v0 . v64))) ((= (@ (@ v64)) (* (* v64 v64) (@ v64)))))
(160 (paramod 159 (1 1) 158 (1 2 1 2)) ((= v64 (* (* (* (* v64 v64) (@ v64)) (* (* v64 v64) (@ v64))) (@ v64)))))
(161 (instantiate 4 ((v0 . (* v64 v64))(v1 . (@ v64))(v2 . (* (* v64 v64) (@ v64))))) ((= (* (* (* (* v64 v64) (@ v64)) (* (* v64 v64) (@ v64))) (@ v64)) (* (* v64 v64) (* (@ v64) (* (* (* v64 v64) (@ v64)) (@ v64)))))))
(162 (paramod 161 (1 1) 160 (1 2)) ((= v64 (* (* v64 v64) (* (@ v64) (* (* (* v64 v64) (@ v64)) (@ v64)))))))
(163 (instantiate 100 ((v0 . (* v64 v64))(v1 . (@ v64)))) ((= (* (* (* v64 v64) (@ v64)) (@ v64)) (* (* v64 v64) (* (@ v64) (@ v64))))))
(164 (paramod 163 (1 1) 162 (1 2 2 2)) ((= v64 (* (* v64 v64) (* (@ v64) (* (* v64 v64) (* (@ v64) (@ v64))))))))
(165 (instantiate 135 ((v0 . v64))) ((= (* (* v64 v64) (* (@ v64) (@ v64))) (1))))
(166 (paramod 165 (1 1) 164 (1 2 2 2)) ((= v64 (* (* v64 v64) (* (@ v64) (1))))))
(167 (instantiate 78 ((v0 . (@ v64)))) ((= (* (@ v64) (1)) (@ v64))))
(168 (paramod 167 (1 1) 166 (1 2 2)) ((= v64 (* (* v64 v64) (@ v64)))))
(169 (flip 168 (1)) ((= (* (* v64 v64) (@ v64)) v64)))
(170 (instantiate 169 ((v64 . v0))) ((= (* (* v0 v0) (@ v0)) v0)))
(171 (paramod 170 (1 1) 122 (1 2)) ((= (@ (@ v0)) v0)))
(172 (instantiate 69 ((v0 . v64)(v1 . v64))) ((= (* v64 (* v64 (* (@ (* v64 v64)) v64))) v64)))
(173 (instantiate 39 ((v0 . v64)(v1 . (@ (* v64 v64))))) ((= (* (@ v64) (* v64 (* v64 (* (@ (* v64 v64)) v64)))) (* v64 (* (@ (* v64 v64)) v64)))))
(174 (paramod 172 (1 1) 173 (1 1 2)) ((= (* (@ v64) v64) (* v64 (* (@ (* v64 v64)) v64)))))
(175 (instantiate 3 ((v0 . v64))) ((= (* (@ v64) v64) (1))))
(176 (paramod 175 (1 1) 174 (1 1)) ((= (1) (* v64 (* (@ (* v64 v64)) v64)))))
(177 (flip 176 (1)) ((= (* v64 (* (@ (* v64 v64)) v64)) (1))))
(178 (instantiate 177 ((v64 . v0))) ((= (* v0 (* (@ (* v0 v0)) v0)) (1))))
(179 (instantiate 178 ((v0 . v64))) ((= (* v64 (* (@ (* v64 v64)) v64)) (1))))
(180 (instantiate 12 ((v0 . v64)(v1 . (@ (* v64 v64))))) ((= (* (@ v64) (* v64 (* (@ (* v64 v64)) v64))) (* (@ (* v64 v64)) v64))))
(181 (paramod 179 (1 1) 180 (1 1 2)) ((= (* (@ v64) (1)) (* (@ (* v64 v64)) v64))))
(182 (instantiate 78 ((v0 . (@ v64)))) ((= (* (@ v64) (1)) (@ v64))))
(183 (paramod 182 (1 1) 181 (1 1)) ((= (@ v64) (* (@ (* v64 v64)) v64))))
(184 (flip 183 (1)) ((= (* (@ (* v64 v64)) v64) (@ v64))))
(185 (instantiate 184 ((v64 . v0))) ((= (* (@ (* v0 v0)) v0) (@ v0))))
(186 (instantiate 185 ((v0 . v64))) ((= (* (@ (* v64 v64)) v64) (@ v64))))
(187 (instantiate 45 ((v0 . v64)(v1 . v65)(v2 . (@ (* v64 v64))))) ((= (* (@ v64) (* v64 (* v65 (* v64 (* (@ (* v64 v64)) v64))))) (* v65 (* v64 (* (@ (* v64 v64)) v64))))))
(188 (paramod 186 (1 1) 187 (1 1 2 2 2 2)) ((= (* (@ v64) (* v64 (* v65 (* v64 (@ v64))))) (* v65 (* v64 (* (@ (* v64 v64)) v64))))))
(189 (instantiate 58 ((v0 . v64))) ((= (* v64 (@ v64)) (1))))
(190 (paramod 189 (1 1) 188 (1 1 2 2 2)) ((= (* (@ v64) (* v64 (* v65 (1)))) (* v65 (* v64 (* (@ (* v64 v64)) v64))))))
(191 (instantiate 78 ((v0 . v65))) ((= (* v65 (1)) v65)))
(192 (paramod 191 (1 1) 190 (1 1 2 2)) ((= (* (@ v64) (* v64 v65)) (* v65 (* v64 (* (@ (* v64 v64)) v64))))))
(193 (instantiate 185 ((v0 . v64))) ((= (* (@ (* v64 v64)) v64) (@ v64))))
(194 (paramod 193 (1 1) 192 (1 2 2 2)) ((= (* (@ v64) (* v64 v65)) (* v65 (* v64 (@ v64))))))
(195 (instantiate 58 ((v0 . v64))) ((= (* v64 (@ v64)) (1))))
(196 (paramod 195 (1 1) 194 (1 2 2)) ((= (* (@ v64) (* v64 v65)) (* v65 (1)))))
(197 (instantiate 78 ((v0 . v65))) ((= (* v65 (1)) v65)))
(198 (paramod 197 (1 1) 196 (1 2)) ((= (* (@ v64) (* v64 v65)) v65)))
(199 (instantiate 198 ((v64 . v0)(v65 . v1))) ((= (* (@ v0) (* v0 v1)) v1)))
(200 (instantiate 45 ((v0 . (@ v0))(v1 . v65)(v2 . (* v0 v0)))) ((= (* (@ (@ v0)) (* (@ v0) (* v65 (* (@ v0) (* (* v0 v0) (@ v0)))))) (* v65 (* (@ v0) (* (* v0 v0) (@ v0)))))))
(201 (paramod 170 (1 1) 200 (1 1 2 2 2 2)) ((= (* (@ (@ v0)) (* (@ v0) (* v65 (* (@ v0) v0)))) (* v65 (* (@ v0) (* (* v0 v0) (@ v0)))))))
(202 (paramod 171 (1 1) 201 (1 1 1)) ((= (* v0 (* (@ v0) (* v65 (* (@ v0) v0)))) (* v65 (* (@ v0) (* (* v0 v0) (@ v0)))))))
(203 (paramod 3 (1 1) 202 (1 1 2 2 2)) ((= (* v0 (* (@ v0) (* v65 (1)))) (* v65 (* (@ v0) (* (* v0 v0) (@ v0)))))))
(204 (instantiate 78 ((v0 . v65))) ((= (* v65 (1)) v65)))
(205 (paramod 204 (1 1) 203 (1 1 2 2)) ((= (* v0 (* (@ v0) v65)) (* v65 (* (@ v0) (* (* v0 v0) (@ v0)))))))
(206 (paramod 170 (1 1) 205 (1 2 2 2)) ((= (* v0 (* (@ v0) v65)) (* v65 (* (@ v0) v0)))))
(207 (paramod 3 (1 1) 206 (1 2 2)) ((= (* v0 (* (@ v0) v65)) (* v65 (1)))))
(208 (instantiate 78 ((v0 . v65))) ((= (* v65 (1)) v65)))
(209 (paramod 208 (1 1) 207 (1 2)) ((= (* v0 (* (@ v0) v65)) v65)))
(210 (instantiate 209 ((v65 . v1))) ((= (* v0 (* (@ v0) v1)) v1)))
(211 (instantiate 69 ((v0 . v64))) ((= (* v64 (* v1 (* (@ (* v64 v1)) v1))) v1)))
(212 (instantiate 199 ((v0 . v64)(v1 . (* v1 (* (@ (* v64 v1)) v1))))) ((= (* (@ v64) (* v64 (* v1 (* (@ (* v64 v1)) v1)))) (* v1 (* (@ (* v64 v1)) v1)))))
(213 (paramod 211 (1 1) 212 (1 1 2)) ((= (* (@ v64) v1) (* v1 (* (@ (* v64 v1)) v1)))))
(214 (flip 213 (1)) ((= (* v1 (* (@ (* v64 v1)) v1)) (* (@ v64) v1))))
(215 (instantiate 214 ((v1 . v0)(v64 . v1))) ((= (* v0 (* (@ (* v1 v0)) v0)) (* (@ v1) v0))))
(216 (instantiate 215 ((v0 . v1)(v1 . v0))) ((= (* v1 (* (@ (* v0 v1)) v1)) (* (@ v0) v1))))
(217 (paramod 216 (1 1) 147 (1 1 2 1)) ((= (* v0 (* (* (@ v0) v1) v0)) (* v1 v0))))
(218 (instantiate 217 ((v0 . (@ v64)))) ((= (* (@ v64) (* (* (@ (@ v64)) v1) (@ v64))) (* v1 (@ v64)))))
(219 (instantiate 210 ((v0 . v64)(v1 . (* (* (@ (@ v64)) v1) (@ v64))))) ((= (* v64 (* (@ v64) (* (* (@ (@ v64)) v1) (@ v64)))) (* (* (@ (@ v64)) v1) (@ v64)))))
(220 (paramod 218 (1 1) 219 (1 1 2)) ((= (* v64 (* v1 (@ v64))) (* (* (@ (@ v64)) v1) (@ v64)))))
(221 (instantiate 171 ((v0 . v64))) ((= (@ (@ v64)) v64)))
(222 (paramod 221 (1 1) 220 (1 2 1 1)) ((= (* v64 (* v1 (@ v64))) (* (* v64 v1) (@ v64)))))
(223 (flip 222 (1)) ((= (* (* v64 v1) (@ v64)) (* v64 (* v1 (@ v64))))))
(224 (instantiate 223 ((v64 . v0))) ((= (* (* v0 v1) (@ v0)) (* v0 (* v1 (@ v0))))))
(225 (instantiate 217 ((v0 . v64))) ((= (* v64 (* (* (@ v64) v1) v64)) (* v1 v64))))
(226 (instantiate 33 ((v0 . v64)(v1 . (* (@ v64) v1)))) ((= (* (* v64 (* (* (@ v64) v1) v64)) (* (@ v64) v1)) (* v64 (* (* (@ v64) v1) (* v64 (* (@ v64) v1)))))))
(227 (paramod 225 (1 1) 226 (1 1 1)) ((= (* (* v1 v64) (* (@ v64) v1)) (* v64 (* (* (@ v64) v1) (* v64 (* (@ v64) v1)))))))
(228 (instantiate 210 ((v0 . v64)(v1 . v1))) ((= (* v64 (* (@ v64) v1)) v1)))
(229 (paramod 228 (1 1) 227 (1 2 2 2)) ((= (* (* v1 v64) (* (@ v64) v1)) (* v64 (* (* (@ v64) v1) v1)))))
(230 (instantiate 100 ((v0 . (@ v64))(v1 . v1))) ((= (* (* (@ v64) v1) v1) (* (@ v64) (* v1 v1)))))
(231 (paramod 230 (1 1) 229 (1 2 2)) ((= (* (* v1 v64) (* (@ v64) v1)) (* v64 (* (@ v64) (* v1 v1))))))
(232 (instantiate 210 ((v0 . v64)(v1 . (* v1 v1)))) ((= (* v64 (* (@ v64) (* v1 v1))) (* v1 v1))))
(233 (paramod 232 (1 1) 231 (1 2)) ((= (* (* v1 v64) (* (@ v64) v1)) (* v1 v1))))
(234 (instantiate 233 ((v1 . v0)(v64 . v1))) ((= (* (* v0 v1) (* (@ v1) v0)) (* v0 v0))))
(235 (instantiate 217 ((v0 . v64))) ((= (* v64 (* (* (@ v64) v1) v64)) (* v1 v64))))
(236 (instantiate 199 ((v0 . v64)(v1 . (* (* (@ v64) v1) v64)))) ((= (* (@ v64) (* v64 (* (* (@ v64) v1) v64))) (* (* (@ v64) v1) v64))))
(237 (paramod 235 (1 1) 236 (1 1 2)) ((= (* (@ v64) (* v1 v64)) (* (* (@ v64) v1) v64))))
(238 (flip 237 (1)) ((= (* (* (@ v64) v1) v64) (* (@ v64) (* v1 v64)))))
(239 (instantiate 238 ((v64 . v0))) ((= (* (* (@ v0) v1) v0) (* (@ v0) (* v1 v0)))))
(240 (instantiate 234 ((v0 . v64)(v1 . v65))) ((= (* (* v64 v65) (* (@ v65) v64)) (* v64 v64))))
(241 (instantiate 4 ((v0 . v64)(v1 . v65)(v2 . (* (@ v65) v64)))) ((= (* (* (* v64 v65) (* (@ v65) v64)) v65) (* v64 (* v65 (* (* (@ v65) v64) v65))))))
(242 (paramod 240 (1 1) 241 (1 1 1)) ((= (* (* v64 v64) v65) (* v64 (* v65 (* (* (@ v65) v64) v65))))))
(243 (instantiate 239 ((v0 . v65)(v1 . v64))) ((= (* (* (@ v65) v64) v65) (* (@ v65) (* v64 v65)))))
(244 (paramod 243 (1 1) 242 (1 2 2 2)) ((= (* (* v64 v64) v65) (* v64 (* v65 (* (@ v65) (* v64 v65)))))))
(245 (instantiate 210 ((v0 . v65)(v1 . (* v64 v65)))) ((= (* v65 (* (@ v65) (* v64 v65))) (* v64 v65))))
(246 (paramod 245 (1 1) 244 (1 2 2)) ((= (* (* v64 v64) v65) (* v64 (* v64 v65)))))
(247 (instantiate 246 ((v64 . v0)(v65 . v1))) ((= (* (* v0 v0) v1) (* v0 (* v0 v1)))))
(248 (instantiate 131 ((v0 . v64))) ((= (* (* v64 (@ v1)) (* v1 (* v1 v1))) (* v64 (* v1 v1)))))
(249 (instantiate 4 ((v0 . v64)(v1 . (@ v1))(v2 . (* v1 (* v1 v1))))) ((= (* (* (* v64 (@ v1)) (* v1 (* v1 v1))) (@ v1)) (* v64 (* (@ v1) (* (* v1 (* v1 v1)) (@ v1)))))))
(250 (paramod 248 (1 1) 249 (1 1 1)) ((= (* (* v64 (* v1 v1)) (@ v1)) (* v64 (* (@ v1) (* (* v1 (* v1 v1)) (@ v1)))))))
(251 (instantiate 224 ((v0 . v1)(v1 . (* v1 v1)))) ((= (* (* v1 (* v1 v1)) (@ v1)) (* v1 (* (* v1 v1) (@ v1))))))
(252 (paramod 251 (1 1) 250 (1 2 2 2)) ((= (* (* v64 (* v1 v1)) (@ v1)) (* v64 (* (@ v1) (* v1 (* (* v1 v1) (@ v1))))))))
(253 (instantiate 247 ((v0 . v1)(v1 . (@ v1)))) ((= (* (* v1 v1) (@ v1)) (* v1 (* v1 (@ v1))))))
(254 (paramod 253 (1 1) 252 (1 2 2 2 2)) ((= (* (* v64 (* v1 v1)) (@ v1)) (* v64 (* (@ v1) (* v1 (* v1 (* v1 (@ v1)))))))))
(255 (instantiate 58 ((v0 . v1))) ((= (* v1 (@ v1)) (1))))
(256 (paramod 255 (1 1) 254 (1 2 2 2 2 2)) ((= (* (* v64 (* v1 v1)) (@ v1)) (* v64 (* (@ v1) (* v1 (* v1 (1))))))))
(257 (instantiate 78 ((v0 . v1))) ((= (* v1 (1)) v1)))
(258 (paramod 257 (1 1) 256 (1 2 2 2 2)) ((= (* (* v64 (* v1 v1)) (@ v1)) (* v64 (* (@ v1) (* v1 v1))))))
(259 (instantiate 199 ((v0 . v1)(v1 . v1))) ((= (* (@ v1) (* v1 v1)) v1)))
(260 (paramod 259 (1 1) 258 (1 2 2)) ((= (* (* v64 (* v1 v1)) (@ v1)) (* v64 v1))))
(261 (instantiate 260 ((v64 . v0))) ((= (* (* v0 (* v1 v1)) (@ v1)) (* v0 v1))))
(262 (instantiate 4 ((v1 . (@ v65))(v2 . (* v65 v65)))) ((= (* (* (* v0 (@ v65)) (* v65 v65)) (@ v65)) (* v0 (* (@ v65) (* (* v65 v65) (@ v65)))))))
(263 (instantiate 261 ((v0 . (* v0 (@ v65)))(v1 . v65))) ((= (* (* (* v0 (@ v65)) (* v65 v65)) (@ v65)) (* (* v0 (@ v65)) v65))))
(264 (paramod 262 (1 1) 263 (1 1)) ((= (* v0 (* (@ v65) (* (* v65 v65) (@ v65)))) (* (* v0 (@ v65)) v65))))
(265 (instantiate 247 ((v0 . v65)(v1 . (@ v65)))) ((= (* (* v65 v65) (@ v65)) (* v65 (* v65 (@ v65))))))
(266 (paramod 265 (1 1) 264 (1 1 2 2)) ((= (* v0 (* (@ v65) (* v65 (* v65 (@ v65))))) (* (* v0 (@ v65)) v65))))
(267 (instantiate 58 ((v0 . v65))) ((= (* v65 (@ v65)) (1))))
(268 (paramod 267 (1 1) 266 (1 1 2 2 2)) ((= (* v0 (* (@ v65) (* v65 (1)))) (* (* v0 (@ v65)) v65))))
(269 (instantiate 78 ((v0 . v65))) ((= (* v65 (1)) v65)))
(270 (paramod 269 (1 1) 268 (1 1 2 2)) ((= (* v0 (* (@ v65) v65)) (* (* v0 (@ v65)) v65))))
(271 (instantiate 3 ((v0 . v65))) ((= (* (@ v65) v65) (1))))
(272 (paramod 271 (1 1) 270 (1 1 2)) ((= (* v0 (1)) (* (* v0 (@ v65)) v65))))
(273 (paramod 78 (1 1) 272 (1 1)) ((= v0 (* (* v0 (@ v65)) v65))))
(274 (flip 273 (1)) ((= (* (* v0 (@ v65)) v65) v0)))
(275 (instantiate 274 ((v65 . v1))) ((= (* (* v0 (@ v1)) v1) v0)))
(276 (instantiate 89 ((v0 . (* (@ (C)) (D))))) ((not (= (* (C) (* (@ (C)) (D))) (D))) (not (= (* v1 (E)) (F)))))
(277 (instantiate 210 ((v0 . (C))(v1 . (D)))) ((= (* (C) (* (@ (C)) (D))) (D))))
(278 (resolve 276 (1) 277 (1)) ((not (= (* v1 (E)) (F)))))
(279 (instantiate 278 ((v1 . v0))) ((not (= (* v0 (E)) (F)))))
(280 (instantiate 279 ((v0 . (* (F) (@ (E)))))) ((not (= (* (* (F) (@ (E))) (E)) (F)))))
(281 (instantiate 275 ((v0 . (F))(v1 . (E)))) ((= (* (* (F) (@ (E))) (E)) (F))))
(282 (resolve 280 (1) 281 (1)) ())
)