;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:18:21 1995
;;
;;;;  -> x=x.
;;;; p(A,A,B)=A, p(A,B,A)=A, p(B,A,A)=A, f(A)=A -> .
;;;;  -> p(p(x,y,y),u,p(p(x,y,y),f(y),z))=y.
;;
;; -----> EMPTY CLAUSE at   0.09 sec ----> 25 [back_demod,18,demod,24,22,unit_del,1,1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((not (= (p (A) (A) (B)) (A))) (not (= (p (A) (B) (A)) (A))) (not (= (p (B) (A) (A)) (A))) (not (= (f (A)) (A)))))
(3 (input) ((= (p (p v0 v1 v1) v2 (p (p v0 v1 v1) (f v1) v3)) v1)))
(4 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . (f v65)))) ((= (p (p v64 v65 v65) (f v65) (p (p v64 v65 v65) (f v65) v3)) v65)))
(5 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . (p (p v64 v65 v65) (f v65) v3)))) ((= (p (p v64 v65 v65) v66 (p (p v64 v65 v65) (f v65) (p (p v64 v65 v65) (f v65) v3))) v65)))
(6 (paramod 4 (1 1) 5 (1 1 3)) ((= (p (p v64 v65 v65) v66 v65) v65)))
(7 (instantiate 6 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (p (p v0 v1 v1) v2 v1) v1)))
(8 (instantiate 7 ((v1 . v65)(v2 . v65))) ((= (p (p v0 v65 v65) v65 v65) v65)))
(9 (instantiate 7 ((v0 . (p v0 v65 v65))(v1 . v65)(v2 . v66))) ((= (p (p (p v0 v65 v65) v65 v65) v66 v65) v65)))
(10 (paramod 8 (1 1) 9 (1 1 1)) ((= (p v65 v66 v65) v65)))
(11 (instantiate 10 ((v65 . v0)(v66 . v1))) ((= (p v0 v1 v0) v0)))
(12 (instantiate 3 ((v2 . (p (p v0 v1 v1) (f v1) v3)))) ((= (p (p v0 v1 v1) (p (p v0 v1 v1) (f v1) v3) (p (p v0 v1 v1) (f v1) v3)) v1)))
(13 (instantiate 7 ((v0 . (p v0 v1 v1))(v1 . (p (p v0 v1 v1) (f v1) v3))(v2 . v66))) ((= (p (p (p v0 v1 v1) (p (p v0 v1 v1) (f v1) v3) (p (p v0 v1 v1) (f v1) v3)) v66 (p (p v0 v1 v1) (f v1) v3)) (p (p v0 v1 v1) (f v1) v3))))
(14 (paramod 12 (1 1) 13 (1 1 1)) ((= (p v1 v66 (p (p v0 v1 v1) (f v1) v3)) (p (p v0 v1 v1) (f v1) v3))))
(15 (instantiate 14 ((v0 . v2)(v1 . v0)(v66 . v1))) ((= (p v0 v1 (p (p v2 v0 v0) (f v0) v3)) (p (p v2 v0 v0) (f v0) v3))))
(16 (instantiate 11 ((v0 . (A))(v1 . (B)))) ((= (p (A) (B) (A)) (A))))
(17 (paramod 16 (1 1) 2 (2 1 1)) ((not (= (p (A) (A) (B)) (A))) (not (= (A) (A))) (not (= (p (B) (A) (A)) (A))) (not (= (f (A)) (A)))))
(18 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(19 (resolve 17 (2) 18 (1)) ((not (= (p (A) (A) (B)) (A))) (not (= (p (B) (A) (A)) (A))) (not (= (f (A)) (A)))))
(20 (instantiate 7 ((v1 . v65)(v2 . v65))) ((= (p (p v0 v65 v65) v65 v65) v65)))
(21 (instantiate 3 ((v0 . (p v0 v65 v65))(v1 . v65)(v2 . v66)(v3 . v67))) ((= (p (p (p v0 v65 v65) v65 v65) v66 (p (p (p v0 v65 v65) v65 v65) (f v65) v67)) v65)))
(22 (paramod 20 (1 1) 21 (1 1 3 1)) ((= (p (p (p v0 v65 v65) v65 v65) v66 (p v65 (f v65) v67)) v65)))
(23 (instantiate 7 ((v0 . v0)(v1 . v65)(v2 . v65))) ((= (p (p v0 v65 v65) v65 v65) v65)))
(24 (paramod 23 (1 1) 22 (1 1 1)) ((= (p v65 v66 (p v65 (f v65) v67)) v65)))
(25 (instantiate 24 ((v65 . v0)(v66 . v1)(v67 . v2))) ((= (p v0 v1 (p v0 (f v0) v2)) v0)))
(26 (instantiate 11 ((v0 . (p v64 v65 v65))(v1 . (f v65)))) ((= (p (p v64 v65 v65) (f v65) (p v64 v65 v65)) (p v64 v65 v65))))
(27 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . (p v64 v65 v65)))) ((= (p (p v64 v65 v65) v66 (p (p v64 v65 v65) (f v65) (p v64 v65 v65))) v65)))
(28 (paramod 26 (1 1) 27 (1 1 3)) ((= (p (p v64 v65 v65) v66 (p v64 v65 v65)) v65)))
(29 (instantiate 11 ((v0 . (p v64 v65 v65))(v1 . v66))) ((= (p (p v64 v65 v65) v66 (p v64 v65 v65)) (p v64 v65 v65))))
(30 (paramod 29 (1 1) 28 (1 1)) ((= (p v64 v65 v65) v65)))
(31 (instantiate 30 ((v64 . v0)(v65 . v1))) ((= (p v0 v1 v1) v1)))
(32 (instantiate 31 ((v0 . (B))(v1 . (A)))) ((= (p (B) (A) (A)) (A))))
(33 (paramod 32 (1 1) 19 (2 1 1)) ((not (= (p (A) (A) (B)) (A))) (not (= (A) (A))) (not (= (f (A)) (A)))))
(34 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(35 (resolve 33 (2) 34 (1)) ((not (= (p (A) (A) (B)) (A))) (not (= (f (A)) (A)))))
(36 (instantiate 31 ((v0 . v2)(v1 . v0))) ((= (p v2 v0 v0) v0)))
(37 (paramod 36 (1 1) 15 (1 1 3 1)) ((= (p v0 v1 (p v0 (f v0) v3)) (p (p v2 v0 v0) (f v0) v3))))
(38 (instantiate 25 ((v0 . v0)(v1 . v1)(v2 . v3))) ((= (p v0 v1 (p v0 (f v0) v3)) v0)))
(39 (paramod 38 (1 1) 37 (1 1)) ((= v0 (p (p v2 v0 v0) (f v0) v3))))
(40 (instantiate 31 ((v0 . v2)(v1 . v0))) ((= (p v2 v0 v0) v0)))
(41 (paramod 40 (1 1) 39 (1 2 1)) ((= v0 (p v0 (f v0) v3))))
(42 (flip 41 (1)) ((= (p v0 (f v0) v3) v0)))
(43 (instantiate 42 ((v3 . v1))) ((= (p v0 (f v0) v1) v0)))
(44 (instantiate 31 ((v0 . v64)(v1 . (f v64)))) ((= (p v64 (f v64) (f v64)) (f v64))))
(45 (instantiate 43 ((v0 . v64)(v1 . (f v64)))) ((= (p v64 (f v64) (f v64)) v64)))
(46 (paramod 44 (1 1) 45 (1 1)) ((= (f v64) v64)))
(47 (instantiate 46 ((v64 . v0))) ((= (f v0) v0)))
(48 (paramod 47 (1 1) 43 (1 1 2)) ((= (p v0 v0 v1) v0)))
(49 (instantiate 48 ((v0 . (A))(v1 . (B)))) ((= (p (A) (A) (B)) (A))))
(50 (paramod 49 (1 1) 35 (1 1 1)) ((not (= (A) (A))) (not (= (f (A)) (A)))))
(51 (instantiate 47 ((v0 . (A)))) ((= (f (A)) (A))))
(52 (paramod 51 (1 1) 50 (2 1 1)) ((not (= (A) (A))) (not (= (A) (A)))))
(53 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(54 (resolve 52 (1) 53 (1)) ((not (= (A) (A)))))
(55 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(56 (resolve 54 (1) 55 (1)) ())
)