MAYBE Problem: *(x,+(y,z)) -> +(*(x,y),*(x,z)) Proof: DP Processor: DPs: *#(x,+(y,z)) -> *#(x,z) *#(x,+(y,z)) -> *#(x,y) TRS: *(x,+(y,z)) -> +(*(x,y),*(x,z)) Usable Rule Processor: DPs: *#(x,+(y,z)) -> *#(x,z) *#(x,+(y,z)) -> *#(x,y) TRS: Restore Modifier: DPs: *#(x,+(y,z)) -> *#(x,z) *#(x,+(y,z)) -> *#(x,y) TRS: *(x,+(y,z)) -> +(*(x,y),*(x,z)) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 DPs: *#(x,+(y,z)) -> *#(x,z) *#(x,+(y,z)) -> *#(x,y) TRS: *(x,+(y,z)) -> +(*(x,y),*(x,z)) Open