NO

Initial ITS
Start location: l18
   0: l0 -> l1 : __disjvr_13^0'=__disjvr_13^post0, __disjvr_7^0'=__disjvr_7^post0, __disjvr_10^0'=__disjvr_10^post0, __disjvr_9^0'=__disjvr_9^post0, __disjvr_4^0'=__disjvr_4^post0, __disjvr_1^0'=__disjvr_1^post0, __disjvr_12^0'=__disjvr_12^post0, y^0'=y^post0, __disjvr_6^0'=__disjvr_6^post0, __disjvr_0^0'=__disjvr_0^post0, __disjvr_3^0'=__disjvr_3^post0, __disjvr_14^0'=__disjvr_14^post0, __disjvr_8^0'=__disjvr_8^post0, __disjvr_11^0'=__disjvr_11^post0, x^0'=x^post0, __disjvr_5^0'=__disjvr_5^post0, __disjvr_2^0'=__disjvr_2^post0, (-x^post0+x^0 == 0 /\ -__disjvr_12^post0+__disjvr_12^0 == 0 /\ __disjvr_6^0-__disjvr_6^post0 == 0 /\ __disjvr_7^0-__disjvr_7^post0 == 0 /\ __disjvr_11^0-__disjvr_11^post0 == 0 /\ -__disjvr_3^post0+__disjvr_3^0 == 0 /\ __disjvr_1^0-__disjvr_1^post0 == 0 /\ -y^post0+y^0 == 0 /\ -__disjvr_14^post0+__disjvr_14^0 == 0 /\ __disjvr_8^0-__disjvr_8^post0 == 0 /\ __disjvr_0^0-__disjvr_0^post0 == 0 /\ __disjvr_4^0-__disjvr_4^post0 == 0 /\ __disjvr_10^0-__disjvr_10^post0 == 0 /\ -__disjvr_5^post0+__disjvr_5^0 == 0 /\ -__disjvr_2^post0+__disjvr_2^0 == 0 /\ __disjvr_13^0-__disjvr_13^post0 == 0 /\ -__disjvr_9^post0+__disjvr_9^0 == 0), cost: 1
   1: l1 -> l3 : __disjvr_13^0'=__disjvr_13^post1, __disjvr_7^0'=__disjvr_7^post1, __disjvr_10^0'=__disjvr_10^post1, __disjvr_9^0'=__disjvr_9^post1, __disjvr_4^0'=__disjvr_4^post1, __disjvr_1^0'=__disjvr_1^post1, __disjvr_12^0'=__disjvr_12^post1, y^0'=y^post1, __disjvr_6^0'=__disjvr_6^post1, __disjvr_0^0'=__disjvr_0^post1, __disjvr_3^0'=__disjvr_3^post1, __disjvr_14^0'=__disjvr_14^post1, __disjvr_8^0'=__disjvr_8^post1, __disjvr_11^0'=__disjvr_11^post1, x^0'=x^post1, __disjvr_5^0'=__disjvr_5^post1, __disjvr_2^0'=__disjvr_2^post1, (-__disjvr_0^0+__disjvr_0^post1 == 0 /\ __disjvr_9^0-__disjvr_9^post1 == 0 /\ __disjvr_13^0-__disjvr_13^post1 == 0 /\ -__disjvr_8^post1+__disjvr_8^0 == 0 /\ -__disjvr_5^post1+__disjvr_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post1 == 0 /\ __disjvr_4^0-__disjvr_4^post1 == 0 /\ -x^post1+x^0 == 0 /\ -__disjvr_12^post1+__disjvr_12^0 == 0 /\ y^0-y^post1 == 0 /\ __disjvr_14^0-__disjvr_14^post1 == 0 /\ __disjvr_1^0-__disjvr_1^post1 == 0 /\ -__disjvr_3^post1+__disjvr_3^0 == 0 /\ -__disjvr_2^post1+__disjvr_2^0 == 0 /\ -__disjvr_11^post1+__disjvr_11^0 == 0 /\ __disjvr_10^0-__disjvr_10^post1 == 0 /\ __disjvr_7^0-__disjvr_7^post1 == 0 /\ __disjvr_6^0-__disjvr_6^post1 == 0), cost: 1
   2: l3 -> l4 : __disjvr_13^0'=__disjvr_13^post2, __disjvr_7^0'=__disjvr_7^post2, __disjvr_10^0'=__disjvr_10^post2, __disjvr_9^0'=__disjvr_9^post2, __disjvr_4^0'=__disjvr_4^post2, __disjvr_1^0'=__disjvr_1^post2, __disjvr_12^0'=__disjvr_12^post2, y^0'=y^post2, __disjvr_6^0'=__disjvr_6^post2, __disjvr_0^0'=__disjvr_0^post2, __disjvr_3^0'=__disjvr_3^post2, __disjvr_14^0'=__disjvr_14^post2, __disjvr_8^0'=__disjvr_8^post2, __disjvr_11^0'=__disjvr_11^post2, x^0'=x^post2, __disjvr_5^0'=__disjvr_5^post2, __disjvr_2^0'=__disjvr_2^post2, (-__disjvr_11^post2+__disjvr_11^0 == 0 /\ -__disjvr_8^post2+__disjvr_8^0 == 0 /\ __disjvr_12^0-__disjvr_12^post2 == 0 /\ __disjvr_7^0-__disjvr_7^post2 == 0 /\ -y^0+x^post2 == 0 /\ -__disjvr_2^post2+__disjvr_2^0 == 0 /\ -__disjvr_5^post2+__disjvr_5^0 == 0 /\ __disjvr_9^0-__disjvr_9^post2 == 0 /\ -x^0 <= 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ -__disjvr_14^post2+__disjvr_14^0 == 0 /\ __disjvr_3^0-__disjvr_3^post2 == 0 /\ __disjvr_4^0-__disjvr_4^post2 == 0 /\ -__disjvr_6^post2+__disjvr_6^0 == 0 /\ __disjvr_10^0-__disjvr_10^post2 == 0 /\ -__disjvr_1^post2+__disjvr_1^0 == 0 /\ x^0 <= 0 /\ y^0-y^post2 == 0 /\ __disjvr_13^0-__disjvr_13^post2 == 0), cost: 1
   3: l4 -> l5 : __disjvr_13^0'=__disjvr_13^post3, __disjvr_7^0'=__disjvr_7^post3, __disjvr_10^0'=__disjvr_10^post3, __disjvr_9^0'=__disjvr_9^post3, __disjvr_4^0'=__disjvr_4^post3, __disjvr_1^0'=__disjvr_1^post3, __disjvr_12^0'=__disjvr_12^post3, y^0'=y^post3, __disjvr_6^0'=__disjvr_6^post3, __disjvr_0^0'=__disjvr_0^post3, __disjvr_3^0'=__disjvr_3^post3, __disjvr_14^0'=__disjvr_14^post3, __disjvr_8^0'=__disjvr_8^post3, __disjvr_11^0'=__disjvr_11^post3, x^0'=x^post3, __disjvr_5^0'=__disjvr_5^post3, __disjvr_2^0'=__disjvr_2^post3, (-__disjvr_0^post3+__disjvr_0^0 == 0 /\ -__disjvr_5^post3+__disjvr_5^0 == 0 /\ __disjvr_12^0-__disjvr_12^post3 == 0 /\ __disjvr_9^0-__disjvr_9^post3 == 0 /\ -x^post3+x^0 == 0 /\ __disjvr_10^0-__disjvr_10^post3 == 0 /\ -__disjvr_6^post3+__disjvr_6^0 == 0 /\ __disjvr_1^post3-__disjvr_1^0 == 0 /\ -__disjvr_2^post3+__disjvr_2^0 == 0 /\ __disjvr_4^0-__disjvr_4^post3 == 0 /\ __disjvr_13^0-__disjvr_13^post3 == 0 /\ -__disjvr_3^post3+__disjvr_3^0 == 0 /\ __disjvr_8^0-__disjvr_8^post3 == 0 /\ -__disjvr_11^post3+__disjvr_11^0 == 0 /\ -__disjvr_7^post3+__disjvr_7^0 == 0 /\ -__disjvr_14^post3+__disjvr_14^0 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ y^0-y^post3 == 0), cost: 1
   4: l5 -> l6 : __disjvr_13^0'=__disjvr_13^post4, __disjvr_7^0'=__disjvr_7^post4, __disjvr_10^0'=__disjvr_10^post4, __disjvr_9^0'=__disjvr_9^post4, __disjvr_4^0'=__disjvr_4^post4, __disjvr_1^0'=__disjvr_1^post4, __disjvr_12^0'=__disjvr_12^post4, y^0'=y^post4, __disjvr_6^0'=__disjvr_6^post4, __disjvr_0^0'=__disjvr_0^post4, __disjvr_3^0'=__disjvr_3^post4, __disjvr_14^0'=__disjvr_14^post4, __disjvr_8^0'=__disjvr_8^post4, __disjvr_11^0'=__disjvr_11^post4, x^0'=x^post4, __disjvr_5^0'=__disjvr_5^post4, __disjvr_2^0'=__disjvr_2^post4, (__disjvr_11^0-__disjvr_11^post4 == 0 /\ -__disjvr_14^post4+__disjvr_14^0 == 0 /\ __disjvr_1^0-__disjvr_1^post4 == 0 /\ -__disjvr_0^post4+__disjvr_0^0 == 0 /\ -__disjvr_2^post4+__disjvr_2^0 == 0 /\ __disjvr_7^0-__disjvr_7^post4 == 0 /\ __disjvr_10^0-__disjvr_10^post4 == 0 /\ __disjvr_6^0-__disjvr_6^post4 == 0 /\ __disjvr_2^post4-__disjvr_2^0 == 0 /\ -__disjvr_3^post4+__disjvr_3^0 == 0 /\ __disjvr_9^0-__disjvr_9^post4 == 0 /\ -__disjvr_5^post4+__disjvr_5^0 == 0 /\ __disjvr_13^0-__disjvr_13^post4 == 0 /\ __disjvr_8^0-__disjvr_8^post4 == 0 /\ -y^post4+y^0 == 0 /\ -x^post4+x^0 == 0 /\ __disjvr_12^0-__disjvr_12^post4 == 0 /\ __disjvr_4^0-__disjvr_4^post4 == 0), cost: 1
   5: l6 -> l7 : __disjvr_13^0'=__disjvr_13^post5, __disjvr_7^0'=__disjvr_7^post5, __disjvr_10^0'=__disjvr_10^post5, __disjvr_9^0'=__disjvr_9^post5, __disjvr_4^0'=__disjvr_4^post5, __disjvr_1^0'=__disjvr_1^post5, __disjvr_12^0'=__disjvr_12^post5, y^0'=y^post5, __disjvr_6^0'=__disjvr_6^post5, __disjvr_0^0'=__disjvr_0^post5, __disjvr_3^0'=__disjvr_3^post5, __disjvr_14^0'=__disjvr_14^post5, __disjvr_8^0'=__disjvr_8^post5, __disjvr_11^0'=__disjvr_11^post5, x^0'=x^post5, __disjvr_5^0'=__disjvr_5^post5, __disjvr_2^0'=__disjvr_2^post5, (__disjvr_0^0-__disjvr_0^post5 == 0 /\ -__disjvr_5^post5+__disjvr_5^0 == 0 /\ -__disjvr_3^post5+__disjvr_3^0 == 0 /\ -__disjvr_9^post5+__disjvr_9^0 == 0 /\ -__disjvr_12^post5+__disjvr_12^0 == 0 /\ -__disjvr_8^post5+__disjvr_8^0 == 0 /\ __disjvr_6^0-__disjvr_6^post5 == 0 /\ __disjvr_11^0-__disjvr_11^post5 == 0 /\ __disjvr_14^0-__disjvr_14^post5 == 0 /\ -y^post5+y^0 == 0 /\ __disjvr_3^post5-__disjvr_3^0 == 0 /\ -x^post5+x^0 == 0 /\ __disjvr_1^0-__disjvr_1^post5 == 0 /\ __disjvr_4^0-__disjvr_4^post5 == 0 /\ __disjvr_10^0-__disjvr_10^post5 == 0 /\ -__disjvr_2^post5+__disjvr_2^0 == 0 /\ __disjvr_13^0-__disjvr_13^post5 == 0 /\ __disjvr_7^0-__disjvr_7^post5 == 0), cost: 1
   6: l7 -> l8 : __disjvr_13^0'=__disjvr_13^post6, __disjvr_7^0'=__disjvr_7^post6, __disjvr_10^0'=__disjvr_10^post6, __disjvr_9^0'=__disjvr_9^post6, __disjvr_4^0'=__disjvr_4^post6, __disjvr_1^0'=__disjvr_1^post6, __disjvr_12^0'=__disjvr_12^post6, y^0'=y^post6, __disjvr_6^0'=__disjvr_6^post6, __disjvr_0^0'=__disjvr_0^post6, __disjvr_3^0'=__disjvr_3^post6, __disjvr_14^0'=__disjvr_14^post6, __disjvr_8^0'=__disjvr_8^post6, __disjvr_11^0'=__disjvr_11^post6, x^0'=x^post6, __disjvr_5^0'=__disjvr_5^post6, __disjvr_2^0'=__disjvr_2^post6, (-__disjvr_11^post6+__disjvr_11^0 == 0 /\ __disjvr_5^0-__disjvr_5^post6 == 0 /\ -__disjvr_6^post6+__disjvr_6^0 == 0 /\ __disjvr_7^0-__disjvr_7^post6 == 0 /\ -__disjvr_2^post6+__disjvr_2^0 == 0 /\ y^0-y^post6 == 0 /\ __disjvr_0^0-__disjvr_0^post6 == 0 /\ __disjvr_10^0-__disjvr_10^post6 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ -__disjvr_8^post6+__disjvr_8^0 == 0 /\ __disjvr_13^0-__disjvr_13^post6 == 0 /\ __disjvr_3^0-__disjvr_3^post6 == 0 /\ -__disjvr_14^post6+__disjvr_14^0 == 0 /\ __disjvr_9^0-__disjvr_9^post6 == 0 /\ -__disjvr_4^0+__disjvr_4^post6 == 0 /\ -x^post6+x^0 == 0 /\ __disjvr_4^0-__disjvr_4^post6 == 0 /\ __disjvr_12^0-__disjvr_12^post6 == 0), cost: 1
   7: l8 -> l9 : __disjvr_13^0'=__disjvr_13^post7, __disjvr_7^0'=__disjvr_7^post7, __disjvr_10^0'=__disjvr_10^post7, __disjvr_9^0'=__disjvr_9^post7, __disjvr_4^0'=__disjvr_4^post7, __disjvr_1^0'=__disjvr_1^post7, __disjvr_12^0'=__disjvr_12^post7, y^0'=y^post7, __disjvr_6^0'=__disjvr_6^post7, __disjvr_0^0'=__disjvr_0^post7, __disjvr_3^0'=__disjvr_3^post7, __disjvr_14^0'=__disjvr_14^post7, __disjvr_8^0'=__disjvr_8^post7, __disjvr_11^0'=__disjvr_11^post7, x^0'=x^post7, __disjvr_5^0'=__disjvr_5^post7, __disjvr_2^0'=__disjvr_2^post7, (-__disjvr_1^post7+__disjvr_1^0 == 0 /\ __disjvr_12^0-__disjvr_12^post7 == 0 /\ __disjvr_9^0-__disjvr_9^post7 == 0 /\ -__disjvr_5^post7+__disjvr_5^0 == 0 /\ -__disjvr_14^post7+__disjvr_14^0 == 0 /\ __disjvr_3^0-__disjvr_3^post7 == 0 /\ -x^post7+x^0 == 0 /\ __disjvr_5^post7-__disjvr_5^0 == 0 /\ -__disjvr_8^post7+__disjvr_8^0 == 0 /\ __disjvr_4^0-__disjvr_4^post7 == 0 /\ -__disjvr_6^post7+__disjvr_6^0 == 0 /\ __disjvr_10^0-__disjvr_10^post7 == 0 /\ -__disjvr_2^post7+__disjvr_2^0 == 0 /\ -__disjvr_11^post7+__disjvr_11^0 == 0 /\ -__disjvr_0^post7+__disjvr_0^0 == 0 /\ __disjvr_13^0-__disjvr_13^post7 == 0 /\ y^0-y^post7 == 0 /\ -__disjvr_7^post7+__disjvr_7^0 == 0), cost: 1
   8: l9 -> l10 : __disjvr_13^0'=__disjvr_13^post8, __disjvr_7^0'=__disjvr_7^post8, __disjvr_10^0'=__disjvr_10^post8, __disjvr_9^0'=__disjvr_9^post8, __disjvr_4^0'=__disjvr_4^post8, __disjvr_1^0'=__disjvr_1^post8, __disjvr_12^0'=__disjvr_12^post8, y^0'=y^post8, __disjvr_6^0'=__disjvr_6^post8, __disjvr_0^0'=__disjvr_0^post8, __disjvr_3^0'=__disjvr_3^post8, __disjvr_14^0'=__disjvr_14^post8, __disjvr_8^0'=__disjvr_8^post8, __disjvr_11^0'=__disjvr_11^post8, x^0'=x^post8, __disjvr_5^0'=__disjvr_5^post8, __disjvr_2^0'=__disjvr_2^post8, (__disjvr_11^0-__disjvr_11^post8 == 0 /\ __disjvr_7^0-__disjvr_7^post8 == 0 /\ -__disjvr_3^post8+__disjvr_3^0 == 0 /\ -__disjvr_2^post8+__disjvr_2^0 == 0 /\ __disjvr_1^0-__disjvr_1^post8 == 0 /\ __disjvr_10^0-__disjvr_10^post8 == 0 /\ __disjvr_13^0-__disjvr_13^post8 == 0 /\ __disjvr_8^0-__disjvr_8^post8 == 0 /\ -__disjvr_6^post8+__disjvr_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post8 == 0 /\ -__disjvr_14^post8+__disjvr_14^0 == 0 /\ -__disjvr_5^post8+__disjvr_5^0 == 0 /\ -__disjvr_9^post8+__disjvr_9^0 == 0 /\ __disjvr_6^post8-__disjvr_6^0 == 0 /\ -y^post8+y^0 == 0 /\ __disjvr_4^0-__disjvr_4^post8 == 0 /\ __disjvr_12^0-__disjvr_12^post8 == 0 /\ -x^post8+x^0 == 0), cost: 1
   9: l10 -> l11 : __disjvr_13^0'=__disjvr_13^post9, __disjvr_7^0'=__disjvr_7^post9, __disjvr_10^0'=__disjvr_10^post9, __disjvr_9^0'=__disjvr_9^post9, __disjvr_4^0'=__disjvr_4^post9, __disjvr_1^0'=__disjvr_1^post9, __disjvr_12^0'=__disjvr_12^post9, y^0'=y^post9, __disjvr_6^0'=__disjvr_6^post9, __disjvr_0^0'=__disjvr_0^post9, __disjvr_3^0'=__disjvr_3^post9, __disjvr_14^0'=__disjvr_14^post9, __disjvr_8^0'=__disjvr_8^post9, __disjvr_11^0'=__disjvr_11^post9, x^0'=x^post9, __disjvr_5^0'=__disjvr_5^post9, __disjvr_2^0'=__disjvr_2^post9, (-__disjvr_5^post9+__disjvr_5^0 == 0 /\ -__disjvr_9^post9+__disjvr_9^0 == 0 /\ __disjvr_14^0-__disjvr_14^post9 == 0 /\ -x^post9+x^0 == 0 /\ -__disjvr_12^post9+__disjvr_12^0 == 0 /\ __disjvr_11^0-__disjvr_11^post9 == 0 /\ __disjvr_1^0-__disjvr_1^post9 == 0 /\ -__disjvr_3^post9+__disjvr_3^0 == 0 /\ __disjvr_4^0-__disjvr_4^post9 == 0 /\ -__disjvr_7^0+__disjvr_7^post9 == 0 /\ -__disjvr_8^post9+__disjvr_8^0 == 0 /\ -__disjvr_2^post9+__disjvr_2^0 == 0 /\ __disjvr_10^0-__disjvr_10^post9 == 0 /\ y^0-y^post9 == 0 /\ __disjvr_0^0-__disjvr_0^post9 == 0 /\ __disjvr_13^0-__disjvr_13^post9 == 0 /\ __disjvr_7^0-__disjvr_7^post9 == 0 /\ __disjvr_6^0-__disjvr_6^post9 == 0), cost: 1
  10: l11 -> l12 : __disjvr_13^0'=__disjvr_13^post10, __disjvr_7^0'=__disjvr_7^post10, __disjvr_10^0'=__disjvr_10^post10, __disjvr_9^0'=__disjvr_9^post10, __disjvr_4^0'=__disjvr_4^post10, __disjvr_1^0'=__disjvr_1^post10, __disjvr_12^0'=__disjvr_12^post10, y^0'=y^post10, __disjvr_6^0'=__disjvr_6^post10, __disjvr_0^0'=__disjvr_0^post10, __disjvr_3^0'=__disjvr_3^post10, __disjvr_14^0'=__disjvr_14^post10, __disjvr_8^0'=__disjvr_8^post10, __disjvr_11^0'=__disjvr_11^post10, x^0'=x^post10, __disjvr_5^0'=__disjvr_5^post10, __disjvr_2^0'=__disjvr_2^post10, (-__disjvr_6^post10+__disjvr_6^0 == 0 /\ -__disjvr_8^post10+__disjvr_8^0 == 0 /\ __disjvr_5^0-__disjvr_5^post10 == 0 /\ __disjvr_7^0-__disjvr_7^post10 == 0 /\ -__disjvr_2^post10+__disjvr_2^0 == 0 /\ -__disjvr_11^post10+__disjvr_11^0 == 0 /\ y^0-y^post10 == 0 /\ __disjvr_8^post10-__disjvr_8^0 == 0 /\ __disjvr_10^0-__disjvr_10^post10 == 0 /\ __disjvr_9^0-__disjvr_9^post10 == 0 /\ __disjvr_3^0-__disjvr_3^post10 == 0 /\ -__disjvr_1^post10+__disjvr_1^0 == 0 /\ __disjvr_13^0-__disjvr_13^post10 == 0 /\ -__disjvr_14^post10+__disjvr_14^0 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ __disjvr_4^0-__disjvr_4^post10 == 0 /\ -x^post10+x^0 == 0 /\ __disjvr_12^0-__disjvr_12^post10 == 0), cost: 1
  11: l12 -> l13 : __disjvr_13^0'=__disjvr_13^post11, __disjvr_7^0'=__disjvr_7^post11, __disjvr_10^0'=__disjvr_10^post11, __disjvr_9^0'=__disjvr_9^post11, __disjvr_4^0'=__disjvr_4^post11, __disjvr_1^0'=__disjvr_1^post11, __disjvr_12^0'=__disjvr_12^post11, y^0'=y^post11, __disjvr_6^0'=__disjvr_6^post11, __disjvr_0^0'=__disjvr_0^post11, __disjvr_3^0'=__disjvr_3^post11, __disjvr_14^0'=__disjvr_14^post11, __disjvr_8^0'=__disjvr_8^post11, __disjvr_11^0'=__disjvr_11^post11, x^0'=x^post11, __disjvr_5^0'=__disjvr_5^post11, __disjvr_2^0'=__disjvr_2^post11, (__disjvr_3^0-__disjvr_3^post11 == 0 /\ -__disjvr_8^post11+__disjvr_8^0 == 0 /\ __disjvr_13^0-__disjvr_13^post11 == 0 /\ x^0-x^post11 == 0 /\ -__disjvr_2^post11+__disjvr_2^0 == 0 /\ -__disjvr_11^post11+__disjvr_11^0 == 0 /\ -y^post11+y^0 == 0 /\ __disjvr_7^0-__disjvr_7^post11 == 0 /\ -__disjvr_6^post11+__disjvr_6^0 == 0 /\ -__disjvr_9^0+__disjvr_9^post11 == 0 /\ -__disjvr_14^post11+__disjvr_14^0 == 0 /\ -__disjvr_5^post11+__disjvr_5^0 == 0 /\ __disjvr_12^0-__disjvr_12^post11 == 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0 /\ __disjvr_10^0-__disjvr_10^post11 == 0 /\ __disjvr_9^0-__disjvr_9^post11 == 0 /\ -__disjvr_4^post11+__disjvr_4^0 == 0 /\ __disjvr_1^0-__disjvr_1^post11 == 0), cost: 1
  12: l13 -> l14 : __disjvr_13^0'=__disjvr_13^post12, __disjvr_7^0'=__disjvr_7^post12, __disjvr_10^0'=__disjvr_10^post12, __disjvr_9^0'=__disjvr_9^post12, __disjvr_4^0'=__disjvr_4^post12, __disjvr_1^0'=__disjvr_1^post12, __disjvr_12^0'=__disjvr_12^post12, y^0'=y^post12, __disjvr_6^0'=__disjvr_6^post12, __disjvr_0^0'=__disjvr_0^post12, __disjvr_3^0'=__disjvr_3^post12, __disjvr_14^0'=__disjvr_14^post12, __disjvr_8^0'=__disjvr_8^post12, __disjvr_11^0'=__disjvr_11^post12, x^0'=x^post12, __disjvr_5^0'=__disjvr_5^post12, __disjvr_2^0'=__disjvr_2^post12, (-__disjvr_5^post12+__disjvr_5^0 == 0 /\ __disjvr_11^0-__disjvr_11^post12 == 0 /\ __disjvr_1^0-__disjvr_1^post12 == 0 /\ __disjvr_14^0-__disjvr_14^post12 == 0 /\ __disjvr_6^0-__disjvr_6^post12 == 0 /\ -x^post12+x^0 == 0 /\ -__disjvr_8^post12+__disjvr_8^0 == 0 /\ __disjvr_10^0-__disjvr_10^post12 == 0 /\ -__disjvr_3^post12+__disjvr_3^0 == 0 /\ -__disjvr_2^post12+__disjvr_2^0 == 0 /\ __disjvr_13^0-__disjvr_13^post12 == 0 /\ __disjvr_12^0-__disjvr_12^post12 == 0 /\ __disjvr_4^0-__disjvr_4^post12 == 0 /\ __disjvr_0^0-__disjvr_0^post12 == 0 /\ -__disjvr_10^0+__disjvr_10^post12 == 0 /\ -__disjvr_9^post12+__disjvr_9^0 == 0 /\ -y^post12+y^0 == 0 /\ __disjvr_7^0-__disjvr_7^post12 == 0), cost: 1
  13: l14 -> l15 : __disjvr_13^0'=__disjvr_13^post13, __disjvr_7^0'=__disjvr_7^post13, __disjvr_10^0'=__disjvr_10^post13, __disjvr_9^0'=__disjvr_9^post13, __disjvr_4^0'=__disjvr_4^post13, __disjvr_1^0'=__disjvr_1^post13, __disjvr_12^0'=__disjvr_12^post13, y^0'=y^post13, __disjvr_6^0'=__disjvr_6^post13, __disjvr_0^0'=__disjvr_0^post13, __disjvr_3^0'=__disjvr_3^post13, __disjvr_14^0'=__disjvr_14^post13, __disjvr_8^0'=__disjvr_8^post13, __disjvr_11^0'=__disjvr_11^post13, x^0'=x^post13, __disjvr_5^0'=__disjvr_5^post13, __disjvr_2^0'=__disjvr_2^post13, (__disjvr_0^0-__disjvr_0^post13 == 0 /\ __disjvr_13^0-__disjvr_13^post13 == 0 /\ -__disjvr_3^post13+__disjvr_3^0 == 0 /\ -__disjvr_8^post13+__disjvr_8^0 == 0 /\ -__disjvr_12^post13+__disjvr_12^0 == 0 /\ -__disjvr_2^post13+__disjvr_2^0 == 0 /\ -__disjvr_11^post13+__disjvr_11^0 == 0 /\ __disjvr_4^0-__disjvr_4^post13 == 0 /\ __disjvr_11^post13-__disjvr_11^0 == 0 /\ y^0-y^post13 == 0 /\ __disjvr_14^0-__disjvr_14^post13 == 0 /\ -__disjvr_5^post13+__disjvr_5^0 == 0 /\ __disjvr_7^0-__disjvr_7^post13 == 0 /\ __disjvr_9^0-__disjvr_9^post13 == 0 /\ __disjvr_6^0-__disjvr_6^post13 == 0 /\ -x^post13+x^0 == 0 /\ __disjvr_10^0-__disjvr_10^post13 == 0 /\ __disjvr_1^0-__disjvr_1^post13 == 0), cost: 1
  14: l15 -> l16 : __disjvr_13^0'=__disjvr_13^post14, __disjvr_7^0'=__disjvr_7^post14, __disjvr_10^0'=__disjvr_10^post14, __disjvr_9^0'=__disjvr_9^post14, __disjvr_4^0'=__disjvr_4^post14, __disjvr_1^0'=__disjvr_1^post14, __disjvr_12^0'=__disjvr_12^post14, y^0'=y^post14, __disjvr_6^0'=__disjvr_6^post14, __disjvr_0^0'=__disjvr_0^post14, __disjvr_3^0'=__disjvr_3^post14, __disjvr_14^0'=__disjvr_14^post14, __disjvr_8^0'=__disjvr_8^post14, __disjvr_11^0'=__disjvr_11^post14, x^0'=x^post14, __disjvr_5^0'=__disjvr_5^post14, __disjvr_2^0'=__disjvr_2^post14, (-__disjvr_5^post14+__disjvr_5^0 == 0 /\ -__disjvr_14^post14+__disjvr_14^0 == 0 /\ -__disjvr_0^post14+__disjvr_0^0 == 0 /\ __disjvr_3^0-__disjvr_3^post14 == 0 /\ __disjvr_9^0-__disjvr_9^post14 == 0 /\ __disjvr_10^0-__disjvr_10^post14 == 0 /\ -__disjvr_6^post14+__disjvr_6^0 == 0 /\ -x^post14+x^0 == 0 /\ -__disjvr_12^0+__disjvr_12^post14 == 0 /\ -__disjvr_8^post14+__disjvr_8^0 == 0 /\ -__disjvr_11^post14+__disjvr_11^0 == 0 /\ -__disjvr_1^post14+__disjvr_1^0 == 0 /\ -__disjvr_2^post14+__disjvr_2^0 == 0 /\ __disjvr_12^0-__disjvr_12^post14 == 0 /\ __disjvr_13^0-__disjvr_13^post14 == 0 /\ __disjvr_4^0-__disjvr_4^post14 == 0 /\ y^0-y^post14 == 0 /\ -__disjvr_7^post14+__disjvr_7^0 == 0), cost: 1
  15: l16 -> l17 : __disjvr_13^0'=__disjvr_13^post15, __disjvr_7^0'=__disjvr_7^post15, __disjvr_10^0'=__disjvr_10^post15, __disjvr_9^0'=__disjvr_9^post15, __disjvr_4^0'=__disjvr_4^post15, __disjvr_1^0'=__disjvr_1^post15, __disjvr_12^0'=__disjvr_12^post15, y^0'=y^post15, __disjvr_6^0'=__disjvr_6^post15, __disjvr_0^0'=__disjvr_0^post15, __disjvr_3^0'=__disjvr_3^post15, __disjvr_14^0'=__disjvr_14^post15, __disjvr_8^0'=__disjvr_8^post15, __disjvr_11^0'=__disjvr_11^post15, x^0'=x^post15, __disjvr_5^0'=__disjvr_5^post15, __disjvr_2^0'=__disjvr_2^post15, (x^0-x^post15 == 0 /\ __disjvr_1^0-__disjvr_1^post15 == 0 /\ __disjvr_3^0-__disjvr_3^post15 == 0 /\ __disjvr_10^0-__disjvr_10^post15 == 0 /\ __disjvr_13^0-__disjvr_13^post15 == 0 /\ -__disjvr_8^post15+__disjvr_8^0 == 0 /\ -__disjvr_2^post15+__disjvr_2^0 == 0 /\ -__disjvr_11^post15+__disjvr_11^0 == 0 /\ -__disjvr_13^0+__disjvr_13^post15 == 0 /\ -y^post15+y^0 == 0 /\ __disjvr_7^0-__disjvr_7^post15 == 0 /\ -__disjvr_4^post15+__disjvr_4^0 == 0 /\ -__disjvr_6^post15+__disjvr_6^0 == 0 /\ -__disjvr_5^post15+__disjvr_5^0 == 0 /\ __disjvr_9^0-__disjvr_9^post15 == 0 /\ -__disjvr_0^post15+__disjvr_0^0 == 0 /\ -__disjvr_14^post15+__disjvr_14^0 == 0 /\ __disjvr_12^0-__disjvr_12^post15 == 0), cost: 1
  16: l17 -> l2 : __disjvr_13^0'=__disjvr_13^post16, __disjvr_7^0'=__disjvr_7^post16, __disjvr_10^0'=__disjvr_10^post16, __disjvr_9^0'=__disjvr_9^post16, __disjvr_4^0'=__disjvr_4^post16, __disjvr_1^0'=__disjvr_1^post16, __disjvr_12^0'=__disjvr_12^post16, y^0'=y^post16, __disjvr_6^0'=__disjvr_6^post16, __disjvr_0^0'=__disjvr_0^post16, __disjvr_3^0'=__disjvr_3^post16, __disjvr_14^0'=__disjvr_14^post16, __disjvr_8^0'=__disjvr_8^post16, __disjvr_11^0'=__disjvr_11^post16, x^0'=x^post16, __disjvr_5^0'=__disjvr_5^post16, __disjvr_2^0'=__disjvr_2^post16, (-__disjvr_14^0+__disjvr_14^post16 == 0 /\ __disjvr_7^0-__disjvr_7^post16 == 0 /\ -__disjvr_5^post16+__disjvr_5^0 == 0 /\ -y^post16+y^0 == 0 /\ __disjvr_6^0-__disjvr_6^post16 == 0 /\ -x^post16+x^0 == 0 /\ __disjvr_1^0-__disjvr_1^post16 == 0 /\ __disjvr_14^0-__disjvr_14^post16 == 0 /\ __disjvr_11^0-__disjvr_11^post16 == 0 /\ __disjvr_10^0-__disjvr_10^post16 == 0 /\ -__disjvr_8^post16+__disjvr_8^0 == 0 /\ -__disjvr_3^post16+__disjvr_3^0 == 0 /\ __disjvr_13^0-__disjvr_13^post16 == 0 /\ -__disjvr_2^post16+__disjvr_2^0 == 0 /\ -__disjvr_9^post16+__disjvr_9^0 == 0 /\ __disjvr_4^0-__disjvr_4^post16 == 0 /\ __disjvr_0^0-__disjvr_0^post16 == 0 /\ __disjvr_12^0-__disjvr_12^post16 == 0), cost: 1
  17: l2 -> l1 : __disjvr_13^0'=__disjvr_13^post17, __disjvr_7^0'=__disjvr_7^post17, __disjvr_10^0'=__disjvr_10^post17, __disjvr_9^0'=__disjvr_9^post17, __disjvr_4^0'=__disjvr_4^post17, __disjvr_1^0'=__disjvr_1^post17, __disjvr_12^0'=__disjvr_12^post17, y^0'=y^post17, __disjvr_6^0'=__disjvr_6^post17, __disjvr_0^0'=__disjvr_0^post17, __disjvr_3^0'=__disjvr_3^post17, __disjvr_14^0'=__disjvr_14^post17, __disjvr_8^0'=__disjvr_8^post17, __disjvr_11^0'=__disjvr_11^post17, x^0'=x^post17, __disjvr_5^0'=__disjvr_5^post17, __disjvr_2^0'=__disjvr_2^post17, (-__disjvr_3^post17+__disjvr_3^0 == 0 /\ -__disjvr_1^post17+__disjvr_1^0 == 0 /\ __disjvr_4^0-__disjvr_4^post17 == 0 /\ -__disjvr_8^post17+__disjvr_8^0 == 0 /\ -__disjvr_11^post17+__disjvr_11^0 == 0 /\ __disjvr_13^0-__disjvr_13^post17 == 0 /\ -__disjvr_12^post17+__disjvr_12^0 == 0 /\ __disjvr_7^0-__disjvr_7^post17 == 0 /\ y^0-y^post17 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ __disjvr_14^0-__disjvr_14^post17 == 0 /\ -__disjvr_5^post17+__disjvr_5^0 == 0 /\ __disjvr_9^0-__disjvr_9^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ __disjvr_6^0-__disjvr_6^post17 == 0 /\ -__disjvr_10^post17+__disjvr_10^0 == 0 /\ -x^post17+x^0 == 0), cost: 1
  18: l18 -> l0 : __disjvr_13^0'=__disjvr_13^post18, __disjvr_7^0'=__disjvr_7^post18, __disjvr_10^0'=__disjvr_10^post18, __disjvr_9^0'=__disjvr_9^post18, __disjvr_4^0'=__disjvr_4^post18, __disjvr_1^0'=__disjvr_1^post18, __disjvr_12^0'=__disjvr_12^post18, y^0'=y^post18, __disjvr_6^0'=__disjvr_6^post18, __disjvr_0^0'=__disjvr_0^post18, __disjvr_3^0'=__disjvr_3^post18, __disjvr_14^0'=__disjvr_14^post18, __disjvr_8^0'=__disjvr_8^post18, __disjvr_11^0'=__disjvr_11^post18, x^0'=x^post18, __disjvr_5^0'=__disjvr_5^post18, __disjvr_2^0'=__disjvr_2^post18, (__disjvr_4^0-__disjvr_4^post18 == 0 /\ y^0-y^post18 == 0 /\ -__disjvr_0^post18+__disjvr_0^0 == 0 /\ __disjvr_5^0-__disjvr_5^post18 == 0 /\ -__disjvr_14^post18+__disjvr_14^0 == 0 /\ -__disjvr_1^post18+__disjvr_1^0 == 0 /\ __disjvr_7^0-__disjvr_7^post18 == 0 /\ __disjvr_3^0-__disjvr_3^post18 == 0 /\ -x^post18+x^0 == 0 /\ __disjvr_13^0-__disjvr_13^post18 == 0 /\ -__disjvr_12^post18+__disjvr_12^0 == 0 /\ -__disjvr_2^post18+__disjvr_2^0 == 0 /\ __disjvr_9^0-__disjvr_9^post18 == 0 /\ __disjvr_6^0-__disjvr_6^post18 == 0 /\ -__disjvr_8^post18+__disjvr_8^0 == 0 /\ -__disjvr_11^post18+__disjvr_11^0 == 0 /\ -__disjvr_10^post18+__disjvr_10^0 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : __disjvr_13^0'=__disjvr_13^post0, __disjvr_7^0'=__disjvr_7^post0, __disjvr_10^0'=__disjvr_10^post0, __disjvr_9^0'=__disjvr_9^post0, __disjvr_4^0'=__disjvr_4^post0, __disjvr_1^0'=__disjvr_1^post0, __disjvr_12^0'=__disjvr_12^post0, y^0'=y^post0, __disjvr_6^0'=__disjvr_6^post0, __disjvr_0^0'=__disjvr_0^post0, __disjvr_3^0'=__disjvr_3^post0, __disjvr_14^0'=__disjvr_14^post0, __disjvr_8^0'=__disjvr_8^post0, __disjvr_11^0'=__disjvr_11^post0, x^0'=x^post0, __disjvr_5^0'=__disjvr_5^post0, __disjvr_2^0'=__disjvr_2^post0, (-x^post0+x^0 == 0 /\ -__disjvr_12^post0+__disjvr_12^0 == 0 /\ __disjvr_6^0-__disjvr_6^post0 == 0 /\ __disjvr_7^0-__disjvr_7^post0 == 0 /\ __disjvr_11^0-__disjvr_11^post0 == 0 /\ -__disjvr_3^post0+__disjvr_3^0 == 0 /\ __disjvr_1^0-__disjvr_1^post0 == 0 /\ -y^post0+y^0 == 0 /\ -__disjvr_14^post0+__disjvr_14^0 == 0 /\ __disjvr_8^0-__disjvr_8^post0 == 0 /\ __disjvr_0^0-__disjvr_0^post0 == 0 /\ __disjvr_4^0-__disjvr_4^post0 == 0 /\ __disjvr_10^0-__disjvr_10^post0 == 0 /\ -__disjvr_5^post0+__disjvr_5^0 == 0 /\ -__disjvr_2^post0+__disjvr_2^0 == 0 /\ __disjvr_13^0-__disjvr_13^post0 == 0 /\ -__disjvr_9^post0+__disjvr_9^0 == 0), cost: 1
