MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3)
  , active(U101(tt(), M, N)) -> mark(U102(isNatKind(M), M, N))
  , active(U102(X1, X2, X3)) -> U102(active(X1), X2, X3)
  , active(U102(tt(), M, N)) -> mark(U103(isNat(N), M, N))
  , active(isNatKind(plus(V1, V2))) -> mark(U41(isNatKind(V1), V2))
  , active(isNatKind(x(V1, V2))) -> mark(U61(isNatKind(V1), V2))
  , active(isNatKind(s(V1))) -> mark(U51(isNatKind(V1)))
  , active(isNatKind(0())) -> mark(tt())
  , active(U103(X1, X2, X3)) -> U103(active(X1), X2, X3)
  , active(U103(tt(), M, N)) -> mark(U104(isNatKind(N), M, N))
  , active(isNat(plus(V1, V2))) -> mark(U11(isNatKind(V1), V1, V2))
  , active(isNat(x(V1, V2))) -> mark(U31(isNatKind(V1), V1, V2))
  , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1))
  , active(isNat(0())) -> mark(tt())
  , active(U104(X1, X2, X3)) -> U104(active(X1), X2, X3)
  , active(U104(tt(), M, N)) -> mark(plus(x(N, M), N))
  , active(plus(X1, X2)) -> plus(X1, active(X2))
  , active(plus(X1, X2)) -> plus(active(X1), X2)
  , active(plus(N, s(M))) -> mark(U81(isNat(M), M, N))
  , active(plus(N, 0())) -> mark(U71(isNat(N), N))
  , active(x(X1, X2)) -> x(X1, active(X2))
  , active(x(X1, X2)) -> x(active(X1), X2)
  , active(x(N, s(M))) -> mark(U101(isNat(M), M, N))
  , active(x(N, 0())) -> mark(U91(isNat(N), N))
  , active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3)
  , active(U11(tt(), V1, V2)) -> mark(U12(isNatKind(V1), V1, V2))
  , active(U12(X1, X2, X3)) -> U12(active(X1), X2, X3)
  , active(U12(tt(), V1, V2)) -> mark(U13(isNatKind(V2), V1, V2))
  , active(U13(X1, X2, X3)) -> U13(active(X1), X2, X3)
  , active(U13(tt(), V1, V2)) -> mark(U14(isNatKind(V2), V1, V2))
  , active(U14(X1, X2, X3)) -> U14(active(X1), X2, X3)
  , active(U14(tt(), V1, V2)) -> mark(U15(isNat(V1), V2))
  , active(U15(X1, X2)) -> U15(active(X1), X2)
  , active(U15(tt(), V2)) -> mark(U16(isNat(V2)))
  , active(U16(X)) -> U16(active(X))
  , active(U16(tt())) -> mark(tt())
  , active(U21(X1, X2)) -> U21(active(X1), X2)
  , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1))
  , active(U22(X1, X2)) -> U22(active(X1), X2)
  , active(U22(tt(), V1)) -> mark(U23(isNat(V1)))
  , active(U23(X)) -> U23(active(X))
  , active(U23(tt())) -> mark(tt())
  , active(U31(X1, X2, X3)) -> U31(active(X1), X2, X3)
  , active(U31(tt(), V1, V2)) -> mark(U32(isNatKind(V1), V1, V2))
  , active(U32(X1, X2, X3)) -> U32(active(X1), X2, X3)
  , active(U32(tt(), V1, V2)) -> mark(U33(isNatKind(V2), V1, V2))
  , active(U33(X1, X2, X3)) -> U33(active(X1), X2, X3)
  , active(U33(tt(), V1, V2)) -> mark(U34(isNatKind(V2), V1, V2))
  , active(U34(X1, X2, X3)) -> U34(active(X1), X2, X3)
  , active(U34(tt(), V1, V2)) -> mark(U35(isNat(V1), V2))
  , active(U35(X1, X2)) -> U35(active(X1), X2)
  , active(U35(tt(), V2)) -> mark(U36(isNat(V2)))
  , active(U36(X)) -> U36(active(X))
  , active(U36(tt())) -> mark(tt())
  , active(U41(X1, X2)) -> U41(active(X1), X2)
  , active(U41(tt(), V2)) -> mark(U42(isNatKind(V2)))
  , active(U42(X)) -> U42(active(X))
  , active(U42(tt())) -> mark(tt())
  , active(U51(X)) -> U51(active(X))
  , active(U51(tt())) -> mark(tt())
  , active(U61(X1, X2)) -> U61(active(X1), X2)
  , active(U61(tt(), V2)) -> mark(U62(isNatKind(V2)))
  , active(U62(X)) -> U62(active(X))
  , active(U62(tt())) -> mark(tt())
  , active(U71(X1, X2)) -> U71(active(X1), X2)
  , active(U71(tt(), N)) -> mark(U72(isNatKind(N), N))
  , active(U72(X1, X2)) -> U72(active(X1), X2)
  , active(U72(tt(), N)) -> mark(N)
  , active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3)
  , active(U81(tt(), M, N)) -> mark(U82(isNatKind(M), M, N))
  , active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3)
  , active(U82(tt(), M, N)) -> mark(U83(isNat(N), M, N))
  , active(U83(X1, X2, X3)) -> U83(active(X1), X2, X3)
  , active(U83(tt(), M, N)) -> mark(U84(isNatKind(N), M, N))
  , active(U84(X1, X2, X3)) -> U84(active(X1), X2, X3)
  , active(U84(tt(), M, N)) -> mark(s(plus(N, M)))
  , active(s(X)) -> s(active(X))
  , active(U91(X1, X2)) -> U91(active(X1), X2)
  , active(U91(tt(), N)) -> mark(U92(isNatKind(N)))
  , active(U92(X)) -> U92(active(X))
  , active(U92(tt())) -> mark(0())
  , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3))
  , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3))
  , U102(mark(X1), X2, X3) -> mark(U102(X1, X2, X3))
  , U102(ok(X1), ok(X2), ok(X3)) -> ok(U102(X1, X2, X3))
  , isNatKind(ok(X)) -> ok(isNatKind(X))
  , U103(mark(X1), X2, X3) -> mark(U103(X1, X2, X3))
  , U103(ok(X1), ok(X2), ok(X3)) -> ok(U103(X1, X2, X3))
  , isNat(ok(X)) -> ok(isNat(X))
  , U104(mark(X1), X2, X3) -> mark(U104(X1, X2, X3))
  , U104(ok(X1), ok(X2), ok(X3)) -> ok(U104(X1, X2, X3))
  , plus(X1, mark(X2)) -> mark(plus(X1, X2))
  , plus(mark(X1), X2) -> mark(plus(X1, X2))
  , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2))
  , x(X1, mark(X2)) -> mark(x(X1, X2))
  , x(mark(X1), X2) -> mark(x(X1, X2))
  , x(ok(X1), ok(X2)) -> ok(x(X1, X2))
  , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3))
  , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3))
  , U12(mark(X1), X2, X3) -> mark(U12(X1, X2, X3))
  , U12(ok(X1), ok(X2), ok(X3)) -> ok(U12(X1, X2, X3))
  , U13(mark(X1), X2, X3) -> mark(U13(X1, X2, X3))
  , U13(ok(X1), ok(X2), ok(X3)) -> ok(U13(X1, X2, X3))
  , U14(mark(X1), X2, X3) -> mark(U14(X1, X2, X3))
  , U14(ok(X1), ok(X2), ok(X3)) -> ok(U14(X1, X2, X3))
  , U15(mark(X1), X2) -> mark(U15(X1, X2))
  , U15(ok(X1), ok(X2)) -> ok(U15(X1, X2))
  , U16(mark(X)) -> mark(U16(X))
  , U16(ok(X)) -> ok(U16(X))
  , U21(mark(X1), X2) -> mark(U21(X1, X2))
  , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2))
  , U22(mark(X1), X2) -> mark(U22(X1, X2))
  , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2))
  , U23(mark(X)) -> mark(U23(X))
  , U23(ok(X)) -> ok(U23(X))
  , U31(mark(X1), X2, X3) -> mark(U31(X1, X2, X3))
  , U31(ok(X1), ok(X2), ok(X3)) -> ok(U31(X1, X2, X3))
  , U32(mark(X1), X2, X3) -> mark(U32(X1, X2, X3))
  , U32(ok(X1), ok(X2), ok(X3)) -> ok(U32(X1, X2, X3))
  , U33(mark(X1), X2, X3) -> mark(U33(X1, X2, X3))
  , U33(ok(X1), ok(X2), ok(X3)) -> ok(U33(X1, X2, X3))
  , U34(mark(X1), X2, X3) -> mark(U34(X1, X2, X3))
  , U34(ok(X1), ok(X2), ok(X3)) -> ok(U34(X1, X2, X3))
  , U35(mark(X1), X2) -> mark(U35(X1, X2))
  , U35(ok(X1), ok(X2)) -> ok(U35(X1, X2))
  , U36(mark(X)) -> mark(U36(X))
  , U36(ok(X)) -> ok(U36(X))
  , U41(mark(X1), X2) -> mark(U41(X1, X2))
  , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2))
  , U42(mark(X)) -> mark(U42(X))
  , U42(ok(X)) -> ok(U42(X))
  , U51(mark(X)) -> mark(U51(X))
  , U51(ok(X)) -> ok(U51(X))
  , U61(mark(X1), X2) -> mark(U61(X1, X2))
  , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2))
  , U62(mark(X)) -> mark(U62(X))
  , U62(ok(X)) -> ok(U62(X))
  , U71(mark(X1), X2) -> mark(U71(X1, X2))
  , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2))
  , U72(mark(X1), X2) -> mark(U72(X1, X2))
  , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2))
  , U81(mark(X1), X2, X3) -> mark(U81(X1, X2, X3))
  , U81(ok(X1), ok(X2), ok(X3)) -> ok(U81(X1, X2, X3))
  , U82(mark(X1), X2, X3) -> mark(U82(X1, X2, X3))
  , U82(ok(X1), ok(X2), ok(X3)) -> ok(U82(X1, X2, X3))
  , U83(mark(X1), X2, X3) -> mark(U83(X1, X2, X3))
  , U83(ok(X1), ok(X2), ok(X3)) -> ok(U83(X1, X2, X3))
  , U84(mark(X1), X2, X3) -> mark(U84(X1, X2, X3))
  , U84(ok(X1), ok(X2), ok(X3)) -> ok(U84(X1, X2, X3))
  , s(mark(X)) -> mark(s(X))
  , s(ok(X)) -> ok(s(X))
  , U91(mark(X1), X2) -> mark(U91(X1, X2))
  , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2))
  , U92(mark(X)) -> mark(U92(X))
  , U92(ok(X)) -> ok(U92(X))
  , proper(U101(X1, X2, X3)) ->
    U101(proper(X1), proper(X2), proper(X3))
  , proper(tt()) -> ok(tt())
  , proper(U102(X1, X2, X3)) ->
    U102(proper(X1), proper(X2), proper(X3))
  , proper(isNatKind(X)) -> isNatKind(proper(X))
  , proper(U103(X1, X2, X3)) ->
    U103(proper(X1), proper(X2), proper(X3))
  , proper(isNat(X)) -> isNat(proper(X))
  , proper(U104(X1, X2, X3)) ->
    U104(proper(X1), proper(X2), proper(X3))
  , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2))
  , proper(x(X1, X2)) -> x(proper(X1), proper(X2))
  , proper(U11(X1, X2, X3)) ->
    U11(proper(X1), proper(X2), proper(X3))
  , proper(U12(X1, X2, X3)) ->
    U12(proper(X1), proper(X2), proper(X3))
  , proper(U13(X1, X2, X3)) ->
    U13(proper(X1), proper(X2), proper(X3))
  , proper(U14(X1, X2, X3)) ->
    U14(proper(X1), proper(X2), proper(X3))
  , proper(U15(X1, X2)) -> U15(proper(X1), proper(X2))
  , proper(U16(X)) -> U16(proper(X))
  , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2))
  , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2))
  , proper(U23(X)) -> U23(proper(X))
  , proper(U31(X1, X2, X3)) ->
    U31(proper(X1), proper(X2), proper(X3))
  , proper(U32(X1, X2, X3)) ->
    U32(proper(X1), proper(X2), proper(X3))
  , proper(U33(X1, X2, X3)) ->
    U33(proper(X1), proper(X2), proper(X3))
  , proper(U34(X1, X2, X3)) ->
    U34(proper(X1), proper(X2), proper(X3))
  , proper(U35(X1, X2)) -> U35(proper(X1), proper(X2))
  , proper(U36(X)) -> U36(proper(X))
  , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2))
  , proper(U42(X)) -> U42(proper(X))
  , proper(U51(X)) -> U51(proper(X))
  , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2))
  , proper(U62(X)) -> U62(proper(X))
  , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2))
  , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2))
  , proper(U81(X1, X2, X3)) ->
    U81(proper(X1), proper(X2), proper(X3))
  , proper(U82(X1, X2, X3)) ->
    U82(proper(X1), proper(X2), proper(X3))
  , proper(U83(X1, X2, X3)) ->
    U83(proper(X1), proper(X2), proper(X3))
  , proper(U84(X1, X2, X3)) ->
    U84(proper(X1), proper(X2), proper(X3))
  , proper(s(X)) -> s(proper(X))
  , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2))
  , proper(U92(X)) -> U92(proper(X))
  , proper(0()) -> ok(0())
  , top(mark(X)) -> top(proper(X))
  , top(ok(X)) -> top(active(X)) }
Obligation:
  runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 60 seconds)' failed due to the
   following reason:
   
   Computation stopped due to timeout after 60.0 seconds.

2) 'Best' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
      failed due to the following reason:
      
      Computation stopped due to timeout after 30.0 seconds.
   
   2) 'Best' failed due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
         following reason:
         
         The processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
      2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
         to the following reason:
         
         The processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
   
   3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
      due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'Bounds with perSymbol-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
      2) 'Bounds with minimal-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
   

