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