4.59/2.16	MAYBE
4.59/2.16	
4.59/2.16	Proof:
4.59/2.16	ConCon could not decide confluence of the system.
4.59/2.16	\cite{GNG13}, Theorem 9 does not apply.
4.59/2.16	This system is of type 3 or smaller.
4.59/2.16	This system is deterministic.
4.59/2.16	This system is weakly left-linear.
4.59/2.16	This system is non-confluent.
4.59/2.16	Call external tool:
4.59/2.16	./csi.sh
4.59/2.16	Input:
4.59/2.16	(VAR x y)
4.59/2.16	(RULES
4.59/2.16	  f(x, y) -> ?1(a, x, y)
4.59/2.16	  ?1(d, x, y) -> g(x)
4.59/2.16	  h(s(x)) -> x
4.59/2.16	  g(s(x)) -> x
4.59/2.16	  b -> d
4.59/2.16	  e -> e
4.59/2.16	  a -> d
4.59/2.16	  f(x, y) -> ?2(b, x, y)
4.59/2.16	  ?2(d, x, y) -> h(x)
4.59/2.16	)
4.59/2.16	
4.59/2.16	 sorted: (order)
4.59/2.16	 0:f(x,y) -> ?1(a(),x,y)
4.59/2.16	   ?1(d(),x,y) -> g(x)
4.59/2.16	   h(s(x)) -> x
4.59/2.16	   g(s(x)) -> x
4.59/2.16	   b() -> d()
4.59/2.16	   a() -> d()
4.59/2.16	   f(x,y) -> ?2(b(),x,y)
4.59/2.16	   ?2(d(),x,y) -> h(x)
4.59/2.16	 1:e() -> e()
4.59/2.16	 -----
4.59/2.16	 sorts
4.59/2.16	   [0>1, 0>4, 1>2, 1>6, 1>19, 2>8, 4>5, 4>11, 4>18, 5>9, 6>7, 7>13, 8>10, 8>16, 9>10, 9>14, 10>15,
4.59/2.16	    11>12, 12>13, 14>17, 16>17, 18>20, 19>20]
4.59/2.16	 sort attachment (non-strict)
4.59/2.16	   f : 17 x 20 -> 0
4.59/2.16	   ?1 : 6 x 16 x 19 -> 1
4.59/2.16	   a : 7
4.59/2.16	   d : 13
4.59/2.16	   g : 8 -> 2
4.59/2.16	   h : 9 -> 5
4.59/2.16	   s : 15 -> 10
4.59/2.16	   b : 12
4.59/2.16	   e : 3
4.59/2.16	   ?2 : 11 x 14 x 18 -> 4
4.59/2.16	 -----
4.59/2.16	 0:f(x,y) -> ?1(a(),x,y)
4.59/2.16	   ?1(d(),x,y) -> g(x)
4.59/2.16	   h(s(x)) -> x
4.59/2.16	   g(s(x)) -> x
4.59/2.16	   b() -> d()
4.59/2.16	   a() -> d()
4.59/2.16	   f(x,y) -> ?2(b(),x,y)
4.59/2.16	   ?2(d(),x,y) -> h(x)
4.59/2.16	   Nonconfluence Processor:
4.59/2.16	    terms: g(x) *<- f(x,y) ->* h(x)
4.59/2.16	    Qed
4.59/2.16	 
4.59/2.16	 
4.59/2.16	 1:e() -> e()
4.59/2.16	   Open
4.59/2.16	 
4.59/2.16	
4.59/2.19	EOF