;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:41:20 1995
;;
;;;;  -> x=x.
;;;; p(A,A,B)=B, p(A,B,B)=A, p(A,B,A)=A, f(A)=A -> .
;;;;  -> p(p(x,x,y),p(f(z),u,z),z)=y.
;;
;; ----> UNIT CONFLICT at   0.06 sec ----> 22 [binary,20.1,19.1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((not (= (p (A) (A) (B)) (B))) (not (= (p (A) (B) (B)) (A))) (not (= (p (A) (B) (A)) (A))) (not (= (f (A)) (A)))))
(3 (input) ((= (p (p v0 v0 v1) (p (f v2) v3 v2) v2) v1)))
(4 (instantiate 3 ((v0 . (f v65))(v1 . v65)(v2 . v65)(v3 . (f v65)))) ((= (p (p (f v65) (f v65) v65) (p (f v65) (f v65) v65) v65) v65)))
(5 (instantiate 3 ((v0 . (p (f v65) (f v65) v65))(v1 . v65)(v2 . v66)(v3 . v67))) ((= (p (p (p (f v65) (f v65) v65) (p (f v65) (f v65) v65) v65) (p (f v66) v67 v66) v66) v65)))
(6 (paramod 4 (1 1) 5 (1 1 1)) ((= (p v65 (p (f v66) v67 v66) v66) v65)))
(7 (instantiate 6 ((v65 . v0)(v66 . v1)(v67 . v2))) ((= (p v0 (p (f v1) v2 v1) v1) v0)))
(8 (instantiate 7 ((v0 . (p v0 v0 v1))(v1 . v2)(v2 . v3))) ((= (p (p v0 v0 v1) (p (f v2) v3 v2) v2) (p v0 v0 v1))))
(9 (paramod 8 (1 1) 3 (1 1)) ((= (p v0 v0 v1) v1)))
(10 (instantiate 9 ((v0 . (A))(v1 . (B)))) ((= (p (A) (A) (B)) (B))))
(11 (paramod 10 (1 1) 2 (1 1 1)) ((not (= (B) (B))) (not (= (p (A) (B) (B)) (A))) (not (= (p (A) (B) (A)) (A))) (not (= (f (A)) (A)))))
(12 (instantiate 1 ((v0 . (B)))) ((= (B) (B))))
(13 (resolve 11 (1) 12 (1)) ((not (= (p (A) (B) (B)) (A))) (not (= (p (A) (B) (A)) (A))) (not (= (f (A)) (A)))))
(14 (instantiate 9 ((v0 . (f v65))(v1 . v65))) ((= (p (f v65) (f v65) v65) v65)))
(15 (instantiate 7 ((v0 . v64)(v1 . v65)(v2 . (f v65)))) ((= (p v64 (p (f v65) (f v65) v65) v65) v64)))
(16 (paramod 14 (1 1) 15 (1 1 2)) ((= (p v64 v65 v65) v64)))
(17 (instantiate 16 ((v64 . v0)(v65 . v1))) ((= (p v0 v1 v1) v0)))
(18 (instantiate 7 ((v0 . (f v65))(v1 . v65))) ((= (p (f v65) (p (f v65) v2 v65) v65) (f v65))))
(19 (instantiate 7 ((v0 . v64)(v1 . v65)(v2 . (p (f v65) v2 v65)))) ((= (p v64 (p (f v65) (p (f v65) v2 v65) v65) v65) v64)))
(20 (paramod 18 (1 1) 19 (1 1 2)) ((= (p v64 (f v65) v65) v64)))
(21 (instantiate 20 ((v64 . v0)(v65 . v1))) ((= (p v0 (f v1) v1) v0)))
(22 (instantiate 9 ((v0 . (p (f v65) v66 v65))(v1 . v65))) ((= (p (p (f v65) v66 v65) (p (f v65) v66 v65) v65) v65)))
(23 (instantiate 7 ((v0 . (p (f v65) v66 v65))(v1 . v65)(v2 . v66))) ((= (p (p (f v65) v66 v65) (p (f v65) v66 v65) v65) (p (f v65) v66 v65))))
(24 (paramod 22 (1 1) 23 (1 1)) ((= v65 (p (f v65) v66 v65))))
(25 (flip 24 (1)) ((= (p (f v65) v66 v65) v65)))
(26 (instantiate 25 ((v65 . v0)(v66 . v1))) ((= (p (f v0) v1 v0) v0)))
(27 (instantiate 17 ((v0 . (A))(v1 . (B)))) ((= (p (A) (B) (B)) (A))))
(28 (paramod 27 (1 1) 13 (1 1 1)) ((not (= (A) (A))) (not (= (p (A) (B) (A)) (A))) (not (= (f (A)) (A)))))
(29 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(30 (resolve 28 (1) 29 (1)) ((not (= (p (A) (B) (A)) (A))) (not (= (f (A)) (A)))))
(31 (instantiate 9 ((v0 . (f v65))(v1 . v65))) ((= (p (f v65) (f v65) v65) v65)))
(32 (instantiate 21 ((v0 . (f v65))(v1 . v65))) ((= (p (f v65) (f v65) v65) (f v65))))
(33 (paramod 31 (1 1) 32 (1 1)) ((= v65 (f v65))))
(34 (flip 33 (1)) ((= (f v65) v65)))
(35 (instantiate 34 ((v65 . v0))) ((= (f v0) v0)))
(36 (instantiate 35 ((v0 . (A)))) ((= (f (A)) (A))))
(37 (paramod 36 (1 1) 30 (2 1 1)) ((not (= (p (A) (B) (A)) (A))) (not (= (A) (A)))))
(38 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(39 (resolve 37 (2) 38 (1)) ((not (= (p (A) (B) (A)) (A)))))
(40 (paramod 35 (1 1) 26 (1 1 1)) ((= (p v0 v1 v0) v0)))
(41 (instantiate 40 ((v0 . (A))(v1 . (B)))) ((= (p (A) (B) (A)) (A))))
(42 (resolve 39 (1) 41 (1)) ())
)