Input TRS:
    1: a(|0|(),b(|0|(),x)) -> b(|0|(),a(|0|(),x))
    2: a(|0|(),x) -> b(|0|(),b(|0|(),x))
    3: a(|0|(),a(|1|(),a(x,y))) -> a(|1|(),a(|0|(),a(x,y)))
    4: b(|0|(),a(|1|(),a(x,y))) -> b(|1|(),a(|0|(),a(x,y)))
    5: a(|0|(),a(x,y)) -> a(|1|(),a(|1|(),a(x,y)))
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... failed.
Freezing b
1: a(|0|(),b❆1_|0|(x)) -> b❆1_|0|(a(|0|(),x))
2: a(|0|(),x) -> b❆1_|0|(b❆1_|0|(x))
3: a(|0|(),a(|1|(),a(x,y))) -> a(|1|(),a(|0|(),a(x,y)))
4: b❆1_|0|(a(|1|(),a(x,y))) -> b❆1_|1|(a(|0|(),a(x,y)))
5: a(|0|(),a(x,y)) -> a(|1|(),a(|1|(),a(x,y)))
6: b(|0|(),_1) ->= b❆1_|0|(_1)
7: b(|1|(),_1) ->= b❆1_|1|(_1)
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... removes: 7 6
   |0|()	weight: 0
     a(x1,x2)	weight: 2 * x1 + x2
     b(x1,x2)	weight: (/ 1 2) + x1 + x2
b❆1_|0|(x1)	weight: x1
   |1|()	weight: 0
b❆1_|1|(x1)	weight: x1
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #a(|0|(),x) -> #b❆1_|0|(b❆1_|0|(x))
   #2: #a(|0|(),x) -> #b❆1_|0|(x)
   #3: #a(|0|(),a(x,y)) -> #a(|1|(),a(|1|(),a(x,y)))
   #4: #a(|0|(),a(x,y)) -> #a(|1|(),a(x,y))
   #5: #a(|0|(),a(|1|(),a(x,y))) -> #a(|1|(),a(|0|(),a(x,y)))
   #6: #a(|0|(),a(|1|(),a(x,y))) -> #a(|0|(),a(x,y))
   #7: #a(|0|(),b❆1_|0|(x)) -> #b❆1_|0|(a(|0|(),x))
   #8: #a(|0|(),b❆1_|0|(x)) -> #a(|0|(),x)
   #9: #b❆1_|0|(a(|1|(),a(x,y))) -> #a(|0|(),a(x,y))
Number of SCCs: 1, DPs: 5, edges: 14
	SCC { #2 #6..9 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
   |0|()	weight: (/ 7 16)
     a(x1,x2)	weight: max{0, (- (/ 1 16)) + x2 + x1}
     b(x1,x2)	weight: 0
b❆1_|0|(x1)	weight: max{0, (/ 3 16) + x1}
#b❆1_|0|(x1)	weight: max{0, (- (/ 1 16)) + x1}
   |1|()	weight: (/ 1 4)
b❆1_|1|(x1)	weight: 0
   #a(x1,x2)	weight: max{0, (/ 1 8) + x2}
    Usable rules: { 1..5 }
    Removed DPs: #2 #6 #8
Number of SCCs: 1, DPs: 2, edges: 2
	SCC { #7 #9 }
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