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.
     k(x1,x2)	weight: 0
   #*(x1,x2)	weight: 0
   #k(x1,x2)	weight: 0
   |1|()	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.
     k(x1,x2)	status: [x1,x2]	precedence above: |1|
   #*(x1,x2)	status: [x2,x1]	precedence above: k |1| *
   #k(x1,x2)	status: [x2]	precedence above:
   |1|()	status: []	precedence above:
     i(x1)	status: [x1]	precedence above: k #* |1| *
     *(x1,x2)	status: [x2,x1]	precedence above: k #* |1|
   #i(x1)	status: []	precedence above:
    Usable rules: { 1..15 }
    Removed DPs: #2 #3 #5 #9 #10
Number of SCCs: 1, DPs: 1, edges: 1
	SCC { #4 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     k(x1,x2)	weight: (/ 1 4) + x2
   #*(x1,x2)	weight: x1
   #k(x1,x2)	weight: 0
   |1|()	weight: 0
     i(x1)	weight: x1
     *(x1,x2)	weight: (/ 1 4) + x1 + x2
   #i(x1)	weight: 0
    Usable rules: { 1..15 }
    Removed DPs: #4
Number of SCCs: 0, DPs: 0, edges: 0
YES