;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:17:22 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*x=x.
;;;;  -> x*y=y*x.
;;;;  -> (x*y)*z=x* (y*z).
;;;; B=A -> .
;;
;; ----> UNIT CONFLICT at   0.55 sec ----> 18 [binary,17.1,8.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 v0) v0)))
(4 (input) ((= (* v0 v1) (* v1 v0))))
(5 (input) ((= (* (* v0 v1) v2) (* v0 (* v1 v2)))))
(6 (input) ((not (= (B) (A)))))
(7 (instantiate 2 ((v0 . v64)(v1 . v65)(v2 . (* v65 v64)))) ((not (= (* v64 v65) (* v65 v64))) (not (= (* v3 v4) (* v65 v64))) (not (= (* v5 v65) v6)) (not (= (* v7 v4) v6)) (not (= (* v64 v8) v9)) (not (= (* v3 v10) v9)) (= (* v5 v8) (* v7 v10))))
(8 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (* v64 v65) (* v65 v64))))
(9 (resolve 7 (1) 8 (1)) ((not (= (* v3 v4) (* v65 v64))) (not (= (* v5 v65) v6)) (not (= (* v7 v4) v6)) (not (= (* v64 v8) v9)) (not (= (* v3 v10) v9)) (= (* v5 v8) (* v7 v10))))
(10 (instantiate 9 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v8 . v7)(v9 . v8)(v10 . v9)(v64 . v3)(v65 . v2))) ((not (= (* v0 v1) (* v2 v3))) (not (= (* v4 v2) v5)) (not (= (* v6 v1) v5)) (not (= (* v3 v7) v8)) (not (= (* v0 v9) v8)) (= (* v4 v7) (* v6 v9))))
(11 (instantiate 10 ((v0 . (* v2 v3))(v1 . (* v2 v3)))) ((not (= (* (* v2 v3) (* v2 v3)) (* v2 v3))) (not (= (* v4 v2) v5)) (not (= (* v6 (* v2 v3)) v5)) (not (= (* v3 v7) v8)) (not (= (* (* v2 v3) v9) v8)) (= (* v4 v7) (* v6 v9))))
(12 (instantiate 3 ((v0 . (* v2 v3)))) ((= (* (* v2 v3) (* v2 v3)) (* v2 v3))))
(13 (resolve 11 (1) 12 (1)) ((not (= (* v4 v2) v5)) (not (= (* v6 (* v2 v3)) v5)) (not (= (* v3 v7) v8)) (not (= (* (* v2 v3) v9) v8)) (= (* v4 v7) (* v6 v9))))
(14 (instantiate 13 ((v2 . v1)(v3 . v4)(v4 . v0)(v5 . v2)(v6 . v3)(v7 . v5)(v8 . v6)(v9 . v7))) ((not (= (* v0 v1) v2)) (not (= (* v3 (* v1 v4)) v2)) (not (= (* v4 v5) v6)) (not (= (* (* v1 v4) v7) v6)) (= (* v0 v5) (* v3 v7))))
(15 (instantiate 14 ((v0 . v64)(v1 . v65)(v2 . (* v65 v64)))) ((not (= (* v64 v65) (* v65 v64))) (not (= (* v3 (* v65 v4)) (* v65 v64))) (not (= (* v4 v5) v6)) (not (= (* (* v65 v4) v7) v6)) (= (* v64 v5) (* v3 v7))))
(16 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (* v64 v65) (* v65 v64))))
(17 (resolve 15 (1) 16 (1)) ((not (= (* v3 (* v65 v4)) (* v65 v64))) (not (= (* v4 v5) v6)) (not (= (* (* v65 v4) v7) v6)) (= (* v64 v5) (* v3 v7))))
(18 (instantiate 17 ((v3 . v0)(v4 . v2)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v3)(v65 . v1))) ((not (= (* v0 (* v1 v2)) (* v1 v3))) (not (= (* v2 v4) v5)) (not (= (* (* v1 v2) v6) v5)) (= (* v3 v4) (* v0 v6))))
(19 (instantiate 18 ((v0 . (* v1 v2))(v3 . v2))) ((not (= (* (* v1 v2) (* v1 v2)) (* v1 v2))) (not (= (* v2 v4) v5)) (not (= (* (* v1 v2) v6) v5)) (= (* v2 v4) (* (* v1 v2) v6))))
(20 (instantiate 3 ((v0 . (* v1 v2)))) ((= (* (* v1 v2) (* v1 v2)) (* v1 v2))))
(21 (resolve 19 (1) 20 (1)) ((not (= (* v2 v4) v5)) (not (= (* (* v1 v2) v6) v5)) (= (* v2 v4) (* (* v1 v2) v6))))
(22 (instantiate 21 ((v1 . v3)(v2 . v0)(v4 . v1)(v5 . v2)(v6 . v4))) ((not (= (* v0 v1) v2)) (not (= (* (* v3 v0) v4) v2)) (= (* v0 v1) (* (* v3 v0) v4))))
(23 (instantiate 22 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* (* v3 v0) v4) (* v0 v1))) (= (* v0 v1) (* (* v3 v0) v4))))
(24 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(25 (resolve 23 (1) 24 (1)) ((not (= (* (* v3 v0) v4) (* v0 v1))) (= (* v0 v1) (* (* v3 v0) v4))))
(26 (instantiate 25 ((v0 . v1)(v1 . v3)(v3 . v0)(v4 . v2))) ((not (= (* (* v0 v1) v2) (* v1 v3))) (= (* v1 v3) (* (* v0 v1) v2))))
(27 (instantiate 26 ((v1 . v65)(v2 . v65)(v3 . (* v0 v65)))) ((not (= (* (* v0 v65) v65) (* v65 (* v0 v65)))) (= (* v65 (* v0 v65)) (* (* v0 v65) v65))))
(28 (instantiate 4 ((v0 . (* v0 v65))(v1 . v65))) ((= (* (* v0 v65) v65) (* v65 (* v0 v65)))))
(29 (resolve 27 (1) 28 (1)) ((= (* v65 (* v0 v65)) (* (* v0 v65) v65))))
(30 (instantiate 29 ((v0 . v1)(v65 . v0))) ((= (* v0 (* v1 v0)) (* (* v1 v0) v0))))
(31 (instantiate 5 ((v0 . v1)(v1 . v0)(v2 . v0))) ((= (* (* v1 v0) v0) (* v1 (* v0 v0)))))
(32 (paramod 31 (1 1) 30 (1 2)) ((= (* v0 (* v1 v0)) (* v1 (* v0 v0)))))
(33 (paramod 3 (1 1) 32 (1 2 2)) ((= (* v0 (* v1 v0)) (* v1 v0))))
(34 (instantiate 2 ((v0 . v64)(v1 . (* v65 v64))(v2 . (* v65 v64)))) ((not (= (* v64 (* v65 v64)) (* v65 v64))) (not (= (* v3 v4) (* v65 v64))) (not (= (* v5 (* v65 v64)) v6)) (not (= (* v7 v4) v6)) (not (= (* v64 v8) v9)) (not (= (* v3 v10) v9)) (= (* v5 v8) (* v7 v10))))
(35 (instantiate 33 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) (* v65 v64))))
(36 (resolve 34 (1) 35 (1)) ((not (= (* v3 v4) (* v65 v64))) (not (= (* v5 (* v65 v64)) v6)) (not (= (* v7 v4) v6)) (not (= (* v64 v8) v9)) (not (= (* v3 v10) v9)) (= (* v5 v8) (* v7 v10))))
(37 (instantiate 36 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v8 . v7)(v9 . v8)(v10 . v9)(v64 . v3)(v65 . v2))) ((not (= (* v0 v1) (* v2 v3))) (not (= (* v4 (* v2 v3)) v5)) (not (= (* v6 v1) v5)) (not (= (* v3 v7) v8)) (not (= (* v0 v9) v8)) (= (* v4 v7) (* v6 v9))))
(38 (instantiate 37 ((v0 . v64)(v1 . (* v65 v64))(v2 . v65)(v3 . v64))) ((not (= (* v64 (* v65 v64)) (* v65 v64))) (not (= (* v4 (* v65 v64)) v5)) (not (= (* v6 (* v65 v64)) v5)) (not (= (* v64 v7) v8)) (not (= (* v64 v9) v8)) (= (* v4 v7) (* v6 v9))))
(39 (instantiate 33 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) (* v65 v64))))
(40 (resolve 38 (1) 39 (1)) ((not (= (* v4 (* v65 v64)) v5)) (not (= (* v6 (* v65 v64)) v5)) (not (= (* v64 v7) v8)) (not (= (* v64 v9) v8)) (= (* v4 v7) (* v6 v9))))
(41 (instantiate 40 ((v4 . v0)(v5 . v3)(v6 . v4)(v7 . v5)(v8 . v6)(v9 . v7)(v64 . v2)(v65 . v1))) ((not (= (* v0 (* v1 v2)) v3)) (not (= (* v4 (* v1 v2)) v3)) (not (= (* v2 v5) v6)) (not (= (* v2 v7) v6)) (= (* v0 v5) (* v4 v7))))
(42 (instantiate 41 ((v0 . v64)(v1 . v65)(v2 . v64)(v3 . (* v65 v64)))) ((not (= (* v64 (* v65 v64)) (* v65 v64))) (not (= (* v4 (* v65 v64)) (* v65 v64))) (not (= (* v64 v5) v6)) (not (= (* v64 v7) v6)) (= (* v64 v5) (* v4 v7))))
(43 (instantiate 33 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) (* v65 v64))))
(44 (resolve 42 (1) 43 (1)) ((not (= (* v4 (* v65 v64)) (* v65 v64))) (not (= (* v64 v5) v6)) (not (= (* v64 v7) v6)) (= (* v64 v5) (* v4 v7))))
(45 (instantiate 44 ((v4 . v0)(v5 . v3)(v6 . v4)(v7 . v5)(v64 . v2)(v65 . v1))) ((not (= (* v0 (* v1 v2)) (* v1 v2))) (not (= (* v2 v3) v4)) (not (= (* v2 v5) v4)) (= (* v2 v3) (* v0 v5))))
(46 (instantiate 45 ((v0 . (* v1 v2)))) ((not (= (* (* v1 v2) (* v1 v2)) (* v1 v2))) (not (= (* v2 v3) v4)) (not (= (* v2 v5) v4)) (= (* v2 v3) (* (* v1 v2) v5))))
(47 (instantiate 3 ((v0 . (* v1 v2)))) ((= (* (* v1 v2) (* v1 v2)) (* v1 v2))))
(48 (resolve 46 (1) 47 (1)) ((not (= (* v2 v3) v4)) (not (= (* v2 v5) v4)) (= (* v2 v3) (* (* v1 v2) v5))))
(49 (instantiate 48 ((v1 . v4)(v2 . v0)(v3 . v1)(v4 . v2)(v5 . v3))) ((not (= (* v0 v1) v2)) (not (= (* v0 v3) v2)) (= (* v0 v1) (* (* v4 v0) v3))))
(50 (instantiate 49 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v0 v3) (* v0 v1))) (= (* v0 v1) (* (* v4 v0) v3))))
(51 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(52 (resolve 50 (1) 51 (1)) ((not (= (* v0 v3) (* v0 v1))) (= (* v0 v1) (* (* v4 v0) v3))))
(53 (instantiate 52 ((v1 . v2)(v3 . v1)(v4 . v3))) ((not (= (* v0 v1) (* v0 v2))) (= (* v0 v2) (* (* v3 v0) v1))))
(54 (instantiate 53 ((v0 . v65)(v1 . (* v65 v65))(v2 . v65))) ((not (= (* v65 (* v65 v65)) (* v65 v65))) (= (* v65 v65) (* (* v3 v65) (* v65 v65)))))
(55 (instantiate 33 ((v0 . v65)(v1 . v65))) ((= (* v65 (* v65 v65)) (* v65 v65))))
(56 (resolve 54 (1) 55 (1)) ((= (* v65 v65) (* (* v3 v65) (* v65 v65)))))
(57 (instantiate 56 ((v3 . v1)(v65 . v0))) ((= (* v0 v0) (* (* v1 v0) (* v0 v0)))))
(58 (paramod 3 (1 1) 57 (1 1)) ((= v0 (* (* v1 v0) (* v0 v0)))))
(59 (paramod 3 (1 1) 58 (1 2 2)) ((= v0 (* (* v1 v0) v0))))
(60 (instantiate 5 ((v0 . v1)(v1 . v0)(v2 . v0))) ((= (* (* v1 v0) v0) (* v1 (* v0 v0)))))
(61 (paramod 60 (1 1) 59 (1 2)) ((= v0 (* v1 (* v0 v0)))))
(62 (paramod 3 (1 1) 61 (1 2 2)) ((= v0 (* v1 v0))))
(63 (flip 62 (1)) ((= (* v1 v0) v0)))
(64 (instantiate 63 ((v0 . v1)(v1 . v0))) ((= (* v0 v1) v1)))
(65 (instantiate 2 ((v0 . v64)(v1 . (* v65 v64))(v2 . (* v65 v64)))) ((not (= (* v64 (* v65 v64)) (* v65 v64))) (not (= (* v3 v4) (* v65 v64))) (not (= (* v5 (* v65 v64)) v6)) (not (= (* v7 v4) v6)) (not (= (* v64 v8) v9)) (not (= (* v3 v10) v9)) (= (* v5 v8) (* v7 v10))))
(66 (instantiate 33 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) (* v65 v64))))
(67 (resolve 65 (1) 66 (1)) ((not (= (* v3 v4) (* v65 v64))) (not (= (* v5 (* v65 v64)) v6)) (not (= (* v7 v4) v6)) (not (= (* v64 v8) v9)) (not (= (* v3 v10) v9)) (= (* v5 v8) (* v7 v10))))
(68 (instantiate 67 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v8 . v7)(v9 . v8)(v10 . v9)(v64 . v3)(v65 . v2))) ((not (= (* v0 v1) (* v2 v3))) (not (= (* v4 (* v2 v3)) v5)) (not (= (* v6 v1) v5)) (not (= (* v3 v7) v8)) (not (= (* v0 v9) v8)) (= (* v4 v7) (* v6 v9))))
(69 (instantiate 68 ((v0 . v64)(v1 . (* v65 v64))(v2 . v65)(v3 . v64))) ((not (= (* v64 (* v65 v64)) (* v65 v64))) (not (= (* v4 (* v65 v64)) v5)) (not (= (* v6 (* v65 v64)) v5)) (not (= (* v64 v7) v8)) (not (= (* v64 v9) v8)) (= (* v4 v7) (* v6 v9))))
(70 (instantiate 33 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) (* v65 v64))))
(71 (resolve 69 (1) 70 (1)) ((not (= (* v4 (* v65 v64)) v5)) (not (= (* v6 (* v65 v64)) v5)) (not (= (* v64 v7) v8)) (not (= (* v64 v9) v8)) (= (* v4 v7) (* v6 v9))))
(72 (instantiate 71 ((v4 . v0)(v5 . v3)(v6 . v4)(v7 . v5)(v8 . v6)(v9 . v7)(v64 . v2)(v65 . v1))) ((not (= (* v0 (* v1 v2)) v3)) (not (= (* v4 (* v1 v2)) v3)) (not (= (* v2 v5) v6)) (not (= (* v2 v7) v6)) (= (* v0 v5) (* v4 v7))))
(73 (instantiate 72 ((v0 . v64)(v3 . (* (* v1 v2) v64)))) ((not (= (* v64 (* v1 v2)) (* (* v1 v2) v64))) (not (= (* v4 (* v1 v2)) (* (* v1 v2) v64))) (not (= (* v2 v5) v6)) (not (= (* v2 v7) v6)) (= (* v64 v5) (* v4 v7))))
(74 (instantiate 4 ((v0 . v64)(v1 . (* v1 v2)))) ((= (* v64 (* v1 v2)) (* (* v1 v2) v64))))
(75 (resolve 73 (1) 74 (1)) ((not (= (* v4 (* v1 v2)) (* (* v1 v2) v64))) (not (= (* v2 v5) v6)) (not (= (* v2 v7) v6)) (= (* v64 v5) (* v4 v7))))
(76 (instantiate 75 ((v4 . v0)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v3))) ((not (= (* v0 (* v1 v2)) (* (* v1 v2) v3))) (not (= (* v2 v4) v5)) (not (= (* v2 v6) v5)) (= (* v3 v4) (* v0 v6))))
(77 (instantiate 76 ((v0 . v64)(v3 . v64))) ((not (= (* v64 (* v1 v2)) (* (* v1 v2) v64))) (not (= (* v2 v4) v5)) (not (= (* v2 v6) v5)) (= (* v64 v4) (* v64 v6))))
(78 (instantiate 4 ((v0 . v64)(v1 . (* v1 v2)))) ((= (* v64 (* v1 v2)) (* (* v1 v2) v64))))
(79 (resolve 77 (1) 78 (1)) ((not (= (* v2 v4) v5)) (not (= (* v2 v6) v5)) (= (* v64 v4) (* v64 v6))))
(80 (instantiate 79 ((v2 . v0)(v4 . v1)(v5 . v2)(v6 . v3)(v64 . v4))) ((not (= (* v0 v1) v2)) (not (= (* v0 v3) v2)) (= (* v4 v1) (* v4 v3))))
(81 (instantiate 80 ((v0 . v64)(v1 . v65)(v2 . (* v65 v64)))) ((not (= (* v64 v65) (* v65 v64))) (not (= (* v64 v3) (* v65 v64))) (= (* v4 v65) (* v4 v3))))
(82 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (* v64 v65) (* v65 v64))))
(83 (resolve 81 (1) 82 (1)) ((not (= (* v64 v3) (* v65 v64))) (= (* v4 v65) (* v4 v3))))
(84 (instantiate 83 ((v3 . v1)(v4 . v3)(v64 . v0)(v65 . v2))) ((not (= (* v0 v1) (* v2 v0))) (= (* v3 v2) (* v3 v1))))
(85 (instantiate 84 ((v0 . v64)(v1 . (* v65 v64))(v2 . v65))) ((not (= (* v64 (* v65 v64)) (* v65 v64))) (= (* v3 v65) (* v3 (* v65 v64)))))
(86 (instantiate 33 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) (* v65 v64))))
(87 (resolve 85 (1) 86 (1)) ((= (* v3 v65) (* v3 (* v65 v64)))))
(88 (instantiate 87 ((v3 . v0)(v64 . v2)(v65 . v1))) ((= (* v0 v1) (* v0 (* v1 v2)))))
(89 (paramod 64 (1 1) 88 (1 1)) ((= v1 (* v0 (* v1 v2)))))
(90 (instantiate 64 ((v0 . v1)(v1 . v2))) ((= (* v1 v2) v2)))
(91 (paramod 90 (1 1) 89 (1 2 2)) ((= v1 (* v0 v2))))
(92 (instantiate 64 ((v0 . v0)(v1 . v2))) ((= (* v0 v2) v2)))
(93 (paramod 92 (1 1) 91 (1 2)) ((= v1 v2)))
(94 (instantiate 93 ((v1 . v0)(v2 . v1))) ((= v0 v1)))
(95 (instantiate 94 ((v0 . (B))(v1 . (A)))) ((= (B) (A))))
(96 (resolve 6 (1) 95 (1)) ())
)