New rule:
l0 -> l1 : TRUE, cost: 1

Applied preprocessing
Original rule:
l1 -> l3 : __disjvr_13^0'=__disjvr_13^post1, __disjvr_7^0'=__disjvr_7^post1, __disjvr_10^0'=__disjvr_10^post1, __disjvr_9^0'=__disjvr_9^post1, __disjvr_4^0'=__disjvr_4^post1, __disjvr_1^0'=__disjvr_1^post1, __disjvr_12^0'=__disjvr_12^post1, y^0'=y^post1, __disjvr_6^0'=__disjvr_6^post1, __disjvr_0^0'=__disjvr_0^post1, __disjvr_3^0'=__disjvr_3^post1, __disjvr_14^0'=__disjvr_14^post1, __disjvr_8^0'=__disjvr_8^post1, __disjvr_11^0'=__disjvr_11^post1, x^0'=x^post1, __disjvr_5^0'=__disjvr_5^post1, __disjvr_2^0'=__disjvr_2^post1, (-__disjvr_0^0+__disjvr_0^post1 == 0 /\ __disjvr_9^0-__disjvr_9^post1 == 0 /\ __disjvr_13^0-__disjvr_13^post1 == 0 /\ -__disjvr_8^post1+__disjvr_8^0 == 0 /\ -__disjvr_5^post1+__disjvr_5^0 == 0 /\ __disjvr_0^0-__disjvr_0^post1 == 0 /\ __disjvr_4^0-__disjvr_4^post1 == 0 /\ -x^post1+x^0 == 0 /\ -__disjvr_12^post1+__disjvr_12^0 == 0 /\ y^0-y^post1 == 0 /\ __disjvr_14^0-__disjvr_14^post1 == 0 /\ __disjvr_1^0-__disjvr_1^post1 == 0 /\ -__disjvr_3^post1+__disjvr_3^0 == 0 /\ -__disjvr_2^post1+__disjvr_2^0 == 0 /\ -__disjvr_11^post1+__disjvr_11^0 == 0 /\ __disjvr_10^0-__disjvr_10^post1 == 0 /\ __disjvr_7^0-__disjvr_7^post1 == 0 /\ __disjvr_6^0-__disjvr_6^post1 == 0), cost: 1
New rule:
l1 -> l3 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l4 : __disjvr_13^0'=__disjvr_13^post2, __disjvr_7^0'=__disjvr_7^post2, __disjvr_10^0'=__disjvr_10^post2, __disjvr_9^0'=__disjvr_9^post2, __disjvr_4^0'=__disjvr_4^post2, __disjvr_1^0'=__disjvr_1^post2, __disjvr_12^0'=__disjvr_12^post2, y^0'=y^post2, __disjvr_6^0'=__disjvr_6^post2, __disjvr_0^0'=__disjvr_0^post2, __disjvr_3^0'=__disjvr_3^post2, __disjvr_14^0'=__disjvr_14^post2, __disjvr_8^0'=__disjvr_8^post2, __disjvr_11^0'=__disjvr_11^post2, x^0'=x^post2, __disjvr_5^0'=__disjvr_5^post2, __disjvr_2^0'=__disjvr_2^post2, (-__disjvr_11^post2+__disjvr_11^0 == 0 /\ -__disjvr_8^post2+__disjvr_8^0 == 0 /\ __disjvr_12^0-__disjvr_12^post2 == 0 /\ __disjvr_7^0-__disjvr_7^post2 == 0 /\ -y^0+x^post2 == 0 /\ -__disjvr_2^post2+__disjvr_2^0 == 0 /\ -__disjvr_5^post2+__disjvr_5^0 == 0 /\ __disjvr_9^0-__disjvr_9^post2 == 0 /\ -x^0 <= 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ -__disjvr_14^post2+__disjvr_14^0 == 0 /\ __disjvr_3^0-__disjvr_3^post2 == 0 /\ __disjvr_4^0-__disjvr_4^post2 == 0 /\ -__disjvr_6^post2+__disjvr_6^0 == 0 /\ __disjvr_10^0-__disjvr_10^post2 == 0 /\ -__disjvr_1^post2+__disjvr_1^0 == 0 /\ x^0 <= 0 /\ y^0-y^post2 == 0 /\ __disjvr_13^0-__disjvr_13^post2 == 0), cost: 1
New rule:
l3 -> l4 : x^0'=y^0, x^0 == 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l5 : __disjvr_13^0'=__disjvr_13^post3, __disjvr_7^0'=__disjvr_7^post3, __disjvr_10^0'=__disjvr_10^post3, __disjvr_9^0'=__disjvr_9^post3, __disjvr_4^0'=__disjvr_4^post3, __disjvr_1^0'=__disjvr_1^post3, __disjvr_12^0'=__disjvr_12^post3, y^0'=y^post3, __disjvr_6^0'=__disjvr_6^post3, __disjvr_0^0'=__disjvr_0^post3, __disjvr_3^0'=__disjvr_3^post3, __disjvr_14^0'=__disjvr_14^post3, __disjvr_8^0'=__disjvr_8^post3, __disjvr_11^0'=__disjvr_11^post3, x^0'=x^post3, __disjvr_5^0'=__disjvr_5^post3, __disjvr_2^0'=__disjvr_2^post3, (-__disjvr_0^post3+__disjvr_0^0 == 0 /\ -__disjvr_5^post3+__disjvr_5^0 == 0 /\ __disjvr_12^0-__disjvr_12^post3 == 0 /\ __disjvr_9^0-__disjvr_9^post3 == 0 /\ -x^post3+x^0 == 0 /\ __disjvr_10^0-__disjvr_10^post3 == 0 /\ -__disjvr_6^post3+__disjvr_6^0 == 0 /\ __disjvr_1^post3-__disjvr_1^0 == 0 /\ -__disjvr_2^post3+__disjvr_2^0 == 0 /\ __disjvr_4^0-__disjvr_4^post3 == 0 /\ __disjvr_13^0-__disjvr_13^post3 == 0 /\ -__disjvr_3^post3+__disjvr_3^0 == 0 /\ __disjvr_8^0-__disjvr_8^post3 == 0 /\ -__disjvr_11^post3+__disjvr_11^0 == 0 /\ -__disjvr_7^post3+__disjvr_7^0 == 0 /\ -__disjvr_14^post3+__disjvr_14^0 == 0 /\ -__disjvr_1^post3+__disjvr_1^0 == 0 /\ y^0-y^post3 == 0), cost: 1
New rule:
l4 -> l5 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l6 : __disjvr_13^0'=__disjvr_13^post4, __disjvr_7^0'=__disjvr_7^post4, __disjvr_10^0'=__disjvr_10^post4, __disjvr_9^0'=__disjvr_9^post4, __disjvr_4^0'=__disjvr_4^post4, __disjvr_1^0'=__disjvr_1^post4, __disjvr_12^0'=__disjvr_12^post4, y^0'=y^post4, __disjvr_6^0'=__disjvr_6^post4, __disjvr_0^0'=__disjvr_0^post4, __disjvr_3^0'=__disjvr_3^post4, __disjvr_14^0'=__disjvr_14^post4, __disjvr_8^0'=__disjvr_8^post4, __disjvr_11^0'=__disjvr_11^post4, x^0'=x^post4, __disjvr_5^0'=__disjvr_5^post4, __disjvr_2^0'=__disjvr_2^post4, (__disjvr_11^0-__disjvr_11^post4 == 0 /\ -__disjvr_14^post4+__disjvr_14^0 == 0 /\ __disjvr_1^0-__disjvr_1^post4 == 0 /\ -__disjvr_0^post4+__disjvr_0^0 == 0 /\ -__disjvr_2^post4+__disjvr_2^0 == 0 /\ __disjvr_7^0-__disjvr_7^post4 == 0 /\ __disjvr_10^0-__disjvr_10^post4 == 0 /\ __disjvr_6^0-__disjvr_6^post4 == 0 /\ __disjvr_2^post4-__disjvr_2^0 == 0 /\ -__disjvr_3^post4+__disjvr_3^0 == 0 /\ __disjvr_9^0-__disjvr_9^post4 == 0 /\ -__disjvr_5^post4+__disjvr_5^0 == 0 /\ __disjvr_13^0-__disjvr_13^post4 == 0 /\ __disjvr_8^0-__disjvr_8^post4 == 0 /\ -y^post4+y^0 == 0 /\ -x^post4+x^0 == 0 /\ __disjvr_12^0-__disjvr_12^post4 == 0 /\ __disjvr_4^0-__disjvr_4^post4 == 0), cost: 1
New rule:
l5 -> l6 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l7 : __disjvr_13^0'=__disjvr_13^post5, __disjvr_7^0'=__disjvr_7^post5, __disjvr_10^0'=__disjvr_10^post5, __disjvr_9^0'=__disjvr_9^post5, __disjvr_4^0'=__disjvr_4^post5, __disjvr_1^0'=__disjvr_1^post5, __disjvr_12^0'=__disjvr_12^post5, y^0'=y^post5, __disjvr_6^0'=__disjvr_6^post5, __disjvr_0^0'=__disjvr_0^post5, __disjvr_3^0'=__disjvr_3^post5, __disjvr_14^0'=__disjvr_14^post5, __disjvr_8^0'=__disjvr_8^post5, __disjvr_11^0'=__disjvr_11^post5, x^0'=x^post5, __disjvr_5^0'=__disjvr_5^post5, __disjvr_2^0'=__disjvr_2^post5, (__disjvr_0^0-__disjvr_0^post5 == 0 /\ -__disjvr_5^post5+__disjvr_5^0 == 0 /\ -__disjvr_3^post5+__disjvr_3^0 == 0 /\ -__disjvr_9^post5+__disjvr_9^0 == 0 /\ -__disjvr_12^post5+__disjvr_12^0 == 0 /\ -__disjvr_8^post5+__disjvr_8^0 == 0 /\ __disjvr_6^0-__disjvr_6^post5 == 0 /\ __disjvr_11^0-__disjvr_11^post5 == 0 /\ __disjvr_14^0-__disjvr_14^post5 == 0 /\ -y^post5+y^0 == 0 /\ __disjvr_3^post5-__disjvr_3^0 == 0 /\ -x^post5+x^0 == 0 /\ __disjvr_1^0-__disjvr_1^post5 == 0 /\ __disjvr_4^0-__disjvr_4^post5 == 0 /\ __disjvr_10^0-__disjvr_10^post5 == 0 /\ -__disjvr_2^post5+__disjvr_2^0 == 0 /\ __disjvr_13^0-__disjvr_13^post5 == 0 /\ __disjvr_7^0-__disjvr_7^post5 == 0), cost: 1
New rule:
l6 -> l7 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l7 -> l8 : __disjvr_13^0'=__disjvr_13^post6, __disjvr_7^0'=__disjvr_7^post6, __disjvr_10^0'=__disjvr_10^post6, __disjvr_9^0'=__disjvr_9^post6, __disjvr_4^0'=__disjvr_4^post6, __disjvr_1^0'=__disjvr_1^post6, __disjvr_12^0'=__disjvr_12^post6, y^0'=y^post6, __disjvr_6^0'=__disjvr_6^post6, __disjvr_0^0'=__disjvr_0^post6, __disjvr_3^0'=__disjvr_3^post6, __disjvr_14^0'=__disjvr_14^post6, __disjvr_8^0'=__disjvr_8^post6, __disjvr_11^0'=__disjvr_11^post6, x^0'=x^post6, __disjvr_5^0'=__disjvr_5^post6, __disjvr_2^0'=__disjvr_2^post6, (-__disjvr_11^post6+__disjvr_11^0 == 0 /\ __disjvr_5^0-__disjvr_5^post6 == 0 /\ -__disjvr_6^post6+__disjvr_6^0 == 0 /\ __disjvr_7^0-__disjvr_7^post6 == 0 /\ -__disjvr_2^post6+__disjvr_2^0 == 0 /\ y^0-y^post6 == 0 /\ __disjvr_0^0-__disjvr_0^post6 == 0 /\ __disjvr_10^0-__disjvr_10^post6 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ -__disjvr_8^post6+__disjvr_8^0 == 0 /\ __disjvr_13^0-__disjvr_13^post6 == 0 /\ __disjvr_3^0-__disjvr_3^post6 == 0 /\ -__disjvr_14^post6+__disjvr_14^0 == 0 /\ __disjvr_9^0-__disjvr_9^post6 == 0 /\ -__disjvr_4^0+__disjvr_4^post6 == 0 /\ -x^post6+x^0 == 0 /\ __disjvr_4^0-__disjvr_4^post6 == 0 /\ __disjvr_12^0-__disjvr_12^post6 == 0), cost: 1
New rule:
l7 -> l8 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l9 : __disjvr_13^0'=__disjvr_13^post7, __disjvr_7^0'=__disjvr_7^post7, __disjvr_10^0'=__disjvr_10^post7, __disjvr_9^0'=__disjvr_9^post7, __disjvr_4^0'=__disjvr_4^post7, __disjvr_1^0'=__disjvr_1^post7, __disjvr_12^0'=__disjvr_12^post7, y^0'=y^post7, __disjvr_6^0'=__disjvr_6^post7, __disjvr_0^0'=__disjvr_0^post7, __disjvr_3^0'=__disjvr_3^post7, __disjvr_14^0'=__disjvr_14^post7, __disjvr_8^0'=__disjvr_8^post7, __disjvr_11^0'=__disjvr_11^post7, x^0'=x^post7, __disjvr_5^0'=__disjvr_5^post7, __disjvr_2^0'=__disjvr_2^post7, (-__disjvr_1^post7+__disjvr_1^0 == 0 /\ __disjvr_12^0-__disjvr_12^post7 == 0 /\ __disjvr_9^0-__disjvr_9^post7 == 0 /\ -__disjvr_5^post7+__disjvr_5^0 == 0 /\ -__disjvr_14^post7+__disjvr_14^0 == 0 /\ __disjvr_3^0-__disjvr_3^post7 == 0 /\ -x^post7+x^0 == 0 /\ __disjvr_5^post7-__disjvr_5^0 == 0 /\ -__disjvr_8^post7+__disjvr_8^0 == 0 /\ __disjvr_4^0-__disjvr_4^post7 == 0 /\ -__disjvr_6^post7+__disjvr_6^0 == 0 /\ __disjvr_10^0-__disjvr_10^post7 == 0 /\ -__disjvr_2^post7+__disjvr_2^0 == 0 /\ -__disjvr_11^post7+__disjvr_11^0 == 0 /\ -__disjvr_0^post7+__disjvr_0^0 == 0 /\ __disjvr_13^0-__disjvr_13^post7 == 0 /\ y^0-y^post7 == 0 /\ -__disjvr_7^post7+__disjvr_7^0 == 0), cost: 1
New rule:
l8 -> l9 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l10 : __disjvr_13^0'=__disjvr_13^post8, __disjvr_7^0'=__disjvr_7^post8, __disjvr_10^0'=__disjvr_10^post8, __disjvr_9^0'=__disjvr_9^post8, __disjvr_4^0'=__disjvr_4^post8, __disjvr_1^0'=__disjvr_1^post8, __disjvr_12^0'=__disjvr_12^post8, y^0'=y^post8, __disjvr_6^0'=__disjvr_6^post8, __disjvr_0^0'=__disjvr_0^post8, __disjvr_3^0'=__disjvr_3^post8, __disjvr_14^0'=__disjvr_14^post8, __disjvr_8^0'=__disjvr_8^post8, __disjvr_11^0'=__disjvr_11^post8, x^0'=x^post8, __disjvr_5^0'=__disjvr_5^post8, __disjvr_2^0'=__disjvr_2^post8, (__disjvr_11^0-__disjvr_11^post8 == 0 /\ __disjvr_7^0-__disjvr_7^post8 == 0 /\ -__disjvr_3^post8+__disjvr_3^0 == 0 /\ -__disjvr_2^post8+__disjvr_2^0 == 0 /\ __disjvr_1^0-__disjvr_1^post8 == 0 /\ __disjvr_10^0-__disjvr_10^post8 == 0 /\ __disjvr_13^0-__disjvr_13^post8 == 0 /\ __disjvr_8^0-__disjvr_8^post8 == 0 /\ -__disjvr_6^post8+__disjvr_6^0 == 0 /\ __disjvr_0^0-__disjvr_0^post8 == 0 /\ -__disjvr_14^post8+__disjvr_14^0 == 0 /\ -__disjvr_5^post8+__disjvr_5^0 == 0 /\ -__disjvr_9^post8+__disjvr_9^0 == 0 /\ __disjvr_6^post8-__disjvr_6^0 == 0 /\ -y^post8+y^0 == 0 /\ __disjvr_4^0-__disjvr_4^post8 == 0 /\ __disjvr_12^0-__disjvr_12^post8 == 0 /\ -x^post8+x^0 == 0), cost: 1
New rule:
l9 -> l10 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l10 -> l11 : __disjvr_13^0'=__disjvr_13^post9, __disjvr_7^0'=__disjvr_7^post9, __disjvr_10^0'=__disjvr_10^post9, __disjvr_9^0'=__disjvr_9^post9, __disjvr_4^0'=__disjvr_4^post9, __disjvr_1^0'=__disjvr_1^post9, __disjvr_12^0'=__disjvr_12^post9, y^0'=y^post9, __disjvr_6^0'=__disjvr_6^post9, __disjvr_0^0'=__disjvr_0^post9, __disjvr_3^0'=__disjvr_3^post9, __disjvr_14^0'=__disjvr_14^post9, __disjvr_8^0'=__disjvr_8^post9, __disjvr_11^0'=__disjvr_11^post9, x^0'=x^post9, __disjvr_5^0'=__disjvr_5^post9, __disjvr_2^0'=__disjvr_2^post9, (-__disjvr_5^post9+__disjvr_5^0 == 0 /\ -__disjvr_9^post9+__disjvr_9^0 == 0 /\ __disjvr_14^0-__disjvr_14^post9 == 0 /\ -x^post9+x^0 == 0 /\ -__disjvr_12^post9+__disjvr_12^0 == 0 /\ __disjvr_11^0-__disjvr_11^post9 == 0 /\ __disjvr_1^0-__disjvr_1^post9 == 0 /\ -__disjvr_3^post9+__disjvr_3^0 == 0 /\ __disjvr_4^0-__disjvr_4^post9 == 0 /\ -__disjvr_7^0+__disjvr_7^post9 == 0 /\ -__disjvr_8^post9+__disjvr_8^0 == 0 /\ -__disjvr_2^post9+__disjvr_2^0 == 0 /\ __disjvr_10^0-__disjvr_10^post9 == 0 /\ y^0-y^post9 == 0 /\ __disjvr_0^0-__disjvr_0^post9 == 0 /\ __disjvr_13^0-__disjvr_13^post9 == 0 /\ __disjvr_7^0-__disjvr_7^post9 == 0 /\ __disjvr_6^0-__disjvr_6^post9 == 0), cost: 1
New rule:
l10 -> l11 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l11 -> l12 : __disjvr_13^0'=__disjvr_13^post10, __disjvr_7^0'=__disjvr_7^post10, __disjvr_10^0'=__disjvr_10^post10, __disjvr_9^0'=__disjvr_9^post10, __disjvr_4^0'=__disjvr_4^post10, __disjvr_1^0'=__disjvr_1^post10, __disjvr_12^0'=__disjvr_12^post10, y^0'=y^post10, __disjvr_6^0'=__disjvr_6^post10, __disjvr_0^0'=__disjvr_0^post10, __disjvr_3^0'=__disjvr_3^post10, __disjvr_14^0'=__disjvr_14^post10, __disjvr_8^0'=__disjvr_8^post10, __disjvr_11^0'=__disjvr_11^post10, x^0'=x^post10, __disjvr_5^0'=__disjvr_5^post10, __disjvr_2^0'=__disjvr_2^post10, (-__disjvr_6^post10+__disjvr_6^0 == 0 /\ -__disjvr_8^post10+__disjvr_8^0 == 0 /\ __disjvr_5^0-__disjvr_5^post10 == 0 /\ __disjvr_7^0-__disjvr_7^post10 == 0 /\ -__disjvr_2^post10+__disjvr_2^0 == 0 /\ -__disjvr_11^post10+__disjvr_11^0 == 0 /\ y^0-y^post10 == 0 /\ __disjvr_8^post10-__disjvr_8^0 == 0 /\ __disjvr_10^0-__disjvr_10^post10 == 0 /\ __disjvr_9^0-__disjvr_9^post10 == 0 /\ __disjvr_3^0-__disjvr_3^post10 == 0 /\ -__disjvr_1^post10+__disjvr_1^0 == 0 /\ __disjvr_13^0-__disjvr_13^post10 == 0 /\ -__disjvr_14^post10+__disjvr_14^0 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ __disjvr_4^0-__disjvr_4^post10 == 0 /\ -x^post10+x^0 == 0 /\ __disjvr_12^0-__disjvr_12^post10 == 0), cost: 1
New rule:
l11 -> l12 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l12 -> l13 : __disjvr_13^0'=__disjvr_13^post11, __disjvr_7^0'=__disjvr_7^post11, __disjvr_10^0'=__disjvr_10^post11, __disjvr_9^0'=__disjvr_9^post11, __disjvr_4^0'=__disjvr_4^post11, __disjvr_1^0'=__disjvr_1^post11, __disjvr_12^0'=__disjvr_12^post11, y^0'=y^post11, __disjvr_6^0'=__disjvr_6^post11, __disjvr_0^0'=__disjvr_0^post11, __disjvr_3^0'=__disjvr_3^post11, __disjvr_14^0'=__disjvr_14^post11, __disjvr_8^0'=__disjvr_8^post11, __disjvr_11^0'=__disjvr_11^post11, x^0'=x^post11, __disjvr_5^0'=__disjvr_5^post11, __disjvr_2^0'=__disjvr_2^post11, (__disjvr_3^0-__disjvr_3^post11 == 0 /\ -__disjvr_8^post11+__disjvr_8^0 == 0 /\ __disjvr_13^0-__disjvr_13^post11 == 0 /\ x^0-x^post11 == 0 /\ -__disjvr_2^post11+__disjvr_2^0 == 0 /\ -__disjvr_11^post11+__disjvr_11^0 == 0 /\ -y^post11+y^0 == 0 /\ __disjvr_7^0-__disjvr_7^post11 == 0 /\ -__disjvr_6^post11+__disjvr_6^0 == 0 /\ -__disjvr_9^0+__disjvr_9^post11 == 0 /\ -__disjvr_14^post11+__disjvr_14^0 == 0 /\ -__disjvr_5^post11+__disjvr_5^0 == 0 /\ __disjvr_12^0-__disjvr_12^post11 == 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0 /\ __disjvr_10^0-__disjvr_10^post11 == 0 /\ __disjvr_9^0-__disjvr_9^post11 == 0 /\ -__disjvr_4^post11+__disjvr_4^0 == 0 /\ __disjvr_1^0-__disjvr_1^post11 == 0), cost: 1
New rule:
l12 -> l13 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l14 : __disjvr_13^0'=__disjvr_13^post12, __disjvr_7^0'=__disjvr_7^post12, __disjvr_10^0'=__disjvr_10^post12, __disjvr_9^0'=__disjvr_9^post12, __disjvr_4^0'=__disjvr_4^post12, __disjvr_1^0'=__disjvr_1^post12, __disjvr_12^0'=__disjvr_12^post12, y^0'=y^post12, __disjvr_6^0'=__disjvr_6^post12, __disjvr_0^0'=__disjvr_0^post12, __disjvr_3^0'=__disjvr_3^post12, __disjvr_14^0'=__disjvr_14^post12, __disjvr_8^0'=__disjvr_8^post12, __disjvr_11^0'=__disjvr_11^post12, x^0'=x^post12, __disjvr_5^0'=__disjvr_5^post12, __disjvr_2^0'=__disjvr_2^post12, (-__disjvr_5^post12+__disjvr_5^0 == 0 /\ __disjvr_11^0-__disjvr_11^post12 == 0 /\ __disjvr_1^0-__disjvr_1^post12 == 0 /\ __disjvr_14^0-__disjvr_14^post12 == 0 /\ __disjvr_6^0-__disjvr_6^post12 == 0 /\ -x^post12+x^0 == 0 /\ -__disjvr_8^post12+__disjvr_8^0 == 0 /\ __disjvr_10^0-__disjvr_10^post12 == 0 /\ -__disjvr_3^post12+__disjvr_3^0 == 0 /\ -__disjvr_2^post12+__disjvr_2^0 == 0 /\ __disjvr_13^0-__disjvr_13^post12 == 0 /\ __disjvr_12^0-__disjvr_12^post12 == 0 /\ __disjvr_4^0-__disjvr_4^post12 == 0 /\ __disjvr_0^0-__disjvr_0^post12 == 0 /\ -__disjvr_10^0+__disjvr_10^post12 == 0 /\ -__disjvr_9^post12+__disjvr_9^0 == 0 /\ -y^post12+y^0 == 0 /\ __disjvr_7^0-__disjvr_7^post12 == 0), cost: 1
New rule:
l13 -> l14 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l14 -> l15 : __disjvr_13^0'=__disjvr_13^post13, __disjvr_7^0'=__disjvr_7^post13, __disjvr_10^0'=__disjvr_10^post13, __disjvr_9^0'=__disjvr_9^post13, __disjvr_4^0'=__disjvr_4^post13, __disjvr_1^0'=__disjvr_1^post13, __disjvr_12^0'=__disjvr_12^post13, y^0'=y^post13, __disjvr_6^0'=__disjvr_6^post13, __disjvr_0^0'=__disjvr_0^post13, __disjvr_3^0'=__disjvr_3^post13, __disjvr_14^0'=__disjvr_14^post13, __disjvr_8^0'=__disjvr_8^post13, __disjvr_11^0'=__disjvr_11^post13, x^0'=x^post13, __disjvr_5^0'=__disjvr_5^post13, __disjvr_2^0'=__disjvr_2^post13, (__disjvr_0^0-__disjvr_0^post13 == 0 /\ __disjvr_13^0-__disjvr_13^post13 == 0 /\ -__disjvr_3^post13+__disjvr_3^0 == 0 /\ -__disjvr_8^post13+__disjvr_8^0 == 0 /\ -__disjvr_12^post13+__disjvr_12^0 == 0 /\ -__disjvr_2^post13+__disjvr_2^0 == 0 /\ -__disjvr_11^post13+__disjvr_11^0 == 0 /\ __disjvr_4^0-__disjvr_4^post13 == 0 /\ __disjvr_11^post13-__disjvr_11^0 == 0 /\ y^0-y^post13 == 0 /\ __disjvr_14^0-__disjvr_14^post13 == 0 /\ -__disjvr_5^post13+__disjvr_5^0 == 0 /\ __disjvr_7^0-__disjvr_7^post13 == 0 /\ __disjvr_9^0-__disjvr_9^post13 == 0 /\ __disjvr_6^0-__disjvr_6^post13 == 0 /\ -x^post13+x^0 == 0 /\ __disjvr_10^0-__disjvr_10^post13 == 0 /\ __disjvr_1^0-__disjvr_1^post13 == 0), cost: 1
New rule:
l14 -> l15 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l15 -> l16 : __disjvr_13^0'=__disjvr_13^post14, __disjvr_7^0'=__disjvr_7^post14, __disjvr_10^0'=__disjvr_10^post14, __disjvr_9^0'=__disjvr_9^post14, __disjvr_4^0'=__disjvr_4^post14, __disjvr_1^0'=__disjvr_1^post14, __disjvr_12^0'=__disjvr_12^post14, y^0'=y^post14, __disjvr_6^0'=__disjvr_6^post14, __disjvr_0^0'=__disjvr_0^post14, __disjvr_3^0'=__disjvr_3^post14, __disjvr_14^0'=__disjvr_14^post14, __disjvr_8^0'=__disjvr_8^post14, __disjvr_11^0'=__disjvr_11^post14, x^0'=x^post14, __disjvr_5^0'=__disjvr_5^post14, __disjvr_2^0'=__disjvr_2^post14, (-__disjvr_5^post14+__disjvr_5^0 == 0 /\ -__disjvr_14^post14+__disjvr_14^0 == 0 /\ -__disjvr_0^post14+__disjvr_0^0 == 0 /\ __disjvr_3^0-__disjvr_3^post14 == 0 /\ __disjvr_9^0-__disjvr_9^post14 == 0 /\ __disjvr_10^0-__disjvr_10^post14 == 0 /\ -__disjvr_6^post14+__disjvr_6^0 == 0 /\ -x^post14+x^0 == 0 /\ -__disjvr_12^0+__disjvr_12^post14 == 0 /\ -__disjvr_8^post14+__disjvr_8^0 == 0 /\ -__disjvr_11^post14+__disjvr_11^0 == 0 /\ -__disjvr_1^post14+__disjvr_1^0 == 0 /\ -__disjvr_2^post14+__disjvr_2^0 == 0 /\ __disjvr_12^0-__disjvr_12^post14 == 0 /\ __disjvr_13^0-__disjvr_13^post14 == 0 /\ __disjvr_4^0-__disjvr_4^post14 == 0 /\ y^0-y^post14 == 0 /\ -__disjvr_7^post14+__disjvr_7^0 == 0), cost: 1
New rule:
l15 -> l16 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l16 -> l17 : __disjvr_13^0'=__disjvr_13^post15, __disjvr_7^0'=__disjvr_7^post15, __disjvr_10^0'=__disjvr_10^post15, __disjvr_9^0'=__disjvr_9^post15, __disjvr_4^0'=__disjvr_4^post15, __disjvr_1^0'=__disjvr_1^post15, __disjvr_12^0'=__disjvr_12^post15, y^0'=y^post15, __disjvr_6^0'=__disjvr_6^post15, __disjvr_0^0'=__disjvr_0^post15, __disjvr_3^0'=__disjvr_3^post15, __disjvr_14^0'=__disjvr_14^post15, __disjvr_8^0'=__disjvr_8^post15, __disjvr_11^0'=__disjvr_11^post15, x^0'=x^post15, __disjvr_5^0'=__disjvr_5^post15, __disjvr_2^0'=__disjvr_2^post15, (x^0-x^post15 == 0 /\ __disjvr_1^0-__disjvr_1^post15 == 0 /\ __disjvr_3^0-__disjvr_3^post15 == 0 /\ __disjvr_10^0-__disjvr_10^post15 == 0 /\ __disjvr_13^0-__disjvr_13^post15 == 0 /\ -__disjvr_8^post15+__disjvr_8^0 == 0 /\ -__disjvr_2^post15+__disjvr_2^0 == 0 /\ -__disjvr_11^post15+__disjvr_11^0 == 0 /\ -__disjvr_13^0+__disjvr_13^post15 == 0 /\ -y^post15+y^0 == 0 /\ __disjvr_7^0-__disjvr_7^post15 == 0 /\ -__disjvr_4^post15+__disjvr_4^0 == 0 /\ -__disjvr_6^post15+__disjvr_6^0 == 0 /\ -__disjvr_5^post15+__disjvr_5^0 == 0 /\ __disjvr_9^0-__disjvr_9^post15 == 0 /\ -__disjvr_0^post15+__disjvr_0^0 == 0 /\ -__disjvr_14^post15+__disjvr_14^0 == 0 /\ __disjvr_12^0-__disjvr_12^post15 == 0), cost: 1
New rule:
l16 -> l17 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l17 -> l2 : __disjvr_13^0'=__disjvr_13^post16, __disjvr_7^0'=__disjvr_7^post16, __disjvr_10^0'=__disjvr_10^post16, __disjvr_9^0'=__disjvr_9^post16, __disjvr_4^0'=__disjvr_4^post16, __disjvr_1^0'=__disjvr_1^post16, __disjvr_12^0'=__disjvr_12^post16, y^0'=y^post16, __disjvr_6^0'=__disjvr_6^post16, __disjvr_0^0'=__disjvr_0^post16, __disjvr_3^0'=__disjvr_3^post16, __disjvr_14^0'=__disjvr_14^post16, __disjvr_8^0'=__disjvr_8^post16, __disjvr_11^0'=__disjvr_11^post16, x^0'=x^post16, __disjvr_5^0'=__disjvr_5^post16, __disjvr_2^0'=__disjvr_2^post16, (-__disjvr_14^0+__disjvr_14^post16 == 0 /\ __disjvr_7^0-__disjvr_7^post16 == 0 /\ -__disjvr_5^post16+__disjvr_5^0 == 0 /\ -y^post16+y^0 == 0 /\ __disjvr_6^0-__disjvr_6^post16 == 0 /\ -x^post16+x^0 == 0 /\ __disjvr_1^0-__disjvr_1^post16 == 0 /\ __disjvr_14^0-__disjvr_14^post16 == 0 /\ __disjvr_11^0-__disjvr_11^post16 == 0 /\ __disjvr_10^0-__disjvr_10^post16 == 0 /\ -__disjvr_8^post16+__disjvr_8^0 == 0 /\ -__disjvr_3^post16+__disjvr_3^0 == 0 /\ __disjvr_13^0-__disjvr_13^post16 == 0 /\ -__disjvr_2^post16+__disjvr_2^0 == 0 /\ -__disjvr_9^post16+__disjvr_9^0 == 0 /\ __disjvr_4^0-__disjvr_4^post16 == 0 /\ __disjvr_0^0-__disjvr_0^post16 == 0 /\ __disjvr_12^0-__disjvr_12^post16 == 0), cost: 1
New rule:
l17 -> l2 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l1 : __disjvr_13^0'=__disjvr_13^post17, __disjvr_7^0'=__disjvr_7^post17, __disjvr_10^0'=__disjvr_10^post17, __disjvr_9^0'=__disjvr_9^post17, __disjvr_4^0'=__disjvr_4^post17, __disjvr_1^0'=__disjvr_1^post17, __disjvr_12^0'=__disjvr_12^post17, y^0'=y^post17, __disjvr_6^0'=__disjvr_6^post17, __disjvr_0^0'=__disjvr_0^post17, __disjvr_3^0'=__disjvr_3^post17, __disjvr_14^0'=__disjvr_14^post17, __disjvr_8^0'=__disjvr_8^post17, __disjvr_11^0'=__disjvr_11^post17, x^0'=x^post17, __disjvr_5^0'=__disjvr_5^post17, __disjvr_2^0'=__disjvr_2^post17, (-__disjvr_3^post17+__disjvr_3^0 == 0 /\ -__disjvr_1^post17+__disjvr_1^0 == 0 /\ __disjvr_4^0-__disjvr_4^post17 == 0 /\ -__disjvr_8^post17+__disjvr_8^0 == 0 /\ -__disjvr_11^post17+__disjvr_11^0 == 0 /\ __disjvr_13^0-__disjvr_13^post17 == 0 /\ -__disjvr_12^post17+__disjvr_12^0 == 0 /\ __disjvr_7^0-__disjvr_7^post17 == 0 /\ y^0-y^post17 == 0 /\ __disjvr_0^0-__disjvr_0^post17 == 0 /\ __disjvr_14^0-__disjvr_14^post17 == 0 /\ -__disjvr_5^post17+__disjvr_5^0 == 0 /\ __disjvr_9^0-__disjvr_9^post17 == 0 /\ -__disjvr_2^post17+__disjvr_2^0 == 0 /\ __disjvr_6^0-__disjvr_6^post17 == 0 /\ -__disjvr_10^post17+__disjvr_10^0 == 0 /\ -x^post17+x^0 == 0), cost: 1
New rule:
l2 -> l1 : TRUE, cost: 1

