NO * Step 1: UnsatRules NO + Considered Problem: Rules: 0. f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] (1,1) 1. f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] (1,1) 2. f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && 0 >= C && C >= 3] (1,1) 3. f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] (1,1) 4. f0(A,B) -> f2(3,C) True (1,1) 5. f0(A,B) -> f2(1,C) [0 >= 1] (1,1) 6. f0(A,B) -> f2(3,C) [0 >= 3] (1,1) 7. f0(A,B) -> f2(1,C) [0 >= 1] (1,1) 8. f2(A,B) -> f2(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] (?,1) 9. f2(A,B) -> f2(B,C) [B >= 5 && B >= 2 && 1 >= B && A = 2*B] (?,1) 10. f2(A,B) -> f2(B,C) [B >= 5 && 0 >= B && B >= 3 && A = 2*B] (?,1) 11. f2(A,B) -> f2(B,C) [B >= 5 && 0 >= B && 1 >= B && A = 2*B] (?,1) 12. f2(A,B) -> f2(B,C) [B = 3 && A = 6] (?,1) 13. f2(A,B) -> f2(B,C) [3 >= B && B >= 2 && 1 >= B && A = 2*B] (?,1) 14. f2(A,B) -> f2(B,C) [0 >= 3 && B = 3 && A = 6] (?,1) 15. f2(A,B) -> f2(B,C) [3 >= B && 0 >= B && 1 >= B && A = 2*B] (?,1) 16. f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 17. f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 0 >= 3 + 6*B && A = 1 + 2*B] (?,1) 18. f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 0 >= 4 + 6*B && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 19. f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 0 >= 4 + 6*B && 0 >= 3 + 6*B && A = 1 + 2*B] (?,1) 20. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 21. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 2 + 6*B >= 0 && 0 >= 3 + 6*B && A = 1 + 2*B] (?,1) 22. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 0 >= 4 + 6*B && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 23. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 0 >= 4 + 6*B && 0 >= 3 + 6*B && A = 1 + 2*B] (?,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},1->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23} ,2->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},3->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},4->{8 ,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},5->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},6->{8,9,10 ,11,12,13,14,15,16,17,18,19,20,21,22,23},7->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},8->{8,9,10,11,12 ,13,14,15,16,17,18,19,20,21,22,23},9->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},10->{8,9,10,11,12,13 ,14,15,16,17,18,19,20,21,22,23},11->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},12->{8,9,10,11,12,13,14 ,15,16,17,18,19,20,21,22,23},13->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},14->{8,9,10,11,12,13,14,15 ,16,17,18,19,20,21,22,23},15->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},16->{8,9,10,11,12,13,14,15,16 ,17,18,19,20,21,22,23},17->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},18->{8,9,10,11,12,13,14,15,16,17 ,18,19,20,21,22,23},19->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},20->{8,9,10,11,12,13,14,15,16,17,18 ,19,20,21,22,23},21->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},22->{8,9,10,11,12,13,14,15,16,17,18,19 ,20,21,22,23},23->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [9,10,11,13,14,17,18,19,21,22] * Step 2: UnsatPaths NO + Considered Problem: Rules: 0. f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] (1,1) 1. f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] (1,1) 2. f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && 0 >= C && C >= 3] (1,1) 3. f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] (1,1) 4. f0(A,B) -> f2(3,C) True (1,1) 5. f0(A,B) -> f2(1,C) [0 >= 1] (1,1) 6. f0(A,B) -> f2(3,C) [0 >= 3] (1,1) 7. f0(A,B) -> f2(1,C) [0 >= 1] (1,1) 8. f2(A,B) -> f2(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] (?,1) 12. f2(A,B) -> f2(B,C) [B = 3 && A = 6] (?,1) 15. f2(A,B) -> f2(B,C) [3 >= B && 0 >= B && 1 >= B && A = 2*B] (?,1) 16. f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 20. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 23. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 0 >= 4 + 6*B && 0 >= 3 + 6*B && A = 1 + 2*B] (?,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{8,12,15,16,20,23},1->{8,12,15,16,20,23},2->{8,12,15,16,20,23},3->{8,12,15,16,20,23},4->{8,12,15,16,20 ,23},5->{8,12,15,16,20,23},6->{8,12,15,16,20,23},7->{8,12,15,16,20,23},8->{8,12,15,16,20,23},12->{8,12,15,16 ,20,23},15->{8,12,15,16,20,23},16->{8,12,15,16,20,23},20->{8,12,15,16,20,23},23->{8,12,15,16,20,23}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,15) ,(0,20) ,(0,23) ,(1,8) ,(1,12) ,(1,15) ,(1,16) ,(1,20) ,(1,23) ,(2,8) ,(2,12) ,(2,15) ,(2,16) ,(2,20) ,(2,23) ,(3,8) ,(3,12) ,(3,15) ,(3,16) ,(3,20) ,(3,23) ,(4,8) ,(4,12) ,(4,15) ,(4,20) ,(4,23) ,(5,8) ,(5,12) ,(5,15) ,(5,16) ,(5,20) ,(5,23) ,(6,8) ,(6,12) ,(6,15) ,(6,16) ,(6,20) ,(6,23) ,(7,8) ,(7,12) ,(7,15) ,(7,16) ,(7,20) ,(7,23) ,(8,15) ,(8,20) ,(8,23) ,(12,8) ,(12,12) ,(12,15) ,(12,20) ,(12,23) ,(15,8) ,(15,12) ,(15,16) ,(15,20) ,(16,15) ,(16,20) ,(16,23) ,(20,8) ,(20,12) ,(20,15) ,(20,20) ,(20,23) ,(23,8) ,(23,12) ,(23,16) ,(23,20)] * Step 3: UnreachableRules NO + Considered Problem: Rules: 0. f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] (1,1) 1. f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] (1,1) 2. f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && 0 >= C && C >= 3] (1,1) 3. f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] (1,1) 4. f0(A,B) -> f2(3,C) True (1,1) 5. f0(A,B) -> f2(1,C) [0 >= 1] (1,1) 6. f0(A,B) -> f2(3,C) [0 >= 3] (1,1) 7. f0(A,B) -> f2(1,C) [0 >= 1] (1,1) 8. f2(A,B) -> f2(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] (?,1) 12. f2(A,B) -> f2(B,C) [B = 3 && A = 6] (?,1) 15. f2(A,B) -> f2(B,C) [3 >= B && 0 >= B && 1 >= B && A = 2*B] (?,1) 16. f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 20. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 23. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 0 >= 4 + 6*B && 0 >= 3 + 6*B && A = 1 + 2*B] (?,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{8,12,16},1->{},2->{},3->{},4->{16},5->{},6->{},7->{},8->{8,12,16},12->{16},15->{15,23},16->{8,12,16} ,20->{16},23->{15,23}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [15,20,23] * Step 4: FromIts NO + Considered Problem: Rules: 0. f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] (1,1) 1. f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] (1,1) 2. f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && 0 >= C && C >= 3] (1,1) 3. f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] (1,1) 4. f0(A,B) -> f2(3,C) True (1,1) 5. f0(A,B) -> f2(1,C) [0 >= 1] (1,1) 6. f0(A,B) -> f2(3,C) [0 >= 3] (1,1) 7. f0(A,B) -> f2(1,C) [0 >= 1] (1,1) 8. f2(A,B) -> f2(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] (?,1) 12. f2(A,B) -> f2(B,C) [B = 3 && A = 6] (?,1) 16. f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{8,12,16},1->{},2->{},3->{},4->{16},5->{},6->{},7->{},8->{8,12,16},12->{16},16->{8,12,16}] + Applied Processor: FromIts + Details: () * Step 5: CloseWith NO + Considered Problem: Rules: f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && 0 >= C && C >= 3] f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] f0(A,B) -> f2(3,C) True f0(A,B) -> f2(1,C) [0 >= 1] f0(A,B) -> f2(3,C) [0 >= 3] f0(A,B) -> f2(1,C) [0 >= 1] f2(A,B) -> f2(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] f2(A,B) -> f2(B,C) [B = 3 && A = 6] f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] Signature: {(f0,2);(f2,2)} Rule Graph: [0->{8,12,16},1->{},2->{},3->{},4->{16},5->{},6->{},7->{},8->{8,12,16},12->{16},16->{8,12,16}] + Applied Processor: CloseWith False + Details: () NO