---

Modelling Puzzles in First Order Logic

Chapter 1. Getting started with Prover9 and Mace4 (run.sh)

• prover9 -f cogito.in > cogito.out
• prover9 -f cogito.in | prooftrans xml renumber | gvizify | dot -Tpdf > cogito.pdf
• prover9 -f cogitoFOL.in > cogitoFOL.out
• mace4 -f or.in > or.out
• mace4 -f or.in | interpformat standard > or_interp.out
• mace4 -f xor.in > xor.out
• mace4 -f two.in | interpformat standard > two.out

 
Chapter 2. Micro arithmetic puzzles (run.sh)

1. Logic equation 4x4: 
    mace4 -f logicequation4x41.in | interpformat standard > logicequation4x41.out

2. Logic equation 4x4
    mace4 -f logicequation4x42.in | interpformat standard > logicequation4x42.out

3. Logic equation 5x5
    mace4 -f logicequation5x51.in | interpformat standard > logicequation5x51.out

4. Logic equation 9x9
    mace4 -f logicequation9x9.in | interpformat standard > logicequation9x9.out

5. Three squares
    mace4 -f square.in | interpformat standard > square.out

6. Pocket money
    mace4 -f pocketmoney.in | interpformat standard > poketmoney.out

7. Dividing the legacy
    mace4 -f dividinglegacy.in | interpformat standard > dividinglegacy.out

8. Boys and girls
    mace4 -f boysgirls.in | interpformat standard > boysgirls.out

9. Robinson’s age
    mace4 -f robinsonage.in | interpformat standard > robinson.out

10. Five cards
    mace4 -f fivecards.in | interpformat standard > fivecards.out

11. A square family
    mace4 -f squarefamily.in | interpformat standard > squarefamily.out

12. Family ages
    mace4 -f familyages.in | interpformat standard > familyages.out

 
Chapter 3. Strange numbers (run.sh)
 
0. Intro
    mace4 -f romeojulieta.in | interpformat standard > romeojulieta.out

1. Adding their cubes
    mace4 -f addingcubes.in | interpformat standard > adddingcubes.out

2. Multiplication
    mace4 -f multiplication.in | interpformat standard > multiplication.out

3. The arithmetical cabby
    mace4 -f arithmeticalcabby.in | interpformat standard > arithmeticalcabby.out

4. The ten barrels
    mace4 -f tenbarrels.in | interpformat standard > tenbarrels.out

5. Find the triangle area
    mace4 -f trianglearea.in | interpformat standard > trianglearea.out

6. A digital difficulty
    mace4 -f digitaldifficulty.in | interpformat standard > digitaldifficulty.out

7. The archery match
    mace4 -f archerymatch.in | interpformat standard > archerymatch.out

8. Target practice
    mace4 -f targetpractice.in | interpformat standard > targetpractice.out

9. The nine barrels
    mace4 -f ninebarrels.in | interpformat standard > ninebarrels.out

10. Upside-down year
      mace4 -f upsideyearb.in | interpformat standard > upsideyearb.out

11. A twisted number
      mace4 -f rotate.in | interpformat standard > rotate.out

12. Unusual number
    mace4 -f unusualnumber.in | interpformat standard > unusualnumber.out

 
Chapter 4. Practical puzzles (run.sh)

1. Secret letter to the parents
    mace4 -f sendmostmoney.in | interpformat standard > sendmostmoney.out

2. Ambiguous dates
   mace4 -f ambigousdates.in | interpformat standard > ambigousdates.out

3. One landlord and 100 servants
    mace4 -f lordlandmoney.in | interpformat standard > lordlandmoney.out

4. Consecutive numbers
    mace4 -f consecutivenumbers.in | interpformat standard > consecutivenumbers.out

5. Colouring Dracula’s land in red
    mace4 -m 100 -f romania.in | interpformat standard > romania.out

6. Golomb ruler
    mace4  -f golomb_4_6.in | interpformat standard > golomb_4_6.out

