MAYBE 0.00/0.03 The problem does not contain well-formed TRSs: 0.00/0.03 Strict Trs: 0.00/0.03 { U104(tt()) -> plus(x(N, M), N) 0.00/0.03 , plus(N, s(M)) -> U81(isNat()) 0.00/0.03 , plus(N, 0()) -> U71(isNat()) 0.00/0.03 , x(N, s(M)) -> U101(isNat()) 0.00/0.03 , x(N, 0()) -> U91(isNat()) 0.00/0.03 , U72(tt()) -> N 0.00/0.03 , U84(tt()) -> s(plus(N, M)) 0.00/0.03 , U101(tt()) -> U102(isNatKind()) 0.00/0.03 , U102(tt()) -> U103(isNat()) 0.00/0.03 , isNatKind() -> tt() 0.00/0.03 , isNatKind() -> U41(isNatKind()) 0.00/0.04 , isNatKind() -> U51(isNatKind()) 0.00/0.04 , isNatKind() -> U61(isNatKind()) 0.00/0.04 , U103(tt()) -> U104(isNatKind()) 0.00/0.04 , isNat() -> tt() 0.00/0.04 , isNat() -> U11(isNatKind()) 0.00/0.04 , isNat() -> U21(isNatKind()) 0.00/0.04 , isNat() -> U31(isNatKind()) 0.00/0.04 , U11(tt()) -> U12(isNatKind()) 0.00/0.04 , U12(tt()) -> U13(isNatKind()) 0.00/0.04 , U13(tt()) -> U14(isNatKind()) 0.00/0.04 , U14(tt()) -> U15(isNat()) 0.00/0.04 , U15(tt()) -> U16(isNat()) 0.00/0.04 , U16(tt()) -> tt() 0.00/0.04 , U21(tt()) -> U22(isNatKind()) 0.00/0.04 , U22(tt()) -> U23(isNat()) 0.00/0.04 , U23(tt()) -> tt() 0.00/0.04 , U31(tt()) -> U32(isNatKind()) 0.00/0.04 , U32(tt()) -> U33(isNatKind()) 0.00/0.04 , U33(tt()) -> U34(isNatKind()) 0.00/0.04 , U34(tt()) -> U35(isNat()) 0.00/0.04 , U35(tt()) -> U36(isNat()) 0.00/0.04 , U36(tt()) -> tt() 0.00/0.04 , U41(tt()) -> U42(isNatKind()) 0.00/0.04 , U42(tt()) -> tt() 0.00/0.04 , U51(tt()) -> tt() 0.00/0.04 , U61(tt()) -> U62(isNatKind()) 0.00/0.04 , U62(tt()) -> tt() 0.00/0.04 , U71(tt()) -> U72(isNatKind()) 0.00/0.04 , U81(tt()) -> U82(isNatKind()) 0.00/0.04 , U82(tt()) -> U83(isNat()) 0.00/0.04 , U83(tt()) -> U84(isNatKind()) 0.00/0.04 , U91(tt()) -> U92(isNatKind()) 0.00/0.04 , U92(tt()) -> 0() } 0.00/0.04 StartTerms: all 0.00/0.04 Strategy: none 0.00/0.04 EOF