24.41/12.41	MAYBE
24.41/12.41	
24.41/12.41	Proof:
24.41/12.41	ConCon could not decide confluence of the system.
24.41/12.41	\cite{ALS94}, Theorem 4.1 does not apply.
24.41/12.41	This system is of type 3 or smaller.
24.41/12.41	This system is strongly deterministic.
24.41/12.41	This system is quasi-decreasing.
24.41/12.41	By \cite{O02}, p. 214, Proposition 7.2.50.
24.41/12.41	This system is of type 3 or smaller.
24.41/12.41	This system is deterministic.
24.41/12.41	System R transformed to optimized U(R).
24.41/12.41	This system is terminating.
24.41/12.41	Call external tool:
24.41/12.41	./ttt2.sh
24.41/12.41	Input:
24.41/12.41	(VAR x y)
24.41/12.41	(RULES
24.41/12.41	  m(x, 0) -> x
24.41/12.41	  m(s(x), s(y)) -> m(x, y)
24.41/12.41	  lt(x, 0) -> false
24.41/12.41	  gcd(0, s(y)) -> s(y)
24.41/12.41	  gcd(s(x), s(y)) -> ?2(lt(x, y), x, y)
24.41/12.41	  ?2(true, x, y) -> gcd(s(x), m(y, x))
24.41/12.41	  lt(s(x), s(y)) -> lt(x, y)
24.41/12.41	  gcd(s(x), s(y)) -> ?1(lt(y, x), x, y)
24.41/12.41	  ?1(true, x, y) -> gcd(m(x, y), s(y))
24.41/12.41	  lt(0, s(x)) -> true
24.41/12.41	  gcd(x, x) -> x
24.41/12.41	  gcd(s(x), 0) -> s(x)
24.41/12.41	  m(0, s(y)) -> 0
24.41/12.41	)
24.41/12.41	
24.41/12.41	 DP Processor:
24.41/12.41	  DPs:
24.41/12.41	   m#(s(x),s(y)) -> m#(x,y)
24.41/12.41	   gcd#(s(x),s(y)) -> lt#(x,y)
24.41/12.41	   gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
24.41/12.41	   ?2#(true(),x,y) -> m#(y,x)
24.41/12.41	   ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
24.41/12.41	   lt#(s(x),s(y)) -> lt#(x,y)
24.41/12.41	   gcd#(s(x),s(y)) -> lt#(y,x)
24.41/12.41	   gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
24.41/12.41	   ?1#(true(),x,y) -> m#(x,y)
24.41/12.41	   ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
24.41/12.41	  TRS:
24.41/12.41	   m(x,0()) -> x
24.41/12.41	   m(s(x),s(y)) -> m(x,y)
24.41/12.41	   lt(x,0()) -> false()
24.41/12.41	   gcd(0(),s(y)) -> s(y)
24.41/12.41	   gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.41/12.41	   ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.41/12.41	   lt(s(x),s(y)) -> lt(x,y)
24.41/12.41	   gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.41/12.41	   ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.41/12.41	   lt(0(),s(x)) -> true()
24.41/12.41	   gcd(x,x) -> x
24.41/12.41	   gcd(s(x),0()) -> s(x)
24.41/12.41	   m(0(),s(y)) -> 0()
24.41/12.41	  TDG Processor:
24.41/12.41	   DPs:
24.41/12.42	    m#(s(x),s(y)) -> m#(x,y)
24.41/12.42	    gcd#(s(x),s(y)) -> lt#(x,y)
24.41/12.42	    gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
24.41/12.42	    ?2#(true(),x,y) -> m#(y,x)
24.41/12.42	    ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
24.41/12.42	    lt#(s(x),s(y)) -> lt#(x,y)
24.41/12.42	    gcd#(s(x),s(y)) -> lt#(y,x)
24.41/12.42	    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
24.41/12.42	    ?1#(true(),x,y) -> m#(x,y)
24.41/12.42	    ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
24.41/12.42	   TRS:
24.41/12.42	    m(x,0()) -> x
24.41/12.42	    m(s(x),s(y)) -> m(x,y)
24.41/12.42	    lt(x,0()) -> false()
24.41/12.42	    gcd(0(),s(y)) -> s(y)
24.41/12.42	    gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.41/12.42	    ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.41/12.42	    lt(s(x),s(y)) -> lt(x,y)
24.41/12.42	    gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.41/12.42	    ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.41/12.42	    lt(0(),s(x)) -> true()
24.41/12.42	    gcd(x,x) -> x
24.41/12.42	    gcd(s(x),0()) -> s(x)
24.41/12.42	    m(0(),s(y)) -> 0()
24.41/12.42	   graph:
24.41/12.42	    ?1#(true(),x,y) -> gcd#(m(x,y),s(y)) ->
24.41/12.42	    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
24.41/12.42	    ?1#(true(),x,y) -> gcd#(m(x,y),s(y)) ->
24.41/12.42	    gcd#(s(x),s(y)) -> lt#(y,x)
24.41/12.42	    ?1#(true(),x,y) -> gcd#(m(x,y),s(y)) ->
24.41/12.42	    gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
24.41/12.42	    ?1#(true(),x,y) -> gcd#(m(x,y),s(y)) -> gcd#(s(x),s(y)) -> lt#(x,y)
24.41/12.42	    ?1#(true(),x,y) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
24.41/12.42	    ?2#(true(),x,y) -> gcd#(s(x),m(y,x)) ->
24.41/12.42	    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
24.41/12.42	    ?2#(true(),x,y) -> gcd#(s(x),m(y,x)) ->
24.41/12.42	    gcd#(s(x),s(y)) -> lt#(y,x)
24.41/12.42	    ?2#(true(),x,y) -> gcd#(s(x),m(y,x)) ->
24.41/12.42	    gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
24.41/12.42	    ?2#(true(),x,y) -> gcd#(s(x),m(y,x)) -> gcd#(s(x),s(y)) -> lt#(x,y)
24.41/12.42	    ?2#(true(),x,y) -> m#(y,x) -> m#(s(x),s(y)) -> m#(x,y)
24.41/12.42	    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y) ->
24.41/12.42	    ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
24.41/12.42	    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y) ->
24.41/12.42	    ?1#(true(),x,y) -> m#(x,y)
24.41/12.42	    gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y) ->
24.41/12.42	    ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
24.41/12.42	    gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y) -> ?2#(true(),x,y) -> m#(y,x)
24.41/12.42	    gcd#(s(x),s(y)) -> lt#(y,x) -> lt#(s(x),s(y)) -> lt#(x,y)
24.41/12.42	    gcd#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
24.41/12.42	    lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
24.41/12.42	    m#(s(x),s(y)) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
24.41/12.42	   SCC Processor:
24.41/12.42	    #sccs: 3
24.41/12.42	    #rules: 6
24.41/12.42	    #arcs: 18/100
24.41/12.42	    DPs:
24.41/12.42	     ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
24.41/12.42	     gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
24.41/12.42	     ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
24.41/12.42	     gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
24.41/12.42	    TRS:
24.41/12.42	     m(x,0()) -> x
24.41/12.42	     m(s(x),s(y)) -> m(x,y)
24.41/12.42	     lt(x,0()) -> false()
24.41/12.42	     gcd(0(),s(y)) -> s(y)
24.41/12.42	     gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.41/12.42	     ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.41/12.42	     lt(s(x),s(y)) -> lt(x,y)
24.41/12.42	     gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.41/12.42	     ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.41/12.42	     lt(0(),s(x)) -> true()
24.41/12.42	     gcd(x,x) -> x
24.41/12.42	     gcd(s(x),0()) -> s(x)
24.41/12.42	     m(0(),s(y)) -> 0()
24.41/12.42	    Subterm Criterion Processor:
24.41/12.42	     simple projection:
24.41/12.42	      pi(m) = 0
24.41/12.42	      pi(s) = [0,0]
24.41/12.42	      pi(gcd#) = 1
24.41/12.42	      pi(?2#) = 2
24.41/12.42	      pi(?1#) = [2,2]
24.41/12.42	     problem:
24.41/12.42	      DPs:
24.41/12.42	       ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
24.41/12.42	       ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
24.41/12.42	       gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
24.41/12.42	      TRS:
24.41/12.42	       m(x,0()) -> x
24.41/12.42	       m(s(x),s(y)) -> m(x,y)
24.41/12.42	       lt(x,0()) -> false()
24.41/12.42	       gcd(0(),s(y)) -> s(y)
24.41/12.42	       gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.41/12.42	       ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.41/12.42	       lt(s(x),s(y)) -> lt(x,y)
24.41/12.42	       gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.41/12.42	       ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.41/12.42	       lt(0(),s(x)) -> true()
24.41/12.42	       gcd(x,x) -> x
24.41/12.42	       gcd(s(x),0()) -> s(x)
24.41/12.42	       m(0(),s(y)) -> 0()
24.41/12.42	     SCC Processor:
24.41/12.42	      #sccs: 1
24.41/12.42	      #rules: 2
24.41/12.42	      #arcs: 6/9
24.41/12.42	      DPs:
24.41/12.42	       ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
24.41/12.42	       gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
24.41/12.42	      TRS:
24.41/12.42	       m(x,0()) -> x
24.41/12.42	       m(s(x),s(y)) -> m(x,y)
24.41/12.42	       lt(x,0()) -> false()
24.41/12.42	       gcd(0(),s(y)) -> s(y)
24.41/12.42	       gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.41/12.42	       ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.41/12.42	       lt(s(x),s(y)) -> lt(x,y)
24.41/12.42	       gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.41/12.42	       ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.41/12.42	       lt(0(),s(x)) -> true()
24.41/12.42	       gcd(x,x) -> x
24.41/12.42	       gcd(s(x),0()) -> s(x)
24.41/12.42	       m(0(),s(y)) -> 0()
24.41/12.42	      Subterm Criterion Processor:
24.41/12.42	       simple projection:
24.41/12.42	        pi(m) = 0
24.41/12.42	        pi(gcd#) = 0
24.41/12.42	        pi(?1#) = 1
24.41/12.42	       problem:
24.41/12.42	        DPs:
24.41/12.42	         ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
24.41/12.42	        TRS:
24.41/12.42	         m(x,0()) -> x
24.41/12.42	         m(s(x),s(y)) -> m(x,y)
24.41/12.42	         lt(x,0()) -> false()
24.41/12.42	         gcd(0(),s(y)) -> s(y)
24.41/12.42	         gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.41/12.42	         ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.41/12.42	         lt(s(x),s(y)) -> lt(x,y)
24.41/12.42	         gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.41/12.42	         ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.41/12.42	         lt(0(),s(x)) -> true()
24.41/12.42	         gcd(x,x) -> x
24.41/12.42	         gcd(s(x),0()) -> s(x)
24.41/12.42	         m(0(),s(y)) -> 0()
24.41/12.42	       SCC Processor:
24.41/12.42	        #sccs: 0
24.41/12.42	        #rules: 0
24.41/12.42	        #arcs: 2/1
24.41/12.42	        
24.41/12.42	    
24.41/12.42	    DPs:
24.41/12.42	     m#(s(x),s(y)) -> m#(x,y)
24.41/12.42	    TRS:
24.41/12.42	     m(x,0()) -> x
24.41/12.42	     m(s(x),s(y)) -> m(x,y)
24.41/12.42	     lt(x,0()) -> false()
24.41/12.42	     gcd(0(),s(y)) -> s(y)
24.41/12.42	     gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.41/12.42	     ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.41/12.42	     lt(s(x),s(y)) -> lt(x,y)
24.41/12.42	     gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.41/12.42	     ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.41/12.42	     lt(0(),s(x)) -> true()
24.41/12.42	     gcd(x,x) -> x
24.41/12.42	     gcd(s(x),0()) -> s(x)
24.41/12.42	     m(0(),s(y)) -> 0()
24.41/12.42	    Subterm Criterion Processor:
24.41/12.42	     simple projection:
24.41/12.42	      pi(m#) = 0
24.41/12.42	     problem:
24.41/12.42	      DPs:
24.41/12.42	       
24.41/12.42	      TRS:
24.41/12.42	       m(x,0()) -> x
24.41/12.42	       m(s(x),s(y)) -> m(x,y)
24.41/12.42	       lt(x,0()) -> false()
24.41/12.42	       gcd(0(),s(y)) -> s(y)
24.41/12.42	       gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.41/12.42	       ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.41/12.42	       lt(s(x),s(y)) -> lt(x,y)
24.41/12.42	       gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.41/12.42	       ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.41/12.42	       lt(0(),s(x)) -> true()
24.41/12.42	       gcd(x,x) -> x
24.41/12.43	       gcd(s(x),0()) -> s(x)
24.41/12.43	       m(0(),s(y)) -> 0()
24.41/12.43	     Qed
24.41/12.43	    
24.41/12.43	    DPs:
24.41/12.43	     lt#(s(x),s(y)) -> lt#(x,y)
24.41/12.43	    TRS:
24.41/12.43	     m(x,0()) -> x
24.41/12.43	     m(s(x),s(y)) -> m(x,y)
24.41/12.43	     lt(x,0()) -> false()
24.41/12.43	     gcd(0(),s(y)) -> s(y)
24.41/12.43	     gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.41/12.43	     ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.41/12.43	     lt(s(x),s(y)) -> lt(x,y)
24.41/12.43	     gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.41/12.43	     ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.41/12.43	     lt(0(),s(x)) -> true()
24.41/12.43	     gcd(x,x) -> x
24.41/12.43	     gcd(s(x),0()) -> s(x)
24.41/12.43	     m(0(),s(y)) -> 0()
24.41/12.43	    Subterm Criterion Processor:
24.41/12.43	     simple projection:
24.41/12.43	      pi(lt#) = 0
24.41/12.43	     problem:
24.41/12.43	      DPs:
24.41/12.43	       
24.41/12.43	      TRS:
24.41/12.43	       m(x,0()) -> x
24.41/12.43	       m(s(x),s(y)) -> m(x,y)
24.41/12.43	       lt(x,0()) -> false()
24.41/12.43	       gcd(0(),s(y)) -> s(y)
24.41/12.43	       gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.41/12.43	       ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.41/12.43	       lt(s(x),s(y)) -> lt(x,y)
24.41/12.43	       gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.41/12.43	       ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.41/12.43	       lt(0(),s(x)) -> true()
24.41/12.43	       gcd(x,x) -> x
24.41/12.43	       gcd(s(x),0()) -> s(x)
24.41/12.43	       m(0(),s(y)) -> 0()
24.41/12.43	     Qed
24.41/12.43	This critical pair is conditional.
24.41/12.43	This critical pair has some non-trivial conditions.
24.41/12.43	ConCon could not decide whether all 6 critical pairs are joinable or not.
24.41/12.43	Overlap: (rule1: gcd(s(z), s(x')) -> gcd(m(z, x'), s(x')) <= lt(x', z) = true, rule2: gcd(s(y'), s(z')) -> gcd(s(y'), m(z', y')) <= lt(y', z') = true, pos: ε, mgu: {(z,y'), (x',z')})
24.41/12.43	CP: gcd(s(y'), m(z', y')) = gcd(m(y', z'), s(z')) <= lt(z', y') = true, lt(y', z') = true
24.41/12.43	ConCon could not decide infeasibility of this critical pair.
24.41/12.43	
24.41/12.46	EOF