7. Two cube calendar
    mace4  -f calendar.in | interpformat standard > calendar.out

8. How many routes?
    mace4  -f howmanyroutes.in | interpformat standard > howmanyroutes.out
    prover9 -f routes_prover9.in > routes_prover9.out

9. Going to church
    mace4 -f goingtochurch.in | interpformat standard > goingtochurch.out
    prover9 -f goingtochurchp.in > goingtochurchp.out

10. Buying wine
      prover9 -f waterjugs.in > waterjugs.out
      prover9 -f waterjugs.in  | prooftrans xml renumber | gvizify | dot -Tpdf > waterjugs.pdf

11. Railway routes
      mace4 -f railwayroutes.in | interpformat standard > railwayroutes.out

12. The stolen balsam
      prover9 -f stolenbalsam.in > stolenbalsam.out
      prover9 -f stolenbalsam.in  | prooftrans xml renumber | gvizify | dot -Tpdf > stolenbalsam.pdf

 
Chapter 5. Ladies and tigers (run.sh)

1. Ladies and tigers
    mace4 -f day1.in | interpformat standard > day1.out
    prover9 -f day1p.in > day1p.out

2. Ladies and tigers reloaded
    mace4 -f day2.in | interpformat standard > day2.out
    prover9 -f day2p.in > day2p.out

3. Ladies only
    mace4 -f day3.in | interpformat standard > day3.out
    prover9 -f day3p.in > day3p.out

4. Ladies are honest but tigers are liars
    mace4 -f day4.in | interpformat standard > day4.out
    prover9 -f day4p.in > day4p.out

5. Ladies are honest in some rooms only
    mace4 -f day5.in | interpformat standard > day5.out
    prover9 -f day5p.in > day5p.out

6. The lady is on the other room
    mace4 -f day6.in | interpformat standard > day6.out
    prover9 -f day6p.in > day6p.out

7. Better choosing the other room
    mace4 -f day7.in | interpformat standard > day7.out
    prover9 -f day7p.in > day7p.out

8. Mixed messages on doors
    mace4 -f day8.in | interpformat standard > day8.out
    prover9 -f day8p.in > day8p.out

9. A lady and two tigers
    mace4 -f day9.in | interpformat standard > day9.out
    prover9 -f day9p.in > day9p.out

10. A lady and two tigers
     mace4 -f day10.in | interpformat standard > day10.out
     prover9 -f day10p.in > day10p.out

11. A lady, two tigers, and other messages
      mace4 -f day11.in > day11.out
      prover9 -f day11p.in > day11p.out
      prover9 -f day11p.in  | prooftrans xml renumber | gvizify | dot -Tpdf > day11p.pdf

12. A logic labyrinth
      mace4 -f day12.in | interpformat standard > day12.out
      prover9 -f day12p.in > day12p.out

 
Chapter 6. Einstein puzzles (run.sh)

1. The magisterial bench
    mace4 -f magisterialbench.in | interpformat standard > magisterialbench.out

2. Five ships in a port
    mace4 -f ships.in | interpformat standard > ships.out

3. Ladies in the committee
    mace4 -f ladiescommittee3.in | interpformat standard > ladiescommittee3.out

4. Cocktail party
    mace4 -f cocktailparty.in | interpformat standard > cocktailparty.out

5. Borrowed books
    mace4 -f borrowedbooks.in | interpformat standard > borrowedbooks.out

6. Baseball coach dilemma
    mace4 -f baseballdilemma.in | interpformat standard > baseballdilemma.out

7. Perfect man
    mace4 -f perfectman3.in | interpformat standard > perfectman3.out

8. Four bikers
    mace4 -f bikers4.in | interpformat standard > bikers4.out

9. Movies night
    mace4 -f moviesnight2.in | interpformat standard > moviesnight2.out

10. Secret Santa
      mace4 -f secretSanta2.in | interpformat standard > secretSanta2.out

