Input TRS: 1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) 2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) 3: a__U13(tt()) -> tt() 4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) 5: a__U22(tt()) -> tt() 6: a__U31(tt(),V1,V2) -> a__U32(a__isNat(V1),V2) 7: a__U32(tt(),V2) -> a__U33(a__isNat(V2)) 8: a__U33(tt()) -> tt() 9: a__U41(tt(),N) -> mark(N) 10: a__U51(tt(),M,N) -> s(a__plus(mark(N),mark(M))) 11: a__U61(tt()) -> 0() 12: a__U71(tt(),M,N) -> a__plus(a__x(mark(N),mark(M)),mark(N)) 13: a__and(tt(),X) -> mark(X) 14: a__isNat(0()) -> tt() 15: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) 16: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) 17: a__isNat(x(V1,V2)) -> a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) 18: a__isNatKind(0()) -> tt() 19: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) 20: a__isNatKind(s(V1)) -> a__isNatKind(V1) 21: a__isNatKind(x(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) 22: a__plus(N,0()) -> a__U41(a__and(a__isNat(N),isNatKind(N)),N) 23: a__plus(N,s(M)) -> a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) 24: a__x(N,0()) -> a__U61(a__and(a__isNat(N),isNatKind(N))) 25: a__x(N,s(M)) -> a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) 26: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) 27: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) 28: mark(isNat(X)) -> a__isNat(X) 29: mark(U13(X)) -> a__U13(mark(X)) 30: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) 31: mark(U22(X)) -> a__U22(mark(X)) 32: mark(U31(X1,X2,X3)) -> a__U31(mark(X1),X2,X3) 33: mark(U32(X1,X2)) -> a__U32(mark(X1),X2) 34: mark(U33(X)) -> a__U33(mark(X)) 35: mark(U41(X1,X2)) -> a__U41(mark(X1),X2) 36: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) 37: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) 38: mark(U61(X)) -> a__U61(mark(X)) 39: mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3) 40: mark(x(X1,X2)) -> a__x(mark(X1),mark(X2)) 41: mark(and(X1,X2)) -> a__and(mark(X1),X2) 42: mark(isNatKind(X)) -> a__isNatKind(X) 43: mark(tt()) -> tt() 44: mark(s(X)) -> s(mark(X)) 45: mark(0()) -> 0() 46: a__U11(X1,X2,X3) -> U11(X1,X2,X3) 47: a__U12(X1,X2) -> U12(X1,X2) 48: a__isNat(X) -> isNat(X) 49: a__U13(X) -> U13(X) 50: a__U21(X1,X2) -> U21(X1,X2) 51: a__U22(X) -> U22(X) 52: a__U31(X1,X2,X3) -> U31(X1,X2,X3) 53: a__U32(X1,X2) -> U32(X1,X2) 54: a__U33(X) -> U33(X) 55: a__U41(X1,X2) -> U41(X1,X2) 56: a__U51(X1,X2,X3) -> U51(X1,X2,X3) 57: a__plus(X1,X2) -> plus(X1,X2) 58: a__U61(X) -> U61(X) 59: a__U71(X1,X2,X3) -> U71(X1,X2,X3) 60: a__x(X1,X2) -> x(X1,X2) 61: a__and(X1,X2) -> and(X1,X2) 62: a__isNatKind(X) -> isNatKind(X) Number of strict rules: 62 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #a__U12(tt(),V2) -> #a__U13(a__isNat(V2)) #2: #a__U12(tt(),V2) -> #a__isNat(V2) #3: #mark(U13(X)) -> #a__U13(mark(X)) #4: #mark(U13(X)) -> #mark(X) #5: #mark(U41(X1,X2)) -> #a__U41(mark(X1),X2) #6: #mark(U41(X1,X2)) -> #mark(X1) #7: #mark(isNatKind(X)) -> #a__isNatKind(X) #8: #mark(and(X1,X2)) -> #a__and(mark(X1),X2) #9: #mark(and(X1,X2)) -> #mark(X1) #10: #mark(plus(X1,X2)) -> #a__plus(mark(X1),mark(X2)) #11: #mark(plus(X1,X2)) -> #mark(X1) #12: #mark(plus(X1,X2)) -> #mark(X2) #13: #mark(U61(X)) -> #a__U61(mark(X)) #14: #mark(U61(X)) -> #mark(X) #15: #a__U31(tt(),V1,V2) -> #a__U32(a__isNat(V1),V2) #16: #a__U31(tt(),V1,V2) -> #a__isNat(V1) #17: #mark(x(X1,X2)) -> #a__x(mark(X1),mark(X2)) #18: #mark(x(X1,X2)) -> #mark(X1) #19: #mark(x(X1,X2)) -> #mark(X2) #20: #a__and(tt(),X) -> #mark(X) #21: #a__U41(tt(),N) -> #mark(N) #22: #a__x(N,0()) -> #a__U61(a__and(a__isNat(N),isNatKind(N))) #23: #a__x(N,0()) -> #a__and(a__isNat(N),isNatKind(N)) #24: #a__x(N,0()) -> #a__isNat(N) #25: #a__plus(N,s(M)) -> #a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) #26: #a__plus(N,s(M)) -> #a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) #27: #a__plus(N,s(M)) -> #a__and(a__isNat(M),isNatKind(M)) #28: #a__plus(N,s(M)) -> #a__isNat(M) #29: #a__U71(tt(),M,N) -> #a__plus(a__x(mark(N),mark(M)),mark(N)) #30: #a__U71(tt(),M,N) -> #a__x(mark(N),mark(M)) #31: #a__U71(tt(),M,N) -> #mark(N) #32: #a__U71(tt(),M,N) -> #mark(M) #33: #a__U71(tt(),M,N) -> #mark(N) #34: #mark(U22(X)) -> #a__U22(mark(X)) #35: #mark(U22(X)) -> #mark(X) #36: #mark(U21(X1,X2)) -> #a__U21(mark(X1),X2) #37: #mark(U21(X1,X2)) -> #mark(X1) #38: #a__x(N,s(M)) -> #a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) #39: #a__x(N,s(M)) -> #a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) #40: #a__x(N,s(M)) -> #a__and(a__isNat(M),isNatKind(M)) #41: #a__x(N,s(M)) -> #a__isNat(M) #42: #a__isNatKind(s(V1)) -> #a__isNatKind(V1) #43: #a__U32(tt(),V2) -> #a__U33(a__isNat(V2)) #44: #a__U32(tt(),V2) -> #a__isNat(V2) #45: #mark(U71(X1,X2,X3)) -> #a__U71(mark(X1),X2,X3) #46: #mark(U71(X1,X2,X3)) -> #mark(X1) #47: #a__U51(tt(),M,N) -> #a__plus(mark(N),mark(M)) #48: #a__U51(tt(),M,N) -> #mark(N) #49: #a__U51(tt(),M,N) -> #mark(M) #50: #mark(U32(X1,X2)) -> #a__U32(mark(X1),X2) #51: #mark(U32(X1,X2)) -> #mark(X1) #52: #mark(s(X)) -> #mark(X) #53: #mark(isNat(X)) -> #a__isNat(X) #54: #a__plus(N,0()) -> #a__U41(a__and(a__isNat(N),isNatKind(N)),N) #55: #a__plus(N,0()) -> #a__and(a__isNat(N),isNatKind(N)) #56: #a__plus(N,0()) -> #a__isNat(N) #57: #mark(U33(X)) -> #a__U33(mark(X)) #58: #mark(U33(X)) -> #mark(X) #59: #mark(U12(X1,X2)) -> #a__U12(mark(X1),X2) #60: #mark(U12(X1,X2)) -> #mark(X1) #61: #a__isNat(x(V1,V2)) -> #a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) #62: #a__isNat(x(V1,V2)) -> #a__and(a__isNatKind(V1),isNatKind(V2)) #63: #a__isNat(x(V1,V2)) -> #a__isNatKind(V1) #64: #mark(U31(X1,X2,X3)) -> #a__U31(mark(X1),X2,X3) #65: #mark(U31(X1,X2,X3)) -> #mark(X1) #66: #a__isNatKind(plus(V1,V2)) -> #a__and(a__isNatKind(V1),isNatKind(V2)) #67: #a__isNatKind(plus(V1,V2)) -> #a__isNatKind(V1) #68: #mark(U11(X1,X2,X3)) -> #a__U11(mark(X1),X2,X3) #69: #mark(U11(X1,X2,X3)) -> #mark(X1) #70: #mark(U51(X1,X2,X3)) -> #a__U51(mark(X1),X2,X3) #71: #mark(U51(X1,X2,X3)) -> #mark(X1) #72: #a__isNatKind(x(V1,V2)) -> #a__and(a__isNatKind(V1),isNatKind(V2)) #73: #a__isNatKind(x(V1,V2)) -> #a__isNatKind(V1) #74: #a__isNat(s(V1)) -> #a__U21(a__isNatKind(V1),V1) #75: #a__isNat(s(V1)) -> #a__isNatKind(V1) #76: #a__U11(tt(),V1,V2) -> #a__U12(a__isNat(V1),V2) #77: #a__U11(tt(),V1,V2) -> #a__isNat(V1) #78: #a__isNat(plus(V1,V2)) -> #a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) #79: #a__isNat(plus(V1,V2)) -> #a__and(a__isNatKind(V1),isNatKind(V2)) #80: #a__isNat(plus(V1,V2)) -> #a__isNatKind(V1) #81: #a__U21(tt(),V1) -> #a__U22(a__isNat(V1)) #82: #a__U21(tt(),V1) -> #a__isNat(V1) Number of SCCs: 1, DPs: 74, edges: 966 SCC { #2 #4..12 #14..21 #23..33 #35..42 #44..56 #58..80 #82 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. #a__isNatKind(x1) weight: (/ 1 32) + x1 isNatKind(x1) weight: x1 a__plus(x1,x2) weight: max{(/ 1 4) + x2, x1} U21(x1,x2) weight: max{x2, x1} #a__U71(x1,x2,x3) weight: max{0, (/ 15 32) + x3, (/ 7 16) + x2} U11(x1,x2,x3) weight: max{(/ 3 32) + x3, x2, x1} s(x1) weight: x1 #a__U31(x1,x2,x3) weight: max{(/ 1 4) + x3, (/ 7 32) + x2, (/ 7 32) + x1} #a__U33(x1) weight: 0 a__U33(x1) weight: (/ 1 32) + x1 #a__isNat(x1) weight: (/ 1 32) + x1 U71(x1,x2,x3) weight: max{(/ 1 4) + x3, (/ 7 32) + x2, (/ 3 16) + x1} and(x1,x2) weight: max{x2, x1} #a__U13(x1) weight: 0 #a__U51(x1,x2,x3) weight: max{0, (/ 7 32) + x3, (/ 15 32) + x2} #a__x(x1,x2) weight: max{(/ 7 16) + x2, (/ 15 32) + x1} a__U22(x1) weight: x1 #a__U11(x1,x2,x3) weight: max{0, (/ 3 32) + x3, (/ 1 32) + x2} a__U31(x1,x2,x3) weight: max{(/ 3 16) + x3, (/ 7 32) + x2, (/ 1 16) + x1} a__U51(x1,x2,x3) weight: max{x3, (/ 1 4) + x2, x1} a__x(x1,x2) weight: max{(/ 7 32) + x2, (/ 1 4) + x1} U12(x1,x2) weight: max{(/ 3 32) + x2, x1} a__U41(x1,x2) weight: max{x2, x1} x(x1,x2) weight: max{(/ 7 32) + x2, (/ 1 4) + x1} #a__U12(x1,x2) weight: max{0, (/ 1 16) + x2} #a__U21(x1,x2) weight: max{0, (/ 1 32) + x2} #a__U61(x1) weight: 0 #a__plus(x1,x2) weight: max{(/ 15 32) + x2, (/ 7 32) + x1} #mark(x1) weight: (/ 7 32) + x1 0() weight: (/ 1 16) #a__and(x1,x2) weight: max{0, (/ 7 32) + x2} a__U21(x1,x2) weight: max{x2, x1} a__U32(x1,x2) weight: max{(/ 5 32) + x2, (/ 3 16) + x1} mark(x1) weight: x1 a__U11(x1,x2,x3) weight: max{(/ 3 32) + x3, x2, x1} U32(x1,x2) weight: max{(/ 5 32) + x2, (/ 3 16) + x1} U33(x1) weight: (/ 1 32) + x1 a__U12(x1,x2) weight: max{(/ 3 32) + x2, x1} isNat(x1) weight: x1 plus(x1,x2) weight: max{(/ 1 4) + x2, x1} U61(x1) weight: (/ 1 32) + x1 #a__U22(x1) weight: 0 a__U13(x1) weight: (/ 3 32) + x1 U31(x1,x2,x3) weight: max{(/ 3 16) + x3, (/ 7 32) + x2, (/ 1 16) + x1} a__U71(x1,x2,x3) weight: max{(/ 1 4) + x3, (/ 7 32) + x2, (/ 3 16) + x1} a__U61(x1) weight: (/ 1 32) + x1 #a__U41(x1,x2) weight: max{(/ 7 32) + x2, (/ 3 16) + x1} tt() weight: (/ 1 16) a__isNat(x1) weight: x1 U13(x1) weight: (/ 3 32) + x1 a__isNatKind(x1) weight: x1 U22(x1) weight: x1 U51(x1,x2,x3) weight: max{x3, (/ 1 4) + x2, x1} a__and(x1,x2) weight: max{x2, x1} U41(x1,x2) weight: max{x2, x1} #a__U32(x1,x2) weight: max{0, (/ 1 16) + x2} Usable rules: { 1..62 } Removed DPs: #2 #4 #7 #12 #14..16 #18 #19 #23 #24 #27 #28 #31..33 #36 #39..41 #44 #46 #49..51 #53 #56 #58 #59 #62..66 #68 #72 #73 #76 #79 Number of SCCs: 3, DPs: 32, edges: 217 SCC { #42 #67 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #a__isNatKind(x1) weight: x1 isNatKind(x1) weight: (/ 1 16) + x1 a__plus(x1,x2) weight: x2 U21(x1,x2) weight: (/ 1 8) + x1 #a__U71(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: (/ 3 8) + x1 + x3 s(x1) weight: (/ 1 16) + x1 #a__U31(x1,x2,x3) weight: 0 #a__U33(x1) weight: 0 a__U33(x1) weight: (/ 7 16) #a__isNat(x1) weight: 0 U71(x1,x2,x3) weight: (/ 1 16) and(x1,x2) weight: (/ 1 4) + x2 #a__U13(x1) weight: 0 #a__U51(x1,x2,x3) weight: 0 #a__x(x1,x2) weight: 0 a__U22(x1) weight: (/ 1 4) #a__U11(x1,x2,x3) weight: 0 a__U31(x1,x2,x3) weight: (/ 5 16) a__U51(x1,x2,x3) weight: (/ 1 8) + x1 + x2 + x3 a__x(x1,x2) weight: (/ 1 16) U12(x1,x2) weight: (/ 7 16) a__U41(x1,x2) weight: (/ 1 16) x(x1,x2) weight: (/ 1 8) + x2 #a__U12(x1,x2) weight: 0 #a__U21(x1,x2) weight: 0 #a__U61(x1) weight: 0 #a__plus(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #a__and(x1,x2) weight: 0 a__U21(x1,x2) weight: (/ 1 16) + x1 + x2 a__U32(x1,x2) weight: (/ 3 8) mark(x1) weight: (/ 1 8) + x1 a__U11(x1,x2,x3) weight: (/ 5 16) + x2 U32(x1,x2) weight: (/ 1 16) + x2 U33(x1) weight: (/ 1 2) + x1 a__U12(x1,x2) weight: (/ 3 8) + x2 isNat(x1) weight: (/ 1 16) plus(x1,x2) weight: (/ 1 16) + x1 U61(x1) weight: (/ 3 16) + x1 #a__U22(x1) weight: 0 a__U13(x1) weight: (/ 7 16) U31(x1,x2,x3) weight: (/ 3 8) + x1 + x2 + x3 a__U71(x1,x2,x3) weight: x1 + x2 a__U61(x1) weight: (/ 1 8) #a__U41(x1,x2) weight: 0 tt() weight: 0 a__isNat(x1) weight: (/ 1 4) U13(x1) weight: (/ 1 2) a__isNatKind(x1) weight: (/ 1 4) + x1 U22(x1) weight: (/ 1 16) + x1 U51(x1,x2,x3) weight: (/ 3 16) + x1 a__and(x1,x2) weight: (/ 7 16) U41(x1,x2) weight: (/ 1 8) + x1 + x2 #a__U32(x1,x2) weight: 0 Usable rules: { } Removed DPs: #42 #67 Number of SCCs: 2, DPs: 30, edges: 213 SCC { #74 #77 #78 #82 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #a__isNatKind(x1) weight: 0 isNatKind(x1) weight: (/ 1 16) + x1 a__plus(x1,x2) weight: x2 U21(x1,x2) weight: (/ 1 8) + x1 #a__U71(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: (/ 3 8) + x1 + x3 s(x1) weight: (/ 1 8) + x1 #a__U31(x1,x2,x3) weight: 0 #a__U33(x1) weight: 0 a__U33(x1) weight: (/ 7 16) #a__isNat(x1) weight: x1 U71(x1,x2,x3) weight: (/ 1 16) and(x1,x2) weight: (/ 1 4) + x2 #a__U13(x1) weight: 0 #a__U51(x1,x2,x3) weight: 0 #a__x(x1,x2) weight: 0 a__U22(x1) weight: (/ 1 4) #a__U11(x1,x2,x3) weight: (/ 1 16) + x2 a__U31(x1,x2,x3) weight: (/ 5 16) a__U51(x1,x2,x3) weight: (/ 3 16) + x1 + x2 + x3 a__x(x1,x2) weight: (/ 1 16) U12(x1,x2) weight: (/ 7 16) a__U41(x1,x2) weight: (/ 1 16) x(x1,x2) weight: (/ 1 8) + x2 #a__U12(x1,x2) weight: 0 #a__U21(x1,x2) weight: (/ 1 16) + x2 #a__U61(x1) weight: 0 #a__plus(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #a__and(x1,x2) weight: 0 a__U21(x1,x2) weight: (/ 1 16) + x1 + x2 a__U32(x1,x2) weight: (/ 3 8) mark(x1) weight: (/ 1 8) + x1 a__U11(x1,x2,x3) weight: (/ 5 16) + x2 U32(x1,x2) weight: (/ 1 16) + x2 U33(x1) weight: (/ 1 2) + x1 a__U12(x1,x2) weight: (/ 3 8) + x2 isNat(x1) weight: (/ 1 16) plus(x1,x2) weight: (/ 1 8) + x1 U61(x1) weight: (/ 3 16) + x1 #a__U22(x1) weight: 0 a__U13(x1) weight: (/ 7 16) U31(x1,x2,x3) weight: (/ 3 8) + x1 + x2 + x3 a__U71(x1,x2,x3) weight: x1 + x2 a__U61(x1) weight: (/ 1 8) #a__U41(x1,x2) weight: 0 tt() weight: 0 a__isNat(x1) weight: (/ 1 4) U13(x1) weight: (/ 1 2) a__isNatKind(x1) weight: (/ 1 4) + x1 U22(x1) weight: (/ 1 16) + x1 U51(x1,x2,x3) weight: (/ 1 4) + x1 a__and(x1,x2) weight: (/ 7 16) U41(x1,x2) weight: (/ 1 8) + x1 + x2 #a__U32(x1,x2) weight: 0 Usable rules: { } Removed DPs: #74 #77 #78 #82 Number of SCCs: 1, DPs: 26, edges: 207 SCC { #5 #6 #8..11 #17 #20 #21 #25 #26 #29 #30 #35 #37 #38 #45 #47 #48 #52 #54 #55 #60 #69..71 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. #a__isNatKind(x1) weight: (/ 1 16) isNatKind(x1) weight: 0 a__plus(x1,x2) weight: max{(/ 1 4) + x2, x1} U21(x1,x2) weight: max{x2, x1} #a__U71(x1,x2,x3) weight: max{0, (/ 1 2) + x3, (/ 5 16) + x2} U11(x1,x2,x3) weight: max{(/ 1 16) + x3, x2, x1} s(x1) weight: x1 #a__U31(x1,x2,x3) weight: 0 #a__U33(x1) weight: 0 a__U33(x1) weight: (/ 1 16) #a__isNat(x1) weight: (/ 1 16) U71(x1,x2,x3) weight: max{(/ 3 8) + x3, (/ 3 16) + x2, (/ 1 16) + x1} and(x1,x2) weight: max{x2, x1} #a__U13(x1) weight: 0 #a__U51(x1,x2,x3) weight: max{0, (/ 1 8) + x3, (/ 1 16) + x2} #a__x(x1,x2) weight: max{(/ 5 16) + x2, (/ 1 2) + x1} a__U22(x1) weight: x1 #a__U11(x1,x2,x3) weight: 0 a__U31(x1,x2,x3) weight: max{0, (/ 1 8) + x3, (/ 3 16) + x2} a__U51(x1,x2,x3) weight: max{x3, (/ 1 4) + x2, x1} a__x(x1,x2) weight: max{(/ 3 16) + x2, (/ 3 8) + x1} U12(x1,x2) weight: max{(/ 1 16) + x2, x1} a__U41(x1,x2) weight: max{x2, x1} x(x1,x2) weight: max{(/ 3 16) + x2, (/ 3 8) + x1} #a__U12(x1,x2) weight: 0 #a__U21(x1,x2) weight: 0 #a__U61(x1) weight: 0 #a__plus(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 8) + x1} #mark(x1) weight: (/ 1 8) + x1 0() weight: (/ 1 8) #a__and(x1,x2) weight: max{0, (/ 1 8) + x2} a__U21(x1,x2) weight: max{x2, x1} a__U32(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 8) + x1} mark(x1) weight: x1 a__U11(x1,x2,x3) weight: max{(/ 1 16) + x3, x2, x1} U32(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 8) + x1} U33(x1) weight: (/ 1 16) a__U12(x1,x2) weight: max{(/ 1 16) + x2, x1} isNat(x1) weight: x1 plus(x1,x2) weight: max{(/ 1 4) + x2, x1} U61(x1) weight: (/ 3 8) + x1 #a__U22(x1) weight: 0 a__U13(x1) weight: (/ 1 16) + x1 U31(x1,x2,x3) weight: max{0, (/ 1 8) + x3, (/ 3 16) + x2} a__U71(x1,x2,x3) weight: max{(/ 3 8) + x3, (/ 3 16) + x2, (/ 1 16) + x1} a__U61(x1) weight: (/ 3 8) + x1 #a__U41(x1,x2) weight: max{0, (/ 1 8) + x2} tt() weight: 0 a__isNat(x1) weight: x1 U13(x1) weight: (/ 1 16) + x1 a__isNatKind(x1) weight: 0 U22(x1) weight: x1 U51(x1,x2,x3) weight: max{x3, (/ 1 4) + x2, x1} a__and(x1,x2) weight: max{x2, x1} U41(x1,x2) weight: max{x2, x1} #a__U32(x1,x2) weight: 0 Usable rules: { 1..62 } Removed DPs: #55 Number of SCCs: 1, DPs: 25, edges: 203 SCC { #5 #6 #8..11 #17 #20 #21 #25 #26 #29 #30 #35 #37 #38 #45 #47 #48 #52 #54 #60 #69..71 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. #a__isNatKind(x1) weight: (/ 1 4) isNatKind(x1) weight: 0 a__plus(x1,x2) weight: max{(/ 1 4) + x2, x1} U21(x1,x2) weight: max{0, x1} #a__U71(x1,x2,x3) weight: max{0, (/ 3 4) + x3, (/ 1 2) + x1} U11(x1,x2,x3) weight: max{0, x1} s(x1) weight: x1 #a__U31(x1,x2,x3) weight: 0 #a__U33(x1) weight: 0 a__U33(x1) weight: 0 #a__isNat(x1) weight: (/ 1 4) U71(x1,x2,x3) weight: max{0, (/ 1 2) + x3, (/ 1 4) + x1} and(x1,x2) weight: max{x2, x1} #a__U13(x1) weight: 0 #a__U51(x1,x2,x3) weight: max{(/ 1 4) + x3, (/ 1 4) + x2, (/ 1 4) + x1} #a__x(x1,x2) weight: max{0, (/ 3 4) + x1} a__U22(x1) weight: x1 #a__U11(x1,x2,x3) weight: 0 a__U31(x1,x2,x3) weight: 0 a__U51(x1,x2,x3) weight: max{x3, (/ 1 4) + x2, x1} a__x(x1,x2) weight: max{0, (/ 1 2) + x1} U12(x1,x2) weight: max{0, x1} a__U41(x1,x2) weight: max{x2, (/ 1 4) + x1} x(x1,x2) weight: max{0, (/ 1 2) + x1} #a__U12(x1,x2) weight: 0 #a__U21(x1,x2) weight: 0 #a__U61(x1) weight: 0 #a__plus(x1,x2) weight: max{(/ 1 4) + x2, (/ 1 4) + x1} #mark(x1) weight: (/ 1 4) + x1 0() weight: (/ 1 4) #a__and(x1,x2) weight: max{0, (/ 1 4) + x2} a__U21(x1,x2) weight: max{0, x1} a__U32(x1,x2) weight: 0 mark(x1) weight: x1 a__U11(x1,x2,x3) weight: max{0, x1} U32(x1,x2) weight: 0 U33(x1) weight: 0 a__U12(x1,x2) weight: max{0, x1} isNat(x1) weight: 0 plus(x1,x2) weight: max{(/ 1 4) + x2, x1} U61(x1) weight: (/ 1 4) #a__U22(x1) weight: 0 a__U13(x1) weight: 0 U31(x1,x2,x3) weight: 0 a__U71(x1,x2,x3) weight: max{0, (/ 1 2) + x3, (/ 1 4) + x1} a__U61(x1) weight: (/ 1 4) #a__U41(x1,x2) weight: max{0, (/ 1 4) + x2} tt() weight: 0 a__isNat(x1) weight: 0 U13(x1) weight: 0 a__isNatKind(x1) weight: 0 U22(x1) weight: x1 U51(x1,x2,x3) weight: max{x3, (/ 1 4) + x2, x1} a__and(x1,x2) weight: max{x2, x1} U41(x1,x2) weight: max{x2, (/ 1 4) + x1} #a__U32(x1,x2) weight: 0 Usable rules: { 1..62 } Removed DPs: #6 Number of SCCs: 1, DPs: 24, edges: 177 SCC { #5 #8..11 #17 #20 #21 #25 #26 #29 #30 #35 #37 #38 #45 #47 #48 #52 #54 #60 #69..71 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. #a__isNatKind(x1) weight: (/ 1 16) isNatKind(x1) weight: 0 a__plus(x1,x2) weight: max{(/ 3 16) + x2, x1} U21(x1,x2) weight: max{0, x1} #a__U71(x1,x2,x3) weight: max{0, (/ 1 4) + x3, (/ 1 16) + x1} U11(x1,x2,x3) weight: max{0, x1} s(x1) weight: x1 #a__U31(x1,x2,x3) weight: 0 #a__U33(x1) weight: 0 a__U33(x1) weight: 0 #a__isNat(x1) weight: (/ 1 16) U71(x1,x2,x3) weight: max{0, (/ 1 4) + x3, (/ 3 16) + x1} and(x1,x2) weight: max{x2, x1} #a__U13(x1) weight: 0 #a__U51(x1,x2,x3) weight: max{x3, (/ 1 8) + x2, x1} #a__x(x1,x2) weight: max{0, (/ 1 4) + x1} a__U22(x1) weight: x1 #a__U11(x1,x2,x3) weight: 0 a__U31(x1,x2,x3) weight: 0 a__U51(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} a__x(x1,x2) weight: max{0, (/ 1 4) + x1} U12(x1,x2) weight: max{0, x1} a__U41(x1,x2) weight: max{x2, (/ 1 16) + x1} x(x1,x2) weight: max{0, (/ 1 4) + x1} #a__U12(x1,x2) weight: 0 #a__U21(x1,x2) weight: 0 #a__U61(x1) weight: 0 #a__plus(x1,x2) weight: max{(/ 1 8) + x2, x1} #mark(x1) weight: x1 0() weight: (/ 1 16) #a__and(x1,x2) weight: max{0, x2} a__U21(x1,x2) weight: max{0, x1} a__U32(x1,x2) weight: 0 mark(x1) weight: x1 a__U11(x1,x2,x3) weight: max{0, x1} U32(x1,x2) weight: 0 U33(x1) weight: 0 a__U12(x1,x2) weight: max{0, x1} isNat(x1) weight: 0 plus(x1,x2) weight: max{(/ 3 16) + x2, x1} U61(x1) weight: (/ 1 16) #a__U22(x1) weight: 0 a__U13(x1) weight: 0 U31(x1,x2,x3) weight: 0 a__U71(x1,x2,x3) weight: max{0, (/ 1 4) + x3, (/ 3 16) + x1} a__U61(x1) weight: (/ 1 16) #a__U41(x1,x2) weight: max{0, x2} tt() weight: 0 a__isNat(x1) weight: 0 U13(x1) weight: 0 a__isNatKind(x1) weight: 0 U22(x1) weight: x1 U51(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} a__and(x1,x2) weight: max{x2, x1} U41(x1,x2) weight: max{x2, (/ 1 16) + x1} #a__U32(x1,x2) weight: 0 Usable rules: { 1..62 } Removed DPs: #26 Number of SCCs: 1, DPs: 23, edges: 173 SCC { #5 #8..11 #17 #20 #21 #25 #29 #30 #35 #37 #38 #45 #47 #48 #52 #54 #60 #69..71 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. #a__isNatKind(x1) weight: (/ 1 4) isNatKind(x1) weight: (/ 18265 2) a__plus(x1,x2) weight: max{(/ 36533 4) + x2, x1} U21(x1,x2) weight: max{0, (/ 1 2) + x1} #a__U71(x1,x2,x3) weight: max{0, (/ 36533 2) + x3, (/ 73065 4) + x2} U11(x1,x2,x3) weight: max{0, (/ 1 2) + x1} s(x1) weight: x1 #a__U31(x1,x2,x3) weight: 0 #a__U33(x1) weight: 0 a__U33(x1) weight: (/ 18265 2) #a__isNat(x1) weight: (/ 1 4) U71(x1,x2,x3) weight: max{(/ 36533 4) + x3, 9133 + x2, (/ 1 4) + x1} and(x1,x2) weight: max{x2, x1} #a__U13(x1) weight: 0 #a__U51(x1,x2,x3) weight: max{0, (/ 36533 4) + x3} #a__x(x1,x2) weight: max{(/ 73065 4) + x2, (/ 36533 2) + x1} a__U22(x1) weight: x1 #a__U11(x1,x2,x3) weight: 0 a__U31(x1,x2,x3) weight: max{0, (/ 1 2) + x1} a__U51(x1,x2,x3) weight: max{x3, (/ 36533 4) + x2, (/ 1 4) + x1} a__x(x1,x2) weight: max{9133 + x2, (/ 36533 4) + x1} U12(x1,x2) weight: max{0, x1} a__U41(x1,x2) weight: max{x2, (/ 1 4) + x1} x(x1,x2) weight: max{9133 + x2, (/ 36533 4) + x1} #a__U12(x1,x2) weight: 0 #a__U21(x1,x2) weight: 0 #a__U61(x1) weight: 0 #a__plus(x1,x2) weight: max{0, (/ 36533 4) + x1} #mark(x1) weight: (/ 36533 4) + x1 0() weight: (/ 1 4) #a__and(x1,x2) weight: max{(/ 36533 4) + x2, 9133 + x1} a__U21(x1,x2) weight: max{0, (/ 1 2) + x1} a__U32(x1,x2) weight: max{0, x1} mark(x1) weight: x1 a__U11(x1,x2,x3) weight: max{0, (/ 1 2) + x1} U32(x1,x2) weight: max{0, x1} U33(x1) weight: (/ 18265 2) a__U12(x1,x2) weight: max{0, x1} isNat(x1) weight: 9133 plus(x1,x2) weight: max{(/ 36533 4) + x2, x1} U61(x1) weight: (/ 1 4) + x1 #a__U22(x1) weight: 0 a__U13(x1) weight: (/ 18265 2) U31(x1,x2,x3) weight: max{0, (/ 1 2) + x1} a__U71(x1,x2,x3) weight: max{(/ 36533 4) + x3, 9133 + x2, (/ 1 4) + x1} a__U61(x1) weight: (/ 1 4) + x1 #a__U41(x1,x2) weight: max{(/ 36533 4) + x2, (/ 1 4) + x1} tt() weight: (/ 18265 2) a__isNat(x1) weight: 9133 U13(x1) weight: (/ 18265 2) a__isNatKind(x1) weight: (/ 18265 2) U22(x1) weight: x1 U51(x1,x2,x3) weight: max{x3, (/ 36533 4) + x2, (/ 1 4) + x1} a__and(x1,x2) weight: max{x2, x1} U41(x1,x2) weight: max{x2, (/ 1 4) + x1} #a__U32(x1,x2) weight: 0 Usable rules: { 1..62 } Removed DPs: #37 #69 #71 Number of SCCs: 1, DPs: 20, edges: 107 SCC { #5 #8..11 #17 #20 #21 #25 #29 #30 #35 #38 #45 #47 #48 #52 #54 #60 #70 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. #a__isNatKind(x1) weight: (/ 1 4) isNatKind(x1) weight: x1 a__plus(x1,x2) weight: max{(/ 51287 2) + x2, x1} U21(x1,x2) weight: max{(/ 1 4) + x2, (/ 1 4) + x1} #a__U71(x1,x2,x3) weight: max{0, (/ 102575 4) + x3, (/ 51287 2) + x2} U11(x1,x2,x3) weight: max{0, (/ 1 4) + x2} s(x1) weight: x1 #a__U31(x1,x2,x3) weight: 0 #a__U33(x1) weight: 0 a__U33(x1) weight: 0 #a__isNat(x1) weight: (/ 1 4) U71(x1,x2,x3) weight: max{0, (/ 102575 4) + x3, (/ 51287 2) + x2} and(x1,x2) weight: max{(/ 51287 2) + x2, x1} #a__U13(x1) weight: 0 #a__U51(x1,x2,x3) weight: max{0, x3} #a__x(x1,x2) weight: max{(/ 51287 2) + x2, (/ 102575 4) + x1} a__U22(x1) weight: x1 #a__U11(x1,x2,x3) weight: 0 a__U31(x1,x2,x3) weight: 0 a__U51(x1,x2,x3) weight: max{0, x3, (/ 51287 2) + x2} a__x(x1,x2) weight: max{(/ 51287 2) + x2, (/ 102575 4) + x1} U12(x1,x2) weight: max{0, x1} a__U41(x1,x2) weight: max{0, x2} x(x1,x2) weight: max{(/ 51287 2) + x2, (/ 102575 4) + x1} #a__U12(x1,x2) weight: 0 #a__U21(x1,x2) weight: 0 #a__U61(x1) weight: 0 #a__plus(x1,x2) weight: max{0, x1} #mark(x1) weight: x1 0() weight: 0 #a__and(x1,x2) weight: max{0, (/ 102573 4) + x2} a__U21(x1,x2) weight: max{(/ 1 4) + x2, (/ 1 4) + x1} a__U32(x1,x2) weight: 0 mark(x1) weight: x1 a__U11(x1,x2,x3) weight: max{0, (/ 1 4) + x2} U32(x1,x2) weight: 0 U33(x1) weight: 0 a__U12(x1,x2) weight: max{0, x1} isNat(x1) weight: (/ 1 4) + x1 plus(x1,x2) weight: max{(/ 51287 2) + x2, x1} U61(x1) weight: 0 #a__U22(x1) weight: 0 a__U13(x1) weight: 0 U31(x1,x2,x3) weight: 0 a__U71(x1,x2,x3) weight: max{0, (/ 102575 4) + x3, (/ 51287 2) + x2} a__U61(x1) weight: 0 #a__U41(x1,x2) weight: max{0, x2} tt() weight: 0 a__isNat(x1) weight: (/ 1 4) + x1 U13(x1) weight: 0 a__isNatKind(x1) weight: x1 U22(x1) weight: x1 U51(x1,x2,x3) weight: max{0, x3, (/ 51287 2) + x2} a__and(x1,x2) weight: max{(/ 51287 2) + x2, x1} U41(x1,x2) weight: max{0, x2} #a__U32(x1,x2) weight: 0 Usable rules: { 1..62 } Removed DPs: #8 #20 Number of SCCs: 1, DPs: 18, edges: 88 SCC { #5 #9..11 #17 #21 #25 #29 #30 #35 #38 #45 #47 #48 #52 #54 #60 #70 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded. #a__isNatKind(x1) status: [] precedence above: isNatKind(x1) status: x1 a__plus(x1,x2) status: [x1,x2] precedence above: isNatKind U21 U11 s and #a__U51 a__U22 a__U51 U12 a__U41 #a__plus #mark a__U21 mark a__U11 a__U12 isNat plus a__U13 #a__U41 tt a__isNat U13 U22 U51 a__and U41 U21(x1,x2) status: [x2,x1] precedence above: U11 a__U22 U12 a__U21 a__U11 a__U12 isNat a__U13 tt a__isNat U13 U22 #a__U71(x1,x2,x3) status: [x3,x2,x1] precedence above: isNatKind a__plus U21 U11 s a__U33 U71 and #a__U51 #a__x a__U22 a__U31 a__U51 a__x U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 a__U71 #a__U41 tt a__isNat U13 U22 U51 a__and U41 U11(x1,x2,x3) status: [x2,x3] precedence above: U12 a__U11 a__U12 isNat a__U13 tt a__isNat U13 s(x1) status: [x1] precedence above: U21 U11 a__U22 U12 a__U21 a__U11 a__U12 isNat a__U13 tt a__isNat U13 U22 #a__U31(x1,x2,x3) status: [x2,x3,x1] precedence above: #a__U33(x1) status: [] precedence above: a__U33(x1) status: [x1] precedence above: U33 #a__isNat(x1) status: [] precedence above: U71(x1,x2,x3) status: [x3,x2,x1] precedence above: isNatKind a__plus U21 #a__U71 U11 s a__U33 and #a__U51 #a__x a__U22 a__U31 a__U51 a__x U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 a__U71 #a__U41 tt a__isNat U13 U22 U51 a__and U41 and(x1,x2) status: [x1,x2] precedence above: a__and #a__U13(x1) status: [] precedence above: #a__U51(x1,x2,x3) status: [x2,x3] precedence above: isNatKind U11 and U12 #a__plus #mark mark a__U11 a__U12 isNat a__U13 #a__U41 tt a__isNat U13 a__and #a__x(x1,x2) status: [x1,x2] precedence above: isNatKind a__plus U21 #a__U71 U11 s a__U33 U71 and #a__U51 a__U22 a__U31 a__U51 a__x U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 a__U71 #a__U41 tt a__isNat U13 U22 U51 a__and U41 a__U22(x1) status: [x1] precedence above: U22 #a__U11(x1,x2,x3) status: [x3,x2,x1] precedence above: a__U31(x1,x2,x3) status: [x3,x2] precedence above: U11 a__U33 U12 a__U32 a__U11 U32 U33 a__U12 isNat a__U13 U31 tt a__isNat U13 a__U51(x1,x2,x3) status: [x3,x2,x1] precedence above: isNatKind a__plus U21 U11 s and #a__U51 a__U22 U12 a__U41 #a__plus #mark a__U21 mark a__U11 a__U12 isNat plus a__U13 #a__U41 tt a__isNat U13 U22 U51 a__and U41 a__x(x1,x2) status: [x1,x2] precedence above: isNatKind a__plus U21 #a__U71 U11 s a__U33 U71 and #a__U51 #a__x a__U22 a__U31 a__U51 U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 a__U71 #a__U41 tt a__isNat U13 U22 U51 a__and U41 U12(x1,x2) status: [x2,x1] precedence above: a__U12 a__U13 tt U13 a__U41(x1,x2) status: [x1,x2] precedence above: #mark mark #a__U41 U41 x(x1,x2) status: [x1,x2] precedence above: isNatKind a__plus U21 #a__U71 U11 s a__U33 U71 and #a__U51 #a__x a__U22 a__U31 a__U51 a__x U12 a__U41 #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 a__U71 #a__U41 tt a__isNat U13 U22 U51 a__and U41 #a__U12(x1,x2) status: [x2] precedence above: #a__U21(x1,x2) status: [] precedence above: #a__U61(x1) status: [] precedence above: #a__plus(x1,x2) status: [x2,x1] precedence above: isNatKind U11 and #a__U51 U12 #mark mark a__U11 a__U12 isNat a__U13 #a__U41 tt a__isNat U13 a__and #mark(x1) status: [x1] precedence above: mark 0() status: [] precedence above: isNatKind and U61 a__U61 tt a__and #a__and(x1,x2) status: [x1] precedence above: a__U21(x1,x2) status: [x2,x1] precedence above: U21 U11 a__U22 U12 a__U11 a__U12 isNat a__U13 tt a__isNat U13 U22 a__U32(x1,x2) status: [x2] precedence above: U11 a__U33 U12 a__U11 U32 U33 a__U12 isNat a__U13 tt a__isNat U13 mark(x1) status: x1 a__U11(x1,x2,x3) status: [x2,x3] precedence above: U11 U12 a__U12 isNat a__U13 tt a__isNat U13 U32(x1,x2) status: [x2] precedence above: U11 a__U33 U12 a__U32 a__U11 U33 a__U12 isNat a__U13 tt a__isNat U13 U33(x1) status: [x1] precedence above: a__U33 a__U12(x1,x2) status: [x2,x1] precedence above: U12 a__U13 tt U13 isNat(x1) status: [x1] precedence above: U11 U12 a__U11 a__U12 a__U13 tt a__isNat U13 plus(x1,x2) status: [x1,x2] precedence above: isNatKind a__plus U21 U11 s and #a__U51 a__U22 a__U51 U12 a__U41 #a__plus #mark a__U21 mark a__U11 a__U12 isNat a__U13 #a__U41 tt a__isNat U13 U22 U51 a__and U41 U61(x1) status: [] precedence above: isNatKind and 0 a__U61 tt a__and #a__U22(x1) status: [] precedence above: a__U13(x1) status: [] precedence above: tt U13 U31(x1,x2,x3) status: [x3,x2] precedence above: U11 a__U33 a__U31 U12 a__U32 a__U11 U32 U33 a__U12 isNat a__U13 tt a__isNat U13 a__U71(x1,x2,x3) status: [x3,x2,x1] precedence above: isNatKind a__plus U21 #a__U71 U11 s a__U33 U71 and #a__U51 #a__x a__U22 a__U31 a__U51 a__x U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 #a__U41 tt a__isNat U13 U22 U51 a__and U41 a__U61(x1) status: [] precedence above: isNatKind and 0 U61 tt a__and #a__U41(x1,x2) status: [x1,x2] precedence above: #mark mark tt() status: [] precedence above: a__isNat(x1) status: [x1] precedence above: U11 U12 a__U11 a__U12 isNat a__U13 tt U13 U13(x1) status: [] precedence above: a__U13 tt a__isNatKind(x1) status: x1 U22(x1) status: [x1] precedence above: a__U22 U51(x1,x2,x3) status: [x3,x2,x1] precedence above: isNatKind a__plus U21 U11 s and #a__U51 a__U22 a__U51 U12 a__U41 #a__plus #mark a__U21 mark a__U11 a__U12 isNat plus a__U13 #a__U41 tt a__isNat U13 U22 a__and U41 a__and(x1,x2) status: [x1,x2] precedence above: and U41(x1,x2) status: [x1,x2] precedence above: a__U41 #mark mark #a__U41 #a__U32(x1,x2) status: [x1] precedence above: Usable rules: { 1..62 } Removed DPs: #5 #9..11 #17 #21 #29 #30 #35 #38 #45 #48 #52 #54 #60 #70 Number of SCCs: 1, DPs: 2, edges: 2 SCC { #25 #47 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded. #a__isNatKind(x1) status: [] precedence above: isNatKind(x1) status: x1 a__plus(x1,x2) status: [x1,x2] precedence above: isNatKind U21 U11 s and #a__U51 a__U22 a__U51 U12 a__U41 #a__plus #mark a__U21 mark a__U11 a__U12 isNat plus a__U13 #a__U41 tt a__isNat U13 U22 U51 a__and U41 U21(x1,x2) status: [x2,x1] precedence above: U11 a__U22 U12 a__U21 a__U11 a__U12 isNat a__U13 tt a__isNat U13 U22 #a__U71(x1,x2,x3) status: [x3,x2,x1] precedence above: isNatKind a__plus U21 U11 s a__U33 U71 and #a__U51 #a__x a__U22 a__U31 a__U51 a__x U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 a__U71 #a__U41 tt a__isNat U13 U22 U51 a__and U41 U11(x1,x2,x3) status: [x2,x3] precedence above: U12 a__U11 a__U12 isNat a__U13 tt a__isNat U13 s(x1) status: [x1] precedence above: U21 U11 a__U22 U12 a__U21 a__U11 a__U12 isNat a__U13 tt a__isNat U13 U22 #a__U31(x1,x2,x3) status: [x2,x3,x1] precedence above: #a__U33(x1) status: [] precedence above: a__U33(x1) status: [x1] precedence above: U33 #a__isNat(x1) status: [] precedence above: U71(x1,x2,x3) status: [x3,x2,x1] precedence above: isNatKind a__plus U21 #a__U71 U11 s a__U33 and #a__U51 #a__x a__U22 a__U31 a__U51 a__x U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 a__U71 #a__U41 tt a__isNat U13 U22 U51 a__and U41 and(x1,x2) status: [x1,x2] precedence above: a__and #a__U13(x1) status: [] precedence above: #a__U51(x1,x2,x3) status: [x2,x3,x1] precedence above: isNatKind U11 and U12 #a__plus #mark mark a__U11 a__U12 isNat a__U13 #a__U41 tt a__isNat U13 a__and #a__x(x1,x2) status: [x1,x2] precedence above: isNatKind a__plus U21 #a__U71 U11 s a__U33 U71 and #a__U51 a__U22 a__U31 a__U51 a__x U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 a__U71 #a__U41 tt a__isNat U13 U22 U51 a__and U41 a__U22(x1) status: [x1] precedence above: U22 #a__U11(x1,x2,x3) status: [x3,x2,x1] precedence above: a__U31(x1,x2,x3) status: [x3,x2] precedence above: U11 a__U33 U12 a__U32 a__U11 U32 U33 a__U12 isNat a__U13 U31 tt a__isNat U13 a__U51(x1,x2,x3) status: [x3,x2,x1] precedence above: isNatKind a__plus U21 U11 s and #a__U51 a__U22 U12 a__U41 #a__plus #mark a__U21 mark a__U11 a__U12 isNat plus a__U13 #a__U41 tt a__isNat U13 U22 U51 a__and U41 a__x(x1,x2) status: [x1,x2] precedence above: isNatKind a__plus U21 #a__U71 U11 s a__U33 U71 and #a__U51 #a__x a__U22 a__U31 a__U51 U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 a__U71 #a__U41 tt a__isNat U13 U22 U51 a__and U41 U12(x1,x2) status: [x2,x1] precedence above: a__U12 a__U13 tt U13 a__U41(x1,x2) status: [x1,x2] precedence above: #mark mark #a__U41 U41 x(x1,x2) status: [x1,x2] precedence above: isNatKind a__plus U21 #a__U71 U11 s a__U33 U71 and #a__U51 #a__x a__U22 a__U31 a__U51 a__x U12 a__U41 #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 a__U71 #a__U41 tt a__isNat U13 U22 U51 a__and U41 #a__U12(x1,x2) status: [x2] precedence above: #a__U21(x1,x2) status: [] precedence above: #a__U61(x1) status: [] precedence above: #a__plus(x1,x2) status: [x2,x1] precedence above: isNatKind U11 and #a__U51 U12 #mark mark a__U11 a__U12 isNat a__U13 #a__U41 tt a__isNat U13 a__and #mark(x1) status: [x1] precedence above: mark 0() status: [] precedence above: isNatKind and U61 a__U61 tt a__and #a__and(x1,x2) status: [x1] precedence above: a__U21(x1,x2) status: [x2,x1] precedence above: U21 U11 a__U22 U12 a__U11 a__U12 isNat a__U13 tt a__isNat U13 U22 a__U32(x1,x2) status: [x2] precedence above: U11 a__U33 U12 a__U11 U32 U33 a__U12 isNat a__U13 tt a__isNat U13 mark(x1) status: x1 a__U11(x1,x2,x3) status: [x2,x3] precedence above: U11 U12 a__U12 isNat a__U13 tt a__isNat U13 U32(x1,x2) status: [x2] precedence above: U11 a__U33 U12 a__U32 a__U11 U33 a__U12 isNat a__U13 tt a__isNat U13 U33(x1) status: [x1] precedence above: a__U33 a__U12(x1,x2) status: [x2,x1] precedence above: U12 a__U13 tt U13 isNat(x1) status: [x1] precedence above: U11 U12 a__U11 a__U12 a__U13 tt a__isNat U13 plus(x1,x2) status: [x1,x2] precedence above: isNatKind a__plus U21 U11 s and #a__U51 a__U22 a__U51 U12 a__U41 #a__plus #mark a__U21 mark a__U11 a__U12 isNat a__U13 #a__U41 tt a__isNat U13 U22 U51 a__and U41 U61(x1) status: [] precedence above: isNatKind and 0 a__U61 tt a__and #a__U22(x1) status: [] precedence above: a__U13(x1) status: [] precedence above: tt U13 U31(x1,x2,x3) status: [x3,x2] precedence above: U11 a__U33 a__U31 U12 a__U32 a__U11 U32 U33 a__U12 isNat a__U13 tt a__isNat U13 a__U71(x1,x2,x3) status: [x3,x2,x1] precedence above: isNatKind a__plus U21 #a__U71 U11 s a__U33 U71 and #a__U51 #a__x a__U22 a__U31 a__U51 a__x U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 #a__U41 tt a__isNat U13 U22 U51 a__and U41 a__U61(x1) status: [] precedence above: isNatKind and 0 U61 tt a__and #a__U41(x1,x2) status: [x1,x2] precedence above: #mark mark tt() status: [] precedence above: a__isNat(x1) status: [x1] precedence above: U11 U12 a__U11 a__U12 isNat a__U13 tt U13 U13(x1) status: [] precedence above: a__U13 tt a__isNatKind(x1) status: x1 U22(x1) status: [x1] precedence above: a__U22 U51(x1,x2,x3) status: [x3,x2,x1] precedence above: isNatKind a__plus U21 U11 s and #a__U51 a__U22 a__U51 U12 a__U41 #a__plus #mark a__U21 mark a__U11 a__U12 isNat plus a__U13 #a__U41 tt a__isNat U13 U22 a__and U41 a__and(x1,x2) status: [x1,x2] precedence above: and U41(x1,x2) status: [x1,x2] precedence above: a__U41 #mark mark #a__U41 #a__U32(x1,x2) status: [x1] precedence above: Usable rules: { 1..62 } Removed DPs: #25 #47 Number of SCCs: 0, DPs: 0, edges: 0 YES