MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f0(A,B,C) -> f154(0,2,0) True (1,1) 1. f154(A,B,C) -> f154(A + C,B,1 + C) [2 >= C] (?,1) 2. f160(A,B,C) -> f160(A + C,B,1 + C) [3 >= C] (?,1) 3. f166(A,B,C) -> f166(A + C,B,1 + C) [2 >= C] (?,1) 4. f172(A,B,C) -> f172(A + C,B,1 + C) [3 >= C] (?,1) 5. f180(A,B,C) -> f180(A + C,B,1 + C) [1 >= C] (?,1) 6. f186(A,B,C) -> f186(A + C,B,1 + C) [2 >= C] (?,1) 7. f192(A,B,C) -> f192(A + C,B,1 + C) [1 >= C] (?,1) 8. f198(A,B,C) -> f198(A + C,B,1 + C) [2 >= C] (?,1) 9. f206(A,B,C) -> f206(A + C,B,1 + C) [0 >= 3 + C] (?,1) 10. f212(A,B,C) -> f212(A + C,B,1 + C) [0 >= 2 + C] (?,1) 11. f218(A,B,C) -> f218(A + C,B,1 + C) [0 >= 3 + C] (?,1) 12. f224(A,B,C) -> f224(A + C,B,1 + C) [0 >= 2 + C] (?,1) 13. f232(A,B,C) -> f232(A + C,B,1 + C) [0 >= 2 + C] (?,1) 14. f238(A,B,C) -> f238(A + C,B,1 + C) [0 >= 1 + C] (?,1) 15. f244(A,B,C) -> f244(A + C,B,1 + C) [0 >= 2 + C] (?,1) 16. f250(A,B,C) -> f250(A + C,B,1 + C) [0 >= 1 + C] (?,1) 17. f258(A,B,C) -> f258(A + C,B,1 + C) [0 >= 1 + C] (?,1) 18. f264(A,B,C) -> f264(A + C,B,1 + C) [0 >= C] (?,1) 19. f270(A,B,C) -> f270(A + C,B,1 + C) [0 >= 1 + C] (?,1) 20. f276(A,B,C) -> f276(A + C,B,1 + C) [0 >= C] (?,1) 21. f284(A,B,C) -> f284(A + C,B,1 + C) [3 >= C] (?,1) 22. f290(A,B,C) -> f290(A + C,B,1 + C) [4 >= C] (?,1) 23. f296(A,B,C) -> f296(A + C,B,1 + C) [3 >= C] (?,1) 24. f302(A,B,C) -> f302(A + C,B,1 + C) [4 >= C] (?,1) 25. f310(A,B,C) -> f310(A + C,B,B + C) [2 >= C] (?,1) 26. f316(A,B,C) -> f316(A + C,B,B + C) [3 >= C] (?,1) 27. f322(A,B,C) -> f322(A + C,B,B + C) [2 >= C] (?,1) 28. f328(A,B,C) -> f328(A + C,B,B + C) [3 >= C] (?,1) 29. f336(A,B,C) -> f336(A + C,B,B + C) [1 >= C] (?,1) 30. f342(A,B,C) -> f342(A + C,B,B + C) [2 >= C] (?,1) 31. f348(A,B,C) -> f348(A + C,B,B + C) [1 >= C] (?,1) 32. f354(A,B,C) -> f354(A + C,B,B + C) [2 >= C] (?,1) 33. f362(A,B,C) -> f362(A + C,B,B + C) [0 >= 3 + C] (?,1) 34. f368(A,B,C) -> f368(A + C,B,B + C) [0 >= 2 + C] (?,1) 35. f374(A,B,C) -> f374(A + C,B,B + C) [0 >= 3 + C] (?,1) 36. f380(A,B,C) -> f380(A + C,B,B + C) [0 >= 2 + C] (?,1) 37. f388(A,B,C) -> f388(A + C,B,B + C) [0 >= 2 + C] (?,1) 38. f394(A,B,C) -> f394(A + C,B,B + C) [0 >= 1 + C] (?,1) 39. f400(A,B,C) -> f400(A + C,B,B + C) [0 >= 2 + C] (?,1) 40. f406(A,B,C) -> f406(A + C,B,B + C) [0 >= 1 + C] (?,1) 41. f414(A,B,C) -> f414(A + C,B,B + C) [0 >= 1 + C] (?,1) 42. f420(A,B,C) -> f420(A + C,B,B + C) [0 >= C] (?,1) 43. f426(A,B,C) -> f426(A + C,B,B + C) [0 >= 1 + C] (?,1) 44. f432(A,B,C) -> f432(A + C,B,B + C) [0 >= C] (?,1) 45. f440(A,B,C) -> f440(A + C,B,B + C) [3 >= C] (?,1) 46. f446(A,B,C) -> f446(A + C,B,B + C) [4 >= C] (?,1) 47. f452(A,B,C) -> f452(A + C,B,B + C) [3 >= C] (?,1) 48. f458(A,B,C) -> f458(A + C,B,B + C) [4 >= C] (?,1) 49. f466(A,B,C) -> f466(A + C,B,-1 + C) [C >= 3] (?,1) 50. f472(A,B,C) -> f472(A + C,B,-1 + C) [C >= 2] (?,1) 51. f478(A,B,C) -> f478(A + C,B,-1 + C) [C >= 3] (?,1) 52. f484(A,B,C) -> f484(A + C,B,-1 + C) [C >= 2] (?,1) 53. f492(A,B,C) -> f492(A + C,B,-1 + C) [C >= 2] (?,1) 54. f498(A,B,C) -> f498(A + C,B,-1 + C) [C >= 1] (?,1) 55. f504(A,B,C) -> f504(A + C,B,-1 + C) [C >= 2] (?,1) 56. f510(A,B,C) -> f510(A + C,B,-1 + C) [C >= 1] (?,1) 57. f518(A,B,C) -> f518(A + C,B,-1 + C) [C >= 1] (?,1) 58. f524(A,B,C) -> f524(A + C,B,-1 + C) [C >= 0] (?,1) 59. f530(A,B,C) -> f530(A + C,B,-1 + C) [C >= 1] (?,1) 60. f536(A,B,C) -> f536(A + C,B,-1 + C) [C >= 0] (?,1) 61. f544(A,B,C) -> f544(A + C,B,-1 + C) [C >= 0] (?,1) 62. f550(A,B,C) -> f550(A + C,B,-1 + C) [1 + C >= 0] (?,1) 63. f556(A,B,C) -> f556(A + C,B,-1 + C) [C >= 0] (?,1) 64. f562(A,B,C) -> f562(A + C,B,-1 + C) [1 + C >= 0] (?,1) 65. f570(A,B,C) -> f570(A + C,B,-1 + C) [1 + C >= 0] (?,1) 66. f576(A,B,C) -> f576(A + C,B,-1 + C) [2 + C >= 0] (?,1) 67. f582(A,B,C) -> f582(A + C,B,-1 + C) [1 + C >= 0] (?,1) 68. f588(A,B,C) -> f588(A + C,B,-1 + C) [2 + C >= 0] (?,1) 69. f596(A,B,C) -> f596(A + C,B,-1 + C) [2 + C >= 0] (?,1) 70. f602(A,B,C) -> f602(A + C,B,-1 + C) [3 + C >= 0] (?,1) 71. f608(A,B,C) -> f608(A + C,B,-1 + C) [2 + C >= 0] (?,1) 72. f614(A,B,C) -> f614(A + C,B,-1 + C) [3 + C >= 0] (?,1) 73. f622(A,B,C) -> f622(A + C,B,-1 + C) [4 + C >= 0] (?,1) 74. f628(A,B,C) -> f628(A + C,B,-1 + C) [5 + C >= 0] (?,1) 75. f634(A,B,C) -> f634(A + C,B,-1 + C) [4 + C >= 0] (?,1) 76. f640(A,B,C) -> f640(A + C,B,-1 + C) [5 + C >= 0] (?,1) 77. f648(A,B,C) -> f648(A + C,B,-1 + C) [6 + C >= 0] (?,1) 78. f654(A,B,C) -> f654(A + C,B,-1 + C) [7 + C >= 0] (?,1) 79. f660(A,B,C) -> f660(A + C,B,-1 + C) [6 + C >= 0] (?,1) 80. f666(A,B,C) -> f666(A + C,B,-1 + C) [7 + C >= 0] (?,1) 81. f674(A,B,C) -> f674(A + C,B,-1 + C) [7 + C >= 0] (?,1) 82. f680(A,B,C) -> f680(A + C,B,-1 + C) [8 + C >= 0] (?,1) 83. f686(A,B,C) -> f686(A + C,B,-1 + C) [7 + C >= 0] (?,1) 84. f692(A,B,C) -> f692(A + C,B,-1 + C) [8 + C >= 0] (?,1) 85. f700(A,B,C) -> f700(A + C,B,-1*B + C) [C >= 3] (?,1) 86. f706(A,B,C) -> f706(A + C,B,-1*B + C) [C >= 2] (?,1) 87. f712(A,B,C) -> f712(A + C,B,-1*B + C) [C >= 3] (?,1) 88. f718(A,B,C) -> f718(A + C,B,-1*B + C) [C >= 2] (?,1) 89. f726(A,B,C) -> f726(A + C,B,-1*B + C) [C >= 2] (?,1) 90. f732(A,B,C) -> f732(A + C,B,-1*B + C) [C >= 1] (?,1) 91. f738(A,B,C) -> f738(A + C,B,-1*B + C) [C >= 2] (?,1) 92. f744(A,B,C) -> f744(A + C,B,-1*B + C) [C >= 1] (?,1) 93. f752(A,B,C) -> f752(A + C,B,-1*B + C) [C >= 1] (?,1) 94. f758(A,B,C) -> f758(A + C,B,-1*B + C) [C >= 0] (?,1) 95. f764(A,B,C) -> f764(A + C,B,-1*B + C) [C >= 1] (?,1) 96. f770(A,B,C) -> f770(A + C,B,-1*B + C) [C >= 0] (?,1) 97. f778(A,B,C) -> f778(A + C,B,-1*B + C) [C >= 0] (?,1) 98. f784(A,B,C) -> f784(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 99. f790(A,B,C) -> f790(A + C,B,-1*B + C) [C >= 0] (?,1) 100. f796(A,B,C) -> f796(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 101. f804(A,B,C) -> f804(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 102. f810(A,B,C) -> f810(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 103. f816(A,B,C) -> f816(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 104. f822(A,B,C) -> f822(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 105. f830(A,B,C) -> f830(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 106. f836(A,B,C) -> f836(A + C,B,-1*B + C) [3 + C >= 0] (?,1) 107. f842(A,B,C) -> f842(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 108. f848(A,B,C) -> f848(A + C,B,-1*B + C) [3 + C >= 0] (?,1) 109. f856(A,B,C) -> f856(A + C,B,-1*B + C) [4 + C >= 0] (?,1) 110. f862(A,B,C) -> f862(A + C,B,-1*B + C) [5 + C >= 0] (?,1) 111. f868(A,B,C) -> f868(A + C,B,-1*B + C) [4 + C >= 0] (?,1) 112. f874(A,B,C) -> f874(A + C,B,-1*B + C) [5 + C >= 0] (?,1) 113. f882(A,B,C) -> f882(A + C,B,-1*B + C) [6 + C >= 0] (?,1) 114. f888(A,B,C) -> f888(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 115. f894(A,B,C) -> f894(A + C,B,-1*B + C) [6 + C >= 0] (?,1) 116. f900(A,B,C) -> f900(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 117. f908(A,B,C) -> f908(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 118. f914(A,B,C) -> f914(A + C,B,-1*B + C) [8 + C >= 0] (?,1) 119. f920(A,B,C) -> f920(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 120. f926(A,B,C) -> f926(A + C,B,-1*B + C) [8 + C >= 0] (?,1) 121. f926(A,B,C) -> f934(A,B,C) [0 >= 9 + C] (?,1) 122. f920(A,B,C) -> f926(A,B,16) [0 >= 8 + C] (?,1) 123. f914(A,B,C) -> f920(A,B,16) [0 >= 9 + C] (?,1) 124. f908(A,B,C) -> f914(A,B,16) [0 >= 8 + C] (?,1) 125. f900(A,B,C) -> f908(A,B,16) [0 >= 8 + C] (?,1) 126. f894(A,B,C) -> f900(A,B,-2) [0 >= 7 + C] (?,1) 127. f888(A,B,C) -> f894(A,B,-2) [0 >= 8 + C] (?,1) 128. f882(A,B,C) -> f888(A,B,-2) [0 >= 7 + C] (?,1) 129. f874(A,B,C) -> f882(A,B,-2) [0 >= 6 + C] (?,1) 130. f868(A,B,C) -> f874(A,B,-1) [0 >= 5 + C] (?,1) 131. f862(A,B,C) -> f868(A,B,-1) [0 >= 6 + C] (?,1) 132. f856(A,B,C) -> f862(A,B,-1) [0 >= 5 + C] (?,1) 133. f848(A,B,C) -> f856(A,B,-1) [0 >= 4 + C] (?,1) 134. f842(A,B,C) -> f848(A,B,0) [0 >= 3 + C] (?,1) 135. f836(A,B,C) -> f842(A,B,0) [0 >= 4 + C] (?,1) 136. f830(A,B,C) -> f836(A,B,0) [0 >= 3 + C] (?,1) 137. f822(A,B,C) -> f830(A,B,0) [0 >= 3 + C] (?,1) 138. f816(A,B,C) -> f822(A,B,9) [0 >= 2 + C] (?,1) 139. f810(A,B,C) -> f816(A,B,9) [0 >= 3 + C] (?,1) 140. f804(A,B,C) -> f810(A,B,9) [0 >= 2 + C] (?,1) 141. f796(A,B,C) -> f804(A,B,9) [0 >= 2 + C] (?,1) 142. f790(A,B,C) -> f796(A,B,8) [0 >= 1 + C] (?,1) 143. f784(A,B,C) -> f790(A,B,8) [0 >= 2 + C] (?,1) 144. f778(A,B,C) -> f784(A,B,8) [0 >= 1 + C] (?,1) 145. f770(A,B,C) -> f778(A,B,8) [0 >= 1 + C] (?,1) 146. f764(A,B,C) -> f770(A,B,7) [0 >= C] (?,1) 147. f758(A,B,C) -> f764(A,B,7) [0 >= 1 + C] (?,1) 148. f752(A,B,C) -> f758(A,B,7) [0 >= C] (?,1) 149. f744(A,B,C) -> f752(A,B,7) [0 >= C] (?,1) 150. f738(A,B,C) -> f744(A,B,6) [1 >= C] (?,1) 151. f732(A,B,C) -> f738(A,B,6) [0 >= C] (?,1) 152. f726(A,B,C) -> f732(A,B,6) [1 >= C] (?,1) 153. f718(A,B,C) -> f726(A,B,6) [1 >= C] (?,1) 154. f712(A,B,C) -> f718(A,B,5) [2 >= C] (?,1) 155. f706(A,B,C) -> f712(A,B,5) [1 >= C] (?,1) 156. f700(A,B,C) -> f706(A,B,5) [2 >= C] (?,1) 157. f692(A,B,C) -> f700(A,B,5) [0 >= 9 + C] (?,1) 158. f686(A,B,C) -> f692(A,B,16) [0 >= 8 + C] (?,1) 159. f680(A,B,C) -> f686(A,B,16) [0 >= 9 + C] (?,1) 160. f674(A,B,C) -> f680(A,B,16) [0 >= 8 + C] (?,1) 161. f666(A,B,C) -> f674(A,B,16) [0 >= 8 + C] (?,1) 162. f660(A,B,C) -> f666(A,B,-2) [0 >= 7 + C] (?,1) 163. f654(A,B,C) -> f660(A,B,-2) [0 >= 8 + C] (?,1) 164. f648(A,B,C) -> f654(A,B,-2) [0 >= 7 + C] (?,1) 165. f640(A,B,C) -> f648(A,B,-2) [0 >= 6 + C] (?,1) 166. f634(A,B,C) -> f640(A,B,-1) [0 >= 5 + C] (?,1) 167. f628(A,B,C) -> f634(A,B,-1) [0 >= 6 + C] (?,1) 168. f622(A,B,C) -> f628(A,B,-1) [0 >= 5 + C] (?,1) 169. f614(A,B,C) -> f622(A,B,-1) [0 >= 4 + C] (?,1) 170. f608(A,B,C) -> f614(A,B,0) [0 >= 3 + C] (?,1) 171. f602(A,B,C) -> f608(A,B,0) [0 >= 4 + C] (?,1) 172. f596(A,B,C) -> f602(A,B,0) [0 >= 3 + C] (?,1) 173. f588(A,B,C) -> f596(A,B,0) [0 >= 3 + C] (?,1) 174. f582(A,B,C) -> f588(A,B,9) [0 >= 2 + C] (?,1) 175. f576(A,B,C) -> f582(A,B,9) [0 >= 3 + C] (?,1) 176. f570(A,B,C) -> f576(A,B,9) [0 >= 2 + C] (?,1) 177. f562(A,B,C) -> f570(A,B,9) [0 >= 2 + C] (?,1) 178. f556(A,B,C) -> f562(A,B,8) [0 >= 1 + C] (?,1) 179. f550(A,B,C) -> f556(A,B,8) [0 >= 2 + C] (?,1) 180. f544(A,B,C) -> f550(A,B,8) [0 >= 1 + C] (?,1) 181. f536(A,B,C) -> f544(A,B,8) [0 >= 1 + C] (?,1) 182. f530(A,B,C) -> f536(A,B,7) [0 >= C] (?,1) 183. f524(A,B,C) -> f530(A,B,7) [0 >= 1 + C] (?,1) 184. f518(A,B,C) -> f524(A,B,7) [0 >= C] (?,1) 185. f510(A,B,C) -> f518(A,B,7) [0 >= C] (?,1) 186. f504(A,B,C) -> f510(A,B,6) [1 >= C] (?,1) 187. f498(A,B,C) -> f504(A,B,6) [0 >= C] (?,1) 188. f492(A,B,C) -> f498(A,B,6) [1 >= C] (?,1) 189. f484(A,B,C) -> f492(A,B,6) [1 >= C] (?,1) 190. f478(A,B,C) -> f484(A,B,5) [2 >= C] (?,1) 191. f472(A,B,C) -> f478(A,B,5) [1 >= C] (?,1) 192. f466(A,B,C) -> f472(A,B,5) [2 >= C] (?,1) 193. f458(A,B,C) -> f466(A,B,5) [C >= 5] (?,1) 194. f452(A,B,C) -> f458(A,B,-6) [C >= 4] (?,1) 195. f446(A,B,C) -> f452(A,B,-6) [C >= 5] (?,1) 196. f440(A,B,C) -> f446(A,B,-6) [C >= 4] (?,1) 197. f432(A,B,C) -> f440(A,B,-6) [C >= 1] (?,1) 198. f426(A,B,C) -> f432(A,B,-5) [C >= 0] (?,1) 199. f420(A,B,C) -> f426(A,B,-5) [C >= 1] (?,1) 200. f414(A,B,C) -> f420(A,B,-5) [C >= 0] (?,1) 201. f406(A,B,C) -> f414(A,B,-5) [C >= 0] (?,1) 202. f400(A,B,C) -> f406(A,B,-4) [1 + C >= 0] (?,1) 203. f394(A,B,C) -> f400(A,B,-4) [C >= 0] (?,1) 204. f388(A,B,C) -> f394(A,B,-4) [1 + C >= 0] (?,1) 205. f380(A,B,C) -> f388(A,B,-4) [1 + C >= 0] (?,1) 206. f374(A,B,C) -> f380(A,B,-3) [2 + C >= 0] (?,1) 207. f368(A,B,C) -> f374(A,B,-3) [1 + C >= 0] (?,1) 208. f362(A,B,C) -> f368(A,B,-3) [2 + C >= 0] (?,1) 209. f354(A,B,C) -> f362(A,B,-3) [C >= 3] (?,1) 210. f348(A,B,C) -> f354(A,B,1) [C >= 2] (?,1) 211. f342(A,B,C) -> f348(A,B,1) [C >= 3] (?,1) 212. f336(A,B,C) -> f342(A,B,1) [C >= 2] (?,1) 213. f328(A,B,C) -> f336(A,B,1) [C >= 4] (?,1) 214. f322(A,B,C) -> f328(A,B,0) [C >= 3] (?,1) 215. f316(A,B,C) -> f322(A,B,0) [C >= 4] (?,1) 216. f310(A,B,C) -> f316(A,B,0) [C >= 3] (?,1) 217. f302(A,B,C) -> f310(A,B,0) [C >= 5] (?,1) 218. f296(A,B,C) -> f302(A,B,-6) [C >= 4] (?,1) 219. f290(A,B,C) -> f296(A,B,-6) [C >= 5] (?,1) 220. f284(A,B,C) -> f290(A,B,-6) [C >= 4] (?,1) 221. f276(A,B,C) -> f284(A,B,-6) [C >= 1] (?,1) 222. f270(A,B,C) -> f276(A,B,-5) [C >= 0] (?,1) 223. f264(A,B,C) -> f270(A,B,-5) [C >= 1] (?,1) 224. f258(A,B,C) -> f264(A,B,-5) [C >= 0] (?,1) 225. f250(A,B,C) -> f258(A,B,-5) [C >= 0] (?,1) 226. f244(A,B,C) -> f250(A,B,-4) [1 + C >= 0] (?,1) 227. f238(A,B,C) -> f244(A,B,-4) [C >= 0] (?,1) 228. f232(A,B,C) -> f238(A,B,-4) [1 + C >= 0] (?,1) 229. f224(A,B,C) -> f232(A,B,-4) [1 + C >= 0] (?,1) 230. f218(A,B,C) -> f224(A,B,-3) [2 + C >= 0] (?,1) 231. f212(A,B,C) -> f218(A,B,-3) [1 + C >= 0] (?,1) 232. f206(A,B,C) -> f212(A,B,-3) [2 + C >= 0] (?,1) 233. f198(A,B,C) -> f206(A,B,-3) [C >= 3] (?,1) 234. f192(A,B,C) -> f198(A,B,1) [C >= 2] (?,1) 235. f186(A,B,C) -> f192(A,B,1) [C >= 3] (?,1) 236. f180(A,B,C) -> f186(A,B,1) [C >= 2] (?,1) 237. f172(A,B,C) -> f180(A,B,1) [C >= 4] (?,1) 238. f166(A,B,C) -> f172(A,B,0) [C >= 3] (?,1) 239. f160(A,B,C) -> f166(A,B,0) [C >= 4] (?,1) 240. f154(A,B,C) -> f160(A,B,0) [C >= 3] (?,1) Signature: {(f0,3) ;(f154,3) ;(f160,3) ;(f166,3) ;(f172,3) ;(f180,3) ;(f186,3) ;(f192,3) ;(f198,3) ;(f206,3) ;(f212,3) ;(f218,3) ;(f224,3) ;(f232,3) ;(f238,3) ;(f244,3) ;(f250,3) ;(f258,3) ;(f264,3) ;(f270,3) ;(f276,3) ;(f284,3) ;(f290,3) ;(f296,3) ;(f302,3) ;(f310,3) ;(f316,3) ;(f322,3) ;(f328,3) ;(f336,3) ;(f342,3) ;(f348,3) ;(f354,3) ;(f362,3) ;(f368,3) ;(f374,3) ;(f380,3) ;(f388,3) ;(f394,3) ;(f400,3) ;(f406,3) ;(f414,3) ;(f420,3) ;(f426,3) ;(f432,3) ;(f440,3) ;(f446,3) ;(f452,3) ;(f458,3) ;(f466,3) ;(f472,3) ;(f478,3) ;(f484,3) ;(f492,3) ;(f498,3) ;(f504,3) ;(f510,3) ;(f518,3) ;(f524,3) ;(f530,3) ;(f536,3) ;(f544,3) ;(f550,3) ;(f556,3) ;(f562,3) ;(f570,3) ;(f576,3) ;(f582,3) ;(f588,3) ;(f596,3) ;(f602,3) ;(f608,3) ;(f614,3) ;(f622,3) ;(f628,3) ;(f634,3) ;(f640,3) ;(f648,3) ;(f654,3) ;(f660,3) ;(f666,3) ;(f674,3) ;(f680,3) ;(f686,3) ;(f692,3) ;(f700,3) ;(f706,3) ;(f712,3) ;(f718,3) ;(f726,3) ;(f732,3) ;(f738,3) ;(f744,3) ;(f752,3) ;(f758,3) ;(f764,3) ;(f770,3) ;(f778,3) ;(f784,3) ;(f790,3) ;(f796,3) ;(f804,3) ;(f810,3) ;(f816,3) ;(f822,3) ;(f830,3) ;(f836,3) ;(f842,3) ;(f848,3) ;(f856,3) ;(f862,3) ;(f868,3) ;(f874,3) ;(f882,3) ;(f888,3) ;(f894,3) ;(f900,3) ;(f908,3) ;(f914,3) ;(f920,3) ;(f926,3) ;(f934,3)} Flow Graph: [0->{1,240},1->{1,240},2->{2,239},3->{3,238},4->{4,237},5->{5,236},6->{6,235},7->{7,234},8->{8,233},9->{9 ,232},10->{10,231},11->{11,230},12->{12,229},13->{13,228},14->{14,227},15->{15,226},16->{16,225},17->{17 ,224},18->{18,223},19->{19,222},20->{20,221},21->{21,220},22->{22,219},23->{23,218},24->{24,217},25->{25 ,216},26->{26,215},27->{27,214},28->{28,213},29->{29,212},30->{30,211},31->{31,210},32->{32,209},33->{33 ,208},34->{34,207},35->{35,206},36->{36,205},37->{37,204},38->{38,203},39->{39,202},40->{40,201},41->{41 ,200},42->{42,199},43->{43,198},44->{44,197},45->{45,196},46->{46,195},47->{47,194},48->{48,193},49->{49 ,192},50->{50,191},51->{51,190},52->{52,189},53->{53,188},54->{54,187},55->{55,186},56->{56,185},57->{57 ,184},58->{58,183},59->{59,182},60->{60,181},61->{61,180},62->{62,179},63->{63,178},64->{64,177},65->{65 ,176},66->{66,175},67->{67,174},68->{68,173},69->{69,172},70->{70,171},71->{71,170},72->{72,169},73->{73 ,168},74->{74,167},75->{75,166},76->{76,165},77->{77,164},78->{78,163},79->{79,162},80->{80,161},81->{81 ,160},82->{82,159},83->{83,158},84->{84,157},85->{85,156},86->{86,155},87->{87,154},88->{88,153},89->{89 ,152},90->{90,151},91->{91,150},92->{92,149},93->{93,148},94->{94,147},95->{95,146},96->{96,145},97->{97 ,144},98->{98,143},99->{99,142},100->{100,141},101->{101,140},102->{102,139},103->{103,138},104->{104,137} ,105->{105,136},106->{106,135},107->{107,134},108->{108,133},109->{109,132},110->{110,131},111->{111,130} ,112->{112,129},113->{113,128},114->{114,127},115->{115,126},116->{116,125},117->{117,124},118->{118,123} ,119->{119,122},120->{120,121},121->{},122->{120,121},123->{119,122},124->{118,123},125->{117,124},126->{116 ,125},127->{115,126},128->{114,127},129->{113,128},130->{112,129},131->{111,130},132->{110,131},133->{109 ,132},134->{108,133},135->{107,134},136->{106,135},137->{105,136},138->{104,137},139->{103,138},140->{102 ,139},141->{101,140},142->{100,141},143->{99,142},144->{98,143},145->{97,144},146->{96,145},147->{95,146} ,148->{94,147},149->{93,148},150->{92,149},151->{91,150},152->{90,151},153->{89,152},154->{88,153},155->{87 ,154},156->{86,155},157->{85,156},158->{84,157},159->{83,158},160->{82,159},161->{81,160},162->{80,161} ,163->{79,162},164->{78,163},165->{77,164},166->{76,165},167->{75,166},168->{74,167},169->{73,168},170->{72 ,169},171->{71,170},172->{70,171},173->{69,172},174->{68,173},175->{67,174},176->{66,175},177->{65,176} ,178->{64,177},179->{63,178},180->{62,179},181->{61,180},182->{60,181},183->{59,182},184->{58,183},185->{57 ,184},186->{56,185},187->{55,186},188->{54,187},189->{53,188},190->{52,189},191->{51,190},192->{50,191} ,193->{49,192},194->{48,193},195->{47,194},196->{46,195},197->{45,196},198->{44,197},199->{43,198},200->{42 ,199},201->{41,200},202->{40,201},203->{39,202},204->{38,203},205->{37,204},206->{36,205},207->{35,206} ,208->{34,207},209->{33,208},210->{32,209},211->{31,210},212->{30,211},213->{29,212},214->{28,213},215->{27 ,214},216->{26,215},217->{25,216},218->{24,217},219->{23,218},220->{22,219},221->{21,220},222->{20,221} ,223->{19,222},224->{18,223},225->{17,224},226->{16,225},227->{15,226},228->{14,227},229->{13,228},230->{12 ,229},231->{11,230},232->{10,231},233->{9,232},234->{8,233},235->{7,234},236->{6,235},237->{5,236},238->{4 ,237},239->{3,238},240->{2,239}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C) -> f154(0,2,0) True (1,1) 1. f154(A,B,C) -> f154(A + C,B,1 + C) [2 >= C] (?,1) 2. f160(A,B,C) -> f160(A + C,B,1 + C) [3 >= C] (?,1) 3. f166(A,B,C) -> f166(A + C,B,1 + C) [2 >= C] (?,1) 4. f172(A,B,C) -> f172(A + C,B,1 + C) [3 >= C] (?,1) 5. f180(A,B,C) -> f180(A + C,B,1 + C) [1 >= C] (?,1) 6. f186(A,B,C) -> f186(A + C,B,1 + C) [2 >= C] (?,1) 7. f192(A,B,C) -> f192(A + C,B,1 + C) [1 >= C] (?,1) 8. f198(A,B,C) -> f198(A + C,B,1 + C) [2 >= C] (?,1) 9. f206(A,B,C) -> f206(A + C,B,1 + C) [0 >= 3 + C] (?,1) 10. f212(A,B,C) -> f212(A + C,B,1 + C) [0 >= 2 + C] (?,1) 11. f218(A,B,C) -> f218(A + C,B,1 + C) [0 >= 3 + C] (?,1) 12. f224(A,B,C) -> f224(A + C,B,1 + C) [0 >= 2 + C] (?,1) 13. f232(A,B,C) -> f232(A + C,B,1 + C) [0 >= 2 + C] (?,1) 14. f238(A,B,C) -> f238(A + C,B,1 + C) [0 >= 1 + C] (?,1) 15. f244(A,B,C) -> f244(A + C,B,1 + C) [0 >= 2 + C] (?,1) 16. f250(A,B,C) -> f250(A + C,B,1 + C) [0 >= 1 + C] (?,1) 17. f258(A,B,C) -> f258(A + C,B,1 + C) [0 >= 1 + C] (?,1) 18. f264(A,B,C) -> f264(A + C,B,1 + C) [0 >= C] (?,1) 19. f270(A,B,C) -> f270(A + C,B,1 + C) [0 >= 1 + C] (?,1) 20. f276(A,B,C) -> f276(A + C,B,1 + C) [0 >= C] (?,1) 21. f284(A,B,C) -> f284(A + C,B,1 + C) [3 >= C] (?,1) 22. f290(A,B,C) -> f290(A + C,B,1 + C) [4 >= C] (?,1) 23. f296(A,B,C) -> f296(A + C,B,1 + C) [3 >= C] (?,1) 24. f302(A,B,C) -> f302(A + C,B,1 + C) [4 >= C] (?,1) 25. f310(A,B,C) -> f310(A + C,B,B + C) [2 >= C] (?,1) 26. f316(A,B,C) -> f316(A + C,B,B + C) [3 >= C] (?,1) 27. f322(A,B,C) -> f322(A + C,B,B + C) [2 >= C] (?,1) 28. f328(A,B,C) -> f328(A + C,B,B + C) [3 >= C] (?,1) 29. f336(A,B,C) -> f336(A + C,B,B + C) [1 >= C] (?,1) 30. f342(A,B,C) -> f342(A + C,B,B + C) [2 >= C] (?,1) 31. f348(A,B,C) -> f348(A + C,B,B + C) [1 >= C] (?,1) 32. f354(A,B,C) -> f354(A + C,B,B + C) [2 >= C] (?,1) 33. f362(A,B,C) -> f362(A + C,B,B + C) [0 >= 3 + C] (?,1) 34. f368(A,B,C) -> f368(A + C,B,B + C) [0 >= 2 + C] (?,1) 35. f374(A,B,C) -> f374(A + C,B,B + C) [0 >= 3 + C] (?,1) 36. f380(A,B,C) -> f380(A + C,B,B + C) [0 >= 2 + C] (?,1) 37. f388(A,B,C) -> f388(A + C,B,B + C) [0 >= 2 + C] (?,1) 38. f394(A,B,C) -> f394(A + C,B,B + C) [0 >= 1 + C] (?,1) 39. f400(A,B,C) -> f400(A + C,B,B + C) [0 >= 2 + C] (?,1) 40. f406(A,B,C) -> f406(A + C,B,B + C) [0 >= 1 + C] (?,1) 41. f414(A,B,C) -> f414(A + C,B,B + C) [0 >= 1 + C] (?,1) 42. f420(A,B,C) -> f420(A + C,B,B + C) [0 >= C] (?,1) 43. f426(A,B,C) -> f426(A + C,B,B + C) [0 >= 1 + C] (?,1) 44. f432(A,B,C) -> f432(A + C,B,B + C) [0 >= C] (?,1) 45. f440(A,B,C) -> f440(A + C,B,B + C) [3 >= C] (?,1) 46. f446(A,B,C) -> f446(A + C,B,B + C) [4 >= C] (?,1) 47. f452(A,B,C) -> f452(A + C,B,B + C) [3 >= C] (?,1) 48. f458(A,B,C) -> f458(A + C,B,B + C) [4 >= C] (?,1) 49. f466(A,B,C) -> f466(A + C,B,-1 + C) [C >= 3] (?,1) 50. f472(A,B,C) -> f472(A + C,B,-1 + C) [C >= 2] (?,1) 51. f478(A,B,C) -> f478(A + C,B,-1 + C) [C >= 3] (?,1) 52. f484(A,B,C) -> f484(A + C,B,-1 + C) [C >= 2] (?,1) 53. f492(A,B,C) -> f492(A + C,B,-1 + C) [C >= 2] (?,1) 54. f498(A,B,C) -> f498(A + C,B,-1 + C) [C >= 1] (?,1) 55. f504(A,B,C) -> f504(A + C,B,-1 + C) [C >= 2] (?,1) 56. f510(A,B,C) -> f510(A + C,B,-1 + C) [C >= 1] (?,1) 57. f518(A,B,C) -> f518(A + C,B,-1 + C) [C >= 1] (?,1) 58. f524(A,B,C) -> f524(A + C,B,-1 + C) [C >= 0] (?,1) 59. f530(A,B,C) -> f530(A + C,B,-1 + C) [C >= 1] (?,1) 60. f536(A,B,C) -> f536(A + C,B,-1 + C) [C >= 0] (?,1) 61. f544(A,B,C) -> f544(A + C,B,-1 + C) [C >= 0] (?,1) 62. f550(A,B,C) -> f550(A + C,B,-1 + C) [1 + C >= 0] (?,1) 63. f556(A,B,C) -> f556(A + C,B,-1 + C) [C >= 0] (?,1) 64. f562(A,B,C) -> f562(A + C,B,-1 + C) [1 + C >= 0] (?,1) 65. f570(A,B,C) -> f570(A + C,B,-1 + C) [1 + C >= 0] (?,1) 66. f576(A,B,C) -> f576(A + C,B,-1 + C) [2 + C >= 0] (?,1) 67. f582(A,B,C) -> f582(A + C,B,-1 + C) [1 + C >= 0] (?,1) 68. f588(A,B,C) -> f588(A + C,B,-1 + C) [2 + C >= 0] (?,1) 69. f596(A,B,C) -> f596(A + C,B,-1 + C) [2 + C >= 0] (?,1) 70. f602(A,B,C) -> f602(A + C,B,-1 + C) [3 + C >= 0] (?,1) 71. f608(A,B,C) -> f608(A + C,B,-1 + C) [2 + C >= 0] (?,1) 72. f614(A,B,C) -> f614(A + C,B,-1 + C) [3 + C >= 0] (?,1) 73. f622(A,B,C) -> f622(A + C,B,-1 + C) [4 + C >= 0] (?,1) 74. f628(A,B,C) -> f628(A + C,B,-1 + C) [5 + C >= 0] (?,1) 75. f634(A,B,C) -> f634(A + C,B,-1 + C) [4 + C >= 0] (?,1) 76. f640(A,B,C) -> f640(A + C,B,-1 + C) [5 + C >= 0] (?,1) 77. f648(A,B,C) -> f648(A + C,B,-1 + C) [6 + C >= 0] (?,1) 78. f654(A,B,C) -> f654(A + C,B,-1 + C) [7 + C >= 0] (?,1) 79. f660(A,B,C) -> f660(A + C,B,-1 + C) [6 + C >= 0] (?,1) 80. f666(A,B,C) -> f666(A + C,B,-1 + C) [7 + C >= 0] (?,1) 81. f674(A,B,C) -> f674(A + C,B,-1 + C) [7 + C >= 0] (?,1) 82. f680(A,B,C) -> f680(A + C,B,-1 + C) [8 + C >= 0] (?,1) 83. f686(A,B,C) -> f686(A + C,B,-1 + C) [7 + C >= 0] (?,1) 84. f692(A,B,C) -> f692(A + C,B,-1 + C) [8 + C >= 0] (?,1) 85. f700(A,B,C) -> f700(A + C,B,-1*B + C) [C >= 3] (?,1) 86. f706(A,B,C) -> f706(A + C,B,-1*B + C) [C >= 2] (?,1) 87. f712(A,B,C) -> f712(A + C,B,-1*B + C) [C >= 3] (?,1) 88. f718(A,B,C) -> f718(A + C,B,-1*B + C) [C >= 2] (?,1) 89. f726(A,B,C) -> f726(A + C,B,-1*B + C) [C >= 2] (?,1) 90. f732(A,B,C) -> f732(A + C,B,-1*B + C) [C >= 1] (?,1) 91. f738(A,B,C) -> f738(A + C,B,-1*B + C) [C >= 2] (?,1) 92. f744(A,B,C) -> f744(A + C,B,-1*B + C) [C >= 1] (?,1) 93. f752(A,B,C) -> f752(A + C,B,-1*B + C) [C >= 1] (?,1) 94. f758(A,B,C) -> f758(A + C,B,-1*B + C) [C >= 0] (?,1) 95. f764(A,B,C) -> f764(A + C,B,-1*B + C) [C >= 1] (?,1) 96. f770(A,B,C) -> f770(A + C,B,-1*B + C) [C >= 0] (?,1) 97. f778(A,B,C) -> f778(A + C,B,-1*B + C) [C >= 0] (?,1) 98. f784(A,B,C) -> f784(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 99. f790(A,B,C) -> f790(A + C,B,-1*B + C) [C >= 0] (?,1) 100. f796(A,B,C) -> f796(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 101. f804(A,B,C) -> f804(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 102. f810(A,B,C) -> f810(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 103. f816(A,B,C) -> f816(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 104. f822(A,B,C) -> f822(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 105. f830(A,B,C) -> f830(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 106. f836(A,B,C) -> f836(A + C,B,-1*B + C) [3 + C >= 0] (?,1) 107. f842(A,B,C) -> f842(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 108. f848(A,B,C) -> f848(A + C,B,-1*B + C) [3 + C >= 0] (?,1) 109. f856(A,B,C) -> f856(A + C,B,-1*B + C) [4 + C >= 0] (?,1) 110. f862(A,B,C) -> f862(A + C,B,-1*B + C) [5 + C >= 0] (?,1) 111. f868(A,B,C) -> f868(A + C,B,-1*B + C) [4 + C >= 0] (?,1) 112. f874(A,B,C) -> f874(A + C,B,-1*B + C) [5 + C >= 0] (?,1) 113. f882(A,B,C) -> f882(A + C,B,-1*B + C) [6 + C >= 0] (?,1) 114. f888(A,B,C) -> f888(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 115. f894(A,B,C) -> f894(A + C,B,-1*B + C) [6 + C >= 0] (?,1) 116. f900(A,B,C) -> f900(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 117. f908(A,B,C) -> f908(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 118. f914(A,B,C) -> f914(A + C,B,-1*B + C) [8 + C >= 0] (?,1) 119. f920(A,B,C) -> f920(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 120. f926(A,B,C) -> f926(A + C,B,-1*B + C) [8 + C >= 0] (?,1) 121. f926(A,B,C) -> f934(A,B,C) [0 >= 9 + C] (1,1) 122. f920(A,B,C) -> f926(A,B,16) [0 >= 8 + C] (1,1) 123. f914(A,B,C) -> f920(A,B,16) [0 >= 9 + C] (1,1) 124. f908(A,B,C) -> f914(A,B,16) [0 >= 8 + C] (1,1) 125. f900(A,B,C) -> f908(A,B,16) [0 >= 8 + C] (1,1) 126. f894(A,B,C) -> f900(A,B,-2) [0 >= 7 + C] (1,1) 127. f888(A,B,C) -> f894(A,B,-2) [0 >= 8 + C] (1,1) 128. f882(A,B,C) -> f888(A,B,-2) [0 >= 7 + C] (1,1) 129. f874(A,B,C) -> f882(A,B,-2) [0 >= 6 + C] (1,1) 130. f868(A,B,C) -> f874(A,B,-1) [0 >= 5 + C] (1,1) 131. f862(A,B,C) -> f868(A,B,-1) [0 >= 6 + C] (1,1) 132. f856(A,B,C) -> f862(A,B,-1) [0 >= 5 + C] (1,1) 133. f848(A,B,C) -> f856(A,B,-1) [0 >= 4 + C] (1,1) 134. f842(A,B,C) -> f848(A,B,0) [0 >= 3 + C] (1,1) 135. f836(A,B,C) -> f842(A,B,0) [0 >= 4 + C] (1,1) 136. f830(A,B,C) -> f836(A,B,0) [0 >= 3 + C] (1,1) 137. f822(A,B,C) -> f830(A,B,0) [0 >= 3 + C] (1,1) 138. f816(A,B,C) -> f822(A,B,9) [0 >= 2 + C] (1,1) 139. f810(A,B,C) -> f816(A,B,9) [0 >= 3 + C] (1,1) 140. f804(A,B,C) -> f810(A,B,9) [0 >= 2 + C] (1,1) 141. f796(A,B,C) -> f804(A,B,9) [0 >= 2 + C] (1,1) 142. f790(A,B,C) -> f796(A,B,8) [0 >= 1 + C] (1,1) 143. f784(A,B,C) -> f790(A,B,8) [0 >= 2 + C] (1,1) 144. f778(A,B,C) -> f784(A,B,8) [0 >= 1 + C] (1,1) 145. f770(A,B,C) -> f778(A,B,8) [0 >= 1 + C] (1,1) 146. f764(A,B,C) -> f770(A,B,7) [0 >= C] (1,1) 147. f758(A,B,C) -> f764(A,B,7) [0 >= 1 + C] (1,1) 148. f752(A,B,C) -> f758(A,B,7) [0 >= C] (1,1) 149. f744(A,B,C) -> f752(A,B,7) [0 >= C] (1,1) 150. f738(A,B,C) -> f744(A,B,6) [1 >= C] (1,1) 151. f732(A,B,C) -> f738(A,B,6) [0 >= C] (1,1) 152. f726(A,B,C) -> f732(A,B,6) [1 >= C] (1,1) 153. f718(A,B,C) -> f726(A,B,6) [1 >= C] (1,1) 154. f712(A,B,C) -> f718(A,B,5) [2 >= C] (1,1) 155. f706(A,B,C) -> f712(A,B,5) [1 >= C] (1,1) 156. f700(A,B,C) -> f706(A,B,5) [2 >= C] (1,1) 157. f692(A,B,C) -> f700(A,B,5) [0 >= 9 + C] (1,1) 158. f686(A,B,C) -> f692(A,B,16) [0 >= 8 + C] (1,1) 159. f680(A,B,C) -> f686(A,B,16) [0 >= 9 + C] (1,1) 160. f674(A,B,C) -> f680(A,B,16) [0 >= 8 + C] (1,1) 161. f666(A,B,C) -> f674(A,B,16) [0 >= 8 + C] (1,1) 162. f660(A,B,C) -> f666(A,B,-2) [0 >= 7 + C] (1,1) 163. f654(A,B,C) -> f660(A,B,-2) [0 >= 8 + C] (1,1) 164. f648(A,B,C) -> f654(A,B,-2) [0 >= 7 + C] (1,1) 165. f640(A,B,C) -> f648(A,B,-2) [0 >= 6 + C] (1,1) 166. f634(A,B,C) -> f640(A,B,-1) [0 >= 5 + C] (1,1) 167. f628(A,B,C) -> f634(A,B,-1) [0 >= 6 + C] (1,1) 168. f622(A,B,C) -> f628(A,B,-1) [0 >= 5 + C] (1,1) 169. f614(A,B,C) -> f622(A,B,-1) [0 >= 4 + C] (1,1) 170. f608(A,B,C) -> f614(A,B,0) [0 >= 3 + C] (1,1) 171. f602(A,B,C) -> f608(A,B,0) [0 >= 4 + C] (1,1) 172. f596(A,B,C) -> f602(A,B,0) [0 >= 3 + C] (1,1) 173. f588(A,B,C) -> f596(A,B,0) [0 >= 3 + C] (1,1) 174. f582(A,B,C) -> f588(A,B,9) [0 >= 2 + C] (1,1) 175. f576(A,B,C) -> f582(A,B,9) [0 >= 3 + C] (1,1) 176. f570(A,B,C) -> f576(A,B,9) [0 >= 2 + C] (1,1) 177. f562(A,B,C) -> f570(A,B,9) [0 >= 2 + C] (1,1) 178. f556(A,B,C) -> f562(A,B,8) [0 >= 1 + C] (1,1) 179. f550(A,B,C) -> f556(A,B,8) [0 >= 2 + C] (1,1) 180. f544(A,B,C) -> f550(A,B,8) [0 >= 1 + C] (1,1) 181. f536(A,B,C) -> f544(A,B,8) [0 >= 1 + C] (1,1) 182. f530(A,B,C) -> f536(A,B,7) [0 >= C] (1,1) 183. f524(A,B,C) -> f530(A,B,7) [0 >= 1 + C] (1,1) 184. f518(A,B,C) -> f524(A,B,7) [0 >= C] (1,1) 185. f510(A,B,C) -> f518(A,B,7) [0 >= C] (1,1) 186. f504(A,B,C) -> f510(A,B,6) [1 >= C] (1,1) 187. f498(A,B,C) -> f504(A,B,6) [0 >= C] (1,1) 188. f492(A,B,C) -> f498(A,B,6) [1 >= C] (1,1) 189. f484(A,B,C) -> f492(A,B,6) [1 >= C] (1,1) 190. f478(A,B,C) -> f484(A,B,5) [2 >= C] (1,1) 191. f472(A,B,C) -> f478(A,B,5) [1 >= C] (1,1) 192. f466(A,B,C) -> f472(A,B,5) [2 >= C] (1,1) 193. f458(A,B,C) -> f466(A,B,5) [C >= 5] (1,1) 194. f452(A,B,C) -> f458(A,B,-6) [C >= 4] (1,1) 195. f446(A,B,C) -> f452(A,B,-6) [C >= 5] (1,1) 196. f440(A,B,C) -> f446(A,B,-6) [C >= 4] (1,1) 197. f432(A,B,C) -> f440(A,B,-6) [C >= 1] (1,1) 198. f426(A,B,C) -> f432(A,B,-5) [C >= 0] (1,1) 199. f420(A,B,C) -> f426(A,B,-5) [C >= 1] (1,1) 200. f414(A,B,C) -> f420(A,B,-5) [C >= 0] (1,1) 201. f406(A,B,C) -> f414(A,B,-5) [C >= 0] (1,1) 202. f400(A,B,C) -> f406(A,B,-4) [1 + C >= 0] (1,1) 203. f394(A,B,C) -> f400(A,B,-4) [C >= 0] (1,1) 204. f388(A,B,C) -> f394(A,B,-4) [1 + C >= 0] (1,1) 205. f380(A,B,C) -> f388(A,B,-4) [1 + C >= 0] (1,1) 206. f374(A,B,C) -> f380(A,B,-3) [2 + C >= 0] (1,1) 207. f368(A,B,C) -> f374(A,B,-3) [1 + C >= 0] (1,1) 208. f362(A,B,C) -> f368(A,B,-3) [2 + C >= 0] (1,1) 209. f354(A,B,C) -> f362(A,B,-3) [C >= 3] (1,1) 210. f348(A,B,C) -> f354(A,B,1) [C >= 2] (1,1) 211. f342(A,B,C) -> f348(A,B,1) [C >= 3] (1,1) 212. f336(A,B,C) -> f342(A,B,1) [C >= 2] (1,1) 213. f328(A,B,C) -> f336(A,B,1) [C >= 4] (1,1) 214. f322(A,B,C) -> f328(A,B,0) [C >= 3] (1,1) 215. f316(A,B,C) -> f322(A,B,0) [C >= 4] (1,1) 216. f310(A,B,C) -> f316(A,B,0) [C >= 3] (1,1) 217. f302(A,B,C) -> f310(A,B,0) [C >= 5] (1,1) 218. f296(A,B,C) -> f302(A,B,-6) [C >= 4] (1,1) 219. f290(A,B,C) -> f296(A,B,-6) [C >= 5] (1,1) 220. f284(A,B,C) -> f290(A,B,-6) [C >= 4] (1,1) 221. f276(A,B,C) -> f284(A,B,-6) [C >= 1] (1,1) 222. f270(A,B,C) -> f276(A,B,-5) [C >= 0] (1,1) 223. f264(A,B,C) -> f270(A,B,-5) [C >= 1] (1,1) 224. f258(A,B,C) -> f264(A,B,-5) [C >= 0] (1,1) 225. f250(A,B,C) -> f258(A,B,-5) [C >= 0] (1,1) 226. f244(A,B,C) -> f250(A,B,-4) [1 + C >= 0] (1,1) 227. f238(A,B,C) -> f244(A,B,-4) [C >= 0] (1,1) 228. f232(A,B,C) -> f238(A,B,-4) [1 + C >= 0] (1,1) 229. f224(A,B,C) -> f232(A,B,-4) [1 + C >= 0] (1,1) 230. f218(A,B,C) -> f224(A,B,-3) [2 + C >= 0] (1,1) 231. f212(A,B,C) -> f218(A,B,-3) [1 + C >= 0] (1,1) 232. f206(A,B,C) -> f212(A,B,-3) [2 + C >= 0] (1,1) 233. f198(A,B,C) -> f206(A,B,-3) [C >= 3] (1,1) 234. f192(A,B,C) -> f198(A,B,1) [C >= 2] (1,1) 235. f186(A,B,C) -> f192(A,B,1) [C >= 3] (1,1) 236. f180(A,B,C) -> f186(A,B,1) [C >= 2] (1,1) 237. f172(A,B,C) -> f180(A,B,1) [C >= 4] (1,1) 238. f166(A,B,C) -> f172(A,B,0) [C >= 3] (1,1) 239. f160(A,B,C) -> f166(A,B,0) [C >= 4] (1,1) 240. f154(A,B,C) -> f160(A,B,0) [C >= 3] (1,1) Signature: {(f0,3) ;(f154,3) ;(f160,3) ;(f166,3) ;(f172,3) ;(f180,3) ;(f186,3) ;(f192,3) ;(f198,3) ;(f206,3) ;(f212,3) ;(f218,3) ;(f224,3) ;(f232,3) ;(f238,3) ;(f244,3) ;(f250,3) ;(f258,3) ;(f264,3) ;(f270,3) ;(f276,3) ;(f284,3) ;(f290,3) ;(f296,3) ;(f302,3) ;(f310,3) ;(f316,3) ;(f322,3) ;(f328,3) ;(f336,3) ;(f342,3) ;(f348,3) ;(f354,3) ;(f362,3) ;(f368,3) ;(f374,3) ;(f380,3) ;(f388,3) ;(f394,3) ;(f400,3) ;(f406,3) ;(f414,3) ;(f420,3) ;(f426,3) ;(f432,3) ;(f440,3) ;(f446,3) ;(f452,3) ;(f458,3) ;(f466,3) ;(f472,3) ;(f478,3) ;(f484,3) ;(f492,3) ;(f498,3) ;(f504,3) ;(f510,3) ;(f518,3) ;(f524,3) ;(f530,3) ;(f536,3) ;(f544,3) ;(f550,3) ;(f556,3) ;(f562,3) ;(f570,3) ;(f576,3) ;(f582,3) ;(f588,3) ;(f596,3) ;(f602,3) ;(f608,3) ;(f614,3) ;(f622,3) ;(f628,3) ;(f634,3) ;(f640,3) ;(f648,3) ;(f654,3) ;(f660,3) ;(f666,3) ;(f674,3) ;(f680,3) ;(f686,3) ;(f692,3) ;(f700,3) ;(f706,3) ;(f712,3) ;(f718,3) ;(f726,3) ;(f732,3) ;(f738,3) ;(f744,3) ;(f752,3) ;(f758,3) ;(f764,3) ;(f770,3) ;(f778,3) ;(f784,3) ;(f790,3) ;(f796,3) ;(f804,3) ;(f810,3) ;(f816,3) ;(f822,3) ;(f830,3) ;(f836,3) ;(f842,3) ;(f848,3) ;(f856,3) ;(f862,3) ;(f868,3) ;(f874,3) ;(f882,3) ;(f888,3) ;(f894,3) ;(f900,3) ;(f908,3) ;(f914,3) ;(f920,3) ;(f926,3) ;(f934,3)} Flow Graph: [0->{1,240},1->{1,240},2->{2,239},3->{3,238},4->{4,237},5->{5,236},6->{6,235},7->{7,234},8->{8,233},9->{9 ,232},10->{10,231},11->{11,230},12->{12,229},13->{13,228},14->{14,227},15->{15,226},16->{16,225},17->{17 ,224},18->{18,223},19->{19,222},20->{20,221},21->{21,220},22->{22,219},23->{23,218},24->{24,217},25->{25 ,216},26->{26,215},27->{27,214},28->{28,213},29->{29,212},30->{30,211},31->{31,210},32->{32,209},33->{33 ,208},34->{34,207},35->{35,206},36->{36,205},37->{37,204},38->{38,203},39->{39,202},40->{40,201},41->{41 ,200},42->{42,199},43->{43,198},44->{44,197},45->{45,196},46->{46,195},47->{47,194},48->{48,193},49->{49 ,192},50->{50,191},51->{51,190},52->{52,189},53->{53,188},54->{54,187},55->{55,186},56->{56,185},57->{57 ,184},58->{58,183},59->{59,182},60->{60,181},61->{61,180},62->{62,179},63->{63,178},64->{64,177},65->{65 ,176},66->{66,175},67->{67,174},68->{68,173},69->{69,172},70->{70,171},71->{71,170},72->{72,169},73->{73 ,168},74->{74,167},75->{75,166},76->{76,165},77->{77,164},78->{78,163},79->{79,162},80->{80,161},81->{81 ,160},82->{82,159},83->{83,158},84->{84,157},85->{85,156},86->{86,155},87->{87,154},88->{88,153},89->{89 ,152},90->{90,151},91->{91,150},92->{92,149},93->{93,148},94->{94,147},95->{95,146},96->{96,145},97->{97 ,144},98->{98,143},99->{99,142},100->{100,141},101->{101,140},102->{102,139},103->{103,138},104->{104,137} ,105->{105,136},106->{106,135},107->{107,134},108->{108,133},109->{109,132},110->{110,131},111->{111,130} ,112->{112,129},113->{113,128},114->{114,127},115->{115,126},116->{116,125},117->{117,124},118->{118,123} ,119->{119,122},120->{120,121},121->{},122->{120,121},123->{119,122},124->{118,123},125->{117,124},126->{116 ,125},127->{115,126},128->{114,127},129->{113,128},130->{112,129},131->{111,130},132->{110,131},133->{109 ,132},134->{108,133},135->{107,134},136->{106,135},137->{105,136},138->{104,137},139->{103,138},140->{102 ,139},141->{101,140},142->{100,141},143->{99,142},144->{98,143},145->{97,144},146->{96,145},147->{95,146} ,148->{94,147},149->{93,148},150->{92,149},151->{91,150},152->{90,151},153->{89,152},154->{88,153},155->{87 ,154},156->{86,155},157->{85,156},158->{84,157},159->{83,158},160->{82,159},161->{81,160},162->{80,161} ,163->{79,162},164->{78,163},165->{77,164},166->{76,165},167->{75,166},168->{74,167},169->{73,168},170->{72 ,169},171->{71,170},172->{70,171},173->{69,172},174->{68,173},175->{67,174},176->{66,175},177->{65,176} ,178->{64,177},179->{63,178},180->{62,179},181->{61,180},182->{60,181},183->{59,182},184->{58,183},185->{57 ,184},186->{56,185},187->{55,186},188->{54,187},189->{53,188},190->{52,189},191->{51,190},192->{50,191} ,193->{49,192},194->{48,193},195->{47,194},196->{46,195},197->{45,196},198->{44,197},199->{43,198},200->{42 ,199},201->{41,200},202->{40,201},203->{39,202},204->{38,203},205->{37,204},206->{36,205},207->{35,206} ,208->{34,207},209->{33,208},210->{32,209},211->{31,210},212->{30,211},213->{29,212},214->{28,213},215->{27 ,214},216->{26,215},217->{25,216},218->{24,217},219->{23,218},220->{22,219},221->{21,220},222->{20,221} ,223->{19,222},224->{18,223},225->{17,224},226->{16,225},227->{15,226},228->{14,227},229->{13,228},230->{12 ,229},231->{11,230},232->{10,231},233->{9,232},234->{8,233},235->{7,234},236->{6,235},237->{5,236},238->{4 ,237},239->{3,238},240->{2,239}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,240) ,(122,121) ,(123,122) ,(124,123) ,(125,124) ,(126,125) ,(127,126) ,(128,127) ,(129,128) ,(130,129) ,(131,130) ,(132,131) ,(133,132) ,(134,133) ,(135,134) ,(136,135) ,(137,136) ,(138,137) ,(139,138) ,(140,139) ,(141,140) ,(142,141) ,(143,142) ,(144,143) ,(145,144) ,(146,145) ,(147,146) ,(148,147) ,(149,148) ,(150,149) ,(151,150) ,(152,151) ,(153,152) ,(154,153) ,(155,154) ,(156,155) ,(157,156) ,(158,157) ,(159,158) ,(160,159) ,(161,160) ,(162,161) ,(163,162) ,(164,163) ,(165,164) ,(166,165) ,(167,166) ,(168,167) ,(169,168) ,(170,169) ,(171,170) ,(172,171) ,(173,172) ,(174,173) ,(175,174) ,(176,175) ,(177,176) ,(178,177) ,(179,178) ,(180,179) ,(181,180) ,(182,181) ,(183,182) ,(184,183) ,(185,184) ,(186,185) ,(187,186) ,(188,187) ,(189,188) ,(190,189) ,(191,190) ,(192,191) ,(193,192) ,(194,193) ,(195,194) ,(196,195) ,(197,196) ,(198,197) ,(199,198) ,(200,199) ,(201,200) ,(202,201) ,(203,202) ,(204,203) ,(205,204) ,(206,205) ,(207,206) ,(208,207) ,(209,208) ,(210,209) ,(211,210) ,(212,211) ,(213,212) ,(214,213) ,(215,214) ,(216,215) ,(217,216) ,(218,217) ,(219,218) ,(220,219) ,(221,220) ,(222,221) ,(223,222) ,(224,223) ,(225,224) ,(226,225) ,(227,226) ,(228,227) ,(229,228) ,(230,229) ,(231,230) ,(232,231) ,(233,232) ,(234,233) ,(235,234) ,(236,235) ,(237,236) ,(238,237) ,(239,238) ,(240,239)] * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. f0(A,B,C) -> f154(0,2,0) True (1,1) 1. f154(A,B,C) -> f154(A + C,B,1 + C) [2 >= C] (?,1) 2. f160(A,B,C) -> f160(A + C,B,1 + C) [3 >= C] (?,1) 3. f166(A,B,C) -> f166(A + C,B,1 + C) [2 >= C] (?,1) 4. f172(A,B,C) -> f172(A + C,B,1 + C) [3 >= C] (?,1) 5. f180(A,B,C) -> f180(A + C,B,1 + C) [1 >= C] (?,1) 6. f186(A,B,C) -> f186(A + C,B,1 + C) [2 >= C] (?,1) 7. f192(A,B,C) -> f192(A + C,B,1 + C) [1 >= C] (?,1) 8. f198(A,B,C) -> f198(A + C,B,1 + C) [2 >= C] (?,1) 9. f206(A,B,C) -> f206(A + C,B,1 + C) [0 >= 3 + C] (?,1) 10. f212(A,B,C) -> f212(A + C,B,1 + C) [0 >= 2 + C] (?,1) 11. f218(A,B,C) -> f218(A + C,B,1 + C) [0 >= 3 + C] (?,1) 12. f224(A,B,C) -> f224(A + C,B,1 + C) [0 >= 2 + C] (?,1) 13. f232(A,B,C) -> f232(A + C,B,1 + C) [0 >= 2 + C] (?,1) 14. f238(A,B,C) -> f238(A + C,B,1 + C) [0 >= 1 + C] (?,1) 15. f244(A,B,C) -> f244(A + C,B,1 + C) [0 >= 2 + C] (?,1) 16. f250(A,B,C) -> f250(A + C,B,1 + C) [0 >= 1 + C] (?,1) 17. f258(A,B,C) -> f258(A + C,B,1 + C) [0 >= 1 + C] (?,1) 18. f264(A,B,C) -> f264(A + C,B,1 + C) [0 >= C] (?,1) 19. f270(A,B,C) -> f270(A + C,B,1 + C) [0 >= 1 + C] (?,1) 20. f276(A,B,C) -> f276(A + C,B,1 + C) [0 >= C] (?,1) 21. f284(A,B,C) -> f284(A + C,B,1 + C) [3 >= C] (?,1) 22. f290(A,B,C) -> f290(A + C,B,1 + C) [4 >= C] (?,1) 23. f296(A,B,C) -> f296(A + C,B,1 + C) [3 >= C] (?,1) 24. f302(A,B,C) -> f302(A + C,B,1 + C) [4 >= C] (?,1) 25. f310(A,B,C) -> f310(A + C,B,B + C) [2 >= C] (?,1) 26. f316(A,B,C) -> f316(A + C,B,B + C) [3 >= C] (?,1) 27. f322(A,B,C) -> f322(A + C,B,B + C) [2 >= C] (?,1) 28. f328(A,B,C) -> f328(A + C,B,B + C) [3 >= C] (?,1) 29. f336(A,B,C) -> f336(A + C,B,B + C) [1 >= C] (?,1) 30. f342(A,B,C) -> f342(A + C,B,B + C) [2 >= C] (?,1) 31. f348(A,B,C) -> f348(A + C,B,B + C) [1 >= C] (?,1) 32. f354(A,B,C) -> f354(A + C,B,B + C) [2 >= C] (?,1) 33. f362(A,B,C) -> f362(A + C,B,B + C) [0 >= 3 + C] (?,1) 34. f368(A,B,C) -> f368(A + C,B,B + C) [0 >= 2 + C] (?,1) 35. f374(A,B,C) -> f374(A + C,B,B + C) [0 >= 3 + C] (?,1) 36. f380(A,B,C) -> f380(A + C,B,B + C) [0 >= 2 + C] (?,1) 37. f388(A,B,C) -> f388(A + C,B,B + C) [0 >= 2 + C] (?,1) 38. f394(A,B,C) -> f394(A + C,B,B + C) [0 >= 1 + C] (?,1) 39. f400(A,B,C) -> f400(A + C,B,B + C) [0 >= 2 + C] (?,1) 40. f406(A,B,C) -> f406(A + C,B,B + C) [0 >= 1 + C] (?,1) 41. f414(A,B,C) -> f414(A + C,B,B + C) [0 >= 1 + C] (?,1) 42. f420(A,B,C) -> f420(A + C,B,B + C) [0 >= C] (?,1) 43. f426(A,B,C) -> f426(A + C,B,B + C) [0 >= 1 + C] (?,1) 44. f432(A,B,C) -> f432(A + C,B,B + C) [0 >= C] (?,1) 45. f440(A,B,C) -> f440(A + C,B,B + C) [3 >= C] (?,1) 46. f446(A,B,C) -> f446(A + C,B,B + C) [4 >= C] (?,1) 47. f452(A,B,C) -> f452(A + C,B,B + C) [3 >= C] (?,1) 48. f458(A,B,C) -> f458(A + C,B,B + C) [4 >= C] (?,1) 49. f466(A,B,C) -> f466(A + C,B,-1 + C) [C >= 3] (?,1) 50. f472(A,B,C) -> f472(A + C,B,-1 + C) [C >= 2] (?,1) 51. f478(A,B,C) -> f478(A + C,B,-1 + C) [C >= 3] (?,1) 52. f484(A,B,C) -> f484(A + C,B,-1 + C) [C >= 2] (?,1) 53. f492(A,B,C) -> f492(A + C,B,-1 + C) [C >= 2] (?,1) 54. f498(A,B,C) -> f498(A + C,B,-1 + C) [C >= 1] (?,1) 55. f504(A,B,C) -> f504(A + C,B,-1 + C) [C >= 2] (?,1) 56. f510(A,B,C) -> f510(A + C,B,-1 + C) [C >= 1] (?,1) 57. f518(A,B,C) -> f518(A + C,B,-1 + C) [C >= 1] (?,1) 58. f524(A,B,C) -> f524(A + C,B,-1 + C) [C >= 0] (?,1) 59. f530(A,B,C) -> f530(A + C,B,-1 + C) [C >= 1] (?,1) 60. f536(A,B,C) -> f536(A + C,B,-1 + C) [C >= 0] (?,1) 61. f544(A,B,C) -> f544(A + C,B,-1 + C) [C >= 0] (?,1) 62. f550(A,B,C) -> f550(A + C,B,-1 + C) [1 + C >= 0] (?,1) 63. f556(A,B,C) -> f556(A + C,B,-1 + C) [C >= 0] (?,1) 64. f562(A,B,C) -> f562(A + C,B,-1 + C) [1 + C >= 0] (?,1) 65. f570(A,B,C) -> f570(A + C,B,-1 + C) [1 + C >= 0] (?,1) 66. f576(A,B,C) -> f576(A + C,B,-1 + C) [2 + C >= 0] (?,1) 67. f582(A,B,C) -> f582(A + C,B,-1 + C) [1 + C >= 0] (?,1) 68. f588(A,B,C) -> f588(A + C,B,-1 + C) [2 + C >= 0] (?,1) 69. f596(A,B,C) -> f596(A + C,B,-1 + C) [2 + C >= 0] (?,1) 70. f602(A,B,C) -> f602(A + C,B,-1 + C) [3 + C >= 0] (?,1) 71. f608(A,B,C) -> f608(A + C,B,-1 + C) [2 + C >= 0] (?,1) 72. f614(A,B,C) -> f614(A + C,B,-1 + C) [3 + C >= 0] (?,1) 73. f622(A,B,C) -> f622(A + C,B,-1 + C) [4 + C >= 0] (?,1) 74. f628(A,B,C) -> f628(A + C,B,-1 + C) [5 + C >= 0] (?,1) 75. f634(A,B,C) -> f634(A + C,B,-1 + C) [4 + C >= 0] (?,1) 76. f640(A,B,C) -> f640(A + C,B,-1 + C) [5 + C >= 0] (?,1) 77. f648(A,B,C) -> f648(A + C,B,-1 + C) [6 + C >= 0] (?,1) 78. f654(A,B,C) -> f654(A + C,B,-1 + C) [7 + C >= 0] (?,1) 79. f660(A,B,C) -> f660(A + C,B,-1 + C) [6 + C >= 0] (?,1) 80. f666(A,B,C) -> f666(A + C,B,-1 + C) [7 + C >= 0] (?,1) 81. f674(A,B,C) -> f674(A + C,B,-1 + C) [7 + C >= 0] (?,1) 82. f680(A,B,C) -> f680(A + C,B,-1 + C) [8 + C >= 0] (?,1) 83. f686(A,B,C) -> f686(A + C,B,-1 + C) [7 + C >= 0] (?,1) 84. f692(A,B,C) -> f692(A + C,B,-1 + C) [8 + C >= 0] (?,1) 85. f700(A,B,C) -> f700(A + C,B,-1*B + C) [C >= 3] (?,1) 86. f706(A,B,C) -> f706(A + C,B,-1*B + C) [C >= 2] (?,1) 87. f712(A,B,C) -> f712(A + C,B,-1*B + C) [C >= 3] (?,1) 88. f718(A,B,C) -> f718(A + C,B,-1*B + C) [C >= 2] (?,1) 89. f726(A,B,C) -> f726(A + C,B,-1*B + C) [C >= 2] (?,1) 90. f732(A,B,C) -> f732(A + C,B,-1*B + C) [C >= 1] (?,1) 91. f738(A,B,C) -> f738(A + C,B,-1*B + C) [C >= 2] (?,1) 92. f744(A,B,C) -> f744(A + C,B,-1*B + C) [C >= 1] (?,1) 93. f752(A,B,C) -> f752(A + C,B,-1*B + C) [C >= 1] (?,1) 94. f758(A,B,C) -> f758(A + C,B,-1*B + C) [C >= 0] (?,1) 95. f764(A,B,C) -> f764(A + C,B,-1*B + C) [C >= 1] (?,1) 96. f770(A,B,C) -> f770(A + C,B,-1*B + C) [C >= 0] (?,1) 97. f778(A,B,C) -> f778(A + C,B,-1*B + C) [C >= 0] (?,1) 98. f784(A,B,C) -> f784(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 99. f790(A,B,C) -> f790(A + C,B,-1*B + C) [C >= 0] (?,1) 100. f796(A,B,C) -> f796(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 101. f804(A,B,C) -> f804(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 102. f810(A,B,C) -> f810(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 103. f816(A,B,C) -> f816(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 104. f822(A,B,C) -> f822(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 105. f830(A,B,C) -> f830(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 106. f836(A,B,C) -> f836(A + C,B,-1*B + C) [3 + C >= 0] (?,1) 107. f842(A,B,C) -> f842(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 108. f848(A,B,C) -> f848(A + C,B,-1*B + C) [3 + C >= 0] (?,1) 109. f856(A,B,C) -> f856(A + C,B,-1*B + C) [4 + C >= 0] (?,1) 110. f862(A,B,C) -> f862(A + C,B,-1*B + C) [5 + C >= 0] (?,1) 111. f868(A,B,C) -> f868(A + C,B,-1*B + C) [4 + C >= 0] (?,1) 112. f874(A,B,C) -> f874(A + C,B,-1*B + C) [5 + C >= 0] (?,1) 113. f882(A,B,C) -> f882(A + C,B,-1*B + C) [6 + C >= 0] (?,1) 114. f888(A,B,C) -> f888(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 115. f894(A,B,C) -> f894(A + C,B,-1*B + C) [6 + C >= 0] (?,1) 116. f900(A,B,C) -> f900(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 117. f908(A,B,C) -> f908(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 118. f914(A,B,C) -> f914(A + C,B,-1*B + C) [8 + C >= 0] (?,1) 119. f920(A,B,C) -> f920(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 120. f926(A,B,C) -> f926(A + C,B,-1*B + C) [8 + C >= 0] (?,1) 121. f926(A,B,C) -> f934(A,B,C) [0 >= 9 + C] (1,1) 122. f920(A,B,C) -> f926(A,B,16) [0 >= 8 + C] (1,1) 123. f914(A,B,C) -> f920(A,B,16) [0 >= 9 + C] (1,1) 124. f908(A,B,C) -> f914(A,B,16) [0 >= 8 + C] (1,1) 125. f900(A,B,C) -> f908(A,B,16) [0 >= 8 + C] (1,1) 126. f894(A,B,C) -> f900(A,B,-2) [0 >= 7 + C] (1,1) 127. f888(A,B,C) -> f894(A,B,-2) [0 >= 8 + C] (1,1) 128. f882(A,B,C) -> f888(A,B,-2) [0 >= 7 + C] (1,1) 129. f874(A,B,C) -> f882(A,B,-2) [0 >= 6 + C] (1,1) 130. f868(A,B,C) -> f874(A,B,-1) [0 >= 5 + C] (1,1) 131. f862(A,B,C) -> f868(A,B,-1) [0 >= 6 + C] (1,1) 132. f856(A,B,C) -> f862(A,B,-1) [0 >= 5 + C] (1,1) 133. f848(A,B,C) -> f856(A,B,-1) [0 >= 4 + C] (1,1) 134. f842(A,B,C) -> f848(A,B,0) [0 >= 3 + C] (1,1) 135. f836(A,B,C) -> f842(A,B,0) [0 >= 4 + C] (1,1) 136. f830(A,B,C) -> f836(A,B,0) [0 >= 3 + C] (1,1) 137. f822(A,B,C) -> f830(A,B,0) [0 >= 3 + C] (1,1) 138. f816(A,B,C) -> f822(A,B,9) [0 >= 2 + C] (1,1) 139. f810(A,B,C) -> f816(A,B,9) [0 >= 3 + C] (1,1) 140. f804(A,B,C) -> f810(A,B,9) [0 >= 2 + C] (1,1) 141. f796(A,B,C) -> f804(A,B,9) [0 >= 2 + C] (1,1) 142. f790(A,B,C) -> f796(A,B,8) [0 >= 1 + C] (1,1) 143. f784(A,B,C) -> f790(A,B,8) [0 >= 2 + C] (1,1) 144. f778(A,B,C) -> f784(A,B,8) [0 >= 1 + C] (1,1) 145. f770(A,B,C) -> f778(A,B,8) [0 >= 1 + C] (1,1) 146. f764(A,B,C) -> f770(A,B,7) [0 >= C] (1,1) 147. f758(A,B,C) -> f764(A,B,7) [0 >= 1 + C] (1,1) 148. f752(A,B,C) -> f758(A,B,7) [0 >= C] (1,1) 149. f744(A,B,C) -> f752(A,B,7) [0 >= C] (1,1) 150. f738(A,B,C) -> f744(A,B,6) [1 >= C] (1,1) 151. f732(A,B,C) -> f738(A,B,6) [0 >= C] (1,1) 152. f726(A,B,C) -> f732(A,B,6) [1 >= C] (1,1) 153. f718(A,B,C) -> f726(A,B,6) [1 >= C] (1,1) 154. f712(A,B,C) -> f718(A,B,5) [2 >= C] (1,1) 155. f706(A,B,C) -> f712(A,B,5) [1 >= C] (1,1) 156. f700(A,B,C) -> f706(A,B,5) [2 >= C] (1,1) 157. f692(A,B,C) -> f700(A,B,5) [0 >= 9 + C] (1,1) 158. f686(A,B,C) -> f692(A,B,16) [0 >= 8 + C] (1,1) 159. f680(A,B,C) -> f686(A,B,16) [0 >= 9 + C] (1,1) 160. f674(A,B,C) -> f680(A,B,16) [0 >= 8 + C] (1,1) 161. f666(A,B,C) -> f674(A,B,16) [0 >= 8 + C] (1,1) 162. f660(A,B,C) -> f666(A,B,-2) [0 >= 7 + C] (1,1) 163. f654(A,B,C) -> f660(A,B,-2) [0 >= 8 + C] (1,1) 164. f648(A,B,C) -> f654(A,B,-2) [0 >= 7 + C] (1,1) 165. f640(A,B,C) -> f648(A,B,-2) [0 >= 6 + C] (1,1) 166. f634(A,B,C) -> f640(A,B,-1) [0 >= 5 + C] (1,1) 167. f628(A,B,C) -> f634(A,B,-1) [0 >= 6 + C] (1,1) 168. f622(A,B,C) -> f628(A,B,-1) [0 >= 5 + C] (1,1) 169. f614(A,B,C) -> f622(A,B,-1) [0 >= 4 + C] (1,1) 170. f608(A,B,C) -> f614(A,B,0) [0 >= 3 + C] (1,1) 171. f602(A,B,C) -> f608(A,B,0) [0 >= 4 + C] (1,1) 172. f596(A,B,C) -> f602(A,B,0) [0 >= 3 + C] (1,1) 173. f588(A,B,C) -> f596(A,B,0) [0 >= 3 + C] (1,1) 174. f582(A,B,C) -> f588(A,B,9) [0 >= 2 + C] (1,1) 175. f576(A,B,C) -> f582(A,B,9) [0 >= 3 + C] (1,1) 176. f570(A,B,C) -> f576(A,B,9) [0 >= 2 + C] (1,1) 177. f562(A,B,C) -> f570(A,B,9) [0 >= 2 + C] (1,1) 178. f556(A,B,C) -> f562(A,B,8) [0 >= 1 + C] (1,1) 179. f550(A,B,C) -> f556(A,B,8) [0 >= 2 + C] (1,1) 180. f544(A,B,C) -> f550(A,B,8) [0 >= 1 + C] (1,1) 181. f536(A,B,C) -> f544(A,B,8) [0 >= 1 + C] (1,1) 182. f530(A,B,C) -> f536(A,B,7) [0 >= C] (1,1) 183. f524(A,B,C) -> f530(A,B,7) [0 >= 1 + C] (1,1) 184. f518(A,B,C) -> f524(A,B,7) [0 >= C] (1,1) 185. f510(A,B,C) -> f518(A,B,7) [0 >= C] (1,1) 186. f504(A,B,C) -> f510(A,B,6) [1 >= C] (1,1) 187. f498(A,B,C) -> f504(A,B,6) [0 >= C] (1,1) 188. f492(A,B,C) -> f498(A,B,6) [1 >= C] (1,1) 189. f484(A,B,C) -> f492(A,B,6) [1 >= C] (1,1) 190. f478(A,B,C) -> f484(A,B,5) [2 >= C] (1,1) 191. f472(A,B,C) -> f478(A,B,5) [1 >= C] (1,1) 192. f466(A,B,C) -> f472(A,B,5) [2 >= C] (1,1) 193. f458(A,B,C) -> f466(A,B,5) [C >= 5] (1,1) 194. f452(A,B,C) -> f458(A,B,-6) [C >= 4] (1,1) 195. f446(A,B,C) -> f452(A,B,-6) [C >= 5] (1,1) 196. f440(A,B,C) -> f446(A,B,-6) [C >= 4] (1,1) 197. f432(A,B,C) -> f440(A,B,-6) [C >= 1] (1,1) 198. f426(A,B,C) -> f432(A,B,-5) [C >= 0] (1,1) 199. f420(A,B,C) -> f426(A,B,-5) [C >= 1] (1,1) 200. f414(A,B,C) -> f420(A,B,-5) [C >= 0] (1,1) 201. f406(A,B,C) -> f414(A,B,-5) [C >= 0] (1,1) 202. f400(A,B,C) -> f406(A,B,-4) [1 + C >= 0] (1,1) 203. f394(A,B,C) -> f400(A,B,-4) [C >= 0] (1,1) 204. f388(A,B,C) -> f394(A,B,-4) [1 + C >= 0] (1,1) 205. f380(A,B,C) -> f388(A,B,-4) [1 + C >= 0] (1,1) 206. f374(A,B,C) -> f380(A,B,-3) [2 + C >= 0] (1,1) 207. f368(A,B,C) -> f374(A,B,-3) [1 + C >= 0] (1,1) 208. f362(A,B,C) -> f368(A,B,-3) [2 + C >= 0] (1,1) 209. f354(A,B,C) -> f362(A,B,-3) [C >= 3] (1,1) 210. f348(A,B,C) -> f354(A,B,1) [C >= 2] (1,1) 211. f342(A,B,C) -> f348(A,B,1) [C >= 3] (1,1) 212. f336(A,B,C) -> f342(A,B,1) [C >= 2] (1,1) 213. f328(A,B,C) -> f336(A,B,1) [C >= 4] (1,1) 214. f322(A,B,C) -> f328(A,B,0) [C >= 3] (1,1) 215. f316(A,B,C) -> f322(A,B,0) [C >= 4] (1,1) 216. f310(A,B,C) -> f316(A,B,0) [C >= 3] (1,1) 217. f302(A,B,C) -> f310(A,B,0) [C >= 5] (1,1) 218. f296(A,B,C) -> f302(A,B,-6) [C >= 4] (1,1) 219. f290(A,B,C) -> f296(A,B,-6) [C >= 5] (1,1) 220. f284(A,B,C) -> f290(A,B,-6) [C >= 4] (1,1) 221. f276(A,B,C) -> f284(A,B,-6) [C >= 1] (1,1) 222. f270(A,B,C) -> f276(A,B,-5) [C >= 0] (1,1) 223. f264(A,B,C) -> f270(A,B,-5) [C >= 1] (1,1) 224. f258(A,B,C) -> f264(A,B,-5) [C >= 0] (1,1) 225. f250(A,B,C) -> f258(A,B,-5) [C >= 0] (1,1) 226. f244(A,B,C) -> f250(A,B,-4) [1 + C >= 0] (1,1) 227. f238(A,B,C) -> f244(A,B,-4) [C >= 0] (1,1) 228. f232(A,B,C) -> f238(A,B,-4) [1 + C >= 0] (1,1) 229. f224(A,B,C) -> f232(A,B,-4) [1 + C >= 0] (1,1) 230. f218(A,B,C) -> f224(A,B,-3) [2 + C >= 0] (1,1) 231. f212(A,B,C) -> f218(A,B,-3) [1 + C >= 0] (1,1) 232. f206(A,B,C) -> f212(A,B,-3) [2 + C >= 0] (1,1) 233. f198(A,B,C) -> f206(A,B,-3) [C >= 3] (1,1) 234. f192(A,B,C) -> f198(A,B,1) [C >= 2] (1,1) 235. f186(A,B,C) -> f192(A,B,1) [C >= 3] (1,1) 236. f180(A,B,C) -> f186(A,B,1) [C >= 2] (1,1) 237. f172(A,B,C) -> f180(A,B,1) [C >= 4] (1,1) 238. f166(A,B,C) -> f172(A,B,0) [C >= 3] (1,1) 239. f160(A,B,C) -> f166(A,B,0) [C >= 4] (1,1) 240. f154(A,B,C) -> f160(A,B,0) [C >= 3] (1,1) Signature: {(f0,3) ;(f154,3) ;(f160,3) ;(f166,3) ;(f172,3) ;(f180,3) ;(f186,3) ;(f192,3) ;(f198,3) ;(f206,3) ;(f212,3) ;(f218,3) ;(f224,3) ;(f232,3) ;(f238,3) ;(f244,3) ;(f250,3) ;(f258,3) ;(f264,3) ;(f270,3) ;(f276,3) ;(f284,3) ;(f290,3) ;(f296,3) ;(f302,3) ;(f310,3) ;(f316,3) ;(f322,3) ;(f328,3) ;(f336,3) ;(f342,3) ;(f348,3) ;(f354,3) ;(f362,3) ;(f368,3) ;(f374,3) ;(f380,3) ;(f388,3) ;(f394,3) ;(f400,3) ;(f406,3) ;(f414,3) ;(f420,3) ;(f426,3) ;(f432,3) ;(f440,3) ;(f446,3) ;(f452,3) ;(f458,3) ;(f466,3) ;(f472,3) ;(f478,3) ;(f484,3) ;(f492,3) ;(f498,3) ;(f504,3) ;(f510,3) ;(f518,3) ;(f524,3) ;(f530,3) ;(f536,3) ;(f544,3) ;(f550,3) ;(f556,3) ;(f562,3) ;(f570,3) ;(f576,3) ;(f582,3) ;(f588,3) ;(f596,3) ;(f602,3) ;(f608,3) ;(f614,3) ;(f622,3) ;(f628,3) ;(f634,3) ;(f640,3) ;(f648,3) ;(f654,3) ;(f660,3) ;(f666,3) ;(f674,3) ;(f680,3) ;(f686,3) ;(f692,3) ;(f700,3) ;(f706,3) ;(f712,3) ;(f718,3) ;(f726,3) ;(f732,3) ;(f738,3) ;(f744,3) ;(f752,3) ;(f758,3) ;(f764,3) ;(f770,3) ;(f778,3) ;(f784,3) ;(f790,3) ;(f796,3) ;(f804,3) ;(f810,3) ;(f816,3) ;(f822,3) ;(f830,3) ;(f836,3) ;(f842,3) ;(f848,3) ;(f856,3) ;(f862,3) ;(f868,3) ;(f874,3) ;(f882,3) ;(f888,3) ;(f894,3) ;(f900,3) ;(f908,3) ;(f914,3) ;(f920,3) ;(f926,3) ;(f934,3)} Flow Graph: [0->{1},1->{1,240},2->{2,239},3->{3,238},4->{4,237},5->{5,236},6->{6,235},7->{7,234},8->{8,233},9->{9,232} ,10->{10,231},11->{11,230},12->{12,229},13->{13,228},14->{14,227},15->{15,226},16->{16,225},17->{17,224} ,18->{18,223},19->{19,222},20->{20,221},21->{21,220},22->{22,219},23->{23,218},24->{24,217},25->{25,216} ,26->{26,215},27->{27,214},28->{28,213},29->{29,212},30->{30,211},31->{31,210},32->{32,209},33->{33,208} ,34->{34,207},35->{35,206},36->{36,205},37->{37,204},38->{38,203},39->{39,202},40->{40,201},41->{41,200} ,42->{42,199},43->{43,198},44->{44,197},45->{45,196},46->{46,195},47->{47,194},48->{48,193},49->{49,192} ,50->{50,191},51->{51,190},52->{52,189},53->{53,188},54->{54,187},55->{55,186},56->{56,185},57->{57,184} ,58->{58,183},59->{59,182},60->{60,181},61->{61,180},62->{62,179},63->{63,178},64->{64,177},65->{65,176} ,66->{66,175},67->{67,174},68->{68,173},69->{69,172},70->{70,171},71->{71,170},72->{72,169},73->{73,168} ,74->{74,167},75->{75,166},76->{76,165},77->{77,164},78->{78,163},79->{79,162},80->{80,161},81->{81,160} ,82->{82,159},83->{83,158},84->{84,157},85->{85,156},86->{86,155},87->{87,154},88->{88,153},89->{89,152} ,90->{90,151},91->{91,150},92->{92,149},93->{93,148},94->{94,147},95->{95,146},96->{96,145},97->{97,144} ,98->{98,143},99->{99,142},100->{100,141},101->{101,140},102->{102,139},103->{103,138},104->{104,137} ,105->{105,136},106->{106,135},107->{107,134},108->{108,133},109->{109,132},110->{110,131},111->{111,130} ,112->{112,129},113->{113,128},114->{114,127},115->{115,126},116->{116,125},117->{117,124},118->{118,123} ,119->{119,122},120->{120,121},121->{},122->{120},123->{119},124->{118},125->{117},126->{116},127->{115} ,128->{114},129->{113},130->{112},131->{111},132->{110},133->{109},134->{108},135->{107},136->{106} ,137->{105},138->{104},139->{103},140->{102},141->{101},142->{100},143->{99},144->{98},145->{97},146->{96} ,147->{95},148->{94},149->{93},150->{92},151->{91},152->{90},153->{89},154->{88},155->{87},156->{86} ,157->{85},158->{84},159->{83},160->{82},161->{81},162->{80},163->{79},164->{78},165->{77},166->{76} ,167->{75},168->{74},169->{73},170->{72},171->{71},172->{70},173->{69},174->{68},175->{67},176->{66} ,177->{65},178->{64},179->{63},180->{62},181->{61},182->{60},183->{59},184->{58},185->{57},186->{56} ,187->{55},188->{54},189->{53},190->{52},191->{51},192->{50},193->{49},194->{48},195->{47},196->{46} ,197->{45},198->{44},199->{43},200->{42},201->{41},202->{40},203->{39},204->{38},205->{37},206->{36} ,207->{35},208->{34},209->{33},210->{32},211->{31},212->{30},213->{29},214->{28},215->{27},216->{26} ,217->{25},218->{24},219->{23},220->{22},221->{21},222->{20},223->{19},224->{18},225->{17},226->{16} ,227->{15},228->{14},229->{13},230->{12},231->{11},232->{10},233->{9},234->{8},235->{7},236->{6},237->{5} ,238->{4},239->{3},240->{2}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C) -> f154(0,2,0) True (1,1) 1. f154(A,B,C) -> f154(A + C,B,1 + C) [2 >= C] (?,1) 2. f160(A,B,C) -> f160(A + C,B,1 + C) [3 >= C] (?,1) 3. f166(A,B,C) -> f166(A + C,B,1 + C) [2 >= C] (?,1) 4. f172(A,B,C) -> f172(A + C,B,1 + C) [3 >= C] (?,1) 5. f180(A,B,C) -> f180(A + C,B,1 + C) [1 >= C] (?,1) 6. f186(A,B,C) -> f186(A + C,B,1 + C) [2 >= C] (?,1) 7. f192(A,B,C) -> f192(A + C,B,1 + C) [1 >= C] (?,1) 8. f198(A,B,C) -> f198(A + C,B,1 + C) [2 >= C] (?,1) 9. f206(A,B,C) -> f206(A + C,B,1 + C) [0 >= 3 + C] (?,1) 10. f212(A,B,C) -> f212(A + C,B,1 + C) [0 >= 2 + C] (?,1) 11. f218(A,B,C) -> f218(A + C,B,1 + C) [0 >= 3 + C] (?,1) 12. f224(A,B,C) -> f224(A + C,B,1 + C) [0 >= 2 + C] (?,1) 13. f232(A,B,C) -> f232(A + C,B,1 + C) [0 >= 2 + C] (?,1) 14. f238(A,B,C) -> f238(A + C,B,1 + C) [0 >= 1 + C] (?,1) 15. f244(A,B,C) -> f244(A + C,B,1 + C) [0 >= 2 + C] (?,1) 16. f250(A,B,C) -> f250(A + C,B,1 + C) [0 >= 1 + C] (?,1) 17. f258(A,B,C) -> f258(A + C,B,1 + C) [0 >= 1 + C] (?,1) 18. f264(A,B,C) -> f264(A + C,B,1 + C) [0 >= C] (?,1) 19. f270(A,B,C) -> f270(A + C,B,1 + C) [0 >= 1 + C] (?,1) 20. f276(A,B,C) -> f276(A + C,B,1 + C) [0 >= C] (?,1) 21. f284(A,B,C) -> f284(A + C,B,1 + C) [3 >= C] (?,1) 22. f290(A,B,C) -> f290(A + C,B,1 + C) [4 >= C] (?,1) 23. f296(A,B,C) -> f296(A + C,B,1 + C) [3 >= C] (?,1) 24. f302(A,B,C) -> f302(A + C,B,1 + C) [4 >= C] (?,1) 25. f310(A,B,C) -> f310(A + C,B,B + C) [2 >= C] (?,1) 26. f316(A,B,C) -> f316(A + C,B,B + C) [3 >= C] (?,1) 27. f322(A,B,C) -> f322(A + C,B,B + C) [2 >= C] (?,1) 28. f328(A,B,C) -> f328(A + C,B,B + C) [3 >= C] (?,1) 29. f336(A,B,C) -> f336(A + C,B,B + C) [1 >= C] (?,1) 30. f342(A,B,C) -> f342(A + C,B,B + C) [2 >= C] (?,1) 31. f348(A,B,C) -> f348(A + C,B,B + C) [1 >= C] (?,1) 32. f354(A,B,C) -> f354(A + C,B,B + C) [2 >= C] (?,1) 33. f362(A,B,C) -> f362(A + C,B,B + C) [0 >= 3 + C] (?,1) 34. f368(A,B,C) -> f368(A + C,B,B + C) [0 >= 2 + C] (?,1) 35. f374(A,B,C) -> f374(A + C,B,B + C) [0 >= 3 + C] (?,1) 36. f380(A,B,C) -> f380(A + C,B,B + C) [0 >= 2 + C] (?,1) 37. f388(A,B,C) -> f388(A + C,B,B + C) [0 >= 2 + C] (?,1) 38. f394(A,B,C) -> f394(A + C,B,B + C) [0 >= 1 + C] (?,1) 39. f400(A,B,C) -> f400(A + C,B,B + C) [0 >= 2 + C] (?,1) 40. f406(A,B,C) -> f406(A + C,B,B + C) [0 >= 1 + C] (?,1) 41. f414(A,B,C) -> f414(A + C,B,B + C) [0 >= 1 + C] (?,1) 42. f420(A,B,C) -> f420(A + C,B,B + C) [0 >= C] (?,1) 43. f426(A,B,C) -> f426(A + C,B,B + C) [0 >= 1 + C] (?,1) 44. f432(A,B,C) -> f432(A + C,B,B + C) [0 >= C] (?,1) 45. f440(A,B,C) -> f440(A + C,B,B + C) [3 >= C] (?,1) 46. f446(A,B,C) -> f446(A + C,B,B + C) [4 >= C] (?,1) 47. f452(A,B,C) -> f452(A + C,B,B + C) [3 >= C] (?,1) 48. f458(A,B,C) -> f458(A + C,B,B + C) [4 >= C] (?,1) 49. f466(A,B,C) -> f466(A + C,B,-1 + C) [C >= 3] (?,1) 50. f472(A,B,C) -> f472(A + C,B,-1 + C) [C >= 2] (?,1) 51. f478(A,B,C) -> f478(A + C,B,-1 + C) [C >= 3] (?,1) 52. f484(A,B,C) -> f484(A + C,B,-1 + C) [C >= 2] (?,1) 53. f492(A,B,C) -> f492(A + C,B,-1 + C) [C >= 2] (?,1) 54. f498(A,B,C) -> f498(A + C,B,-1 + C) [C >= 1] (?,1) 55. f504(A,B,C) -> f504(A + C,B,-1 + C) [C >= 2] (?,1) 56. f510(A,B,C) -> f510(A + C,B,-1 + C) [C >= 1] (?,1) 57. f518(A,B,C) -> f518(A + C,B,-1 + C) [C >= 1] (?,1) 58. f524(A,B,C) -> f524(A + C,B,-1 + C) [C >= 0] (?,1) 59. f530(A,B,C) -> f530(A + C,B,-1 + C) [C >= 1] (?,1) 60. f536(A,B,C) -> f536(A + C,B,-1 + C) [C >= 0] (?,1) 61. f544(A,B,C) -> f544(A + C,B,-1 + C) [C >= 0] (?,1) 62. f550(A,B,C) -> f550(A + C,B,-1 + C) [1 + C >= 0] (?,1) 63. f556(A,B,C) -> f556(A + C,B,-1 + C) [C >= 0] (?,1) 64. f562(A,B,C) -> f562(A + C,B,-1 + C) [1 + C >= 0] (?,1) 65. f570(A,B,C) -> f570(A + C,B,-1 + C) [1 + C >= 0] (?,1) 66. f576(A,B,C) -> f576(A + C,B,-1 + C) [2 + C >= 0] (?,1) 67. f582(A,B,C) -> f582(A + C,B,-1 + C) [1 + C >= 0] (?,1) 68. f588(A,B,C) -> f588(A + C,B,-1 + C) [2 + C >= 0] (?,1) 69. f596(A,B,C) -> f596(A + C,B,-1 + C) [2 + C >= 0] (?,1) 70. f602(A,B,C) -> f602(A + C,B,-1 + C) [3 + C >= 0] (?,1) 71. f608(A,B,C) -> f608(A + C,B,-1 + C) [2 + C >= 0] (?,1) 72. f614(A,B,C) -> f614(A + C,B,-1 + C) [3 + C >= 0] (?,1) 73. f622(A,B,C) -> f622(A + C,B,-1 + C) [4 + C >= 0] (?,1) 74. f628(A,B,C) -> f628(A + C,B,-1 + C) [5 + C >= 0] (?,1) 75. f634(A,B,C) -> f634(A + C,B,-1 + C) [4 + C >= 0] (?,1) 76. f640(A,B,C) -> f640(A + C,B,-1 + C) [5 + C >= 0] (?,1) 77. f648(A,B,C) -> f648(A + C,B,-1 + C) [6 + C >= 0] (?,1) 78. f654(A,B,C) -> f654(A + C,B,-1 + C) [7 + C >= 0] (?,1) 79. f660(A,B,C) -> f660(A + C,B,-1 + C) [6 + C >= 0] (?,1) 80. f666(A,B,C) -> f666(A + C,B,-1 + C) [7 + C >= 0] (?,1) 81. f674(A,B,C) -> f674(A + C,B,-1 + C) [7 + C >= 0] (?,1) 82. f680(A,B,C) -> f680(A + C,B,-1 + C) [8 + C >= 0] (?,1) 83. f686(A,B,C) -> f686(A + C,B,-1 + C) [7 + C >= 0] (?,1) 84. f692(A,B,C) -> f692(A + C,B,-1 + C) [8 + C >= 0] (?,1) 85. f700(A,B,C) -> f700(A + C,B,-1*B + C) [C >= 3] (?,1) 86. f706(A,B,C) -> f706(A + C,B,-1*B + C) [C >= 2] (?,1) 87. f712(A,B,C) -> f712(A + C,B,-1*B + C) [C >= 3] (?,1) 88. f718(A,B,C) -> f718(A + C,B,-1*B + C) [C >= 2] (?,1) 89. f726(A,B,C) -> f726(A + C,B,-1*B + C) [C >= 2] (?,1) 90. f732(A,B,C) -> f732(A + C,B,-1*B + C) [C >= 1] (?,1) 91. f738(A,B,C) -> f738(A + C,B,-1*B + C) [C >= 2] (?,1) 92. f744(A,B,C) -> f744(A + C,B,-1*B + C) [C >= 1] (?,1) 93. f752(A,B,C) -> f752(A + C,B,-1*B + C) [C >= 1] (?,1) 94. f758(A,B,C) -> f758(A + C,B,-1*B + C) [C >= 0] (?,1) 95. f764(A,B,C) -> f764(A + C,B,-1*B + C) [C >= 1] (?,1) 96. f770(A,B,C) -> f770(A + C,B,-1*B + C) [C >= 0] (?,1) 97. f778(A,B,C) -> f778(A + C,B,-1*B + C) [C >= 0] (?,1) 98. f784(A,B,C) -> f784(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 99. f790(A,B,C) -> f790(A + C,B,-1*B + C) [C >= 0] (?,1) 100. f796(A,B,C) -> f796(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 101. f804(A,B,C) -> f804(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 102. f810(A,B,C) -> f810(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 103. f816(A,B,C) -> f816(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 104. f822(A,B,C) -> f822(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 105. f830(A,B,C) -> f830(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 106. f836(A,B,C) -> f836(A + C,B,-1*B + C) [3 + C >= 0] (?,1) 107. f842(A,B,C) -> f842(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 108. f848(A,B,C) -> f848(A + C,B,-1*B + C) [3 + C >= 0] (?,1) 109. f856(A,B,C) -> f856(A + C,B,-1*B + C) [4 + C >= 0] (?,1) 110. f862(A,B,C) -> f862(A + C,B,-1*B + C) [5 + C >= 0] (?,1) 111. f868(A,B,C) -> f868(A + C,B,-1*B + C) [4 + C >= 0] (?,1) 112. f874(A,B,C) -> f874(A + C,B,-1*B + C) [5 + C >= 0] (?,1) 113. f882(A,B,C) -> f882(A + C,B,-1*B + C) [6 + C >= 0] (?,1) 114. f888(A,B,C) -> f888(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 115. f894(A,B,C) -> f894(A + C,B,-1*B + C) [6 + C >= 0] (?,1) 116. f900(A,B,C) -> f900(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 117. f908(A,B,C) -> f908(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 118. f914(A,B,C) -> f914(A + C,B,-1*B + C) [8 + C >= 0] (?,1) 119. f920(A,B,C) -> f920(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 120. f926(A,B,C) -> f926(A + C,B,-1*B + C) [8 + C >= 0] (?,1) 121. f926(A,B,C) -> f934(A,B,C) [0 >= 9 + C] (?,1) 122. f920(A,B,C) -> f926(A,B,16) [0 >= 8 + C] (?,1) 123. f914(A,B,C) -> f920(A,B,16) [0 >= 9 + C] (?,1) 124. f908(A,B,C) -> f914(A,B,16) [0 >= 8 + C] (?,1) 125. f900(A,B,C) -> f908(A,B,16) [0 >= 8 + C] (?,1) 126. f894(A,B,C) -> f900(A,B,-2) [0 >= 7 + C] (?,1) 127. f888(A,B,C) -> f894(A,B,-2) [0 >= 8 + C] (?,1) 128. f882(A,B,C) -> f888(A,B,-2) [0 >= 7 + C] (?,1) 129. f874(A,B,C) -> f882(A,B,-2) [0 >= 6 + C] (?,1) 130. f868(A,B,C) -> f874(A,B,-1) [0 >= 5 + C] (?,1) 131. f862(A,B,C) -> f868(A,B,-1) [0 >= 6 + C] (?,1) 132. f856(A,B,C) -> f862(A,B,-1) [0 >= 5 + C] (?,1) 133. f848(A,B,C) -> f856(A,B,-1) [0 >= 4 + C] (?,1) 134. f842(A,B,C) -> f848(A,B,0) [0 >= 3 + C] (?,1) 135. f836(A,B,C) -> f842(A,B,0) [0 >= 4 + C] (?,1) 136. f830(A,B,C) -> f836(A,B,0) [0 >= 3 + C] (?,1) 137. f822(A,B,C) -> f830(A,B,0) [0 >= 3 + C] (?,1) 138. f816(A,B,C) -> f822(A,B,9) [0 >= 2 + C] (?,1) 139. f810(A,B,C) -> f816(A,B,9) [0 >= 3 + C] (?,1) 140. f804(A,B,C) -> f810(A,B,9) [0 >= 2 + C] (?,1) 141. f796(A,B,C) -> f804(A,B,9) [0 >= 2 + C] (?,1) 142. f790(A,B,C) -> f796(A,B,8) [0 >= 1 + C] (?,1) 143. f784(A,B,C) -> f790(A,B,8) [0 >= 2 + C] (?,1) 144. f778(A,B,C) -> f784(A,B,8) [0 >= 1 + C] (?,1) 145. f770(A,B,C) -> f778(A,B,8) [0 >= 1 + C] (?,1) 146. f764(A,B,C) -> f770(A,B,7) [0 >= C] (?,1) 147. f758(A,B,C) -> f764(A,B,7) [0 >= 1 + C] (?,1) 148. f752(A,B,C) -> f758(A,B,7) [0 >= C] (?,1) 149. f744(A,B,C) -> f752(A,B,7) [0 >= C] (?,1) 150. f738(A,B,C) -> f744(A,B,6) [1 >= C] (?,1) 151. f732(A,B,C) -> f738(A,B,6) [0 >= C] (?,1) 152. f726(A,B,C) -> f732(A,B,6) [1 >= C] (?,1) 153. f718(A,B,C) -> f726(A,B,6) [1 >= C] (?,1) 154. f712(A,B,C) -> f718(A,B,5) [2 >= C] (?,1) 155. f706(A,B,C) -> f712(A,B,5) [1 >= C] (?,1) 156. f700(A,B,C) -> f706(A,B,5) [2 >= C] (?,1) 157. f692(A,B,C) -> f700(A,B,5) [0 >= 9 + C] (?,1) 158. f686(A,B,C) -> f692(A,B,16) [0 >= 8 + C] (?,1) 159. f680(A,B,C) -> f686(A,B,16) [0 >= 9 + C] (?,1) 160. f674(A,B,C) -> f680(A,B,16) [0 >= 8 + C] (?,1) 161. f666(A,B,C) -> f674(A,B,16) [0 >= 8 + C] (?,1) 162. f660(A,B,C) -> f666(A,B,-2) [0 >= 7 + C] (?,1) 163. f654(A,B,C) -> f660(A,B,-2) [0 >= 8 + C] (?,1) 164. f648(A,B,C) -> f654(A,B,-2) [0 >= 7 + C] (?,1) 165. f640(A,B,C) -> f648(A,B,-2) [0 >= 6 + C] (?,1) 166. f634(A,B,C) -> f640(A,B,-1) [0 >= 5 + C] (?,1) 167. f628(A,B,C) -> f634(A,B,-1) [0 >= 6 + C] (?,1) 168. f622(A,B,C) -> f628(A,B,-1) [0 >= 5 + C] (?,1) 169. f614(A,B,C) -> f622(A,B,-1) [0 >= 4 + C] (?,1) 170. f608(A,B,C) -> f614(A,B,0) [0 >= 3 + C] (?,1) 171. f602(A,B,C) -> f608(A,B,0) [0 >= 4 + C] (?,1) 172. f596(A,B,C) -> f602(A,B,0) [0 >= 3 + C] (?,1) 173. f588(A,B,C) -> f596(A,B,0) [0 >= 3 + C] (?,1) 174. f582(A,B,C) -> f588(A,B,9) [0 >= 2 + C] (?,1) 175. f576(A,B,C) -> f582(A,B,9) [0 >= 3 + C] (?,1) 176. f570(A,B,C) -> f576(A,B,9) [0 >= 2 + C] (?,1) 177. f562(A,B,C) -> f570(A,B,9) [0 >= 2 + C] (?,1) 178. f556(A,B,C) -> f562(A,B,8) [0 >= 1 + C] (?,1) 179. f550(A,B,C) -> f556(A,B,8) [0 >= 2 + C] (?,1) 180. f544(A,B,C) -> f550(A,B,8) [0 >= 1 + C] (?,1) 181. f536(A,B,C) -> f544(A,B,8) [0 >= 1 + C] (?,1) 182. f530(A,B,C) -> f536(A,B,7) [0 >= C] (?,1) 183. f524(A,B,C) -> f530(A,B,7) [0 >= 1 + C] (?,1) 184. f518(A,B,C) -> f524(A,B,7) [0 >= C] (?,1) 185. f510(A,B,C) -> f518(A,B,7) [0 >= C] (?,1) 186. f504(A,B,C) -> f510(A,B,6) [1 >= C] (?,1) 187. f498(A,B,C) -> f504(A,B,6) [0 >= C] (?,1) 188. f492(A,B,C) -> f498(A,B,6) [1 >= C] (?,1) 189. f484(A,B,C) -> f492(A,B,6) [1 >= C] (?,1) 190. f478(A,B,C) -> f484(A,B,5) [2 >= C] (?,1) 191. f472(A,B,C) -> f478(A,B,5) [1 >= C] (?,1) 192. f466(A,B,C) -> f472(A,B,5) [2 >= C] (?,1) 193. f458(A,B,C) -> f466(A,B,5) [C >= 5] (?,1) 194. f452(A,B,C) -> f458(A,B,-6) [C >= 4] (?,1) 195. f446(A,B,C) -> f452(A,B,-6) [C >= 5] (?,1) 196. f440(A,B,C) -> f446(A,B,-6) [C >= 4] (?,1) 197. f432(A,B,C) -> f440(A,B,-6) [C >= 1] (?,1) 198. f426(A,B,C) -> f432(A,B,-5) [C >= 0] (?,1) 199. f420(A,B,C) -> f426(A,B,-5) [C >= 1] (?,1) 200. f414(A,B,C) -> f420(A,B,-5) [C >= 0] (?,1) 201. f406(A,B,C) -> f414(A,B,-5) [C >= 0] (?,1) 202. f400(A,B,C) -> f406(A,B,-4) [1 + C >= 0] (?,1) 203. f394(A,B,C) -> f400(A,B,-4) [C >= 0] (?,1) 204. f388(A,B,C) -> f394(A,B,-4) [1 + C >= 0] (?,1) 205. f380(A,B,C) -> f388(A,B,-4) [1 + C >= 0] (?,1) 206. f374(A,B,C) -> f380(A,B,-3) [2 + C >= 0] (?,1) 207. f368(A,B,C) -> f374(A,B,-3) [1 + C >= 0] (?,1) 208. f362(A,B,C) -> f368(A,B,-3) [2 + C >= 0] (?,1) 209. f354(A,B,C) -> f362(A,B,-3) [C >= 3] (?,1) 210. f348(A,B,C) -> f354(A,B,1) [C >= 2] (?,1) 211. f342(A,B,C) -> f348(A,B,1) [C >= 3] (?,1) 212. f336(A,B,C) -> f342(A,B,1) [C >= 2] (?,1) 213. f328(A,B,C) -> f336(A,B,1) [C >= 4] (?,1) 214. f322(A,B,C) -> f328(A,B,0) [C >= 3] (?,1) 215. f316(A,B,C) -> f322(A,B,0) [C >= 4] (?,1) 216. f310(A,B,C) -> f316(A,B,0) [C >= 3] (?,1) 217. f302(A,B,C) -> f310(A,B,0) [C >= 5] (?,1) 218. f296(A,B,C) -> f302(A,B,-6) [C >= 4] (?,1) 219. f290(A,B,C) -> f296(A,B,-6) [C >= 5] (?,1) 220. f284(A,B,C) -> f290(A,B,-6) [C >= 4] (?,1) 221. f276(A,B,C) -> f284(A,B,-6) [C >= 1] (?,1) 222. f270(A,B,C) -> f276(A,B,-5) [C >= 0] (?,1) 223. f264(A,B,C) -> f270(A,B,-5) [C >= 1] (?,1) 224. f258(A,B,C) -> f264(A,B,-5) [C >= 0] (?,1) 225. f250(A,B,C) -> f258(A,B,-5) [C >= 0] (?,1) 226. f244(A,B,C) -> f250(A,B,-4) [1 + C >= 0] (?,1) 227. f238(A,B,C) -> f244(A,B,-4) [C >= 0] (?,1) 228. f232(A,B,C) -> f238(A,B,-4) [1 + C >= 0] (?,1) 229. f224(A,B,C) -> f232(A,B,-4) [1 + C >= 0] (?,1) 230. f218(A,B,C) -> f224(A,B,-3) [2 + C >= 0] (?,1) 231. f212(A,B,C) -> f218(A,B,-3) [1 + C >= 0] (?,1) 232. f206(A,B,C) -> f212(A,B,-3) [2 + C >= 0] (?,1) 233. f198(A,B,C) -> f206(A,B,-3) [C >= 3] (?,1) 234. f192(A,B,C) -> f198(A,B,1) [C >= 2] (?,1) 235. f186(A,B,C) -> f192(A,B,1) [C >= 3] (?,1) 236. f180(A,B,C) -> f186(A,B,1) [C >= 2] (?,1) 237. f172(A,B,C) -> f180(A,B,1) [C >= 4] (?,1) 238. f166(A,B,C) -> f172(A,B,0) [C >= 3] (?,1) 239. f160(A,B,C) -> f166(A,B,0) [C >= 4] (?,1) 240. f154(A,B,C) -> f160(A,B,0) [C >= 3] (?,1) 241. f926(A,B,C) -> exitus616(A,B,C) True (?,1) Signature: {(exitus616,3) ;(f0,3) ;(f154,3) ;(f160,3) ;(f166,3) ;(f172,3) ;(f180,3) ;(f186,3) ;(f192,3) ;(f198,3) ;(f206,3) ;(f212,3) ;(f218,3) ;(f224,3) ;(f232,3) ;(f238,3) ;(f244,3) ;(f250,3) ;(f258,3) ;(f264,3) ;(f270,3) ;(f276,3) ;(f284,3) ;(f290,3) ;(f296,3) ;(f302,3) ;(f310,3) ;(f316,3) ;(f322,3) ;(f328,3) ;(f336,3) ;(f342,3) ;(f348,3) ;(f354,3) ;(f362,3) ;(f368,3) ;(f374,3) ;(f380,3) ;(f388,3) ;(f394,3) ;(f400,3) ;(f406,3) ;(f414,3) ;(f420,3) ;(f426,3) ;(f432,3) ;(f440,3) ;(f446,3) ;(f452,3) ;(f458,3) ;(f466,3) ;(f472,3) ;(f478,3) ;(f484,3) ;(f492,3) ;(f498,3) ;(f504,3) ;(f510,3) ;(f518,3) ;(f524,3) ;(f530,3) ;(f536,3) ;(f544,3) ;(f550,3) ;(f556,3) ;(f562,3) ;(f570,3) ;(f576,3) ;(f582,3) ;(f588,3) ;(f596,3) ;(f602,3) ;(f608,3) ;(f614,3) ;(f622,3) ;(f628,3) ;(f634,3) ;(f640,3) ;(f648,3) ;(f654,3) ;(f660,3) ;(f666,3) ;(f674,3) ;(f680,3) ;(f686,3) ;(f692,3) ;(f700,3) ;(f706,3) ;(f712,3) ;(f718,3) ;(f726,3) ;(f732,3) ;(f738,3) ;(f744,3) ;(f752,3) ;(f758,3) ;(f764,3) ;(f770,3) ;(f778,3) ;(f784,3) ;(f790,3) ;(f796,3) ;(f804,3) ;(f810,3) ;(f816,3) ;(f822,3) ;(f830,3) ;(f836,3) ;(f842,3) ;(f848,3) ;(f856,3) ;(f862,3) ;(f868,3) ;(f874,3) ;(f882,3) ;(f888,3) ;(f894,3) ;(f900,3) ;(f908,3) ;(f914,3) ;(f920,3) ;(f926,3) ;(f934,3)} Flow Graph: [0->{1,240},1->{1,240},2->{2,239},3->{3,238},4->{4,237},5->{5,236},6->{6,235},7->{7,234},8->{8,233},9->{9 ,232},10->{10,231},11->{11,230},12->{12,229},13->{13,228},14->{14,227},15->{15,226},16->{16,225},17->{17 ,224},18->{18,223},19->{19,222},20->{20,221},21->{21,220},22->{22,219},23->{23,218},24->{24,217},25->{25 ,216},26->{26,215},27->{27,214},28->{28,213},29->{29,212},30->{30,211},31->{31,210},32->{32,209},33->{33 ,208},34->{34,207},35->{35,206},36->{36,205},37->{37,204},38->{38,203},39->{39,202},40->{40,201},41->{41 ,200},42->{42,199},43->{43,198},44->{44,197},45->{45,196},46->{46,195},47->{47,194},48->{48,193},49->{49 ,192},50->{50,191},51->{51,190},52->{52,189},53->{53,188},54->{54,187},55->{55,186},56->{56,185},57->{57 ,184},58->{58,183},59->{59,182},60->{60,181},61->{61,180},62->{62,179},63->{63,178},64->{64,177},65->{65 ,176},66->{66,175},67->{67,174},68->{68,173},69->{69,172},70->{70,171},71->{71,170},72->{72,169},73->{73 ,168},74->{74,167},75->{75,166},76->{76,165},77->{77,164},78->{78,163},79->{79,162},80->{80,161},81->{81 ,160},82->{82,159},83->{83,158},84->{84,157},85->{85,156},86->{86,155},87->{87,154},88->{88,153},89->{89 ,152},90->{90,151},91->{91,150},92->{92,149},93->{93,148},94->{94,147},95->{95,146},96->{96,145},97->{97 ,144},98->{98,143},99->{99,142},100->{100,141},101->{101,140},102->{102,139},103->{103,138},104->{104,137} ,105->{105,136},106->{106,135},107->{107,134},108->{108,133},109->{109,132},110->{110,131},111->{111,130} ,112->{112,129},113->{113,128},114->{114,127},115->{115,126},116->{116,125},117->{117,124},118->{118,123} ,119->{119,122},120->{120,121,241},121->{},122->{120,121,241},123->{119,122},124->{118,123},125->{117,124} ,126->{116,125},127->{115,126},128->{114,127},129->{113,128},130->{112,129},131->{111,130},132->{110,131} ,133->{109,132},134->{108,133},135->{107,134},136->{106,135},137->{105,136},138->{104,137},139->{103,138} ,140->{102,139},141->{101,140},142->{100,141},143->{99,142},144->{98,143},145->{97,144},146->{96,145} ,147->{95,146},148->{94,147},149->{93,148},150->{92,149},151->{91,150},152->{90,151},153->{89,152},154->{88 ,153},155->{87,154},156->{86,155},157->{85,156},158->{84,157},159->{83,158},160->{82,159},161->{81,160} ,162->{80,161},163->{79,162},164->{78,163},165->{77,164},166->{76,165},167->{75,166},168->{74,167},169->{73 ,168},170->{72,169},171->{71,170},172->{70,171},173->{69,172},174->{68,173},175->{67,174},176->{66,175} ,177->{65,176},178->{64,177},179->{63,178},180->{62,179},181->{61,180},182->{60,181},183->{59,182},184->{58 ,183},185->{57,184},186->{56,185},187->{55,186},188->{54,187},189->{53,188},190->{52,189},191->{51,190} ,192->{50,191},193->{49,192},194->{48,193},195->{47,194},196->{46,195},197->{45,196},198->{44,197},199->{43 ,198},200->{42,199},201->{41,200},202->{40,201},203->{39,202},204->{38,203},205->{37,204},206->{36,205} ,207->{35,206},208->{34,207},209->{33,208},210->{32,209},211->{31,210},212->{30,211},213->{29,212},214->{28 ,213},215->{27,214},216->{26,215},217->{25,216},218->{24,217},219->{23,218},220->{22,219},221->{21,220} ,222->{20,221},223->{19,222},224->{18,223},225->{17,224},226->{16,225},227->{15,226},228->{14,227},229->{13 ,228},230->{12,229},231->{11,230},232->{10,231},233->{9,232},234->{8,233},235->{7,234},236->{6,235},237->{5 ,236},238->{4,237},239->{3,238},240->{2,239},241->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,240) ,(122,121) ,(123,122) ,(124,123) ,(125,124) ,(126,125) ,(127,126) ,(128,127) ,(129,128) ,(130,129) ,(131,130) ,(132,131) ,(133,132) ,(134,133) ,(135,134) ,(136,135) ,(137,136) ,(138,137) ,(139,138) ,(140,139) ,(141,140) ,(142,141) ,(143,142) ,(144,143) ,(145,144) ,(146,145) ,(147,146) ,(148,147) ,(149,148) ,(150,149) ,(151,150) ,(152,151) ,(153,152) ,(154,153) ,(155,154) ,(156,155) ,(157,156) ,(158,157) ,(159,158) ,(160,159) ,(161,160) ,(162,161) ,(163,162) ,(164,163) ,(165,164) ,(166,165) ,(167,166) ,(168,167) ,(169,168) ,(170,169) ,(171,170) ,(172,171) ,(173,172) ,(174,173) ,(175,174) ,(176,175) ,(177,176) ,(178,177) ,(179,178) ,(180,179) ,(181,180) ,(182,181) ,(183,182) ,(184,183) ,(185,184) ,(186,185) ,(187,186) ,(188,187) ,(189,188) ,(190,189) ,(191,190) ,(192,191) ,(193,192) ,(194,193) ,(195,194) ,(196,195) ,(197,196) ,(198,197) ,(199,198) ,(200,199) ,(201,200) ,(202,201) ,(203,202) ,(204,203) ,(205,204) ,(206,205) ,(207,206) ,(208,207) ,(209,208) ,(210,209) ,(211,210) ,(212,211) ,(213,212) ,(214,213) ,(215,214) ,(216,215) ,(217,216) ,(218,217) ,(219,218) ,(220,219) ,(221,220) ,(222,221) ,(223,222) ,(224,223) ,(225,224) ,(226,225) ,(227,226) ,(228,227) ,(229,228) ,(230,229) ,(231,230) ,(232,231) ,(233,232) ,(234,233) ,(235,234) ,(236,235) ,(237,236) ,(238,237) ,(239,238) ,(240,239)] * Step 5: Failure MAYBE + Considered Problem: Rules: 0. f0(A,B,C) -> f154(0,2,0) True (1,1) 1. f154(A,B,C) -> f154(A + C,B,1 + C) [2 >= C] (?,1) 2. f160(A,B,C) -> f160(A + C,B,1 + C) [3 >= C] (?,1) 3. f166(A,B,C) -> f166(A + C,B,1 + C) [2 >= C] (?,1) 4. f172(A,B,C) -> f172(A + C,B,1 + C) [3 >= C] (?,1) 5. f180(A,B,C) -> f180(A + C,B,1 + C) [1 >= C] (?,1) 6. f186(A,B,C) -> f186(A + C,B,1 + C) [2 >= C] (?,1) 7. f192(A,B,C) -> f192(A + C,B,1 + C) [1 >= C] (?,1) 8. f198(A,B,C) -> f198(A + C,B,1 + C) [2 >= C] (?,1) 9. f206(A,B,C) -> f206(A + C,B,1 + C) [0 >= 3 + C] (?,1) 10. f212(A,B,C) -> f212(A + C,B,1 + C) [0 >= 2 + C] (?,1) 11. f218(A,B,C) -> f218(A + C,B,1 + C) [0 >= 3 + C] (?,1) 12. f224(A,B,C) -> f224(A + C,B,1 + C) [0 >= 2 + C] (?,1) 13. f232(A,B,C) -> f232(A + C,B,1 + C) [0 >= 2 + C] (?,1) 14. f238(A,B,C) -> f238(A + C,B,1 + C) [0 >= 1 + C] (?,1) 15. f244(A,B,C) -> f244(A + C,B,1 + C) [0 >= 2 + C] (?,1) 16. f250(A,B,C) -> f250(A + C,B,1 + C) [0 >= 1 + C] (?,1) 17. f258(A,B,C) -> f258(A + C,B,1 + C) [0 >= 1 + C] (?,1) 18. f264(A,B,C) -> f264(A + C,B,1 + C) [0 >= C] (?,1) 19. f270(A,B,C) -> f270(A + C,B,1 + C) [0 >= 1 + C] (?,1) 20. f276(A,B,C) -> f276(A + C,B,1 + C) [0 >= C] (?,1) 21. f284(A,B,C) -> f284(A + C,B,1 + C) [3 >= C] (?,1) 22. f290(A,B,C) -> f290(A + C,B,1 + C) [4 >= C] (?,1) 23. f296(A,B,C) -> f296(A + C,B,1 + C) [3 >= C] (?,1) 24. f302(A,B,C) -> f302(A + C,B,1 + C) [4 >= C] (?,1) 25. f310(A,B,C) -> f310(A + C,B,B + C) [2 >= C] (?,1) 26. f316(A,B,C) -> f316(A + C,B,B + C) [3 >= C] (?,1) 27. f322(A,B,C) -> f322(A + C,B,B + C) [2 >= C] (?,1) 28. f328(A,B,C) -> f328(A + C,B,B + C) [3 >= C] (?,1) 29. f336(A,B,C) -> f336(A + C,B,B + C) [1 >= C] (?,1) 30. f342(A,B,C) -> f342(A + C,B,B + C) [2 >= C] (?,1) 31. f348(A,B,C) -> f348(A + C,B,B + C) [1 >= C] (?,1) 32. f354(A,B,C) -> f354(A + C,B,B + C) [2 >= C] (?,1) 33. f362(A,B,C) -> f362(A + C,B,B + C) [0 >= 3 + C] (?,1) 34. f368(A,B,C) -> f368(A + C,B,B + C) [0 >= 2 + C] (?,1) 35. f374(A,B,C) -> f374(A + C,B,B + C) [0 >= 3 + C] (?,1) 36. f380(A,B,C) -> f380(A + C,B,B + C) [0 >= 2 + C] (?,1) 37. f388(A,B,C) -> f388(A + C,B,B + C) [0 >= 2 + C] (?,1) 38. f394(A,B,C) -> f394(A + C,B,B + C) [0 >= 1 + C] (?,1) 39. f400(A,B,C) -> f400(A + C,B,B + C) [0 >= 2 + C] (?,1) 40. f406(A,B,C) -> f406(A + C,B,B + C) [0 >= 1 + C] (?,1) 41. f414(A,B,C) -> f414(A + C,B,B + C) [0 >= 1 + C] (?,1) 42. f420(A,B,C) -> f420(A + C,B,B + C) [0 >= C] (?,1) 43. f426(A,B,C) -> f426(A + C,B,B + C) [0 >= 1 + C] (?,1) 44. f432(A,B,C) -> f432(A + C,B,B + C) [0 >= C] (?,1) 45. f440(A,B,C) -> f440(A + C,B,B + C) [3 >= C] (?,1) 46. f446(A,B,C) -> f446(A + C,B,B + C) [4 >= C] (?,1) 47. f452(A,B,C) -> f452(A + C,B,B + C) [3 >= C] (?,1) 48. f458(A,B,C) -> f458(A + C,B,B + C) [4 >= C] (?,1) 49. f466(A,B,C) -> f466(A + C,B,-1 + C) [C >= 3] (?,1) 50. f472(A,B,C) -> f472(A + C,B,-1 + C) [C >= 2] (?,1) 51. f478(A,B,C) -> f478(A + C,B,-1 + C) [C >= 3] (?,1) 52. f484(A,B,C) -> f484(A + C,B,-1 + C) [C >= 2] (?,1) 53. f492(A,B,C) -> f492(A + C,B,-1 + C) [C >= 2] (?,1) 54. f498(A,B,C) -> f498(A + C,B,-1 + C) [C >= 1] (?,1) 55. f504(A,B,C) -> f504(A + C,B,-1 + C) [C >= 2] (?,1) 56. f510(A,B,C) -> f510(A + C,B,-1 + C) [C >= 1] (?,1) 57. f518(A,B,C) -> f518(A + C,B,-1 + C) [C >= 1] (?,1) 58. f524(A,B,C) -> f524(A + C,B,-1 + C) [C >= 0] (?,1) 59. f530(A,B,C) -> f530(A + C,B,-1 + C) [C >= 1] (?,1) 60. f536(A,B,C) -> f536(A + C,B,-1 + C) [C >= 0] (?,1) 61. f544(A,B,C) -> f544(A + C,B,-1 + C) [C >= 0] (?,1) 62. f550(A,B,C) -> f550(A + C,B,-1 + C) [1 + C >= 0] (?,1) 63. f556(A,B,C) -> f556(A + C,B,-1 + C) [C >= 0] (?,1) 64. f562(A,B,C) -> f562(A + C,B,-1 + C) [1 + C >= 0] (?,1) 65. f570(A,B,C) -> f570(A + C,B,-1 + C) [1 + C >= 0] (?,1) 66. f576(A,B,C) -> f576(A + C,B,-1 + C) [2 + C >= 0] (?,1) 67. f582(A,B,C) -> f582(A + C,B,-1 + C) [1 + C >= 0] (?,1) 68. f588(A,B,C) -> f588(A + C,B,-1 + C) [2 + C >= 0] (?,1) 69. f596(A,B,C) -> f596(A + C,B,-1 + C) [2 + C >= 0] (?,1) 70. f602(A,B,C) -> f602(A + C,B,-1 + C) [3 + C >= 0] (?,1) 71. f608(A,B,C) -> f608(A + C,B,-1 + C) [2 + C >= 0] (?,1) 72. f614(A,B,C) -> f614(A + C,B,-1 + C) [3 + C >= 0] (?,1) 73. f622(A,B,C) -> f622(A + C,B,-1 + C) [4 + C >= 0] (?,1) 74. f628(A,B,C) -> f628(A + C,B,-1 + C) [5 + C >= 0] (?,1) 75. f634(A,B,C) -> f634(A + C,B,-1 + C) [4 + C >= 0] (?,1) 76. f640(A,B,C) -> f640(A + C,B,-1 + C) [5 + C >= 0] (?,1) 77. f648(A,B,C) -> f648(A + C,B,-1 + C) [6 + C >= 0] (?,1) 78. f654(A,B,C) -> f654(A + C,B,-1 + C) [7 + C >= 0] (?,1) 79. f660(A,B,C) -> f660(A + C,B,-1 + C) [6 + C >= 0] (?,1) 80. f666(A,B,C) -> f666(A + C,B,-1 + C) [7 + C >= 0] (?,1) 81. f674(A,B,C) -> f674(A + C,B,-1 + C) [7 + C >= 0] (?,1) 82. f680(A,B,C) -> f680(A + C,B,-1 + C) [8 + C >= 0] (?,1) 83. f686(A,B,C) -> f686(A + C,B,-1 + C) [7 + C >= 0] (?,1) 84. f692(A,B,C) -> f692(A + C,B,-1 + C) [8 + C >= 0] (?,1) 85. f700(A,B,C) -> f700(A + C,B,-1*B + C) [C >= 3] (?,1) 86. f706(A,B,C) -> f706(A + C,B,-1*B + C) [C >= 2] (?,1) 87. f712(A,B,C) -> f712(A + C,B,-1*B + C) [C >= 3] (?,1) 88. f718(A,B,C) -> f718(A + C,B,-1*B + C) [C >= 2] (?,1) 89. f726(A,B,C) -> f726(A + C,B,-1*B + C) [C >= 2] (?,1) 90. f732(A,B,C) -> f732(A + C,B,-1*B + C) [C >= 1] (?,1) 91. f738(A,B,C) -> f738(A + C,B,-1*B + C) [C >= 2] (?,1) 92. f744(A,B,C) -> f744(A + C,B,-1*B + C) [C >= 1] (?,1) 93. f752(A,B,C) -> f752(A + C,B,-1*B + C) [C >= 1] (?,1) 94. f758(A,B,C) -> f758(A + C,B,-1*B + C) [C >= 0] (?,1) 95. f764(A,B,C) -> f764(A + C,B,-1*B + C) [C >= 1] (?,1) 96. f770(A,B,C) -> f770(A + C,B,-1*B + C) [C >= 0] (?,1) 97. f778(A,B,C) -> f778(A + C,B,-1*B + C) [C >= 0] (?,1) 98. f784(A,B,C) -> f784(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 99. f790(A,B,C) -> f790(A + C,B,-1*B + C) [C >= 0] (?,1) 100. f796(A,B,C) -> f796(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 101. f804(A,B,C) -> f804(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 102. f810(A,B,C) -> f810(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 103. f816(A,B,C) -> f816(A + C,B,-1*B + C) [1 + C >= 0] (?,1) 104. f822(A,B,C) -> f822(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 105. f830(A,B,C) -> f830(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 106. f836(A,B,C) -> f836(A + C,B,-1*B + C) [3 + C >= 0] (?,1) 107. f842(A,B,C) -> f842(A + C,B,-1*B + C) [2 + C >= 0] (?,1) 108. f848(A,B,C) -> f848(A + C,B,-1*B + C) [3 + C >= 0] (?,1) 109. f856(A,B,C) -> f856(A + C,B,-1*B + C) [4 + C >= 0] (?,1) 110. f862(A,B,C) -> f862(A + C,B,-1*B + C) [5 + C >= 0] (?,1) 111. f868(A,B,C) -> f868(A + C,B,-1*B + C) [4 + C >= 0] (?,1) 112. f874(A,B,C) -> f874(A + C,B,-1*B + C) [5 + C >= 0] (?,1) 113. f882(A,B,C) -> f882(A + C,B,-1*B + C) [6 + C >= 0] (?,1) 114. f888(A,B,C) -> f888(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 115. f894(A,B,C) -> f894(A + C,B,-1*B + C) [6 + C >= 0] (?,1) 116. f900(A,B,C) -> f900(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 117. f908(A,B,C) -> f908(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 118. f914(A,B,C) -> f914(A + C,B,-1*B + C) [8 + C >= 0] (?,1) 119. f920(A,B,C) -> f920(A + C,B,-1*B + C) [7 + C >= 0] (?,1) 120. f926(A,B,C) -> f926(A + C,B,-1*B + C) [8 + C >= 0] (?,1) 121. f926(A,B,C) -> f934(A,B,C) [0 >= 9 + C] (?,1) 122. f920(A,B,C) -> f926(A,B,16) [0 >= 8 + C] (?,1) 123. f914(A,B,C) -> f920(A,B,16) [0 >= 9 + C] (?,1) 124. f908(A,B,C) -> f914(A,B,16) [0 >= 8 + C] (?,1) 125. f900(A,B,C) -> f908(A,B,16) [0 >= 8 + C] (?,1) 126. f894(A,B,C) -> f900(A,B,-2) [0 >= 7 + C] (?,1) 127. f888(A,B,C) -> f894(A,B,-2) [0 >= 8 + C] (?,1) 128. f882(A,B,C) -> f888(A,B,-2) [0 >= 7 + C] (?,1) 129. f874(A,B,C) -> f882(A,B,-2) [0 >= 6 + C] (?,1) 130. f868(A,B,C) -> f874(A,B,-1) [0 >= 5 + C] (?,1) 131. f862(A,B,C) -> f868(A,B,-1) [0 >= 6 + C] (?,1) 132. f856(A,B,C) -> f862(A,B,-1) [0 >= 5 + C] (?,1) 133. f848(A,B,C) -> f856(A,B,-1) [0 >= 4 + C] (?,1) 134. f842(A,B,C) -> f848(A,B,0) [0 >= 3 + C] (?,1) 135. f836(A,B,C) -> f842(A,B,0) [0 >= 4 + C] (?,1) 136. f830(A,B,C) -> f836(A,B,0) [0 >= 3 + C] (?,1) 137. f822(A,B,C) -> f830(A,B,0) [0 >= 3 + C] (?,1) 138. f816(A,B,C) -> f822(A,B,9) [0 >= 2 + C] (?,1) 139. f810(A,B,C) -> f816(A,B,9) [0 >= 3 + C] (?,1) 140. f804(A,B,C) -> f810(A,B,9) [0 >= 2 + C] (?,1) 141. f796(A,B,C) -> f804(A,B,9) [0 >= 2 + C] (?,1) 142. f790(A,B,C) -> f796(A,B,8) [0 >= 1 + C] (?,1) 143. f784(A,B,C) -> f790(A,B,8) [0 >= 2 + C] (?,1) 144. f778(A,B,C) -> f784(A,B,8) [0 >= 1 + C] (?,1) 145. f770(A,B,C) -> f778(A,B,8) [0 >= 1 + C] (?,1) 146. f764(A,B,C) -> f770(A,B,7) [0 >= C] (?,1) 147. f758(A,B,C) -> f764(A,B,7) [0 >= 1 + C] (?,1) 148. f752(A,B,C) -> f758(A,B,7) [0 >= C] (?,1) 149. f744(A,B,C) -> f752(A,B,7) [0 >= C] (?,1) 150. f738(A,B,C) -> f744(A,B,6) [1 >= C] (?,1) 151. f732(A,B,C) -> f738(A,B,6) [0 >= C] (?,1) 152. f726(A,B,C) -> f732(A,B,6) [1 >= C] (?,1) 153. f718(A,B,C) -> f726(A,B,6) [1 >= C] (?,1) 154. f712(A,B,C) -> f718(A,B,5) [2 >= C] (?,1) 155. f706(A,B,C) -> f712(A,B,5) [1 >= C] (?,1) 156. f700(A,B,C) -> f706(A,B,5) [2 >= C] (?,1) 157. f692(A,B,C) -> f700(A,B,5) [0 >= 9 + C] (?,1) 158. f686(A,B,C) -> f692(A,B,16) [0 >= 8 + C] (?,1) 159. f680(A,B,C) -> f686(A,B,16) [0 >= 9 + C] (?,1) 160. f674(A,B,C) -> f680(A,B,16) [0 >= 8 + C] (?,1) 161. f666(A,B,C) -> f674(A,B,16) [0 >= 8 + C] (?,1) 162. f660(A,B,C) -> f666(A,B,-2) [0 >= 7 + C] (?,1) 163. f654(A,B,C) -> f660(A,B,-2) [0 >= 8 + C] (?,1) 164. f648(A,B,C) -> f654(A,B,-2) [0 >= 7 + C] (?,1) 165. f640(A,B,C) -> f648(A,B,-2) [0 >= 6 + C] (?,1) 166. f634(A,B,C) -> f640(A,B,-1) [0 >= 5 + C] (?,1) 167. f628(A,B,C) -> f634(A,B,-1) [0 >= 6 + C] (?,1) 168. f622(A,B,C) -> f628(A,B,-1) [0 >= 5 + C] (?,1) 169. f614(A,B,C) -> f622(A,B,-1) [0 >= 4 + C] (?,1) 170. f608(A,B,C) -> f614(A,B,0) [0 >= 3 + C] (?,1) 171. f602(A,B,C) -> f608(A,B,0) [0 >= 4 + C] (?,1) 172. f596(A,B,C) -> f602(A,B,0) [0 >= 3 + C] (?,1) 173. f588(A,B,C) -> f596(A,B,0) [0 >= 3 + C] (?,1) 174. f582(A,B,C) -> f588(A,B,9) [0 >= 2 + C] (?,1) 175. f576(A,B,C) -> f582(A,B,9) [0 >= 3 + C] (?,1) 176. f570(A,B,C) -> f576(A,B,9) [0 >= 2 + C] (?,1) 177. f562(A,B,C) -> f570(A,B,9) [0 >= 2 + C] (?,1) 178. f556(A,B,C) -> f562(A,B,8) [0 >= 1 + C] (?,1) 179. f550(A,B,C) -> f556(A,B,8) [0 >= 2 + C] (?,1) 180. f544(A,B,C) -> f550(A,B,8) [0 >= 1 + C] (?,1) 181. f536(A,B,C) -> f544(A,B,8) [0 >= 1 + C] (?,1) 182. f530(A,B,C) -> f536(A,B,7) [0 >= C] (?,1) 183. f524(A,B,C) -> f530(A,B,7) [0 >= 1 + C] (?,1) 184. f518(A,B,C) -> f524(A,B,7) [0 >= C] (?,1) 185. f510(A,B,C) -> f518(A,B,7) [0 >= C] (?,1) 186. f504(A,B,C) -> f510(A,B,6) [1 >= C] (?,1) 187. f498(A,B,C) -> f504(A,B,6) [0 >= C] (?,1) 188. f492(A,B,C) -> f498(A,B,6) [1 >= C] (?,1) 189. f484(A,B,C) -> f492(A,B,6) [1 >= C] (?,1) 190. f478(A,B,C) -> f484(A,B,5) [2 >= C] (?,1) 191. f472(A,B,C) -> f478(A,B,5) [1 >= C] (?,1) 192. f466(A,B,C) -> f472(A,B,5) [2 >= C] (?,1) 193. f458(A,B,C) -> f466(A,B,5) [C >= 5] (?,1) 194. f452(A,B,C) -> f458(A,B,-6) [C >= 4] (?,1) 195. f446(A,B,C) -> f452(A,B,-6) [C >= 5] (?,1) 196. f440(A,B,C) -> f446(A,B,-6) [C >= 4] (?,1) 197. f432(A,B,C) -> f440(A,B,-6) [C >= 1] (?,1) 198. f426(A,B,C) -> f432(A,B,-5) [C >= 0] (?,1) 199. f420(A,B,C) -> f426(A,B,-5) [C >= 1] (?,1) 200. f414(A,B,C) -> f420(A,B,-5) [C >= 0] (?,1) 201. f406(A,B,C) -> f414(A,B,-5) [C >= 0] (?,1) 202. f400(A,B,C) -> f406(A,B,-4) [1 + C >= 0] (?,1) 203. f394(A,B,C) -> f400(A,B,-4) [C >= 0] (?,1) 204. f388(A,B,C) -> f394(A,B,-4) [1 + C >= 0] (?,1) 205. f380(A,B,C) -> f388(A,B,-4) [1 + C >= 0] (?,1) 206. f374(A,B,C) -> f380(A,B,-3) [2 + C >= 0] (?,1) 207. f368(A,B,C) -> f374(A,B,-3) [1 + C >= 0] (?,1) 208. f362(A,B,C) -> f368(A,B,-3) [2 + C >= 0] (?,1) 209. f354(A,B,C) -> f362(A,B,-3) [C >= 3] (?,1) 210. f348(A,B,C) -> f354(A,B,1) [C >= 2] (?,1) 211. f342(A,B,C) -> f348(A,B,1) [C >= 3] (?,1) 212. f336(A,B,C) -> f342(A,B,1) [C >= 2] (?,1) 213. f328(A,B,C) -> f336(A,B,1) [C >= 4] (?,1) 214. f322(A,B,C) -> f328(A,B,0) [C >= 3] (?,1) 215. f316(A,B,C) -> f322(A,B,0) [C >= 4] (?,1) 216. f310(A,B,C) -> f316(A,B,0) [C >= 3] (?,1) 217. f302(A,B,C) -> f310(A,B,0) [C >= 5] (?,1) 218. f296(A,B,C) -> f302(A,B,-6) [C >= 4] (?,1) 219. f290(A,B,C) -> f296(A,B,-6) [C >= 5] (?,1) 220. f284(A,B,C) -> f290(A,B,-6) [C >= 4] (?,1) 221. f276(A,B,C) -> f284(A,B,-6) [C >= 1] (?,1) 222. f270(A,B,C) -> f276(A,B,-5) [C >= 0] (?,1) 223. f264(A,B,C) -> f270(A,B,-5) [C >= 1] (?,1) 224. f258(A,B,C) -> f264(A,B,-5) [C >= 0] (?,1) 225. f250(A,B,C) -> f258(A,B,-5) [C >= 0] (?,1) 226. f244(A,B,C) -> f250(A,B,-4) [1 + C >= 0] (?,1) 227. f238(A,B,C) -> f244(A,B,-4) [C >= 0] (?,1) 228. f232(A,B,C) -> f238(A,B,-4) [1 + C >= 0] (?,1) 229. f224(A,B,C) -> f232(A,B,-4) [1 + C >= 0] (?,1) 230. f218(A,B,C) -> f224(A,B,-3) [2 + C >= 0] (?,1) 231. f212(A,B,C) -> f218(A,B,-3) [1 + C >= 0] (?,1) 232. f206(A,B,C) -> f212(A,B,-3) [2 + C >= 0] (?,1) 233. f198(A,B,C) -> f206(A,B,-3) [C >= 3] (?,1) 234. f192(A,B,C) -> f198(A,B,1) [C >= 2] (?,1) 235. f186(A,B,C) -> f192(A,B,1) [C >= 3] (?,1) 236. f180(A,B,C) -> f186(A,B,1) [C >= 2] (?,1) 237. f172(A,B,C) -> f180(A,B,1) [C >= 4] (?,1) 238. f166(A,B,C) -> f172(A,B,0) [C >= 3] (?,1) 239. f160(A,B,C) -> f166(A,B,0) [C >= 4] (?,1) 240. f154(A,B,C) -> f160(A,B,0) [C >= 3] (?,1) 241. f926(A,B,C) -> exitus616(A,B,C) True (?,1) Signature: {(exitus616,3) ;(f0,3) ;(f154,3) ;(f160,3) ;(f166,3) ;(f172,3) ;(f180,3) ;(f186,3) ;(f192,3) ;(f198,3) ;(f206,3) ;(f212,3) ;(f218,3) ;(f224,3) ;(f232,3) ;(f238,3) ;(f244,3) ;(f250,3) ;(f258,3) ;(f264,3) ;(f270,3) ;(f276,3) ;(f284,3) ;(f290,3) ;(f296,3) ;(f302,3) ;(f310,3) ;(f316,3) ;(f322,3) ;(f328,3) ;(f336,3) ;(f342,3) ;(f348,3) ;(f354,3) ;(f362,3) ;(f368,3) ;(f374,3) ;(f380,3) ;(f388,3) ;(f394,3) ;(f400,3) ;(f406,3) ;(f414,3) ;(f420,3) ;(f426,3) ;(f432,3) ;(f440,3) ;(f446,3) ;(f452,3) ;(f458,3) ;(f466,3) ;(f472,3) ;(f478,3) ;(f484,3) ;(f492,3) ;(f498,3) ;(f504,3) ;(f510,3) ;(f518,3) ;(f524,3) ;(f530,3) ;(f536,3) ;(f544,3) ;(f550,3) ;(f556,3) ;(f562,3) ;(f570,3) ;(f576,3) ;(f582,3) ;(f588,3) ;(f596,3) ;(f602,3) ;(f608,3) ;(f614,3) ;(f622,3) ;(f628,3) ;(f634,3) ;(f640,3) ;(f648,3) ;(f654,3) ;(f660,3) ;(f666,3) ;(f674,3) ;(f680,3) ;(f686,3) ;(f692,3) ;(f700,3) ;(f706,3) ;(f712,3) ;(f718,3) ;(f726,3) ;(f732,3) ;(f738,3) ;(f744,3) ;(f752,3) ;(f758,3) ;(f764,3) ;(f770,3) ;(f778,3) ;(f784,3) ;(f790,3) ;(f796,3) ;(f804,3) ;(f810,3) ;(f816,3) ;(f822,3) ;(f830,3) ;(f836,3) ;(f842,3) ;(f848,3) ;(f856,3) ;(f862,3) ;(f868,3) ;(f874,3) ;(f882,3) ;(f888,3) ;(f894,3) ;(f900,3) ;(f908,3) ;(f914,3) ;(f920,3) ;(f926,3) ;(f934,3)} Flow Graph: [0->{1},1->{1,240},2->{2,239},3->{3,238},4->{4,237},5->{5,236},6->{6,235},7->{7,234},8->{8,233},9->{9,232} ,10->{10,231},11->{11,230},12->{12,229},13->{13,228},14->{14,227},15->{15,226},16->{16,225},17->{17,224} ,18->{18,223},19->{19,222},20->{20,221},21->{21,220},22->{22,219},23->{23,218},24->{24,217},25->{25,216} ,26->{26,215},27->{27,214},28->{28,213},29->{29,212},30->{30,211},31->{31,210},32->{32,209},33->{33,208} ,34->{34,207},35->{35,206},36->{36,205},37->{37,204},38->{38,203},39->{39,202},40->{40,201},41->{41,200} ,42->{42,199},43->{43,198},44->{44,197},45->{45,196},46->{46,195},47->{47,194},48->{48,193},49->{49,192} ,50->{50,191},51->{51,190},52->{52,189},53->{53,188},54->{54,187},55->{55,186},56->{56,185},57->{57,184} ,58->{58,183},59->{59,182},60->{60,181},61->{61,180},62->{62,179},63->{63,178},64->{64,177},65->{65,176} ,66->{66,175},67->{67,174},68->{68,173},69->{69,172},70->{70,171},71->{71,170},72->{72,169},73->{73,168} ,74->{74,167},75->{75,166},76->{76,165},77->{77,164},78->{78,163},79->{79,162},80->{80,161},81->{81,160} ,82->{82,159},83->{83,158},84->{84,157},85->{85,156},86->{86,155},87->{87,154},88->{88,153},89->{89,152} ,90->{90,151},91->{91,150},92->{92,149},93->{93,148},94->{94,147},95->{95,146},96->{96,145},97->{97,144} ,98->{98,143},99->{99,142},100->{100,141},101->{101,140},102->{102,139},103->{103,138},104->{104,137} ,105->{105,136},106->{106,135},107->{107,134},108->{108,133},109->{109,132},110->{110,131},111->{111,130} ,112->{112,129},113->{113,128},114->{114,127},115->{115,126},116->{116,125},117->{117,124},118->{118,123} ,119->{119,122},120->{120,121,241},121->{},122->{120,241},123->{119},124->{118},125->{117},126->{116} ,127->{115},128->{114},129->{113},130->{112},131->{111},132->{110},133->{109},134->{108},135->{107} ,136->{106},137->{105},138->{104},139->{103},140->{102},141->{101},142->{100},143->{99},144->{98},145->{97} ,146->{96},147->{95},148->{94},149->{93},150->{92},151->{91},152->{90},153->{89},154->{88},155->{87} ,156->{86},157->{85},158->{84},159->{83},160->{82},161->{81},162->{80},163->{79},164->{78},165->{77} ,166->{76},167->{75},168->{74},169->{73},170->{72},171->{71},172->{70},173->{69},174->{68},175->{67} ,176->{66},177->{65},178->{64},179->{63},180->{62},181->{61},182->{60},183->{59},184->{58},185->{57} ,186->{56},187->{55},188->{54},189->{53},190->{52},191->{51},192->{50},193->{49},194->{48},195->{47} ,196->{46},197->{45},198->{44},199->{43},200->{42},201->{41},202->{40},203->{39},204->{38},205->{37} ,206->{36},207->{35},208->{34},209->{33},210->{32},211->{31},212->{30},213->{29},214->{28},215->{27} ,216->{26},217->{25},218->{24},219->{23},220->{22},221->{21},222->{20},223->{19},224->{18},225->{17} ,226->{16},227->{15},228->{14},229->{13},230->{12},231->{11},232->{10},233->{9},234->{8},235->{7},236->{6} ,237->{5},238->{4},239->{3},240->{2},241->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241] | +- p:[1] c: [1] | +- p:[2] c: [2] | +- p:[3] c: [3] | +- p:[4] c: [4] | +- p:[5] c: [5] | +- p:[6] c: [6] | +- p:[7] c: [7] | +- p:[8] c: [8] | +- p:[9] c: [9] | +- p:[10] c: [10] | +- p:[11] c: [11] | +- p:[12] c: [12] | +- p:[13] c: [13] | +- p:[14] c: [14] | +- p:[15] c: [15] | +- p:[16] c: [16] | +- p:[17] c: [17] | +- p:[18] c: [18] | +- p:[19] c: [19] | +- p:[20] c: [20] | +- p:[21] c: [21] | +- p:[22] c: [22] | +- p:[23] c: [23] | +- p:[24] c: [24] | +- p:[25] c: [] | +- p:[26] c: [] | +- p:[27] c: [] | +- p:[28] c: [] | +- p:[29] c: [] | +- p:[30] c: [] | +- p:[31] c: [] | +- p:[32] c: [] | +- p:[33] c: [] | +- p:[34] c: [] | +- p:[35] c: [] | +- p:[36] c: [] | +- p:[37] c: [] | +- p:[38] c: [] | +- p:[39] c: [] | +- p:[40] c: [] | +- p:[41] c: [] | +- p:[42] c: [] | +- p:[43] c: [] | +- p:[44] c: [] | +- p:[45] c: [] | +- p:[46] c: [] | +- p:[47] c: [] | +- p:[48] c: [] | +- p:[49] c: [49] | +- p:[50] c: [50] | +- p:[51] c: [51] | +- p:[52] c: [52] | +- p:[53] c: [53] | +- p:[54] c: [54] | +- p:[55] c: [55] | +- p:[56] c: [56] | +- p:[57] c: [57] | +- p:[58] c: [58] | +- p:[59] c: [59] | +- p:[60] c: [60] | +- p:[61] c: [61] | +- p:[62] c: [62] | +- p:[63] c: [63] | +- p:[64] c: [64] | +- p:[65] c: [65] | +- p:[66] c: [66] | +- p:[67] c: [67] | +- p:[68] c: [68] | +- p:[69] c: [69] | +- p:[70] c: [70] | +- p:[71] c: [71] | +- p:[72] c: [72] | +- p:[73] c: [73] | +- p:[74] c: [74] | +- p:[75] c: [75] | +- p:[76] c: [76] | +- p:[77] c: [77] | +- p:[78] c: [78] | +- p:[79] c: [79] | +- p:[80] c: [80] | +- p:[81] c: [81] | +- p:[82] c: [82] | +- p:[83] c: [83] | +- p:[84] c: [84] | +- p:[85] c: [] | +- p:[86] c: [] | +- p:[87] c: [] | +- p:[88] c: [] | +- p:[89] c: [] | +- p:[90] c: [] | +- p:[91] c: [] | +- p:[92] c: [] | +- p:[93] c: [] | +- p:[94] c: [] | +- p:[95] c: [] | +- p:[96] c: [] | +- p:[97] c: [] | +- p:[98] c: [] | +- p:[99] c: [] | +- p:[100] c: [] | +- p:[101] c: [] | +- p:[102] c: [] | +- p:[103] c: [] | +- p:[104] c: [] | +- p:[105] c: [] | +- p:[106] c: [] | +- p:[107] c: [] | +- p:[108] c: [] | +- p:[109] c: [] | +- p:[110] c: [] | +- p:[111] c: [] | +- p:[112] c: [] | +- p:[113] c: [] | +- p:[114] c: [] | +- p:[115] c: [] | +- p:[116] c: [] | +- p:[117] c: [] | +- p:[118] c: [] | +- p:[119] c: [] | `- p:[120] c: [] MAYBE