11. Seating the party
      mace4 -f partyseating.in | interpformat standard > partyseating.out

12. Passengers in a railroad compartment
      mace4 -f p265_passengers.in | interpformat standard > p265_passengers.out

 
Chapter 7. Island of truth (run.sh)
 
1. We are both knaves
    mace4 -f kk0.in | interpformat standard > kk0.out
    prover9 -f kk0p.in > kk0p.out

2. At least one of us is a knave
    mace4 -f kk1.in | interpformat standard > kk1.out
    prover9 -f kk1p.in > kk1p.out

3. Either I am a knave or B is a knight
    mace4 -f kk1b.in | interpformat standard > kk1b.out
    prover9 -f kk1bp.in > kk1bp.out

4. We are both the same
    mace4 -f kk4.in | interpformat standard > kk4.out
    prover9 -f kk4p.in > kk4p.out

5. Three inhabitants and two messages .
    mace4 -f kk2.in | interpformat standard > kk2.out
   prover9 -f kk2p.in > kk2p.out

6. Three inhabitants and not enough information
    mace4 -f kk9.in | interpformat standard > kk9.out
    prover9 -f kk9p.in > kk9p.out

7. Three inhabitants and two of the same type
    mace4 -f kk10.in | interpformat standard > kk10.out
    prover9 -f kk10p.in > kk10p.out

8. Jim, Jon, and Joe
    mace4 -f kk3.in | interpformat standard > kk3.out
    prover9 -f kk3p.in > kk3p.out

9. A spy appears
   mace4 -f kk5.in | interpformat standard > kk5.out
   prover9 -f kk5p.in > kk5p.out

10. Who is the spy?
    mace4 -f kk6.in | interpformat standard > kk6.out
    prover9 -f kk6p.in > kk6p.out

11. The whole truth and nothing but the truth
      mace4 -f alltruth.in | interpformat standard > alltruth.out

12. Three goddesses
      mace4 -f threegoddesses.in | interpformat standard > threegoddesses.out
      prover9 -f threegoddessesp.in > threegoddessesp.out

 
Chapter 8. Love and marriage (run.sh)

1. Looking at unmarried people
    prover9 -f married.in > married.out

2. Married people do not lie
    mace4 -f friends1.in | interpformat standard > friends1.out

3. Minos and aminos: we are both married
    mace4 -f minosaminos.in | interpformat standard > minosaminos.out

4. Minos and aminos: we are both married or both unmarried
    mace4 -f minosaminos2.in | interpformat standard > minosaminos2.out
    prover9 -f minosaminos2p.in > minosaminos2p.out

5. Marriage in company
    mace4 -f marriedincompany.in | interpformat standard > marriedincompany.out

6. What is my relationship to Teresa?
    mace4 -f teresa.in | interpformat standard > teresa.out

7. Who is Helen's husband?
    mace4 -f helen.in | interpformat standard > helen.out

8. Arranged royal marrage
    mace4 -f arranged_married.in | interpformat standard > arranged_married.out
    prover9 -f arranged_married_p.in > arranged_married_p.out

9. Two single persons at the end of the row
    mace4 -f singlepersons1.in | interpformat standard > singlepersons1.out  
    mace4 -f singlepersons1.in singlepersons2.in | interpformat standard >     singlepersons2.out 

10. Five couples
      mace4 -f fivecouples0.in | interpformat standard > fivecouples0.out
      mace4 -f fivecouples.in | interpformat standard > fivecouples.out  

11. A family tree
      mace4 -f family_tree_3.in | interpformat standard > family_tree_3.out 
      mace4 -f family_tree_3.in family_test | interpformat standard > family_tree_3_test.out

12. Uncles and aunts
      mace4 -f uncles_aunts.in | interpformat standard > uncles_aunts.out  

 
Chapter 9. Grid puzzles (run.sh)

1. A five in the middle
    mace4 -f five.in | interpformat standard > five.out

2. Roses, shamrocks and thistles
    mace4 -f roses.in | interpformat standard > roses.out

