+
+//test base2 ok
+!x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1))
+
+//test base3 (unification fails)
+!x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1)))
+
+//test base4 ok
+!x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1))
+
+//test base5 ok
+!x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0))
+
+//test base6 (unification fails)
+!x:R.!y:R.(Eq R x y) -> (Rgt (Rplus y R1) (Rminus x R1))
+
+//test base7 (should fail) ok
+!x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1))
+
+