NO * Step 1: FromIts NO + Considered Problem: Rules: 0. f4(A,B,C,D,E,F,G) -> f4(A + -1*B,B,C,D,E,F,G) [A >= 0] (?,1) 1. f4(A,B,C,D,E,F,G) -> f6(A,B,0,0,0,0,0) [0 >= 1 + A] (?,1) 2. f5(A,B,C,D,E,F,G) -> f4(A,B,C,D,E,F,G) [0 >= 1 + B] (1,1) 3. f5(A,B,C,D,E,F,G) -> f6(A,B,0,0,0,0,0) [B >= 0] (1,1) Signature: {(f4,7);(f5,7);(f6,7)} Flow Graph: [0->{0,1},1->{},2->{0,1},3->{}] + Applied Processor: FromIts + Details: () * Step 2: CloseWith NO + Considered Problem: Rules: f4(A,B,C,D,E,F,G) -> f4(A + -1*B,B,C,D,E,F,G) [A >= 0] f4(A,B,C,D,E,F,G) -> f6(A,B,0,0,0,0,0) [0 >= 1 + A] f5(A,B,C,D,E,F,G) -> f4(A,B,C,D,E,F,G) [0 >= 1 + B] f5(A,B,C,D,E,F,G) -> f6(A,B,0,0,0,0,0) [B >= 0] Signature: {(f4,7);(f5,7);(f6,7)} Rule Graph: [0->{0,1},1->{},2->{0,1},3->{}] + Applied Processor: CloseWith False + Details: () NO