3. Nine squares
    mace4 -f ninesquare.in | interpformat standard > ninesquare.out
 
4. Latin square
    mace4 -f latinsquare.in | interpformat standard > latin_square.out
    mace4 -f latinsquare.in | get_interps | isofilter > latin_square_isofilter.out
    mace4 -f latinsquare.in normalised_latin_square.in | interpformat standard > latinsquarenormalised.out
    mace4 -n 4 -f latinsquare.in normalised_latin_square.in | interpformat standard > latinsquarenormalised4.out
    mace4 -n 5 -f latinsquare.in normalised_latin_square.in | interpformat standard > latinsquarenormalised5.out
    mace4 -n 6 -f latinsquare.in normalised_latin_square.in | interpformat standard > latinsquarenormalised6.out
     mace4 -n 4 -f latinsquare.in normalised_latin_square.in albert.in | interpformat standard > latinsquarenormalisedalbert.out

5. Magic square
   mace4 -f magicsquare3x3.in | interpformat standard > magicsquare3x3.out 

6. Magic five-pointed star
    mace4 -f fivepointedstar1.in | interpformat standard > fivepointedstar1.out 
    mace4 -f fivepointedstar2.in | interpformat standard > fivepointedstar2.out
    mace4 -f fivepointedstar3.in | interpformat standard > fivepointedstar3.out

7. Fort Garrisons
    mace4 -f fortgarrisons.in | interpformat standard > fortgarrisons.out

8.  Three in a row
     mace4 -f 3rows.in | interpformat standard > 3rows.out
     mace4 -f 3rows2.in | interpformat standard > 3rows2.out

9. Star battle
    mace4 -f starbattle.in | interpformat standard > starbattle.out

10. Start battle reloaded
      mace4 -f starbattlereloaded.in | interpformat standard > starbattlereloaded.out

11. Fancy queens
      mace4 -f fancyqueens.in | interpformat standard > fancyqueens.out

12. Playing minesweeper
      mace4 -f minesweeper.in | interpformat standard > minesweeper.out

 
Chapter 10. Japanese puzzles (run.sh)
 

1. Killer Sudoku
    mace4 -f killersudoku.in > killersudoku.out 

2. Futoshiki
    mace4 -f futoshiki.in  > futoshiki.out 

3. Kaos Sudoku
    mace4 -f kaossudoku.in > kaossudoku.out

4. Kakurasu
    mace4 -f kakurasu.in  > kakurasu.out
    mace4 -f kakurasu2.in > kakurasu2.out
    mace4 -f kakurasu3.in > kakurasu3.out

5. Takuzo
    mace4 -f takuzu.in > takuzu.out

6. Kakuro
    mace4 -f kakuro.in > kakuro.out

7. Daily neighbours
    mace4 -f neighbours.in > neighbours.out

8. Kendoku
    mace4 -f kendoku.in  > kendoku.out

9. Magic labyrinth
    mace4 -f magic_labyrinth.in  > magic_labyrinth.out

10. Stars and arrows
      mace4 -f stars_arrows2.in  > stars_arrows2.out

11. Tents and trees
      mace4 -f tents_trees.in  > tents_trees.out

12. Sun and moon
      mace4 -m 2 -f sun_moon.in  > sun_moon.out

 
Chapter 11. Russian puzzles (run.sh)
 
1. Young communist arranging flags
    mace4 -f p019.in > p019.out

2. Keep it even
    mace4 -f p021a.in > p021a.out

3. Magic triangle
    mace4 -f p022.in > p022.out
    mace4 -f p022_prop_sum20.in > p022_prop_sum20.out

4. From 1 to 19
    mace4 -f p034prop.in > p034prop.out
    mace4 -f p034intro.in > p034intro.out
    mace4 -f p034a.in > p034a.out

5. A duel in arithmetic
    mace4 -f p048b.in > p048b.out

6. Twenty
    mace4 -f p049.in > p049.out

