MAYBE 0.00/0.02 The problem does not contain well-formed TRSs: 0.00/0.02 Strict Trs: 0.00/0.02 { U41(tt()) -> N 0.00/0.02 , U52(tt()) -> s(plus(N, M)) 0.00/0.02 , plus(N, s(M)) -> U51(isNat()) 0.00/0.02 , plus(N, 0()) -> U41(isNat()) 0.00/0.02 , U72(tt()) -> plus(x(N, M), N) 0.00/0.02 , x(N, s(M)) -> U71(isNat()) 0.00/0.02 , x(N, 0()) -> U61(isNat()) 0.00/0.02 , U11(tt()) -> U12(isNat()) 0.00/0.02 , U12(tt()) -> tt() 0.00/0.02 , isNat() -> tt() 0.00/0.02 , isNat() -> U11(isNat()) 0.00/0.02 , isNat() -> U21(isNat()) 0.00/0.02 , isNat() -> U31(isNat()) 0.00/0.02 , U21(tt()) -> tt() 0.00/0.02 , U31(tt()) -> U32(isNat()) 0.00/0.02 , U32(tt()) -> tt() 0.00/0.02 , U51(tt()) -> U52(isNat()) 0.00/0.02 , U61(tt()) -> 0() 0.00/0.02 , U71(tt()) -> U72(isNat()) } 0.00/0.02 StartTerms: basic terms 0.00/0.02 Strategy: none 0.00/0.02 EOF