(VAR a b mtmp res res' t tmp x x' y )
(STRATEGY INNERMOST)
(RULES 
        m2(S(0),b,res,True) -> False
        m2(S(S(x)),b,res,True) -> True
        m2(0,b,res,True) -> False
        m3(S(0),b,res,t) -> False
        m3(S(S(x)),b,res,t) -> True
        m3(0,b,res,t) -> False
        l8(res,y,res',True,mtmp,t) -> res
        l5(x,y,res,tmp,mtmp,True) -> 0
        help1(S(0)) -> False
        help1(S(S(x))) -> True
        e4(a,b,res,False) -> False
        e4(a,b,res,True) -> True
        e2(a,b,res,False) -> False
        l15(x,y,res,tmp,False,t) -> l16(x,y,gcd(y,0),tmp,False,t)
        l15(x,y,res,tmp,True,t) -> l16(x,y,gcd(y,S(0)),tmp,True,t)
        l13(x,y,res,tmp,False,t) -> l16(x,y,gcd(0,y),tmp,False,t)
        l13(x,y,res,tmp,True,t) -> l16(x,y,gcd(S(0),y),tmp,True,t)
        m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
        m2(a,b,res,False) -> m4(a,b,res,False)
        l8(x,y,res,False,mtmp,t) -> l10(x,y,res,False,mtmp,t)
        l5(x,y,res,tmp,mtmp,False) -> l7(x,y,res,tmp,mtmp,False)
        l2(x,y,res,tmp,mtmp,False) -> l3(x,y,res,tmp,mtmp,False)
        l2(x,y,res,tmp,mtmp,True) -> res
        l11(x,y,res,tmp,mtmp,False) -> l14(x,y,res,tmp,mtmp,False)
        l11(x,y,res,tmp,mtmp,True) -> l12(x,y,res,tmp,mtmp,True)
        help1(0) -> False
        e2(a,b,res,True) -> e3(a,b,res,True)
        bool2Nat(False) -> 0
        bool2Nat(True) -> S(0)
        m1(a,x,res,t) -> m2(a,x,res,False)
        l9(res,y,res',tmp,mtmp,t) -> res
        l6(x,y,res,tmp,mtmp,t) -> 0
        l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False)
        l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False)
        e7(a,b,res,t) -> False
        e6(a,b,res,t) -> False
        e5(a,b,res,t) -> True
        monus(a,b) -> m1(a,b,False,False)
        m5(a,b,res,t) -> res
        l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
        l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0,tmp,mtmp,t)
        l16(x,y,res,tmp,mtmp,t) -> res
        l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
        l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
        l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
        gcd(x,y) -> l1(x,y,0,False,False,False)
        equal0(a,b) -> e1(a,b,False,False)
        e8(a,b,res,t) -> res
        e3(a,b,res,t) -> e4(a,b,res,<(b,a))
        e1(a,b,res,t) -> e2(a,b,res,<(a,b))
        <(S(x),S(y)) ->= <(x,y)
        <(0,S(y)) ->= True
        <(x,0) ->= False
)