(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR x y z u tv) (RULES f0(x,y,z,u) -> f1(x,0,z,u) f1(x,y,z,u) -> f1(x-1,y+x,z,u) :|: x > 0 f1(x,y,z,u) -> f2(x,y,y,u) :|: x <= 0 f2(x,y,z,u) -> f3(x,y,z,z-1) :|: z > 0 f3(x,y,z,u) -> f3(x,y,z,u-tv) :|: u > 0 && tv > 0 f3(x,y,z,u) -> f2(x,y,z-1,u) :|: u <= 0 )