Input TRS: 1: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) 2: active(add(0(),X)) -> mark(X) 3: active(add(s(X),Y)) -> mark(s(add(X,Y))) 4: active(prod(0(),X)) -> mark(0()) 5: active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) 6: active(if(true(),X,Y)) -> mark(X) 7: active(if(false(),X,Y)) -> mark(Y) 8: active(zero(0())) -> mark(true()) 9: active(zero(s(X))) -> mark(false()) 10: active(p(s(X))) -> mark(X) 11: mark(fact(X)) -> active(fact(mark(X))) 12: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3)) 13: mark(zero(X)) -> active(zero(mark(X))) 14: mark(s(X)) -> active(s(mark(X))) 15: mark(0()) -> active(0()) 16: mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2))) 17: mark(p(X)) -> active(p(mark(X))) 18: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2))) 19: mark(true()) -> active(true()) 20: mark(false()) -> active(false()) 21: fact(mark(X)) -> fact(X) 22: fact(active(X)) -> fact(X) 23: if(mark(X1),X2,X3) -> if(X1,X2,X3) 24: if(X1,mark(X2),X3) -> if(X1,X2,X3) 25: if(X1,X2,mark(X3)) -> if(X1,X2,X3) 26: if(active(X1),X2,X3) -> if(X1,X2,X3) 27: if(X1,active(X2),X3) -> if(X1,X2,X3) 28: if(X1,X2,active(X3)) -> if(X1,X2,X3) 29: zero(mark(X)) -> zero(X) 30: zero(active(X)) -> zero(X) 31: s(mark(X)) -> s(X) 32: s(active(X)) -> s(X) 33: prod(mark(X1),X2) -> prod(X1,X2) 34: prod(X1,mark(X2)) -> prod(X1,X2) 35: prod(active(X1),X2) -> prod(X1,X2) 36: prod(X1,active(X2)) -> prod(X1,X2) 37: p(mark(X)) -> p(X) 38: p(active(X)) -> p(X) 39: add(mark(X1),X2) -> add(X1,X2) 40: add(X1,mark(X2)) -> add(X1,X2) 41: add(active(X1),X2) -> add(X1,X2) 42: add(X1,active(X2)) -> add(X1,X2) Number of strict rules: 42 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #active(add(0(),X)) -> #mark(X) #2: #zero(mark(X)) -> #zero(X) #3: #prod(active(X1),X2) -> #prod(X1,X2) #4: #add(X1,active(X2)) -> #add(X1,X2) #5: #add(active(X1),X2) -> #add(X1,X2) #6: #p(mark(X)) -> #p(X) #7: #p(active(X)) -> #p(X) #8: #active(if(true(),X,Y)) -> #mark(X) #9: #add(X1,mark(X2)) -> #add(X1,X2) #10: #mark(zero(X)) -> #active(zero(mark(X))) #11: #mark(zero(X)) -> #zero(mark(X)) #12: #mark(zero(X)) -> #mark(X) #13: #active(zero(s(X))) -> #mark(false()) #14: #mark(fact(X)) -> #active(fact(mark(X))) #15: #mark(fact(X)) -> #fact(mark(X)) #16: #mark(fact(X)) -> #mark(X) #17: #if(X1,mark(X2),X3) -> #if(X1,X2,X3) #18: #if(mark(X1),X2,X3) -> #if(X1,X2,X3) #19: #mark(if(X1,X2,X3)) -> #active(if(mark(X1),X2,X3)) #20: #mark(if(X1,X2,X3)) -> #if(mark(X1),X2,X3) #21: #mark(if(X1,X2,X3)) -> #mark(X1) #22: #s(mark(X)) -> #s(X) #23: #mark(s(X)) -> #active(s(mark(X))) #24: #mark(s(X)) -> #s(mark(X)) #25: #mark(s(X)) -> #mark(X) #26: #zero(active(X)) -> #zero(X) #27: #if(X1,X2,mark(X3)) -> #if(X1,X2,X3) #28: #mark(false()) -> #active(false()) #29: #active(if(false(),X,Y)) -> #mark(Y) #30: #add(mark(X1),X2) -> #add(X1,X2) #31: #active(p(s(X))) -> #mark(X) #32: #prod(mark(X1),X2) -> #prod(X1,X2) #33: #active(prod(s(X),Y)) -> #mark(add(Y,prod(X,Y))) #34: #active(prod(s(X),Y)) -> #add(Y,prod(X,Y)) #35: #active(prod(s(X),Y)) -> #prod(X,Y) #36: #if(X1,X2,active(X3)) -> #if(X1,X2,X3) #37: #fact(active(X)) -> #fact(X) #38: #prod(X1,mark(X2)) -> #prod(X1,X2) #39: #if(X1,active(X2),X3) -> #if(X1,X2,X3) #40: #mark(p(X)) -> #active(p(mark(X))) #41: #mark(p(X)) -> #p(mark(X)) #42: #mark(p(X)) -> #mark(X) #43: #s(active(X)) -> #s(X) #44: #mark(true()) -> #active(true()) #45: #if(active(X1),X2,X3) -> #if(X1,X2,X3) #46: #prod(X1,active(X2)) -> #prod(X1,X2) #47: #fact(mark(X)) -> #fact(X) #48: #mark(prod(X1,X2)) -> #active(prod(mark(X1),mark(X2))) #49: #mark(prod(X1,X2)) -> #prod(mark(X1),mark(X2)) #50: #mark(prod(X1,X2)) -> #mark(X1) #51: #mark(prod(X1,X2)) -> #mark(X2) #52: #active(add(s(X),Y)) -> #mark(s(add(X,Y))) #53: #active(add(s(X),Y)) -> #s(add(X,Y)) #54: #active(add(s(X),Y)) -> #add(X,Y) #55: #active(fact(X)) -> #mark(if(zero(X),s(0()),prod(X,fact(p(X))))) #56: #active(fact(X)) -> #if(zero(X),s(0()),prod(X,fact(p(X)))) #57: #active(fact(X)) -> #zero(X) #58: #active(fact(X)) -> #s(0()) #59: #active(fact(X)) -> #prod(X,fact(p(X))) #60: #active(fact(X)) -> #fact(p(X)) #61: #active(fact(X)) -> #p(X) #62: #active(zero(0())) -> #mark(true()) #63: #mark(0()) -> #active(0()) #64: #active(prod(0(),X)) -> #mark(0()) #65: #mark(add(X1,X2)) -> #active(add(mark(X1),mark(X2))) #66: #mark(add(X1,X2)) -> #add(mark(X1),mark(X2)) #67: #mark(add(X1,X2)) -> #mark(X1) #68: #mark(add(X1,X2)) -> #mark(X2) Number of SCCs: 8, DPs: 43, edges: 279 SCC { #2 #26 } Removing DPs: Order(PosReal,>,Sum)... succeeded. zero(x1) weight: 0 prod(x1,x2) weight: 0 s(x1) weight: 0 #prod(x1,x2) weight: 0 false() weight: 0 #fact(x1) weight: 0 #p(x1) weight: 0 true() weight: 0 p(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #s(x1) weight: 0 fact(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 active(x1) weight: (/ 1 2) + x1 #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 #add(x1,x2) weight: 0 add(x1,x2) weight: 0 #zero(x1) weight: x1 Usable rules: { } Removed DPs: #2 #26 Number of SCCs: 7, DPs: 41, edges: 275 SCC { #22 #43 } Removing DPs: Order(PosReal,>,Sum)... succeeded. zero(x1) weight: 0 prod(x1,x2) weight: 0 s(x1) weight: 0 #prod(x1,x2) weight: 0 false() weight: 0 #fact(x1) weight: 0 #p(x1) weight: 0 true() weight: 0 p(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #s(x1) weight: x1 fact(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 active(x1) weight: (/ 1 2) + x1 #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 #add(x1,x2) weight: 0 add(x1,x2) weight: 0 #zero(x1) weight: 0 Usable rules: { } Removed DPs: #22 #43 Number of SCCs: 6, DPs: 39, edges: 271 SCC { #6 #7 } Removing DPs: Order(PosReal,>,Sum)... succeeded. zero(x1) weight: 0 prod(x1,x2) weight: 0 s(x1) weight: 0 #prod(x1,x2) weight: 0 false() weight: 0 #fact(x1) weight: 0 #p(x1) weight: x1 true() weight: 0 p(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #s(x1) weight: 0 fact(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 active(x1) weight: (/ 1 2) + x1 #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 #add(x1,x2) weight: 0 add(x1,x2) weight: 0 #zero(x1) weight: 0 Usable rules: { } Removed DPs: #6 #7 Number of SCCs: 5, DPs: 37, edges: 267 SCC { #37 #47 } Removing DPs: Order(PosReal,>,Sum)... succeeded. zero(x1) weight: 0 prod(x1,x2) weight: 0 s(x1) weight: 0 #prod(x1,x2) weight: 0 false() weight: 0 #fact(x1) weight: x1 #p(x1) weight: 0 true() weight: 0 p(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #s(x1) weight: 0 fact(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 active(x1) weight: (/ 1 2) + x1 #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 #add(x1,x2) weight: 0 add(x1,x2) weight: 0 #zero(x1) weight: 0 Usable rules: { } Removed DPs: #37 #47 Number of SCCs: 4, DPs: 35, edges: 263 SCC { #4 #5 #9 #30 } Removing DPs: Order(PosReal,>,Sum)... succeeded. zero(x1) weight: 0 prod(x1,x2) weight: 0 s(x1) weight: 0 #prod(x1,x2) weight: 0 false() weight: 0 #fact(x1) weight: 0 #p(x1) weight: 0 true() weight: 0 p(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #s(x1) weight: 0 fact(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 active(x1) weight: (/ 1 2) + x1 #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 #add(x1,x2) weight: x2 add(x1,x2) weight: 0 #zero(x1) weight: 0 Usable rules: { } Removed DPs: #4 #9 Number of SCCs: 4, DPs: 33, edges: 251 SCC { #5 #30 } Removing DPs: Order(PosReal,>,Sum)... succeeded. zero(x1) weight: 0 prod(x1,x2) weight: 0 s(x1) weight: 0 #prod(x1,x2) weight: 0 false() weight: 0 #fact(x1) weight: 0 #p(x1) weight: 0 true() weight: 0 p(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #s(x1) weight: 0 fact(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 active(x1) weight: (/ 1 2) + x1 #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 #add(x1,x2) weight: x1 add(x1,x2) weight: 0 #zero(x1) weight: 0 Usable rules: { } Removed DPs: #5 #30 Number of SCCs: 3, DPs: 31, edges: 247 SCC { #3 #32 #38 #46 } Removing DPs: Order(PosReal,>,Sum)... succeeded. zero(x1) weight: 0 prod(x1,x2) weight: 0 s(x1) weight: 0 #prod(x1,x2) weight: x1 false() weight: 0 #fact(x1) weight: 0 #p(x1) weight: 0 true() weight: 0 p(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #s(x1) weight: 0 fact(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 active(x1) weight: (/ 1 2) + x1 #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 #add(x1,x2) weight: 0 add(x1,x2) weight: 0 #zero(x1) weight: 0 Usable rules: { } Removed DPs: #3 #32 Number of SCCs: 4, DPs: 29, edges: 235 SCC { #38 #46 } Removing DPs: Order(PosReal,>,Sum)... succeeded. zero(x1) weight: 0 prod(x1,x2) weight: 0 s(x1) weight: 0 #prod(x1,x2) weight: x2 false() weight: 0 #fact(x1) weight: 0 #p(x1) weight: 0 true() weight: 0 p(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #s(x1) weight: 0 fact(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 active(x1) weight: (/ 1 2) + x1 #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 #add(x1,x2) weight: 0 add(x1,x2) weight: 0 #zero(x1) weight: 0 Usable rules: { } Removed DPs: #38 #46 Number of SCCs: 3, DPs: 27, edges: 231 SCC { #17 #18 #27 #36 #39 #45 } Removing DPs: Order(PosReal,>,Sum)... succeeded. zero(x1) weight: 0 prod(x1,x2) weight: 0 s(x1) weight: 0 #prod(x1,x2) weight: 0 false() weight: 0 #fact(x1) weight: 0 #p(x1) weight: 0 true() weight: 0 p(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #s(x1) weight: 0 fact(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 active(x1) weight: (/ 1 2) + x1 #if(x1,x2,x3) weight: x1 + x3 #active(x1) weight: 0 #add(x1,x2) weight: 0 add(x1,x2) weight: 0 #zero(x1) weight: 0 Usable rules: { } Removed DPs: #18 #27 #36 #45 Number of SCCs: 4, DPs: 23, edges: 199 SCC { #17 #39 } Removing DPs: Order(PosReal,>,Sum)... succeeded. zero(x1) weight: 0 prod(x1,x2) weight: 0 s(x1) weight: 0 #prod(x1,x2) weight: 0 false() weight: 0 #fact(x1) weight: 0 #p(x1) weight: 0 true() weight: 0 p(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #s(x1) weight: 0 fact(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 active(x1) weight: (/ 1 2) + x1 #if(x1,x2,x3) weight: x2 #active(x1) weight: 0 #add(x1,x2) weight: 0 add(x1,x2) weight: 0 #zero(x1) weight: 0 Usable rules: { } Removed DPs: #17 #39 Number of SCCs: 3, DPs: 21, edges: 195 SCC { #1 #8 #12 #14 #16 #19 #21 #25 #29 #31 #33 #40 #42 #48 #50..52 #55 #65 #67 #68 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. zero(x1) weight: (/ 1 8) + x1 prod(x1,x2) weight: max{x2, (/ 1 8) + x1} s(x1) weight: x1 #prod(x1,x2) weight: 0 false() weight: (/ 1 8) #fact(x1) weight: 0 #p(x1) weight: 0 true() weight: 0 p(x1) weight: x1 #mark(x1) weight: x1 0() weight: (/ 1 8) if(x1,x2,x3) weight: max{x3, (/ 1 4) + x2, (/ 1 8) + x1} #s(x1) weight: 0 fact(x1) weight: (/ 1 2) + x1 mark(x1) weight: x1 active(x1) weight: x1 #if(x1,x2,x3) weight: 0 #active(x1) weight: x1 #add(x1,x2) weight: 0 add(x1,x2) weight: max{x2, x1} #zero(x1) weight: 0 Usable rules: { 1..42 } Removed DPs: #8 #12 #16 #21 #50 Number of SCCs: 4, DPs: 16, edges: 91 SCC { #1 #14 #19 #25 #29 #31 #33 #40 #42 #48 #51 #52 #55 #65 #67 #68 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. zero(x1) weight: (/ 1 4) prod(x1,x2) weight: max{0, x2} s(x1) weight: x1 #prod(x1,x2) weight: 0 false() weight: (/ 1 4) #fact(x1) weight: 0 #p(x1) weight: 0 true() weight: (/ 1 4) p(x1) weight: (/ 1 4) + x1 #mark(x1) weight: x1 0() weight: 0 if(x1,x2,x3) weight: max{x3, (/ 1 2) + x2, (/ 1 4) + x1} #s(x1) weight: 0 fact(x1) weight: (/ 3 4) mark(x1) weight: x1 active(x1) weight: x1 #if(x1,x2,x3) weight: 0 #active(x1) weight: x1 #add(x1,x2) weight: 0 add(x1,x2) weight: max{x2, x1} #zero(x1) weight: 0 Usable rules: { 1..42 } Removed DPs: #31 #42 Number of SCCs: 4, DPs: 13, edges: 58 SCC { #1 #14 #19 #25 #29 #33 #48 #51 #52 #55 #65 #67 #68 } 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