;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:24:29 1995
;;
;;;;  -> x=x.
;;;; z1*x=u, z2*y=u, z1*z=w, z3*y=w -> z2*z=z3*x.
;;;;  -> ((x*e)*e)*e=x.
;;;;  -> e* (e* (e*x))=x.
;;;;  -> C4*A=C3*B.
;;;;  -> C2*A=C1*B.
;;;;  -> C4*F=C3*E.
;;;; C2*F=C1*E -> .
;;
;; ----> UNIT CONFLICT at  74.62 sec ----> 517 [binary,515.1,13.1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((not (= (* v0 v1) v2)) (not (= (* v3 v4) v2)) (not (= (* v0 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v1))))
(3 (input) ((= (* (* (* v0 (e)) (e)) (e)) v0)))
(4 (input) ((= (* (e) (* (e) (* (e) v0))) v0)))
(5 (input) ((= (* (C4) (A)) (* (C3) (B)))))
(6 (input) ((= (* (C2) (A)) (* (C1) (B)))))
(7 (input) ((= (* (C4) (F)) (* (C3) (E)))))
(8 (input) ((not (= (* (C2) (F)) (* (C1) (E))))))
(9 (instantiate 2 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v3 v4) (* v0 v1))) (not (= (* v0 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v1))))
(10 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(11 (resolve 9 (1) 10 (1)) ((not (= (* v3 v4) (* v0 v1))) (not (= (* v0 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v1))))
(12 (instantiate 11 ((v0 . v2)(v1 . v3)(v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6))) ((not (= (* v0 v1) (* v2 v3))) (not (= (* v2 v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 v3))))
(13 (instantiate 12 ((v0 . (* (* (* v2 v3) (e)) (e)))(v1 . (e)))) ((not (= (* (* (* (* v2 v3) (e)) (e)) (e)) (* v2 v3))) (not (= (* v2 v4) v5)) (not (= (* v6 (e)) v5)) (= (* (* (* (* v2 v3) (e)) (e)) v4) (* v6 v3))))
(14 (instantiate 3 ((v0 . (* v2 v3)))) ((= (* (* (* (* v2 v3) (e)) (e)) (e)) (* v2 v3))))
(15 (resolve 13 (1) 14 (1)) ((not (= (* v2 v4) v5)) (not (= (* v6 (e)) v5)) (= (* (* (* (* v2 v3) (e)) (e)) v4) (* v6 v3))))
(16 (instantiate 15 ((v2 . v0)(v3 . v4)(v4 . v1)(v5 . v2)(v6 . v3))) ((not (= (* v0 v1) v2)) (not (= (* v3 (e)) v2)) (= (* (* (* (* v0 v4) (e)) (e)) v1) (* v3 v4))))
(17 (instantiate 16 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v3 (e)) (* v0 v1))) (= (* (* (* (* v0 v4) (e)) (e)) v1) (* v3 v4))))
(18 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(19 (resolve 17 (1) 18 (1)) ((not (= (* v3 (e)) (* v0 v1))) (= (* (* (* (* v0 v4) (e)) (e)) v1) (* v3 v4))))
(20 (instantiate 19 ((v0 . v1)(v1 . v2)(v3 . v0)(v4 . v3))) ((not (= (* v0 (e)) (* v1 v2))) (= (* (* (* (* v1 v3) (e)) (e)) v2) (* v0 v3))))
(21 (instantiate 20 ((v0 . (* (* (* v1 v2) (e)) (e))))) ((not (= (* (* (* (* v1 v2) (e)) (e)) (e)) (* v1 v2))) (= (* (* (* (* v1 v3) (e)) (e)) v2) (* (* (* (* v1 v2) (e)) (e)) v3))))
(22 (instantiate 3 ((v0 . (* v1 v2)))) ((= (* (* (* (* v1 v2) (e)) (e)) (e)) (* v1 v2))))
(23 (resolve 21 (1) 22 (1)) ((= (* (* (* (* v1 v3) (e)) (e)) v2) (* (* (* (* v1 v2) (e)) (e)) v3))))
(24 (instantiate 23 ((v1 . v0)(v3 . v1))) ((= (* (* (* (* v0 v1) (e)) (e)) v2) (* (* (* (* v0 v2) (e)) (e)) v1))))
(25 (instantiate 2 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v3 v4) (* v0 v1))) (not (= (* v0 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v1))))
(26 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(27 (resolve 25 (1) 26 (1)) ((not (= (* v3 v4) (* v0 v1))) (not (= (* v0 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v1))))
(28 (instantiate 27 ((v0 . v2)(v1 . v3)(v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6))) ((not (= (* v0 v1) (* v2 v3))) (not (= (* v2 v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 v3))))
(29 (instantiate 28 ((v0 . (* (* (* v2 v3) (e)) (e)))(v1 . (e)))) ((not (= (* (* (* (* v2 v3) (e)) (e)) (e)) (* v2 v3))) (not (= (* v2 v4) v5)) (not (= (* v6 (e)) v5)) (= (* (* (* (* v2 v3) (e)) (e)) v4) (* v6 v3))))
(30 (instantiate 3 ((v0 . (* v2 v3)))) ((= (* (* (* (* v2 v3) (e)) (e)) (e)) (* v2 v3))))
(31 (resolve 29 (1) 30 (1)) ((not (= (* v2 v4) v5)) (not (= (* v6 (e)) v5)) (= (* (* (* (* v2 v3) (e)) (e)) v4) (* v6 v3))))
(32 (instantiate 31 ((v2 . v0)(v3 . v4)(v4 . v1)(v5 . v2)(v6 . v3))) ((not (= (* v0 v1) v2)) (not (= (* v3 (e)) v2)) (= (* (* (* (* v0 v4) (e)) (e)) v1) (* v3 v4))))
(33 (instantiate 32 ((v0 . (C2))(v1 . (A))(v2 . (* (C1) (B))))) ((not (= (* (C2) (A)) (* (C1) (B)))) (not (= (* v3 (e)) (* (C1) (B)))) (= (* (* (* (* (C2) v4) (e)) (e)) (A)) (* v3 v4))))
(34 (resolve 33 (1) 6 (1)) ((not (= (* v3 (e)) (* (C1) (B)))) (= (* (* (* (* (C2) v4) (e)) (e)) (A)) (* v3 v4))))
(35 (instantiate 34 ((v3 . v0)(v4 . v1))) ((not (= (* v0 (e)) (* (C1) (B)))) (= (* (* (* (* (C2) v1) (e)) (e)) (A)) (* v0 v1))))
(36 (instantiate 35 ((v0 . (* (* (* (C1) (B)) (e)) (e))))) ((not (= (* (* (* (* (C1) (B)) (e)) (e)) (e)) (* (C1) (B)))) (= (* (* (* (* (C2) v1) (e)) (e)) (A)) (* (* (* (* (C1) (B)) (e)) (e)) v1))))
(37 (instantiate 3 ((v0 . (* (C1) (B))))) ((= (* (* (* (* (C1) (B)) (e)) (e)) (e)) (* (C1) (B)))))
(38 (resolve 36 (1) 37 (1)) ((= (* (* (* (* (C2) v1) (e)) (e)) (A)) (* (* (* (* (C1) (B)) (e)) (e)) v1))))
(39 (instantiate 38 ((v1 . v0))) ((= (* (* (* (* (C2) v0) (e)) (e)) (A)) (* (* (* (* (C1) (B)) (e)) (e)) v0))))
(40 (instantiate 2 ((v0 . (e))(v1 . (* (e) (* (e) v64)))(v2 . v64))) ((not (= (* (e) (* (e) (* (e) v64))) v64)) (not (= (* v3 v4) v64)) (not (= (* (e) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* (e) (* (e) v64))))))
(41 (instantiate 4 ((v0 . v64))) ((= (* (e) (* (e) (* (e) v64))) v64)))
(42 (resolve 40 (1) 41 (1)) ((not (= (* v3 v4) v64)) (not (= (* (e) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* (e) (* (e) v64))))))
(43 (instantiate 42 ((v3 . v0)(v4 . v1)(v5 . v3)(v6 . v4)(v7 . v5)(v64 . v2))) ((not (= (* v0 v1) v2)) (not (= (* (e) v3) v4)) (not (= (* v5 v1) v4)) (= (* v0 v3) (* v5 (* (e) (* (e) v2))))))
(44 (instantiate 43 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* (e) v3) v4)) (not (= (* v5 v1) v4)) (= (* v0 v3) (* v5 (* (e) (* (e) (* v0 v1)))))))
(45 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(46 (resolve 44 (1) 45 (1)) ((not (= (* (e) v3) v4)) (not (= (* v5 v1) v4)) (= (* v0 v3) (* v5 (* (e) (* (e) (* v0 v1)))))))
(47 (instantiate 46 ((v0 . v4)(v1 . v3)(v3 . v0)(v4 . v1)(v5 . v2))) ((not (= (* (e) v0) v1)) (not (= (* v2 v3) v1)) (= (* v4 v0) (* v2 (* (e) (* (e) (* v4 v3)))))))
(48 (instantiate 47 ((v0 . (* (e) (* (e) v64)))(v1 . v64))) ((not (= (* (e) (* (e) (* (e) v64))) v64)) (not (= (* v2 v3) v64)) (= (* v4 (* (e) (* (e) v64))) (* v2 (* (e) (* (e) (* v4 v3)))))))
(49 (instantiate 4 ((v0 . v64))) ((= (* (e) (* (e) (* (e) v64))) v64)))
(50 (resolve 48 (1) 49 (1)) ((not (= (* v2 v3) v64)) (= (* v4 (* (e) (* (e) v64))) (* v2 (* (e) (* (e) (* v4 v3)))))))
(51 (instantiate 50 ((v2 . v0)(v3 . v1)(v4 . v3)(v64 . v2))) ((not (= (* v0 v1) v2)) (= (* v3 (* (e) (* (e) v2))) (* v0 (* (e) (* (e) (* v3 v1)))))))
(52 (instantiate 51 ((v0 . (* (* v64 (e)) (e)))(v1 . (e))(v2 . v64))) ((not (= (* (* (* v64 (e)) (e)) (e)) v64)) (= (* v3 (* (e) (* (e) v64))) (* (* (* v64 (e)) (e)) (* (e) (* (e) (* v3 (e))))))))
(53 (instantiate 3 ((v0 . v64))) ((= (* (* (* v64 (e)) (e)) (e)) v64)))
(54 (resolve 52 (1) 53 (1)) ((= (* v3 (* (e) (* (e) v64))) (* (* (* v64 (e)) (e)) (* (e) (* (e) (* v3 (e))))))))
(55 (instantiate 54 ((v3 . v0)(v64 . v1))) ((= (* v0 (* (e) (* (e) v1))) (* (* (* v1 (e)) (e)) (* (e) (* (e) (* v0 (e))))))))
(56 (instantiate 2 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v3 v4) (* v0 v1))) (not (= (* v0 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v1))))
(57 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(58 (resolve 56 (1) 57 (1)) ((not (= (* v3 v4) (* v0 v1))) (not (= (* v0 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v1))))
(59 (instantiate 58 ((v0 . v2)(v1 . v3)(v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6))) ((not (= (* v0 v1) (* v2 v3))) (not (= (* v2 v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 v3))))
(60 (instantiate 59 ((v0 . (* (* (* v2 v3) (e)) (e)))(v1 . (e)))) ((not (= (* (* (* (* v2 v3) (e)) (e)) (e)) (* v2 v3))) (not (= (* v2 v4) v5)) (not (= (* v6 (e)) v5)) (= (* (* (* (* v2 v3) (e)) (e)) v4) (* v6 v3))))
(61 (instantiate 3 ((v0 . (* v2 v3)))) ((= (* (* (* (* v2 v3) (e)) (e)) (e)) (* v2 v3))))
(62 (resolve 60 (1) 61 (1)) ((not (= (* v2 v4) v5)) (not (= (* v6 (e)) v5)) (= (* (* (* (* v2 v3) (e)) (e)) v4) (* v6 v3))))
(63 (instantiate 62 ((v2 . v0)(v3 . v4)(v4 . v1)(v5 . v2)(v6 . v3))) ((not (= (* v0 v1) v2)) (not (= (* v3 (e)) v2)) (= (* (* (* (* v0 v4) (e)) (e)) v1) (* v3 v4))))
(64 (instantiate 63 ((v0 . (e))(v1 . (* (e) (* (e) v64)))(v2 . v64))) ((not (= (* (e) (* (e) (* (e) v64))) v64)) (not (= (* v3 (e)) v64)) (= (* (* (* (* (e) v4) (e)) (e)) (* (e) (* (e) v64))) (* v3 v4))))
(65 (instantiate 4 ((v0 . v64))) ((= (* (e) (* (e) (* (e) v64))) v64)))
(66 (resolve 64 (1) 65 (1)) ((not (= (* v3 (e)) v64)) (= (* (* (* (* (e) v4) (e)) (e)) (* (e) (* (e) v64))) (* v3 v4))))
(67 (instantiate 66 ((v3 . v0)(v4 . v2)(v64 . v1))) ((not (= (* v0 (e)) v1)) (= (* (* (* (* (e) v2) (e)) (e)) (* (e) (* (e) v1))) (* v0 v2))))
(68 (instantiate 67 ((v1 . (* v0 (e))))) ((not (= (* v0 (e)) (* v0 (e)))) (= (* (* (* (* (e) v2) (e)) (e)) (* (e) (* (e) (* v0 (e))))) (* v0 v2))))
(69 (instantiate 1 ((v0 . (* v0 (e))))) ((= (* v0 (e)) (* v0 (e)))))
(70 (resolve 68 (1) 69 (1)) ((= (* (* (* (* (e) v2) (e)) (e)) (* (e) (* (e) (* v0 (e))))) (* v0 v2))))
(71 (instantiate 70 ((v0 . v1)(v2 . v0))) ((= (* (* (* (* (e) v0) (e)) (e)) (* (e) (* (e) (* v1 (e))))) (* v1 v0))))
(72 (instantiate 2 ((v0 . (C4))(v1 . (F))(v2 . (* (C3) (E))))) ((not (= (* (C4) (F)) (* (C3) (E)))) (not (= (* v3 v4) (* (C3) (E)))) (not (= (* (C4) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (F)))))
(73 (resolve 72 (1) 7 (1)) ((not (= (* v3 v4) (* (C3) (E)))) (not (= (* (C4) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (F)))))
(74 (instantiate 73 ((v3 . v0)(v4 . v1)(v5 . v2)(v6 . v3)(v7 . v4))) ((not (= (* v0 v1) (* (C3) (E)))) (not (= (* (C4) v2) v3)) (not (= (* v4 v1) v3)) (= (* v0 v2) (* v4 (F)))))
(75 (instantiate 74 ((v0 . (* (* (* (e) (E)) (e)) (e)))(v1 . (* (e) (* (e) (* (C3) (e))))))) ((not (= (* (* (* (* (e) (E)) (e)) (e)) (* (e) (* (e) (* (C3) (e))))) (* (C3) (E)))) (not (= (* (C4) v2) v3)) (not (= (* v4 (* (e) (* (e) (* (C3) (e))))) v3)) (= (* (* (* (* (e) (E)) (e)) (e)) v2) (* v4 (F)))))
(76 (instantiate 71 ((v0 . (E))(v1 . (C3)))) ((= (* (* (* (* (e) (E)) (e)) (e)) (* (e) (* (e) (* (C3) (e))))) (* (C3) (E)))))
(77 (resolve 75 (1) 76 (1)) ((not (= (* (C4) v2) v3)) (not (= (* v4 (* (e) (* (e) (* (C3) (e))))) v3)) (= (* (* (* (* (e) (E)) (e)) (e)) v2) (* v4 (F)))))
(78 (instantiate 77 ((v2 . v0)(v3 . v1)(v4 . v2))) ((not (= (* (C4) v0) v1)) (not (= (* v2 (* (e) (* (e) (* (C3) (e))))) v1)) (= (* (* (* (* (e) (E)) (e)) (e)) v0) (* v2 (F)))))
(79 (instantiate 78 ((v0 . (A))(v1 . (* (C3) (B))))) ((not (= (* (C4) (A)) (* (C3) (B)))) (not (= (* v2 (* (e) (* (e) (* (C3) (e))))) (* (C3) (B)))) (= (* (* (* (* (e) (E)) (e)) (e)) (A)) (* v2 (F)))))
(80 (resolve 79 (1) 5 (1)) ((not (= (* v2 (* (e) (* (e) (* (C3) (e))))) (* (C3) (B)))) (= (* (* (* (* (e) (E)) (e)) (e)) (A)) (* v2 (F)))))
(81 (instantiate 80 ((v2 . v0))) ((not (= (* v0 (* (e) (* (e) (* (C3) (e))))) (* (C3) (B)))) (= (* (* (* (* (e) (E)) (e)) (e)) (A)) (* v0 (F)))))
(82 (instantiate 81 ((v0 . (* (* (* (e) (B)) (e)) (e))))) ((not (= (* (* (* (* (e) (B)) (e)) (e)) (* (e) (* (e) (* (C3) (e))))) (* (C3) (B)))) (= (* (* (* (* (e) (E)) (e)) (e)) (A)) (* (* (* (* (e) (B)) (e)) (e)) (F)))))
(83 (instantiate 71 ((v0 . (B))(v1 . (C3)))) ((= (* (* (* (* (e) (B)) (e)) (e)) (* (e) (* (e) (* (C3) (e))))) (* (C3) (B)))))
(84 (resolve 82 (1) 83 (1)) ((= (* (* (* (* (e) (E)) (e)) (e)) (A)) (* (* (* (* (e) (B)) (e)) (e)) (F)))))
(85 (instantiate 2 ((v0 . (* (* (* (e) v64) (e)) (e)))(v1 . (* (e) (* (e) (* v65 (e)))))(v2 . (* v65 v64)))) ((not (= (* (* (* (* (e) v64) (e)) (e)) (* (e) (* (e) (* v65 (e))))) (* v65 v64))) (not (= (* v3 v4) (* v65 v64))) (not (= (* (* (* (* (e) v64) (e)) (e)) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* (e) (* (e) (* v65 (e))))))))
(86 (instantiate 71 ((v0 . v64)(v1 . v65))) ((= (* (* (* (* (e) v64) (e)) (e)) (* (e) (* (e) (* v65 (e))))) (* v65 v64))))
(87 (resolve 85 (1) 86 (1)) ((not (= (* v3 v4) (* v65 v64))) (not (= (* (* (* (* (e) v64) (e)) (e)) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* (e) (* (e) (* v65 (e))))))))
(88 (instantiate 87 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v3)(v65 . v2))) ((not (= (* v0 v1) (* v2 v3))) (not (= (* (* (* (* (e) v3) (e)) (e)) v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 (* (e) (* (e) (* v2 (e))))))))
(89 (instantiate 88 ((v0 . (* (* (* (C2) v64) (e)) (e)))(v1 . (A))(v2 . (* (* (* (C1) (B)) (e)) (e)))(v3 . v64))) ((not (= (* (* (* (* (C2) v64) (e)) (e)) (A)) (* (* (* (* (C1) (B)) (e)) (e)) v64))) (not (= (* (* (* (* (e) v64) (e)) (e)) v4) v5)) (not (= (* v6 (A)) v5)) (= (* (* (* (* (C2) v64) (e)) (e)) v4) (* v6 (* (e) (* (e) (* (* (* (* (C1) (B)) (e)) (e)) (e))))))))
(90 (instantiate 39 ((v0 . v64))) ((= (* (* (* (* (C2) v64) (e)) (e)) (A)) (* (* (* (* (C1) (B)) (e)) (e)) v64))))
(91 (resolve 89 (1) 90 (1)) ((not (= (* (* (* (* (e) v64) (e)) (e)) v4) v5)) (not (= (* v6 (A)) v5)) (= (* (* (* (* (C2) v64) (e)) (e)) v4) (* v6 (* (e) (* (e) (* (* (* (* (C1) (B)) (e)) (e)) (e))))))))
(92 (instantiate 91 ((v4 . v1)(v5 . v2)(v6 . v3)(v64 . v0))) ((not (= (* (* (* (* (e) v0) (e)) (e)) v1) v2)) (not (= (* v3 (A)) v2)) (= (* (* (* (* (C2) v0) (e)) (e)) v1) (* v3 (* (e) (* (e) (* (* (* (* (C1) (B)) (e)) (e)) (e))))))))
(93 (instantiate 92 ((v0 . v64)(v1 . (* (e) (* (e) (* v65 (e)))))(v2 . (* v65 v64)))) ((not (= (* (* (* (* (e) v64) (e)) (e)) (* (e) (* (e) (* v65 (e))))) (* v65 v64))) (not (= (* v3 (A)) (* v65 v64))) (= (* (* (* (* (C2) v64) (e)) (e)) (* (e) (* (e) (* v65 (e))))) (* v3 (* (e) (* (e) (* (* (* (* (C1) (B)) (e)) (e)) (e))))))))
(94 (instantiate 71 ((v0 . v64)(v1 . v65))) ((= (* (* (* (* (e) v64) (e)) (e)) (* (e) (* (e) (* v65 (e))))) (* v65 v64))))
(95 (resolve 93 (1) 94 (1)) ((not (= (* v3 (A)) (* v65 v64))) (= (* (* (* (* (C2) v64) (e)) (e)) (* (e) (* (e) (* v65 (e))))) (* v3 (* (e) (* (e) (* (* (* (* (C1) (B)) (e)) (e)) (e))))))))
(96 (instantiate 95 ((v3 . v0)(v64 . v2)(v65 . v1))) ((not (= (* v0 (A)) (* v1 v2))) (= (* (* (* (* (C2) v2) (e)) (e)) (* (e) (* (e) (* v1 (e))))) (* v0 (* (e) (* (e) (* (* (* (* (C1) (B)) (e)) (e)) (e))))))))
(97 (instantiate 96 ((v0 . (* (* (* (e) (E)) (e)) (e)))(v1 . (* (* (* (e) (B)) (e)) (e)))(v2 . (F)))) ((not (= (* (* (* (* (e) (E)) (e)) (e)) (A)) (* (* (* (* (e) (B)) (e)) (e)) (F)))) (= (* (* (* (* (C2) (F)) (e)) (e)) (* (e) (* (e) (* (* (* (* (e) (B)) (e)) (e)) (e))))) (* (* (* (* (e) (E)) (e)) (e)) (* (e) (* (e) (* (* (* (* (C1) (B)) (e)) (e)) (e))))))))
(98 (resolve 97 (1) 84 (1)) ((= (* (* (* (* (C2) (F)) (e)) (e)) (* (e) (* (e) (* (* (* (* (e) (B)) (e)) (e)) (e))))) (* (* (* (* (e) (E)) (e)) (e)) (* (e) (* (e) (* (* (* (* (C1) (B)) (e)) (e)) (e))))))))
(99 (instantiate 3 ((v0 . (* (e) (B))))) ((= (* (* (* (* (e) (B)) (e)) (e)) (e)) (* (e) (B)))))
(100 (paramod 99 (1 1) 98 (1 1 2 2 2)) ((= (* (* (* (* (C2) (F)) (e)) (e)) (* (e) (* (e) (* (e) (B))))) (* (* (* (* (e) (E)) (e)) (e)) (* (e) (* (e) (* (* (* (* (C1) (B)) (e)) (e)) (e))))))))
(101 (instantiate 4 ((v0 . (B)))) ((= (* (e) (* (e) (* (e) (B)))) (B))))
(102 (paramod 101 (1 1) 100 (1 1 2)) ((= (* (* (* (* (C2) (F)) (e)) (e)) (B)) (* (* (* (* (e) (E)) (e)) (e)) (* (e) (* (e) (* (* (* (* (C1) (B)) (e)) (e)) (e))))))))
(103 (instantiate 3 ((v0 . (* (C1) (B))))) ((= (* (* (* (* (C1) (B)) (e)) (e)) (e)) (* (C1) (B)))))
(104 (paramod 103 (1 1) 102 (1 2 2 2 2)) ((= (* (* (* (* (C2) (F)) (e)) (e)) (B)) (* (* (* (* (e) (E)) (e)) (e)) (* (e) (* (e) (* (C1) (B))))))))
(105 (flip 104 (1)) ((= (* (* (* (* (e) (E)) (e)) (e)) (* (e) (* (e) (* (C1) (B))))) (* (* (* (* (C2) (F)) (e)) (e)) (B)))))
(106 (instantiate 2 ((v0 . v64)(v1 . (* (e) (* (e) v65)))(v2 . (* (* (* v65 (e)) (e)) (* (e) (* (e) (* v64 (e)))))))) ((not (= (* v64 (* (e) (* (e) v65))) (* (* (* v65 (e)) (e)) (* (e) (* (e) (* v64 (e))))))) (not (= (* v3 v4) (* (* (* v65 (e)) (e)) (* (e) (* (e) (* v64 (e))))))) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* (e) (* (e) v65))))))
(107 (instantiate 55 ((v0 . v64)(v1 . v65))) ((= (* v64 (* (e) (* (e) v65))) (* (* (* v65 (e)) (e)) (* (e) (* (e) (* v64 (e))))))))
(108 (resolve 106 (1) 107 (1)) ((not (= (* v3 v4) (* (* (* v65 (e)) (e)) (* (e) (* (e) (* v64 (e))))))) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* (e) (* (e) v65))))))
(109 (instantiate 108 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v3)(v65 . v2))) ((not (= (* v0 v1) (* (* (* v2 (e)) (e)) (* (e) (* (e) (* v3 (e))))))) (not (= (* v3 v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 (* (e) (* (e) v2))))))
(110 (instantiate 109 ((v0 . (* (* (* (C2) (* (e) (* (e) (* v3 (e))))) (e)) (e)))(v1 . (A))(v2 . (* (C1) (B))))) ((not (= (* (* (* (* (C2) (* (e) (* (e) (* v3 (e))))) (e)) (e)) (A)) (* (* (* (* (C1) (B)) (e)) (e)) (* (e) (* (e) (* v3 (e))))))) (not (= (* v3 v4) v5)) (not (= (* v6 (A)) v5)) (= (* (* (* (* (C2) (* (e) (* (e) (* v3 (e))))) (e)) (e)) v4) (* v6 (* (e) (* (e) (* (C1) (B))))))))
(111 (instantiate 39 ((v0 . (* (e) (* (e) (* v3 (e))))))) ((= (* (* (* (* (C2) (* (e) (* (e) (* v3 (e))))) (e)) (e)) (A)) (* (* (* (* (C1) (B)) (e)) (e)) (* (e) (* (e) (* v3 (e))))))))
(112 (resolve 110 (1) 111 (1)) ((not (= (* v3 v4) v5)) (not (= (* v6 (A)) v5)) (= (* (* (* (* (C2) (* (e) (* (e) (* v3 (e))))) (e)) (e)) v4) (* v6 (* (e) (* (e) (* (C1) (B))))))))
(113 (instantiate 112 ((v3 . v0)(v4 . v1)(v5 . v2)(v6 . v3))) ((not (= (* v0 v1) v2)) (not (= (* v3 (A)) v2)) (= (* (* (* (* (C2) (* (e) (* (e) (* v0 (e))))) (e)) (e)) v1) (* v3 (* (e) (* (e) (* (C1) (B))))))))
(114 (instantiate 113 ((v0 . (* (* (* (e) (E)) (e)) (e)))(v1 . (A))(v2 . (* (* (* (* (e) (B)) (e)) (e)) (F))))) ((not (= (* (* (* (* (e) (E)) (e)) (e)) (A)) (* (* (* (* (e) (B)) (e)) (e)) (F)))) (not (= (* v3 (A)) (* (* (* (* (e) (B)) (e)) (e)) (F)))) (= (* (* (* (* (C2) (* (e) (* (e) (* (* (* (* (e) (E)) (e)) (e)) (e))))) (e)) (e)) (A)) (* v3 (* (e) (* (e) (* (C1) (B))))))))
(115 (resolve 114 (1) 84 (1)) ((not (= (* v3 (A)) (* (* (* (* (e) (B)) (e)) (e)) (F)))) (= (* (* (* (* (C2) (* (e) (* (e) (* (* (* (* (e) (E)) (e)) (e)) (e))))) (e)) (e)) (A)) (* v3 (* (e) (* (e) (* (C1) (B))))))))
(116 (instantiate 115 ((v3 . v0))) ((not (= (* v0 (A)) (* (* (* (* (e) (B)) (e)) (e)) (F)))) (= (* (* (* (* (C2) (* (e) (* (e) (* (* (* (* (e) (E)) (e)) (e)) (e))))) (e)) (e)) (A)) (* v0 (* (e) (* (e) (* (C1) (B))))))))
(117 (instantiate 116 ((v0 . (* (* (* (e) (E)) (e)) (e))))) ((not (= (* (* (* (* (e) (E)) (e)) (e)) (A)) (* (* (* (* (e) (B)) (e)) (e)) (F)))) (= (* (* (* (* (C2) (* (e) (* (e) (* (* (* (* (e) (E)) (e)) (e)) (e))))) (e)) (e)) (A)) (* (* (* (* (e) (E)) (e)) (e)) (* (e) (* (e) (* (C1) (B))))))))
(118 (resolve 117 (1) 84 (1)) ((= (* (* (* (* (C2) (* (e) (* (e) (* (* (* (* (e) (E)) (e)) (e)) (e))))) (e)) (e)) (A)) (* (* (* (* (e) (E)) (e)) (e)) (* (e) (* (e) (* (C1) (B))))))))
(119 (instantiate 3 ((v0 . (* (e) (E))))) ((= (* (* (* (* (e) (E)) (e)) (e)) (e)) (* (e) (E)))))
(120 (paramod 119 (1 1) 118 (1 1 1 1 1 2 2 2)) ((= (* (* (* (* (C2) (* (e) (* (e) (* (e) (E))))) (e)) (e)) (A)) (* (* (* (* (e) (E)) (e)) (e)) (* (e) (* (e) (* (C1) (B))))))))
(121 (instantiate 4 ((v0 . (E)))) ((= (* (e) (* (e) (* (e) (E)))) (E))))
(122 (paramod 121 (1 1) 120 (1 1 1 1 1 2)) ((= (* (* (* (* (C2) (E)) (e)) (e)) (A)) (* (* (* (* (e) (E)) (e)) (e)) (* (e) (* (e) (* (C1) (B))))))))
(123 (instantiate 39 ((v0 . (E)))) ((= (* (* (* (* (C2) (E)) (e)) (e)) (A)) (* (* (* (* (C1) (B)) (e)) (e)) (E)))))
(124 (paramod 123 (1 1) 122 (1 1)) ((= (* (* (* (* (C1) (B)) (e)) (e)) (E)) (* (* (* (* (e) (E)) (e)) (e)) (* (e) (* (e) (* (C1) (B))))))))
(125 (paramod 105 (1 1) 124 (1 2)) ((= (* (* (* (* (C1) (B)) (e)) (e)) (E)) (* (* (* (* (C2) (F)) (e)) (e)) (B)))))
(126 (flip 125 (1)) ((= (* (* (* (* (C2) (F)) (e)) (e)) (B)) (* (* (* (* (C1) (B)) (e)) (e)) (E)))))
(127 (instantiate 2 ((v0 . (* (* v64 (e)) (e)))(v1 . (e))(v2 . v64))) ((not (= (* (* (* v64 (e)) (e)) (e)) v64)) (not (= (* v3 v4) v64)) (not (= (* (* (* v64 (e)) (e)) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (e)))))
(128 (instantiate 3 ((v0 . v64))) ((= (* (* (* v64 (e)) (e)) (e)) v64)))
(129 (resolve 127 (1) 128 (1)) ((not (= (* v3 v4) v64)) (not (= (* (* (* v64 (e)) (e)) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (e)))))
(130 (instantiate 129 ((v3 . v0)(v4 . v1)(v5 . v3)(v6 . v4)(v7 . v5)(v64 . v2))) ((not (= (* v0 v1) v2)) (not (= (* (* (* v2 (e)) (e)) v3) v4)) (not (= (* v5 v1) v4)) (= (* v0 v3) (* v5 (e)))))
(131 (instantiate 130 ((v0 . (* (* (* v64 v65) (e)) (e)))(v1 . v66)(v2 . (* (* (* (* v64 v66) (e)) (e)) v65)))) ((not (= (* (* (* (* v64 v65) (e)) (e)) v66) (* (* (* (* v64 v66) (e)) (e)) v65))) (not (= (* (* (* (* (* (* (* v64 v66) (e)) (e)) v65) (e)) (e)) v3) v4)) (not (= (* v5 v66) v4)) (= (* (* (* (* v64 v65) (e)) (e)) v3) (* v5 (e)))))
(132 (instantiate 24 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (* (* (* (* v64 v65) (e)) (e)) v66) (* (* (* (* v64 v66) (e)) (e)) v65))))
(133 (resolve 131 (1) 132 (1)) ((not (= (* (* (* (* (* (* (* v64 v66) (e)) (e)) v65) (e)) (e)) v3) v4)) (not (= (* v5 v66) v4)) (= (* (* (* (* v64 v65) (e)) (e)) v3) (* v5 (e)))))
(134 (instantiate 133 ((v64 . v0)(v65 . v2)(v66 . v1))) ((not (= (* (* (* (* (* (* (* v0 v1) (e)) (e)) v2) (e)) (e)) v3) v4)) (not (= (* v5 v1) v4)) (= (* (* (* (* v0 v2) (e)) (e)) v3) (* v5 (e)))))
(135 (instantiate 134 ((v3 . (e))(v4 . (* (* (* (* v0 v1) (e)) (e)) v2)))) ((not (= (* (* (* (* (* (* (* v0 v1) (e)) (e)) v2) (e)) (e)) (e)) (* (* (* (* v0 v1) (e)) (e)) v2))) (not (= (* v5 v1) (* (* (* (* v0 v1) (e)) (e)) v2))) (= (* (* (* (* v0 v2) (e)) (e)) (e)) (* v5 (e)))))
(136 (instantiate 3 ((v0 . (* (* (* (* v0 v1) (e)) (e)) v2)))) ((= (* (* (* (* (* (* (* v0 v1) (e)) (e)) v2) (e)) (e)) (e)) (* (* (* (* v0 v1) (e)) (e)) v2))))
(137 (resolve 135 (1) 136 (1)) ((not (= (* v5 v1) (* (* (* (* v0 v1) (e)) (e)) v2))) (= (* (* (* (* v0 v2) (e)) (e)) (e)) (* v5 (e)))))
(138 (instantiate 137 ((v0 . v2)(v2 . v3)(v5 . v0))) ((not (= (* v0 v1) (* (* (* (* v2 v1) (e)) (e)) v3))) (= (* (* (* (* v2 v3) (e)) (e)) (e)) (* v0 (e)))))
(139 (instantiate 138 ((v0 . (* (* (* (C2) (F)) (e)) (e)))(v1 . (B))(v2 . (C1))(v3 . (E)))) ((not (= (* (* (* (* (C2) (F)) (e)) (e)) (B)) (* (* (* (* (C1) (B)) (e)) (e)) (E)))) (= (* (* (* (* (C1) (E)) (e)) (e)) (e)) (* (* (* (* (C2) (F)) (e)) (e)) (e)))))
(140 (resolve 139 (1) 126 (1)) ((= (* (* (* (* (C1) (E)) (e)) (e)) (e)) (* (* (* (* (C2) (F)) (e)) (e)) (e)))))
(141 (instantiate 3 ((v0 . (* (C1) (E))))) ((= (* (* (* (* (C1) (E)) (e)) (e)) (e)) (* (C1) (E)))))
(142 (paramod 141 (1 1) 140 (1 1)) ((= (* (C1) (E)) (* (* (* (* (C2) (F)) (e)) (e)) (e)))))
(143 (instantiate 3 ((v0 . (* (C2) (F))))) ((= (* (* (* (* (C2) (F)) (e)) (e)) (e)) (* (C2) (F)))))
(144 (paramod 143 (1 1) 142 (1 2)) ((= (* (C1) (E)) (* (C2) (F)))))
(145 (flip 144 (1)) ((= (* (C2) (F)) (* (C1) (E)))))
(146 (resolve 8 (1) 145 (1)) ())
)