1.74/1.31	MAYBE
1.74/1.31	
1.74/1.31	Proof:
1.74/1.31	ConCon could not decide confluence of the system.
1.74/1.31	\cite{GNG13}, Theorem 9 does not apply.
1.74/1.31	This system is of type 3 or smaller.
1.74/1.31	This system is deterministic.
1.74/1.31	This system is weakly left-linear.
1.74/1.31	This system is non-confluent.
1.74/1.31	Call external tool:
1.74/1.31	./csi.sh
1.74/1.31	Input:
1.74/1.31	  plus(0, y) -> y
1.74/1.31	  plus(s(x), y) -> plus(x, s(y))
1.74/1.31	  f(x, y) -> ?1(plus(x, y), x, y)
1.74/1.31	  ?1(plus(z, z'), x, y) -> z
1.74/1.31	
1.74/1.31	 Nonconfluence Processor:
1.74/1.31	  terms: ?1(f5(),f6(),f7()) *<- ?1(plus(0(),f5()),f6(),f7()) ->* 0()
1.74/1.31	  Qed
1.74/1.31	  
1.74/1.31	  first automaton:
1.74/1.31	   final states: {10}
1.74/1.31	   transitions:
1.74/1.31	    ?1(13,12,11) -> 10*
1.74/1.31	    f5() -> 13*
1.74/1.31	    f6() -> 12*
1.74/1.31	    f7() -> 11*
1.74/1.31	  
1.74/1.31	  second automaton:
1.74/1.31	   final states: {14}
1.74/1.31	   transitions:
1.74/1.31	    0() -> 14*
1.74/1.31	
1.74/1.34	EOF