speculate-0.3.5: tests/model/minus-c.out
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 (holes: Int)
0 :: Int
1 :: Int
id :: Int -> Int
(+) :: Int -> Int -> Int
negate :: Int -> Int
(-) :: Int -> Int -> Int
_ :: Int (holes: Int)
0 :: Int
1 :: Int
negate _ :: Int (holes: Int)
negate 1 :: Int
_ + _ :: Int (holes: Int, Int)
_ + 1 :: Int (holes: Int)
1 + 1 :: Int
_ - _ :: Int (holes: Int, Int)
_ - 1 :: Int (holes: Int)
1 - _ :: Int (holes: Int)
negate (_ + _) :: Int (holes: Int, Int)
negate (_ + 1) :: Int (holes: Int)
negate (1 + 1) :: Int
_ + (_ + _) :: Int (holes: Int, Int, Int)
_ + (_ + 1) :: Int (holes: Int, Int)
_ + (1 + 1) :: Int (holes: Int)
_ + (_ - _) :: Int (holes: Int, Int, Int)
_ + (_ - 1) :: Int (holes: Int, Int)
_ + (1 - _) :: Int (holes: Int, Int)
1 + (1 + 1) :: Int
1 + (1 - _) :: Int (holes: Int)
_ - (_ + _) :: Int (holes: Int, Int, Int)
_ - (_ + 1) :: Int (holes: Int, Int)
_ - (1 + 1) :: Int (holes: Int)
1 - (_ + _) :: Int (holes: Int, Int)
x :: Int
0 :: Int
1 :: Int
negate x :: Int
negate 1 :: Int
x + x :: Int
x + 1 :: Int
1 + 1 :: Int
x - 1 :: Int
1 - x :: Int
negate (x + x) :: Int
negate (x + 1) :: Int
negate (1 + 1) :: Int
x + (x + x) :: Int
x + (x + 1) :: Int
x + (1 + 1) :: Int
x + (x - 1) :: Int
1 + (1 + 1) :: Int
1 + (1 - x) :: Int
x - (1 + 1) :: Int
1 - (x + x) :: Int
x :: Int
y :: Int
0 :: Int
1 :: Int
negate x :: Int
negate y :: Int
negate 1 :: Int
x + x :: Int
x + y :: Int
y + y :: Int
x + 1 :: Int
y + 1 :: Int
1 + 1 :: Int
x - y :: Int
y - x :: Int
x - 1 :: Int
y - 1 :: Int
1 - x :: Int
1 - y :: Int
negate (x + x) :: Int
negate (x + y) :: Int
negate (y + y) :: Int
negate (x + 1) :: Int
negate (y + 1) :: Int
negate (1 + 1) :: 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 - y) :: Int
y + (y - x) :: Int
x + (x - 1) :: Int
x + (y - 1) :: Int
y + (y - 1) :: Int
x + (1 - y) :: Int
y + (1 - x) :: Int
1 + (1 + 1) :: Int
1 + (1 - x) :: Int
1 + (1 - y) :: Int
x - (y + y) :: Int
y - (x + x) :: Int
x - (y + 1) :: Int
y - (x + 1) :: Int
x - (1 + 1) :: Int
y - (1 + 1) :: Int
1 - (x + x) :: Int
1 - (x + y) :: Int
1 - (y + y) :: Int
x :: Int
y :: Int
z :: Int
0 :: Int
1 :: Int
negate x :: Int
negate y :: Int
negate z :: Int
negate 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 - y :: Int
x - z :: Int
y - x :: Int
y - z :: Int
z - x :: Int
z - y :: Int
x - 1 :: Int
y - 1 :: Int
z - 1 :: Int
1 - x :: Int
1 - y :: Int
1 - z :: Int
negate (x + x) :: Int
negate (x + y) :: Int
negate (x + z) :: Int
negate (y + y) :: Int
negate (y + z) :: Int
negate (z + z) :: Int
negate (x + 1) :: Int
negate (y + 1) :: Int
negate (z + 1) :: Int
negate (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 + (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 - y) :: Int
x + (x - z) :: Int
x + (y - z) :: Int
x + (z - y) :: Int
y + (y - x) :: Int
y + (y - z) :: Int
y + (z - x) :: Int
z + (z - x) :: Int
z + (z - y) :: 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 - y) :: Int
x + (1 - z) :: Int
y + (1 - x) :: Int
y + (1 - z) :: Int
z + (1 - x) :: Int
z + (1 - y) :: Int
1 + (1 + 1) :: Int
1 + (1 - x) :: Int
1 + (1 - y) :: Int
1 + (1 - z) :: Int
x - (y + y) :: Int
x - (y + z) :: Int
x - (z + z) :: Int
y - (x + x) :: Int
y - (x + z) :: Int
y - (z + z) :: Int
z - (x + x) :: Int
z - (x + y) :: Int
z - (y + y) :: Int
x - (y + 1) :: Int
x - (z + 1) :: Int
y - (x + 1) :: Int
y - (z + 1) :: Int
z - (x + 1) :: Int
z - (y + 1) :: Int
x - (1 + 1) :: Int
y - (1 + 1) :: Int
z - (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
Number of Eq schema classes: 26
Number of Eq 1-var classes: 21
Number of Eq 2-var classes: 53
Number of Eq 3-var classes: 109