YES * Step 1: FromIts YES + Considered Problem: Rules: 0. f2(A,B,C,D,E,F) -> f2(-1 + A,-1 + B,A,B,-2 + A,F) [A >= 1 && B >= 1] (?,1) 1. f3(A,B,C,D,E,F) -> f2(A,B,C,D,E,F) True (1,1) 2. f2(A,B,C,D,E,F) -> f4(A,G,C,D,E,H) [0 >= B && 0 >= G] (?,1) 3. f2(A,B,C,D,E,F) -> f4(A,B,C,D,E,H) [B >= 1 && 0 >= A] (?,1) Signature: {(f2,6);(f3,6);(f4,6)} Flow Graph: [0->{0,2,3},1->{0,2,3},2->{},3->{}] + Applied Processor: FromIts + Details: () * Step 2: Decompose YES + Considered Problem: Rules: f2(A,B,C,D,E,F) -> f2(-1 + A,-1 + B,A,B,-2 + A,F) [A >= 1 && B >= 1] f3(A,B,C,D,E,F) -> f2(A,B,C,D,E,F) True f2(A,B,C,D,E,F) -> f4(A,G,C,D,E,H) [0 >= B && 0 >= G] f2(A,B,C,D,E,F) -> f4(A,B,C,D,E,H) [B >= 1 && 0 >= A] Signature: {(f2,6);(f3,6);(f4,6)} Rule Graph: [0->{0,2,3},1->{0,2,3},2->{},3->{}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3] | `- p:[0] c: [0] * Step 3: CloseWith YES + Considered Problem: (Rules: f2(A,B,C,D,E,F) -> f2(-1 + A,-1 + B,A,B,-2 + A,F) [A >= 1 && B >= 1] f3(A,B,C,D,E,F) -> f2(A,B,C,D,E,F) True f2(A,B,C,D,E,F) -> f4(A,G,C,D,E,H) [0 >= B && 0 >= G] f2(A,B,C,D,E,F) -> f4(A,B,C,D,E,H) [B >= 1 && 0 >= A] Signature: {(f2,6);(f3,6);(f4,6)} Rule Graph: [0->{0,2,3},1->{0,2,3},2->{},3->{}] ,We construct a looptree: P: [0,1,2,3] | `- p:[0] c: [0]) + Applied Processor: CloseWith True + Details: () YES