Applied preprocessing
Original rule:
l18 -> l0 : __disjvr_13^0'=__disjvr_13^post18, __disjvr_7^0'=__disjvr_7^post18, __disjvr_10^0'=__disjvr_10^post18, __disjvr_9^0'=__disjvr_9^post18, __disjvr_4^0'=__disjvr_4^post18, __disjvr_1^0'=__disjvr_1^post18, __disjvr_12^0'=__disjvr_12^post18, y^0'=y^post18, __disjvr_6^0'=__disjvr_6^post18, __disjvr_0^0'=__disjvr_0^post18, __disjvr_3^0'=__disjvr_3^post18, __disjvr_14^0'=__disjvr_14^post18, __disjvr_8^0'=__disjvr_8^post18, __disjvr_11^0'=__disjvr_11^post18, x^0'=x^post18, __disjvr_5^0'=__disjvr_5^post18, __disjvr_2^0'=__disjvr_2^post18, (__disjvr_4^0-__disjvr_4^post18 == 0 /\ y^0-y^post18 == 0 /\ -__disjvr_0^post18+__disjvr_0^0 == 0 /\ __disjvr_5^0-__disjvr_5^post18 == 0 /\ -__disjvr_14^post18+__disjvr_14^0 == 0 /\ -__disjvr_1^post18+__disjvr_1^0 == 0 /\ __disjvr_7^0-__disjvr_7^post18 == 0 /\ __disjvr_3^0-__disjvr_3^post18 == 0 /\ -x^post18+x^0 == 0 /\ __disjvr_13^0-__disjvr_13^post18 == 0 /\ -__disjvr_12^post18+__disjvr_12^0 == 0 /\ -__disjvr_2^post18+__disjvr_2^0 == 0 /\ __disjvr_9^0-__disjvr_9^post18 == 0 /\ __disjvr_6^0-__disjvr_6^post18 == 0 /\ -__disjvr_8^post18+__disjvr_8^0 == 0 /\ -__disjvr_11^post18+__disjvr_11^0 == 0 /\ -__disjvr_10^post18+__disjvr_10^0 == 0), cost: 1
New rule:
l18 -> l0 : TRUE, cost: 1

