2.99/1.99	MAYBE
2.99/1.99	
2.99/1.99	Proof:
2.99/1.99	ConCon could not decide confluence of the system.
2.99/1.99	\cite{GNG13}, Theorem 9 does not apply.
2.99/1.99	This system is of type 3 or smaller.
2.99/1.99	This system is deterministic.
2.99/1.99	This system is weakly left-linear.
2.99/1.99	This system is non-confluent.
2.99/1.99	Call external tool:
2.99/1.99	./csi.sh
2.99/1.99	Input:
2.99/1.99	(VAR y x z z')
2.99/1.99	(RULES
2.99/1.99	  plus(0, y) -> y
2.99/1.99	  plus(s(x), y) -> plus(x, s(y))
2.99/1.99	  f(x, y) -> ?1(plus(x, y), x, y)
2.99/1.99	  ?1(plus(z, z'), x, y) -> z
2.99/1.99	)
2.99/1.99	
2.99/1.99	 Nonconfluence Processor:
2.99/1.99	  terms: ?1(z',x,y) *<- ?1(plus(0(),z'),x,y) ->* 0()
2.99/1.99	  Qed
2.99/1.99	
2.99/2.02	EOF