Merge of the V7_3_new_exportation branch.

[helm.git] / helm / gTopLevel / esempi / fourier / fourier_benchmarks.cic

diff --git a/helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic b/helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic
new file mode 100644 (file)
index 0000000..68166c1
--- /dev/null
+++ b/helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic
@@ -0,0 +1,170 @@
+!x:R.!y:R.!z:R.!t:R.
+(Rle (Rplus (Rmult  R0 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) z) (Rplus (Rmult  R1 t) (Ropp R1))))) R0)
+->
+(Rle (Rplus (Rmult  R1 x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) y) (Rplus (Rmult  R0 z) (Rplus (Rmult (Rplus R1  R1) t) (Ropp R1))))) R0)
+->
+(Rle (Rplus (Rmult  R0 x) (Rplus (Rmult (Rplus R1  R1) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) t) (Ropp R1))))) R0)
+->
+(Rle (Rplus (Rmult  R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) t) (Ropp R1))))) R0)
+->
+(Rle (Rplus (Rmult  R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) t) (Ropp R1))))) R0)
+
+[1'02'' 363K m=5 n=4 K=8]
+
+------------------------------------------------------------------------------------------------------------
+!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.
+(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) y) (Rplus (Rmult (Rplus R1  R1) z) (Rplus (Rmult (Rplus R1  R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) v) (Ropp R1))))))) R0)
+->
+(Rle (Rplus (Rmult  R1 x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1  R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) t) (Rplus (Rmult  R1 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) v) (Ropp R1))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) x) (Rplus (Rmult  R0 y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) t) (Rplus (Rmult (Rplus R1  R1) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) v) (Ropp R1))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) t) (Rplus (Rmult  R0 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) v) (Ropp R1))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) x) (Rplus (Rmult  R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) t) (Rplus (Rmult (Ropp (Rplus R1  R1)) u) (Rplus (Rmult  R1 v) (Ropp R1))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1  R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1  R1)))) v) (Ropp R1))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1  R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1  R1)))) v) (Ropp R1))))))) R0)
+
+[1'25'' 501K m=7 n=6 K=8]
+
+-----------------------------------------------------------------------------------------------------------
+!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.!w:R.!g:R.!h:R.!j:R.
+(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) x) (Rplus (Rmult  R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) z) (Rplus (Rmult  R1 t) (Rplus (Rmult (Rplus R1  R1) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) v) (Rplus (Rmult  R0 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) g) (Rplus (Rmult  R0 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1  R1) x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1  R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) t) (Rplus (Rmult  R0 u) (Rplus (Rmult  R0 v) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) h) (Rplus (Rmult (Rplus R1  R1) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult  R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) w) (Rplus (Rmult  R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) t) (Rplus (Rmult  R0 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) x) (Rplus (Rmult  R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) t) (Rplus (Rmult  R0 u) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) v) (Rplus (Rmult  R1 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) g) (Rplus (Rmult  R0 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult  R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) t) (Rplus (Rmult  R0 u) (Rplus (Rmult (Ropp  R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) w) (Rplus (Rmult  R0 g) (Rplus (Rmult  R1 h) (Rplus (Rmult  R1 j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) t) (Rplus (Rmult (Rplus R1  R1) u) (Rplus (Rmult (Rplus R1  R1) v) (Rplus (Rmult (Ropp (Rplus R1  R1)) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) u) (Rplus (Rmult  R0 v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) w) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1  R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) z) (Rplus (Rmult  R1 t) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) u) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) w) (Rplus (Rmult (Rplus R1  R1) g) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) h) (Rplus (Rmult  R1 j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult  R0 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) y) (Rplus (Rmult  R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) v) (Rplus (Rmult  R1 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) g) (Rplus (Rmult (Rplus R1  R1) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1  R1))) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult  R0 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) y) (Rplus (Rmult  R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) v) (Rplus (Rmult  R1 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) g) (Rplus (Rmult (Rplus R1  R1) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1  R1))) j) (Ropp R1))))))))))) R0)
+
+[1'50'' 787K m=11 n=10 K=8]
+
+-------------------------------------------------------------------------------------------------------
+
+!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.!w:R.!g:R.!h:R.!j:R.!l:R.!m:R.!n:R.!o:R.!p:R.!q:R.!r:R.!s:R.!a:R.!b:R.
+(Rle (Rplus (Rmult (Ropp (Rplus R1  R1)) x) (Rplus (Rmult  R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) z) (Rplus (Rmult  R0 t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) g) (Rplus (Rmult  R1 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) j) (Rplus (Rmult  R1 l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) n) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) o) (Rplus (Rmult  R1 p) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) q) (Rplus (Rmult (Rplus R1  R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) y) (Rplus (Rmult (Rplus R1  R1) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) u) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) w) (Rplus (Rmult (Rplus R1  R1) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) h) (Rplus (Rmult (Rplus R1  R1) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) o) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) a) (Rplus (Rmult  R0 b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult  R1 x) (Rplus (Rmult  R1 y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) t) (Rplus (Rmult  R1 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) v) (Rplus (Rmult  R0 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) g) (Rplus (Rmult  R0 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) j) (Rplus (Rmult (Rplus R1  R1) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) m) (Rplus (Rmult  R1 n) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) o) (Rplus (Rmult  R1 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) r) (Rplus (Rmult  R0 s) (Rplus (Rmult (Rplus R1  R1) a) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) x) (Rplus (Rmult  R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) t) (Rplus (Rmult (Rplus R1  R1) u) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) w) (Rplus (Rmult  R0 g) (Rplus (Rmult (Rplus R1  R1) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) j) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) l) (Rplus (Rmult (Rplus R1  R1) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) o) (Rplus (Rmult  R0 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) q) (Rplus (Rmult  R1 r) (Rplus (Rmult  R1 s) (Rplus (Rmult  R0 a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) t) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) v) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) j) (Rplus (Rmult  R1 l) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) p) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) q) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) r) (Rplus (Rmult  R0 s) (Rplus (Rmult (Rplus R1  R1) a) (Rplus (Rmult (Rplus R1  R1) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult  R1 x) (Rplus (Rmult (Rplus R1  R1) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) u) (Rplus (Rmult (Ropp  R1) v) (Rplus (Rmult (Rplus R1  R1) w) (Rplus (Rmult  R1 g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) h) (Rplus (Rmult  R1 j) (Rplus (Rmult (Rplus R1  R1) l) (Rplus (Rmult  R0 m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) o) (Rplus (Rmult (Rplus R1  R1) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) r) (Rplus (Rmult (Rplus R1  R1) s) (Rplus (Rmult (Rplus R1  R1) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) z) (Rplus (Rmult  R1 t) (Rplus (Rmult  R1 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) v) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) w) (Rplus (Rmult  R1 g) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) h) (Rplus (Rmult  R1 j) (Rplus (Rmult  R1 l) (Rplus (Rmult (Rplus R1  R1) m) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) o) (Rplus (Rmult  R1 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) q) (Rplus (Rmult  R0 r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) s) (Rplus (Rmult  R0 a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) t) (Rplus (Rmult (Rplus R1  R1) u) (Rplus (Rmult (Rplus R1  R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) w) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1  R1)))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) j) (Rplus (Rmult  R0 l) (Rplus (Rmult  R1 m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) o) (Rplus (Rmult (Rplus R1  R1) p) (Rplus (Rmult (Rplus R1  R1) q) (Rplus (Rmult  R0 r) (Rplus (Rmult  R1 s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) a) (Rplus (Rmult  R1 b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1  R1) x) (Rplus (Rmult (Rplus R1  R1) y) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) g) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1  R1)))) h) (Rplus (Rmult  R1 j) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) l) (Rplus (Rmult  R1 m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) o) (Rplus (Rmult  R0 p) (Rplus (Rmult  R0 q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) r) (Rplus (Rmult  R0 s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) y) (Rplus (Rmult (Rplus R1  R1) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) u) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) w) (Rplus (Rmult (Rplus R1  R1) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) l) (Rplus (Rmult  R1 m) (Rplus (Rmult  R0 n) (Rplus (Rmult (Rplus R1  R1) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) p) (Rplus (Rmult (Rplus R1  R1) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) s) (Rplus (Rmult  R0 a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) x) (Rplus (Rmult  R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) z) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) u) (Rplus (Rmult  R0 v) (Rplus (Rmult  R1 w) (Rplus (Rmult  R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) j) (Rplus (Rmult  R0 l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult  R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) t) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) v) (Rplus (Rmult (Rplus R1  R1) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) h) (Rplus (Rmult  R0 j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) l) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) o) (Rplus (Rmult  R0 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) r) (Rplus (Rmult (Rplus R1  R1) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) z) (Rplus (Rmult (Rplus R1  R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) u) (Rplus (Rmult (Rplus R1  R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) m) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) o) (Rplus (Rmult  R0 p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) a) (Rplus (Rmult  R1 b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) z) (Rplus (Rmult (Rplus R1  R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) w) (Rplus (Rmult  R0 g) (Rplus (Rmult  R1 h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) l) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) n) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1  R1)))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) q) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) a) (Rplus (Rmult  R1 b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult  R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) z) (Rplus (Rmult (Rplus R1  R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) l) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) o) (Rplus (Rmult (Ropp  R1) p) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) q) (Rplus (Rmult (Rplus R1  R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) s) (Rplus (Rmult  R1 a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) u) (Rplus (Rmult  R0 v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) g) (Rplus (Rmult (Rplus R1  R1) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) m) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) n) (Rplus (Rmult  R0 o) (Rplus (Rmult (Rplus R1  R1) p) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1  R1)))) q) (Rplus (Rmult  R1 r) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) x) (Rplus (Rmult  R1 y) (Rplus (Rmult (Rplus R1  R1) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) t) (Rplus (Rmult  R0 u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) w) (Rplus (Rmult  R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) j) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) m) (Rplus (Rmult  R0 n) (Rplus (Rmult (Rplus R1  R1) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) p) (Rplus (Rmult  R0 q) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult  R1 x) (Rplus (Rmult  R0 y) (Rplus (Rmult (Rplus R1  R1) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) u) (Rplus (Rmult  R1 v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) j) (Rplus (Rmult  R1 l) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) m) (Rplus (Rmult  R0 n) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) p) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) q) (Rplus (Rmult  R0 r) (Rplus (Rmult (Ropp  R1) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) a) (Rplus (Rmult  R1 b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) x) (Rplus (Rmult  R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) z) (Rplus (Rmult (Rplus R1  R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) u) (Rplus (Rmult (Rplus R1  R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) w) (Rplus (Rmult  R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) j) (Rplus (Rmult (Rplus R1  R1) l) (Rplus (Rmult (Rplus R1  R1) m) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) p) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) q) (Rplus (Rmult (Rplus R1  R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) s) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) a) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1  R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) z) (Rplus (Rmult (Rplus R1  R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) u) (Rplus (Rmult  R0 v) (Rplus (Rmult  R0 w) (Rplus (Rmult  R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) h) (Rplus (Rmult (Rplus R1  R1) j) (Rplus (Rmult  R0 l) (Rplus (Rmult  R1 m) (Rplus (Rmult  R0 n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) p) (Rplus (Rmult  R0 q) (Rplus (Rmult (Rplus R1  R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) a) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) b) (Ropp R1))))))))))))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1  R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) z) (Rplus (Rmult (Rplus R1  R1) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) u) (Rplus (Rmult  R0 v) (Rplus (Rmult  R0 w) (Rplus (Rmult  R0 g) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) h) (Rplus (Rmult (Rplus R1  R1) j) (Rplus (Rmult  R0 l) (Rplus (Rmult  R1 m) (Rplus (Rmult  R0 n) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) o) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) p) (Rplus (Rmult  R0 q) (Rplus (Rmult (Rplus R1  R1) r) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) s) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) a) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) b) (Ropp R1))))))))))))))))))))) R0)
+
+
+[19'30'' 1.9M m=21 n=20 K=8 ty=13'35'']
+
+--------------------------------------------------------------------------------------------------------
+
+!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.!w:R.!g:R.!h:R.!j:R.
+(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) v) (Rplus (Rmult  R0 w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult  R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))) h) (Rplus (Rmult (Rplus R1  R1) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) g) (Rplus (Rmult  R0 h) (Rplus (Rmult  R1 j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) y) (Rplus (Rmult  R0 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))))))) t) (Rplus (Rmult (Ropp (Rplus R1  R1)) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))) y) (Rplus (Rmult  R0 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))) h) (Rplus (Rmult  R0 j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult  R1 x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))) v) (Rplus (Rmult (Ropp  R1) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) w) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) u) (Rplus (Rmult (Rplus R1  R1) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))) w) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) g) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))))) h) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) y) (Rplus (Rmult  R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))))) j) (Ropp R1))))))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) y) (Rplus (Rmult  R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))))) v) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) w) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) g) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) h) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))))) j) (Ropp R1))))))))))) R0)
+
+[ K m=11 n=10 K=18 ty=] (TRASH)
+
+
+----------------------------------------------
+
+!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.
+(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) t) (Rplus (Rmult (Rplus R1  R1) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) v) (Ropp R1))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) x) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) y) (Rplus (Rmult  R0 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1  R1))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))) u) (Rplus (Rmult  R0 v) (Ropp R1))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1  R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) v) (Ropp R1))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))) x) (Rplus (Rmult  R0 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) v) (Ropp R1))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1  R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) t) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))) u) (Rplus (Rmult (Rplus R1 (Rplus R1  R1)) v) (Ropp R1))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))) x) (Rplus (Rmult  R1 y) (Rplus (Rmult  R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) v) (Ropp R1))))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))) x) (Rplus (Rmult  R1 y) (Rplus (Rmult  R1 z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))) t) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) u) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))) v) (Ropp R1))))))) R0)
+
+[4'  658K m=7 n=6 K=13 ty=50'']
+
+----------------------------------------------------------------
+
+!x:R.!y:R.!z:R.!t:R.
+(Rle (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))))) t) (Ropp R1))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))) x) (Rplus (Rmult (Ropp (Rplus R1  R1)) y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))) z) (Rplus (Rmult (Rplus R1  R1) t) (Ropp R1))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1  R1) x) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))) y) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))))) z) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))))))))) t) (Ropp R1))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1  R1) x) (Rplus (Rmult  R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))) t) (Ropp R1))))) R0)
+->
+(Rle (Rplus (Rmult (Rplus R1  R1) x) (Rplus (Rmult  R1 y) (Rplus (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1)))) z) (Rplus (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1  R1))))))))))) t) (Ropp R1))))) R0)
+
+[3':20''  658K m=5 n=4 K=13 ty=41'']
+
+
+
+