max expr size  =    7
  |- on ineqs  =    6
  |- on conds  =    6
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

rules:
x * 0 == 0
x * 1 == x
0 * x == 0
1 * x == x
x + 0 == x
0 + x == x
(x * y) * z == x * (y * z)
(x * y) * z == y * (x * z)
(x + y) + z == x + (y + z)
(x + y) + z == y + (x + z)
x * (y + z) == x * y + x * z
x * (y + z) == x * z + x * y
(x + x) * y == x * y + x * y
(x + 1) * y == y + x * y
(1 + x) * y == y + x * y
(x + x * y) * z == x * z + x * (y * z)
(x + y * x) * z == x * z + x * (y * z)
(x * y + x) * z == x * z + x * (y * z)
(x + (y + 1)) * z == z + (x + y) * z
(x + (x + x)) * y == x * y + (x * y + x * y)
equations:
y * x == x * y
y + x == x + y
y * (x * z) == x * (y * z)
z * (x * y) == x * (y * z)
z * (y * x) == x * (y * z)
y + (x + z) == x + (y + z)
z + (x + y) == x + (y + z)
z + (y + x) == x + (y + z)
z * y + x == x + y * z
y * (x * (x' * z)) == x * (y * (z * x'))
z * (x * (y * x')) == x * (y * (z * x'))
z * (y * (x * x')) == x * (y * (z * x'))
z * (x' * (x * y)) == x * (y * (z * x'))
x' * (y * (z * x)) == x * (y * (z * x'))
x' * (z * (y * x)) == x * (y * (z * x'))
y + (x + (x' + z)) == x + (y + (z + x'))
z + (x + (y + x')) == x + (y + (z + x'))
z + (y + (x + x')) == x + (y + (z + x'))
z + (x' + (x + y)) == x + (y + (z + x'))
x' + (y + (z + x)) == x + (y + (z + x'))
x' + (z + (y + x)) == x + (y + (z + x'))
x' * ((z + y) * x) == x * ((y + z) * x')
y + (x + x' * z) == x + (y + z * x')
x' + (x + z * y) == x + (y * z + x')
x' + (z * y + x) == x + (y * z + x')
y * (x' * z) + x == x + y * (z * x')
z * (y * x') + x == x + y * (z * x')
z * (x' * y) + x == x + y * (z * x')
x' * z + y * x == x * y + z * x'
x' * z + (x + y) == x + (y + z * x')
x' * z + (y + x) == x + (y + z * x')
x' * (y * z) + x == x + y * (z * x')
x' * (z * y) + x == x + y * (z * x')
z * y + z * x == (x + y) * z

            x + 0 == x
            x * 1 == x
            x * 0 == 0
            x + y == y + x
            x * y == y * x
      (x + y) + z == x + (y + z)
      (x * y) * z == x * (y * z)
      x * (y + z) == x * y + x * z
(x + (x + x)) * y == x * y + (x * y + x * y)

_ :: 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
_ + (_ + (_ + _)) :: Int
_ + (_ + (_ + 1)) :: Int
_ + (_ + (1 + 1)) :: Int
_ + (_ + _ * _) :: Int
_ + (1 + (1 + 1)) :: Int
_ + (1 + _ * _) :: Int
_ + _ * (_ + _) :: Int
_ + _ * (_ * _) :: Int
1 + (1 + (1 + 1)) :: Int
1 + (1 + _ * _) :: Int
1 + _ * (_ + _) :: Int
1 + _ * (_ + 1) :: Int
1 + _ * (_ * _) :: Int
_ * (_ + (_ + _)) :: Int
_ * (_ + _ * _) :: Int
_ * (_ * (_ + _)) :: Int
_ * (_ * (_ * _)) :: Int
_ * _ + _ * _ :: Int
(_ + _) * (_ + _) :: Int
(_ + _) * (_ + 1) :: Int
(_ + 1) * (_ + 1) :: Int
(_ + 1) * (1 + 1) :: Int
(_ + 1) * (_ * _) :: Int
(_ + (_ + 1)) * _ :: Int

Number of Eq schema classes: 40