Nitpicking formula...
Timestamp: 16:20:12
The types bnd_mworld and bnd_product passed the monotonicity test; Nitpick
might be able to skip some scopes
Using SAT solver "Lingeling_JNI" The following solvers are configured:
"Lingeling_JNI", "CryptoMiniSat_JNI", "MiniSat_JNI", "SAT4J", "SAT4J_Light"
Skipping 5000 scopes. (Consider using "mono" or "merge_type_vars" to prevent
this.)
Batch 1 of 1000: Trying 5 scopes:
  card bnd_mworld = 1, card bnd_product = 1, and card bnd_person = 1
  card bnd_mworld = 2, card bnd_product = 2, and card bnd_person = 2
  card bnd_mworld = 3, card bnd_product = 3, and card bnd_person = 3
  card bnd_mworld = 4, card bnd_product = 4, and card bnd_person = 4
  card bnd_mworld = 5, card bnd_product = 5, and card bnd_person = 5
% SZS status Satisfiable % SZS output start FiniteModel
Nitpick found a model for card bnd_mworld = 2, card bnd_product = 2, and
card bnd_person = 2:

  Constants:
    bnd_alex = b1
    bnd_chris = b2
    bnd_gets_rich =
      (\<lambda>x. _)
      (b1 := (\<lambda>x. _)(b1 := False, b2 := True),
       b2 := (\<lambda>x. _)(b1 := True, b2 := False))
    bnd_leo = b1
    bnd_mactual = b1
    bnd_mrel =
      (\<lambda>x. _)
      (b1 := (\<lambda>x. _)(b1 := True, b2 := True),
       b2 := (\<lambda>x. _)(b1 := False, b2 := True))
    bnd_work_hard =
      (\<lambda>x. _)
      (b1 := (\<lambda>x. _)
         (b1 := (\<lambda>x. _)(b1 := True, b2 := True),
          b2 := (\<lambda>x. _)(b1 := True, b2 := True)),
       b2 := (\<lambda>x. _)
         (b1 := (\<lambda>x. _)(b1 := True, b2 := True),
          b2 := (\<lambda>x. _)(b1 := True, b2 := True)))
% SZS output end FiniteModel