MAYBE Problem: f(a(),b()) -> f(a(),c()) f(c(),d()) -> f(b(),d()) Proof: DP Processor: DPs: f#(a(),b()) -> f#(a(),c()) f#(c(),d()) -> f#(b(),d()) TRS: f(a(),b()) -> f(a(),c()) f(c(),d()) -> f(b(),d()) Usable Rule Processor: DPs: f#(a(),b()) -> f#(a(),c()) f#(c(),d()) -> f#(b(),d()) TRS: Restore Modifier: DPs: f#(a(),b()) -> f#(a(),c()) f#(c(),d()) -> f#(b(),d()) TRS: f(a(),b()) -> f(a(),c()) f(c(),d()) -> f(b(),d()) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 DPs: f#(a(),b()) -> f#(a(),c()) f#(c(),d()) -> f#(b(),d()) TRS: f(a(),b()) -> f(a(),c()) f(c(),d()) -> f(b(),d()) Open