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) _ :: Bool False :: Bool True :: Bool not :: Bool -> Bool (&&) :: Bool -> Bool -> Bool (||) :: Bool -> Bool -> Bool (==) :: Bool -> Bool -> Bool _ :: Bool False :: Bool True :: Bool not _ :: Bool _ && _ :: Bool _ || _ :: Bool _ == _ :: Bool not (_ && _) :: Bool not (_ || _) :: Bool not (_ == _) :: Bool _ && not _ :: Bool _ || not _ :: Bool _ && (_ && _) :: Bool _ && (_ || _) :: Bool _ && _ == _ :: Bool _ || _ && _ :: Bool _ || (_ || _) :: Bool _ || _ == _ :: Bool _ == (_ && _) :: Bool _ == (_ || _) :: Bool _ == (_ == _) :: Bool p :: Bool False :: Bool True :: Bool not p :: Bool p :: Bool q :: Bool False :: Bool True :: Bool not p :: Bool not q :: Bool p && q :: Bool p || q :: Bool p == q :: Bool not (p && q) :: Bool not (p || q) :: Bool not (p == q) :: Bool p && not q :: Bool q && not p :: Bool p || not q :: Bool q || not p :: Bool p :: Bool q :: Bool r :: Bool False :: Bool True :: Bool not p :: Bool not q :: Bool not r :: Bool p && q :: Bool p && r :: Bool q && r :: Bool p || q :: Bool p || r :: Bool q || r :: Bool p == q :: Bool p == r :: Bool q == r :: Bool not (p && q) :: Bool not (p && r) :: Bool not (q && r) :: Bool not (p || q) :: Bool not (p || r) :: Bool not (q || r) :: Bool not (p == q) :: Bool not (p == r) :: Bool not (q == r) :: Bool p && not q :: Bool p && not r :: Bool q && not p :: Bool q && not r :: Bool r && not p :: Bool r && not q :: Bool p || not q :: Bool p || not r :: Bool q || not p :: Bool q || not r :: Bool r || not p :: Bool r || not q :: Bool p && (q && r) :: Bool p && (q || r) :: Bool q && (p || r) :: Bool r && (p || q) :: Bool p && q == r :: Bool q && p == r :: Bool r && p == q :: Bool p || q && r :: Bool q || p && r :: Bool r || p && q :: Bool p || (q || r) :: Bool p || q == r :: Bool q || p == r :: Bool r || p == q :: Bool p == (q && r) :: Bool q == (p && r) :: Bool r == (p && q) :: Bool p == (q || r) :: Bool q == (p || r) :: Bool r == (p || q) :: Bool p == (q == r) :: Bool Number of Eq schema classes: 21 Number of Eq 1-var classes: 4 Number of Eq 2-var classes: 16 Number of Eq 3-var classes: 59