;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:21:00 1995
;;
;;;; x=x.
;;;; f(f(v,w,x),y,f(v,w,z))=f(v,w,f(x,y,z)).
;;;; f(y,x,x)=x.
;;;; f(x,y,g(y))=x.
;;;; f(x,x,y)=x.
;;;; f(g(y),y,x)=x.
;;;; f(f(A,g(A),B),g(f(f(C,D,E),F,f(C,D,G))),f(D,f(G,F,E),C))!=B.
;;
;; ----> UNIT CONFLICT at   3.78 sec ----> 1086 [binary,1085.1,1.1] $F.
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((= (f (f v0 v1 v2) v3 (f v0 v1 v4)) (f v0 v1 (f v2 v3 v4)))))
(3 (input) ((= (f v0 v1 v1) v1)))
(4 (input) ((= (f v0 v1 (g v1)) v0)))
(5 (input) ((= (f v0 v0 v1) v0)))
(6 (input) ((= (f (g v0) v0 v1) v1)))
(7 (input) ((not (= (f (f (A) (g (A)) (B)) (g (f (f (C) (D) (E)) (F) (f (C) (D) (G)))) (f (D) (f (G) (F) (E)) (C))) (B)))))
(8 (instantiate 2 ((v0 . (C))(v1 . (D))(v2 . (E))(v3 . (F))(v4 . (G)))) ((= (f (f (C) (D) (E)) (F) (f (C) (D) (G))) (f (C) (D) (f (E) (F) (G))))))
(9 (paramod 8 (1 1) 7 (1 1 1 2 1)) ((not (= (f (f (A) (g (A)) (B)) (g (f (C) (D) (f (E) (F) (G)))) (f (D) (f (G) (F) (E)) (C))) (B)))))
(10 (instantiate 2 ((v3 . (f v0 v1 v4)))) ((= (f (f v0 v1 v2) (f v0 v1 v4) (f v0 v1 v4)) (f v0 v1 (f v2 (f v0 v1 v4) v4)))))
(11 (instantiate 3 ((v0 . (f v0 v1 v2))(v1 . (f v0 v1 v4)))) ((= (f (f v0 v1 v2) (f v0 v1 v4) (f v0 v1 v4)) (f v0 v1 v4))))
(12 (paramod 10 (1 1) 11 (1 1)) ((= (f v0 v1 (f v2 (f v0 v1 v4) v4)) (f v0 v1 v4))))
(13 (instantiate 12 ((v4 . v3))) ((= (f v0 v1 (f v2 (f v0 v1 v3) v3)) (f v0 v1 v3))))
(14 (instantiate 3 ((v0 . v64)(v1 . v68))) ((= (f v64 v68 v68) v68)))
(15 (instantiate 2 ((v0 . v64)(v1 . v68)(v2 . v66)(v3 . v67)(v4 . v68))) ((= (f (f v64 v68 v66) v67 (f v64 v68 v68)) (f v64 v68 (f v66 v67 v68)))))
(16 (paramod 14 (1 1) 15 (1 1 3)) ((= (f (f v64 v68 v66) v67 v68) (f v64 v68 (f v66 v67 v68)))))
(17 (instantiate 16 ((v64 . v0)(v66 . v2)(v67 . v3)(v68 . v1))) ((= (f (f v0 v1 v2) v3 v1) (f v0 v1 (f v2 v3 v1)))))
(18 (instantiate 3 ((v0 . v64)(v1 . v66))) ((= (f v64 v66 v66) v66)))
(19 (instantiate 2 ((v0 . v64)(v1 . v66)(v2 . v66)(v3 . v67)(v4 . v68))) ((= (f (f v64 v66 v66) v67 (f v64 v66 v68)) (f v64 v66 (f v66 v67 v68)))))
(20 (paramod 18 (1 1) 19 (1 1 1)) ((= (f v66 v67 (f v64 v66 v68)) (f v64 v66 (f v66 v67 v68)))))
(21 (instantiate 20 ((v64 . v2)(v66 . v0)(v67 . v1)(v68 . v3))) ((= (f v0 v1 (f v2 v0 v3)) (f v2 v0 (f v0 v1 v3)))))
(22 (flip 21 (1)) ((= (f v2 v0 (f v0 v1 v3)) (f v0 v1 (f v2 v0 v3)))))
(23 (instantiate 2 ((v3 . (f v0 v1 v2)))) ((= (f (f v0 v1 v2) (f v0 v1 v2) (f v0 v1 v4)) (f v0 v1 (f v2 (f v0 v1 v2) v4)))))
(24 (instantiate 5 ((v0 . (f v0 v1 v2))(v1 . (f v0 v1 v4)))) ((= (f (f v0 v1 v2) (f v0 v1 v2) (f v0 v1 v4)) (f v0 v1 v2))))
(25 (paramod 23 (1 1) 24 (1 1)) ((= (f v0 v1 (f v2 (f v0 v1 v2) v4)) (f v0 v1 v2))))
(26 (instantiate 25 ((v4 . v3))) ((= (f v0 v1 (f v2 (f v0 v1 v2) v3)) (f v0 v1 v2))))
(27 (instantiate 5 ((v0 . v65)(v1 . v68))) ((= (f v65 v65 v68) v65)))
(28 (instantiate 2 ((v0 . v65)(v1 . v65)(v2 . v66)(v3 . v67)(v4 . v68))) ((= (f (f v65 v65 v66) v67 (f v65 v65 v68)) (f v65 v65 (f v66 v67 v68)))))
(29 (paramod 27 (1 1) 28 (1 1 3)) ((= (f (f v65 v65 v66) v67 v65) (f v65 v65 (f v66 v67 v68)))))
(30 (instantiate 5 ((v0 . v65)(v1 . v66))) ((= (f v65 v65 v66) v65)))
(31 (paramod 30 (1 1) 29 (1 1 1)) ((= (f v65 v67 v65) (f v65 v65 (f v66 v67 v68)))))
(32 (instantiate 5 ((v0 . v65)(v1 . (f v66 v67 v68)))) ((= (f v65 v65 (f v66 v67 v68)) v65)))
(33 (paramod 32 (1 1) 31 (1 2)) ((= (f v65 v67 v65) v65)))
(34 (instantiate 33 ((v65 . v0)(v67 . v1))) ((= (f v0 v1 v0) v0)))
(35 (instantiate 34 ((v0 . v68)(v1 . v65))) ((= (f v68 v65 v68) v68)))
(36 (instantiate 2 ((v0 . v68)(v1 . v65)(v2 . v66)(v3 . v67)(v4 . v68))) ((= (f (f v68 v65 v66) v67 (f v68 v65 v68)) (f v68 v65 (f v66 v67 v68)))))
(37 (paramod 35 (1 1) 36 (1 1 3)) ((= (f (f v68 v65 v66) v67 v68) (f v68 v65 (f v66 v67 v68)))))
(38 (instantiate 37 ((v65 . v1)(v66 . v2)(v67 . v3)(v68 . v0))) ((= (f (f v0 v1 v2) v3 v0) (f v0 v1 (f v2 v3 v0)))))
(39 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (f v64 v65 (g v65)) v64)))
(40 (instantiate 13 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . (g v65)))) ((= (f v64 v65 (f v66 (f v64 v65 (g v65)) (g v65))) (f v64 v65 (g v65)))))
(41 (paramod 39 (1 1) 40 (1 1 3 2)) ((= (f v64 v65 (f v66 v64 (g v65))) (f v64 v65 (g v65)))))
(42 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (f v64 v65 (g v65)) v64)))
(43 (paramod 42 (1 1) 41 (1 2)) ((= (f v64 v65 (f v66 v64 (g v65))) v64)))
(44 (instantiate 43 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (f v0 v1 (f v2 v0 (g v1))) v0)))
(45 (instantiate 44 ((v0 . v64)(v1 . v65))) ((= (f v64 v65 (f v2 v64 (g v65))) v64)))
(46 (instantiate 2 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67)(v4 . (f v2 v64 (g v65))))) ((= (f (f v64 v65 v66) v67 (f v64 v65 (f v2 v64 (g v65)))) (f v64 v65 (f v66 v67 (f v2 v64 (g v65)))))))
(47 (paramod 45 (1 1) 46 (1 1 3)) ((= (f (f v64 v65 v66) v67 v64) (f v64 v65 (f v66 v67 (f v2 v64 (g v65)))))))
(48 (instantiate 38 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) ((= (f (f v64 v65 v66) v67 v64) (f v64 v65 (f v66 v67 v64)))))
(49 (paramod 48 (1 1) 47 (1 1)) ((= (f v64 v65 (f v66 v67 v64)) (f v64 v65 (f v66 v67 (f v2 v64 (g v65)))))))
(50 (flip 49 (1)) ((= (f v64 v65 (f v66 v67 (f v2 v64 (g v65)))) (f v64 v65 (f v66 v67 v64)))))
(51 (instantiate 50 ((v2 . v4)(v64 . v0)(v65 . v1)(v66 . v2)(v67 . v3))) ((= (f v0 v1 (f v2 v3 (f v4 v0 (g v1)))) (f v0 v1 (f v2 v3 v0)))))
(52 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (f v64 v65 (g v65)) v64)))
(53 (instantiate 17 ((v0 . v64)(v1 . v65)(v2 . (g v65))(v3 . v67))) ((= (f (f v64 v65 (g v65)) v67 v65) (f v64 v65 (f (g v65) v67 v65)))))
(54 (paramod 52 (1 1) 53 (1 1 1)) ((= (f v64 v67 v65) (f v64 v65 (f (g v65) v67 v65)))))
(55 (instantiate 54 ((v64 . v0)(v65 . v2)(v67 . v1))) ((= (f v0 v1 v2) (f v0 v2 (f (g v2) v1 v2)))))
(56 (flip 55 (1)) ((= (f v0 v2 (f (g v2) v1 v2)) (f v0 v1 v2))))
(57 (instantiate 17 ((v1 . (g v65))(v3 . v64))) ((= (f (f v0 (g v65) v2) v64 (g v65)) (f v0 (g v65) (f v2 v64 (g v65))))))
(58 (instantiate 44 ((v0 . v64)(v1 . v65)(v2 . (f v0 (g v65) v2)))) ((= (f v64 v65 (f (f v0 (g v65) v2) v64 (g v65))) v64)))
(59 (paramod 57 (1 1) 58 (1 1 3)) ((= (f v64 v65 (f v0 (g v65) (f v2 v64 (g v65)))) v64)))
(60 (instantiate 51 ((v0 . v64)(v1 . v65)(v2 . v0)(v3 . (g v65))(v4 . v2))) ((= (f v64 v65 (f v0 (g v65) (f v2 v64 (g v65)))) (f v64 v65 (f v0 (g v65) v64)))))
(61 (paramod 60 (1 1) 59 (1 1)) ((= (f v64 v65 (f v0 (g v65) v64)) v64)))
(62 (instantiate 61 ((v0 . v2)(v64 . v0)(v65 . v1))) ((= (f v0 v1 (f v2 (g v1) v0)) v0)))
(63 (instantiate 4 ((v0 . v66)(v1 . (g v65)))) ((= (f v66 (g v65) (g (g v65))) v66)))
(64 (instantiate 62 ((v0 . (g (g v65)))(v1 . v65)(v2 . v66))) ((= (f (g (g v65)) v65 (f v66 (g v65) (g (g v65)))) (g (g v65)))))
(65 (paramod 63 (1 1) 64 (1 1 3)) ((= (f (g (g v65)) v65 v66) (g (g v65)))))
(66 (instantiate 65 ((v65 . v0)(v66 . v1))) ((= (f (g (g v0)) v0 v1) (g (g v0)))))
(67 (instantiate 3 ((v0 . (g (g v65)))(v1 . v65))) ((= (f (g (g v65)) v65 v65) v65)))
(68 (instantiate 66 ((v0 . v65)(v1 . v65))) ((= (f (g (g v65)) v65 v65) (g (g v65)))))
(69 (paramod 67 (1 1) 68 (1 1)) ((= v65 (g (g v65)))))
(70 (flip 69 (1)) ((= (g (g v65)) v65)))
(71 (instantiate 70 ((v65 . v0))) ((= (g (g v0)) v0)))
(72 (instantiate 6 ((v0 . (g v0))(v1 . v65))) ((= (f (g (g v0)) (g v0) v65) v65)))
(73 (paramod 71 (1 1) 72 (1 1 1)) ((= (f v0 (g v0) v65) v65)))
(74 (instantiate 73 ((v65 . v1))) ((= (f v0 (g v0) v1) v1)))
(75 (instantiate 62 ((v0 . v64)(v1 . (g v0))(v2 . v66))) ((= (f v64 (g v0) (f v66 (g (g v0)) v64)) v64)))
(76 (paramod 71 (1 1) 75 (1 1 3 2)) ((= (f v64 (g v0) (f v66 v0 v64)) v64)))
(77 (instantiate 76 ((v0 . v1)(v64 . v0)(v66 . v2))) ((= (f v0 (g v1) (f v2 v1 v0)) v0)))
(78 (instantiate 4 ((v0 . v64)(v1 . (g v0)))) ((= (f v64 (g v0) (g (g v0))) v64)))
(79 (paramod 71 (1 1) 78 (1 1 3)) ((= (f v64 (g v0) v0) v64)))
(80 (instantiate 79 ((v0 . v1)(v64 . v0))) ((= (f v0 (g v1) v1) v0)))
(81 (instantiate 74 ((v0 . (A))(v1 . (B)))) ((= (f (A) (g (A)) (B)) (B))))
(82 (paramod 81 (1 1) 9 (1 1 1 1)) ((not (= (f (B) (g (f (C) (D) (f (E) (F) (G)))) (f (D) (f (G) (F) (E)) (C))) (B)))))
(83 (instantiate 3 ((v0 . v64)(v1 . v67))) ((= (f v64 v67 v67) v67)))
(84 (instantiate 22 ((v0 . v64)(v1 . v67)(v2 . v66)(v3 . v67))) ((= (f v66 v64 (f v64 v67 v67)) (f v64 v67 (f v66 v64 v67)))))
(85 (paramod 83 (1 1) 84 (1 1 3)) ((= (f v66 v64 v67) (f v64 v67 (f v66 v64 v67)))))
(86 (flip 85 (1)) ((= (f v64 v67 (f v66 v64 v67)) (f v66 v64 v67))))
(87 (instantiate 86 ((v64 . v0)(v66 . v2)(v67 . v1))) ((= (f v0 v1 (f v2 v0 v1)) (f v2 v0 v1))))
(88 (instantiate 80 ((v0 . v64)(v1 . v66))) ((= (f v64 (g v66) v66) v64)))
(89 (instantiate 26 ((v0 . v64)(v1 . (g v66))(v2 . v66)(v3 . v67))) ((= (f v64 (g v66) (f v66 (f v64 (g v66) v66) v67)) (f v64 (g v66) v66))))
(90 (paramod 88 (1 1) 89 (1 1 3 2)) ((= (f v64 (g v66) (f v66 v64 v67)) (f v64 (g v66) v66))))
(91 (instantiate 80 ((v0 . v64)(v1 . v66))) ((= (f v64 (g v66) v66) v64)))
(92 (paramod 91 (1 1) 90 (1 2)) ((= (f v64 (g v66) (f v66 v64 v67)) v64)))
(93 (instantiate 92 ((v64 . v0)(v66 . v1)(v67 . v2))) ((= (f v0 (g v1) (f v1 v0 v2)) v0)))
(94 (instantiate 93 ((v0 . v66))) ((= (f v66 (g v1) (f v1 v66 v2)) v66)))
(95 (instantiate 77 ((v0 . (f v1 v66 v2))(v1 . (g v1))(v2 . v66))) ((= (f (f v1 v66 v2) (g (g v1)) (f v66 (g v1) (f v1 v66 v2))) (f v1 v66 v2))))
(96 (paramod 94 (1 1) 95 (1 1 3)) ((= (f (f v1 v66 v2) (g (g v1)) v66) (f v1 v66 v2))))
(97 (instantiate 71 ((v0 . v1))) ((= (g (g v1)) v1)))
(98 (paramod 97 (1 1) 96 (1 1 2)) ((= (f (f v1 v66 v2) v1 v66) (f v1 v66 v2))))
(99 (instantiate 17 ((v0 . v1)(v1 . v66)(v2 . v2)(v3 . v1))) ((= (f (f v1 v66 v2) v1 v66) (f v1 v66 (f v2 v1 v66)))))
(100 (paramod 99 (1 1) 98 (1 1)) ((= (f v1 v66 (f v2 v1 v66)) (f v1 v66 v2))))
(101 (instantiate 87 ((v0 . v1)(v1 . v66)(v2 . v2))) ((= (f v1 v66 (f v2 v1 v66)) (f v2 v1 v66))))
(102 (paramod 101 (1 1) 100 (1 1)) ((= (f v2 v1 v66) (f v1 v66 v2))))
(103 (instantiate 102 ((v2 . v0)(v66 . v2))) ((= (f v0 v1 v2) (f v1 v2 v0))))
(104 (instantiate 74 ((v0 . v64)(v1 . v66))) ((= (f v64 (g v64) v66) v66)))
(105 (instantiate 103 ((v0 . v64)(v1 . (g v64))(v2 . v66))) ((= (f v64 (g v64) v66) (f (g v64) v66 v64))))
(106 (paramod 104 (1 1) 105 (1 1)) ((= v66 (f (g v64) v66 v64))))
(107 (flip 106 (1)) ((= (f (g v64) v66 v64) v66)))
(108 (instantiate 107 ((v64 . v0)(v66 . v1))) ((= (f (g v0) v1 v0) v1)))
(109 (instantiate 108 ((v0 . v2)(v1 . v1))) ((= (f (g v2) v1 v2) v1)))
(110 (paramod 109 (1 1) 56 (1 1 3)) ((= (f v0 v2 v1) (f v0 v1 v2))))
(111 (instantiate 110 ((v1 . v2)(v2 . v1))) ((= (f v0 v1 v2) (f v0 v2 v1))))
(112 (instantiate 103 ((v0 . (C))(v1 . (D))(v2 . (f (E) (F) (G))))) ((= (f (C) (D) (f (E) (F) (G))) (f (D) (f (E) (F) (G)) (C)))))
(113 (paramod 112 (1 1) 82 (1 1 1 2 1)) ((not (= (f (B) (g (f (D) (f (E) (F) (G)) (C))) (f (D) (f (G) (F) (E)) (C))) (B)))))
(114 (instantiate 103 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (f v64 v65 v66) (f v65 v66 v64))))
(115 (instantiate 111 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (f v64 v65 v66) (f v64 v66 v65))))
(116 (paramod 114 (1 1) 115 (1 1)) ((= (f v65 v66 v64) (f v64 v66 v65))))
(117 (instantiate 116 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (f v0 v1 v2) (f v2 v1 v0))))
(118 (instantiate 117 ((v0 . (E))(v1 . (F))(v2 . (G)))) ((= (f (E) (F) (G)) (f (G) (F) (E)))))
(119 (paramod 118 (1 1) 113 (1 1 1 2 1 2)) ((not (= (f (B) (g (f (D) (f (G) (F) (E)) (C))) (f (D) (f (G) (F) (E)) (C))) (B)))))
(120 (instantiate 80 ((v0 . (B))(v1 . (f (D) (f (G) (F) (E)) (C))))) ((= (f (B) (g (f (D) (f (G) (F) (E)) (C))) (f (D) (f (G) (F) (E)) (C))) (B))))
(121 (paramod 120 (1 1) 119 (1 1 1)) ((not (= (B) (B)))))
(122 (instantiate 1 ((v0 . (B)))) ((= (B) (B))))
(123 (resolve 121 (1) 122 (1)) ())
)