NO * Step 1: UnsatPaths NO + Considered Problem: Rules: 0. f0(A,B,C) -> f15(2,B,C) True (1,1) 1. f15(A,B,C) -> f18(A,A,C) [10 >= A] (?,1) 2. f18(A,B,C) -> f18(A,-1 + B,F) [D >= 1 + E] (?,1) 3. f18(A,B,C) -> f15(1 + A,B,C) True (?,1) 4. f15(A,B,C) -> f28(A,B,C) [A >= 11] (?,1) Signature: {(f0,3);(f15,3);(f18,3);(f28,3)} Flow Graph: [0->{1,4},1->{2,3},2->{2,3},3->{1,4},4->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,4)] * Step 2: FromIts NO + Considered Problem: Rules: 0. f0(A,B,C) -> f15(2,B,C) True (1,1) 1. f15(A,B,C) -> f18(A,A,C) [10 >= A] (?,1) 2. f18(A,B,C) -> f18(A,-1 + B,F) [D >= 1 + E] (?,1) 3. f18(A,B,C) -> f15(1 + A,B,C) True (?,1) 4. f15(A,B,C) -> f28(A,B,C) [A >= 11] (?,1) Signature: {(f0,3);(f15,3);(f18,3);(f28,3)} Flow Graph: [0->{1},1->{2,3},2->{2,3},3->{1,4},4->{}] + Applied Processor: FromIts + Details: () * Step 3: CloseWith NO + Considered Problem: Rules: f0(A,B,C) -> f15(2,B,C) True f15(A,B,C) -> f18(A,A,C) [10 >= A] f18(A,B,C) -> f18(A,-1 + B,F) [D >= 1 + E] f18(A,B,C) -> f15(1 + A,B,C) True f15(A,B,C) -> f28(A,B,C) [A >= 11] Signature: {(f0,3);(f15,3);(f18,3);(f28,3)} Rule Graph: [0->{1},1->{2,3},2->{2,3},3->{1,4},4->{}] + Applied Processor: CloseWith False + Details: () NO