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