YES(?,O(n^2)) 766.23/281.93 YES(?,O(n^2)) 766.23/281.94 766.23/281.94 Problem: 766.23/281.94 a12(a12(x1)) -> x1 766.23/281.94 a13(a13(x1)) -> x1 766.23/281.94 a14(a14(x1)) -> x1 766.23/281.94 a15(a15(x1)) -> x1 766.23/281.94 a16(a16(x1)) -> x1 766.23/281.94 a23(a23(x1)) -> x1 766.23/281.94 a24(a24(x1)) -> x1 766.23/281.94 a25(a25(x1)) -> x1 766.23/281.94 a26(a26(x1)) -> x1 766.23/281.94 a34(a34(x1)) -> x1 766.23/281.94 a35(a35(x1)) -> x1 766.23/281.94 a36(a36(x1)) -> x1 766.23/281.94 a45(a45(x1)) -> x1 766.23/281.94 a46(a46(x1)) -> x1 766.23/281.94 a56(a56(x1)) -> x1 766.23/281.94 a13(x1) -> a12(a23(a12(x1))) 766.23/281.94 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.23/281.94 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.94 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.94 a24(x1) -> a23(a34(a23(x1))) 766.23/281.94 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.23/281.94 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.94 a35(x1) -> a34(a45(a34(x1))) 766.23/281.94 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.23/281.94 a46(x1) -> a45(a56(a45(x1))) 766.23/281.94 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.23/281.94 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.23/281.94 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.23/281.94 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.23/281.94 a12(a34(x1)) -> a34(a12(x1)) 766.23/281.94 a12(a45(x1)) -> a45(a12(x1)) 766.23/281.94 a12(a56(x1)) -> a56(a12(x1)) 766.23/281.94 a23(a45(x1)) -> a45(a23(x1)) 766.23/281.94 a23(a56(x1)) -> a56(a23(x1)) 766.23/281.94 a34(a56(x1)) -> a56(a34(x1)) 766.23/281.94 766.23/281.94 Proof: 766.23/281.94 Complexity Transformation Processor: 766.23/281.94 strict: 766.23/281.94 a12(a12(x1)) -> x1 766.23/281.94 a13(a13(x1)) -> x1 766.23/281.94 a14(a14(x1)) -> x1 766.23/281.94 a15(a15(x1)) -> x1 766.23/281.94 a16(a16(x1)) -> x1 766.23/281.94 a23(a23(x1)) -> x1 766.23/281.94 a24(a24(x1)) -> x1 766.23/281.94 a25(a25(x1)) -> x1 766.23/281.94 a26(a26(x1)) -> x1 766.23/281.94 a34(a34(x1)) -> x1 766.23/281.94 a35(a35(x1)) -> x1 766.23/281.94 a36(a36(x1)) -> x1 766.23/281.94 a45(a45(x1)) -> x1 766.23/281.94 a46(a46(x1)) -> x1 766.23/281.94 a56(a56(x1)) -> x1 766.23/281.94 a13(x1) -> a12(a23(a12(x1))) 766.23/281.94 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.23/281.94 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.94 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.94 a24(x1) -> a23(a34(a23(x1))) 766.23/281.94 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.23/281.94 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.94 a35(x1) -> a34(a45(a34(x1))) 766.23/281.94 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.23/281.94 a46(x1) -> a45(a56(a45(x1))) 766.23/281.94 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.23/281.94 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.23/281.94 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.23/281.94 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.23/281.94 a12(a34(x1)) -> a34(a12(x1)) 766.23/281.94 a12(a45(x1)) -> a45(a12(x1)) 766.23/281.94 a12(a56(x1)) -> a56(a12(x1)) 766.23/281.94 a23(a45(x1)) -> a45(a23(x1)) 766.23/281.94 a23(a56(x1)) -> a56(a23(x1)) 766.23/281.94 a34(a56(x1)) -> a56(a34(x1)) 766.23/281.94 weak: 766.23/281.94 766.23/281.94 Matrix Interpretation Processor: dim=1 766.23/281.94 766.23/281.94 max_matrix: 766.23/281.94 1 766.23/281.94 interpretation: 766.23/281.94 [a56](x0) = x0, 766.23/281.94 766.23/281.94 [a46](x0) = x0 + 2, 766.23/281.94 766.23/281.94 [a45](x0) = x0, 766.23/281.94 766.23/281.94 [a36](x0) = x0 + 5, 766.23/281.94 766.23/281.94 [a35](x0) = x0 + 8, 766.23/281.94 766.23/281.94 [a34](x0) = x0 + 8, 766.23/281.94 766.23/281.94 [a26](x0) = x0 + 1, 766.23/281.94 766.23/281.94 [a25](x0) = x0 + 4, 766.23/281.94 766.23/281.94 [a24](x0) = x0 + 2, 766.23/281.94 766.23/281.94 [a23](x0) = x0, 766.23/281.94 766.23/281.94 [a16](x0) = x0, 766.23/281.94 766.23/281.94 [a15](x0) = x0 + 8, 766.23/281.94 766.23/281.94 [a14](x0) = x0 + 8, 766.23/281.94 766.23/281.94 [a13](x0) = x0, 766.23/281.94 766.23/281.94 [a12](x0) = x0 + 1 766.23/281.94 orientation: 766.23/281.94 a12(a12(x1)) = x1 + 2 >= x1 = x1 766.23/281.94 766.23/281.94 a13(a13(x1)) = x1 >= x1 = x1 766.23/281.94 766.23/281.94 a14(a14(x1)) = x1 + 16 >= x1 = x1 766.23/281.94 766.23/281.94 a15(a15(x1)) = x1 + 16 >= x1 = x1 766.23/281.94 766.23/281.94 a16(a16(x1)) = x1 >= x1 = x1 766.23/281.94 766.23/281.94 a23(a23(x1)) = x1 >= x1 = x1 766.23/281.94 766.23/281.94 a24(a24(x1)) = x1 + 4 >= x1 = x1 766.23/281.94 766.23/281.94 a25(a25(x1)) = x1 + 8 >= x1 = x1 766.23/281.94 766.23/281.94 a26(a26(x1)) = x1 + 2 >= x1 = x1 766.23/281.94 766.23/281.94 a34(a34(x1)) = x1 + 16 >= x1 = x1 766.23/281.94 766.23/281.94 a35(a35(x1)) = x1 + 16 >= x1 = x1 766.23/281.94 766.23/281.94 a36(a36(x1)) = x1 + 10 >= x1 = x1 766.23/281.94 766.23/281.94 a45(a45(x1)) = x1 >= x1 = x1 766.23/281.94 766.23/281.94 a46(a46(x1)) = x1 + 4 >= x1 = x1 766.23/281.94 766.23/281.94 a56(a56(x1)) = x1 >= x1 = x1 766.23/281.94 766.23/281.94 a13(x1) = x1 >= x1 + 2 = a12(a23(a12(x1))) 766.23/281.94 766.23/281.94 a14(x1) = x1 + 8 >= x1 + 10 = a12(a23(a34(a23(a12(x1))))) 766.23/281.94 766.23/281.94 a15(x1) = x1 + 8 >= x1 + 18 = a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.94 766.23/281.94 a16(x1) = x1 >= x1 + 18 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.94 766.23/281.94 a24(x1) = x1 + 2 >= x1 + 8 = a23(a34(a23(x1))) 766.23/281.94 766.23/281.94 a25(x1) = x1 + 4 >= x1 + 16 = a23(a34(a45(a34(a23(x1))))) 766.23/281.94 766.23/281.94 a26(x1) = x1 + 1 >= x1 + 16 = a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.94 766.23/281.94 a35(x1) = x1 + 8 >= x1 + 16 = a34(a45(a34(x1))) 766.23/281.94 766.23/281.94 a36(x1) = x1 + 5 >= x1 + 16 = a34(a45(a56(a45(a34(x1))))) 766.23/281.94 766.23/281.94 a46(x1) = x1 + 2 >= x1 = a45(a56(a45(x1))) 766.23/281.94 766.23/281.94 a12(a23(a12(a23(a12(a23(x1)))))) = x1 + 3 >= x1 = x1 766.23/281.94 766.23/281.94 a23(a34(a23(a34(a23(a34(x1)))))) = x1 + 24 >= x1 = x1 766.23/281.94 766.23/281.94 a34(a45(a34(a45(a34(a45(x1)))))) = x1 + 24 >= x1 = x1 766.23/281.94 766.23/281.94 a45(a56(a45(a56(a45(a56(x1)))))) = x1 >= x1 = x1 766.23/281.94 766.23/281.94 a12(a34(x1)) = x1 + 9 >= x1 + 9 = a34(a12(x1)) 766.23/281.94 766.23/281.94 a12(a45(x1)) = x1 + 1 >= x1 + 1 = a45(a12(x1)) 766.23/281.94 766.23/281.94 a12(a56(x1)) = x1 + 1 >= x1 + 1 = a56(a12(x1)) 766.23/281.94 766.23/281.94 a23(a45(x1)) = x1 >= x1 = a45(a23(x1)) 766.23/281.94 766.23/281.94 a23(a56(x1)) = x1 >= x1 = a56(a23(x1)) 766.23/281.94 766.23/281.94 a34(a56(x1)) = x1 + 8 >= x1 + 8 = a56(a34(x1)) 766.23/281.94 problem: 766.23/281.94 strict: 766.23/281.94 a13(a13(x1)) -> x1 766.23/281.94 a16(a16(x1)) -> x1 766.23/281.94 a23(a23(x1)) -> x1 766.23/281.94 a45(a45(x1)) -> x1 766.23/281.94 a56(a56(x1)) -> x1 766.23/281.94 a13(x1) -> a12(a23(a12(x1))) 766.23/281.94 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.23/281.94 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.94 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.94 a24(x1) -> a23(a34(a23(x1))) 766.23/281.94 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.23/281.94 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.94 a35(x1) -> a34(a45(a34(x1))) 766.23/281.94 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.23/281.94 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.23/281.94 a12(a34(x1)) -> a34(a12(x1)) 766.23/281.94 a12(a45(x1)) -> a45(a12(x1)) 766.23/281.94 a12(a56(x1)) -> a56(a12(x1)) 766.23/281.94 a23(a45(x1)) -> a45(a23(x1)) 766.23/281.94 a23(a56(x1)) -> a56(a23(x1)) 766.23/281.94 a34(a56(x1)) -> a56(a34(x1)) 766.23/281.94 weak: 766.23/281.94 a12(a12(x1)) -> x1 766.23/281.94 a14(a14(x1)) -> x1 766.23/281.94 a15(a15(x1)) -> x1 766.23/281.94 a24(a24(x1)) -> x1 766.23/281.94 a25(a25(x1)) -> x1 766.23/281.94 a26(a26(x1)) -> x1 766.23/281.94 a34(a34(x1)) -> x1 766.23/281.94 a35(a35(x1)) -> x1 766.23/281.94 a36(a36(x1)) -> x1 766.23/281.94 a46(a46(x1)) -> x1 766.23/281.94 a46(x1) -> a45(a56(a45(x1))) 766.23/281.94 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.23/281.94 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.23/281.94 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.23/281.94 Matrix Interpretation Processor: dim=1 766.23/281.94 766.23/281.94 max_matrix: 766.23/281.94 1 766.23/281.94 interpretation: 766.23/281.94 [a56](x0) = x0, 766.23/281.94 766.23/281.94 [a46](x0) = x0, 766.23/281.94 766.23/281.94 [a45](x0) = x0, 766.23/281.94 766.23/281.94 [a36](x0) = x0, 766.23/281.94 766.23/281.94 [a35](x0) = x0 + 9, 766.23/281.94 766.23/281.94 [a34](x0) = x0 + 8, 766.23/281.94 766.23/281.94 [a26](x0) = x0, 766.23/281.94 766.23/281.94 [a25](x0) = x0 + 4, 766.23/281.94 766.23/281.94 [a24](x0) = x0 + 1, 766.23/281.94 766.23/281.94 [a23](x0) = x0, 766.23/281.95 766.23/281.95 [a16](x0) = x0, 766.23/281.95 766.23/281.95 [a15](x0) = x0, 766.23/281.95 766.23/281.95 [a14](x0) = x0 + 2, 766.23/281.95 766.23/281.95 [a13](x0) = x0 + 4, 766.23/281.95 766.23/281.95 [a12](x0) = x0 766.23/281.95 orientation: 766.23/281.95 a13(a13(x1)) = x1 + 8 >= x1 = x1 766.23/281.95 766.23/281.95 a16(a16(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a23(a23(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a45(a45(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a56(a56(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a13(x1) = x1 + 4 >= x1 = a12(a23(a12(x1))) 766.23/281.95 766.23/281.95 a14(x1) = x1 + 2 >= x1 + 8 = a12(a23(a34(a23(a12(x1))))) 766.23/281.95 766.23/281.95 a15(x1) = x1 >= x1 + 16 = a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.95 766.23/281.95 a16(x1) = x1 >= x1 + 16 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.95 766.23/281.95 a24(x1) = x1 + 1 >= x1 + 8 = a23(a34(a23(x1))) 766.23/281.95 766.23/281.95 a25(x1) = x1 + 4 >= x1 + 16 = a23(a34(a45(a34(a23(x1))))) 766.23/281.95 766.23/281.95 a26(x1) = x1 >= x1 + 16 = a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.95 766.23/281.95 a35(x1) = x1 + 9 >= x1 + 16 = a34(a45(a34(x1))) 766.23/281.95 766.23/281.95 a36(x1) = x1 >= x1 + 16 = a34(a45(a56(a45(a34(x1))))) 766.23/281.95 766.23/281.95 a45(a56(a45(a56(a45(a56(x1)))))) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a12(a34(x1)) = x1 + 8 >= x1 + 8 = a34(a12(x1)) 766.23/281.95 766.23/281.95 a12(a45(x1)) = x1 >= x1 = a45(a12(x1)) 766.23/281.95 766.23/281.95 a12(a56(x1)) = x1 >= x1 = a56(a12(x1)) 766.23/281.95 766.23/281.95 a23(a45(x1)) = x1 >= x1 = a45(a23(x1)) 766.23/281.95 766.23/281.95 a23(a56(x1)) = x1 >= x1 = a56(a23(x1)) 766.23/281.95 766.23/281.95 a34(a56(x1)) = x1 + 8 >= x1 + 8 = a56(a34(x1)) 766.23/281.95 766.23/281.95 a12(a12(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a14(a14(x1)) = x1 + 4 >= x1 = x1 766.23/281.95 766.23/281.95 a15(a15(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a24(a24(x1)) = x1 + 2 >= x1 = x1 766.23/281.95 766.23/281.95 a25(a25(x1)) = x1 + 8 >= x1 = x1 766.23/281.95 766.23/281.95 a26(a26(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a34(a34(x1)) = x1 + 16 >= x1 = x1 766.23/281.95 766.23/281.95 a35(a35(x1)) = x1 + 18 >= x1 = x1 766.23/281.95 766.23/281.95 a36(a36(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a46(a46(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a46(x1) = x1 >= x1 = a45(a56(a45(x1))) 766.23/281.95 766.23/281.95 a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a23(a34(a23(a34(a23(a34(x1)))))) = x1 + 24 >= x1 = x1 766.23/281.95 766.23/281.95 a34(a45(a34(a45(a34(a45(x1)))))) = x1 + 24 >= x1 = x1 766.23/281.95 problem: 766.23/281.95 strict: 766.23/281.95 a16(a16(x1)) -> x1 766.23/281.95 a23(a23(x1)) -> x1 766.23/281.95 a45(a45(x1)) -> x1 766.23/281.95 a56(a56(x1)) -> x1 766.23/281.95 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.23/281.95 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.95 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.95 a24(x1) -> a23(a34(a23(x1))) 766.23/281.95 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.23/281.95 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.95 a35(x1) -> a34(a45(a34(x1))) 766.23/281.95 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.23/281.95 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.23/281.95 a12(a34(x1)) -> a34(a12(x1)) 766.23/281.95 a12(a45(x1)) -> a45(a12(x1)) 766.23/281.95 a12(a56(x1)) -> a56(a12(x1)) 766.23/281.95 a23(a45(x1)) -> a45(a23(x1)) 766.23/281.95 a23(a56(x1)) -> a56(a23(x1)) 766.23/281.95 a34(a56(x1)) -> a56(a34(x1)) 766.23/281.95 weak: 766.23/281.95 a13(a13(x1)) -> x1 766.23/281.95 a13(x1) -> a12(a23(a12(x1))) 766.23/281.95 a12(a12(x1)) -> x1 766.23/281.95 a14(a14(x1)) -> x1 766.23/281.95 a15(a15(x1)) -> x1 766.23/281.95 a24(a24(x1)) -> x1 766.23/281.95 a25(a25(x1)) -> x1 766.23/281.95 a26(a26(x1)) -> x1 766.23/281.95 a34(a34(x1)) -> x1 766.23/281.95 a35(a35(x1)) -> x1 766.23/281.95 a36(a36(x1)) -> x1 766.23/281.95 a46(a46(x1)) -> x1 766.23/281.95 a46(x1) -> a45(a56(a45(x1))) 766.23/281.95 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.23/281.95 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.23/281.95 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.23/281.95 Matrix Interpretation Processor: dim=1 766.23/281.95 766.23/281.95 max_matrix: 766.23/281.95 1 766.23/281.95 interpretation: 766.23/281.95 [a56](x0) = x0, 766.23/281.95 766.23/281.95 [a46](x0) = x0, 766.23/281.95 766.23/281.95 [a45](x0) = x0, 766.23/281.95 766.23/281.95 [a36](x0) = x0 + 10, 766.23/281.95 766.23/281.95 [a35](x0) = x0 + 1, 766.23/281.95 766.23/281.95 [a34](x0) = x0, 766.23/281.95 766.23/281.95 [a26](x0) = x0, 766.23/281.95 766.23/281.95 [a25](x0) = x0 + 4, 766.23/281.95 766.23/281.95 [a24](x0) = x0, 766.23/281.95 766.23/281.95 [a23](x0) = x0, 766.23/281.95 766.23/281.95 [a16](x0) = x0 + 1, 766.23/281.95 766.23/281.95 [a15](x0) = x0, 766.23/281.95 766.23/281.95 [a14](x0) = x0, 766.23/281.95 766.23/281.95 [a13](x0) = x0 + 2, 766.23/281.95 766.23/281.95 [a12](x0) = x0 766.23/281.95 orientation: 766.23/281.95 a16(a16(x1)) = x1 + 2 >= x1 = x1 766.23/281.95 766.23/281.95 a23(a23(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a45(a45(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a56(a56(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a14(x1) = x1 >= x1 = a12(a23(a34(a23(a12(x1))))) 766.23/281.95 766.23/281.95 a15(x1) = x1 >= x1 = a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.95 766.23/281.95 a16(x1) = x1 + 1 >= x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.95 766.23/281.95 a24(x1) = x1 >= x1 = a23(a34(a23(x1))) 766.23/281.95 766.23/281.95 a25(x1) = x1 + 4 >= x1 = a23(a34(a45(a34(a23(x1))))) 766.23/281.95 766.23/281.95 a26(x1) = x1 >= x1 = a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.95 766.23/281.95 a35(x1) = x1 + 1 >= x1 = a34(a45(a34(x1))) 766.23/281.95 766.23/281.95 a36(x1) = x1 + 10 >= x1 = a34(a45(a56(a45(a34(x1))))) 766.23/281.95 766.23/281.95 a45(a56(a45(a56(a45(a56(x1)))))) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a12(a34(x1)) = x1 >= x1 = a34(a12(x1)) 766.23/281.95 766.23/281.95 a12(a45(x1)) = x1 >= x1 = a45(a12(x1)) 766.23/281.95 766.23/281.95 a12(a56(x1)) = x1 >= x1 = a56(a12(x1)) 766.23/281.95 766.23/281.95 a23(a45(x1)) = x1 >= x1 = a45(a23(x1)) 766.23/281.95 766.23/281.95 a23(a56(x1)) = x1 >= x1 = a56(a23(x1)) 766.23/281.95 766.23/281.95 a34(a56(x1)) = x1 >= x1 = a56(a34(x1)) 766.23/281.95 766.23/281.95 a13(a13(x1)) = x1 + 4 >= x1 = x1 766.23/281.95 766.23/281.95 a13(x1) = x1 + 2 >= x1 = a12(a23(a12(x1))) 766.23/281.95 766.23/281.95 a12(a12(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a14(a14(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a15(a15(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a24(a24(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a25(a25(x1)) = x1 + 8 >= x1 = x1 766.23/281.95 766.23/281.95 a26(a26(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a34(a34(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a35(a35(x1)) = x1 + 2 >= x1 = x1 766.23/281.95 766.23/281.95 a36(a36(x1)) = x1 + 20 >= x1 = x1 766.23/281.95 766.23/281.95 a46(a46(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a46(x1) = x1 >= x1 = a45(a56(a45(x1))) 766.23/281.95 766.23/281.95 a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1 766.23/281.95 problem: 766.23/281.95 strict: 766.23/281.95 a23(a23(x1)) -> x1 766.23/281.95 a45(a45(x1)) -> x1 766.23/281.95 a56(a56(x1)) -> x1 766.23/281.95 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.23/281.95 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.95 a24(x1) -> a23(a34(a23(x1))) 766.23/281.95 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.95 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.23/281.95 a12(a34(x1)) -> a34(a12(x1)) 766.23/281.95 a12(a45(x1)) -> a45(a12(x1)) 766.23/281.95 a12(a56(x1)) -> a56(a12(x1)) 766.23/281.95 a23(a45(x1)) -> a45(a23(x1)) 766.23/281.95 a23(a56(x1)) -> a56(a23(x1)) 766.23/281.95 a34(a56(x1)) -> a56(a34(x1)) 766.23/281.95 weak: 766.23/281.95 a16(a16(x1)) -> x1 766.23/281.95 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.95 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.23/281.95 a35(x1) -> a34(a45(a34(x1))) 766.23/281.95 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.23/281.95 a13(a13(x1)) -> x1 766.23/281.95 a13(x1) -> a12(a23(a12(x1))) 766.23/281.95 a12(a12(x1)) -> x1 766.23/281.95 a14(a14(x1)) -> x1 766.23/281.95 a15(a15(x1)) -> x1 766.23/281.95 a24(a24(x1)) -> x1 766.23/281.95 a25(a25(x1)) -> x1 766.23/281.95 a26(a26(x1)) -> x1 766.23/281.95 a34(a34(x1)) -> x1 766.23/281.95 a35(a35(x1)) -> x1 766.23/281.95 a36(a36(x1)) -> x1 766.23/281.95 a46(a46(x1)) -> x1 766.23/281.95 a46(x1) -> a45(a56(a45(x1))) 766.23/281.95 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.23/281.95 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.23/281.95 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.23/281.95 Matrix Interpretation Processor: dim=1 766.23/281.95 766.23/281.95 max_matrix: 766.23/281.95 1 766.23/281.95 interpretation: 766.23/281.95 [a56](x0) = x0 + 4, 766.23/281.95 766.23/281.95 [a46](x0) = x0 + 4, 766.23/281.95 766.23/281.95 [a45](x0) = x0, 766.23/281.95 766.23/281.95 [a36](x0) = x0 + 4, 766.23/281.95 766.23/281.95 [a35](x0) = x0, 766.23/281.95 766.23/281.95 [a34](x0) = x0, 766.23/281.95 766.23/281.95 [a26](x0) = x0, 766.23/281.95 766.23/281.95 [a25](x0) = x0 + 8, 766.23/281.95 766.23/281.95 [a24](x0) = x0 + 1, 766.23/281.95 766.23/281.95 [a23](x0) = x0, 766.23/281.95 766.23/281.95 [a16](x0) = x0 + 4, 766.23/281.95 766.23/281.95 [a15](x0) = x0 + 2, 766.23/281.95 766.23/281.95 [a14](x0) = x0, 766.23/281.95 766.23/281.95 [a13](x0) = x0, 766.23/281.95 766.23/281.95 [a12](x0) = x0 766.23/281.95 orientation: 766.23/281.95 a23(a23(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a45(a45(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a56(a56(x1)) = x1 + 8 >= x1 = x1 766.23/281.95 766.23/281.95 a14(x1) = x1 >= x1 = a12(a23(a34(a23(a12(x1))))) 766.23/281.95 766.23/281.95 a15(x1) = x1 + 2 >= x1 = a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.95 766.23/281.95 a24(x1) = x1 + 1 >= x1 = a23(a34(a23(x1))) 766.23/281.95 766.23/281.95 a26(x1) = x1 >= x1 + 4 = a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.95 766.23/281.95 a45(a56(a45(a56(a45(a56(x1)))))) = x1 + 12 >= x1 = x1 766.23/281.95 766.23/281.95 a12(a34(x1)) = x1 >= x1 = a34(a12(x1)) 766.23/281.95 766.23/281.95 a12(a45(x1)) = x1 >= x1 = a45(a12(x1)) 766.23/281.95 766.23/281.95 a12(a56(x1)) = x1 + 4 >= x1 + 4 = a56(a12(x1)) 766.23/281.95 766.23/281.95 a23(a45(x1)) = x1 >= x1 = a45(a23(x1)) 766.23/281.95 766.23/281.95 a23(a56(x1)) = x1 + 4 >= x1 + 4 = a56(a23(x1)) 766.23/281.95 766.23/281.95 a34(a56(x1)) = x1 + 4 >= x1 + 4 = a56(a34(x1)) 766.23/281.95 766.23/281.95 a16(a16(x1)) = x1 + 8 >= x1 = x1 766.23/281.95 766.23/281.95 a16(x1) = x1 + 4 >= x1 + 4 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.95 766.23/281.95 a25(x1) = x1 + 8 >= x1 = a23(a34(a45(a34(a23(x1))))) 766.23/281.95 766.23/281.95 a35(x1) = x1 >= x1 = a34(a45(a34(x1))) 766.23/281.95 766.23/281.95 a36(x1) = x1 + 4 >= x1 + 4 = a34(a45(a56(a45(a34(x1))))) 766.23/281.95 766.23/281.95 a13(a13(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a13(x1) = x1 >= x1 = a12(a23(a12(x1))) 766.23/281.95 766.23/281.95 a12(a12(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a14(a14(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a15(a15(x1)) = x1 + 4 >= x1 = x1 766.23/281.95 766.23/281.95 a24(a24(x1)) = x1 + 2 >= x1 = x1 766.23/281.95 766.23/281.95 a25(a25(x1)) = x1 + 16 >= x1 = x1 766.23/281.95 766.23/281.95 a26(a26(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a34(a34(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a35(a35(x1)) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a36(a36(x1)) = x1 + 8 >= x1 = x1 766.23/281.95 766.23/281.95 a46(a46(x1)) = x1 + 8 >= x1 = x1 766.23/281.95 766.23/281.95 a46(x1) = x1 + 4 >= x1 + 4 = a45(a56(a45(x1))) 766.23/281.95 766.23/281.95 a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1 766.23/281.95 766.23/281.95 a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1 766.23/281.95 problem: 766.23/281.95 strict: 766.23/281.95 a23(a23(x1)) -> x1 766.23/281.95 a45(a45(x1)) -> x1 766.23/281.95 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.23/281.95 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.95 a12(a34(x1)) -> a34(a12(x1)) 766.23/281.95 a12(a45(x1)) -> a45(a12(x1)) 766.23/281.95 a12(a56(x1)) -> a56(a12(x1)) 766.23/281.95 a23(a45(x1)) -> a45(a23(x1)) 766.23/281.95 a23(a56(x1)) -> a56(a23(x1)) 766.23/281.95 a34(a56(x1)) -> a56(a34(x1)) 766.23/281.95 weak: 766.23/281.95 a56(a56(x1)) -> x1 766.23/281.95 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.95 a24(x1) -> a23(a34(a23(x1))) 766.23/281.95 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.23/281.95 a16(a16(x1)) -> x1 766.23/281.95 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.95 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.23/281.96 a35(x1) -> a34(a45(a34(x1))) 766.23/281.96 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.23/281.96 a13(a13(x1)) -> x1 766.23/281.96 a13(x1) -> a12(a23(a12(x1))) 766.23/281.96 a12(a12(x1)) -> x1 766.23/281.96 a14(a14(x1)) -> x1 766.23/281.96 a15(a15(x1)) -> x1 766.23/281.96 a24(a24(x1)) -> x1 766.23/281.96 a25(a25(x1)) -> x1 766.23/281.96 a26(a26(x1)) -> x1 766.23/281.96 a34(a34(x1)) -> x1 766.23/281.96 a35(a35(x1)) -> x1 766.23/281.96 a36(a36(x1)) -> x1 766.23/281.96 a46(a46(x1)) -> x1 766.23/281.96 a46(x1) -> a45(a56(a45(x1))) 766.23/281.96 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.23/281.96 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.23/281.96 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.23/281.96 Matrix Interpretation Processor: dim=1 766.23/281.96 766.23/281.96 max_matrix: 766.23/281.96 1 766.23/281.96 interpretation: 766.23/281.96 [a56](x0) = x0 + 3, 766.23/281.96 766.23/281.96 [a46](x0) = x0 + 8, 766.23/281.96 766.23/281.96 [a45](x0) = x0 + 1, 766.23/281.96 766.23/281.96 [a36](x0) = x0 + 6, 766.23/281.96 766.23/281.96 [a35](x0) = x0 + 1, 766.23/281.96 766.23/281.96 [a34](x0) = x0, 766.23/281.96 766.23/281.96 [a26](x0) = x0 + 3, 766.23/281.96 766.23/281.96 [a25](x0) = x0 + 3, 766.23/281.96 766.23/281.96 [a24](x0) = x0 + 8, 766.23/281.96 766.23/281.96 [a23](x0) = x0 + 1, 766.23/281.96 766.23/281.96 [a16](x0) = x0 + 29, 766.23/281.96 766.23/281.96 [a15](x0) = x0 + 25, 766.23/281.96 766.23/281.96 [a14](x0) = x0 + 16, 766.23/281.96 766.23/281.96 [a13](x0) = x0 + 23, 766.23/281.96 766.23/281.96 [a12](x0) = x0 + 11 766.23/281.96 orientation: 766.23/281.96 a23(a23(x1)) = x1 + 2 >= x1 = x1 766.23/281.96 766.23/281.96 a45(a45(x1)) = x1 + 2 >= x1 = x1 766.23/281.96 766.23/281.96 a14(x1) = x1 + 16 >= x1 + 24 = a12(a23(a34(a23(a12(x1))))) 766.23/281.96 766.23/281.96 a26(x1) = x1 + 3 >= x1 + 7 = a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.96 766.23/281.96 a12(a34(x1)) = x1 + 11 >= x1 + 11 = a34(a12(x1)) 766.23/281.96 766.23/281.96 a12(a45(x1)) = x1 + 12 >= x1 + 12 = a45(a12(x1)) 766.23/281.96 766.23/281.96 a12(a56(x1)) = x1 + 14 >= x1 + 14 = a56(a12(x1)) 766.23/281.96 766.23/281.96 a23(a45(x1)) = x1 + 2 >= x1 + 2 = a45(a23(x1)) 766.23/281.96 766.23/281.96 a23(a56(x1)) = x1 + 4 >= x1 + 4 = a56(a23(x1)) 766.23/281.96 766.23/281.96 a34(a56(x1)) = x1 + 3 >= x1 + 3 = a56(a34(x1)) 766.23/281.96 766.23/281.96 a56(a56(x1)) = x1 + 6 >= x1 = x1 766.23/281.96 766.23/281.96 a15(x1) = x1 + 25 >= x1 + 25 = a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.96 766.23/281.96 a24(x1) = x1 + 8 >= x1 + 2 = a23(a34(a23(x1))) 766.23/281.96 766.23/281.96 a45(a56(a45(a56(a45(a56(x1)))))) = x1 + 12 >= x1 = x1 766.23/281.96 766.23/281.96 a16(a16(x1)) = x1 + 58 >= x1 = x1 766.23/281.96 766.23/281.96 a16(x1) = x1 + 29 >= x1 + 29 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.96 766.23/281.96 a25(x1) = x1 + 3 >= x1 + 3 = a23(a34(a45(a34(a23(x1))))) 766.23/281.96 766.23/281.96 a35(x1) = x1 + 1 >= x1 + 1 = a34(a45(a34(x1))) 766.23/281.96 766.23/281.96 a36(x1) = x1 + 6 >= x1 + 5 = a34(a45(a56(a45(a34(x1))))) 766.23/281.96 766.23/281.96 a13(a13(x1)) = x1 + 46 >= x1 = x1 766.23/281.96 766.23/281.96 a13(x1) = x1 + 23 >= x1 + 23 = a12(a23(a12(x1))) 766.23/281.96 766.23/281.96 a12(a12(x1)) = x1 + 22 >= x1 = x1 766.23/281.96 766.23/281.96 a14(a14(x1)) = x1 + 32 >= x1 = x1 766.23/281.96 766.23/281.96 a15(a15(x1)) = x1 + 50 >= x1 = x1 766.23/281.96 766.23/281.96 a24(a24(x1)) = x1 + 16 >= x1 = x1 766.23/281.96 766.23/281.96 a25(a25(x1)) = x1 + 6 >= x1 = x1 766.23/281.96 766.23/281.96 a26(a26(x1)) = x1 + 6 >= x1 = x1 766.23/281.96 766.23/281.96 a34(a34(x1)) = x1 >= x1 = x1 766.23/281.96 766.23/281.96 a35(a35(x1)) = x1 + 2 >= x1 = x1 766.23/281.96 766.23/281.96 a36(a36(x1)) = x1 + 12 >= x1 = x1 766.23/281.96 766.23/281.96 a46(a46(x1)) = x1 + 16 >= x1 = x1 766.23/281.96 766.23/281.96 a46(x1) = x1 + 8 >= x1 + 5 = a45(a56(a45(x1))) 766.23/281.96 766.23/281.96 a12(a23(a12(a23(a12(a23(x1)))))) = x1 + 36 >= x1 = x1 766.23/281.96 766.23/281.96 a23(a34(a23(a34(a23(a34(x1)))))) = x1 + 3 >= x1 = x1 766.23/281.96 766.23/281.96 a34(a45(a34(a45(a34(a45(x1)))))) = x1 + 3 >= x1 = x1 766.23/281.96 problem: 766.23/281.96 strict: 766.23/281.96 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.23/281.96 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.96 a12(a34(x1)) -> a34(a12(x1)) 766.23/281.96 a12(a45(x1)) -> a45(a12(x1)) 766.23/281.96 a12(a56(x1)) -> a56(a12(x1)) 766.23/281.96 a23(a45(x1)) -> a45(a23(x1)) 766.23/281.96 a23(a56(x1)) -> a56(a23(x1)) 766.23/281.96 a34(a56(x1)) -> a56(a34(x1)) 766.23/281.96 weak: 766.23/281.96 a23(a23(x1)) -> x1 766.23/281.96 a45(a45(x1)) -> x1 766.23/281.96 a56(a56(x1)) -> x1 766.23/281.96 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.96 a24(x1) -> a23(a34(a23(x1))) 766.23/281.96 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.23/281.96 a16(a16(x1)) -> x1 766.23/281.96 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.96 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.23/281.96 a35(x1) -> a34(a45(a34(x1))) 766.23/281.96 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.23/281.96 a13(a13(x1)) -> x1 766.23/281.96 a13(x1) -> a12(a23(a12(x1))) 766.23/281.96 a12(a12(x1)) -> x1 766.23/281.96 a14(a14(x1)) -> x1 766.23/281.96 a15(a15(x1)) -> x1 766.23/281.96 a24(a24(x1)) -> x1 766.23/281.96 a25(a25(x1)) -> x1 766.23/281.96 a26(a26(x1)) -> x1 766.23/281.96 a34(a34(x1)) -> x1 766.23/281.96 a35(a35(x1)) -> x1 766.23/281.96 a36(a36(x1)) -> x1 766.23/281.96 a46(a46(x1)) -> x1 766.23/281.96 a46(x1) -> a45(a56(a45(x1))) 766.23/281.96 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.23/281.96 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.23/281.96 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.23/281.96 Matrix Interpretation Processor: dim=1 766.23/281.96 766.23/281.96 max_matrix: 766.23/281.96 1 766.23/281.96 interpretation: 766.23/281.96 [a56](x0) = x0 + 4, 766.23/281.96 766.23/281.96 [a46](x0) = x0 + 4, 766.23/281.96 766.23/281.96 [a45](x0) = x0, 766.23/281.96 766.23/281.96 [a36](x0) = x0 + 11, 766.23/281.96 766.23/281.96 [a35](x0) = x0, 766.23/281.96 766.23/281.96 [a34](x0) = x0, 766.23/281.96 766.23/281.96 [a26](x0) = x0, 766.23/281.96 766.23/281.96 [a25](x0) = x0 + 1, 766.23/281.96 766.23/281.96 [a24](x0) = x0, 766.23/281.96 766.23/281.96 [a23](x0) = x0, 766.23/281.96 766.23/281.96 [a16](x0) = x0 + 6, 766.23/281.96 766.23/281.96 [a15](x0) = x0 + 12, 766.23/281.96 766.23/281.96 [a14](x0) = x0 + 14, 766.23/281.96 766.23/281.96 [a13](x0) = x0 + 2, 766.23/281.96 766.23/281.96 [a12](x0) = x0 + 1 766.23/281.96 orientation: 766.23/281.96 a14(x1) = x1 + 14 >= x1 + 2 = a12(a23(a34(a23(a12(x1))))) 766.23/281.96 766.23/281.96 a26(x1) = x1 >= x1 + 4 = a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.96 766.23/281.96 a12(a34(x1)) = x1 + 1 >= x1 + 1 = a34(a12(x1)) 766.23/281.96 766.23/281.96 a12(a45(x1)) = x1 + 1 >= x1 + 1 = a45(a12(x1)) 766.23/281.96 766.23/281.96 a12(a56(x1)) = x1 + 5 >= x1 + 5 = a56(a12(x1)) 766.23/281.96 766.23/281.96 a23(a45(x1)) = x1 >= x1 = a45(a23(x1)) 766.23/281.96 766.23/281.96 a23(a56(x1)) = x1 + 4 >= x1 + 4 = a56(a23(x1)) 766.23/281.96 766.23/281.96 a34(a56(x1)) = x1 + 4 >= x1 + 4 = a56(a34(x1)) 766.23/281.96 766.23/281.96 a23(a23(x1)) = x1 >= x1 = x1 766.23/281.96 766.23/281.96 a45(a45(x1)) = x1 >= x1 = x1 766.23/281.96 766.23/281.96 a56(a56(x1)) = x1 + 8 >= x1 = x1 766.23/281.96 766.23/281.96 a15(x1) = x1 + 12 >= x1 + 2 = a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.96 766.23/281.96 a24(x1) = x1 >= x1 = a23(a34(a23(x1))) 766.23/281.96 766.23/281.96 a45(a56(a45(a56(a45(a56(x1)))))) = x1 + 12 >= x1 = x1 766.23/281.96 766.23/281.96 a16(a16(x1)) = x1 + 12 >= x1 = x1 766.23/281.96 766.23/281.96 a16(x1) = x1 + 6 >= x1 + 6 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.96 766.23/281.96 a25(x1) = x1 + 1 >= x1 = a23(a34(a45(a34(a23(x1))))) 766.23/281.96 766.23/281.96 a35(x1) = x1 >= x1 = a34(a45(a34(x1))) 766.23/281.96 766.23/281.96 a36(x1) = x1 + 11 >= x1 + 4 = a34(a45(a56(a45(a34(x1))))) 766.23/281.96 766.23/281.96 a13(a13(x1)) = x1 + 4 >= x1 = x1 766.23/281.96 766.23/281.96 a13(x1) = x1 + 2 >= x1 + 2 = a12(a23(a12(x1))) 766.23/281.96 766.23/281.96 a12(a12(x1)) = x1 + 2 >= x1 = x1 766.23/281.96 766.23/281.96 a14(a14(x1)) = x1 + 28 >= x1 = x1 766.23/281.96 766.23/281.96 a15(a15(x1)) = x1 + 24 >= x1 = x1 766.23/281.96 766.23/281.96 a24(a24(x1)) = x1 >= x1 = x1 766.23/281.96 766.23/281.96 a25(a25(x1)) = x1 + 2 >= x1 = x1 766.23/281.96 766.23/281.96 a26(a26(x1)) = x1 >= x1 = x1 766.23/281.96 766.23/281.96 a34(a34(x1)) = x1 >= x1 = x1 766.23/281.96 766.23/281.96 a35(a35(x1)) = x1 >= x1 = x1 766.23/281.96 766.23/281.96 a36(a36(x1)) = x1 + 22 >= x1 = x1 766.23/281.96 766.23/281.96 a46(a46(x1)) = x1 + 8 >= x1 = x1 766.23/281.96 766.23/281.96 a46(x1) = x1 + 4 >= x1 + 4 = a45(a56(a45(x1))) 766.23/281.96 766.23/281.96 a12(a23(a12(a23(a12(a23(x1)))))) = x1 + 3 >= x1 = x1 766.23/281.96 766.23/281.96 a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1 766.23/281.96 766.23/281.96 a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1 766.23/281.96 problem: 766.23/281.96 strict: 766.23/281.96 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.96 a12(a34(x1)) -> a34(a12(x1)) 766.23/281.96 a12(a45(x1)) -> a45(a12(x1)) 766.23/281.96 a12(a56(x1)) -> a56(a12(x1)) 766.23/281.96 a23(a45(x1)) -> a45(a23(x1)) 766.23/281.96 a23(a56(x1)) -> a56(a23(x1)) 766.23/281.96 a34(a56(x1)) -> a56(a34(x1)) 766.23/281.96 weak: 766.23/281.96 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.23/281.96 a23(a23(x1)) -> x1 766.23/281.96 a45(a45(x1)) -> x1 766.23/281.96 a56(a56(x1)) -> x1 766.23/281.96 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.97 a24(x1) -> a23(a34(a23(x1))) 766.23/281.97 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.23/281.97 a16(a16(x1)) -> x1 766.23/281.97 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.97 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.23/281.97 a35(x1) -> a34(a45(a34(x1))) 766.23/281.97 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.23/281.97 a13(a13(x1)) -> x1 766.23/281.97 a13(x1) -> a12(a23(a12(x1))) 766.23/281.97 a12(a12(x1)) -> x1 766.23/281.97 a14(a14(x1)) -> x1 766.23/281.97 a15(a15(x1)) -> x1 766.23/281.97 a24(a24(x1)) -> x1 766.23/281.97 a25(a25(x1)) -> x1 766.23/281.97 a26(a26(x1)) -> x1 766.23/281.97 a34(a34(x1)) -> x1 766.23/281.97 a35(a35(x1)) -> x1 766.23/281.97 a36(a36(x1)) -> x1 766.23/281.97 a46(a46(x1)) -> x1 766.23/281.97 a46(x1) -> a45(a56(a45(x1))) 766.23/281.97 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.23/281.97 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.23/281.97 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.23/281.97 Matrix Interpretation Processor: dim=1 766.23/281.97 766.23/281.97 max_matrix: 766.23/281.97 1 766.23/281.97 interpretation: 766.23/281.97 [a56](x0) = x0 + 4, 766.23/281.97 766.23/281.97 [a46](x0) = x0 + 8, 766.23/281.97 766.23/281.97 [a45](x0) = x0, 766.23/281.97 766.23/281.97 [a36](x0) = x0 + 4, 766.23/281.97 766.23/281.97 [a35](x0) = x0 + 1, 766.23/281.97 766.23/281.97 [a34](x0) = x0, 766.23/281.97 766.23/281.97 [a26](x0) = x0 + 12, 766.23/281.97 766.23/281.97 [a25](x0) = x0 + 2, 766.23/281.97 766.23/281.97 [a24](x0) = x0 + 10, 766.23/281.97 766.23/281.97 [a23](x0) = x0 + 1, 766.23/281.97 766.23/281.97 [a16](x0) = x0 + 8, 766.23/281.97 766.23/281.97 [a15](x0) = x0 + 4, 766.23/281.97 766.23/281.97 [a14](x0) = x0 + 8, 766.23/281.97 766.23/281.97 [a13](x0) = x0 + 3, 766.23/281.97 766.23/281.97 [a12](x0) = x0 + 1 766.23/281.97 orientation: 766.23/281.97 a26(x1) = x1 + 12 >= x1 + 6 = a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.97 766.23/281.97 a12(a34(x1)) = x1 + 1 >= x1 + 1 = a34(a12(x1)) 766.23/281.97 766.23/281.97 a12(a45(x1)) = x1 + 1 >= x1 + 1 = a45(a12(x1)) 766.23/281.97 766.23/281.97 a12(a56(x1)) = x1 + 5 >= x1 + 5 = a56(a12(x1)) 766.23/281.97 766.23/281.97 a23(a45(x1)) = x1 + 1 >= x1 + 1 = a45(a23(x1)) 766.23/281.97 766.23/281.97 a23(a56(x1)) = x1 + 5 >= x1 + 5 = a56(a23(x1)) 766.23/281.97 766.23/281.97 a34(a56(x1)) = x1 + 4 >= x1 + 4 = a56(a34(x1)) 766.23/281.97 766.23/281.97 a14(x1) = x1 + 8 >= x1 + 4 = a12(a23(a34(a23(a12(x1))))) 766.23/281.97 766.23/281.97 a23(a23(x1)) = x1 + 2 >= x1 = x1 766.23/281.97 766.23/281.97 a45(a45(x1)) = x1 >= x1 = x1 766.23/281.97 766.23/281.97 a56(a56(x1)) = x1 + 8 >= x1 = x1 766.23/281.97 766.23/281.97 a15(x1) = x1 + 4 >= x1 + 4 = a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.97 766.23/281.97 a24(x1) = x1 + 10 >= x1 + 2 = a23(a34(a23(x1))) 766.23/281.97 766.23/281.97 a45(a56(a45(a56(a45(a56(x1)))))) = x1 + 12 >= x1 = x1 766.23/281.97 766.23/281.97 a16(a16(x1)) = x1 + 16 >= x1 = x1 766.23/281.97 766.23/281.97 a16(x1) = x1 + 8 >= x1 + 8 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.97 766.23/281.97 a25(x1) = x1 + 2 >= x1 + 2 = a23(a34(a45(a34(a23(x1))))) 766.23/281.97 766.23/281.97 a35(x1) = x1 + 1 >= x1 = a34(a45(a34(x1))) 766.23/281.97 766.23/281.97 a36(x1) = x1 + 4 >= x1 + 4 = a34(a45(a56(a45(a34(x1))))) 766.23/281.97 766.23/281.97 a13(a13(x1)) = x1 + 6 >= x1 = x1 766.23/281.97 766.23/281.97 a13(x1) = x1 + 3 >= x1 + 3 = a12(a23(a12(x1))) 766.23/281.97 766.23/281.97 a12(a12(x1)) = x1 + 2 >= x1 = x1 766.23/281.97 766.23/281.97 a14(a14(x1)) = x1 + 16 >= x1 = x1 766.23/281.97 766.23/281.97 a15(a15(x1)) = x1 + 8 >= x1 = x1 766.23/281.97 766.23/281.97 a24(a24(x1)) = x1 + 20 >= x1 = x1 766.23/281.97 766.23/281.97 a25(a25(x1)) = x1 + 4 >= x1 = x1 766.23/281.97 766.23/281.97 a26(a26(x1)) = x1 + 24 >= x1 = x1 766.23/281.97 766.23/281.97 a34(a34(x1)) = x1 >= x1 = x1 766.23/281.97 766.23/281.97 a35(a35(x1)) = x1 + 2 >= x1 = x1 766.23/281.97 766.23/281.97 a36(a36(x1)) = x1 + 8 >= x1 = x1 766.23/281.97 766.23/281.97 a46(a46(x1)) = x1 + 16 >= x1 = x1 766.23/281.97 766.23/281.97 a46(x1) = x1 + 8 >= x1 + 4 = a45(a56(a45(x1))) 766.23/281.97 766.23/281.97 a12(a23(a12(a23(a12(a23(x1)))))) = x1 + 6 >= x1 = x1 766.23/281.97 766.23/281.97 a23(a34(a23(a34(a23(a34(x1)))))) = x1 + 3 >= x1 = x1 766.23/281.97 766.23/281.97 a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1 766.23/281.97 problem: 766.23/281.97 strict: 766.23/281.97 a12(a34(x1)) -> a34(a12(x1)) 766.23/281.97 a12(a45(x1)) -> a45(a12(x1)) 766.23/281.97 a12(a56(x1)) -> a56(a12(x1)) 766.23/281.97 a23(a45(x1)) -> a45(a23(x1)) 766.23/281.97 a23(a56(x1)) -> a56(a23(x1)) 766.23/281.97 a34(a56(x1)) -> a56(a34(x1)) 766.23/281.97 weak: 766.23/281.97 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.97 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.23/281.97 a23(a23(x1)) -> x1 766.23/281.97 a45(a45(x1)) -> x1 766.23/281.97 a56(a56(x1)) -> x1 766.23/281.97 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.97 a24(x1) -> a23(a34(a23(x1))) 766.23/281.97 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.23/281.97 a16(a16(x1)) -> x1 766.23/281.97 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.97 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.23/281.97 a35(x1) -> a34(a45(a34(x1))) 766.23/281.97 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.23/281.97 a13(a13(x1)) -> x1 766.23/281.97 a13(x1) -> a12(a23(a12(x1))) 766.23/281.97 a12(a12(x1)) -> x1 766.23/281.97 a14(a14(x1)) -> x1 766.23/281.97 a15(a15(x1)) -> x1 766.23/281.97 a24(a24(x1)) -> x1 766.23/281.97 a25(a25(x1)) -> x1 766.23/281.97 a26(a26(x1)) -> x1 766.23/281.97 a34(a34(x1)) -> x1 766.23/281.97 a35(a35(x1)) -> x1 766.23/281.97 a36(a36(x1)) -> x1 766.23/281.97 a46(a46(x1)) -> x1 766.23/281.97 a46(x1) -> a45(a56(a45(x1))) 766.23/281.97 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.23/281.97 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.23/281.97 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.23/281.97 Matrix Interpretation Processor: dim=2 766.23/281.97 766.23/281.97 max_matrix: 766.23/281.97 [1 2] 766.23/281.97 [0 1] 766.23/281.97 interpretation: 766.23/281.97 [0] 766.23/281.97 [a56](x0) = x0 + [1], 766.23/281.97 766.23/281.97 [1 1] [2] 766.23/281.97 [a46](x0) = [0 1]x0 + [2], 766.23/281.97 766.23/281.97 766.23/281.97 [a45](x0) = x0, 766.23/281.97 766.23/281.97 [0] 766.23/281.97 [a36](x0) = x0 + [2], 766.23/281.97 766.23/281.97 [0] 766.23/281.97 [a35](x0) = x0 + [1], 766.23/281.97 766.23/281.97 766.23/281.97 [a34](x0) = x0, 766.23/281.97 766.23/281.97 [1 2] [1] 766.23/281.97 [a26](x0) = [0 1]x0 + [1], 766.23/281.97 766.23/281.97 [1 2] 766.23/281.97 [a25](x0) = [0 1]x0, 766.23/281.97 766.23/281.97 [1 2] [0] 766.23/281.97 [a24](x0) = [0 1]x0 + [2], 766.23/281.97 766.23/281.97 [1 1] 766.23/281.97 [a23](x0) = [0 1]x0, 766.23/281.97 766.23/281.97 [1 2] [2] 766.23/281.97 [a16](x0) = [0 1]x0 + [1], 766.23/281.97 766.23/281.97 [1 2] [2] 766.23/281.97 [a15](x0) = [0 1]x0 + [0], 766.23/281.97 766.23/281.97 [1 2] [0] 766.23/281.97 [a14](x0) = [0 1]x0 + [2], 766.23/281.97 766.23/281.97 [1 1] [2] 766.23/281.97 [a13](x0) = [0 1]x0 + [3], 766.23/281.97 766.23/281.97 766.23/281.97 [a12](x0) = x0 766.23/281.97 orientation: 766.23/281.97 766.23/281.97 a12(a34(x1)) = x1 >= x1 = a34(a12(x1)) 766.23/281.97 766.23/281.97 766.23/281.97 a12(a45(x1)) = x1 >= x1 = a45(a12(x1)) 766.23/281.97 766.23/281.97 [0] [0] 766.23/281.97 a12(a56(x1)) = x1 + [1] >= x1 + [1] = a56(a12(x1)) 766.23/281.97 766.23/281.97 [1 1] [1 1] 766.23/281.97 a23(a45(x1)) = [0 1]x1 >= [0 1]x1 = a45(a23(x1)) 766.23/281.97 766.23/281.97 [1 1] [1] [1 1] [0] 766.23/281.97 a23(a56(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a56(a23(x1)) 766.23/281.97 766.23/281.97 [0] [0] 766.23/281.97 a34(a56(x1)) = x1 + [1] >= x1 + [1] = a56(a34(x1)) 766.23/281.97 766.23/281.97 [1 2] [1] [1 2] [1] 766.23/281.97 a26(x1) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.97 766.23/281.97 [1 2] [0] [1 2] 766.23/281.97 a14(x1) = [0 1]x1 + [2] >= [0 1]x1 = a12(a23(a34(a23(a12(x1))))) 766.23/281.97 766.23/281.97 [1 2] 766.23/281.97 a23(a23(x1)) = [0 1]x1 >= x1 = x1 766.23/281.97 766.23/281.97 766.23/281.97 a45(a45(x1)) = x1 >= x1 = x1 766.23/281.97 766.23/281.97 [0] 766.23/281.97 a56(a56(x1)) = x1 + [2] >= x1 = x1 766.23/281.97 766.23/281.97 [1 2] [2] [1 2] 766.23/281.98 a15(x1) = [0 1]x1 + [0] >= [0 1]x1 = a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.98 766.23/281.98 [1 2] [0] [1 2] 766.23/281.98 a24(x1) = [0 1]x1 + [2] >= [0 1]x1 = a23(a34(a23(x1))) 766.23/281.98 766.23/281.98 [0] 766.23/281.98 a45(a56(a45(a56(a45(a56(x1)))))) = x1 + [3] >= x1 = x1 766.23/281.98 766.23/281.98 [1 4] [6] 766.23/281.98 a16(a16(x1)) = [0 1]x1 + [2] >= x1 = x1 766.23/281.98 766.23/281.98 [1 2] [2] [1 2] [1] 766.23/281.98 a16(x1) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.98 766.23/281.98 [1 2] [1 2] 766.23/281.98 a25(x1) = [0 1]x1 >= [0 1]x1 = a23(a34(a45(a34(a23(x1))))) 766.23/281.98 766.23/281.98 [0] 766.23/281.98 a35(x1) = x1 + [1] >= x1 = a34(a45(a34(x1))) 766.23/281.98 766.23/281.98 [0] [0] 766.23/281.98 a36(x1) = x1 + [2] >= x1 + [1] = a34(a45(a56(a45(a34(x1))))) 766.23/281.98 766.23/281.98 [1 2] [7] 766.23/281.98 a13(a13(x1)) = [0 1]x1 + [6] >= x1 = x1 766.23/281.98 766.23/281.98 [1 1] [2] [1 1] 766.23/281.98 a13(x1) = [0 1]x1 + [3] >= [0 1]x1 = a12(a23(a12(x1))) 766.23/281.98 766.23/281.98 766.23/281.98 a12(a12(x1)) = x1 >= x1 = x1 766.23/281.98 766.23/281.98 [1 4] [4] 766.23/281.98 a14(a14(x1)) = [0 1]x1 + [4] >= x1 = x1 766.23/281.98 766.23/281.98 [1 4] [4] 766.23/281.98 a15(a15(x1)) = [0 1]x1 + [0] >= x1 = x1 766.23/281.98 766.23/281.98 [1 4] [4] 766.23/281.98 a24(a24(x1)) = [0 1]x1 + [4] >= x1 = x1 766.23/281.98 766.23/281.98 [1 4] 766.23/281.98 a25(a25(x1)) = [0 1]x1 >= x1 = x1 766.23/281.98 766.23/281.98 [1 4] [4] 766.23/281.98 a26(a26(x1)) = [0 1]x1 + [2] >= x1 = x1 766.23/281.98 766.23/281.98 766.23/281.98 a34(a34(x1)) = x1 >= x1 = x1 766.23/281.98 766.23/281.98 [0] 766.23/281.98 a35(a35(x1)) = x1 + [2] >= x1 = x1 766.23/281.98 766.23/281.98 [0] 766.23/281.98 a36(a36(x1)) = x1 + [4] >= x1 = x1 766.23/281.98 766.23/281.98 [1 2] [6] 766.23/281.98 a46(a46(x1)) = [0 1]x1 + [4] >= x1 = x1 766.23/281.98 766.23/281.98 [1 1] [2] [0] 766.23/281.98 a46(x1) = [0 1]x1 + [2] >= x1 + [1] = a45(a56(a45(x1))) 766.23/281.98 766.23/281.98 [1 3] 766.23/281.98 a12(a23(a12(a23(a12(a23(x1)))))) = [0 1]x1 >= x1 = x1 766.23/281.98 766.23/281.98 [1 3] 766.23/281.98 a23(a34(a23(a34(a23(a34(x1)))))) = [0 1]x1 >= x1 = x1 766.23/281.98 766.23/281.98 766.23/281.98 a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1 766.23/281.98 problem: 766.23/281.98 strict: 766.23/281.98 a12(a34(x1)) -> a34(a12(x1)) 766.23/281.98 a12(a45(x1)) -> a45(a12(x1)) 766.23/281.98 a12(a56(x1)) -> a56(a12(x1)) 766.23/281.98 a23(a45(x1)) -> a45(a23(x1)) 766.23/281.98 a34(a56(x1)) -> a56(a34(x1)) 766.23/281.98 weak: 766.23/281.98 a23(a56(x1)) -> a56(a23(x1)) 766.23/281.98 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.98 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.23/281.98 a23(a23(x1)) -> x1 766.23/281.98 a45(a45(x1)) -> x1 766.23/281.98 a56(a56(x1)) -> x1 766.23/281.98 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.98 a24(x1) -> a23(a34(a23(x1))) 766.23/281.98 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.23/281.98 a16(a16(x1)) -> x1 766.23/281.98 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.98 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.23/281.98 a35(x1) -> a34(a45(a34(x1))) 766.23/281.98 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.23/281.98 a13(a13(x1)) -> x1 766.23/281.98 a13(x1) -> a12(a23(a12(x1))) 766.23/281.98 a12(a12(x1)) -> x1 766.23/281.98 a14(a14(x1)) -> x1 766.23/281.98 a15(a15(x1)) -> x1 766.23/281.98 a24(a24(x1)) -> x1 766.23/281.98 a25(a25(x1)) -> x1 766.23/281.98 a26(a26(x1)) -> x1 766.23/281.98 a34(a34(x1)) -> x1 766.23/281.98 a35(a35(x1)) -> x1 766.23/281.98 a36(a36(x1)) -> x1 766.23/281.98 a46(a46(x1)) -> x1 766.23/281.98 a46(x1) -> a45(a56(a45(x1))) 766.23/281.98 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.23/281.98 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.23/281.98 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.23/281.98 Matrix Interpretation Processor: dim=2 766.23/281.98 766.23/281.98 max_matrix: 766.23/281.98 [1 3] 766.23/281.98 [0 1] 766.23/281.98 interpretation: 766.23/281.98 [0] 766.23/281.98 [a56](x0) = x0 + [1], 766.23/281.98 766.23/281.98 [1 1] [1] 766.23/281.98 [a46](x0) = [0 1]x0 + [1], 766.23/281.98 766.23/281.98 766.23/281.98 [a45](x0) = x0, 766.23/281.98 766.23/281.98 [1 2] [1] 766.23/281.98 [a36](x0) = [0 1]x0 + [2], 766.23/281.98 766.23/281.98 [1 3] 766.23/281.98 [a35](x0) = [0 1]x0, 766.23/281.98 766.23/281.98 [1 1] 766.23/281.98 [a34](x0) = [0 1]x0, 766.23/281.98 766.23/281.98 [1 2] [1] 766.23/281.98 [a26](x0) = [0 1]x0 + [1], 766.23/281.98 766.23/281.98 [1 2] [0] 766.23/281.98 [a25](x0) = [0 1]x0 + [2], 766.23/281.98 766.23/281.98 [1 1] 766.23/281.98 [a24](x0) = [0 1]x0, 766.23/281.98 766.23/281.98 766.23/281.98 [a23](x0) = x0, 766.23/281.98 766.23/281.98 [1 2] [2] 766.23/281.98 [a16](x0) = [0 1]x0 + [1], 766.23/281.98 766.23/281.98 [1 2] [0] 766.23/281.98 [a15](x0) = [0 1]x0 + [1], 766.23/281.98 766.23/281.98 [1 3] 766.23/281.98 [a14](x0) = [0 1]x0, 766.23/281.98 766.23/281.98 766.23/281.98 [a13](x0) = x0, 766.23/281.98 766.23/281.98 766.23/281.98 [a12](x0) = x0 766.23/281.98 orientation: 766.23/281.98 [1 1] [1 1] 766.23/281.98 a12(a34(x1)) = [0 1]x1 >= [0 1]x1 = a34(a12(x1)) 766.23/281.98 766.23/281.98 766.23/281.98 a12(a45(x1)) = x1 >= x1 = a45(a12(x1)) 766.23/281.98 766.23/281.98 [0] [0] 766.23/281.98 a12(a56(x1)) = x1 + [1] >= x1 + [1] = a56(a12(x1)) 766.23/281.98 766.23/281.98 766.23/281.98 a23(a45(x1)) = x1 >= x1 = a45(a23(x1)) 766.23/281.98 766.23/281.98 [1 1] [1] [1 1] [0] 766.23/281.98 a34(a56(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a56(a34(x1)) 766.23/281.98 766.23/281.98 [0] [0] 766.23/281.98 a23(a56(x1)) = x1 + [1] >= x1 + [1] = a56(a23(x1)) 766.23/281.98 766.23/281.98 [1 2] [1] [1 2] [1] 766.23/281.98 a26(x1) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.98 766.23/281.98 [1 3] [1 1] 766.23/281.98 a14(x1) = [0 1]x1 >= [0 1]x1 = a12(a23(a34(a23(a12(x1))))) 766.23/281.98 766.23/281.98 766.23/281.98 a23(a23(x1)) = x1 >= x1 = x1 766.23/281.98 766.23/281.98 766.23/281.98 a45(a45(x1)) = x1 >= x1 = x1 766.23/281.98 766.23/281.98 [0] 766.23/281.98 a56(a56(x1)) = x1 + [2] >= x1 = x1 766.23/281.98 766.23/281.98 [1 2] [0] [1 2] 766.23/281.98 a15(x1) = [0 1]x1 + [1] >= [0 1]x1 = a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.98 766.23/281.98 [1 1] [1 1] 766.23/281.98 a24(x1) = [0 1]x1 >= [0 1]x1 = a23(a34(a23(x1))) 766.23/281.98 766.23/281.98 [0] 766.23/281.98 a45(a56(a45(a56(a45(a56(x1)))))) = x1 + [3] >= x1 = x1 766.23/281.98 766.23/281.98 [1 4] [6] 766.23/281.98 a16(a16(x1)) = [0 1]x1 + [2] >= x1 = x1 766.23/281.98 766.23/281.98 [1 2] [2] [1 2] [1] 766.23/281.98 a16(x1) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.98 766.23/281.98 [1 2] [0] [1 2] 766.23/281.99 a25(x1) = [0 1]x1 + [2] >= [0 1]x1 = a23(a34(a45(a34(a23(x1))))) 766.23/281.99 766.23/281.99 [1 3] [1 2] 766.23/281.99 a35(x1) = [0 1]x1 >= [0 1]x1 = a34(a45(a34(x1))) 766.23/281.99 766.23/281.99 [1 2] [1] [1 2] [1] 766.23/281.99 a36(x1) = [0 1]x1 + [2] >= [0 1]x1 + [1] = a34(a45(a56(a45(a34(x1))))) 766.23/281.99 766.23/281.99 766.23/281.99 a13(a13(x1)) = x1 >= x1 = x1 766.23/281.99 766.23/281.99 766.23/281.99 a13(x1) = x1 >= x1 = a12(a23(a12(x1))) 766.23/281.99 766.23/281.99 766.23/281.99 a12(a12(x1)) = x1 >= x1 = x1 766.23/281.99 766.23/281.99 [1 6] 766.23/281.99 a14(a14(x1)) = [0 1]x1 >= x1 = x1 766.23/281.99 766.23/281.99 [1 4] [2] 766.23/281.99 a15(a15(x1)) = [0 1]x1 + [2] >= x1 = x1 766.23/281.99 766.23/281.99 [1 2] 766.23/281.99 a24(a24(x1)) = [0 1]x1 >= x1 = x1 766.23/281.99 766.23/281.99 [1 4] [4] 766.23/281.99 a25(a25(x1)) = [0 1]x1 + [4] >= x1 = x1 766.23/281.99 766.23/281.99 [1 4] [4] 766.23/281.99 a26(a26(x1)) = [0 1]x1 + [2] >= x1 = x1 766.23/281.99 766.23/281.99 [1 2] 766.23/281.99 a34(a34(x1)) = [0 1]x1 >= x1 = x1 766.23/281.99 766.23/281.99 [1 6] 766.23/281.99 a35(a35(x1)) = [0 1]x1 >= x1 = x1 766.23/281.99 766.23/281.99 [1 4] [6] 766.23/281.99 a36(a36(x1)) = [0 1]x1 + [4] >= x1 = x1 766.23/281.99 766.23/281.99 [1 2] [3] 766.23/281.99 a46(a46(x1)) = [0 1]x1 + [2] >= x1 = x1 766.23/281.99 766.23/281.99 [1 1] [1] [0] 766.23/281.99 a46(x1) = [0 1]x1 + [1] >= x1 + [1] = a45(a56(a45(x1))) 766.23/281.99 766.23/281.99 766.23/281.99 a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1 766.23/281.99 766.23/281.99 [1 3] 766.23/281.99 a23(a34(a23(a34(a23(a34(x1)))))) = [0 1]x1 >= x1 = x1 766.23/281.99 766.23/281.99 [1 3] 766.23/281.99 a34(a45(a34(a45(a34(a45(x1)))))) = [0 1]x1 >= x1 = x1 766.23/281.99 problem: 766.23/281.99 strict: 766.23/281.99 a12(a34(x1)) -> a34(a12(x1)) 766.23/281.99 a12(a45(x1)) -> a45(a12(x1)) 766.23/281.99 a12(a56(x1)) -> a56(a12(x1)) 766.23/281.99 a23(a45(x1)) -> a45(a23(x1)) 766.23/281.99 weak: 766.23/281.99 a34(a56(x1)) -> a56(a34(x1)) 766.23/281.99 a23(a56(x1)) -> a56(a23(x1)) 766.23/281.99 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.99 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.23/281.99 a23(a23(x1)) -> x1 766.23/281.99 a45(a45(x1)) -> x1 766.23/281.99 a56(a56(x1)) -> x1 766.23/281.99 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.99 a24(x1) -> a23(a34(a23(x1))) 766.23/281.99 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.23/281.99 a16(a16(x1)) -> x1 766.23/281.99 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.99 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.23/281.99 a35(x1) -> a34(a45(a34(x1))) 766.23/281.99 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.23/281.99 a13(a13(x1)) -> x1 766.23/281.99 a13(x1) -> a12(a23(a12(x1))) 766.23/281.99 a12(a12(x1)) -> x1 766.23/281.99 a14(a14(x1)) -> x1 766.23/281.99 a15(a15(x1)) -> x1 766.23/281.99 a24(a24(x1)) -> x1 766.23/281.99 a25(a25(x1)) -> x1 766.23/281.99 a26(a26(x1)) -> x1 766.23/281.99 a34(a34(x1)) -> x1 766.23/281.99 a35(a35(x1)) -> x1 766.23/281.99 a36(a36(x1)) -> x1 766.23/281.99 a46(a46(x1)) -> x1 766.23/281.99 a46(x1) -> a45(a56(a45(x1))) 766.23/281.99 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.23/281.99 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.23/281.99 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.23/281.99 Matrix Interpretation Processor: dim=2 766.23/281.99 766.23/281.99 max_matrix: 766.23/281.99 [1 3] 766.23/281.99 [0 1] 766.23/281.99 interpretation: 766.23/281.99 [1 1] [0] 766.23/281.99 [a56](x0) = [0 1]x0 + [1], 766.23/281.99 766.23/281.99 [1 2] [0] 766.23/281.99 [a46](x0) = [0 1]x0 + [3], 766.23/281.99 766.23/281.99 766.23/281.99 [a45](x0) = x0, 766.23/281.99 766.23/281.99 [1 3] [1] 766.23/281.99 [a36](x0) = [0 1]x0 + [1], 766.23/281.99 766.23/281.99 [1 2] [3] 766.23/281.99 [a35](x0) = [0 1]x0 + [0], 766.23/281.99 766.23/281.99 766.23/281.99 [a34](x0) = x0, 766.23/281.99 766.23/281.99 [1 1] [2] 766.23/281.99 [a26](x0) = [0 1]x0 + [2], 766.23/281.99 766.23/281.99 [1 2] 766.23/281.99 [a25](x0) = [0 1]x0, 766.23/281.99 766.23/281.99 [2] 766.23/281.99 [a24](x0) = x0 + [1], 766.23/281.99 766.23/281.99 766.23/281.99 [a23](x0) = x0, 766.23/281.99 766.23/281.99 [1 3] [1] 766.23/281.99 [a16](x0) = [0 1]x0 + [1], 766.23/281.99 766.23/281.99 [1 2] 766.23/281.99 [a15](x0) = [0 1]x0, 766.23/281.99 766.23/281.99 [1 3] [2] 766.23/281.99 [a14](x0) = [0 1]x0 + [0], 766.23/281.99 766.23/281.99 [1 2] 766.23/281.99 [a13](x0) = [0 1]x0, 766.23/281.99 766.23/281.99 [1 1] 766.23/281.99 [a12](x0) = [0 1]x0 766.23/281.99 orientation: 766.23/281.99 [1 1] [1 1] 766.23/281.99 a12(a34(x1)) = [0 1]x1 >= [0 1]x1 = a34(a12(x1)) 766.23/281.99 766.23/281.99 [1 1] [1 1] 766.23/281.99 a12(a45(x1)) = [0 1]x1 >= [0 1]x1 = a45(a12(x1)) 766.23/281.99 766.23/281.99 [1 2] [1] [1 2] [0] 766.23/281.99 a12(a56(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a56(a12(x1)) 766.23/281.99 766.23/281.99 766.23/281.99 a23(a45(x1)) = x1 >= x1 = a45(a23(x1)) 766.23/281.99 766.23/281.99 [1 1] [0] [1 1] [0] 766.23/281.99 a34(a56(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a56(a34(x1)) 766.23/281.99 766.23/281.99 [1 1] [0] [1 1] [0] 766.23/281.99 a23(a56(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a56(a23(x1)) 766.23/281.99 766.23/281.99 [1 1] [2] [1 1] [0] 766.23/281.99 a26(x1) = [0 1]x1 + [2] >= [0 1]x1 + [1] = a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.23/281.99 766.23/281.99 [1 3] [2] [1 2] 766.23/281.99 a14(x1) = [0 1]x1 + [0] >= [0 1]x1 = a12(a23(a34(a23(a12(x1))))) 766.23/281.99 766.23/281.99 766.23/281.99 a23(a23(x1)) = x1 >= x1 = x1 766.23/281.99 766.23/281.99 766.23/281.99 a45(a45(x1)) = x1 >= x1 = x1 766.23/281.99 766.23/281.99 [1 2] [1] 766.23/281.99 a56(a56(x1)) = [0 1]x1 + [2] >= x1 = x1 766.23/281.99 766.23/281.99 [1 2] [1 2] 766.23/281.99 a15(x1) = [0 1]x1 >= [0 1]x1 = a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.23/281.99 766.23/281.99 [2] 766.23/281.99 a24(x1) = x1 + [1] >= x1 = a23(a34(a23(x1))) 766.23/281.99 766.23/281.99 [1 3] [3] 766.23/281.99 a45(a56(a45(a56(a45(a56(x1)))))) = [0 1]x1 + [3] >= x1 = x1 766.23/281.99 766.23/281.99 [1 6] [5] 766.23/281.99 a16(a16(x1)) = [0 1]x1 + [2] >= x1 = x1 766.23/281.99 766.23/281.99 [1 3] [1] [1 3] [1] 766.23/281.99 a16(x1) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.23/281.99 766.23/281.99 [1 2] 766.23/281.99 a25(x1) = [0 1]x1 >= x1 = a23(a34(a45(a34(a23(x1))))) 766.23/281.99 766.23/281.99 [1 2] [3] 766.23/281.99 a35(x1) = [0 1]x1 + [0] >= x1 = a34(a45(a34(x1))) 766.23/281.99 766.23/281.99 [1 3] [1] [1 1] [0] 766.23/281.99 a36(x1) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a34(a45(a56(a45(a34(x1))))) 766.23/281.99 766.23/281.99 [1 4] 766.23/281.99 a13(a13(x1)) = [0 1]x1 >= x1 = x1 766.23/281.99 766.23/281.99 [1 2] [1 2] 766.33/282.00 a13(x1) = [0 1]x1 >= [0 1]x1 = a12(a23(a12(x1))) 766.33/282.00 766.33/282.00 [1 2] 766.33/282.00 a12(a12(x1)) = [0 1]x1 >= x1 = x1 766.33/282.00 766.33/282.00 [1 6] [4] 766.33/282.00 a14(a14(x1)) = [0 1]x1 + [0] >= x1 = x1 766.33/282.00 766.33/282.00 [1 4] 766.33/282.00 a15(a15(x1)) = [0 1]x1 >= x1 = x1 766.33/282.00 766.33/282.00 [4] 766.33/282.00 a24(a24(x1)) = x1 + [2] >= x1 = x1 766.33/282.00 766.33/282.00 [1 4] 766.33/282.00 a25(a25(x1)) = [0 1]x1 >= x1 = x1 766.33/282.00 766.33/282.00 [1 2] [6] 766.33/282.00 a26(a26(x1)) = [0 1]x1 + [4] >= x1 = x1 766.33/282.00 766.33/282.00 766.33/282.00 a34(a34(x1)) = x1 >= x1 = x1 766.33/282.00 766.33/282.00 [1 4] [6] 766.33/282.00 a35(a35(x1)) = [0 1]x1 + [0] >= x1 = x1 766.33/282.00 766.33/282.00 [1 6] [5] 766.33/282.00 a36(a36(x1)) = [0 1]x1 + [2] >= x1 = x1 766.33/282.00 766.33/282.00 [1 4] [6] 766.33/282.00 a46(a46(x1)) = [0 1]x1 + [6] >= x1 = x1 766.33/282.00 766.33/282.00 [1 2] [0] [1 1] [0] 766.33/282.00 a46(x1) = [0 1]x1 + [3] >= [0 1]x1 + [1] = a45(a56(a45(x1))) 766.33/282.00 766.33/282.00 [1 3] 766.33/282.00 a12(a23(a12(a23(a12(a23(x1)))))) = [0 1]x1 >= x1 = x1 766.33/282.00 766.33/282.00 766.33/282.00 a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1 766.33/282.00 766.33/282.00 766.33/282.00 a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1 766.33/282.00 problem: 766.33/282.00 strict: 766.33/282.00 a12(a34(x1)) -> a34(a12(x1)) 766.33/282.00 a12(a45(x1)) -> a45(a12(x1)) 766.33/282.00 a23(a45(x1)) -> a45(a23(x1)) 766.33/282.00 weak: 766.33/282.00 a12(a56(x1)) -> a56(a12(x1)) 766.33/282.00 a34(a56(x1)) -> a56(a34(x1)) 766.33/282.00 a23(a56(x1)) -> a56(a23(x1)) 766.33/282.00 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.33/282.00 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.33/282.00 a23(a23(x1)) -> x1 766.33/282.00 a45(a45(x1)) -> x1 766.33/282.00 a56(a56(x1)) -> x1 766.33/282.00 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.33/282.00 a24(x1) -> a23(a34(a23(x1))) 766.33/282.00 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.33/282.00 a16(a16(x1)) -> x1 766.33/282.00 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.33/282.00 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.33/282.00 a35(x1) -> a34(a45(a34(x1))) 766.33/282.00 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.33/282.00 a13(a13(x1)) -> x1 766.33/282.00 a13(x1) -> a12(a23(a12(x1))) 766.33/282.00 a12(a12(x1)) -> x1 766.33/282.00 a14(a14(x1)) -> x1 766.33/282.00 a15(a15(x1)) -> x1 766.33/282.00 a24(a24(x1)) -> x1 766.33/282.00 a25(a25(x1)) -> x1 766.33/282.00 a26(a26(x1)) -> x1 766.33/282.00 a34(a34(x1)) -> x1 766.33/282.00 a35(a35(x1)) -> x1 766.33/282.00 a36(a36(x1)) -> x1 766.33/282.00 a46(a46(x1)) -> x1 766.33/282.00 a46(x1) -> a45(a56(a45(x1))) 766.33/282.00 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.33/282.00 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.33/282.00 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.33/282.00 Matrix Interpretation Processor: dim=2 766.33/282.00 766.33/282.00 max_matrix: 766.33/282.00 [1 4] 766.33/282.00 [0 1] 766.33/282.00 interpretation: 766.33/282.00 [1] 766.33/282.00 [a56](x0) = x0 + [1], 766.33/282.00 766.33/282.00 [1 4] [1] 766.33/282.00 [a46](x0) = [0 1]x0 + [3], 766.33/282.00 766.33/282.00 766.33/282.00 [a45](x0) = x0, 766.33/282.00 766.33/282.00 [1] 766.33/282.00 [a36](x0) = x0 + [5], 766.33/282.00 766.33/282.00 [1] 766.33/282.00 [a35](x0) = x0 + [2], 766.33/282.00 766.33/282.00 [0] 766.33/282.00 [a34](x0) = x0 + [1], 766.33/282.00 766.33/282.00 [1] 766.33/282.00 [a26](x0) = x0 + [4], 766.33/282.00 766.33/282.00 [0] 766.33/282.00 [a25](x0) = x0 + [4], 766.33/282.00 766.33/282.00 [1 4] [0] 766.33/282.00 [a24](x0) = [0 1]x0 + [3], 766.33/282.00 766.33/282.00 766.33/282.00 [a23](x0) = x0, 766.33/282.00 766.33/282.00 [1 2] [4] 766.33/282.00 [a16](x0) = [0 1]x0 + [3], 766.33/282.00 766.33/282.00 [1 4] [2] 766.33/282.00 [a15](x0) = [0 1]x0 + [2], 766.33/282.00 766.33/282.00 [1 4] [5] 766.33/282.00 [a14](x0) = [0 1]x0 + [1], 766.33/282.00 766.33/282.00 [1 2] [5] 766.33/282.00 [a13](x0) = [0 1]x0 + [0], 766.33/282.00 766.33/282.00 [1 1] 766.33/282.00 [a12](x0) = [0 1]x0 766.33/282.00 orientation: 766.33/282.00 [1 1] [1] [1 1] [0] 766.33/282.00 a12(a34(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a34(a12(x1)) 766.33/282.00 766.33/282.00 [1 1] [1 1] 766.33/282.00 a12(a45(x1)) = [0 1]x1 >= [0 1]x1 = a45(a12(x1)) 766.33/282.00 766.33/282.00 766.33/282.00 a23(a45(x1)) = x1 >= x1 = a45(a23(x1)) 766.33/282.00 766.33/282.00 [1 1] [2] [1 1] [1] 766.33/282.00 a12(a56(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a56(a12(x1)) 766.33/282.00 766.33/282.00 [1] [1] 766.33/282.00 a34(a56(x1)) = x1 + [2] >= x1 + [2] = a56(a34(x1)) 766.33/282.00 766.33/282.00 [1] [1] 766.33/282.00 a23(a56(x1)) = x1 + [1] >= x1 + [1] = a56(a23(x1)) 766.33/282.00 766.33/282.00 [1] [1] 766.33/282.00 a26(x1) = x1 + [4] >= x1 + [3] = a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.33/282.00 766.33/282.00 [1 4] [5] [1 2] [1] 766.33/282.00 a14(x1) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a12(a23(a34(a23(a12(x1))))) 766.33/282.00 766.33/282.00 766.33/282.00 a23(a23(x1)) = x1 >= x1 = x1 766.33/282.00 766.33/282.00 766.33/282.00 a45(a45(x1)) = x1 >= x1 = x1 766.33/282.00 766.33/282.00 [2] 766.33/282.00 a56(a56(x1)) = x1 + [2] >= x1 = x1 766.33/282.00 766.33/282.00 [1 4] [2] [1 2] [2] 766.33/282.00 a15(x1) = [0 1]x1 + [2] >= [0 1]x1 + [2] = a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.33/282.00 766.33/282.00 [1 4] [0] [0] 766.33/282.00 a24(x1) = [0 1]x1 + [3] >= x1 + [1] = a23(a34(a23(x1))) 766.33/282.00 766.33/282.00 [3] 766.33/282.00 a45(a56(a45(a56(a45(a56(x1)))))) = x1 + [3] >= x1 = x1 766.33/282.00 766.33/282.00 [1 4] [14] 766.33/282.00 a16(a16(x1)) = [0 1]x1 + [6 ] >= x1 = x1 766.33/282.00 766.33/282.00 [1 2] [4] [1 2] [4] 766.33/282.00 a16(x1) = [0 1]x1 + [3] >= [0 1]x1 + [3] = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.33/282.00 766.33/282.00 [0] [0] 766.33/282.00 a25(x1) = x1 + [4] >= x1 + [2] = a23(a34(a45(a34(a23(x1))))) 766.33/282.00 766.33/282.00 [1] [0] 766.33/282.00 a35(x1) = x1 + [2] >= x1 + [2] = a34(a45(a34(x1))) 766.33/282.00 766.33/282.00 [1] [1] 766.33/282.00 a36(x1) = x1 + [5] >= x1 + [3] = a34(a45(a56(a45(a34(x1))))) 766.33/282.00 766.33/282.00 [1 4] [10] 766.33/282.00 a13(a13(x1)) = [0 1]x1 + [0 ] >= x1 = x1 766.33/282.00 766.33/282.00 [1 2] [5] [1 2] 766.33/282.00 a13(x1) = [0 1]x1 + [0] >= [0 1]x1 = a12(a23(a12(x1))) 766.33/282.00 766.33/282.00 [1 2] 766.33/282.00 a12(a12(x1)) = [0 1]x1 >= x1 = x1 766.33/282.00 766.33/282.00 [1 8] [14] 766.33/282.00 a14(a14(x1)) = [0 1]x1 + [2 ] >= x1 = x1 766.33/282.00 766.33/282.00 [1 8] [12] 766.33/282.00 a15(a15(x1)) = [0 1]x1 + [4 ] >= x1 = x1 766.33/282.00 766.33/282.00 [1 8] [12] 766.33/282.00 a24(a24(x1)) = [0 1]x1 + [6 ] >= x1 = x1 766.33/282.00 766.33/282.00 [0] 766.33/282.00 a25(a25(x1)) = x1 + [8] >= x1 = x1 766.33/282.00 766.33/282.00 [2] 766.33/282.00 a26(a26(x1)) = x1 + [8] >= x1 = x1 766.33/282.00 766.33/282.00 [0] 766.33/282.00 a34(a34(x1)) = x1 + [2] >= x1 = x1 766.33/282.00 766.33/282.00 [2] 766.33/282.00 a35(a35(x1)) = x1 + [4] >= x1 = x1 766.33/282.00 766.33/282.00 [2 ] 766.33/282.00 a36(a36(x1)) = x1 + [10] >= x1 = x1 766.33/282.00 766.33/282.00 [1 8] [14] 766.33/282.00 a46(a46(x1)) = [0 1]x1 + [6 ] >= x1 = x1 766.33/282.00 766.33/282.00 [1 4] [1] [1] 766.33/282.00 a46(x1) = [0 1]x1 + [3] >= x1 + [1] = a45(a56(a45(x1))) 766.33/282.00 766.33/282.00 [1 3] 766.33/282.00 a12(a23(a12(a23(a12(a23(x1)))))) = [0 1]x1 >= x1 = x1 766.33/282.00 766.33/282.00 [0] 766.33/282.00 a23(a34(a23(a34(a23(a34(x1)))))) = x1 + [3] >= x1 = x1 766.33/282.00 766.33/282.00 [0] 766.33/282.00 a34(a45(a34(a45(a34(a45(x1)))))) = x1 + [3] >= x1 = x1 766.33/282.00 problem: 766.33/282.00 strict: 766.33/282.00 a12(a45(x1)) -> a45(a12(x1)) 766.33/282.00 a23(a45(x1)) -> a45(a23(x1)) 766.33/282.00 weak: 766.33/282.00 a12(a34(x1)) -> a34(a12(x1)) 766.33/282.00 a12(a56(x1)) -> a56(a12(x1)) 766.33/282.00 a34(a56(x1)) -> a56(a34(x1)) 766.33/282.00 a23(a56(x1)) -> a56(a23(x1)) 766.33/282.00 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.33/282.00 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.33/282.00 a23(a23(x1)) -> x1 766.33/282.00 a45(a45(x1)) -> x1 766.33/282.00 a56(a56(x1)) -> x1 766.33/282.00 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.33/282.00 a24(x1) -> a23(a34(a23(x1))) 766.33/282.00 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.33/282.00 a16(a16(x1)) -> x1 766.33/282.00 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.33/282.00 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.33/282.00 a35(x1) -> a34(a45(a34(x1))) 766.33/282.00 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.33/282.00 a13(a13(x1)) -> x1 766.33/282.00 a13(x1) -> a12(a23(a12(x1))) 766.33/282.00 a12(a12(x1)) -> x1 766.33/282.00 a14(a14(x1)) -> x1 766.33/282.00 a15(a15(x1)) -> x1 766.33/282.00 a24(a24(x1)) -> x1 766.33/282.00 a25(a25(x1)) -> x1 766.33/282.00 a26(a26(x1)) -> x1 766.33/282.00 a34(a34(x1)) -> x1 766.33/282.00 a35(a35(x1)) -> x1 766.33/282.00 a36(a36(x1)) -> x1 766.33/282.00 a46(a46(x1)) -> x1 766.33/282.00 a46(x1) -> a45(a56(a45(x1))) 766.33/282.00 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.33/282.00 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.33/282.00 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.33/282.00 Matrix Interpretation Processor: dim=2 766.33/282.00 766.33/282.00 max_matrix: 766.33/282.00 [1 4] 766.33/282.00 [0 1] 766.33/282.00 interpretation: 766.33/282.00 [1] 766.33/282.00 [a56](x0) = x0 + [0], 766.33/282.00 766.33/282.00 [2] 766.33/282.00 [a46](x0) = x0 + [2], 766.33/282.00 766.33/282.00 [0] 766.33/282.00 [a45](x0) = x0 + [1], 766.33/282.00 766.33/282.00 [4] 766.33/282.00 [a36](x0) = x0 + [2], 766.33/282.00 766.33/282.00 [0] 766.33/282.00 [a35](x0) = x0 + [1], 766.33/282.00 766.33/282.00 766.33/282.00 [a34](x0) = x0, 766.33/282.00 766.33/282.00 [1 3] [1] 766.33/282.00 [a26](x0) = [0 1]x0 + [2], 766.33/282.00 766.33/282.00 [0] 766.33/282.00 [a25](x0) = x0 + [4], 766.33/282.01 766.33/282.01 [3] 766.33/282.01 [a24](x0) = x0 + [0], 766.33/282.01 766.33/282.01 766.33/282.01 [a23](x0) = x0, 766.33/282.01 766.33/282.01 [1 3] [3] 766.33/282.01 [a16](x0) = [0 1]x0 + [3], 766.33/282.01 766.33/282.01 [1 4] [1] 766.33/282.01 [a15](x0) = [0 1]x0 + [2], 766.33/282.01 766.33/282.01 [1 4] 766.33/282.01 [a14](x0) = [0 1]x0, 766.33/282.01 766.33/282.01 [1 3] [1] 766.33/282.01 [a13](x0) = [0 1]x0 + [1], 766.33/282.01 766.33/282.01 [1 1] 766.33/282.01 [a12](x0) = [0 1]x0 766.33/282.01 orientation: 766.33/282.01 [1 1] [1] [1 1] [0] 766.33/282.01 a12(a45(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a45(a12(x1)) 766.33/282.01 766.33/282.01 [0] [0] 766.33/282.01 a23(a45(x1)) = x1 + [1] >= x1 + [1] = a45(a23(x1)) 766.33/282.01 766.33/282.01 [1 1] [1 1] 766.33/282.01 a12(a34(x1)) = [0 1]x1 >= [0 1]x1 = a34(a12(x1)) 766.33/282.01 766.33/282.01 [1 1] [1] [1 1] [1] 766.33/282.01 a12(a56(x1)) = [0 1]x1 + [0] >= [0 1]x1 + [0] = a56(a12(x1)) 766.33/282.01 766.33/282.01 [1] [1] 766.33/282.01 a34(a56(x1)) = x1 + [0] >= x1 + [0] = a56(a34(x1)) 766.33/282.01 766.33/282.01 [1] [1] 766.33/282.01 a23(a56(x1)) = x1 + [0] >= x1 + [0] = a56(a23(x1)) 766.33/282.01 766.33/282.01 [1 3] [1] [1] 766.33/282.01 a26(x1) = [0 1]x1 + [2] >= x1 + [2] = a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.33/282.01 766.33/282.01 [1 4] [1 2] 766.33/282.01 a14(x1) = [0 1]x1 >= [0 1]x1 = a12(a23(a34(a23(a12(x1))))) 766.33/282.01 766.33/282.01 766.33/282.01 a23(a23(x1)) = x1 >= x1 = x1 766.33/282.01 766.33/282.01 [0] 766.33/282.01 a45(a45(x1)) = x1 + [2] >= x1 = x1 766.33/282.01 766.33/282.01 [2] 766.33/282.01 a56(a56(x1)) = x1 + [0] >= x1 = x1 766.33/282.01 766.33/282.01 [1 4] [1] [1 2] [1] 766.33/282.01 a15(x1) = [0 1]x1 + [2] >= [0 1]x1 + [1] = a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.33/282.01 766.33/282.01 [3] 766.33/282.01 a24(x1) = x1 + [0] >= x1 = a23(a34(a23(x1))) 766.33/282.01 766.33/282.01 [3] 766.33/282.01 a45(a56(a45(a56(a45(a56(x1)))))) = x1 + [3] >= x1 = x1 766.33/282.01 766.33/282.01 [1 6] [15] 766.33/282.01 a16(a16(x1)) = [0 1]x1 + [6 ] >= x1 = x1 766.33/282.01 766.33/282.01 [1 3] [3] [1 2] [3] 766.33/282.01 a16(x1) = [0 1]x1 + [3] >= [0 1]x1 + [2] = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.33/282.01 766.33/282.01 [0] [0] 766.33/282.01 a25(x1) = x1 + [4] >= x1 + [1] = a23(a34(a45(a34(a23(x1))))) 766.33/282.01 766.33/282.01 [0] [0] 766.33/282.01 a35(x1) = x1 + [1] >= x1 + [1] = a34(a45(a34(x1))) 766.33/282.01 766.33/282.01 [4] [1] 766.33/282.01 a36(x1) = x1 + [2] >= x1 + [2] = a34(a45(a56(a45(a34(x1))))) 766.33/282.01 766.33/282.01 [1 6] [5] 766.33/282.01 a13(a13(x1)) = [0 1]x1 + [2] >= x1 = x1 766.33/282.01 766.33/282.01 [1 3] [1] [1 2] 766.33/282.01 a13(x1) = [0 1]x1 + [1] >= [0 1]x1 = a12(a23(a12(x1))) 766.33/282.01 766.33/282.01 [1 2] 766.33/282.01 a12(a12(x1)) = [0 1]x1 >= x1 = x1 766.33/282.01 766.33/282.01 [1 8] 766.33/282.01 a14(a14(x1)) = [0 1]x1 >= x1 = x1 766.33/282.01 766.33/282.01 [1 8] [10] 766.33/282.01 a15(a15(x1)) = [0 1]x1 + [4 ] >= x1 = x1 766.33/282.01 766.33/282.01 [6] 766.33/282.01 a24(a24(x1)) = x1 + [0] >= x1 = x1 766.33/282.01 766.33/282.01 [0] 766.33/282.01 a25(a25(x1)) = x1 + [8] >= x1 = x1 766.33/282.01 766.33/282.01 [1 6] [8] 766.33/282.01 a26(a26(x1)) = [0 1]x1 + [4] >= x1 = x1 766.33/282.01 766.33/282.01 766.33/282.01 a34(a34(x1)) = x1 >= x1 = x1 766.33/282.01 766.33/282.01 [0] 766.33/282.01 a35(a35(x1)) = x1 + [2] >= x1 = x1 766.33/282.01 766.33/282.01 [8] 766.33/282.01 a36(a36(x1)) = x1 + [4] >= x1 = x1 766.33/282.01 766.33/282.01 [4] 766.33/282.01 a46(a46(x1)) = x1 + [4] >= x1 = x1 766.33/282.01 766.33/282.01 [2] [1] 766.33/282.01 a46(x1) = x1 + [2] >= x1 + [2] = a45(a56(a45(x1))) 766.33/282.01 766.33/282.01 [1 3] 766.33/282.01 a12(a23(a12(a23(a12(a23(x1)))))) = [0 1]x1 >= x1 = x1 766.33/282.01 766.33/282.01 766.33/282.01 a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1 766.33/282.01 766.33/282.01 [0] 766.33/282.01 a34(a45(a34(a45(a34(a45(x1)))))) = x1 + [3] >= x1 = x1 766.33/282.01 problem: 766.33/282.01 strict: 766.33/282.01 a23(a45(x1)) -> a45(a23(x1)) 766.33/282.01 weak: 766.33/282.01 a12(a45(x1)) -> a45(a12(x1)) 766.33/282.01 a12(a34(x1)) -> a34(a12(x1)) 766.33/282.01 a12(a56(x1)) -> a56(a12(x1)) 766.33/282.01 a34(a56(x1)) -> a56(a34(x1)) 766.33/282.01 a23(a56(x1)) -> a56(a23(x1)) 766.33/282.01 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.33/282.01 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.33/282.01 a23(a23(x1)) -> x1 766.33/282.01 a45(a45(x1)) -> x1 766.33/282.01 a56(a56(x1)) -> x1 766.33/282.01 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.33/282.01 a24(x1) -> a23(a34(a23(x1))) 766.33/282.01 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.33/282.01 a16(a16(x1)) -> x1 766.33/282.01 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.33/282.01 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.33/282.01 a35(x1) -> a34(a45(a34(x1))) 766.33/282.01 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.33/282.01 a13(a13(x1)) -> x1 766.33/282.01 a13(x1) -> a12(a23(a12(x1))) 766.33/282.01 a12(a12(x1)) -> x1 766.33/282.01 a14(a14(x1)) -> x1 766.33/282.01 a15(a15(x1)) -> x1 766.33/282.01 a24(a24(x1)) -> x1 766.33/282.01 a25(a25(x1)) -> x1 766.33/282.01 a26(a26(x1)) -> x1 766.33/282.01 a34(a34(x1)) -> x1 766.33/282.01 a35(a35(x1)) -> x1 766.33/282.01 a36(a36(x1)) -> x1 766.33/282.01 a46(a46(x1)) -> x1 766.33/282.01 a46(x1) -> a45(a56(a45(x1))) 766.33/282.01 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.33/282.01 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.33/282.01 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.33/282.01 Matrix Interpretation Processor: dim=2 766.33/282.01 766.33/282.01 max_matrix: 766.33/282.01 [1 5] 766.33/282.01 [0 1] 766.33/282.01 interpretation: 766.33/282.01 [1 1] 766.33/282.01 [a56](x0) = [0 1]x0, 766.33/282.01 766.33/282.01 [1 2] [2] 766.33/282.01 [a46](x0) = [0 1]x0 + [4], 766.33/282.01 766.33/282.01 [0] 766.33/282.01 [a45](x0) = x0 + [1], 766.33/282.01 766.33/282.01 [1 1] [1] 766.33/282.01 [a36](x0) = [0 1]x0 + [4], 766.33/282.01 766.33/282.01 [2] 766.33/282.01 [a35](x0) = x0 + [1], 766.33/282.01 766.33/282.01 766.33/282.01 [a34](x0) = x0, 766.33/282.01 766.33/282.01 [1 3] [3] 766.33/282.01 [a26](x0) = [0 1]x0 + [2], 766.33/282.01 766.33/282.01 [1 5] [4] 766.33/282.01 [a25](x0) = [0 1]x0 + [1], 766.33/282.02 766.33/282.02 [1 2] 766.33/282.02 [a24](x0) = [0 1]x0, 766.33/282.02 766.33/282.02 [1 1] 766.33/282.02 [a23](x0) = [0 1]x0, 766.33/282.02 766.33/282.02 [1 3] [3] 766.33/282.02 [a16](x0) = [0 1]x0 + [3], 766.33/282.02 766.33/282.02 [1 3] [1] 766.33/282.02 [a15](x0) = [0 1]x0 + [3], 766.33/282.02 766.33/282.02 [1 5] 766.33/282.02 [a14](x0) = [0 1]x0, 766.33/282.02 766.33/282.02 [1 1] [2] 766.33/282.02 [a13](x0) = [0 1]x0 + [0], 766.33/282.02 766.33/282.02 766.33/282.02 [a12](x0) = x0 766.33/282.02 orientation: 766.33/282.02 [1 1] [1] [1 1] [0] 766.33/282.02 a23(a45(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a45(a23(x1)) 766.33/282.02 766.33/282.02 [0] [0] 766.33/282.02 a12(a45(x1)) = x1 + [1] >= x1 + [1] = a45(a12(x1)) 766.33/282.02 766.33/282.02 766.33/282.02 a12(a34(x1)) = x1 >= x1 = a34(a12(x1)) 766.33/282.02 766.33/282.02 [1 1] [1 1] 766.33/282.02 a12(a56(x1)) = [0 1]x1 >= [0 1]x1 = a56(a12(x1)) 766.33/282.02 766.33/282.02 [1 1] [1 1] 766.33/282.02 a34(a56(x1)) = [0 1]x1 >= [0 1]x1 = a56(a34(x1)) 766.33/282.02 766.33/282.02 [1 2] [1 2] 766.33/282.02 a23(a56(x1)) = [0 1]x1 >= [0 1]x1 = a56(a23(x1)) 766.33/282.02 766.33/282.02 [1 3] [3] [1 3] [3] 766.33/282.02 a26(x1) = [0 1]x1 + [2] >= [0 1]x1 + [2] = a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.33/282.02 766.33/282.02 [1 5] [1 2] 766.33/282.02 a14(x1) = [0 1]x1 >= [0 1]x1 = a12(a23(a34(a23(a12(x1))))) 766.33/282.02 766.33/282.02 [1 2] 766.33/282.02 a23(a23(x1)) = [0 1]x1 >= x1 = x1 766.33/282.02 766.33/282.02 [0] 766.33/282.02 a45(a45(x1)) = x1 + [2] >= x1 = x1 766.33/282.02 766.33/282.02 [1 2] 766.33/282.02 a56(a56(x1)) = [0 1]x1 >= x1 = x1 766.33/282.02 766.33/282.02 [1 3] [1] [1 2] [1] 766.33/282.02 a15(x1) = [0 1]x1 + [3] >= [0 1]x1 + [1] = a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.33/282.02 766.33/282.02 [1 2] [1 2] 766.33/282.02 a24(x1) = [0 1]x1 >= [0 1]x1 = a23(a34(a23(x1))) 766.33/282.02 766.33/282.02 [1 3] [3] 766.33/282.02 a45(a56(a45(a56(a45(a56(x1)))))) = [0 1]x1 + [3] >= x1 = x1 766.33/282.02 766.33/282.02 [1 6] [15] 766.33/282.02 a16(a16(x1)) = [0 1]x1 + [6 ] >= x1 = x1 766.33/282.02 766.33/282.02 [1 3] [3] [1 3] [3] 766.33/282.02 a16(x1) = [0 1]x1 + [3] >= [0 1]x1 + [2] = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.33/282.02 766.33/282.02 [1 5] [4] [1 2] [1] 766.33/282.02 a25(x1) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a23(a34(a45(a34(a23(x1))))) 766.33/282.02 766.33/282.02 [2] [0] 766.33/282.02 a35(x1) = x1 + [1] >= x1 + [1] = a34(a45(a34(x1))) 766.33/282.02 766.33/282.02 [1 1] [1] [1 1] [1] 766.33/282.02 a36(x1) = [0 1]x1 + [4] >= [0 1]x1 + [2] = a34(a45(a56(a45(a34(x1))))) 766.33/282.02 766.33/282.02 [1 2] [4] 766.33/282.02 a13(a13(x1)) = [0 1]x1 + [0] >= x1 = x1 766.33/282.02 766.33/282.02 [1 1] [2] [1 1] 766.33/282.02 a13(x1) = [0 1]x1 + [0] >= [0 1]x1 = a12(a23(a12(x1))) 766.33/282.02 766.33/282.02 766.33/282.02 a12(a12(x1)) = x1 >= x1 = x1 766.33/282.02 766.33/282.02 [1 10] 766.33/282.02 a14(a14(x1)) = [0 1 ]x1 >= x1 = x1 766.33/282.02 766.33/282.02 [1 6] [11] 766.33/282.02 a15(a15(x1)) = [0 1]x1 + [6 ] >= x1 = x1 766.33/282.02 766.33/282.02 [1 4] 766.33/282.02 a24(a24(x1)) = [0 1]x1 >= x1 = x1 766.33/282.02 766.33/282.02 [1 10] [13] 766.33/282.02 a25(a25(x1)) = [0 1 ]x1 + [2 ] >= x1 = x1 766.33/282.02 766.33/282.02 [1 6] [12] 766.33/282.02 a26(a26(x1)) = [0 1]x1 + [4 ] >= x1 = x1 766.33/282.02 766.33/282.02 766.33/282.02 a34(a34(x1)) = x1 >= x1 = x1 766.33/282.02 766.33/282.02 [4] 766.33/282.02 a35(a35(x1)) = x1 + [2] >= x1 = x1 766.33/282.02 766.33/282.02 [1 2] [6] 766.33/282.02 a36(a36(x1)) = [0 1]x1 + [8] >= x1 = x1 766.33/282.02 766.33/282.02 [1 4] [12] 766.33/282.02 a46(a46(x1)) = [0 1]x1 + [8 ] >= x1 = x1 766.33/282.02 766.33/282.02 [1 2] [2] [1 1] [1] 766.33/282.02 a46(x1) = [0 1]x1 + [4] >= [0 1]x1 + [2] = a45(a56(a45(x1))) 766.33/282.02 766.33/282.02 [1 3] 766.33/282.02 a12(a23(a12(a23(a12(a23(x1)))))) = [0 1]x1 >= x1 = x1 766.33/282.02 766.33/282.02 [1 3] 766.33/282.02 a23(a34(a23(a34(a23(a34(x1)))))) = [0 1]x1 >= x1 = x1 766.33/282.02 766.33/282.02 [0] 766.33/282.02 a34(a45(a34(a45(a34(a45(x1)))))) = x1 + [3] >= x1 = x1 766.33/282.02 problem: 766.33/282.02 strict: 766.33/282.02 766.33/282.02 weak: 766.33/282.02 a23(a45(x1)) -> a45(a23(x1)) 766.33/282.02 a12(a45(x1)) -> a45(a12(x1)) 766.33/282.02 a12(a34(x1)) -> a34(a12(x1)) 766.33/282.02 a12(a56(x1)) -> a56(a12(x1)) 766.33/282.02 a34(a56(x1)) -> a56(a34(x1)) 766.33/282.02 a23(a56(x1)) -> a56(a23(x1)) 766.33/282.02 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 766.33/282.02 a14(x1) -> a12(a23(a34(a23(a12(x1))))) 766.33/282.02 a23(a23(x1)) -> x1 766.33/282.02 a45(a45(x1)) -> x1 766.33/282.02 a56(a56(x1)) -> x1 766.33/282.02 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 766.33/282.02 a24(x1) -> a23(a34(a23(x1))) 766.33/282.02 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 766.33/282.02 a16(a16(x1)) -> x1 766.33/282.02 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 766.33/282.02 a25(x1) -> a23(a34(a45(a34(a23(x1))))) 766.33/282.02 a35(x1) -> a34(a45(a34(x1))) 766.33/282.02 a36(x1) -> a34(a45(a56(a45(a34(x1))))) 766.33/282.02 a13(a13(x1)) -> x1 766.33/282.02 a13(x1) -> a12(a23(a12(x1))) 766.33/282.02 a12(a12(x1)) -> x1 766.33/282.02 a14(a14(x1)) -> x1 766.33/282.02 a15(a15(x1)) -> x1 766.33/282.02 a24(a24(x1)) -> x1 766.33/282.02 a25(a25(x1)) -> x1 766.33/282.02 a26(a26(x1)) -> x1 766.33/282.02 a34(a34(x1)) -> x1 766.33/282.02 a35(a35(x1)) -> x1 766.33/282.02 a36(a36(x1)) -> x1 766.33/282.02 a46(a46(x1)) -> x1 766.33/282.02 a46(x1) -> a45(a56(a45(x1))) 766.33/282.02 a12(a23(a12(a23(a12(a23(x1)))))) -> x1 766.33/282.02 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 766.33/282.02 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 766.33/282.02 Qed 766.33/282.03 EOF