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 = (\x. _) (b1 := (\x. _)(b1 := False, b2 := True), b2 := (\x. _)(b1 := True, b2 := False)) bnd_leo = b1 bnd_mactual = b1 bnd_mrel = (\x. _) (b1 := (\x. _)(b1 := True, b2 := True), b2 := (\x. _)(b1 := False, b2 := True)) bnd_work_hard = (\x. _) (b1 := (\x. _) (b1 := (\x. _)(b1 := True, b2 := True), b2 := (\x. _)(b1 := True, b2 := True)), b2 := (\x. _) (b1 := (\x. _)(b1 := True, b2 := True), b2 := (\x. _)(b1 := True, b2 := True))) % SZS output end FiniteModel