Input TRS:
    1: *(x,1()) -> x
    2: *(1(),y) -> y
    3: *(i(x),x) -> 1()
    4: *(x,i(x)) -> 1()
    5: *(x,*(y,z)) -> *(*(x,y),z)
    6: i(1()) -> 1()
    7: *(*(x,y),i(y)) -> x
    8: *(*(x,i(y)),y) -> x
    9: i(i(x)) -> x
    10: i(*(x,y)) -> *(i(y),i(x))
    11: k(x,1()) -> 1()
    12: k(x,x) -> 1()
    13: *(k(x,y),k(y,x)) -> 1()
    14: *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x))
    15: k(*(x,i(y)),*(y,i(x))) -> 1()
Number of strict rules: 15
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #*(*(i(x),k(y,z)),x) -> #k(*(*(i(x),y),x),*(*(i(x),z),x))
   #2: #*(*(i(x),k(y,z)),x) -> #*(*(i(x),y),x)
   #3: #*(*(i(x),k(y,z)),x) -> #*(i(x),y)
   #4: #*(*(i(x),k(y,z)),x) -> #*(*(i(x),z),x)
   #5: #*(*(i(x),k(y,z)),x) -> #*(i(x),z)
   #6: #i(*(x,y)) -> #*(i(y),i(x))
   #7: #i(*(x,y)) -> #i(y)
   #8: #i(*(x,y)) -> #i(x)
   #9: #*(x,*(y,z)) -> #*(*(x,y),z)
   #10: #*(x,*(y,z)) -> #*(x,y)
Number of SCCs: 2, DPs: 8, edges: 40
	SCC { #7 #8 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     1()	weight: 0
     k(x1,x2)	weight: 0
   #*(x1,x2)	weight: 0
   #k(x1,x2)	weight: 0
     i(x1)	weight: 0
     *(x1,x2)	weight: (/ 1 2) + x1 + x2
   #i(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #7 #8
Number of SCCs: 1, DPs: 6, edges: 36
	SCC { #2..5 #9 #10 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
     1()	status: []	precedence above:
     k(x1,x2)	status: [x2,x1]	precedence above: 1
   #*(x1,x2)	status: [x2,x1]	precedence above: 1 k *
   #k(x1,x2)	status: [x2,x1]	precedence above:
     i(x1)	status: [x1]	precedence above: 1 k #* *
     *(x1,x2)	status: [x2,x1]	precedence above: 1 k #*
   #i(x1)	status: []	precedence above:
    Usable rules: { 1..15 }
    Removed DPs: #3 #5 #9 #10
Number of SCCs: 1, DPs: 2, edges: 4
	SCC { #2 #4 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
     1()	status: []	precedence above:
     k(x1,x2)	status: [x2,x1]	precedence above: 1
   #*(x1,x2)	status: [x2,x1]	precedence above: 1 k
   #k(x1,x2)	status: [x2,x1]	precedence above:
     i(x1)	status: [x1]	precedence above: 1 k #* *
     *(x1,x2)	status: [x2,x1]	precedence above: 1 k #*
   #i(x1)	status: []	precedence above:
    Usable rules: { 1..15 }
    Removed DPs: #2 #4
Number of SCCs: 0, DPs: 0, edges: 0
YES