YES(O(1),O(1))
516.60/148.06	YES(O(1),O(1))
516.60/148.06	
516.60/148.06	We are left with following problem, upon which TcT provides the
516.60/148.06	certificate YES(O(1),O(1)).
516.60/148.06	
516.60/148.06	Strict Trs:
516.60/148.06	  { f(c(c(a(), y, a()), b(x, z), a())) -> b(y, f(c(f(a()), z, z)))
516.60/148.06	  , f(b(b(x, f(y)), z)) -> c(z, x, f(b(b(f(a()), y), y)))
516.60/148.06	  , c(b(a(), a()), b(y, z), x) -> b(a(), b(z, z)) }
516.60/148.06	Obligation:
516.60/148.06	  innermost runtime complexity
516.60/148.06	Answer:
516.60/148.06	  YES(O(1),O(1))
516.60/148.06	
516.60/148.06	We add the following dependency tuples:
516.60/148.06	
516.60/148.06	Strict DPs:
516.60/148.06	  { f^#(c(c(a(), y, a()), b(x, z), a())) ->
516.60/148.06	    c_1(f^#(c(f(a()), z, z)), c^#(f(a()), z, z), f^#(a()))
516.60/148.06	  , f^#(b(b(x, f(y)), z)) ->
516.60/148.06	    c_2(c^#(z, x, f(b(b(f(a()), y), y))),
516.60/148.06	        f^#(b(b(f(a()), y), y)),
516.60/148.06	        f^#(a()))
516.60/148.06	  , c^#(b(a(), a()), b(y, z), x) -> c_3() }
516.60/148.06	
516.60/148.06	and mark the set of starting terms.
516.60/148.06	
516.60/148.06	We are left with following problem, upon which TcT provides the
516.60/148.06	certificate YES(O(1),O(1)).
516.60/148.06	
516.60/148.06	Strict DPs:
516.60/148.06	  { f^#(c(c(a(), y, a()), b(x, z), a())) ->
516.60/148.06	    c_1(f^#(c(f(a()), z, z)), c^#(f(a()), z, z), f^#(a()))
516.60/148.06	  , f^#(b(b(x, f(y)), z)) ->
516.60/148.06	    c_2(c^#(z, x, f(b(b(f(a()), y), y))),
516.60/148.06	        f^#(b(b(f(a()), y), y)),
516.60/148.06	        f^#(a()))
516.60/148.06	  , c^#(b(a(), a()), b(y, z), x) -> c_3() }
516.60/148.06	Weak Trs:
516.60/148.06	  { f(c(c(a(), y, a()), b(x, z), a())) -> b(y, f(c(f(a()), z, z)))
516.60/148.06	  , f(b(b(x, f(y)), z)) -> c(z, x, f(b(b(f(a()), y), y)))
516.60/148.06	  , c(b(a(), a()), b(y, z), x) -> b(a(), b(z, z)) }
516.60/148.06	Obligation:
516.60/148.06	  innermost runtime complexity
516.60/148.06	Answer:
516.60/148.06	  YES(O(1),O(1))
516.60/148.06	
516.60/148.06	Consider the dependency graph:
516.60/148.06	
516.60/148.06	  1: f^#(c(c(a(), y, a()), b(x, z), a())) ->
516.60/148.06	     c_1(f^#(c(f(a()), z, z)), c^#(f(a()), z, z), f^#(a()))
516.60/148.06	  
516.60/148.06	  2: f^#(b(b(x, f(y)), z)) ->
516.60/148.06	     c_2(c^#(z, x, f(b(b(f(a()), y), y))),
516.60/148.06	         f^#(b(b(f(a()), y), y)),
516.60/148.06	         f^#(a()))
516.60/148.06	     -->_1 c^#(b(a(), a()), b(y, z), x) -> c_3() :3
516.60/148.06	     -->_2 f^#(b(b(x, f(y)), z)) ->
516.60/148.06	           c_2(c^#(z, x, f(b(b(f(a()), y), y))),
516.60/148.06	               f^#(b(b(f(a()), y), y)),
516.60/148.06	               f^#(a())) :2
516.60/148.06	  
516.60/148.06	  3: c^#(b(a(), a()), b(y, z), x) -> c_3()
516.60/148.06	  
516.60/148.06	
516.60/148.06	Only the nodes {3} are reachable from nodes {3} that start
516.60/148.06	derivation from marked basic terms. The nodes not reachable are
516.60/148.06	removed from the problem.
516.60/148.06	
516.60/148.06	We are left with following problem, upon which TcT provides the
516.60/148.06	certificate YES(O(1),O(1)).
516.60/148.06	
516.60/148.06	Strict DPs: { c^#(b(a(), a()), b(y, z), x) -> c_3() }
516.60/148.06	Weak Trs:
516.60/148.06	  { f(c(c(a(), y, a()), b(x, z), a())) -> b(y, f(c(f(a()), z, z)))
516.60/148.06	  , f(b(b(x, f(y)), z)) -> c(z, x, f(b(b(f(a()), y), y)))
516.60/148.06	  , c(b(a(), a()), b(y, z), x) -> b(a(), b(z, z)) }
516.60/148.06	Obligation:
516.60/148.06	  innermost runtime complexity
516.60/148.06	Answer:
516.60/148.06	  YES(O(1),O(1))
516.60/148.06	
516.60/148.06	We estimate the number of application of {1} by applications of
516.60/148.06	Pre({1}) = {}. Here rules are labeled as follows:
516.60/148.06	
516.60/148.06	  DPs:
516.60/148.06	    { 1: c^#(b(a(), a()), b(y, z), x) -> c_3() }
516.60/148.06	
516.60/148.06	We are left with following problem, upon which TcT provides the
516.60/148.06	certificate YES(O(1),O(1)).
516.60/148.06	
516.60/148.06	Weak DPs: { c^#(b(a(), a()), b(y, z), x) -> c_3() }
516.60/148.06	Weak Trs:
516.60/148.06	  { f(c(c(a(), y, a()), b(x, z), a())) -> b(y, f(c(f(a()), z, z)))
516.60/148.06	  , f(b(b(x, f(y)), z)) -> c(z, x, f(b(b(f(a()), y), y)))
516.60/148.06	  , c(b(a(), a()), b(y, z), x) -> b(a(), b(z, z)) }
516.60/148.06	Obligation:
516.60/148.06	  innermost runtime complexity
516.60/148.06	Answer:
516.60/148.06	  YES(O(1),O(1))
516.60/148.06	
516.60/148.06	The following weak DPs constitute a sub-graph of the DG that is
516.60/148.06	closed under successors. The DPs are removed.
516.60/148.06	
516.60/148.06	{ c^#(b(a(), a()), b(y, z), x) -> c_3() }
516.60/148.06	
516.60/148.06	We are left with following problem, upon which TcT provides the
516.60/148.06	certificate YES(O(1),O(1)).
516.60/148.06	
516.60/148.06	Weak Trs:
516.60/148.06	  { f(c(c(a(), y, a()), b(x, z), a())) -> b(y, f(c(f(a()), z, z)))
516.60/148.06	  , f(b(b(x, f(y)), z)) -> c(z, x, f(b(b(f(a()), y), y)))
516.60/148.06	  , c(b(a(), a()), b(y, z), x) -> b(a(), b(z, z)) }
516.60/148.06	Obligation:
516.60/148.06	  innermost runtime complexity
516.60/148.06	Answer:
516.60/148.06	  YES(O(1),O(1))
516.60/148.06	
516.60/148.06	No rule is usable, rules are removed from the input problem.
516.60/148.06	
516.60/148.06	We are left with following problem, upon which TcT provides the
516.60/148.06	certificate YES(O(1),O(1)).
516.60/148.06	
516.60/148.06	Rules: Empty
516.60/148.06	Obligation:
516.60/148.06	  innermost runtime complexity
516.60/148.06	Answer:
516.60/148.06	  YES(O(1),O(1))
516.60/148.06	
516.60/148.06	Empty rules are trivially bounded
516.60/148.06	
516.60/148.06	Hurray, we answered YES(O(1),O(1))
516.99/148.25	EOF