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