Simplified rules
Start location: l18
  19: l0 -> l1 : TRUE, cost: 1
  20: l1 -> l3 : 0 == 0, cost: 1
  21: l3 -> l4 : x^0'=y^0, x^0 == 0, cost: 1
  22: l4 -> l5 : 0 == 0, cost: 1
  23: l5 -> l6 : 0 == 0, cost: 1
  24: l6 -> l7 : 0 == 0, cost: 1
  25: l7 -> l8 : 0 == 0, cost: 1
  26: l8 -> l9 : 0 == 0, cost: 1
  27: l9 -> l10 : 0 == 0, cost: 1
  28: l10 -> l11 : 0 == 0, cost: 1
  29: l11 -> l12 : 0 == 0, cost: 1
  30: l12 -> l13 : 0 == 0, cost: 1
  31: l13 -> l14 : 0 == 0, cost: 1
  32: l14 -> l15 : 0 == 0, cost: 1
  33: l15 -> l16 : 0 == 0, cost: 1
  34: l16 -> l17 : 0 == 0, cost: 1
  35: l17 -> l2 : 0 == 0, cost: 1
  36: l2 -> l1 : TRUE, cost: 1
  37: l18 -> l0 : TRUE, cost: 1


Eliminating location l0 by chaining:

Applied chaining
First rule:
l18 -> l0 : TRUE, cost: 1
Second rule:
l0 -> l1 : TRUE, cost: 1
New rule:
l18 -> l1 : TRUE, cost: 2

