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