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