Applied deletion
Removed the following rules: 19 37

Eliminating location l3 by chaining:

Applied chaining
First rule:
l1 -> l3 : 0 == 0, cost: 1
Second rule:
l3 -> l4 : x^0'=y^0, x^0 == 0, cost: 1
New rule:
l1 -> l4 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 2

Applied simplification
Original rule:
l1 -> l4 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 2
New rule:
l1 -> l4 : x^0'=y^0, x^0 == 0, cost: 2

Applied deletion
Removed the following rules: 20 21

Eliminating location l4 by chaining:

Applied chaining
First rule:
l1 -> l4 : x^0'=y^0, x^0 == 0, cost: 2
Second rule:
l4 -> l5 : 0 == 0, cost: 1
New rule:
l1 -> l5 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 3

Applied simplification
Original rule:
l1 -> l5 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 3
New rule:
l1 -> l5 : x^0'=y^0, x^0 == 0, cost: 3

Applied deletion
Removed the following rules: 22 39

Eliminating location l5 by chaining:

Applied chaining
First rule:
l1 -> l5 : x^0'=y^0, x^0 == 0, cost: 3
Second rule:
l5 -> l6 : 0 == 0, cost: 1
New rule:
l1 -> l6 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 4

Applied simplification
Original rule:
l1 -> l6 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 4
New rule:
l1 -> l6 : x^0'=y^0, x^0 == 0, cost: 4

