Input TRS: 1: p(s(N)) -> N 2: +(N,0()) -> N 3: +(s(N),s(M)) -> s(s(+(N,M))) 4: *(N,0()) -> 0() 5: *(s(N),s(M)) -> s(+(N,+(M,*(N,M)))) 6: gt(0(),M) -> False() 7: gt(NzN,0()) -> u_4(is_NzNat(NzN)) 8: u_4(True()) -> True() 9: is_NzNat(0()) -> False() 10: is_NzNat(s(N)) -> True() 11: gt(s(N),s(M)) -> gt(N,M) 12: lt(N,M) -> gt(M,N) 13: d(0(),N) -> N 14: d(s(N),s(M)) -> d(N,M) 15: quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM) 16: u_11(True(),N,NzM) -> u_1(gt(N,NzM),N,NzM) 17: u_1(True(),N,NzM) -> s(quot(d(N,NzM),NzM)) 18: quot(NzM,NzM) -> u_01(is_NzNat(NzM)) 19: u_01(True()) -> s(0()) 20: quot(N,NzM) -> u_21(is_NzNat(NzM),NzM,N) 21: u_21(True(),NzM,N) -> u_2(gt(NzM,N)) 22: u_2(True()) -> 0() 23: gcd(0(),N) -> 0() 24: gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM) 25: u_02(True(),NzM) -> NzM 26: gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM) 27: u_31(True(),True(),NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM) 28: u_3(True(),NzN,NzM) -> gcd(d(NzN,NzM),NzM) Number of strict rules: 28 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #gt(s(N),s(M)) -> #gt(N,M) #2: #gcd(NzM,NzM) -> #u_02(is_NzNat(NzM),NzM) #3: #gcd(NzM,NzM) -> #is_NzNat(NzM) #4: #lt(N,M) -> #gt(M,N) #5: #d(s(N),s(M)) -> #d(N,M) #6: #quot(N,NzM) -> #u_21(is_NzNat(NzM),NzM,N) #7: #quot(N,NzM) -> #is_NzNat(NzM) #8: #gt(NzN,0()) -> #u_4(is_NzNat(NzN)) #9: #gt(NzN,0()) -> #is_NzNat(NzN) #10: #*(s(N),s(M)) -> #+(N,+(M,*(N,M))) #11: #*(s(N),s(M)) -> #+(M,*(N,M)) #12: #*(s(N),s(M)) -> #*(N,M) #13: #u_3(True(),NzN,NzM) -> #gcd(d(NzN,NzM),NzM) #14: #u_3(True(),NzN,NzM) -> #d(NzN,NzM) #15: #u_31(True(),True(),NzN,NzM) -> #u_3(gt(NzN,NzM),NzN,NzM) #16: #u_31(True(),True(),NzN,NzM) -> #gt(NzN,NzM) #17: #u_1(True(),N,NzM) -> #quot(d(N,NzM),NzM) #18: #u_1(True(),N,NzM) -> #d(N,NzM) #19: #gcd(NzN,NzM) -> #u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM) #20: #gcd(NzN,NzM) -> #is_NzNat(NzN) #21: #gcd(NzN,NzM) -> #is_NzNat(NzM) #22: #u_21(True(),NzM,N) -> #u_2(gt(NzM,N)) #23: #u_21(True(),NzM,N) -> #gt(NzM,N) #24: #u_11(True(),N,NzM) -> #u_1(gt(N,NzM),N,NzM) #25: #u_11(True(),N,NzM) -> #gt(N,NzM) #26: #+(s(N),s(M)) -> #+(N,M) #27: #quot(N,NzM) -> #u_11(is_NzNat(NzM),N,NzM) #28: #quot(N,NzM) -> #is_NzNat(NzM) #29: #quot(NzM,NzM) -> #u_01(is_NzNat(NzM)) #30: #quot(NzM,NzM) -> #is_NzNat(NzM) Number of SCCs: 6, DPs: 10, edges: 10 SCC { #26 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #u_3(x1,x2,x3) weight: 0 u_11(x1,x2,x3) weight: 0 d(x1,x2) weight: 0 is_NzNat(x1) weight: 0 s(x1) weight: (/ 1 2) + x1 #lt(x1,x2) weight: 0 u_3(x1,x2,x3) weight: 0 #u_01(x1) weight: 0 u_21(x1,x2,x3) weight: 0 gt(x1,x2) weight: 0 u_2(x1) weight: 0 gcd(x1,x2) weight: 0 #u_21(x1,x2,x3) weight: 0 False() weight: 0 #*(x1,x2) weight: 0 #p(x1) weight: 0 True() weight: 0 #is_NzNat(x1) weight: 0 p(x1) weight: 0 0() weight: 0 quot(x1,x2) weight: 0 #u_2(x1) weight: 0 u_4(x1) weight: 0 #d(x1,x2) weight: 0 #gt(x1,x2) weight: 0 #u_4(x1) weight: 0 u_31(x1,x2,x3,x4) weight: 0 u_02(x1,x2) weight: 0 #u_11(x1,x2,x3) weight: 0 #u_31(x1,x2,x3,x4) weight: 0 u_1(x1,x2,x3) weight: 0 #quot(x1,x2) weight: 0 #u_02(x1,x2) weight: 0 u_01(x1) weight: 0 +(x1,x2) weight: 0 #u_1(x1,x2,x3) weight: 0 lt(x1,x2) weight: 0 #+(x1,x2) weight: x2 *(x1,x2) weight: 0 #gcd(x1,x2) weight: 0 Usable rules: { } Removed DPs: #26 Number of SCCs: 5, DPs: 9, edges: 9 SCC { #5 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #u_3(x1,x2,x3) weight: 0 u_11(x1,x2,x3) weight: 0 d(x1,x2) weight: 0 is_NzNat(x1) weight: 0 s(x1) weight: (/ 1 2) + x1 #lt(x1,x2) weight: 0 u_3(x1,x2,x3) weight: 0 #u_01(x1) weight: 0 u_21(x1,x2,x3) weight: 0 gt(x1,x2) weight: 0 u_2(x1) weight: 0 gcd(x1,x2) weight: 0 #u_21(x1,x2,x3) weight: 0 False() weight: 0 #*(x1,x2) weight: 0 #p(x1) weight: 0 True() weight: 0 #is_NzNat(x1) weight: 0 p(x1) weight: 0 0() weight: 0 quot(x1,x2) weight: 0 #u_2(x1) weight: 0 u_4(x1) weight: 0 #d(x1,x2) weight: x2 #gt(x1,x2) weight: 0 #u_4(x1) weight: 0 u_31(x1,x2,x3,x4) weight: 0 u_02(x1,x2) weight: 0 #u_11(x1,x2,x3) weight: 0 #u_31(x1,x2,x3,x4) weight: 0 u_1(x1,x2,x3) weight: 0 #quot(x1,x2) weight: 0 #u_02(x1,x2) weight: 0 u_01(x1) weight: 0 +(x1,x2) weight: 0 #u_1(x1,x2,x3) weight: 0 lt(x1,x2) weight: 0 #+(x1,x2) weight: 0 *(x1,x2) weight: 0 #gcd(x1,x2) weight: 0 Usable rules: { } Removed DPs: #5 Number of SCCs: 4, DPs: 8, edges: 8 SCC { #1 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #u_3(x1,x2,x3) weight: 0 u_11(x1,x2,x3) weight: 0 d(x1,x2) weight: 0 is_NzNat(x1) weight: 0 s(x1) weight: (/ 1 2) + x1 #lt(x1,x2) weight: 0 u_3(x1,x2,x3) weight: 0 #u_01(x1) weight: 0 u_21(x1,x2,x3) weight: 0 gt(x1,x2) weight: 0 u_2(x1) weight: 0 gcd(x1,x2) weight: 0 #u_21(x1,x2,x3) weight: 0 False() weight: 0 #*(x1,x2) weight: 0 #p(x1) weight: 0 True() weight: 0 #is_NzNat(x1) weight: 0 p(x1) weight: 0 0() weight: 0 quot(x1,x2) weight: 0 #u_2(x1) weight: 0 u_4(x1) weight: 0 #d(x1,x2) weight: 0 #gt(x1,x2) weight: x1 #u_4(x1) weight: 0 u_31(x1,x2,x3,x4) weight: 0 u_02(x1,x2) weight: 0 #u_11(x1,x2,x3) weight: 0 #u_31(x1,x2,x3,x4) weight: 0 u_1(x1,x2,x3) weight: 0 #quot(x1,x2) weight: 0 #u_02(x1,x2) weight: 0 u_01(x1) weight: 0 +(x1,x2) weight: 0 #u_1(x1,x2,x3) weight: 0 lt(x1,x2) weight: 0 #+(x1,x2) weight: 0 *(x1,x2) weight: 0 #gcd(x1,x2) weight: 0 Usable rules: { } Removed DPs: #1 Number of SCCs: 3, DPs: 7, edges: 7 SCC { #12 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #u_3(x1,x2,x3) weight: 0 u_11(x1,x2,x3) weight: 0 d(x1,x2) weight: 0 is_NzNat(x1) weight: 0 s(x1) weight: (/ 1 2) + x1 #lt(x1,x2) weight: 0 u_3(x1,x2,x3) weight: 0 #u_01(x1) weight: 0 u_21(x1,x2,x3) weight: 0 gt(x1,x2) weight: 0 u_2(x1) weight: 0 gcd(x1,x2) weight: 0 #u_21(x1,x2,x3) weight: 0 False() weight: 0 #*(x1,x2) weight: x2 #p(x1) weight: 0 True() weight: 0 #is_NzNat(x1) weight: 0 p(x1) weight: 0 0() weight: 0 quot(x1,x2) weight: 0 #u_2(x1) weight: 0 u_4(x1) weight: 0 #d(x1,x2) weight: 0 #gt(x1,x2) weight: 0 #u_4(x1) weight: 0 u_31(x1,x2,x3,x4) weight: 0 u_02(x1,x2) weight: 0 #u_11(x1,x2,x3) weight: 0 #u_31(x1,x2,x3,x4) weight: 0 u_1(x1,x2,x3) weight: 0 #quot(x1,x2) weight: 0 #u_02(x1,x2) weight: 0 u_01(x1) weight: 0 +(x1,x2) weight: 0 #u_1(x1,x2,x3) weight: 0 lt(x1,x2) weight: 0 #+(x1,x2) weight: 0 *(x1,x2) weight: 0 #gcd(x1,x2) weight: 0 Usable rules: { } Removed DPs: #12 Number of SCCs: 2, DPs: 6, edges: 6 SCC { #17 #24 #27 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed. Removing edges: failed. Finding a loop... failed. MAYBE