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