Applied deletion
Removed the following rules: 23 40

Eliminating location l6 by chaining:

Applied chaining
First rule:
l1 -> l6 : x^0'=y^0, x^0 == 0, cost: 4
Second rule:
l6 -> l7 : 0 == 0, cost: 1
New rule:
l1 -> l7 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 5

Applied simplification
Original rule:
l1 -> l7 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 5
New rule:
l1 -> l7 : x^0'=y^0, x^0 == 0, cost: 5

Applied deletion
Removed the following rules: 24 41

Eliminating location l7 by chaining:

Applied chaining
First rule:
l1 -> l7 : x^0'=y^0, x^0 == 0, cost: 5
Second rule:
l7 -> l8 : 0 == 0, cost: 1
New rule:
l1 -> l8 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 6

Applied simplification
Original rule:
l1 -> l8 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 6
New rule:
l1 -> l8 : x^0'=y^0, x^0 == 0, cost: 6

Applied deletion
Removed the following rules: 25 42

Eliminating location l8 by chaining:

Applied chaining
First rule:
l1 -> l8 : x^0'=y^0, x^0 == 0, cost: 6
Second rule:
l8 -> l9 : 0 == 0, cost: 1
New rule:
l1 -> l9 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 7

Applied simplification
Original rule:
l1 -> l9 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 7
New rule:
l1 -> l9 : x^0'=y^0, x^0 == 0, cost: 7

