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