NO * Step 1: UnsatPaths NO + Considered Problem: Rules: 0. f4(A,B,C) -> f5(A,B,C) [A >= 1 + B] (?,1) 1. f0(A,B,C) -> f4(D,1 + D,B) True (1,1) 2. f4(A,B,C) -> f4(D,1 + D,B) True (?,1) Signature: {(f0,3);(f4,3);(f5,3)} Flow Graph: [0->{},1->{0,2},2->{0,2}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,0),(2,0)] * Step 2: UnreachableRules NO + Considered Problem: Rules: 0. f4(A,B,C) -> f5(A,B,C) [A >= 1 + B] (?,1) 1. f0(A,B,C) -> f4(D,1 + D,B) True (1,1) 2. f4(A,B,C) -> f4(D,1 + D,B) True (?,1) Signature: {(f0,3);(f4,3);(f5,3)} Flow Graph: [0->{},1->{2},2->{2}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [0] * Step 3: FromIts NO + Considered Problem: Rules: 1. f0(A,B,C) -> f4(D,1 + D,B) True (1,1) 2. f4(A,B,C) -> f4(D,1 + D,B) True (?,1) Signature: {(f0,3);(f4,3);(f5,3)} Flow Graph: [1->{2},2->{2}] + Applied Processor: FromIts + Details: () * Step 4: CloseWith NO + Considered Problem: Rules: f0(A,B,C) -> f4(D,1 + D,B) True f4(A,B,C) -> f4(D,1 + D,B) True Signature: {(f0,3);(f4,3);(f5,3)} Rule Graph: [1->{2},2->{2}] + Applied Processor: CloseWith False + Details: () NO