Applied deletion
Removed the following rules: 26 43

Eliminating location l9 by chaining:

Applied chaining
First rule:
l1 -> l9 : x^0'=y^0, x^0 == 0, cost: 7
Second rule:
l9 -> l10 : 0 == 0, cost: 1
New rule:
l1 -> l10 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 8

Applied simplification
Original rule:
l1 -> l10 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 8
New rule:
l1 -> l10 : x^0'=y^0, x^0 == 0, cost: 8

Applied deletion
Removed the following rules: 27 44

Eliminating location l10 by chaining:

Applied chaining
First rule:
l1 -> l10 : x^0'=y^0, x^0 == 0, cost: 8
Second rule:
l10 -> l11 : 0 == 0, cost: 1
New rule:
l1 -> l11 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 9

Applied simplification
Original rule:
l1 -> l11 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 9
New rule:
l1 -> l11 : x^0'=y^0, x^0 == 0, cost: 9

Applied deletion
Removed the following rules: 28 45

Eliminating location l11 by chaining:

Applied chaining
First rule:
l1 -> l11 : x^0'=y^0, x^0 == 0, cost: 9
Second rule:
l11 -> l12 : 0 == 0, cost: 1
New rule:
l1 -> l12 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 10

Applied simplification
Original rule:
l1 -> l12 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 10
New rule:
l1 -> l12 : x^0'=y^0, x^0 == 0, cost: 10

