MAYBE * Step 1: FromIts MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E) -> f3(0,0,C,D,E) True (1,1) 1. f3(A,B,C,D,E) -> f3(A,B,-1 + C,F,E) [-1*B >= 0 (?,1) && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && C >= 1 && F >= 1] 2. f3(A,B,C,D,E) -> f3(A,B,-2 + C,F,E) [-1*B >= 0 (?,1) && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && C >= 1 && 0 >= F] 3. f3(A,B,C,D,E) -> f6(A,B,C,D,F) [-1*B >= 0 (?,1) && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && 0 >= C] 4. f6(A,B,C,D,E) -> f6(1,B,C,D,F) [-1*C >= 0 (?,1) && B + -1*C >= 0 && -1*B + -1*C >= 0 && A + -1*C >= 0 && -1*B >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= 1] 5. f6(A,B,C,D,E) -> f6(0,B,C,D,F) [-1*C >= 0 (?,1) && B + -1*C >= 0 && -1*B + -1*C >= 0 && A + -1*C >= 0 && -1*B >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= E] Signature: {(f0,5);(f3,5);(f6,5)} Flow Graph: [0->{1,2,3},1->{1,2,3},2->{1,2,3},3->{4,5},4->{4,5},5->{4,5}] + Applied Processor: FromIts + Details: () * Step 2: AddSinks MAYBE + Considered Problem: Rules: f0(A,B,C,D,E) -> f3(0,0,C,D,E) True f3(A,B,C,D,E) -> f3(A,B,-1 + C,F,E) [-1*B >= 0 && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && C >= 1 && F >= 1] f3(A,B,C,D,E) -> f3(A,B,-2 + C,F,E) [-1*B >= 0 && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && C >= 1 && 0 >= F] f3(A,B,C,D,E) -> f6(A,B,C,D,F) [-1*B >= 0 && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && 0 >= C] f6(A,B,C,D,E) -> f6(1,B,C,D,F) [-1*C >= 0 && B + -1*C >= 0 && -1*B + -1*C >= 0 && A + -1*C >= 0 && -1*B >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= 1] f6(A,B,C,D,E) -> f6(0,B,C,D,F) [-1*C >= 0 && B + -1*C >= 0 && -1*B + -1*C >= 0 && A + -1*C >= 0 && -1*B >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= E] Signature: {(f0,5);(f3,5);(f6,5)} Rule Graph: [0->{1,2,3},1->{1,2,3},2->{1,2,3},3->{4,5},4->{4,5},5->{4,5}] + Applied Processor: AddSinks + Details: () * Step 3: Failure MAYBE + Considered Problem: Rules: f0(A,B,C,D,E) -> f3(0,0,C,D,E) True f3(A,B,C,D,E) -> f3(A,B,-1 + C,F,E) [-1*B >= 0 && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && C >= 1 && F >= 1] f3(A,B,C,D,E) -> f3(A,B,-2 + C,F,E) [-1*B >= 0 && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && C >= 1 && 0 >= F] f3(A,B,C,D,E) -> f6(A,B,C,D,F) [-1*B >= 0 && A + -1*B >= 0 && -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && -1*A >= 0 && A >= 0 && 0 >= C] f6(A,B,C,D,E) -> f6(1,B,C,D,F) [-1*C >= 0 && B + -1*C >= 0 && -1*B + -1*C >= 0 && A + -1*C >= 0 && -1*B >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= 1] f6(A,B,C,D,E) -> f6(0,B,C,D,F) [-1*C >= 0 && B + -1*C >= 0 && -1*B + -1*C >= 0 && A + -1*C >= 0 && -1*B >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= E] f6(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f6(A,B,C,D,E) -> exitus616(A,B,C,D,E) True Signature: {(exitus616,5);(f0,5);(f3,5);(f6,5)} Rule Graph: [0->{1,2,3},1->{1,2,3},2->{1,2,3},3->{4,5},4->{4,5,6},5->{4,5,7}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7] | +- p:[1,2] c: [1,2] | `- p:[4,5] c: [] MAYBE