3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
   due to the following reason:
   
   We add the following weak dependency pairs:
   
   Strict DPs:
     { active^#(U101(X1, X2, X3)) -> c_1(U101^#(active(X1), X2, X3))
     , active^#(U101(tt(), M, N)) -> c_2(U102^#(isNatKind(M), M, N))
     , active^#(U102(X1, X2, X3)) -> c_3(U102^#(active(X1), X2, X3))
     , active^#(U102(tt(), M, N)) -> c_4(U103^#(isNat(N), M, N))
     , active^#(isNatKind(plus(V1, V2))) ->
       c_5(U41^#(isNatKind(V1), V2))
     , active^#(isNatKind(x(V1, V2))) -> c_6(U61^#(isNatKind(V1), V2))
     , active^#(isNatKind(s(V1))) -> c_7(U51^#(isNatKind(V1)))
     , active^#(isNatKind(0())) -> c_8()
     , active^#(U103(X1, X2, X3)) -> c_9(U103^#(active(X1), X2, X3))
     , active^#(U103(tt(), M, N)) -> c_10(U104^#(isNatKind(N), M, N))
     , active^#(isNat(plus(V1, V2))) ->
       c_11(U11^#(isNatKind(V1), V1, V2))
     , active^#(isNat(x(V1, V2))) -> c_12(U31^#(isNatKind(V1), V1, V2))
     , active^#(isNat(s(V1))) -> c_13(U21^#(isNatKind(V1), V1))
     , active^#(isNat(0())) -> c_14()
     , active^#(U104(X1, X2, X3)) -> c_15(U104^#(active(X1), X2, X3))
     , active^#(U104(tt(), M, N)) -> c_16(plus^#(x(N, M), N))
     , active^#(plus(X1, X2)) -> c_17(plus^#(X1, active(X2)))
     , active^#(plus(X1, X2)) -> c_18(plus^#(active(X1), X2))
     , active^#(plus(N, s(M))) -> c_19(U81^#(isNat(M), M, N))
     , active^#(plus(N, 0())) -> c_20(U71^#(isNat(N), N))
     , active^#(x(X1, X2)) -> c_21(x^#(X1, active(X2)))
     , active^#(x(X1, X2)) -> c_22(x^#(active(X1), X2))
     , active^#(x(N, s(M))) -> c_23(U101^#(isNat(M), M, N))
     , active^#(x(N, 0())) -> c_24(U91^#(isNat(N), N))
     , active^#(U11(X1, X2, X3)) -> c_25(U11^#(active(X1), X2, X3))
     , active^#(U11(tt(), V1, V2)) -> c_26(U12^#(isNatKind(V1), V1, V2))
     , active^#(U12(X1, X2, X3)) -> c_27(U12^#(active(X1), X2, X3))
     , active^#(U12(tt(), V1, V2)) -> c_28(U13^#(isNatKind(V2), V1, V2))
     , active^#(U13(X1, X2, X3)) -> c_29(U13^#(active(X1), X2, X3))
     , active^#(U13(tt(), V1, V2)) -> c_30(U14^#(isNatKind(V2), V1, V2))
     , active^#(U14(X1, X2, X3)) -> c_31(U14^#(active(X1), X2, X3))
     , active^#(U14(tt(), V1, V2)) -> c_32(U15^#(isNat(V1), V2))
     , active^#(U15(X1, X2)) -> c_33(U15^#(active(X1), X2))
     , active^#(U15(tt(), V2)) -> c_34(U16^#(isNat(V2)))
     , active^#(U16(X)) -> c_35(U16^#(active(X)))
     , active^#(U16(tt())) -> c_36()
     , active^#(U21(X1, X2)) -> c_37(U21^#(active(X1), X2))
     , active^#(U21(tt(), V1)) -> c_38(U22^#(isNatKind(V1), V1))
     , active^#(U22(X1, X2)) -> c_39(U22^#(active(X1), X2))
     , active^#(U22(tt(), V1)) -> c_40(U23^#(isNat(V1)))
     , active^#(U23(X)) -> c_41(U23^#(active(X)))
     , active^#(U23(tt())) -> c_42()
     , active^#(U31(X1, X2, X3)) -> c_43(U31^#(active(X1), X2, X3))
     , active^#(U31(tt(), V1, V2)) -> c_44(U32^#(isNatKind(V1), V1, V2))
     , active^#(U32(X1, X2, X3)) -> c_45(U32^#(active(X1), X2, X3))
     , active^#(U32(tt(), V1, V2)) -> c_46(U33^#(isNatKind(V2), V1, V2))
     , active^#(U33(X1, X2, X3)) -> c_47(U33^#(active(X1), X2, X3))
     , active^#(U33(tt(), V1, V2)) -> c_48(U34^#(isNatKind(V2), V1, V2))
     , active^#(U34(X1, X2, X3)) -> c_49(U34^#(active(X1), X2, X3))
     , active^#(U34(tt(), V1, V2)) -> c_50(U35^#(isNat(V1), V2))
     , active^#(U35(X1, X2)) -> c_51(U35^#(active(X1), X2))
     , active^#(U35(tt(), V2)) -> c_52(U36^#(isNat(V2)))
     , active^#(U36(X)) -> c_53(U36^#(active(X)))
     , active^#(U36(tt())) -> c_54()
     , active^#(U41(X1, X2)) -> c_55(U41^#(active(X1), X2))
     , active^#(U41(tt(), V2)) -> c_56(U42^#(isNatKind(V2)))
     , active^#(U42(X)) -> c_57(U42^#(active(X)))
     , active^#(U42(tt())) -> c_58()
     , active^#(U51(X)) -> c_59(U51^#(active(X)))
     , active^#(U51(tt())) -> c_60()
     , active^#(U61(X1, X2)) -> c_61(U61^#(active(X1), X2))
     , active^#(U61(tt(), V2)) -> c_62(U62^#(isNatKind(V2)))
     , active^#(U62(X)) -> c_63(U62^#(active(X)))
     , active^#(U62(tt())) -> c_64()
     , active^#(U71(X1, X2)) -> c_65(U71^#(active(X1), X2))
     , active^#(U71(tt(), N)) -> c_66(U72^#(isNatKind(N), N))
     , active^#(U72(X1, X2)) -> c_67(U72^#(active(X1), X2))
     , active^#(U72(tt(), N)) -> c_68(N)
     , active^#(U81(X1, X2, X3)) -> c_69(U81^#(active(X1), X2, X3))
     , active^#(U81(tt(), M, N)) -> c_70(U82^#(isNatKind(M), M, N))
     , active^#(U82(X1, X2, X3)) -> c_71(U82^#(active(X1), X2, X3))
     , active^#(U82(tt(), M, N)) -> c_72(U83^#(isNat(N), M, N))
     , active^#(U83(X1, X2, X3)) -> c_73(U83^#(active(X1), X2, X3))
     , active^#(U83(tt(), M, N)) -> c_74(U84^#(isNatKind(N), M, N))
     , active^#(U84(X1, X2, X3)) -> c_75(U84^#(active(X1), X2, X3))
     , active^#(U84(tt(), M, N)) -> c_76(s^#(plus(N, M)))
     , active^#(s(X)) -> c_77(s^#(active(X)))
     , active^#(U91(X1, X2)) -> c_78(U91^#(active(X1), X2))
     , active^#(U91(tt(), N)) -> c_79(U92^#(isNatKind(N)))
     , active^#(U92(X)) -> c_80(U92^#(active(X)))
     , active^#(U92(tt())) -> c_81()
     , U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3))
     , U101^#(ok(X1), ok(X2), ok(X3)) -> c_83(U101^#(X1, X2, X3))
     , U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3))
     , U102^#(ok(X1), ok(X2), ok(X3)) -> c_85(U102^#(X1, X2, X3))
     , U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3))
     , U103^#(ok(X1), ok(X2), ok(X3)) -> c_88(U103^#(X1, X2, X3))
     , U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2))
     , U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2))
     , U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2))
     , U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2))
     , U51^#(mark(X)) -> c_132(U51^#(X))
     , U51^#(ok(X)) -> c_133(U51^#(X))
     , U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3))
     , U104^#(ok(X1), ok(X2), ok(X3)) -> c_91(U104^#(X1, X2, X3))
     , U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3))
     , U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3))
     , U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3))
     , U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3))
     , U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2))
     , U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2))
     , plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2))
     , plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2))
     , plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2))
     , U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3))
     , U81^#(ok(X1), ok(X2), ok(X3)) -> c_143(U81^#(X1, X2, X3))
     , U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2))
     , U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2))
     , x^#(X1, mark(X2)) -> c_95(x^#(X1, X2))
     , x^#(mark(X1), X2) -> c_96(x^#(X1, X2))
     , x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2))
     , U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2))
     , U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2))
     , U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3))
     , U12^#(ok(X1), ok(X2), ok(X3)) -> c_101(U12^#(X1, X2, X3))
     , U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3))
     , U13^#(ok(X1), ok(X2), ok(X3)) -> c_103(U13^#(X1, X2, X3))
     , U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3))
     , U14^#(ok(X1), ok(X2), ok(X3)) -> c_105(U14^#(X1, X2, X3))
     , U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2))
     , U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2))
     , U16^#(mark(X)) -> c_108(U16^#(X))
     , U16^#(ok(X)) -> c_109(U16^#(X))
     , U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2))
     , U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2))
     , U23^#(mark(X)) -> c_114(U23^#(X))
     , U23^#(ok(X)) -> c_115(U23^#(X))
     , U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3))
     , U32^#(ok(X1), ok(X2), ok(X3)) -> c_119(U32^#(X1, X2, X3))
     , U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3))
     , U33^#(ok(X1), ok(X2), ok(X3)) -> c_121(U33^#(X1, X2, X3))
     , U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3))
     , U34^#(ok(X1), ok(X2), ok(X3)) -> c_123(U34^#(X1, X2, X3))
     , U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2))
     , U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2))
     , U36^#(mark(X)) -> c_126(U36^#(X))
     , U36^#(ok(X)) -> c_127(U36^#(X))
     , U42^#(mark(X)) -> c_130(U42^#(X))
     , U42^#(ok(X)) -> c_131(U42^#(X))
     , U62^#(mark(X)) -> c_136(U62^#(X))
     , U62^#(ok(X)) -> c_137(U62^#(X))
     , U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2))
     , U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2))
     , U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3))
     , U82^#(ok(X1), ok(X2), ok(X3)) -> c_145(U82^#(X1, X2, X3))
     , U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3))
     , U83^#(ok(X1), ok(X2), ok(X3)) -> c_147(U83^#(X1, X2, X3))
     , U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3))
     , U84^#(ok(X1), ok(X2), ok(X3)) -> c_149(U84^#(X1, X2, X3))
     , s^#(mark(X)) -> c_150(s^#(X))
     , s^#(ok(X)) -> c_151(s^#(X))
     , U92^#(mark(X)) -> c_154(U92^#(X))
     , U92^#(ok(X)) -> c_155(U92^#(X))
     , isNatKind^#(ok(X)) -> c_86(isNatKind^#(X))
     , isNat^#(ok(X)) -> c_89(isNat^#(X))
     , proper^#(U101(X1, X2, X3)) ->
       c_156(U101^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(tt()) -> c_157()
     , proper^#(U102(X1, X2, X3)) ->
       c_158(U102^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(isNatKind(X)) -> c_159(isNatKind^#(proper(X)))
     , proper^#(U103(X1, X2, X3)) ->
       c_160(U103^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(isNat(X)) -> c_161(isNat^#(proper(X)))
     , proper^#(U104(X1, X2, X3)) ->
       c_162(U104^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(plus(X1, X2)) -> c_163(plus^#(proper(X1), proper(X2)))
     , proper^#(x(X1, X2)) -> c_164(x^#(proper(X1), proper(X2)))
     , proper^#(U11(X1, X2, X3)) ->
       c_165(U11^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U12(X1, X2, X3)) ->
       c_166(U12^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U13(X1, X2, X3)) ->
       c_167(U13^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U14(X1, X2, X3)) ->
       c_168(U14^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U15(X1, X2)) -> c_169(U15^#(proper(X1), proper(X2)))
     , proper^#(U16(X)) -> c_170(U16^#(proper(X)))
     , proper^#(U21(X1, X2)) -> c_171(U21^#(proper(X1), proper(X2)))
     , proper^#(U22(X1, X2)) -> c_172(U22^#(proper(X1), proper(X2)))
     , proper^#(U23(X)) -> c_173(U23^#(proper(X)))
     , proper^#(U31(X1, X2, X3)) ->
       c_174(U31^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U32(X1, X2, X3)) ->
       c_175(U32^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U33(X1, X2, X3)) ->
       c_176(U33^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U34(X1, X2, X3)) ->
       c_177(U34^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U35(X1, X2)) -> c_178(U35^#(proper(X1), proper(X2)))
     , proper^#(U36(X)) -> c_179(U36^#(proper(X)))
     , proper^#(U41(X1, X2)) -> c_180(U41^#(proper(X1), proper(X2)))
     , proper^#(U42(X)) -> c_181(U42^#(proper(X)))
     , proper^#(U51(X)) -> c_182(U51^#(proper(X)))
     , proper^#(U61(X1, X2)) -> c_183(U61^#(proper(X1), proper(X2)))
     , proper^#(U62(X)) -> c_184(U62^#(proper(X)))
     , proper^#(U71(X1, X2)) -> c_185(U71^#(proper(X1), proper(X2)))
     , proper^#(U72(X1, X2)) -> c_186(U72^#(proper(X1), proper(X2)))
     , proper^#(U81(X1, X2, X3)) ->
       c_187(U81^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U82(X1, X2, X3)) ->
       c_188(U82^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U83(X1, X2, X3)) ->
       c_189(U83^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U84(X1, X2, X3)) ->
       c_190(U84^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(s(X)) -> c_191(s^#(proper(X)))
     , proper^#(U91(X1, X2)) -> c_192(U91^#(proper(X1), proper(X2)))
     , proper^#(U92(X)) -> c_193(U92^#(proper(X)))
     , proper^#(0()) -> c_194()
     , top^#(mark(X)) -> c_195(top^#(proper(X)))
     , top^#(ok(X)) -> c_196(top^#(active(X))) }
   
   and mark the set of starting terms.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { active^#(U101(X1, X2, X3)) -> c_1(U101^#(active(X1), X2, X3))
     , active^#(U101(tt(), M, N)) -> c_2(U102^#(isNatKind(M), M, N))
     , active^#(U102(X1, X2, X3)) -> c_3(U102^#(active(X1), X2, X3))
     , active^#(U102(tt(), M, N)) -> c_4(U103^#(isNat(N), M, N))
     , active^#(isNatKind(plus(V1, V2))) ->
       c_5(U41^#(isNatKind(V1), V2))
     , active^#(isNatKind(x(V1, V2))) -> c_6(U61^#(isNatKind(V1), V2))
     , active^#(isNatKind(s(V1))) -> c_7(U51^#(isNatKind(V1)))
     , active^#(isNatKind(0())) -> c_8()
     , active^#(U103(X1, X2, X3)) -> c_9(U103^#(active(X1), X2, X3))
     , active^#(U103(tt(), M, N)) -> c_10(U104^#(isNatKind(N), M, N))
     , active^#(isNat(plus(V1, V2))) ->
       c_11(U11^#(isNatKind(V1), V1, V2))
     , active^#(isNat(x(V1, V2))) -> c_12(U31^#(isNatKind(V1), V1, V2))
     , active^#(isNat(s(V1))) -> c_13(U21^#(isNatKind(V1), V1))
     , active^#(isNat(0())) -> c_14()
     , active^#(U104(X1, X2, X3)) -> c_15(U104^#(active(X1), X2, X3))
     , active^#(U104(tt(), M, N)) -> c_16(plus^#(x(N, M), N))
     , active^#(plus(X1, X2)) -> c_17(plus^#(X1, active(X2)))
     , active^#(plus(X1, X2)) -> c_18(plus^#(active(X1), X2))
     , active^#(plus(N, s(M))) -> c_19(U81^#(isNat(M), M, N))
     , active^#(plus(N, 0())) -> c_20(U71^#(isNat(N), N))
     , active^#(x(X1, X2)) -> c_21(x^#(X1, active(X2)))
     , active^#(x(X1, X2)) -> c_22(x^#(active(X1), X2))
     , active^#(x(N, s(M))) -> c_23(U101^#(isNat(M), M, N))
     , active^#(x(N, 0())) -> c_24(U91^#(isNat(N), N))
     , active^#(U11(X1, X2, X3)) -> c_25(U11^#(active(X1), X2, X3))
     , active^#(U11(tt(), V1, V2)) -> c_26(U12^#(isNatKind(V1), V1, V2))
     , active^#(U12(X1, X2, X3)) -> c_27(U12^#(active(X1), X2, X3))
     , active^#(U12(tt(), V1, V2)) -> c_28(U13^#(isNatKind(V2), V1, V2))
     , active^#(U13(X1, X2, X3)) -> c_29(U13^#(active(X1), X2, X3))
     , active^#(U13(tt(), V1, V2)) -> c_30(U14^#(isNatKind(V2), V1, V2))
     , active^#(U14(X1, X2, X3)) -> c_31(U14^#(active(X1), X2, X3))
     , active^#(U14(tt(), V1, V2)) -> c_32(U15^#(isNat(V1), V2))
     , active^#(U15(X1, X2)) -> c_33(U15^#(active(X1), X2))
     , active^#(U15(tt(), V2)) -> c_34(U16^#(isNat(V2)))
     , active^#(U16(X)) -> c_35(U16^#(active(X)))
     , active^#(U16(tt())) -> c_36()
     , active^#(U21(X1, X2)) -> c_37(U21^#(active(X1), X2))
     , active^#(U21(tt(), V1)) -> c_38(U22^#(isNatKind(V1), V1))
     , active^#(U22(X1, X2)) -> c_39(U22^#(active(X1), X2))
     , active^#(U22(tt(), V1)) -> c_40(U23^#(isNat(V1)))
     , active^#(U23(X)) -> c_41(U23^#(active(X)))
     , active^#(U23(tt())) -> c_42()
     , active^#(U31(X1, X2, X3)) -> c_43(U31^#(active(X1), X2, X3))
     , active^#(U31(tt(), V1, V2)) -> c_44(U32^#(isNatKind(V1), V1, V2))
     , active^#(U32(X1, X2, X3)) -> c_45(U32^#(active(X1), X2, X3))
     , active^#(U32(tt(), V1, V2)) -> c_46(U33^#(isNatKind(V2), V1, V2))
     , active^#(U33(X1, X2, X3)) -> c_47(U33^#(active(X1), X2, X3))
     , active^#(U33(tt(), V1, V2)) -> c_48(U34^#(isNatKind(V2), V1, V2))
     , active^#(U34(X1, X2, X3)) -> c_49(U34^#(active(X1), X2, X3))
     , active^#(U34(tt(), V1, V2)) -> c_50(U35^#(isNat(V1), V2))
     , active^#(U35(X1, X2)) -> c_51(U35^#(active(X1), X2))
     , active^#(U35(tt(), V2)) -> c_52(U36^#(isNat(V2)))
     , active^#(U36(X)) -> c_53(U36^#(active(X)))
     , active^#(U36(tt())) -> c_54()
     , active^#(U41(X1, X2)) -> c_55(U41^#(active(X1), X2))
     , active^#(U41(tt(), V2)) -> c_56(U42^#(isNatKind(V2)))
     , active^#(U42(X)) -> c_57(U42^#(active(X)))
     , active^#(U42(tt())) -> c_58()
     , active^#(U51(X)) -> c_59(U51^#(active(X)))
     , active^#(U51(tt())) -> c_60()
     , active^#(U61(X1, X2)) -> c_61(U61^#(active(X1), X2))
     , active^#(U61(tt(), V2)) -> c_62(U62^#(isNatKind(V2)))
     , active^#(U62(X)) -> c_63(U62^#(active(X)))
     , active^#(U62(tt())) -> c_64()
     , active^#(U71(X1, X2)) -> c_65(U71^#(active(X1), X2))
     , active^#(U71(tt(), N)) -> c_66(U72^#(isNatKind(N), N))
     , active^#(U72(X1, X2)) -> c_67(U72^#(active(X1), X2))
     , active^#(U72(tt(), N)) -> c_68(N)
     , active^#(U81(X1, X2, X3)) -> c_69(U81^#(active(X1), X2, X3))
     , active^#(U81(tt(), M, N)) -> c_70(U82^#(isNatKind(M), M, N))
     , active^#(U82(X1, X2, X3)) -> c_71(U82^#(active(X1), X2, X3))
     , active^#(U82(tt(), M, N)) -> c_72(U83^#(isNat(N), M, N))
     , active^#(U83(X1, X2, X3)) -> c_73(U83^#(active(X1), X2, X3))
     , active^#(U83(tt(), M, N)) -> c_74(U84^#(isNatKind(N), M, N))
     , active^#(U84(X1, X2, X3)) -> c_75(U84^#(active(X1), X2, X3))
     , active^#(U84(tt(), M, N)) -> c_76(s^#(plus(N, M)))
     , active^#(s(X)) -> c_77(s^#(active(X)))
     , active^#(U91(X1, X2)) -> c_78(U91^#(active(X1), X2))
     , active^#(U91(tt(), N)) -> c_79(U92^#(isNatKind(N)))
     , active^#(U92(X)) -> c_80(U92^#(active(X)))
     , active^#(U92(tt())) -> c_81()
     , U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3))
     , U101^#(ok(X1), ok(X2), ok(X3)) -> c_83(U101^#(X1, X2, X3))
     , U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3))
     , U102^#(ok(X1), ok(X2), ok(X3)) -> c_85(U102^#(X1, X2, X3))
     , U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3))
     , U103^#(ok(X1), ok(X2), ok(X3)) -> c_88(U103^#(X1, X2, X3))
     , U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2))
     , U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2))
     , U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2))
     , U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2))
     , U51^#(mark(X)) -> c_132(U51^#(X))
     , U51^#(ok(X)) -> c_133(U51^#(X))
     , U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3))
     , U104^#(ok(X1), ok(X2), ok(X3)) -> c_91(U104^#(X1, X2, X3))
     , U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3))
     , U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3))
     , U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3))
     , U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3))
     , U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2))
     , U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2))
     , plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2))
     , plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2))
     , plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2))
     , U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3))
     , U81^#(ok(X1), ok(X2), ok(X3)) -> c_143(U81^#(X1, X2, X3))
     , U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2))
     , U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2))
     , x^#(X1, mark(X2)) -> c_95(x^#(X1, X2))
     , x^#(mark(X1), X2) -> c_96(x^#(X1, X2))
     , x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2))
     , U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2))
     , U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2))
     , U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3))
     , U12^#(ok(X1), ok(X2), ok(X3)) -> c_101(U12^#(X1, X2, X3))
     , U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3))
     , U13^#(ok(X1), ok(X2), ok(X3)) -> c_103(U13^#(X1, X2, X3))
     , U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3))
     , U14^#(ok(X1), ok(X2), ok(X3)) -> c_105(U14^#(X1, X2, X3))
     , U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2))
     , U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2))
     , U16^#(mark(X)) -> c_108(U16^#(X))
     , U16^#(ok(X)) -> c_109(U16^#(X))
     , U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2))
     , U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2))
     , U23^#(mark(X)) -> c_114(U23^#(X))
     , U23^#(ok(X)) -> c_115(U23^#(X))
     , U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3))
     , U32^#(ok(X1), ok(X2), ok(X3)) -> c_119(U32^#(X1, X2, X3))
     , U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3))
     , U33^#(ok(X1), ok(X2), ok(X3)) -> c_121(U33^#(X1, X2, X3))
     , U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3))
     , U34^#(ok(X1), ok(X2), ok(X3)) -> c_123(U34^#(X1, X2, X3))
     , U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2))
     , U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2))
     , U36^#(mark(X)) -> c_126(U36^#(X))
     , U36^#(ok(X)) -> c_127(U36^#(X))
     , U42^#(mark(X)) -> c_130(U42^#(X))
     , U42^#(ok(X)) -> c_131(U42^#(X))
     , U62^#(mark(X)) -> c_136(U62^#(X))
     , U62^#(ok(X)) -> c_137(U62^#(X))
     , U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2))
     , U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2))
     , U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3))
     , U82^#(ok(X1), ok(X2), ok(X3)) -> c_145(U82^#(X1, X2, X3))
     , U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3))
     , U83^#(ok(X1), ok(X2), ok(X3)) -> c_147(U83^#(X1, X2, X3))
     , U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3))
     , U84^#(ok(X1), ok(X2), ok(X3)) -> c_149(U84^#(X1, X2, X3))
     , s^#(mark(X)) -> c_150(s^#(X))
     , s^#(ok(X)) -> c_151(s^#(X))
     , U92^#(mark(X)) -> c_154(U92^#(X))
     , U92^#(ok(X)) -> c_155(U92^#(X))
     , isNatKind^#(ok(X)) -> c_86(isNatKind^#(X))
     , isNat^#(ok(X)) -> c_89(isNat^#(X))
     , proper^#(U101(X1, X2, X3)) ->
       c_156(U101^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(tt()) -> c_157()
     , proper^#(U102(X1, X2, X3)) ->
       c_158(U102^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(isNatKind(X)) -> c_159(isNatKind^#(proper(X)))
     , proper^#(U103(X1, X2, X3)) ->
       c_160(U103^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(isNat(X)) -> c_161(isNat^#(proper(X)))
     , proper^#(U104(X1, X2, X3)) ->
       c_162(U104^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(plus(X1, X2)) -> c_163(plus^#(proper(X1), proper(X2)))
     , proper^#(x(X1, X2)) -> c_164(x^#(proper(X1), proper(X2)))
     , proper^#(U11(X1, X2, X3)) ->
       c_165(U11^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U12(X1, X2, X3)) ->
       c_166(U12^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U13(X1, X2, X3)) ->
       c_167(U13^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U14(X1, X2, X3)) ->
       c_168(U14^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U15(X1, X2)) -> c_169(U15^#(proper(X1), proper(X2)))
     , proper^#(U16(X)) -> c_170(U16^#(proper(X)))
     , proper^#(U21(X1, X2)) -> c_171(U21^#(proper(X1), proper(X2)))
     , proper^#(U22(X1, X2)) -> c_172(U22^#(proper(X1), proper(X2)))
     , proper^#(U23(X)) -> c_173(U23^#(proper(X)))
     , proper^#(U31(X1, X2, X3)) ->
       c_174(U31^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U32(X1, X2, X3)) ->
       c_175(U32^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U33(X1, X2, X3)) ->
       c_176(U33^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U34(X1, X2, X3)) ->
       c_177(U34^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U35(X1, X2)) -> c_178(U35^#(proper(X1), proper(X2)))
     , proper^#(U36(X)) -> c_179(U36^#(proper(X)))
     , proper^#(U41(X1, X2)) -> c_180(U41^#(proper(X1), proper(X2)))
     , proper^#(U42(X)) -> c_181(U42^#(proper(X)))
     , proper^#(U51(X)) -> c_182(U51^#(proper(X)))
     , proper^#(U61(X1, X2)) -> c_183(U61^#(proper(X1), proper(X2)))
     , proper^#(U62(X)) -> c_184(U62^#(proper(X)))
     , proper^#(U71(X1, X2)) -> c_185(U71^#(proper(X1), proper(X2)))
     , proper^#(U72(X1, X2)) -> c_186(U72^#(proper(X1), proper(X2)))
     , proper^#(U81(X1, X2, X3)) ->
       c_187(U81^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U82(X1, X2, X3)) ->
       c_188(U82^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U83(X1, X2, X3)) ->
       c_189(U83^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(U84(X1, X2, X3)) ->
       c_190(U84^#(proper(X1), proper(X2), proper(X3)))
     , proper^#(s(X)) -> c_191(s^#(proper(X)))
     , proper^#(U91(X1, X2)) -> c_192(U91^#(proper(X1), proper(X2)))
     , proper^#(U92(X)) -> c_193(U92^#(proper(X)))
     , proper^#(0()) -> c_194()
     , top^#(mark(X)) -> c_195(top^#(proper(X)))
     , top^#(ok(X)) -> c_196(top^#(active(X))) }
   Strict Trs:
     { active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3)
     , active(U101(tt(), M, N)) -> mark(U102(isNatKind(M), M, N))
     , active(U102(X1, X2, X3)) -> U102(active(X1), X2, X3)
     , active(U102(tt(), M, N)) -> mark(U103(isNat(N), M, N))
     , active(isNatKind(plus(V1, V2))) -> mark(U41(isNatKind(V1), V2))
     , active(isNatKind(x(V1, V2))) -> mark(U61(isNatKind(V1), V2))
     , active(isNatKind(s(V1))) -> mark(U51(isNatKind(V1)))
     , active(isNatKind(0())) -> mark(tt())
     , active(U103(X1, X2, X3)) -> U103(active(X1), X2, X3)
     , active(U103(tt(), M, N)) -> mark(U104(isNatKind(N), M, N))
     , active(isNat(plus(V1, V2))) -> mark(U11(isNatKind(V1), V1, V2))
     , active(isNat(x(V1, V2))) -> mark(U31(isNatKind(V1), V1, V2))
     , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1))
     , active(isNat(0())) -> mark(tt())
     , active(U104(X1, X2, X3)) -> U104(active(X1), X2, X3)
     , active(U104(tt(), M, N)) -> mark(plus(x(N, M), N))
     , active(plus(X1, X2)) -> plus(X1, active(X2))
     , active(plus(X1, X2)) -> plus(active(X1), X2)
     , active(plus(N, s(M))) -> mark(U81(isNat(M), M, N))
     , active(plus(N, 0())) -> mark(U71(isNat(N), N))
     , active(x(X1, X2)) -> x(X1, active(X2))
     , active(x(X1, X2)) -> x(active(X1), X2)
     , active(x(N, s(M))) -> mark(U101(isNat(M), M, N))
     , active(x(N, 0())) -> mark(U91(isNat(N), N))
     , active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3)
     , active(U11(tt(), V1, V2)) -> mark(U12(isNatKind(V1), V1, V2))
     , active(U12(X1, X2, X3)) -> U12(active(X1), X2, X3)
     , active(U12(tt(), V1, V2)) -> mark(U13(isNatKind(V2), V1, V2))
     , active(U13(X1, X2, X3)) -> U13(active(X1), X2, X3)
     , active(U13(tt(), V1, V2)) -> mark(U14(isNatKind(V2), V1, V2))
     , active(U14(X1, X2, X3)) -> U14(active(X1), X2, X3)
     , active(U14(tt(), V1, V2)) -> mark(U15(isNat(V1), V2))
     , active(U15(X1, X2)) -> U15(active(X1), X2)
     , active(U15(tt(), V2)) -> mark(U16(isNat(V2)))
     , active(U16(X)) -> U16(active(X))
     , active(U16(tt())) -> mark(tt())
     , active(U21(X1, X2)) -> U21(active(X1), X2)
     , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1))
     , active(U22(X1, X2)) -> U22(active(X1), X2)
     , active(U22(tt(), V1)) -> mark(U23(isNat(V1)))
     , active(U23(X)) -> U23(active(X))
     , active(U23(tt())) -> mark(tt())
     , active(U31(X1, X2, X3)) -> U31(active(X1), X2, X3)
     , active(U31(tt(), V1, V2)) -> mark(U32(isNatKind(V1), V1, V2))
     , active(U32(X1, X2, X3)) -> U32(active(X1), X2, X3)
     , active(U32(tt(), V1, V2)) -> mark(U33(isNatKind(V2), V1, V2))
     , active(U33(X1, X2, X3)) -> U33(active(X1), X2, X3)
     , active(U33(tt(), V1, V2)) -> mark(U34(isNatKind(V2), V1, V2))
     , active(U34(X1, X2, X3)) -> U34(active(X1), X2, X3)
     , active(U34(tt(), V1, V2)) -> mark(U35(isNat(V1), V2))
     , active(U35(X1, X2)) -> U35(active(X1), X2)
     , active(U35(tt(), V2)) -> mark(U36(isNat(V2)))
     , active(U36(X)) -> U36(active(X))
     , active(U36(tt())) -> mark(tt())
     , active(U41(X1, X2)) -> U41(active(X1), X2)
     , active(U41(tt(), V2)) -> mark(U42(isNatKind(V2)))
     , active(U42(X)) -> U42(active(X))
     , active(U42(tt())) -> mark(tt())
     , active(U51(X)) -> U51(active(X))
     , active(U51(tt())) -> mark(tt())
     , active(U61(X1, X2)) -> U61(active(X1), X2)
     , active(U61(tt(), V2)) -> mark(U62(isNatKind(V2)))
     , active(U62(X)) -> U62(active(X))
     , active(U62(tt())) -> mark(tt())
     , active(U71(X1, X2)) -> U71(active(X1), X2)
     , active(U71(tt(), N)) -> mark(U72(isNatKind(N), N))
     , active(U72(X1, X2)) -> U72(active(X1), X2)
     , active(U72(tt(), N)) -> mark(N)
     , active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3)
     , active(U81(tt(), M, N)) -> mark(U82(isNatKind(M), M, N))
     , active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3)
     , active(U82(tt(), M, N)) -> mark(U83(isNat(N), M, N))
     , active(U83(X1, X2, X3)) -> U83(active(X1), X2, X3)
     , active(U83(tt(), M, N)) -> mark(U84(isNatKind(N), M, N))
     , active(U84(X1, X2, X3)) -> U84(active(X1), X2, X3)
     , active(U84(tt(), M, N)) -> mark(s(plus(N, M)))
     , active(s(X)) -> s(active(X))
     , active(U91(X1, X2)) -> U91(active(X1), X2)
     , active(U91(tt(), N)) -> mark(U92(isNatKind(N)))
     , active(U92(X)) -> U92(active(X))
     , active(U92(tt())) -> mark(0())
     , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3))
     , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3))
     , U102(mark(X1), X2, X3) -> mark(U102(X1, X2, X3))
     , U102(ok(X1), ok(X2), ok(X3)) -> ok(U102(X1, X2, X3))
     , isNatKind(ok(X)) -> ok(isNatKind(X))
     , U103(mark(X1), X2, X3) -> mark(U103(X1, X2, X3))
     , U103(ok(X1), ok(X2), ok(X3)) -> ok(U103(X1, X2, X3))
     , isNat(ok(X)) -> ok(isNat(X))
     , U104(mark(X1), X2, X3) -> mark(U104(X1, X2, X3))
     , U104(ok(X1), ok(X2), ok(X3)) -> ok(U104(X1, X2, X3))
     , plus(X1, mark(X2)) -> mark(plus(X1, X2))
     , plus(mark(X1), X2) -> mark(plus(X1, X2))
     , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2))
     , x(X1, mark(X2)) -> mark(x(X1, X2))
     , x(mark(X1), X2) -> mark(x(X1, X2))
     , x(ok(X1), ok(X2)) -> ok(x(X1, X2))
     , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3))
     , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3))
     , U12(mark(X1), X2, X3) -> mark(U12(X1, X2, X3))
     , U12(ok(X1), ok(X2), ok(X3)) -> ok(U12(X1, X2, X3))
     , U13(mark(X1), X2, X3) -> mark(U13(X1, X2, X3))
     , U13(ok(X1), ok(X2), ok(X3)) -> ok(U13(X1, X2, X3))
     , U14(mark(X1), X2, X3) -> mark(U14(X1, X2, X3))
     , U14(ok(X1), ok(X2), ok(X3)) -> ok(U14(X1, X2, X3))
     , U15(mark(X1), X2) -> mark(U15(X1, X2))
     , U15(ok(X1), ok(X2)) -> ok(U15(X1, X2))
     , U16(mark(X)) -> mark(U16(X))
     , U16(ok(X)) -> ok(U16(X))
     , U21(mark(X1), X2) -> mark(U21(X1, X2))
     , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2))
     , U22(mark(X1), X2) -> mark(U22(X1, X2))
     , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2))
     , U23(mark(X)) -> mark(U23(X))
     , U23(ok(X)) -> ok(U23(X))
     , U31(mark(X1), X2, X3) -> mark(U31(X1, X2, X3))
     , U31(ok(X1), ok(X2), ok(X3)) -> ok(U31(X1, X2, X3))
     , U32(mark(X1), X2, X3) -> mark(U32(X1, X2, X3))
     , U32(ok(X1), ok(X2), ok(X3)) -> ok(U32(X1, X2, X3))
     , U33(mark(X1), X2, X3) -> mark(U33(X1, X2, X3))
     , U33(ok(X1), ok(X2), ok(X3)) -> ok(U33(X1, X2, X3))
     , U34(mark(X1), X2, X3) -> mark(U34(X1, X2, X3))
     , U34(ok(X1), ok(X2), ok(X3)) -> ok(U34(X1, X2, X3))
     , U35(mark(X1), X2) -> mark(U35(X1, X2))
     , U35(ok(X1), ok(X2)) -> ok(U35(X1, X2))
     , U36(mark(X)) -> mark(U36(X))
     , U36(ok(X)) -> ok(U36(X))
     , U41(mark(X1), X2) -> mark(U41(X1, X2))
     , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2))
     , U42(mark(X)) -> mark(U42(X))
     , U42(ok(X)) -> ok(U42(X))
     , U51(mark(X)) -> mark(U51(X))
     , U51(ok(X)) -> ok(U51(X))
     , U61(mark(X1), X2) -> mark(U61(X1, X2))
     , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2))
     , U62(mark(X)) -> mark(U62(X))
     , U62(ok(X)) -> ok(U62(X))
     , U71(mark(X1), X2) -> mark(U71(X1, X2))
     , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2))
     , U72(mark(X1), X2) -> mark(U72(X1, X2))
     , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2))
     , U81(mark(X1), X2, X3) -> mark(U81(X1, X2, X3))
     , U81(ok(X1), ok(X2), ok(X3)) -> ok(U81(X1, X2, X3))
     , U82(mark(X1), X2, X3) -> mark(U82(X1, X2, X3))
     , U82(ok(X1), ok(X2), ok(X3)) -> ok(U82(X1, X2, X3))
     , U83(mark(X1), X2, X3) -> mark(U83(X1, X2, X3))
     , U83(ok(X1), ok(X2), ok(X3)) -> ok(U83(X1, X2, X3))
     , U84(mark(X1), X2, X3) -> mark(U84(X1, X2, X3))
     , U84(ok(X1), ok(X2), ok(X3)) -> ok(U84(X1, X2, X3))
     , s(mark(X)) -> mark(s(X))
     , s(ok(X)) -> ok(s(X))
     , U91(mark(X1), X2) -> mark(U91(X1, X2))
     , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2))
     , U92(mark(X)) -> mark(U92(X))
     , U92(ok(X)) -> ok(U92(X))
     , proper(U101(X1, X2, X3)) ->
       U101(proper(X1), proper(X2), proper(X3))
     , proper(tt()) -> ok(tt())
     , proper(U102(X1, X2, X3)) ->
       U102(proper(X1), proper(X2), proper(X3))
     , proper(isNatKind(X)) -> isNatKind(proper(X))
     , proper(U103(X1, X2, X3)) ->
       U103(proper(X1), proper(X2), proper(X3))
     , proper(isNat(X)) -> isNat(proper(X))
     , proper(U104(X1, X2, X3)) ->
       U104(proper(X1), proper(X2), proper(X3))
     , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2))
     , proper(x(X1, X2)) -> x(proper(X1), proper(X2))
     , proper(U11(X1, X2, X3)) ->
       U11(proper(X1), proper(X2), proper(X3))
     , proper(U12(X1, X2, X3)) ->
       U12(proper(X1), proper(X2), proper(X3))
     , proper(U13(X1, X2, X3)) ->
       U13(proper(X1), proper(X2), proper(X3))
     , proper(U14(X1, X2, X3)) ->
       U14(proper(X1), proper(X2), proper(X3))
     , proper(U15(X1, X2)) -> U15(proper(X1), proper(X2))
     , proper(U16(X)) -> U16(proper(X))
     , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2))
     , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2))
     , proper(U23(X)) -> U23(proper(X))
     , proper(U31(X1, X2, X3)) ->
       U31(proper(X1), proper(X2), proper(X3))
     , proper(U32(X1, X2, X3)) ->
       U32(proper(X1), proper(X2), proper(X3))
     , proper(U33(X1, X2, X3)) ->
       U33(proper(X1), proper(X2), proper(X3))
     , proper(U34(X1, X2, X3)) ->
       U34(proper(X1), proper(X2), proper(X3))
     , proper(U35(X1, X2)) -> U35(proper(X1), proper(X2))
     , proper(U36(X)) -> U36(proper(X))
     , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2))
     , proper(U42(X)) -> U42(proper(X))
     , proper(U51(X)) -> U51(proper(X))
     , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2))
     , proper(U62(X)) -> U62(proper(X))
     , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2))
     , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2))
     , proper(U81(X1, X2, X3)) ->
       U81(proper(X1), proper(X2), proper(X3))
     , proper(U82(X1, X2, X3)) ->
       U82(proper(X1), proper(X2), proper(X3))
     , proper(U83(X1, X2, X3)) ->
       U83(proper(X1), proper(X2), proper(X3))
     , proper(U84(X1, X2, X3)) ->
       U84(proper(X1), proper(X2), proper(X3))
     , proper(s(X)) -> s(proper(X))
     , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2))
     , proper(U92(X)) -> U92(proper(X))
     , proper(0()) -> ok(0())
     , top(mark(X)) -> top(proper(X))
     , top(ok(X)) -> top(active(X)) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Consider the dependency graph:
   
     1: active^#(U101(X1, X2, X3)) -> c_1(U101^#(active(X1), X2, X3))
        -->_1 U101^#(ok(X1), ok(X2), ok(X3)) ->
              c_83(U101^#(X1, X2, X3)) :83
        -->_1 U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) :82
     
     2: active^#(U101(tt(), M, N)) -> c_2(U102^#(isNatKind(M), M, N))
        -->_1 U102^#(ok(X1), ok(X2), ok(X3)) ->
              c_85(U102^#(X1, X2, X3)) :85
        -->_1 U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) :84
     
     3: active^#(U102(X1, X2, X3)) -> c_3(U102^#(active(X1), X2, X3))
        -->_1 U102^#(ok(X1), ok(X2), ok(X3)) ->
              c_85(U102^#(X1, X2, X3)) :85
        -->_1 U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) :84
     
     4: active^#(U102(tt(), M, N)) -> c_4(U103^#(isNat(N), M, N))
        -->_1 U103^#(ok(X1), ok(X2), ok(X3)) ->
              c_88(U103^#(X1, X2, X3)) :87
        -->_1 U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) :86
     
     5: active^#(isNatKind(plus(V1, V2))) ->
        c_5(U41^#(isNatKind(V1), V2))
        -->_1 U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) :89
        -->_1 U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) :88
     
     6: active^#(isNatKind(x(V1, V2))) -> c_6(U61^#(isNatKind(V1), V2))
        -->_1 U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) :91
        -->_1 U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) :90
     
     7: active^#(isNatKind(s(V1))) -> c_7(U51^#(isNatKind(V1)))
        -->_1 U51^#(ok(X)) -> c_133(U51^#(X)) :93
        -->_1 U51^#(mark(X)) -> c_132(U51^#(X)) :92
     
     8: active^#(isNatKind(0())) -> c_8()
     
     9: active^#(U103(X1, X2, X3)) -> c_9(U103^#(active(X1), X2, X3))
        -->_1 U103^#(ok(X1), ok(X2), ok(X3)) ->
              c_88(U103^#(X1, X2, X3)) :87
        -->_1 U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) :86
     
     10: active^#(U103(tt(), M, N)) -> c_10(U104^#(isNatKind(N), M, N))
        -->_1 U104^#(ok(X1), ok(X2), ok(X3)) ->
              c_91(U104^#(X1, X2, X3)) :95
        -->_1 U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) :94
     
     11: active^#(isNat(plus(V1, V2))) ->
         c_11(U11^#(isNatKind(V1), V1, V2))
        -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) :97
        -->_1 U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) :96
     
     12: active^#(isNat(x(V1, V2))) ->
         c_12(U31^#(isNatKind(V1), V1, V2))
        -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) :99
        -->_1 U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) :98
     
     13: active^#(isNat(s(V1))) -> c_13(U21^#(isNatKind(V1), V1))
        -->_1 U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) :101
        -->_1 U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) :100
     
     14: active^#(isNat(0())) -> c_14()
     
     15: active^#(U104(X1, X2, X3)) -> c_15(U104^#(active(X1), X2, X3))
        -->_1 U104^#(ok(X1), ok(X2), ok(X3)) ->
              c_91(U104^#(X1, X2, X3)) :95
        -->_1 U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) :94
     
     16: active^#(U104(tt(), M, N)) -> c_16(plus^#(x(N, M), N))
        -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104
        -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103
        -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102
     
     17: active^#(plus(X1, X2)) -> c_17(plus^#(X1, active(X2)))
        -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104
        -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103
        -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102
     
     18: active^#(plus(X1, X2)) -> c_18(plus^#(active(X1), X2))
        -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104
        -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103
        -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102
     
     19: active^#(plus(N, s(M))) -> c_19(U81^#(isNat(M), M, N))
        -->_1 U81^#(ok(X1), ok(X2), ok(X3)) ->
              c_143(U81^#(X1, X2, X3)) :106
        -->_1 U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) :105
     
     20: active^#(plus(N, 0())) -> c_20(U71^#(isNat(N), N))
        -->_1 U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) :108
        -->_1 U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) :107
     
     21: active^#(x(X1, X2)) -> c_21(x^#(X1, active(X2)))
        -->_1 x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) :111
        -->_1 x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) :110
        -->_1 x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) :109
     
     22: active^#(x(X1, X2)) -> c_22(x^#(active(X1), X2))
        -->_1 x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) :111
        -->_1 x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) :110
        -->_1 x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) :109
     
     23: active^#(x(N, s(M))) -> c_23(U101^#(isNat(M), M, N))
        -->_1 U101^#(ok(X1), ok(X2), ok(X3)) ->
              c_83(U101^#(X1, X2, X3)) :83
        -->_1 U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) :82
     
     24: active^#(x(N, 0())) -> c_24(U91^#(isNat(N), N))
        -->_1 U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) :113
        -->_1 U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) :112
     
     25: active^#(U11(X1, X2, X3)) -> c_25(U11^#(active(X1), X2, X3))
        -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) :97
        -->_1 U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) :96
     
     26: active^#(U11(tt(), V1, V2)) ->
         c_26(U12^#(isNatKind(V1), V1, V2))
        -->_1 U12^#(ok(X1), ok(X2), ok(X3)) ->
              c_101(U12^#(X1, X2, X3)) :115
        -->_1 U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) :114
     
     27: active^#(U12(X1, X2, X3)) -> c_27(U12^#(active(X1), X2, X3))
        -->_1 U12^#(ok(X1), ok(X2), ok(X3)) ->
              c_101(U12^#(X1, X2, X3)) :115
        -->_1 U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) :114
     
     28: active^#(U12(tt(), V1, V2)) ->
         c_28(U13^#(isNatKind(V2), V1, V2))
        -->_1 U13^#(ok(X1), ok(X2), ok(X3)) ->
              c_103(U13^#(X1, X2, X3)) :117
        -->_1 U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) :116
     
     29: active^#(U13(X1, X2, X3)) -> c_29(U13^#(active(X1), X2, X3))
        -->_1 U13^#(ok(X1), ok(X2), ok(X3)) ->
              c_103(U13^#(X1, X2, X3)) :117
        -->_1 U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) :116
     
     30: active^#(U13(tt(), V1, V2)) ->
         c_30(U14^#(isNatKind(V2), V1, V2))
        -->_1 U14^#(ok(X1), ok(X2), ok(X3)) ->
              c_105(U14^#(X1, X2, X3)) :119
        -->_1 U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) :118
     
     31: active^#(U14(X1, X2, X3)) -> c_31(U14^#(active(X1), X2, X3))
        -->_1 U14^#(ok(X1), ok(X2), ok(X3)) ->
              c_105(U14^#(X1, X2, X3)) :119
        -->_1 U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) :118
     
     32: active^#(U14(tt(), V1, V2)) -> c_32(U15^#(isNat(V1), V2))
        -->_1 U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) :121
        -->_1 U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) :120
     
     33: active^#(U15(X1, X2)) -> c_33(U15^#(active(X1), X2))
        -->_1 U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) :121
        -->_1 U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) :120
     
     34: active^#(U15(tt(), V2)) -> c_34(U16^#(isNat(V2)))
        -->_1 U16^#(ok(X)) -> c_109(U16^#(X)) :123
        -->_1 U16^#(mark(X)) -> c_108(U16^#(X)) :122
     
     35: active^#(U16(X)) -> c_35(U16^#(active(X)))
        -->_1 U16^#(ok(X)) -> c_109(U16^#(X)) :123
        -->_1 U16^#(mark(X)) -> c_108(U16^#(X)) :122
     
     36: active^#(U16(tt())) -> c_36()
     
     37: active^#(U21(X1, X2)) -> c_37(U21^#(active(X1), X2))
        -->_1 U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) :101
        -->_1 U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) :100
     
     38: active^#(U21(tt(), V1)) -> c_38(U22^#(isNatKind(V1), V1))
        -->_1 U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) :125
        -->_1 U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) :124
     
     39: active^#(U22(X1, X2)) -> c_39(U22^#(active(X1), X2))
        -->_1 U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) :125
        -->_1 U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) :124
     
     40: active^#(U22(tt(), V1)) -> c_40(U23^#(isNat(V1)))
        -->_1 U23^#(ok(X)) -> c_115(U23^#(X)) :127
        -->_1 U23^#(mark(X)) -> c_114(U23^#(X)) :126
     
     41: active^#(U23(X)) -> c_41(U23^#(active(X)))
        -->_1 U23^#(ok(X)) -> c_115(U23^#(X)) :127
        -->_1 U23^#(mark(X)) -> c_114(U23^#(X)) :126
     
     42: active^#(U23(tt())) -> c_42()
     
     43: active^#(U31(X1, X2, X3)) -> c_43(U31^#(active(X1), X2, X3))
        -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) :99
        -->_1 U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) :98
     
     44: active^#(U31(tt(), V1, V2)) ->
         c_44(U32^#(isNatKind(V1), V1, V2))
        -->_1 U32^#(ok(X1), ok(X2), ok(X3)) ->
              c_119(U32^#(X1, X2, X3)) :129
        -->_1 U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) :128
     
     45: active^#(U32(X1, X2, X3)) -> c_45(U32^#(active(X1), X2, X3))
        -->_1 U32^#(ok(X1), ok(X2), ok(X3)) ->
              c_119(U32^#(X1, X2, X3)) :129
        -->_1 U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) :128
     
     46: active^#(U32(tt(), V1, V2)) ->
         c_46(U33^#(isNatKind(V2), V1, V2))
        -->_1 U33^#(ok(X1), ok(X2), ok(X3)) ->
              c_121(U33^#(X1, X2, X3)) :131
        -->_1 U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) :130
     
     47: active^#(U33(X1, X2, X3)) -> c_47(U33^#(active(X1), X2, X3))
        -->_1 U33^#(ok(X1), ok(X2), ok(X3)) ->
              c_121(U33^#(X1, X2, X3)) :131
        -->_1 U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) :130
     
     48: active^#(U33(tt(), V1, V2)) ->
         c_48(U34^#(isNatKind(V2), V1, V2))
        -->_1 U34^#(ok(X1), ok(X2), ok(X3)) ->
              c_123(U34^#(X1, X2, X3)) :133
        -->_1 U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) :132
     
     49: active^#(U34(X1, X2, X3)) -> c_49(U34^#(active(X1), X2, X3))
        -->_1 U34^#(ok(X1), ok(X2), ok(X3)) ->
              c_123(U34^#(X1, X2, X3)) :133
        -->_1 U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) :132
     
     50: active^#(U34(tt(), V1, V2)) -> c_50(U35^#(isNat(V1), V2))
        -->_1 U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) :135
        -->_1 U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) :134
     
     51: active^#(U35(X1, X2)) -> c_51(U35^#(active(X1), X2))
        -->_1 U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) :135
        -->_1 U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) :134
     
     52: active^#(U35(tt(), V2)) -> c_52(U36^#(isNat(V2)))
        -->_1 U36^#(ok(X)) -> c_127(U36^#(X)) :137
        -->_1 U36^#(mark(X)) -> c_126(U36^#(X)) :136
     
     53: active^#(U36(X)) -> c_53(U36^#(active(X)))
        -->_1 U36^#(ok(X)) -> c_127(U36^#(X)) :137
        -->_1 U36^#(mark(X)) -> c_126(U36^#(X)) :136
     
     54: active^#(U36(tt())) -> c_54()
     
     55: active^#(U41(X1, X2)) -> c_55(U41^#(active(X1), X2))
        -->_1 U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) :89
        -->_1 U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) :88
     
     56: active^#(U41(tt(), V2)) -> c_56(U42^#(isNatKind(V2)))
        -->_1 U42^#(ok(X)) -> c_131(U42^#(X)) :139
        -->_1 U42^#(mark(X)) -> c_130(U42^#(X)) :138
     
     57: active^#(U42(X)) -> c_57(U42^#(active(X)))
        -->_1 U42^#(ok(X)) -> c_131(U42^#(X)) :139
        -->_1 U42^#(mark(X)) -> c_130(U42^#(X)) :138
     
     58: active^#(U42(tt())) -> c_58()
     
     59: active^#(U51(X)) -> c_59(U51^#(active(X)))
        -->_1 U51^#(ok(X)) -> c_133(U51^#(X)) :93
        -->_1 U51^#(mark(X)) -> c_132(U51^#(X)) :92
     
     60: active^#(U51(tt())) -> c_60()
     
     61: active^#(U61(X1, X2)) -> c_61(U61^#(active(X1), X2))
        -->_1 U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) :91
        -->_1 U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) :90
     
     62: active^#(U61(tt(), V2)) -> c_62(U62^#(isNatKind(V2)))
        -->_1 U62^#(ok(X)) -> c_137(U62^#(X)) :141
        -->_1 U62^#(mark(X)) -> c_136(U62^#(X)) :140
     
     63: active^#(U62(X)) -> c_63(U62^#(active(X)))
        -->_1 U62^#(ok(X)) -> c_137(U62^#(X)) :141
        -->_1 U62^#(mark(X)) -> c_136(U62^#(X)) :140
     
     64: active^#(U62(tt())) -> c_64()
     
     65: active^#(U71(X1, X2)) -> c_65(U71^#(active(X1), X2))
        -->_1 U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) :108
        -->_1 U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) :107
     
     66: active^#(U71(tt(), N)) -> c_66(U72^#(isNatKind(N), N))
        -->_1 U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) :143
        -->_1 U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) :142
     
     67: active^#(U72(X1, X2)) -> c_67(U72^#(active(X1), X2))
        -->_1 U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) :143
        -->_1 U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) :142
     
     68: active^#(U72(tt(), N)) -> c_68(N)
        -->_1 top^#(ok(X)) -> c_196(top^#(active(X))) :196
        -->_1 top^#(mark(X)) -> c_195(top^#(proper(X))) :195
        -->_1 proper^#(U92(X)) -> c_193(U92^#(proper(X))) :193
        -->_1 proper^#(U91(X1, X2)) ->
              c_192(U91^#(proper(X1), proper(X2))) :192
        -->_1 proper^#(s(X)) -> c_191(s^#(proper(X))) :191
        -->_1 proper^#(U84(X1, X2, X3)) ->
              c_190(U84^#(proper(X1), proper(X2), proper(X3))) :190
        -->_1 proper^#(U83(X1, X2, X3)) ->
              c_189(U83^#(proper(X1), proper(X2), proper(X3))) :189
        -->_1 proper^#(U82(X1, X2, X3)) ->
              c_188(U82^#(proper(X1), proper(X2), proper(X3))) :188
        -->_1 proper^#(U81(X1, X2, X3)) ->
              c_187(U81^#(proper(X1), proper(X2), proper(X3))) :187
        -->_1 proper^#(U72(X1, X2)) ->
              c_186(U72^#(proper(X1), proper(X2))) :186
        -->_1 proper^#(U71(X1, X2)) ->
              c_185(U71^#(proper(X1), proper(X2))) :185
        -->_1 proper^#(U62(X)) -> c_184(U62^#(proper(X))) :184
        -->_1 proper^#(U61(X1, X2)) ->
              c_183(U61^#(proper(X1), proper(X2))) :183
        -->_1 proper^#(U51(X)) -> c_182(U51^#(proper(X))) :182
        -->_1 proper^#(U42(X)) -> c_181(U42^#(proper(X))) :181
        -->_1 proper^#(U41(X1, X2)) ->
              c_180(U41^#(proper(X1), proper(X2))) :180
        -->_1 proper^#(U36(X)) -> c_179(U36^#(proper(X))) :179
        -->_1 proper^#(U35(X1, X2)) ->
              c_178(U35^#(proper(X1), proper(X2))) :178
        -->_1 proper^#(U34(X1, X2, X3)) ->
              c_177(U34^#(proper(X1), proper(X2), proper(X3))) :177
        -->_1 proper^#(U33(X1, X2, X3)) ->
              c_176(U33^#(proper(X1), proper(X2), proper(X3))) :176
        -->_1 proper^#(U32(X1, X2, X3)) ->
              c_175(U32^#(proper(X1), proper(X2), proper(X3))) :175
        -->_1 proper^#(U31(X1, X2, X3)) ->
              c_174(U31^#(proper(X1), proper(X2), proper(X3))) :174
        -->_1 proper^#(U23(X)) -> c_173(U23^#(proper(X))) :173
        -->_1 proper^#(U22(X1, X2)) ->
              c_172(U22^#(proper(X1), proper(X2))) :172
        -->_1 proper^#(U21(X1, X2)) ->
              c_171(U21^#(proper(X1), proper(X2))) :171
        -->_1 proper^#(U16(X)) -> c_170(U16^#(proper(X))) :170
        -->_1 proper^#(U15(X1, X2)) ->
              c_169(U15^#(proper(X1), proper(X2))) :169
        -->_1 proper^#(U14(X1, X2, X3)) ->
              c_168(U14^#(proper(X1), proper(X2), proper(X3))) :168
        -->_1 proper^#(U13(X1, X2, X3)) ->
              c_167(U13^#(proper(X1), proper(X2), proper(X3))) :167
        -->_1 proper^#(U12(X1, X2, X3)) ->
              c_166(U12^#(proper(X1), proper(X2), proper(X3))) :166
        -->_1 proper^#(U11(X1, X2, X3)) ->
              c_165(U11^#(proper(X1), proper(X2), proper(X3))) :165
        -->_1 proper^#(x(X1, X2)) ->
              c_164(x^#(proper(X1), proper(X2))) :164
        -->_1 proper^#(plus(X1, X2)) ->
              c_163(plus^#(proper(X1), proper(X2))) :163
        -->_1 proper^#(U104(X1, X2, X3)) ->
              c_162(U104^#(proper(X1), proper(X2), proper(X3))) :162
        -->_1 proper^#(isNat(X)) -> c_161(isNat^#(proper(X))) :161
        -->_1 proper^#(U103(X1, X2, X3)) ->
              c_160(U103^#(proper(X1), proper(X2), proper(X3))) :160
        -->_1 proper^#(isNatKind(X)) -> c_159(isNatKind^#(proper(X))) :159
        -->_1 proper^#(U102(X1, X2, X3)) ->
              c_158(U102^#(proper(X1), proper(X2), proper(X3))) :158
        -->_1 proper^#(U101(X1, X2, X3)) ->
              c_156(U101^#(proper(X1), proper(X2), proper(X3))) :156
        -->_1 isNat^#(ok(X)) -> c_89(isNat^#(X)) :155
        -->_1 isNatKind^#(ok(X)) -> c_86(isNatKind^#(X)) :154
        -->_1 U92^#(ok(X)) -> c_155(U92^#(X)) :153
        -->_1 U92^#(mark(X)) -> c_154(U92^#(X)) :152
        -->_1 s^#(ok(X)) -> c_151(s^#(X)) :151
        -->_1 s^#(mark(X)) -> c_150(s^#(X)) :150
        -->_1 U84^#(ok(X1), ok(X2), ok(X3)) ->
              c_149(U84^#(X1, X2, X3)) :149
        -->_1 U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) :148
        -->_1 U83^#(ok(X1), ok(X2), ok(X3)) ->
              c_147(U83^#(X1, X2, X3)) :147
        -->_1 U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) :146
        -->_1 U82^#(ok(X1), ok(X2), ok(X3)) ->
              c_145(U82^#(X1, X2, X3)) :145
        -->_1 U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) :144
        -->_1 U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) :143
        -->_1 U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) :142
        -->_1 U62^#(ok(X)) -> c_137(U62^#(X)) :141
        -->_1 U62^#(mark(X)) -> c_136(U62^#(X)) :140
        -->_1 U42^#(ok(X)) -> c_131(U42^#(X)) :139
        -->_1 U42^#(mark(X)) -> c_130(U42^#(X)) :138
        -->_1 U36^#(ok(X)) -> c_127(U36^#(X)) :137
        -->_1 U36^#(mark(X)) -> c_126(U36^#(X)) :136
        -->_1 U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) :135
        -->_1 U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) :134
        -->_1 U34^#(ok(X1), ok(X2), ok(X3)) ->
              c_123(U34^#(X1, X2, X3)) :133
        -->_1 U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) :132
        -->_1 U33^#(ok(X1), ok(X2), ok(X3)) ->
              c_121(U33^#(X1, X2, X3)) :131
        -->_1 U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) :130
        -->_1 U32^#(ok(X1), ok(X2), ok(X3)) ->
              c_119(U32^#(X1, X2, X3)) :129
        -->_1 U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) :128
        -->_1 U23^#(ok(X)) -> c_115(U23^#(X)) :127
        -->_1 U23^#(mark(X)) -> c_114(U23^#(X)) :126
        -->_1 U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) :125
        -->_1 U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) :124
        -->_1 U16^#(ok(X)) -> c_109(U16^#(X)) :123
        -->_1 U16^#(mark(X)) -> c_108(U16^#(X)) :122
        -->_1 U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) :121
        -->_1 U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) :120
        -->_1 U14^#(ok(X1), ok(X2), ok(X3)) ->
              c_105(U14^#(X1, X2, X3)) :119
        -->_1 U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) :118
        -->_1 U13^#(ok(X1), ok(X2), ok(X3)) ->
              c_103(U13^#(X1, X2, X3)) :117
        -->_1 U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) :116
        -->_1 U12^#(ok(X1), ok(X2), ok(X3)) ->
              c_101(U12^#(X1, X2, X3)) :115
        -->_1 U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) :114
        -->_1 U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) :113
        -->_1 U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) :112
        -->_1 x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) :111
        -->_1 x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) :110
        -->_1 x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) :109
        -->_1 U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) :108
        -->_1 U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) :107
        -->_1 U81^#(ok(X1), ok(X2), ok(X3)) ->
              c_143(U81^#(X1, X2, X3)) :106
        -->_1 U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) :105
        -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104
        -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103
        -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102
        -->_1 U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) :101
        -->_1 U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) :100
        -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) :99
        -->_1 U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) :98
        -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) :97
        -->_1 U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) :96
        -->_1 U104^#(ok(X1), ok(X2), ok(X3)) ->
              c_91(U104^#(X1, X2, X3)) :95
        -->_1 U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) :94
        -->_1 U51^#(ok(X)) -> c_133(U51^#(X)) :93
        -->_1 U51^#(mark(X)) -> c_132(U51^#(X)) :92
        -->_1 U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) :91
        -->_1 U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) :90
        -->_1 U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) :89
        -->_1 U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) :88
        -->_1 U103^#(ok(X1), ok(X2), ok(X3)) ->
              c_88(U103^#(X1, X2, X3)) :87
        -->_1 U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) :86
        -->_1 U102^#(ok(X1), ok(X2), ok(X3)) ->
              c_85(U102^#(X1, X2, X3)) :85
        -->_1 U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) :84
        -->_1 U101^#(ok(X1), ok(X2), ok(X3)) ->
              c_83(U101^#(X1, X2, X3)) :83
        -->_1 U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) :82
        -->_1 active^#(U92(X)) -> c_80(U92^#(active(X))) :80
        -->_1 active^#(U91(tt(), N)) -> c_79(U92^#(isNatKind(N))) :79
        -->_1 active^#(U91(X1, X2)) -> c_78(U91^#(active(X1), X2)) :78
        -->_1 active^#(s(X)) -> c_77(s^#(active(X))) :77
        -->_1 active^#(U84(tt(), M, N)) -> c_76(s^#(plus(N, M))) :76
        -->_1 active^#(U84(X1, X2, X3)) ->
              c_75(U84^#(active(X1), X2, X3)) :75
        -->_1 active^#(U83(tt(), M, N)) ->
              c_74(U84^#(isNatKind(N), M, N)) :74
        -->_1 active^#(U83(X1, X2, X3)) ->
              c_73(U83^#(active(X1), X2, X3)) :73
        -->_1 active^#(U82(tt(), M, N)) -> c_72(U83^#(isNat(N), M, N)) :72
        -->_1 active^#(U82(X1, X2, X3)) ->
              c_71(U82^#(active(X1), X2, X3)) :71
        -->_1 active^#(U81(tt(), M, N)) ->
              c_70(U82^#(isNatKind(M), M, N)) :70
        -->_1 active^#(U81(X1, X2, X3)) ->
              c_69(U81^#(active(X1), X2, X3)) :69
        -->_1 proper^#(0()) -> c_194() :194
        -->_1 proper^#(tt()) -> c_157() :157
        -->_1 active^#(U92(tt())) -> c_81() :81
        -->_1 active^#(U72(tt(), N)) -> c_68(N) :68
        -->_1 active^#(U72(X1, X2)) -> c_67(U72^#(active(X1), X2)) :67
        -->_1 active^#(U71(tt(), N)) -> c_66(U72^#(isNatKind(N), N)) :66
        -->_1 active^#(U71(X1, X2)) -> c_65(U71^#(active(X1), X2)) :65
        -->_1 active^#(U62(tt())) -> c_64() :64
        -->_1 active^#(U62(X)) -> c_63(U62^#(active(X))) :63
        -->_1 active^#(U61(tt(), V2)) -> c_62(U62^#(isNatKind(V2))) :62
        -->_1 active^#(U61(X1, X2)) -> c_61(U61^#(active(X1), X2)) :61
        -->_1 active^#(U51(tt())) -> c_60() :60
        -->_1 active^#(U51(X)) -> c_59(U51^#(active(X))) :59
        -->_1 active^#(U42(tt())) -> c_58() :58
        -->_1 active^#(U42(X)) -> c_57(U42^#(active(X))) :57
        -->_1 active^#(U41(tt(), V2)) -> c_56(U42^#(isNatKind(V2))) :56
        -->_1 active^#(U41(X1, X2)) -> c_55(U41^#(active(X1), X2)) :55
        -->_1 active^#(U36(tt())) -> c_54() :54
        -->_1 active^#(U36(X)) -> c_53(U36^#(active(X))) :53
        -->_1 active^#(U35(tt(), V2)) -> c_52(U36^#(isNat(V2))) :52
        -->_1 active^#(U35(X1, X2)) -> c_51(U35^#(active(X1), X2)) :51
        -->_1 active^#(U34(tt(), V1, V2)) -> c_50(U35^#(isNat(V1), V2)) :50
        -->_1 active^#(U34(X1, X2, X3)) ->
              c_49(U34^#(active(X1), X2, X3)) :49
        -->_1 active^#(U33(tt(), V1, V2)) ->
              c_48(U34^#(isNatKind(V2), V1, V2)) :48
        -->_1 active^#(U33(X1, X2, X3)) ->
              c_47(U33^#(active(X1), X2, X3)) :47
        -->_1 active^#(U32(tt(), V1, V2)) ->
              c_46(U33^#(isNatKind(V2), V1, V2)) :46
        -->_1 active^#(U32(X1, X2, X3)) ->
              c_45(U32^#(active(X1), X2, X3)) :45
        -->_1 active^#(U31(tt(), V1, V2)) ->
              c_44(U32^#(isNatKind(V1), V1, V2)) :44
        -->_1 active^#(U31(X1, X2, X3)) ->
              c_43(U31^#(active(X1), X2, X3)) :43
        -->_1 active^#(U23(tt())) -> c_42() :42
        -->_1 active^#(U23(X)) -> c_41(U23^#(active(X))) :41
        -->_1 active^#(U22(tt(), V1)) -> c_40(U23^#(isNat(V1))) :40
        -->_1 active^#(U22(X1, X2)) -> c_39(U22^#(active(X1), X2)) :39
        -->_1 active^#(U21(tt(), V1)) -> c_38(U22^#(isNatKind(V1), V1)) :38
        -->_1 active^#(U21(X1, X2)) -> c_37(U21^#(active(X1), X2)) :37
        -->_1 active^#(U16(tt())) -> c_36() :36
        -->_1 active^#(U16(X)) -> c_35(U16^#(active(X))) :35
        -->_1 active^#(U15(tt(), V2)) -> c_34(U16^#(isNat(V2))) :34
        -->_1 active^#(U15(X1, X2)) -> c_33(U15^#(active(X1), X2)) :33
        -->_1 active^#(U14(tt(), V1, V2)) -> c_32(U15^#(isNat(V1), V2)) :32
        -->_1 active^#(U14(X1, X2, X3)) ->
              c_31(U14^#(active(X1), X2, X3)) :31
        -->_1 active^#(U13(tt(), V1, V2)) ->
              c_30(U14^#(isNatKind(V2), V1, V2)) :30
        -->_1 active^#(U13(X1, X2, X3)) ->
              c_29(U13^#(active(X1), X2, X3)) :29
        -->_1 active^#(U12(tt(), V1, V2)) ->
              c_28(U13^#(isNatKind(V2), V1, V2)) :28
        -->_1 active^#(U12(X1, X2, X3)) ->
              c_27(U12^#(active(X1), X2, X3)) :27
        -->_1 active^#(U11(tt(), V1, V2)) ->
              c_26(U12^#(isNatKind(V1), V1, V2)) :26
        -->_1 active^#(U11(X1, X2, X3)) ->
              c_25(U11^#(active(X1), X2, X3)) :25
        -->_1 active^#(x(N, 0())) -> c_24(U91^#(isNat(N), N)) :24
        -->_1 active^#(x(N, s(M))) -> c_23(U101^#(isNat(M), M, N)) :23
        -->_1 active^#(x(X1, X2)) -> c_22(x^#(active(X1), X2)) :22
        -->_1 active^#(x(X1, X2)) -> c_21(x^#(X1, active(X2))) :21
        -->_1 active^#(plus(N, 0())) -> c_20(U71^#(isNat(N), N)) :20
        -->_1 active^#(plus(N, s(M))) -> c_19(U81^#(isNat(M), M, N)) :19
        -->_1 active^#(plus(X1, X2)) -> c_18(plus^#(active(X1), X2)) :18
        -->_1 active^#(plus(X1, X2)) -> c_17(plus^#(X1, active(X2))) :17
        -->_1 active^#(U104(tt(), M, N)) -> c_16(plus^#(x(N, M), N)) :16
        -->_1 active^#(U104(X1, X2, X3)) ->
              c_15(U104^#(active(X1), X2, X3)) :15
        -->_1 active^#(isNat(0())) -> c_14() :14
        -->_1 active^#(isNat(s(V1))) -> c_13(U21^#(isNatKind(V1), V1)) :13
        -->_1 active^#(isNat(x(V1, V2))) ->
              c_12(U31^#(isNatKind(V1), V1, V2)) :12
        -->_1 active^#(isNat(plus(V1, V2))) ->
              c_11(U11^#(isNatKind(V1), V1, V2)) :11
        -->_1 active^#(U103(tt(), M, N)) ->
              c_10(U104^#(isNatKind(N), M, N)) :10
        -->_1 active^#(U103(X1, X2, X3)) ->
              c_9(U103^#(active(X1), X2, X3)) :9
        -->_1 active^#(isNatKind(0())) -> c_8() :8
        -->_1 active^#(isNatKind(s(V1))) -> c_7(U51^#(isNatKind(V1))) :7
        -->_1 active^#(isNatKind(x(V1, V2))) ->
              c_6(U61^#(isNatKind(V1), V2)) :6
        -->_1 active^#(isNatKind(plus(V1, V2))) ->
              c_5(U41^#(isNatKind(V1), V2)) :5
        -->_1 active^#(U102(tt(), M, N)) -> c_4(U103^#(isNat(N), M, N)) :4
        -->_1 active^#(U102(X1, X2, X3)) ->
              c_3(U102^#(active(X1), X2, X3)) :3
        -->_1 active^#(U101(tt(), M, N)) ->
              c_2(U102^#(isNatKind(M), M, N)) :2
        -->_1 active^#(U101(X1, X2, X3)) ->
              c_1(U101^#(active(X1), X2, X3)) :1
     
     69: active^#(U81(X1, X2, X3)) -> c_69(U81^#(active(X1), X2, X3))
        -->_1 U81^#(ok(X1), ok(X2), ok(X3)) ->
              c_143(U81^#(X1, X2, X3)) :106
        -->_1 U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) :105
     
     70: active^#(U81(tt(), M, N)) -> c_70(U82^#(isNatKind(M), M, N))
        -->_1 U82^#(ok(X1), ok(X2), ok(X3)) ->
              c_145(U82^#(X1, X2, X3)) :145
        -->_1 U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) :144
     
     71: active^#(U82(X1, X2, X3)) -> c_71(U82^#(active(X1), X2, X3))
        -->_1 U82^#(ok(X1), ok(X2), ok(X3)) ->
              c_145(U82^#(X1, X2, X3)) :145
        -->_1 U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) :144
     
     72: active^#(U82(tt(), M, N)) -> c_72(U83^#(isNat(N), M, N))
        -->_1 U83^#(ok(X1), ok(X2), ok(X3)) ->
              c_147(U83^#(X1, X2, X3)) :147
        -->_1 U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) :146
     
     73: active^#(U83(X1, X2, X3)) -> c_73(U83^#(active(X1), X2, X3))
        -->_1 U83^#(ok(X1), ok(X2), ok(X3)) ->
              c_147(U83^#(X1, X2, X3)) :147
        -->_1 U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) :146
     
     74: active^#(U83(tt(), M, N)) -> c_74(U84^#(isNatKind(N), M, N))
        -->_1 U84^#(ok(X1), ok(X2), ok(X3)) ->
              c_149(U84^#(X1, X2, X3)) :149
        -->_1 U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) :148
     
     75: active^#(U84(X1, X2, X3)) -> c_75(U84^#(active(X1), X2, X3))
        -->_1 U84^#(ok(X1), ok(X2), ok(X3)) ->
              c_149(U84^#(X1, X2, X3)) :149
        -->_1 U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) :148
     
     76: active^#(U84(tt(), M, N)) -> c_76(s^#(plus(N, M)))
        -->_1 s^#(ok(X)) -> c_151(s^#(X)) :151
        -->_1 s^#(mark(X)) -> c_150(s^#(X)) :150
     
     77: active^#(s(X)) -> c_77(s^#(active(X)))
        -->_1 s^#(ok(X)) -> c_151(s^#(X)) :151
        -->_1 s^#(mark(X)) -> c_150(s^#(X)) :150
     
     78: active^#(U91(X1, X2)) -> c_78(U91^#(active(X1), X2))
        -->_1 U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) :113
        -->_1 U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) :112
     
     79: active^#(U91(tt(), N)) -> c_79(U92^#(isNatKind(N)))
        -->_1 U92^#(ok(X)) -> c_155(U92^#(X)) :153
        -->_1 U92^#(mark(X)) -> c_154(U92^#(X)) :152
     
     80: active^#(U92(X)) -> c_80(U92^#(active(X)))
        -->_1 U92^#(ok(X)) -> c_155(U92^#(X)) :153
        -->_1 U92^#(mark(X)) -> c_154(U92^#(X)) :152
     
     81: active^#(U92(tt())) -> c_81()
     
     82: U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3))
        -->_1 U101^#(ok(X1), ok(X2), ok(X3)) ->
              c_83(U101^#(X1, X2, X3)) :83
        -->_1 U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) :82
     
     83: U101^#(ok(X1), ok(X2), ok(X3)) -> c_83(U101^#(X1, X2, X3))
        -->_1 U101^#(ok(X1), ok(X2), ok(X3)) ->
              c_83(U101^#(X1, X2, X3)) :83
        -->_1 U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) :82
     
     84: U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3))
        -->_1 U102^#(ok(X1), ok(X2), ok(X3)) ->
              c_85(U102^#(X1, X2, X3)) :85
        -->_1 U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) :84
     
     85: U102^#(ok(X1), ok(X2), ok(X3)) -> c_85(U102^#(X1, X2, X3))
        -->_1 U102^#(ok(X1), ok(X2), ok(X3)) ->
              c_85(U102^#(X1, X2, X3)) :85
        -->_1 U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) :84
     
     86: U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3))
        -->_1 U103^#(ok(X1), ok(X2), ok(X3)) ->
              c_88(U103^#(X1, X2, X3)) :87
        -->_1 U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) :86
     
     87: U103^#(ok(X1), ok(X2), ok(X3)) -> c_88(U103^#(X1, X2, X3))
        -->_1 U103^#(ok(X1), ok(X2), ok(X3)) ->
              c_88(U103^#(X1, X2, X3)) :87
        -->_1 U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) :86
     
     88: U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2))
        -->_1 U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) :89
        -->_1 U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) :88
     
     89: U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2))
        -->_1 U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) :89
        -->_1 U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) :88
     
     90: U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2))
        -->_1 U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) :91
        -->_1 U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) :90
     
     91: U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2))
        -->_1 U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) :91
        -->_1 U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) :90
     
     92: U51^#(mark(X)) -> c_132(U51^#(X))
        -->_1 U51^#(ok(X)) -> c_133(U51^#(X)) :93
        -->_1 U51^#(mark(X)) -> c_132(U51^#(X)) :92
     
     93: U51^#(ok(X)) -> c_133(U51^#(X))
        -->_1 U51^#(ok(X)) -> c_133(U51^#(X)) :93
        -->_1 U51^#(mark(X)) -> c_132(U51^#(X)) :92
     
     94: U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3))
        -->_1 U104^#(ok(X1), ok(X2), ok(X3)) ->
              c_91(U104^#(X1, X2, X3)) :95
        -->_1 U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) :94
     
     95: U104^#(ok(X1), ok(X2), ok(X3)) -> c_91(U104^#(X1, X2, X3))
        -->_1 U104^#(ok(X1), ok(X2), ok(X3)) ->
              c_91(U104^#(X1, X2, X3)) :95
        -->_1 U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) :94
     
     96: U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3))
        -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) :97
        -->_1 U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) :96
     
     97: U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3))
        -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) :97
        -->_1 U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) :96
     
     98: U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3))
        -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) :99
        -->_1 U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) :98
     
     99: U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3))
        -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) :99
        -->_1 U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) :98
     
     100: U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2))
        -->_1 U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) :101
        -->_1 U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) :100
     
     101: U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2))
        -->_1 U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) :101
        -->_1 U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) :100
     
     102: plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2))
        -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104
        -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103
        -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102
     
     103: plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2))
        -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104
        -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103
        -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102
     
     104: plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2))
        -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104
        -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103
        -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102
     
     105: U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3))
        -->_1 U81^#(ok(X1), ok(X2), ok(X3)) ->
              c_143(U81^#(X1, X2, X3)) :106
        -->_1 U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) :105
     
     106: U81^#(ok(X1), ok(X2), ok(X3)) -> c_143(U81^#(X1, X2, X3))
        -->_1 U81^#(ok(X1), ok(X2), ok(X3)) ->
              c_143(U81^#(X1, X2, X3)) :106
        -->_1 U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) :105
     
     107: U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2))
        -->_1 U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) :108
        -->_1 U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) :107
     
     108: U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2))
        -->_1 U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) :108
        -->_1 U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) :107
     
     109: x^#(X1, mark(X2)) -> c_95(x^#(X1, X2))
        -->_1 x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) :111
        -->_1 x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) :110
        -->_1 x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) :109
     
     110: x^#(mark(X1), X2) -> c_96(x^#(X1, X2))
        -->_1 x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) :111
        -->_1 x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) :110
        -->_1 x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) :109
     
     111: x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2))
        -->_1 x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) :111
        -->_1 x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) :110
        -->_1 x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) :109
     
     112: U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2))
        -->_1 U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) :113
        -->_1 U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) :112
     
     113: U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2))
        -->_1 U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) :113
        -->_1 U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) :112
     
     114: U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3))
        -->_1 U12^#(ok(X1), ok(X2), ok(X3)) ->
              c_101(U12^#(X1, X2, X3)) :115
        -->_1 U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) :114
     
     115: U12^#(ok(X1), ok(X2), ok(X3)) -> c_101(U12^#(X1, X2, X3))
        -->_1 U12^#(ok(X1), ok(X2), ok(X3)) ->
              c_101(U12^#(X1, X2, X3)) :115
        -->_1 U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) :114
     
     116: U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3))
        -->_1 U13^#(ok(X1), ok(X2), ok(X3)) ->
              c_103(U13^#(X1, X2, X3)) :117
        -->_1 U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) :116
     
     117: U13^#(ok(X1), ok(X2), ok(X3)) -> c_103(U13^#(X1, X2, X3))
        -->_1 U13^#(ok(X1), ok(X2), ok(X3)) ->
              c_103(U13^#(X1, X2, X3)) :117
        -->_1 U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) :116
     
     118: U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3))
        -->_1 U14^#(ok(X1), ok(X2), ok(X3)) ->
              c_105(U14^#(X1, X2, X3)) :119
        -->_1 U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) :118
     
     119: U14^#(ok(X1), ok(X2), ok(X3)) -> c_105(U14^#(X1, X2, X3))
        -->_1 U14^#(ok(X1), ok(X2), ok(X3)) ->
              c_105(U14^#(X1, X2, X3)) :119
        -->_1 U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) :118
     
     120: U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2))
        -->_1 U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) :121
        -->_1 U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) :120
     
     121: U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2))
        -->_1 U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) :121
        -->_1 U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) :120
     
     122: U16^#(mark(X)) -> c_108(U16^#(X))
        -->_1 U16^#(ok(X)) -> c_109(U16^#(X)) :123
        -->_1 U16^#(mark(X)) -> c_108(U16^#(X)) :122
     
     123: U16^#(ok(X)) -> c_109(U16^#(X))
        -->_1 U16^#(ok(X)) -> c_109(U16^#(X)) :123
        -->_1 U16^#(mark(X)) -> c_108(U16^#(X)) :122
     
     124: U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2))
        -->_1 U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) :125
        -->_1 U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) :124
     
     125: U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2))
        -->_1 U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) :125
        -->_1 U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) :124
     
     126: U23^#(mark(X)) -> c_114(U23^#(X))
        -->_1 U23^#(ok(X)) -> c_115(U23^#(X)) :127
        -->_1 U23^#(mark(X)) -> c_114(U23^#(X)) :126
     
     127: U23^#(ok(X)) -> c_115(U23^#(X))
        -->_1 U23^#(ok(X)) -> c_115(U23^#(X)) :127
        -->_1 U23^#(mark(X)) -> c_114(U23^#(X)) :126
     
     128: U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3))
        -->_1 U32^#(ok(X1), ok(X2), ok(X3)) ->
              c_119(U32^#(X1, X2, X3)) :129
        -->_1 U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) :128
     
     129: U32^#(ok(X1), ok(X2), ok(X3)) -> c_119(U32^#(X1, X2, X3))
        -->_1 U32^#(ok(X1), ok(X2), ok(X3)) ->
              c_119(U32^#(X1, X2, X3)) :129
        -->_1 U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) :128
     
     130: U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3))
        -->_1 U33^#(ok(X1), ok(X2), ok(X3)) ->
              c_121(U33^#(X1, X2, X3)) :131
        -->_1 U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) :130
     
     131: U33^#(ok(X1), ok(X2), ok(X3)) -> c_121(U33^#(X1, X2, X3))
        -->_1 U33^#(ok(X1), ok(X2), ok(X3)) ->
              c_121(U33^#(X1, X2, X3)) :131
        -->_1 U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) :130
     
     132: U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3))
        -->_1 U34^#(ok(X1), ok(X2), ok(X3)) ->
              c_123(U34^#(X1, X2, X3)) :133
        -->_1 U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) :132
     
     133: U34^#(ok(X1), ok(X2), ok(X3)) -> c_123(U34^#(X1, X2, X3))
        -->_1 U34^#(ok(X1), ok(X2), ok(X3)) ->
              c_123(U34^#(X1, X2, X3)) :133
        -->_1 U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) :132
     
     134: U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2))
        -->_1 U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) :135
        -->_1 U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) :134
     
     135: U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2))
        -->_1 U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) :135
        -->_1 U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) :134
     
     136: U36^#(mark(X)) -> c_126(U36^#(X))
        -->_1 U36^#(ok(X)) -> c_127(U36^#(X)) :137
        -->_1 U36^#(mark(X)) -> c_126(U36^#(X)) :136
     
     137: U36^#(ok(X)) -> c_127(U36^#(X))
        -->_1 U36^#(ok(X)) -> c_127(U36^#(X)) :137
        -->_1 U36^#(mark(X)) -> c_126(U36^#(X)) :136
     
     138: U42^#(mark(X)) -> c_130(U42^#(X))
        -->_1 U42^#(ok(X)) -> c_131(U42^#(X)) :139
        -->_1 U42^#(mark(X)) -> c_130(U42^#(X)) :138
     
     139: U42^#(ok(X)) -> c_131(U42^#(X))
        -->_1 U42^#(ok(X)) -> c_131(U42^#(X)) :139
        -->_1 U42^#(mark(X)) -> c_130(U42^#(X)) :138
     
     140: U62^#(mark(X)) -> c_136(U62^#(X))
        -->_1 U62^#(ok(X)) -> c_137(U62^#(X)) :141
        -->_1 U62^#(mark(X)) -> c_136(U62^#(X)) :140
     
     141: U62^#(ok(X)) -> c_137(U62^#(X))
        -->_1 U62^#(ok(X)) -> c_137(U62^#(X)) :141
        -->_1 U62^#(mark(X)) -> c_136(U62^#(X)) :140
     
     142: U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2))
        -->_1 U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) :143
        -->_1 U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) :142
     
     143: U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2))
        -->_1 U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) :143
        -->_1 U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) :142
     
     144: U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3))
        -->_1 U82^#(ok(X1), ok(X2), ok(X3)) ->
              c_145(U82^#(X1, X2, X3)) :145
        -->_1 U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) :144
     
     145: U82^#(ok(X1), ok(X2), ok(X3)) -> c_145(U82^#(X1, X2, X3))
        -->_1 U82^#(ok(X1), ok(X2), ok(X3)) ->
              c_145(U82^#(X1, X2, X3)) :145
        -->_1 U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) :144
     
     146: U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3))
        -->_1 U83^#(ok(X1), ok(X2), ok(X3)) ->
              c_147(U83^#(X1, X2, X3)) :147
        -->_1 U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) :146
     
     147: U83^#(ok(X1), ok(X2), ok(X3)) -> c_147(U83^#(X1, X2, X3))
        -->_1 U83^#(ok(X1), ok(X2), ok(X3)) ->
              c_147(U83^#(X1, X2, X3)) :147
        -->_1 U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) :146
     
     148: U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3))
        -->_1 U84^#(ok(X1), ok(X2), ok(X3)) ->
              c_149(U84^#(X1, X2, X3)) :149
        -->_1 U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) :148
     
     149: U84^#(ok(X1), ok(X2), ok(X3)) -> c_149(U84^#(X1, X2, X3))
        -->_1 U84^#(ok(X1), ok(X2), ok(X3)) ->
              c_149(U84^#(X1, X2, X3)) :149
        -->_1 U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) :148
     
     150: s^#(mark(X)) -> c_150(s^#(X))
        -->_1 s^#(ok(X)) -> c_151(s^#(X)) :151
        -->_1 s^#(mark(X)) -> c_150(s^#(X)) :150
     
     151: s^#(ok(X)) -> c_151(s^#(X))
        -->_1 s^#(ok(X)) -> c_151(s^#(X)) :151
        -->_1 s^#(mark(X)) -> c_150(s^#(X)) :150
     
     152: U92^#(mark(X)) -> c_154(U92^#(X))
        -->_1 U92^#(ok(X)) -> c_155(U92^#(X)) :153
        -->_1 U92^#(mark(X)) -> c_154(U92^#(X)) :152
     
     153: U92^#(ok(X)) -> c_155(U92^#(X))
        -->_1 U92^#(ok(X)) -> c_155(U92^#(X)) :153
        -->_1 U92^#(mark(X)) -> c_154(U92^#(X)) :152
     
     154: isNatKind^#(ok(X)) -> c_86(isNatKind^#(X))
        -->_1 isNatKind^#(ok(X)) -> c_86(isNatKind^#(X)) :154
     
     155: isNat^#(ok(X)) -> c_89(isNat^#(X))
        -->_1 isNat^#(ok(X)) -> c_89(isNat^#(X)) :155
     
     156: proper^#(U101(X1, X2, X3)) ->
          c_156(U101^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U101^#(ok(X1), ok(X2), ok(X3)) ->
              c_83(U101^#(X1, X2, X3)) :83
        -->_1 U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) :82
     
     157: proper^#(tt()) -> c_157()
     
     158: proper^#(U102(X1, X2, X3)) ->
          c_158(U102^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U102^#(ok(X1), ok(X2), ok(X3)) ->
              c_85(U102^#(X1, X2, X3)) :85
        -->_1 U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) :84
     
     159: proper^#(isNatKind(X)) -> c_159(isNatKind^#(proper(X)))
        -->_1 isNatKind^#(ok(X)) -> c_86(isNatKind^#(X)) :154
     
     160: proper^#(U103(X1, X2, X3)) ->
          c_160(U103^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U103^#(ok(X1), ok(X2), ok(X3)) ->
              c_88(U103^#(X1, X2, X3)) :87
        -->_1 U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) :86
     
     161: proper^#(isNat(X)) -> c_161(isNat^#(proper(X)))
        -->_1 isNat^#(ok(X)) -> c_89(isNat^#(X)) :155
     
     162: proper^#(U104(X1, X2, X3)) ->
          c_162(U104^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U104^#(ok(X1), ok(X2), ok(X3)) ->
              c_91(U104^#(X1, X2, X3)) :95
        -->_1 U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) :94
     
     163: proper^#(plus(X1, X2)) ->
          c_163(plus^#(proper(X1), proper(X2)))
        -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104
        -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103
        -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102
     
     164: proper^#(x(X1, X2)) -> c_164(x^#(proper(X1), proper(X2)))
        -->_1 x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) :111
        -->_1 x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) :110
        -->_1 x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) :109
     
     165: proper^#(U11(X1, X2, X3)) ->
          c_165(U11^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) :97
        -->_1 U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) :96
     
     166: proper^#(U12(X1, X2, X3)) ->
          c_166(U12^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U12^#(ok(X1), ok(X2), ok(X3)) ->
              c_101(U12^#(X1, X2, X3)) :115
        -->_1 U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) :114
     
     167: proper^#(U13(X1, X2, X3)) ->
          c_167(U13^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U13^#(ok(X1), ok(X2), ok(X3)) ->
              c_103(U13^#(X1, X2, X3)) :117
        -->_1 U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) :116
     
     168: proper^#(U14(X1, X2, X3)) ->
          c_168(U14^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U14^#(ok(X1), ok(X2), ok(X3)) ->
              c_105(U14^#(X1, X2, X3)) :119
        -->_1 U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) :118
     
     169: proper^#(U15(X1, X2)) -> c_169(U15^#(proper(X1), proper(X2)))
        -->_1 U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) :121
        -->_1 U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) :120
     
     170: proper^#(U16(X)) -> c_170(U16^#(proper(X)))
        -->_1 U16^#(ok(X)) -> c_109(U16^#(X)) :123
        -->_1 U16^#(mark(X)) -> c_108(U16^#(X)) :122
     
     171: proper^#(U21(X1, X2)) -> c_171(U21^#(proper(X1), proper(X2)))
        -->_1 U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) :101
        -->_1 U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) :100
     
     172: proper^#(U22(X1, X2)) -> c_172(U22^#(proper(X1), proper(X2)))
        -->_1 U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) :125
        -->_1 U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) :124
     
     173: proper^#(U23(X)) -> c_173(U23^#(proper(X)))
        -->_1 U23^#(ok(X)) -> c_115(U23^#(X)) :127
        -->_1 U23^#(mark(X)) -> c_114(U23^#(X)) :126
     
     174: proper^#(U31(X1, X2, X3)) ->
          c_174(U31^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) :99
        -->_1 U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) :98
     
     175: proper^#(U32(X1, X2, X3)) ->
          c_175(U32^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U32^#(ok(X1), ok(X2), ok(X3)) ->
              c_119(U32^#(X1, X2, X3)) :129
        -->_1 U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) :128
     
     176: proper^#(U33(X1, X2, X3)) ->
          c_176(U33^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U33^#(ok(X1), ok(X2), ok(X3)) ->
              c_121(U33^#(X1, X2, X3)) :131
        -->_1 U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) :130
     
     177: proper^#(U34(X1, X2, X3)) ->
          c_177(U34^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U34^#(ok(X1), ok(X2), ok(X3)) ->
              c_123(U34^#(X1, X2, X3)) :133
        -->_1 U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) :132
     
     178: proper^#(U35(X1, X2)) -> c_178(U35^#(proper(X1), proper(X2)))
        -->_1 U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) :135
        -->_1 U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) :134
     
     179: proper^#(U36(X)) -> c_179(U36^#(proper(X)))
        -->_1 U36^#(ok(X)) -> c_127(U36^#(X)) :137
        -->_1 U36^#(mark(X)) -> c_126(U36^#(X)) :136
     
     180: proper^#(U41(X1, X2)) -> c_180(U41^#(proper(X1), proper(X2)))
        -->_1 U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) :89
        -->_1 U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) :88
     
     181: proper^#(U42(X)) -> c_181(U42^#(proper(X)))
        -->_1 U42^#(ok(X)) -> c_131(U42^#(X)) :139
        -->_1 U42^#(mark(X)) -> c_130(U42^#(X)) :138
     
     182: proper^#(U51(X)) -> c_182(U51^#(proper(X)))
        -->_1 U51^#(ok(X)) -> c_133(U51^#(X)) :93
        -->_1 U51^#(mark(X)) -> c_132(U51^#(X)) :92
     
     183: proper^#(U61(X1, X2)) -> c_183(U61^#(proper(X1), proper(X2)))
        -->_1 U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) :91
        -->_1 U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) :90
     
     184: proper^#(U62(X)) -> c_184(U62^#(proper(X)))
        -->_1 U62^#(ok(X)) -> c_137(U62^#(X)) :141
        -->_1 U62^#(mark(X)) -> c_136(U62^#(X)) :140
     
     185: proper^#(U71(X1, X2)) -> c_185(U71^#(proper(X1), proper(X2)))
        -->_1 U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) :108
        -->_1 U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) :107
     
     186: proper^#(U72(X1, X2)) -> c_186(U72^#(proper(X1), proper(X2)))
        -->_1 U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) :143
        -->_1 U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) :142
     
     187: proper^#(U81(X1, X2, X3)) ->
          c_187(U81^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U81^#(ok(X1), ok(X2), ok(X3)) ->
              c_143(U81^#(X1, X2, X3)) :106
        -->_1 U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) :105
     
     188: proper^#(U82(X1, X2, X3)) ->
          c_188(U82^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U82^#(ok(X1), ok(X2), ok(X3)) ->
              c_145(U82^#(X1, X2, X3)) :145
        -->_1 U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) :144
     
     189: proper^#(U83(X1, X2, X3)) ->
          c_189(U83^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U83^#(ok(X1), ok(X2), ok(X3)) ->
              c_147(U83^#(X1, X2, X3)) :147
        -->_1 U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) :146
     
     190: proper^#(U84(X1, X2, X3)) ->
          c_190(U84^#(proper(X1), proper(X2), proper(X3)))
        -->_1 U84^#(ok(X1), ok(X2), ok(X3)) ->
              c_149(U84^#(X1, X2, X3)) :149
        -->_1 U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) :148
     
     191: proper^#(s(X)) -> c_191(s^#(proper(X)))
        -->_1 s^#(ok(X)) -> c_151(s^#(X)) :151
        -->_1 s^#(mark(X)) -> c_150(s^#(X)) :150
     
     192: proper^#(U91(X1, X2)) -> c_192(U91^#(proper(X1), proper(X2)))
        -->_1 U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) :113
        -->_1 U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) :112
     
     193: proper^#(U92(X)) -> c_193(U92^#(proper(X)))
        -->_1 U92^#(ok(X)) -> c_155(U92^#(X)) :153
        -->_1 U92^#(mark(X)) -> c_154(U92^#(X)) :152
     
     194: proper^#(0()) -> c_194()
     
     195: top^#(mark(X)) -> c_195(top^#(proper(X)))
        -->_1 top^#(ok(X)) -> c_196(top^#(active(X))) :196
        -->_1 top^#(mark(X)) -> c_195(top^#(proper(X))) :195
     
     196: top^#(ok(X)) -> c_196(top^#(active(X)))
        -->_1 top^#(ok(X)) -> c_196(top^#(active(X))) :196
        -->_1 top^#(mark(X)) -> c_195(top^#(proper(X))) :195
     
   
   Only the nodes
   {82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,104,103,105,106,107,108,109,111,110,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,157,194,195,196}
   are reachable from nodes
   {82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,157,194,195,196}
   that start derivation from marked basic terms. The nodes not
   reachable are removed from the problem.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3))
     , U101^#(ok(X1), ok(X2), ok(X3)) -> c_83(U101^#(X1, X2, X3))
     , U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3))
     , U102^#(ok(X1), ok(X2), ok(X3)) -> c_85(U102^#(X1, X2, X3))
     , U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3))
     , U103^#(ok(X1), ok(X2), ok(X3)) -> c_88(U103^#(X1, X2, X3))
     , U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2))
     , U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2))
     , U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2))
     , U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2))
     , U51^#(mark(X)) -> c_132(U51^#(X))
     , U51^#(ok(X)) -> c_133(U51^#(X))
     , U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3))
     , U104^#(ok(X1), ok(X2), ok(X3)) -> c_91(U104^#(X1, X2, X3))
     , U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3))
     , U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3))
     , U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3))
     , U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3))
     , U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2))
     , U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2))
     , plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2))
     , plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2))
     , plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2))
     , U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3))
     , U81^#(ok(X1), ok(X2), ok(X3)) -> c_143(U81^#(X1, X2, X3))
     , U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2))
     , U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2))
     , x^#(X1, mark(X2)) -> c_95(x^#(X1, X2))
     , x^#(mark(X1), X2) -> c_96(x^#(X1, X2))
     , x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2))
     , U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2))
     , U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2))
     , U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3))
     , U12^#(ok(X1), ok(X2), ok(X3)) -> c_101(U12^#(X1, X2, X3))
     , U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3))
     , U13^#(ok(X1), ok(X2), ok(X3)) -> c_103(U13^#(X1, X2, X3))
     , U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3))
     , U14^#(ok(X1), ok(X2), ok(X3)) -> c_105(U14^#(X1, X2, X3))
     , U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2))
     , U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2))
     , U16^#(mark(X)) -> c_108(U16^#(X))
     , U16^#(ok(X)) -> c_109(U16^#(X))
     , U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2))
     , U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2))
     , U23^#(mark(X)) -> c_114(U23^#(X))
     , U23^#(ok(X)) -> c_115(U23^#(X))
     , U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3))
     , U32^#(ok(X1), ok(X2), ok(X3)) -> c_119(U32^#(X1, X2, X3))
     , U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3))
     , U33^#(ok(X1), ok(X2), ok(X3)) -> c_121(U33^#(X1, X2, X3))
     , U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3))
     , U34^#(ok(X1), ok(X2), ok(X3)) -> c_123(U34^#(X1, X2, X3))
     , U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2))
     , U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2))
     , U36^#(mark(X)) -> c_126(U36^#(X))
     , U36^#(ok(X)) -> c_127(U36^#(X))
     , U42^#(mark(X)) -> c_130(U42^#(X))
     , U42^#(ok(X)) -> c_131(U42^#(X))
     , U62^#(mark(X)) -> c_136(U62^#(X))
     , U62^#(ok(X)) -> c_137(U62^#(X))
     , U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2))
     , U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2))
     , U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3))
     , U82^#(ok(X1), ok(X2), ok(X3)) -> c_145(U82^#(X1, X2, X3))
     , U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3))
     , U83^#(ok(X1), ok(X2), ok(X3)) -> c_147(U83^#(X1, X2, X3))
     , U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3))
     , U84^#(ok(X1), ok(X2), ok(X3)) -> c_149(U84^#(X1, X2, X3))
     , s^#(mark(X)) -> c_150(s^#(X))
     , s^#(ok(X)) -> c_151(s^#(X))
     , U92^#(mark(X)) -> c_154(U92^#(X))
     , U92^#(ok(X)) -> c_155(U92^#(X))
     , isNatKind^#(ok(X)) -> c_86(isNatKind^#(X))
     , isNat^#(ok(X)) -> c_89(isNat^#(X))
     , proper^#(tt()) -> c_157()
     , proper^#(0()) -> c_194()
     , top^#(mark(X)) -> c_195(top^#(proper(X)))
     , top^#(ok(X)) -> c_196(top^#(active(X))) }
   Strict Trs:
     { active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3)
     , active(U101(tt(), M, N)) -> mark(U102(isNatKind(M), M, N))
     , active(U102(X1, X2, X3)) -> U102(active(X1), X2, X3)
     , active(U102(tt(), M, N)) -> mark(U103(isNat(N), M, N))
     , active(isNatKind(plus(V1, V2))) -> mark(U41(isNatKind(V1), V2))
     , active(isNatKind(x(V1, V2))) -> mark(U61(isNatKind(V1), V2))
     , active(isNatKind(s(V1))) -> mark(U51(isNatKind(V1)))
     , active(isNatKind(0())) -> mark(tt())
     , active(U103(X1, X2, X3)) -> U103(active(X1), X2, X3)
     , active(U103(tt(), M, N)) -> mark(U104(isNatKind(N), M, N))
     , active(isNat(plus(V1, V2))) -> mark(U11(isNatKind(V1), V1, V2))
     , active(isNat(x(V1, V2))) -> mark(U31(isNatKind(V1), V1, V2))
     , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1))
     , active(isNat(0())) -> mark(tt())
     , active(U104(X1, X2, X3)) -> U104(active(X1), X2, X3)
     , active(U104(tt(), M, N)) -> mark(plus(x(N, M), N))
     , active(plus(X1, X2)) -> plus(X1, active(X2))
     , active(plus(X1, X2)) -> plus(active(X1), X2)
     , active(plus(N, s(M))) -> mark(U81(isNat(M), M, N))
     , active(plus(N, 0())) -> mark(U71(isNat(N), N))
     , active(x(X1, X2)) -> x(X1, active(X2))
     , active(x(X1, X2)) -> x(active(X1), X2)
     , active(x(N, s(M))) -> mark(U101(isNat(M), M, N))
     , active(x(N, 0())) -> mark(U91(isNat(N), N))
     , active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3)
     , active(U11(tt(), V1, V2)) -> mark(U12(isNatKind(V1), V1, V2))
     , active(U12(X1, X2, X3)) -> U12(active(X1), X2, X3)
     , active(U12(tt(), V1, V2)) -> mark(U13(isNatKind(V2), V1, V2))
     , active(U13(X1, X2, X3)) -> U13(active(X1), X2, X3)
     , active(U13(tt(), V1, V2)) -> mark(U14(isNatKind(V2), V1, V2))
     , active(U14(X1, X2, X3)) -> U14(active(X1), X2, X3)
     , active(U14(tt(), V1, V2)) -> mark(U15(isNat(V1), V2))
     , active(U15(X1, X2)) -> U15(active(X1), X2)
     , active(U15(tt(), V2)) -> mark(U16(isNat(V2)))
     , active(U16(X)) -> U16(active(X))
     , active(U16(tt())) -> mark(tt())
     , active(U21(X1, X2)) -> U21(active(X1), X2)
     , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1))
     , active(U22(X1, X2)) -> U22(active(X1), X2)
     , active(U22(tt(), V1)) -> mark(U23(isNat(V1)))
     , active(U23(X)) -> U23(active(X))
     , active(U23(tt())) -> mark(tt())
     , active(U31(X1, X2, X3)) -> U31(active(X1), X2, X3)
     , active(U31(tt(), V1, V2)) -> mark(U32(isNatKind(V1), V1, V2))
     , active(U32(X1, X2, X3)) -> U32(active(X1), X2, X3)
     , active(U32(tt(), V1, V2)) -> mark(U33(isNatKind(V2), V1, V2))
     , active(U33(X1, X2, X3)) -> U33(active(X1), X2, X3)
     , active(U33(tt(), V1, V2)) -> mark(U34(isNatKind(V2), V1, V2))
     , active(U34(X1, X2, X3)) -> U34(active(X1), X2, X3)
     , active(U34(tt(), V1, V2)) -> mark(U35(isNat(V1), V2))
     , active(U35(X1, X2)) -> U35(active(X1), X2)
     , active(U35(tt(), V2)) -> mark(U36(isNat(V2)))
     , active(U36(X)) -> U36(active(X))
     , active(U36(tt())) -> mark(tt())
     , active(U41(X1, X2)) -> U41(active(X1), X2)
     , active(U41(tt(), V2)) -> mark(U42(isNatKind(V2)))
     , active(U42(X)) -> U42(active(X))
     , active(U42(tt())) -> mark(tt())
     , active(U51(X)) -> U51(active(X))
     , active(U51(tt())) -> mark(tt())
     , active(U61(X1, X2)) -> U61(active(X1), X2)
     , active(U61(tt(), V2)) -> mark(U62(isNatKind(V2)))
     , active(U62(X)) -> U62(active(X))
     , active(U62(tt())) -> mark(tt())
     , active(U71(X1, X2)) -> U71(active(X1), X2)
     , active(U71(tt(), N)) -> mark(U72(isNatKind(N), N))
     , active(U72(X1, X2)) -> U72(active(X1), X2)
     , active(U72(tt(), N)) -> mark(N)
     , active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3)
     , active(U81(tt(), M, N)) -> mark(U82(isNatKind(M), M, N))
     , active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3)
     , active(U82(tt(), M, N)) -> mark(U83(isNat(N), M, N))
     , active(U83(X1, X2, X3)) -> U83(active(X1), X2, X3)
     , active(U83(tt(), M, N)) -> mark(U84(isNatKind(N), M, N))
     , active(U84(X1, X2, X3)) -> U84(active(X1), X2, X3)
     , active(U84(tt(), M, N)) -> mark(s(plus(N, M)))
     , active(s(X)) -> s(active(X))
     , active(U91(X1, X2)) -> U91(active(X1), X2)
     , active(U91(tt(), N)) -> mark(U92(isNatKind(N)))
     , active(U92(X)) -> U92(active(X))
     , active(U92(tt())) -> mark(0())
     , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3))
     , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3))
     , U102(mark(X1), X2, X3) -> mark(U102(X1, X2, X3))
     , U102(ok(X1), ok(X2), ok(X3)) -> ok(U102(X1, X2, X3))
     , isNatKind(ok(X)) -> ok(isNatKind(X))
     , U103(mark(X1), X2, X3) -> mark(U103(X1, X2, X3))
     , U103(ok(X1), ok(X2), ok(X3)) -> ok(U103(X1, X2, X3))
     , isNat(ok(X)) -> ok(isNat(X))
     , U104(mark(X1), X2, X3) -> mark(U104(X1, X2, X3))
     , U104(ok(X1), ok(X2), ok(X3)) -> ok(U104(X1, X2, X3))
     , plus(X1, mark(X2)) -> mark(plus(X1, X2))
     , plus(mark(X1), X2) -> mark(plus(X1, X2))
     , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2))
     , x(X1, mark(X2)) -> mark(x(X1, X2))
     , x(mark(X1), X2) -> mark(x(X1, X2))
     , x(ok(X1), ok(X2)) -> ok(x(X1, X2))
     , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3))
     , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3))
     , U12(mark(X1), X2, X3) -> mark(U12(X1, X2, X3))
     , U12(ok(X1), ok(X2), ok(X3)) -> ok(U12(X1, X2, X3))
     , U13(mark(X1), X2, X3) -> mark(U13(X1, X2, X3))
     , U13(ok(X1), ok(X2), ok(X3)) -> ok(U13(X1, X2, X3))
     , U14(mark(X1), X2, X3) -> mark(U14(X1, X2, X3))
     , U14(ok(X1), ok(X2), ok(X3)) -> ok(U14(X1, X2, X3))
     , U15(mark(X1), X2) -> mark(U15(X1, X2))
     , U15(ok(X1), ok(X2)) -> ok(U15(X1, X2))
     , U16(mark(X)) -> mark(U16(X))
     , U16(ok(X)) -> ok(U16(X))
     , U21(mark(X1), X2) -> mark(U21(X1, X2))
     , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2))
     , U22(mark(X1), X2) -> mark(U22(X1, X2))
     , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2))
     , U23(mark(X)) -> mark(U23(X))
     , U23(ok(X)) -> ok(U23(X))
     , U31(mark(X1), X2, X3) -> mark(U31(X1, X2, X3))
     , U31(ok(X1), ok(X2), ok(X3)) -> ok(U31(X1, X2, X3))
     , U32(mark(X1), X2, X3) -> mark(U32(X1, X2, X3))
     , U32(ok(X1), ok(X2), ok(X3)) -> ok(U32(X1, X2, X3))
     , U33(mark(X1), X2, X3) -> mark(U33(X1, X2, X3))
     , U33(ok(X1), ok(X2), ok(X3)) -> ok(U33(X1, X2, X3))
     , U34(mark(X1), X2, X3) -> mark(U34(X1, X2, X3))
     , U34(ok(X1), ok(X2), ok(X3)) -> ok(U34(X1, X2, X3))
     , U35(mark(X1), X2) -> mark(U35(X1, X2))
     , U35(ok(X1), ok(X2)) -> ok(U35(X1, X2))
     , U36(mark(X)) -> mark(U36(X))
     , U36(ok(X)) -> ok(U36(X))
     , U41(mark(X1), X2) -> mark(U41(X1, X2))
     , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2))
     , U42(mark(X)) -> mark(U42(X))
     , U42(ok(X)) -> ok(U42(X))
     , U51(mark(X)) -> mark(U51(X))
     , U51(ok(X)) -> ok(U51(X))
     , U61(mark(X1), X2) -> mark(U61(X1, X2))
     , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2))
     , U62(mark(X)) -> mark(U62(X))
     , U62(ok(X)) -> ok(U62(X))
     , U71(mark(X1), X2) -> mark(U71(X1, X2))
     , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2))
     , U72(mark(X1), X2) -> mark(U72(X1, X2))
     , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2))
     , U81(mark(X1), X2, X3) -> mark(U81(X1, X2, X3))
     , U81(ok(X1), ok(X2), ok(X3)) -> ok(U81(X1, X2, X3))
     , U82(mark(X1), X2, X3) -> mark(U82(X1, X2, X3))
     , U82(ok(X1), ok(X2), ok(X3)) -> ok(U82(X1, X2, X3))
     , U83(mark(X1), X2, X3) -> mark(U83(X1, X2, X3))
     , U83(ok(X1), ok(X2), ok(X3)) -> ok(U83(X1, X2, X3))
     , U84(mark(X1), X2, X3) -> mark(U84(X1, X2, X3))
     , U84(ok(X1), ok(X2), ok(X3)) -> ok(U84(X1, X2, X3))
     , s(mark(X)) -> mark(s(X))
     , s(ok(X)) -> ok(s(X))
     , U91(mark(X1), X2) -> mark(U91(X1, X2))
     , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2))
     , U92(mark(X)) -> mark(U92(X))
     , U92(ok(X)) -> ok(U92(X))
     , proper(U101(X1, X2, X3)) ->
       U101(proper(X1), proper(X2), proper(X3))
     , proper(tt()) -> ok(tt())
     , proper(U102(X1, X2, X3)) ->
       U102(proper(X1), proper(X2), proper(X3))
     , proper(isNatKind(X)) -> isNatKind(proper(X))
     , proper(U103(X1, X2, X3)) ->
       U103(proper(X1), proper(X2), proper(X3))
     , proper(isNat(X)) -> isNat(proper(X))
     , proper(U104(X1, X2, X3)) ->
       U104(proper(X1), proper(X2), proper(X3))
     , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2))
     , proper(x(X1, X2)) -> x(proper(X1), proper(X2))
     , proper(U11(X1, X2, X3)) ->
       U11(proper(X1), proper(X2), proper(X3))
     , proper(U12(X1, X2, X3)) ->
       U12(proper(X1), proper(X2), proper(X3))
     , proper(U13(X1, X2, X3)) ->
       U13(proper(X1), proper(X2), proper(X3))
     , proper(U14(X1, X2, X3)) ->
       U14(proper(X1), proper(X2), proper(X3))
     , proper(U15(X1, X2)) -> U15(proper(X1), proper(X2))
     , proper(U16(X)) -> U16(proper(X))
     , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2))
     , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2))
     , proper(U23(X)) -> U23(proper(X))
     , proper(U31(X1, X2, X3)) ->
       U31(proper(X1), proper(X2), proper(X3))
     , proper(U32(X1, X2, X3)) ->
       U32(proper(X1), proper(X2), proper(X3))
     , proper(U33(X1, X2, X3)) ->
       U33(proper(X1), proper(X2), proper(X3))
     , proper(U34(X1, X2, X3)) ->
       U34(proper(X1), proper(X2), proper(X3))
     , proper(U35(X1, X2)) -> U35(proper(X1), proper(X2))
     , proper(U36(X)) -> U36(proper(X))
     , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2))
     , proper(U42(X)) -> U42(proper(X))
     , proper(U51(X)) -> U51(proper(X))
     , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2))
     , proper(U62(X)) -> U62(proper(X))
     , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2))
     , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2))
     , proper(U81(X1, X2, X3)) ->
       U81(proper(X1), proper(X2), proper(X3))
     , proper(U82(X1, X2, X3)) ->
       U82(proper(X1), proper(X2), proper(X3))
     , proper(U83(X1, X2, X3)) ->
       U83(proper(X1), proper(X2), proper(X3))
     , proper(U84(X1, X2, X3)) ->
       U84(proper(X1), proper(X2), proper(X3))
     , proper(s(X)) -> s(proper(X))
     , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2))
     , proper(U92(X)) -> U92(proper(X))
     , proper(0()) -> ok(0())
     , top(mark(X)) -> top(proper(X))
     , top(ok(X)) -> top(active(X)) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {75,76} by applications of
   Pre({75,76}) = {}. Here rules are labeled as follows:
   
     DPs:
       { 1: U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3))
       , 2: U101^#(ok(X1), ok(X2), ok(X3)) -> c_83(U101^#(X1, X2, X3))
       , 3: U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3))
       , 4: U102^#(ok(X1), ok(X2), ok(X3)) -> c_85(U102^#(X1, X2, X3))
       , 5: U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3))
       , 6: U103^#(ok(X1), ok(X2), ok(X3)) -> c_88(U103^#(X1, X2, X3))
       , 7: U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2))
       , 8: U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2))
       , 9: U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2))
       , 10: U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2))
       , 11: U51^#(mark(X)) -> c_132(U51^#(X))
       , 12: U51^#(ok(X)) -> c_133(U51^#(X))
       , 13: U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3))
       , 14: U104^#(ok(X1), ok(X2), ok(X3)) -> c_91(U104^#(X1, X2, X3))
       , 15: U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3))
       , 16: U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3))
       , 17: U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3))
       , 18: U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3))
       , 19: U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2))
       , 20: U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2))
       , 21: plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2))
       , 22: plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2))
       , 23: plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2))
       , 24: U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3))
       , 25: U81^#(ok(X1), ok(X2), ok(X3)) -> c_143(U81^#(X1, X2, X3))
       , 26: U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2))
       , 27: U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2))
       , 28: x^#(X1, mark(X2)) -> c_95(x^#(X1, X2))
       , 29: x^#(mark(X1), X2) -> c_96(x^#(X1, X2))
       , 30: x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2))
       , 31: U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2))
       , 32: U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2))
       , 33: U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3))
       , 34: U12^#(ok(X1), ok(X2), ok(X3)) -> c_101(U12^#(X1, X2, X3))
       , 35: U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3))
       , 36: U13^#(ok(X1), ok(X2), ok(X3)) -> c_103(U13^#(X1, X2, X3))
       , 37: U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3))
       , 38: U14^#(ok(X1), ok(X2), ok(X3)) -> c_105(U14^#(X1, X2, X3))
       , 39: U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2))
       , 40: U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2))
       , 41: U16^#(mark(X)) -> c_108(U16^#(X))
       , 42: U16^#(ok(X)) -> c_109(U16^#(X))
       , 43: U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2))
       , 44: U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2))
       , 45: U23^#(mark(X)) -> c_114(U23^#(X))
       , 46: U23^#(ok(X)) -> c_115(U23^#(X))
       , 47: U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3))
       , 48: U32^#(ok(X1), ok(X2), ok(X3)) -> c_119(U32^#(X1, X2, X3))
       , 49: U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3))
       , 50: U33^#(ok(X1), ok(X2), ok(X3)) -> c_121(U33^#(X1, X2, X3))
       , 51: U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3))
       , 52: U34^#(ok(X1), ok(X2), ok(X3)) -> c_123(U34^#(X1, X2, X3))
       , 53: U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2))
       , 54: U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2))
       , 55: U36^#(mark(X)) -> c_126(U36^#(X))
       , 56: U36^#(ok(X)) -> c_127(U36^#(X))
       , 57: U42^#(mark(X)) -> c_130(U42^#(X))
       , 58: U42^#(ok(X)) -> c_131(U42^#(X))
       , 59: U62^#(mark(X)) -> c_136(U62^#(X))
       , 60: U62^#(ok(X)) -> c_137(U62^#(X))
       , 61: U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2))
       , 62: U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2))
       , 63: U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3))
       , 64: U82^#(ok(X1), ok(X2), ok(X3)) -> c_145(U82^#(X1, X2, X3))
       , 65: U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3))
       , 66: U83^#(ok(X1), ok(X2), ok(X3)) -> c_147(U83^#(X1, X2, X3))
       , 67: U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3))
       , 68: U84^#(ok(X1), ok(X2), ok(X3)) -> c_149(U84^#(X1, X2, X3))
       , 69: s^#(mark(X)) -> c_150(s^#(X))
       , 70: s^#(ok(X)) -> c_151(s^#(X))
       , 71: U92^#(mark(X)) -> c_154(U92^#(X))
       , 72: U92^#(ok(X)) -> c_155(U92^#(X))
       , 73: isNatKind^#(ok(X)) -> c_86(isNatKind^#(X))
       , 74: isNat^#(ok(X)) -> c_89(isNat^#(X))
       , 75: proper^#(tt()) -> c_157()
       , 76: proper^#(0()) -> c_194()
       , 77: top^#(mark(X)) -> c_195(top^#(proper(X)))
       , 78: top^#(ok(X)) -> c_196(top^#(active(X))) }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3))
     , U101^#(ok(X1), ok(X2), ok(X3)) -> c_83(U101^#(X1, X2, X3))
     , U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3))
     , U102^#(ok(X1), ok(X2), ok(X3)) -> c_85(U102^#(X1, X2, X3))
     , U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3))
     , U103^#(ok(X1), ok(X2), ok(X3)) -> c_88(U103^#(X1, X2, X3))
     , U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2))
     , U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2))
     , U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2))
     , U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2))
     , U51^#(mark(X)) -> c_132(U51^#(X))
     , U51^#(ok(X)) -> c_133(U51^#(X))
     , U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3))
     , U104^#(ok(X1), ok(X2), ok(X3)) -> c_91(U104^#(X1, X2, X3))
     , U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3))
     , U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3))
     , U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3))
     , U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3))
     , U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2))
     , U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2))
     , plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2))
     , plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2))
     , plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2))
     , U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3))
     , U81^#(ok(X1), ok(X2), ok(X3)) -> c_143(U81^#(X1, X2, X3))
     , U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2))
     , U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2))
     , x^#(X1, mark(X2)) -> c_95(x^#(X1, X2))
     , x^#(mark(X1), X2) -> c_96(x^#(X1, X2))
     , x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2))
     , U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2))
     , U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2))
     , U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3))
     , U12^#(ok(X1), ok(X2), ok(X3)) -> c_101(U12^#(X1, X2, X3))
     , U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3))
     , U13^#(ok(X1), ok(X2), ok(X3)) -> c_103(U13^#(X1, X2, X3))
     , U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3))
     , U14^#(ok(X1), ok(X2), ok(X3)) -> c_105(U14^#(X1, X2, X3))
     , U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2))
     , U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2))
     , U16^#(mark(X)) -> c_108(U16^#(X))
     , U16^#(ok(X)) -> c_109(U16^#(X))
     , U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2))
     , U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2))
     , U23^#(mark(X)) -> c_114(U23^#(X))
     , U23^#(ok(X)) -> c_115(U23^#(X))
     , U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3))
     , U32^#(ok(X1), ok(X2), ok(X3)) -> c_119(U32^#(X1, X2, X3))
     , U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3))
     , U33^#(ok(X1), ok(X2), ok(X3)) -> c_121(U33^#(X1, X2, X3))
     , U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3))
     , U34^#(ok(X1), ok(X2), ok(X3)) -> c_123(U34^#(X1, X2, X3))
     , U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2))
     , U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2))
     , U36^#(mark(X)) -> c_126(U36^#(X))
     , U36^#(ok(X)) -> c_127(U36^#(X))
     , U42^#(mark(X)) -> c_130(U42^#(X))
     , U42^#(ok(X)) -> c_131(U42^#(X))
     , U62^#(mark(X)) -> c_136(U62^#(X))
     , U62^#(ok(X)) -> c_137(U62^#(X))
     , U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2))
     , U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2))
     , U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3))
     , U82^#(ok(X1), ok(X2), ok(X3)) -> c_145(U82^#(X1, X2, X3))
     , U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3))
     , U83^#(ok(X1), ok(X2), ok(X3)) -> c_147(U83^#(X1, X2, X3))
     , U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3))
     , U84^#(ok(X1), ok(X2), ok(X3)) -> c_149(U84^#(X1, X2, X3))
     , s^#(mark(X)) -> c_150(s^#(X))
     , s^#(ok(X)) -> c_151(s^#(X))
     , U92^#(mark(X)) -> c_154(U92^#(X))
     , U92^#(ok(X)) -> c_155(U92^#(X))
     , isNatKind^#(ok(X)) -> c_86(isNatKind^#(X))
     , isNat^#(ok(X)) -> c_89(isNat^#(X))
     , top^#(mark(X)) -> c_195(top^#(proper(X)))
     , top^#(ok(X)) -> c_196(top^#(active(X))) }
   Strict Trs:
     { active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3)
     , active(U101(tt(), M, N)) -> mark(U102(isNatKind(M), M, N))
     , active(U102(X1, X2, X3)) -> U102(active(X1), X2, X3)
     , active(U102(tt(), M, N)) -> mark(U103(isNat(N), M, N))
     , active(isNatKind(plus(V1, V2))) -> mark(U41(isNatKind(V1), V2))
     , active(isNatKind(x(V1, V2))) -> mark(U61(isNatKind(V1), V2))
     , active(isNatKind(s(V1))) -> mark(U51(isNatKind(V1)))
     , active(isNatKind(0())) -> mark(tt())
     , active(U103(X1, X2, X3)) -> U103(active(X1), X2, X3)
     , active(U103(tt(), M, N)) -> mark(U104(isNatKind(N), M, N))
     , active(isNat(plus(V1, V2))) -> mark(U11(isNatKind(V1), V1, V2))
     , active(isNat(x(V1, V2))) -> mark(U31(isNatKind(V1), V1, V2))
     , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1))
     , active(isNat(0())) -> mark(tt())
     , active(U104(X1, X2, X3)) -> U104(active(X1), X2, X3)
     , active(U104(tt(), M, N)) -> mark(plus(x(N, M), N))
     , active(plus(X1, X2)) -> plus(X1, active(X2))
     , active(plus(X1, X2)) -> plus(active(X1), X2)
     , active(plus(N, s(M))) -> mark(U81(isNat(M), M, N))
     , active(plus(N, 0())) -> mark(U71(isNat(N), N))
     , active(x(X1, X2)) -> x(X1, active(X2))
     , active(x(X1, X2)) -> x(active(X1), X2)
     , active(x(N, s(M))) -> mark(U101(isNat(M), M, N))
     , active(x(N, 0())) -> mark(U91(isNat(N), N))
     , active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3)
     , active(U11(tt(), V1, V2)) -> mark(U12(isNatKind(V1), V1, V2))
     , active(U12(X1, X2, X3)) -> U12(active(X1), X2, X3)
     , active(U12(tt(), V1, V2)) -> mark(U13(isNatKind(V2), V1, V2))
     , active(U13(X1, X2, X3)) -> U13(active(X1), X2, X3)
     , active(U13(tt(), V1, V2)) -> mark(U14(isNatKind(V2), V1, V2))
     , active(U14(X1, X2, X3)) -> U14(active(X1), X2, X3)
     , active(U14(tt(), V1, V2)) -> mark(U15(isNat(V1), V2))
     , active(U15(X1, X2)) -> U15(active(X1), X2)
     , active(U15(tt(), V2)) -> mark(U16(isNat(V2)))
     , active(U16(X)) -> U16(active(X))
     , active(U16(tt())) -> mark(tt())
     , active(U21(X1, X2)) -> U21(active(X1), X2)
     , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1))
     , active(U22(X1, X2)) -> U22(active(X1), X2)
     , active(U22(tt(), V1)) -> mark(U23(isNat(V1)))
     , active(U23(X)) -> U23(active(X))
     , active(U23(tt())) -> mark(tt())
     , active(U31(X1, X2, X3)) -> U31(active(X1), X2, X3)
     , active(U31(tt(), V1, V2)) -> mark(U32(isNatKind(V1), V1, V2))
     , active(U32(X1, X2, X3)) -> U32(active(X1), X2, X3)
     , active(U32(tt(), V1, V2)) -> mark(U33(isNatKind(V2), V1, V2))
     , active(U33(X1, X2, X3)) -> U33(active(X1), X2, X3)
     , active(U33(tt(), V1, V2)) -> mark(U34(isNatKind(V2), V1, V2))
     , active(U34(X1, X2, X3)) -> U34(active(X1), X2, X3)
     , active(U34(tt(), V1, V2)) -> mark(U35(isNat(V1), V2))
     , active(U35(X1, X2)) -> U35(active(X1), X2)
     , active(U35(tt(), V2)) -> mark(U36(isNat(V2)))
     , active(U36(X)) -> U36(active(X))
     , active(U36(tt())) -> mark(tt())
     , active(U41(X1, X2)) -> U41(active(X1), X2)
     , active(U41(tt(), V2)) -> mark(U42(isNatKind(V2)))
     , active(U42(X)) -> U42(active(X))
     , active(U42(tt())) -> mark(tt())
     , active(U51(X)) -> U51(active(X))
     , active(U51(tt())) -> mark(tt())
     , active(U61(X1, X2)) -> U61(active(X1), X2)
     , active(U61(tt(), V2)) -> mark(U62(isNatKind(V2)))
     , active(U62(X)) -> U62(active(X))
     , active(U62(tt())) -> mark(tt())
     , active(U71(X1, X2)) -> U71(active(X1), X2)
     , active(U71(tt(), N)) -> mark(U72(isNatKind(N), N))
     , active(U72(X1, X2)) -> U72(active(X1), X2)
     , active(U72(tt(), N)) -> mark(N)
     , active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3)
     , active(U81(tt(), M, N)) -> mark(U82(isNatKind(M), M, N))
     , active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3)
     , active(U82(tt(), M, N)) -> mark(U83(isNat(N), M, N))
     , active(U83(X1, X2, X3)) -> U83(active(X1), X2, X3)
     , active(U83(tt(), M, N)) -> mark(U84(isNatKind(N), M, N))
     , active(U84(X1, X2, X3)) -> U84(active(X1), X2, X3)
     , active(U84(tt(), M, N)) -> mark(s(plus(N, M)))
     , active(s(X)) -> s(active(X))
     , active(U91(X1, X2)) -> U91(active(X1), X2)
     , active(U91(tt(), N)) -> mark(U92(isNatKind(N)))
     , active(U92(X)) -> U92(active(X))
     , active(U92(tt())) -> mark(0())
     , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3))
     , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3))
     , U102(mark(X1), X2, X3) -> mark(U102(X1, X2, X3))
     , U102(ok(X1), ok(X2), ok(X3)) -> ok(U102(X1, X2, X3))
     , isNatKind(ok(X)) -> ok(isNatKind(X))
     , U103(mark(X1), X2, X3) -> mark(U103(X1, X2, X3))
     , U103(ok(X1), ok(X2), ok(X3)) -> ok(U103(X1, X2, X3))
     , isNat(ok(X)) -> ok(isNat(X))
     , U104(mark(X1), X2, X3) -> mark(U104(X1, X2, X3))
     , U104(ok(X1), ok(X2), ok(X3)) -> ok(U104(X1, X2, X3))
     , plus(X1, mark(X2)) -> mark(plus(X1, X2))
     , plus(mark(X1), X2) -> mark(plus(X1, X2))
     , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2))
     , x(X1, mark(X2)) -> mark(x(X1, X2))
     , x(mark(X1), X2) -> mark(x(X1, X2))
     , x(ok(X1), ok(X2)) -> ok(x(X1, X2))
     , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3))
     , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3))
     , U12(mark(X1), X2, X3) -> mark(U12(X1, X2, X3))
     , U12(ok(X1), ok(X2), ok(X3)) -> ok(U12(X1, X2, X3))
     , U13(mark(X1), X2, X3) -> mark(U13(X1, X2, X3))
     , U13(ok(X1), ok(X2), ok(X3)) -> ok(U13(X1, X2, X3))
     , U14(mark(X1), X2, X3) -> mark(U14(X1, X2, X3))
     , U14(ok(X1), ok(X2), ok(X3)) -> ok(U14(X1, X2, X3))
     , U15(mark(X1), X2) -> mark(U15(X1, X2))
     , U15(ok(X1), ok(X2)) -> ok(U15(X1, X2))
     , U16(mark(X)) -> mark(U16(X))
     , U16(ok(X)) -> ok(U16(X))
     , U21(mark(X1), X2) -> mark(U21(X1, X2))
     , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2))
     , U22(mark(X1), X2) -> mark(U22(X1, X2))
     , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2))
     , U23(mark(X)) -> mark(U23(X))
     , U23(ok(X)) -> ok(U23(X))
     , U31(mark(X1), X2, X3) -> mark(U31(X1, X2, X3))
     , U31(ok(X1), ok(X2), ok(X3)) -> ok(U31(X1, X2, X3))
     , U32(mark(X1), X2, X3) -> mark(U32(X1, X2, X3))
     , U32(ok(X1), ok(X2), ok(X3)) -> ok(U32(X1, X2, X3))
     , U33(mark(X1), X2, X3) -> mark(U33(X1, X2, X3))
     , U33(ok(X1), ok(X2), ok(X3)) -> ok(U33(X1, X2, X3))
     , U34(mark(X1), X2, X3) -> mark(U34(X1, X2, X3))
     , U34(ok(X1), ok(X2), ok(X3)) -> ok(U34(X1, X2, X3))
     , U35(mark(X1), X2) -> mark(U35(X1, X2))
     , U35(ok(X1), ok(X2)) -> ok(U35(X1, X2))
     , U36(mark(X)) -> mark(U36(X))
     , U36(ok(X)) -> ok(U36(X))
     , U41(mark(X1), X2) -> mark(U41(X1, X2))
     , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2))
     , U42(mark(X)) -> mark(U42(X))
     , U42(ok(X)) -> ok(U42(X))
     , U51(mark(X)) -> mark(U51(X))
     , U51(ok(X)) -> ok(U51(X))
     , U61(mark(X1), X2) -> mark(U61(X1, X2))
     , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2))
     , U62(mark(X)) -> mark(U62(X))
     , U62(ok(X)) -> ok(U62(X))
     , U71(mark(X1), X2) -> mark(U71(X1, X2))
     , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2))
     , U72(mark(X1), X2) -> mark(U72(X1, X2))
     , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2))
     , U81(mark(X1), X2, X3) -> mark(U81(X1, X2, X3))
     , U81(ok(X1), ok(X2), ok(X3)) -> ok(U81(X1, X2, X3))
     , U82(mark(X1), X2, X3) -> mark(U82(X1, X2, X3))
     , U82(ok(X1), ok(X2), ok(X3)) -> ok(U82(X1, X2, X3))
     , U83(mark(X1), X2, X3) -> mark(U83(X1, X2, X3))
     , U83(ok(X1), ok(X2), ok(X3)) -> ok(U83(X1, X2, X3))
     , U84(mark(X1), X2, X3) -> mark(U84(X1, X2, X3))
     , U84(ok(X1), ok(X2), ok(X3)) -> ok(U84(X1, X2, X3))
     , s(mark(X)) -> mark(s(X))
     , s(ok(X)) -> ok(s(X))
     , U91(mark(X1), X2) -> mark(U91(X1, X2))
     , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2))
     , U92(mark(X)) -> mark(U92(X))
     , U92(ok(X)) -> ok(U92(X))
     , proper(U101(X1, X2, X3)) ->
       U101(proper(X1), proper(X2), proper(X3))
     , proper(tt()) -> ok(tt())
     , proper(U102(X1, X2, X3)) ->
       U102(proper(X1), proper(X2), proper(X3))
     , proper(isNatKind(X)) -> isNatKind(proper(X))
     , proper(U103(X1, X2, X3)) ->
       U103(proper(X1), proper(X2), proper(X3))
     , proper(isNat(X)) -> isNat(proper(X))
     , proper(U104(X1, X2, X3)) ->
       U104(proper(X1), proper(X2), proper(X3))
     , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2))
     , proper(x(X1, X2)) -> x(proper(X1), proper(X2))
     , proper(U11(X1, X2, X3)) ->
       U11(proper(X1), proper(X2), proper(X3))
     , proper(U12(X1, X2, X3)) ->
       U12(proper(X1), proper(X2), proper(X3))
     , proper(U13(X1, X2, X3)) ->
       U13(proper(X1), proper(X2), proper(X3))
     , proper(U14(X1, X2, X3)) ->
       U14(proper(X1), proper(X2), proper(X3))
     , proper(U15(X1, X2)) -> U15(proper(X1), proper(X2))
     , proper(U16(X)) -> U16(proper(X))
     , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2))
     , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2))
     , proper(U23(X)) -> U23(proper(X))
     , proper(U31(X1, X2, X3)) ->
       U31(proper(X1), proper(X2), proper(X3))
     , proper(U32(X1, X2, X3)) ->
       U32(proper(X1), proper(X2), proper(X3))
     , proper(U33(X1, X2, X3)) ->
       U33(proper(X1), proper(X2), proper(X3))
     , proper(U34(X1, X2, X3)) ->
       U34(proper(X1), proper(X2), proper(X3))
     , proper(U35(X1, X2)) -> U35(proper(X1), proper(X2))
     , proper(U36(X)) -> U36(proper(X))
     , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2))
     , proper(U42(X)) -> U42(proper(X))
     , proper(U51(X)) -> U51(proper(X))
     , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2))
     , proper(U62(X)) -> U62(proper(X))
     , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2))
     , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2))
     , proper(U81(X1, X2, X3)) ->
       U81(proper(X1), proper(X2), proper(X3))
     , proper(U82(X1, X2, X3)) ->
       U82(proper(X1), proper(X2), proper(X3))
     , proper(U83(X1, X2, X3)) ->
       U83(proper(X1), proper(X2), proper(X3))
     , proper(U84(X1, X2, X3)) ->
       U84(proper(X1), proper(X2), proper(X3))
     , proper(s(X)) -> s(proper(X))
     , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2))
     , proper(U92(X)) -> U92(proper(X))
     , proper(0()) -> ok(0())
     , top(mark(X)) -> top(proper(X))
     , top(ok(X)) -> top(active(X)) }
   Weak DPs:
     { proper^#(tt()) -> c_157()
     , proper^#(0()) -> c_194() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..