;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:22:13 1995
;;
;;;;  -> x=x.
;;;; z1*x=u, z2*y=u, z1*z=w, z3*y=w -> z2*z=z3*x.
;;;; B*A=A*B, (A*B)*C=A* (B*C) -> .
;;;;  -> e*x=x.
;;;;  -> x*e=x.
;;
;; -----> EMPTY CLAUSE at   0.55 sec ----> 45 [back_demod,3,demod,32,unit_del,9,8]  -> .
;;
(
(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) ((not (= (* (B) (A)) (* (A) (B)))) (not (= (* (* (A) (B)) (C)) (* (A) (* (B) (C)))))))
(4 (input) ((= (* (e) v0) v0)))
(5 (input) ((= (* v0 (e)) v0)))
(6 (instantiate 2 ((v0 . (e))(v1 . v64)(v2 . v64))) ((not (= (* (e) v64) v64)) (not (= (* v3 v4) v64)) (not (= (* (e) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v64))))
(7 (instantiate 4 ((v0 . v64))) ((= (* (e) v64) v64)))
(8 (resolve 6 (1) 7 (1)) ((not (= (* v3 v4) v64)) (not (= (* (e) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v64))))
(9 (instantiate 8 ((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 v2))))
(10 (instantiate 9 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* (e) v3) v4)) (not (= (* v5 v1) v4)) (= (* v0 v3) (* v5 (* v0 v1)))))
(11 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(12 (resolve 10 (1) 11 (1)) ((not (= (* (e) v3) v4)) (not (= (* v5 v1) v4)) (= (* v0 v3) (* v5 (* v0 v1)))))
(13 (instantiate 12 ((v0 . v4)(v1 . v3)(v3 . v0)(v4 . v1)(v5 . v2))) ((not (= (* (e) v0) v1)) (not (= (* v2 v3) v1)) (= (* v4 v0) (* v2 (* v4 v3)))))
(14 (instantiate 13 ((v0 . v64)(v1 . v64))) ((not (= (* (e) v64) v64)) (not (= (* v2 v3) v64)) (= (* v4 v64) (* v2 (* v4 v3)))))
(15 (instantiate 4 ((v0 . v64))) ((= (* (e) v64) v64)))
(16 (resolve 14 (1) 15 (1)) ((not (= (* v2 v3) v64)) (= (* v4 v64) (* v2 (* v4 v3)))))
(17 (instantiate 16 ((v2 . v0)(v3 . v1)(v4 . v3)(v64 . v2))) ((not (= (* v0 v1) v2)) (= (* v3 v2) (* v0 (* v3 v1)))))
(18 (instantiate 17 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (= (* v3 (* v0 v1)) (* v0 (* v3 v1)))))
(19 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(20 (resolve 18 (1) 19 (1)) ((= (* v3 (* v0 v1)) (* v0 (* v3 v1)))))
(21 (instantiate 20 ((v0 . v1)(v1 . v2)(v3 . v0))) ((= (* v0 (* v1 v2)) (* v1 (* v0 v2)))))
(22 (instantiate 2 ((v0 . (e))(v1 . v64)(v2 . v64))) ((not (= (* (e) v64) v64)) (not (= (* v3 v4) v64)) (not (= (* (e) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v64))))
(23 (instantiate 4 ((v0 . v64))) ((= (* (e) v64) v64)))
(24 (resolve 22 (1) 23 (1)) ((not (= (* v3 v4) v64)) (not (= (* (e) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v64))))
(25 (instantiate 24 ((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 v2))))
(26 (instantiate 25 ((v0 . v64)(v1 . (e))(v2 . v64))) ((not (= (* v64 (e)) v64)) (not (= (* (e) v3) v4)) (not (= (* v5 (e)) v4)) (= (* v64 v3) (* v5 v64))))
(27 (instantiate 5 ((v0 . v64))) ((= (* v64 (e)) v64)))
(28 (resolve 26 (1) 27 (1)) ((not (= (* (e) v3) v4)) (not (= (* v5 (e)) v4)) (= (* v64 v3) (* v5 v64))))
(29 (instantiate 28 ((v3 . v0)(v4 . v1)(v5 . v2)(v64 . v3))) ((not (= (* (e) v0) v1)) (not (= (* v2 (e)) v1)) (= (* v3 v0) (* v2 v3))))
(30 (instantiate 29 ((v0 . v64)(v1 . v64))) ((not (= (* (e) v64) v64)) (not (= (* v2 (e)) v64)) (= (* v3 v64) (* v2 v3))))
(31 (instantiate 4 ((v0 . v64))) ((= (* (e) v64) v64)))
(32 (resolve 30 (1) 31 (1)) ((not (= (* v2 (e)) v64)) (= (* v3 v64) (* v2 v3))))
(33 (instantiate 32 ((v2 . v0)(v3 . v2)(v64 . v1))) ((not (= (* v0 (e)) v1)) (= (* v2 v1) (* v0 v2))))
(34 (instantiate 33 ((v0 . v64)(v1 . v64))) ((not (= (* v64 (e)) v64)) (= (* v2 v64) (* v64 v2))))
(35 (instantiate 5 ((v0 . v64))) ((= (* v64 (e)) v64)))
(36 (resolve 34 (1) 35 (1)) ((= (* v2 v64) (* v64 v2))))
(37 (instantiate 36 ((v2 . v0)(v64 . v1))) ((= (* v0 v1) (* v1 v0))))
(38 (instantiate 2 ((v0 . v64)(v1 . (e))(v2 . v64))) ((not (= (* v64 (e)) v64)) (not (= (* v3 v4) v64)) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (e)))))
(39 (instantiate 5 ((v0 . v64))) ((= (* v64 (e)) v64)))
(40 (resolve 38 (1) 39 (1)) ((not (= (* v3 v4) v64)) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (e)))))
(41 (instantiate 40 ((v3 . v0)(v4 . v1)(v5 . v3)(v6 . v4)(v7 . v5)(v64 . v2))) ((not (= (* v0 v1) v2)) (not (= (* v2 v3) v4)) (not (= (* v5 v1) v4)) (= (* v0 v3) (* v5 (e)))))
(42 (instantiate 41 ((v0 . v64)(v1 . v65)(v2 . (* v65 v64)))) ((not (= (* v64 v65) (* v65 v64))) (not (= (* (* v65 v64) v3) v4)) (not (= (* v5 v65) v4)) (= (* v64 v3) (* v5 (e)))))
(43 (instantiate 37 ((v0 . v64)(v1 . v65))) ((= (* v64 v65) (* v65 v64))))
(44 (resolve 42 (1) 43 (1)) ((not (= (* (* v65 v64) v3) v4)) (not (= (* v5 v65) v4)) (= (* v64 v3) (* v5 (e)))))
(45 (instantiate 44 ((v3 . v2)(v4 . v3)(v5 . v4)(v64 . v1)(v65 . v0))) ((not (= (* (* v0 v1) v2) v3)) (not (= (* v4 v0) v3)) (= (* v1 v2) (* v4 (e)))))
(46 (instantiate 45 ((v2 . (* v65 v66))(v3 . (* v65 (* (* v0 v1) v66))))) ((not (= (* (* v0 v1) (* v65 v66)) (* v65 (* (* v0 v1) v66)))) (not (= (* v4 v0) (* v65 (* (* v0 v1) v66)))) (= (* v1 (* v65 v66)) (* v4 (e)))))
(47 (instantiate 21 ((v0 . (* v0 v1))(v1 . v65)(v2 . v66))) ((= (* (* v0 v1) (* v65 v66)) (* v65 (* (* v0 v1) v66)))))
(48 (resolve 46 (1) 47 (1)) ((not (= (* v4 v0) (* v65 (* (* v0 v1) v66)))) (= (* v1 (* v65 v66)) (* v4 (e)))))
(49 (instantiate 48 ((v0 . v1)(v1 . v3)(v4 . v0)(v65 . v2)(v66 . v4))) ((not (= (* v0 v1) (* v2 (* (* v1 v3) v4)))) (= (* v3 (* v2 v4)) (* v0 (e)))))
(50 (instantiate 49 ((v0 . (* (* v65 v3) v4))(v1 . v65)(v2 . v65))) ((not (= (* (* (* v65 v3) v4) v65) (* v65 (* (* v65 v3) v4)))) (= (* v3 (* v65 v4)) (* (* (* v65 v3) v4) (e)))))
(51 (instantiate 37 ((v0 . (* (* v65 v3) v4))(v1 . v65))) ((= (* (* (* v65 v3) v4) v65) (* v65 (* (* v65 v3) v4)))))
(52 (resolve 50 (1) 51 (1)) ((= (* v3 (* v65 v4)) (* (* (* v65 v3) v4) (e)))))
(53 (instantiate 52 ((v3 . v0)(v4 . v2)(v65 . v1))) ((= (* v0 (* v1 v2)) (* (* (* v1 v0) v2) (e)))))
(54 (instantiate 5 ((v0 . (* (* v1 v0) v2)))) ((= (* (* (* v1 v0) v2) (e)) (* (* v1 v0) v2))))
(55 (paramod 54 (1 1) 53 (1 2)) ((= (* v0 (* v1 v2)) (* (* v1 v0) v2))))
(56 (flip 55 (1)) ((= (* (* v1 v0) v2) (* v0 (* v1 v2)))))
(57 (instantiate 56 ((v0 . v1)(v1 . v0))) ((= (* (* v0 v1) v2) (* v1 (* v0 v2)))))
(58 (instantiate 57 ((v0 . (A))(v1 . (B))(v2 . (C)))) ((= (* (* (A) (B)) (C)) (* (B) (* (A) (C))))))
(59 (paramod 58 (1 1) 3 (2 1 1)) ((not (= (* (B) (A)) (* (A) (B)))) (not (= (* (B) (* (A) (C))) (* (A) (* (B) (C)))))))
(60 (instantiate 37 ((v0 . (B))(v1 . (A)))) ((= (* (B) (A)) (* (A) (B)))))
(61 (resolve 59 (1) 60 (1)) ((not (= (* (B) (* (A) (C))) (* (A) (* (B) (C)))))))
(62 (instantiate 21 ((v0 . (B))(v1 . (A))(v2 . (C)))) ((= (* (B) (* (A) (C))) (* (A) (* (B) (C))))))
(63 (resolve 61 (1) 62 (1)) ())
)