2.75/1.99	MAYBE
3.15/1.99	
3.15/1.99	Proof:
3.15/1.99	ConCon could not decide confluence of the system.
3.15/1.99	\cite{GNG13}, Theorem 9 does not apply.
3.15/1.99	This system is of type 3 or smaller.
3.15/2.00	This system is deterministic.
3.15/2.00	This system is weakly left-linear.
3.15/2.00	This system is non-confluent.
3.15/2.00	Call external tool:
3.15/2.00	./csi.sh -s AUTO[30] -C CR -ext trs -
3.15/2.00	Input:
3.15/2.00	(VAR x)
3.15/2.00	(RULES
3.15/2.00	  a -> b
3.15/2.00	  f(x) -> ?1(x, x)
3.15/2.00	  ?1(a, x) -> c
3.15/2.00	)
3.15/2.00	
3.15/2.00	 Nonconfluence Processor:
3.15/2.00	  terms: ?1(b(),f5()) *<- ?1(a(),f5()) ->* c()
3.15/2.00	  Qed
3.15/2.00	  
3.15/2.00	  first automaton:
3.15/2.00	   final states: {1}
3.15/2.00	   transitions:
3.15/2.00	    ?1(3,2) -> 1*
3.15/2.00	    b() -> 3*
3.15/2.00	    f5() -> 2*
3.15/2.00	  
3.15/2.00	  second automaton:
3.15/2.00	   final states: {4}
3.15/2.00	   transitions:
3.15/2.00	    c() -> 4*
3.15/2.00	
3.15/2.03	EOF