MAYBE Problem: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Proof: DP Processor: DPs: active#(f(X)) -> f#(true()) active#(f(X)) -> if#(X,c(),f(true())) active#(f(X)) -> mark#(if(X,c(),f(true()))) active#(if(true(),X,Y)) -> mark#(X) active#(if(false(),X,Y)) -> mark#(Y) mark#(f(X)) -> mark#(X) mark#(f(X)) -> f#(mark(X)) mark#(f(X)) -> active#(f(mark(X))) mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) mark#(c()) -> active#(c()) mark#(true()) -> active#(true()) mark#(false()) -> active#(false()) f#(mark(X)) -> f#(X) f#(active(X)) -> f#(X) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) EDG Processor: DPs: active#(f(X)) -> f#(true()) active#(f(X)) -> if#(X,c(),f(true())) active#(f(X)) -> mark#(if(X,c(),f(true()))) active#(if(true(),X,Y)) -> mark#(X) active#(if(false(),X,Y)) -> mark#(Y) mark#(f(X)) -> mark#(X) mark#(f(X)) -> f#(mark(X)) mark#(f(X)) -> active#(f(mark(X))) mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) mark#(c()) -> active#(c()) mark#(true()) -> active#(true()) mark#(false()) -> active#(false()) f#(mark(X)) -> f#(X) f#(active(X)) -> f#(X) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) graph: mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(f(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(f(X)) -> f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(f(X)) -> active#(f(mark(X))) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(c()) -> active#(c()) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(true()) -> active#(true()) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(false()) -> active#(false()) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(f(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(f(X)) -> f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(f(X)) -> active#(f(mark(X))) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(c()) -> active#(c()) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(true()) -> active#(true()) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(false()) -> active#(false()) mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) -> active#(f(X)) -> f#(true()) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) -> active#(f(X)) -> if#(X,c(),f(true())) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) -> active#(f(X)) -> mark#(if(X,c(),f(true()))) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) -> active#(if(true(),X,Y)) -> mark#(X) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) -> active#(if(false(),X,Y)) -> mark#(Y) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> f#(mark(X)) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X))) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) mark#(f(X)) -> mark#(X) -> mark#(c()) -> active#(c()) mark#(f(X)) -> mark#(X) -> mark#(true()) -> active#(true()) mark#(f(X)) -> mark#(X) -> mark#(false()) -> active#(false()) mark#(f(X)) -> f#(mark(X)) -> f#(mark(X)) -> f#(X) mark#(f(X)) -> f#(mark(X)) -> f#(active(X)) -> f#(X) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(X)) -> f#(true()) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(X)) -> if#(X,c(),f(true())) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(X)) -> mark#(if(X,c(),f(true()))) mark#(f(X)) -> active#(f(mark(X))) -> active#(if(true(),X,Y)) -> mark#(X) mark#(f(X)) -> active#(f(mark(X))) -> active#(if(false(),X,Y)) -> mark#(Y) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,X2,active(X3)) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,X2,active(X3)) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) -> if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) -> if#(X1,X2,active(X3)) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) -> if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) -> if#(X1,X2,active(X3)) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) -> if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) -> if#(X1,X2,active(X3)) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) -> if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) -> if#(X1,X2,active(X3)) -> if#(X1,X2,X3) f#(mark(X)) -> f#(X) -> f#(mark(X)) -> f#(X) f#(mark(X)) -> f#(X) -> f#(active(X)) -> f#(X) f#(active(X)) -> f#(X) -> f#(mark(X)) -> f#(X) f#(active(X)) -> f#(X) -> f#(active(X)) -> f#(X) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(f(X)) -> mark#(X) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(f(X)) -> f#(mark(X)) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(f(X)) -> active#(f(mark(X))) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> mark#(X2) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> mark#(X1) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(c()) -> active#(c()) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(true()) -> active#(true()) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(false()) -> active#(false()) active#(if(true(),X,Y)) -> mark#(X) -> mark#(f(X)) -> mark#(X) active#(if(true(),X,Y)) -> mark#(X) -> mark#(f(X)) -> f#(mark(X)) active#(if(true(),X,Y)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X))) active#(if(true(),X,Y)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X2) active#(if(true(),X,Y)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) active#(if(true(),X,Y)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) active#(if(true(),X,Y)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) active#(if(true(),X,Y)) -> mark#(X) -> mark#(c()) -> active#(c()) active#(if(true(),X,Y)) -> mark#(X) -> mark#(true()) -> active#(true()) active#(if(true(),X,Y)) -> mark#(X) -> mark#(false()) -> active#(false()) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(f(X)) -> mark#(X) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(f(X)) -> f#(mark(X)) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(f(X)) -> active#(f(mark(X))) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(if(X1,X2,X3)) -> mark#(X2) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(if(X1,X2,X3)) -> mark#(X1) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) SCC Processor: #sccs: 3 #rules: 16 #arcs: 113/529 DPs: mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) active#(if(false(),X,Y)) -> mark#(Y) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(f(X)) -> active#(f(mark(X))) active#(if(true(),X,Y)) -> mark#(X) mark#(f(X)) -> mark#(X) active#(f(X)) -> mark#(if(X,c(),f(true()))) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Open DPs: f#(active(X)) -> f#(X) f#(mark(X)) -> f#(X) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Open DPs: if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Open