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