4.02/1.54	MAYBE
4.02/1.54	
4.02/1.54	Proof:
4.02/1.54	ConCon could not decide confluence of the system.
4.02/1.54	\cite{GNG13}, Theorem 9 does not apply.
4.02/1.54	This system is of type 3 or smaller.
4.02/1.54	This system is deterministic.
4.02/1.54	This system is weakly left-linear.
4.02/1.54	This system is non-confluent.
4.02/1.54	Call external tool:
4.02/1.54	./csi.sh
4.02/1.54	Input:
4.02/1.54	  p(q(x)) -> p(r(x))
4.02/1.54	  q(h(x)) -> r(x)
4.02/1.54	  r(x) -> ?1(s(x), x)
4.02/1.54	  ?1(0, x) -> r(h(x))
4.02/1.54	  s(x) -> 1
4.02/1.54	
4.02/1.54	 Nonconfluence Processor:
4.02/1.54	  terms: p(r(f8())) *<- p(q(h(f8()))) ->* p(r(h(f8())))
4.02/1.54	  Qed
4.02/1.54	  
4.02/1.54	  first automaton:
4.02/1.54	   final states: {1}
4.02/1.54	   transitions:
4.02/1.54	    p(3) -> 1*
4.02/1.54	    r(2) -> 3*
4.02/1.54	    s(2) -> 13*
4.02/1.54	    ?1(13,2) -> 3*
4.02/1.54	    1() -> 13*
4.02/1.54	    f8() -> 2*
4.02/1.54	  
4.02/1.54	  second automaton:
4.02/1.54	   final states: {4}
4.02/1.54	   transitions:
4.02/1.54	    p(7) -> 4*
4.02/1.54	    r(6) -> 7*
4.02/1.54	    h(5) -> 6*
4.02/1.54	    s(6) -> 12*
4.02/1.54	    ?1(12,6) -> 7*
4.02/1.54	    1() -> 12*
4.02/1.54	    f8() -> 5*
4.02/1.54	
4.02/1.57	EOF