7. Order the numbers
    mace4 -f p051.in > p051.out

8. A mysterious box
   mace4 -f mysteriousbox.in > mysteriousbox.out
   mace4 -f mysteriousbox26.in > mysteriousbox26.out

9. The courageous garrison
    mace4 -f p101_courageousgarrison.in > p101_courageousgarrison.out

10. A grouping of integers 1 to 15
      mace4 -f p112_groupingintegers.in > p112_groupingintegers.out

11. A star
      mace4 -f p324_star.in > p324_star.out

12. The hexagon
      mace4 -f p327_hexagon.in > p327_hexagon.out
 

Chapter 12. Polyomino puzzles (run.sh)
 
1. Broken chess row
    mace4 -f chessline.in no_rotation.in > chessline.out
    mace4 -f chessline.in rotation.in > chesslinerotation.out

2. A simple polyomino
    mace4 -f one-to-three.in > one-to-three.out

3. Rotating polyomino
    mace4 -f one-to-three_rotate.in > one-to-three_rotate.out
 
4. Fixed Ten-Yen
    mace4 -f ten-yen.in > ten-yen.out
   
5. Rotating Ten-Yen
    mace4 -f ten-yen-rotate_r4.in > ten-yen-rotate_r4.out

6. A 4 × 5 pentomino
    mace4 -f 4x5.in > 4x5.out

7. The twelve pentominoes
    mace4 -f 3x20.in $P/t.in $P/u.in $P/v.in $P/w.in $P/x.in $P/y.in $P/z.in $P/f.in $P/i.in $P/l.in $P/p.in $P/n.in 3x20help.in > 3x20.out
    mace4 -f 3x20.in $P/all12.in 3x20help.in > 3x20.out

8. Importing six pentominoes
    mace4 -f 5x6.in vars_t_w_y_z_i_l.in $P/t.in $P/w.in $P/y.in $P/z.in $P/i.in $P/l.in > 5x6.out

9. Importing other six pentominoes
    mace4 -f 5x6.in vars_u_v_x_f_p_n.in $P/u.in $P/v.in $P/x.in $P/f.in $P/p.in $P/n.in  > 5x6other.out

10. Twelve pentominoes on a chessboard
      mace4 -m -1 -f 8x8.in $P/all12.in

11. Five tetrominoes on a strange shape
      mace4 -f 4x8.in 5tetros.in > 4x8.out

12. Broken chess
      mace4 -f brokenchess2.in > brokenchess2.out

 
 
Chapter 13. Self-reference and other puzzles (run.sh)
 
1. Tricky messages
    mace4 -f trickymessages.in > trickymessages.out

2. Not so tricky messages
    mace4 -f trickymessages2.in > trickymessages2.out
    prover9 -f trickymessages2p.in > trickymessages2p.out
    prover9 -f trickymessages2p.in  | prooftrans xml renumber | gvizify | dot -Tpdf > trickymessages2p.pdf

3. Six tricky messages
    mace4 -f trickymessages3.in > trickymessages3.out
    mace4 -f trickymessages3fol.in > trickymessages3fol.out

4. Which hand?
    mace4 -f p044.in > p044.out

5. An ornament for a window
    mace4 -f p326_ornament.in > p326_ornament.out

6. At the brook
    prover9 -f atthebrook.in > atthebrook.out

7. A car tour
    mace4 -f cartourfol.in > cartourfol.out

8. A diamond ring
    mace4 -m 6 -f p325_crystal.in > p325_crystal.out

9. Drinker paradox
    prover9 -f drinker1.in > drinker1.out
    prover9 -f drinker2.in > drinker2.out

10. Ten sentences
      mace4 -f 10sentences.in >10sentences.out

11. Ten relaxed sentences
      mace4 -f 10sentencesAtLeast.in > 10sentencesAtLeast.out

12. Self-counting sentences
      mace4 -f selfcountingsentence2.in > selfcountingsentence2.out