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