max expr size = 5 |- on ineqs = 4 |- on conds = 4 max #-tests = 500 min #-tests = 25 (to consider p ==> q true) max #-vars = 2 (for inequational and conditional laws) _ :: Int 0 :: Int 1 :: Int (+) :: Int -> Int -> Int (*) :: Int -> Int -> Int _ :: Int 0 :: Int 1 :: Int _ + _ :: Int _ + 1 :: Int 1 + 1 :: Int _ * _ :: Int _ + (_ + _) :: Int _ + (_ + 1) :: Int _ + (1 + 1) :: Int _ + _ * _ :: Int 1 + (1 + 1) :: Int 1 + _ * _ :: Int _ * (_ + _) :: Int _ * (_ + 1) :: Int _ * (_ * _) :: Int x :: Int 0 :: Int 1 :: Int x + x :: Int x + 1 :: Int 1 + 1 :: Int x * x :: Int x + (x + x) :: Int x + (x + 1) :: Int x + (1 + 1) :: Int x + x * x :: Int 1 + (1 + 1) :: Int 1 + x * x :: Int x * (x + x) :: Int x * (x * x) :: Int x :: Int y :: Int 0 :: Int 1 :: Int x + x :: Int x + y :: Int y + y :: Int x + 1 :: Int y + 1 :: Int 1 + 1 :: Int x * x :: Int x * y :: Int y * y :: Int x + (x + x) :: Int x + (x + y) :: Int x + (y + y) :: Int y + (y + y) :: Int x + (x + 1) :: Int x + (y + 1) :: Int y + (y + 1) :: Int x + (1 + 1) :: Int y + (1 + 1) :: Int x + x * x :: Int x + x * y :: Int x + y * y :: Int y + x * x :: Int y + x * y :: Int y + y * y :: Int 1 + (1 + 1) :: Int 1 + x * x :: Int 1 + x * y :: Int 1 + y * y :: Int x * (x + x) :: Int x * (x + y) :: Int x * (y + y) :: Int y * (x + y) :: Int y * (y + y) :: Int x * (x * x) :: Int x * (x * y) :: Int x * (y * y) :: Int y * (y * y) :: Int x :: Int y :: Int z :: Int 0 :: Int 1 :: Int x + x :: Int x + y :: Int x + z :: Int y + y :: Int y + z :: Int z + z :: Int x + 1 :: Int y + 1 :: Int z + 1 :: Int 1 + 1 :: Int x * x :: Int x * y :: Int x * z :: Int y * y :: Int y * z :: Int z * z :: Int x + (x + x) :: Int x + (x + y) :: Int x + (x + z) :: Int x + (y + y) :: Int x + (y + z) :: Int x + (z + z) :: Int y + (y + y) :: Int y + (y + z) :: Int y + (z + z) :: Int z + (z + z) :: Int x + (x + 1) :: Int x + (y + 1) :: Int x + (z + 1) :: Int y + (y + 1) :: Int y + (z + 1) :: Int z + (z + 1) :: Int x + (1 + 1) :: Int y + (1 + 1) :: Int z + (1 + 1) :: Int x + x * x :: Int x + x * y :: Int x + x * z :: Int x + y * y :: Int x + y * z :: Int x + z * z :: Int y + x * x :: Int y + x * y :: Int y + x * z :: Int y + y * y :: Int y + y * z :: Int y + z * z :: Int z + x * x :: Int z + x * y :: Int z + x * z :: Int z + y * y :: Int z + y * z :: Int z + z * z :: Int 1 + (1 + 1) :: Int 1 + x * x :: Int 1 + x * y :: Int 1 + x * z :: Int 1 + y * y :: Int 1 + y * z :: Int 1 + z * z :: Int x * (x + x) :: Int x * (x + y) :: Int x * (x + z) :: Int x * (y + y) :: Int x * (y + z) :: Int x * (z + z) :: Int y * (x + y) :: Int y * (x + z) :: Int y * (y + y) :: Int y * (y + z) :: Int y * (z + z) :: Int z * (x + y) :: Int z * (x + z) :: Int z * (y + z) :: Int z * (z + z) :: Int x * (x * x) :: Int x * (x * y) :: Int x * (x * z) :: Int x * (y * y) :: Int x * (y * z) :: Int x * (z * z) :: Int y * (y * y) :: Int y * (y * z) :: Int y * (z * z) :: Int z * (z * z) :: Int Number of Eq schema classes: 16 Number of Eq 1-var classes: 15 Number of Eq 2-var classes: 41 Number of Eq 3-var classes: 90