Applied deletion
Removed the following rules: 29 46

Eliminating location l12 by chaining:

Applied chaining
First rule:
l1 -> l12 : x^0'=y^0, x^0 == 0, cost: 10
Second rule:
l12 -> l13 : 0 == 0, cost: 1
New rule:
l1 -> l13 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 11

Applied simplification
Original rule:
l1 -> l13 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 11
New rule:
l1 -> l13 : x^0'=y^0, x^0 == 0, cost: 11

Applied deletion
Removed the following rules: 30 47

Eliminating location l13 by chaining:

Applied chaining
First rule:
l1 -> l13 : x^0'=y^0, x^0 == 0, cost: 11
Second rule:
l13 -> l14 : 0 == 0, cost: 1
New rule:
l1 -> l14 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 12

Applied simplification
Original rule:
l1 -> l14 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 12
New rule:
l1 -> l14 : x^0'=y^0, x^0 == 0, cost: 12

Applied deletion
Removed the following rules: 31 48

Eliminating location l14 by chaining:

Applied chaining
First rule:
l1 -> l14 : x^0'=y^0, x^0 == 0, cost: 12
Second rule:
l14 -> l15 : 0 == 0, cost: 1
New rule:
l1 -> l15 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 13

Applied simplification
Original rule:
l1 -> l15 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 13
New rule:
l1 -> l15 : x^0'=y^0, x^0 == 0, cost: 13

Applied deletion
Removed the following rules: 32 49

Eliminating location l15 by chaining:

Applied chaining
First rule:
l1 -> l15 : x^0'=y^0, x^0 == 0, cost: 13
Second rule:
l15 -> l16 : 0 == 0, cost: 1
New rule:
l1 -> l16 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 14

Applied simplification
Original rule:
l1 -> l16 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 14
New rule:
l1 -> l16 : x^0'=y^0, x^0 == 0, cost: 14

Applied deletion
Removed the following rules: 33 50

Eliminating location l16 by chaining:

Applied chaining
First rule:
l1 -> l16 : x^0'=y^0, x^0 == 0, cost: 14
Second rule:
l16 -> l17 : 0 == 0, cost: 1
New rule:
l1 -> l17 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 15

Applied simplification
Original rule:
l1 -> l17 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 15
New rule:
l1 -> l17 : x^0'=y^0, x^0 == 0, cost: 15

Applied deletion
Removed the following rules: 34 51

Eliminating location l17 by chaining:

Applied chaining
First rule:
l1 -> l17 : x^0'=y^0, x^0 == 0, cost: 15
Second rule:
l17 -> l2 : 0 == 0, cost: 1
New rule:
l1 -> l2 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 16

Applied simplification
Original rule:
l1 -> l2 : x^0'=y^0, (0 == 0 /\ x^0 == 0), cost: 16
New rule:
l1 -> l2 : x^0'=y^0, x^0 == 0, cost: 16

Applied deletion
Removed the following rules: 35 52

Eliminating location l2 by chaining:

Applied chaining
First rule:
l1 -> l2 : x^0'=y^0, x^0 == 0, cost: 16
Second rule:
l2 -> l1 : TRUE, cost: 1
New rule:
l1 -> l1 : x^0'=y^0, x^0 == 0, cost: 17

Applied deletion
Removed the following rules: 36 53

Eliminated locations on linear paths
Start location: l18
  54: l1 -> l1 : x^0'=y^0, x^0 == 0, cost: 17
  38: l18 -> l1 : TRUE, cost: 2


Applied acceleration
Original rule:
l1 -> l1 : x^0'=y^0, x^0 == 0, cost: 17
New rule:
l1 -> l1 : x^0'=y^0, (-y^0 >= 0 /\ y^0 >= 0 /\ -1+n >= 0 /\ -x^0 >= 0 /\ x^0 >= 0), cost: 17*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_AnebcA.txt

Applied nonterm
Original rule:
l1 -> l1 : x^0'=y^0, x^0 == 0, cost: 17
New rule:
l1 -> [19] : (-x^0 >= 0 /\ -y^0+x^0 <= 0 /\ x^0 >= 0 /\ y^0-x^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ejonLf.txt

Applied simplification
Original rule:
l1 -> l1 : x^0'=y^0, (-y^0 >= 0 /\ y^0 >= 0 /\ -1+n >= 0 /\ -x^0 >= 0 /\ x^0 >= 0), cost: 17*n
New rule:
l1 -> l1 : x^0'=y^0, (y^0 <= 0 /\ y^0 >= 0 /\ -1+n >= 0 /\ x^0 <= 0 /\ x^0 >= 0), cost: 17*n

Applied simplification
Original rule:
l1 -> [19] : (-x^0 >= 0 /\ -y^0+x^0 <= 0 /\ x^0 >= 0 /\ y^0-x^0 <= 0), cost: NONTERM
New rule:
l1 -> [19] : (-y^0+x^0 <= 0 /\ x^0 <= 0 /\ x^0 >= 0 /\ y^0-x^0 <= 0), cost: NONTERM

Applied deletion
Removed the following rules: 54

Accelerated simple loops
Start location: l18
  57: l1 -> l1 : x^0'=y^0, (y^0 <= 0 /\ y^0 >= 0 /\ -1+n >= 0 /\ x^0 <= 0 /\ x^0 >= 0), cost: 17*n
  58: l1 -> [19] : (-y^0+x^0 <= 0 /\ x^0 <= 0 /\ x^0 >= 0 /\ y^0-x^0 <= 0), cost: NONTERM
  38: l18 -> l1 : TRUE, cost: 2


Applied chaining
First rule:
l18 -> l1 : TRUE, cost: 2
Second rule:
l1 -> l1 : x^0'=y^0, (y^0 <= 0 /\ y^0 >= 0 /\ -1+n >= 0 /\ x^0 <= 0 /\ x^0 >= 0), cost: 17*n
New rule:
l18 -> l1 : x^0'=y^0, (y^0 == 0 /\ -1+n >= 0 /\ x^0 == 0), cost: 2+17*n

Applied chaining
First rule:
l18 -> l1 : TRUE, cost: 2
Second rule:
l1 -> [19] : (-y^0+x^0 <= 0 /\ x^0 <= 0 /\ x^0 >= 0 /\ y^0-x^0 <= 0), cost: NONTERM
New rule:
l18 -> [19] : (-y^0+x^0 == 0 /\ x^0 == 0), cost: NONTERM

Applied deletion
Removed the following rules: 57 58

Chained accelerated rules with incoming rules
Start location: l18
  38: l18 -> l1 : TRUE, cost: 2
  59: l18 -> l1 : x^0'=y^0, (y^0 == 0 /\ -1+n >= 0 /\ x^0 == 0), cost: 2+17*n
  60: l18 -> [19] : (-y^0+x^0 == 0 /\ x^0 == 0), cost: NONTERM


Removed unreachable locations and irrelevant leafs
Start location: l18
  60: l18 -> [19] : (-y^0+x^0 == 0 /\ x^0 == 0), cost: NONTERM


Computing asymptotic complexity
Proved nontermination of rule 60 via SMT.

Proved the following lower bound
Complexity:  Nonterm
Cpx degree: Nonterm

Solved cost: NONTERM
Rule cost:   NONTERM
Rule guard:  (-y^0+x^0 == 0 /\ x^0 == 0)