YES * Step 1: FromIts YES + Considered Problem: Rules: 0. start(A,B,C,D) -> lbl41(E,B,C,D) [A = B && C = D] (?,1) 1. lbl41(A,B,C,D) -> stop(A,B,A,D) [C = D] (?,1) 2. start0(A,B,C,D) -> start(B,B,D,D) True (1,1) Signature: {(lbl41,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{1},1->{},2->{0}] + Applied Processor: FromIts + Details: () * Step 2: Decompose YES + Considered Problem: Rules: start(A,B,C,D) -> lbl41(E,B,C,D) [A = B && C = D] lbl41(A,B,C,D) -> stop(A,B,A,D) [C = D] start0(A,B,C,D) -> start(B,B,D,D) True Signature: {(lbl41,4);(start,4);(start0,4);(stop,4)} Rule Graph: [0->{1},1->{},2->{0}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2] * Step 3: CloseWith YES + Considered Problem: (Rules: start(A,B,C,D) -> lbl41(E,B,C,D) [A = B && C = D] lbl41(A,B,C,D) -> stop(A,B,A,D) [C = D] start0(A,B,C,D) -> start(B,B,D,D) True Signature: {(lbl41,4);(start,4);(start0,4);(stop,4)} Rule Graph: [0->{1},1->{},2->{0}] ,We construct a looptree: P: [0,1,2]) + Applied Processor: CloseWith True + Details: () YES