example_list = {"b":{"SAT uf20-02":"   \/* a small SAT problem with 20 variables and 91 clauses *\/\n   (  x10=FALSE  or  x16=FALSE  or  x5=TRUE  ) &\n   (  x16=TRUE  or  x6=FALSE  or  x5=TRUE  ) &\n   (  x17=FALSE  or  x14=FALSE  or  x18=FALSE  ) &\n   (  x10=FALSE  or  x15=FALSE  or  x19=TRUE  ) &\n   (  x1=FALSE  or  x9=FALSE  or  x18=FALSE  ) &\n   (  x3=TRUE  or  x7=TRUE  or  x6=FALSE  ) &\n   (  x13=FALSE  or  x1=TRUE  or  x6=TRUE  ) &\n   (  x2=FALSE  or  x16=FALSE  or  x20=FALSE  ) &\n   (  x7=TRUE  or  x8=TRUE  or  x18=TRUE  ) &\n   (  x7=FALSE  or  x10=TRUE  or  x20=FALSE  ) &\n   (  x2=TRUE  or  x14=FALSE  or  x17=FALSE  ) &\n   (  x2=TRUE  or  x1=TRUE  or  x19=TRUE  ) &\n   (  x7=TRUE  or  x20=FALSE  or  x1=FALSE  ) &\n   (  x11=FALSE  or  x1=TRUE  or  x17=FALSE  ) &\n   (  x3=TRUE  or  x12=FALSE  or  x19=TRUE  ) &\n   (  x3=FALSE  or  x13=FALSE  or  x6=TRUE  ) &\n   (  x13=FALSE  or  x3=TRUE  or  x12=FALSE  ) &\n   (  x5=TRUE  or  x7=FALSE  or  x12=FALSE  ) &\n   (  x20=TRUE  or  x8=TRUE  or  x16=FALSE  ) &\n   (  x13=FALSE  or  x6=FALSE  or  x19=TRUE  ) &\n   (  x5=FALSE  or  x1=TRUE  or  x14=TRUE  ) &\n   (  x9=TRUE  or  x5=FALSE  or  x18=TRUE  ) &\n   (  x12=FALSE  or  x17=FALSE  or  x1=FALSE  ) &\n   (  x20=FALSE  or  x16=FALSE  or  x19=TRUE  ) &\n   (  x12=TRUE  or  x10=TRUE  or  x11=FALSE  ) &\n   (  x6=TRUE  or  x7=FALSE  or  x2=FALSE  ) &\n   (  x13=TRUE  or  x10=FALSE  or  x17=TRUE  ) &\n   (  x20=FALSE  or  x8=TRUE  or  x16=FALSE  ) &\n   (  x10=FALSE  or  x1=FALSE  or  x8=FALSE  ) &\n   (  x7=FALSE  or  x3=FALSE  or  x19=TRUE  ) &\n   (  x19=TRUE  or  x1=FALSE  or  x6=FALSE  ) &\n   (  x19=TRUE  or  x2=FALSE  or  x13=TRUE  ) &\n   (  x2=FALSE  or  x20=TRUE  or  x9=FALSE  ) &\n   (  x8=FALSE  or  x20=FALSE  or  x16=TRUE  ) &\n   (  x13=FALSE  or  x1=FALSE  or  x11=TRUE  ) &\n   (  x15=TRUE  or  x12=FALSE  or  x6=FALSE  ) &\n   (  x17=FALSE  or  x19=FALSE  or  x9=TRUE  ) &\n   (  x19=TRUE  or  x18=FALSE  or  x16=TRUE  ) &\n   (  x7=TRUE  or  x8=FALSE  or  x19=FALSE  ) &\n   (  x3=FALSE  or  x7=FALSE  or  x1=FALSE  ) &\n   (  x7=TRUE  or  x17=FALSE  or  x16=FALSE  ) &\n   (  x2=FALSE  or  x14=FALSE  or  x1=TRUE  ) &\n   (  x18=FALSE  or  x10=FALSE  or  x8=FALSE  ) &\n   (  x16=FALSE  or  x5=TRUE  or  x8=TRUE  ) &\n   (  x4=TRUE  or  x8=TRUE  or  x10=TRUE  ) &\n   (  x20=FALSE  or  x11=FALSE  or  x19=FALSE  ) &\n   (  x8=TRUE  or  x16=FALSE  or  x6=FALSE  ) &\n   (  x18=TRUE  or  x12=TRUE  or  x8=TRUE  ) &\n   (  x5=FALSE  or  x20=FALSE  or  x10=FALSE  ) &\n   (  x16=TRUE  or  x17=TRUE  or  x3=TRUE  ) &\n   (  x7=TRUE  or  x1=FALSE  or  x17=FALSE  ) &\n   (  x17=TRUE  or  x4=FALSE  or  x7=TRUE  ) &\n   (  x20=TRUE  or  x9=FALSE  or  x13=FALSE  ) &\n   (  x13=TRUE  or  x18=TRUE  or  x16=TRUE  ) &\n   (  x16=FALSE  or  x6=FALSE  or  x5=TRUE  ) &\n   (  x5=TRUE  or  x17=TRUE  or  x7=TRUE  ) &\n   (  x12=FALSE  or  x17=FALSE  or  x6=FALSE  ) &\n   (  x20=FALSE  or  x19=TRUE  or  x5=FALSE  ) &\n   (  x9=TRUE  or  x19=FALSE  or  x16=TRUE  ) &\n   (  x13=FALSE  or  x16=FALSE  or  x11=TRUE  ) &\n   (  x4=FALSE  or  x19=FALSE  or  x18=FALSE  ) &\n   (  x13=FALSE  or  x10=TRUE  or  x15=FALSE  ) &\n   (  x16=TRUE  or  x7=FALSE  or  x14=FALSE  ) &\n   (  x19=FALSE  or  x7=FALSE  or  x18=FALSE  ) &\n   (  x20=FALSE  or  x5=TRUE  or  x13=TRUE  ) &\n   (  x12=TRUE  or  x6=FALSE  or  x4=TRUE  ) &\n   (  x7=TRUE  or  x9=TRUE  or  x13=FALSE  ) &\n   (  x16=TRUE  or  x3=TRUE  or  x7=TRUE  ) &\n   (  x9=TRUE  or  x1=FALSE  or  x12=TRUE  ) &\n   (  x3=FALSE  or  x14=TRUE  or  x7=TRUE  ) &\n   (  x1=TRUE  or  x15=TRUE  or  x14=TRUE  ) &\n   (  x8=FALSE  or  x11=FALSE  or  x18=TRUE  ) &\n   (  x19=TRUE  or  x9=FALSE  or  x7=TRUE  ) &\n   (  x10=FALSE  or  x6=TRUE  or  x2=TRUE  ) &\n   (  x14=TRUE  or  x18=TRUE  or  x11=FALSE  ) &\n   (  x9=FALSE  or  x16=FALSE  or  x14=TRUE  ) &\n   (  x1=TRUE  or  x11=TRUE  or  x20=FALSE  ) &\n   (  x11=TRUE  or  x12=TRUE  or  x4=FALSE  ) &\n   (  x13=TRUE  or  x11=FALSE  or  x14=FALSE  ) &\n   (  x17=TRUE  or  x12=FALSE  or  x9=TRUE  ) &\n   (  x14=TRUE  or  x9=TRUE  or  x1=TRUE  ) &\n   (  x8=TRUE  or  x19=TRUE  or  x4=TRUE  ) &\n   (  x6=TRUE  or  x13=FALSE  or  x20=FALSE  ) &\n   (  x2=FALSE  or  x13=FALSE  or  x11=TRUE  ) &\n   (  x14=TRUE  or  x13=FALSE  or  x17=TRUE  ) &\n   (  x9=TRUE  or  x11=FALSE  or  x18=TRUE  ) &\n   (  x13=FALSE  or  x6=FALSE  or  x5=TRUE  ) &\n   (  x5=TRUE  or  x19=TRUE  or  x18=FALSE  ) &\n   (  x4=FALSE  or  x10=TRUE  or  x11=TRUE  ) &\n   (  x18=FALSE  or  x19=FALSE  or  x20=FALSE  ) &\n   (  x3=TRUE  or  x9=FALSE  or  x8=TRUE  )","NoNeighbours":" ID={\"A\",\"B\",\"C\",\"D\",\"E\",\"F\",\"G\",\"H\"} &\n next: ID <-> ID  &\n number: ID --> 1..8 &\n !(x,y).(x|->y:next => (number(x)-number(y) >1 or number(y)-number(x) > 1)) &\n next = { \"A\"|->\"B\", \"A\"|->\"C\", \"A\"|->\"D\", \"A\"|->\"E\",\n          \"B\"|->\"D\", \"B\"|->\"E\", \"B\"|->\"F\",\n          \"C\"|->\"D\", \"C\"|->\"G\",\n          \"D\"|->\"E\", \"D\"|->\"G\", \"D\"|->\"H\",\n          \"E\"|->\"F\", \"E\"|->\"G\", \"E\"|->\"H\",\n          \"F\"|->\"H\",\n          \"G\"|->\"H\" } \n\/*\nAssign the numbers 1..8 to vertices A..H in the graph below such that the values of connected vertices differ by more than one:\n\n     A----B\n    \/|\\  \/|\\\n   \/ | \\\/ | \\\n  \/  | \/\\ |  \\\n \/   |\/  \\|   \\\nC----D----E----F\n \\   |\\  \/|   \/\n  \\  | \\\/ |  \/\n   \\ | \/\\ | \/\n    \\|\/  \\|\/\n     G----H\n\nFrom : http:\/\/www.g12.csse.unimelb.edu.au\/wiki\/doku.php?id=contrib:no_neighbours:wiki\n\n*\/","TautologyPL":"((A=TRUE & B=TRUE) => C=TRUE) <=> (A=TRUE => (B=TRUE => C=TRUE))\n\n\/* Tautology from http:\/\/en.wikipedia.org\/wiki\/Tautology_(logic) *\/","SudokuNoPartialSol":" DOM = 1..9 & \n SUBSQ = { {1,2,3}, {4,5,6}, {7,8,9} } &\n Board : DOM --> (DOM --> DOM)   &\n  !y.(y:DOM => !(x1,x2).(x1:DOM & x1<x2 & x2:DOM  => (Board(x1)(y) \/= Board(x2)(y) &\n                                                      Board(y)(x1) \/= Board(y)(x2)))) &\n  !(s1,s2).(s1:SUBSQ & s2:SUBSQ =>\n             !(x1,y1,x2,y2).( (x1:s1 & x2:s1 & x1>=x2 & (x1=x2 => y1>y2) &\n                               y1:s2 & y2:s2 & (x1,y1) \/= (x2,y2))\n                              =>\n                              Board(x1)(y1) \/= Board(x2)(y2)\n                            ))\n                            \n","SubsetSum":"coins = {16,17,23,24,39,40} &  \/* number of coins in each bag *\/\n stolen : coins --> NATURAL & \/* number of bags of each type stolen *\/\n SIGMA(x).(x:coins|stolen(x)*x)=100\n \n \/*\n $ From Katta G. Murty: \"Optimization Models for Decision Making\", page 340\n$ http:\/\/ioe.engin.umich.edu\/people\/fac\/books\/murty\/opti_model\/junior-7.pdf\n$ \n$ Example 7.8.1\n $ A bank van had several bags of coins, each containing either\n$ 16, 17, 23, 24, 39, or 40 coins. While the van was parked on the\n$ street, thieves stole some bags. A total of 100 coins were lost.\n$ It is required to find how many bags were stolen.\n*\/","NQueens Card92":"\/* Find values for n which the n-Queens puzzle has 92 solutions *\/\ncard({queens| queens : 1..n >-> 1..n &\n      !(q1,q2).(q1:1..n & q2:2..n & q2>q1\n          => queens(q1)+(q2-q1) \/= queens(q2) &\n             queens(q1)+(q1-q2) \/= queens(q2))}) = 92 & n:1..50","LoopCFG":" \/* Try to find loops in flow graphs *\/\n Blocks={\"b1\",\"b2\",\"b3\",\"b4\",\"b5\",\"b6\",\"entry\",\"exit\"} &\n succs = {\"entry\" |-> \"b1\", \"b1\"|-> \"b2\", \"b2\"|-> \"b3\", \"b3\" |-> \"b3\", \"b3\"|-> \"b4\",\n         \"b4\" |-> \"b2\", \"b4\" |-> \"b5\", \"b5\" |-> \"b6\", \"b6\" |-> \"b6\", \"b6\" |-> \"exit\"}\n  \/* Figure 8.9, page 530 of DragonBook *\/\n & L <: Blocks\n & lentry : L\n & succs~[L-{lentry}] <: L\n & !l.(l:Blocks \/\\ L => lentry : closure1(L <| succs |> L)[{l}])","SimplePredicate":"3 < 19","KissPassion":"\/*\nFind a different digit (between 0 and 9) for each \u000bcapital letter in the following equation:\nK I S S * K I S S = P A S S I O N\n(Found at http:\/\/www.cse.unsw.edu.au\/~cs4418\/2010\/Lectures\/ )\n*\/\n    {K,P} <: 1..9 &\n    {I,S,A,O,N} <: 0..9 &\n\n    (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) \n     =  1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N &\n\n    card({K, I, S, P, A, O, N}) = 7","BBook Page83":"\/* Translation of example from page 83 of Abrial's B-Book *\/\n  p = {3|->5, 3|->9, 6|->3, 9|->2} &\n  w = {1, 2, 3} &\n  p[w] = {5,9} &\n  q = {2|->7, 3|->4, 5|->1, 9|->5} &\n  q <+ p = {3|->5, 3|->9, 6|->3, 9|->2, 2|->7, 5|->1} &\n  f = {8|->10, 7|->11, 2|->11, 6|->12} &\n  g = {1|->20, 7|->20, 2|->21, 1|->22} &\n  f >< g = {(7|->(11|->20)), (2|->(11|->21))} &\n  s = {1,4} &\n  t = {2,3} &\n  prj1(s,t) = {((1|->2)|->1),((1|->3)|->1),((4|->2)|->4),((4|->3)|->4)} &\n  prj2(s,t) = {((1|->2)|->2),((1|->3)|->3),((4|->2)|->2),((4|->3)|->3)} &\n  h = {1|->11, 4|->12} &\n  k = {2|->21, 7|->22} &\n  (h||k) = { (1,2) |-> (11,21), (1,7) |-> (11,22),\n             (4,2) |-> (12,21), (4,7) |-> (12,22) }\n&\n\/* and now some assertions about the above : *\/\n  p[w] = {5,9} &\n  q <+ p = {(3|->5),(3|->9),(6|->3),(9|->2),(2|->7),(5|->1)} &\n  f >< g = {(7|->(11|->20)), (2|->(11|->21))} &\n  prj1(s,t) = {((1|->2)|->1),((1|->3)|->1),((4|->2)|->4),((4|->3)|->4)} &\n  prj2(s,t) = {((1|->2)|->2),((1|->3)|->3),((4|->2)|->2),((4|->3)|->3)} &\n  (h||k) = { (1,2) |-> (11,21), (1,7) |-> (11,22),\n             (4,2) |-> (12,21), (4,7) |-> (12,22) }","SendMoreMoney":"  {S,E,N,D, M,O,R, Y} <: 0..9 &\n  S >0 & M >0 & \n  card({S,E,N,D, M,O,R, Y}) = 8 & \n  S*1000 + E*100 + N*10 + D +\n   M*1000 + O*100 + R*10 + E =\n  M*10000 + O*1000 + N*100 + E*10 + Y","choochootrain":"\/* Find all solutions to puzzle: CHOO + CHOO = TRAIN *\/\n{C,H,O,T,R,A,I,N| {C,T}<:1..9 & {H,O,R,A,I,N} <:0..9 &\n 22*O + 200*H + 2000*C = T*10000+R*1000+A*100+I*10+N &\n card({C,H,O,T,R,A,I,N})=8}","Parity":"parity = %x.(x:NATURAL|x mod 2) &\nparity[1..10] = res &\nmapresult = ( [2,3,5,7] ; parity)\n\n","TautologiesPL":" \/* A list of tautologies taken from\n   http:\/\/pythonism.wordpress.com\/2010\/09\/13\/propositional-logic-and-some-tautologies \n   in turn taken from the book \"Logic\" by Wilfried Hodges *\/\n   \n   not(P=TRUE & not(P=TRUE)) \n &\n  (P=TRUE or not(P=TRUE)) \n &\n  (P=TRUE <=> not(not(P=TRUE))) \n &\n  ((P=TRUE or Q=TRUE) <=> not(not(P=TRUE) & not(Q=TRUE))) \n &\n  ((P=TRUE or Q=TRUE) <=> (not(P=TRUE) => Q=TRUE)) \n &\n  ((P=TRUE or Q=TRUE) <=> (Q=TRUE or P=TRUE)) \n &\n  (((P=TRUE or Q=TRUE) or R=TRUE) <=> (P=TRUE or (Q=TRUE or R=TRUE))) \n &\n  ((P=TRUE or P=TRUE) <=> P=TRUE) \n &\n  (P=TRUE => (P=TRUE or Q=TRUE)) \n &\n  ((P=TRUE => R=TRUE) => ((Q=TRUE => R=TRUE) => ((P=TRUE or Q=TRUE) => R=TRUE))) \n &\n  (not(P=TRUE) => ((P=TRUE or Q=TRUE) <=> Q=TRUE)) \n &\n  ((P=TRUE & Q=TRUE) <=> not(not(P=TRUE) or not(Q=TRUE))) \n &\n  ((P=TRUE & Q=TRUE) <=> not(P=TRUE => not(Q=TRUE))) \n &\n  ((P=TRUE & Q=TRUE) <=> (Q=TRUE & P=TRUE)) \n &\n  (((P=TRUE & Q=TRUE) & R=TRUE) <=> (P=TRUE & (Q=TRUE & R=TRUE))) \n &\n  ((P=TRUE & P=TRUE) => P=TRUE) \n &\n  ((P=TRUE & Q=TRUE) => P=TRUE) \n &\n  ((P=TRUE & Q=TRUE) => Q=TRUE) \n &\n  (P=TRUE => (Q=TRUE => (P=TRUE & Q=TRUE))) \n &\n  ((P=TRUE => Q=TRUE) => ((P=TRUE => R=TRUE) => (P=TRUE => (Q=TRUE & R=TRUE)))) \n &\n  (P=TRUE => ((P=TRUE & Q=TRUE) <=> Q=TRUE)) \n &\n  ((P=TRUE & (Q=TRUE or P=TRUE)) <=> P=TRUE) \n &\n  ((P=TRUE or (Q=TRUE & P=TRUE)) <=> P=TRUE) \n &\n  ((P=TRUE & (Q=TRUE or R=TRUE)) <=> ((P=TRUE & Q=TRUE) or (P=TRUE & R=TRUE))) \n &\n  ((P=TRUE or (Q=TRUE & R=TRUE)) <=> ((P=TRUE or Q=TRUE) & (P=TRUE or R=TRUE))) \n &\n  (((P=TRUE or Q=TRUE) & not(P=TRUE)) => Q=TRUE) \n &\n  (P=TRUE <=> ((P=TRUE & Q=TRUE) or (P=TRUE & not(Q=TRUE)))) \n &\n  (P=TRUE <=> ((P=TRUE or Q=TRUE) & (P=TRUE or not(Q=TRUE)))) \n &\n  ((P=TRUE => Q=TRUE) <=> (not(P=TRUE) or Q=TRUE)) \n &\n  ((P=TRUE => Q=TRUE) <=> not(P=TRUE & not(Q=TRUE))) \n &\n  (P=TRUE => P=TRUE) \n &\n  (P=TRUE => (Q=TRUE => P=TRUE)) \n &\n  (((P=TRUE => Q=TRUE) => P=TRUE) => P=TRUE) \n &\n  ((P=TRUE => (Q=TRUE => R=TRUE)) => ((P=TRUE => Q=TRUE) => (P=TRUE => R=TRUE))) \n &\n  ((P=TRUE => Q=TRUE) => ((Q=TRUE => R=TRUE) => (P=TRUE => R=TRUE))) \n &\n  (not(P=TRUE) => (P=TRUE => Q=TRUE))\n &\n  ((not(Q=TRUE) => not(P=TRUE)) => (P=TRUE => Q=TRUE)) \n &\n  ((P=TRUE => (Q=TRUE => R=TRUE) <=> ((P=TRUE & Q=TRUE) => R=TRUE)))\n &\n  ((P=TRUE <=> Q=TRUE) <=> ((P=TRUE & Q=TRUE) or (not(P=TRUE) & not(Q=TRUE)))) \n &\n  ((P=TRUE <=> Q=TRUE) <=> (not(P=TRUE & not(Q=TRUE)) & not(not(P=TRUE) & Q=TRUE))) \n &\n  ((P=TRUE <=> Q=TRUE) <=> ((P=TRUE => Q=TRUE) & (Q=TRUE => P=TRUE))) \n &\n  (P=TRUE <=> P=TRUE) \n &\n  ((P=TRUE <=> Q=TRUE) => (P=TRUE => Q=TRUE)) \n &\n  ((P=TRUE <=> Q=TRUE) <=> (Q=TRUE <=> P=TRUE)) \n &\n  ((P=TRUE <=> Q=TRUE) => ((Q=TRUE <=> R=TRUE) => (P=TRUE <=> R=TRUE))) \n &\n  ((P=TRUE <=> Q=TRUE) <=> (not(P=TRUE) <=> not(Q=TRUE))) \n &\n  ((P=TRUE <=> Q=TRUE) <=> not(P=TRUE <=> not(Q=TRUE)))","KnightsKnavesAll":"\/* A Puzzle from Smullyan:\n Knights: always tell the truth\n Knaves: always lie\n\n 1: A says: \u201cB is a knave or C is a knave\u201d\n 2: B says \u201cA is a knight\u201d\n\n What are A & B & C?\n Note: A,B,C are equal to TRUE if they are a Knight *\/\n \n\/* this computes the set of all models: *\/ \n{A,B,C| (A=TRUE <=> (B=FALSE or C=FALSE)) &\n        (B=TRUE <=> A=TRUE) }","GraphColouring40":" \/* Colouring a graph with 40 vertexes and 200 edges *\/\n Vertexes = 1..40 & \n maxnocol : 1..6 &  \/* possible number of colours *\/\n colour: Vertexes --> 1..maxnocol &\n !(x,y).(x|->y : Edges => colour(x) \/= colour(y)) & \/* neighbours have different colour *\/\n colour(1) = 1 \/* fix the colour of vertex 1 *\/\n &\n Edges = {13|->3, 26|->14, 19|->24, 2|->13, 1|->18, 10|->20, 15|->8, 9|->8, 4|->19, 7|->3, 23|->27, 9|->7, 23|->2, 29|->17, 35|->14, 8|->1, 27|->2, 9|->36, 34|->26, 7|->26, 34|->23, 14|->20, 39|->3, 7|->31, 5|->21, 23|->11, 35|->30, 6|->11, 9|->28, 18|->30, 19|->33, 25|->28, 39|->4, 2|->19, 9|->24, 8|->26, 10|->6, 22|->25, 32|->25, 23|->40, 30|->17, 2|->4, 5|->24, 27|->36, 20|->38, 31|->38, 35|->9, 19|->5, 8|->16, 18|->15, 35|->4, 19|->21, 15|->37, 34|->24, 6|->8, 8|->36, 2|->1, 23|->13, 13|->35, 36|->25, 26|->20, 32|->36, 24|->2, 9|->17, 38|->27, 18|->38, 36|->20, 34|->32, 8|->5, 5|->1, 28|->7, 33|->8, 5|->22, 31|->9, 30|->40, 26|->33, 32|->1, 6|->19, 14|->5, 8|->18, 40|->22, 4|->5, 5|->13, 34|->40, 12|->15, 25|->14, 3|->35, 10|->23, 18|->26, 31|->15, 13|->38, 13|->18, 20|->22, 18|->9, 11|->13, 40|->25, 40|->5, 28|->20, 37|->28, 3|->26, 38|->4, 3|->12, 5|->6, 30|->26, 32|->26, 7|->17, 31|->32, 22|->37, 38|->26, 3|->23, 34|->3, 6|->35, 34|->30, 23|->4, 23|->15, 10|->17, 12|->37, 40|->37, 28|->34, 38|->5, 16|->29, 5|->25, 21|->30, 37|->39, 32|->7, 7|->13, 15|->20, 39|->13, 26|->36, 18|->12, 4|->6, 21|->39, 21|->7, 29|->36, 11|->21, 20|->11, 22|->36, 24|->23, 38|->24, 4|->10, 20|->23, 38|->36, 16|->23, 12|->30, 17|->6, 29|->10, 10|->31, 7|->37, 40|->19, 27|->18, 12|->16, 6|->7, 8|->30, 25|->27, 38|->21, 27|->31, 4|->31, 5|->9, 23|->29, 35|->8, 11|->27, 17|->21, 26|->37, 3|->6, 5|->27, 9|->6, 26|->27, 5|->12, 14|->30, 35|->29, 10|->11, 38|->8, 36|->28, 1|->14, 31|->37, 13|->34, 26|->2, 12|->7, 34|->5, 3|->19, 15|->16, 20|->39, 19|->10, 12|->23, 6|->30, 11|->2, 25|->34, 24|->10, 40|->38, 24|->13, 35|->37, 37|->2, 33|->2, 31|->22, 15|->11, 22|->29, 9|->34, 34|->8, 17|->12, 1|->29}\n","GolombRuler":" n=7 & length = 25 &\n a:1..n --> 0..length &\n !i.(i:2..n => a(i-1) < a(i)) &\n !(i1,j1,i2,j2).(( i1>0 & i2>0 & j1<=n & j2 <= n &\n                   i1<j1 & i2<j2 & (i1,j1) \/= (i2,j2) & \n                   i1<=i2 & (i1=i2 => j1<j2)\n                 ) => (a(j1)-a(i1) \/= a(j2)-a(i2)))","SimpleRailway":"\/* We define a simple toplogy of track sections : *\/\nnext = {\"L\"|->\"A\",\"A\"|->\"B\",\"B\"|->\"C\",\"B\"|->\"D\",\n        \"D\"|->\"E\", \"D\"|->\"K\", \"E\"|->\"F\", \"F\"|->\"G\"}\n& \/* now we specify which sections are occupied  by which train: *\/\noccupied = {\"A\"|->\"Train1\", \"B\"|->\"Train1\", \"F\"|->\"Train2\"}\n&\nr1 = occupied~[{\"Train1\"}] & \/* the sections occupied by a train *\/\nn1 = closure1(next)[r1] & \/* the reachable sections, in forward direction *\/\no1 = occupied[n1] \/* which trains occupy these; should be equal to {\"Train1\"}; but it is not *\/","KnightsKnaves":"\/* A Puzzle from Smullyan:\n Knights: always tell the truth\n Knaves: always lie\n\n 1: A says: \u201cB is a knave or C is a knave\u201d\n 2: B says \u201cA is a knight\u201d\n\n What are A & B & C?\n Note: A,B,C are equal to TRUE if they are a Knight *\/\n \n (A=TRUE <=> (B=FALSE or C=FALSE)) &\n (B=TRUE <=> A=TRUE)","NQueens":" n = 8 &  \n queens : 1..n >-> 1..n \/* for each column the row in which the queen is in *\/\n &\n !(q1,q2).(q1:1..n & q2:2..n & q2>q1\n    => queens(q1)+(q2-q1) \/= queens(q2) & queens(q1)+(q1-q2) \/= queens(q2))","WhoKilledAgatha":"Persons = { \"Agatha\", \"butler\", \"Charles\"} \/* it is more efficient in B to use enumerated sets; but in the eval window we cannot define them *\/\n &\n hates : Persons <-> Persons &\n richer : Persons <-> Persons &  \/* richer \/\\ richer~ = {} & *\/\n richer \/\\ id(Persons) = {} &\n !(x,y,z).(x|->y:richer & y|->z:richer => x|->z:richer) &\n !(x,y).(x:Persons & y:Persons & x\/=y => (x|->y:richer <=> y|->x \/: richer)) &\n \n killer : Persons &   victim : Persons &\n killer|->victim : hates & \/* A killer always hates his victim *\/\n killer|->victim \/: richer & \/* and is no richer than his victim *\/\n hates[{ \"Agatha\"}] \/\\ hates[{\"Charles\"}] = {} & \/* Charles hates noone that Agatha hates. *\/\n hates[{ \"Agatha\"}] = Persons - {\"butler\"} & \/* Agatha hates everybody except the butler. *\/\n !x.( x: Persons & x|-> \"Agatha\" \/: richer => \"butler\"|->x : hates) & \/* The butler hates everyone not richer than Aunt Agatha *\/\n hates[{ \"Agatha\"}] <: hates[{\"butler\"}] & \/* The butler hates everyone whom Agatha hates.  *\/\n !x.(x:Persons => hates[{x}] \/= Persons) \/* Noone hates everyone. *\/ &\n victim =  \"Agatha\"\n \n \/* & killer \/= Agatha *\/  \/* comment this out: the predicate becomes unsatisfiable *\/","Sqrt":" sqrt>0 & sqrt*sqrt <= i & (sqrt+1)*(sqrt+1)>i \n \/* specify the integer square root of i *\/\n & i = 10000000\n","GraphIsomorphism":"  n=9 &\n  graph1 = {1|->3,2|->3, 3|->6, 4|->6,5|->6, 8|->9,9|->8,  6 |-> 6, 7|->7} &\n  graph2 = {2|->5,3|->5, 4|->5, 6|->4,7|->4, 1|->9,9|->1,  5 |-> 5, 8|->8} &\n  \n  \/* now try and find an isomporphism p : *\/\n  p: 1..n >->> 1..n &\n  !i.(i:1..n => p[graph1[{i}]] = graph2[p[{i}]])","Pex NonlinearArithmetic":"\nx >= 0 & x <= 100 &\ny >= 0 & y <= 100 &\nx * y - 37 * y + 71 * x - 2627 = 0\n        \n\/*\n Source: http:\/\/pexforfun.com:80\/default.aspx?language=CSharp&sample=NonLinearArithmetic\n    \/\/ What values of x and y solve this equation? Ask Pex to find out!\n    if (x >= 0 && x <= 100 &&\n        y >= 0 && y <= 100 &&\n        x * y - 37 * y + 71 * x - 2627 == 0)        \n      Console.WriteLine(\"equation solved\"); \n*\/\n","MapImage":"\/* define an infinite function cube and\n   map it over a list using relational composition (;)\n   and compute its image over the set 1..10 *\/\n  \n cube = %x.(x:INTEGER|x*x*x) &\n ([1,2,3,4,5] ; cube) = list &\n  cube[1..10] = image &\n  \n  cube(y) = 15625  \/* and take the cubic root of a number *\/","Cheryl's Birthday":"\/* A simplified version of the SumProduct Puzzle taken from\nhttp:\/\/www.nytimes.com\/2015\/04\/15\/science\/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html?_r=0\n*\/\n \n \/* Albert and Bernard just met Cheryl. \"When\u2019s your birthday?\" Albert asked Cheryl.*\/\n Month:STRING & Day:NATURAL1 & \n\/* Cheryl thought a second and said, :I\u2019m not going to tell you, but I\u2019ll give you some clues. She wrote down a list of 10 dates: *\/\nPD = {(\"aug\"|->14),(\"aug\"|->15),(\"aug\"|->17),(\"july\"|->14),(\"july\"|->16),(\"june\"|->17),(\"june\"|->18),(\"may\"|->15),(\"may\"|->16),(\"may\"|->19)}\n&\n\/*\nThen Cheryl whispered in Albert\u2019s ear the month \u2014 and only the month \u2014 of her birthday. To Bernard, she whispered the day, and only the day. \n*\/\n Month : dom(PD) &\n Day : ran(PD) &\n Month|->Day : PD &\n\n\/* Albert: I don\u2019t know when your birthday is, *\/\ncard(PD[{Month}]) > 1 &\n\/* but I know Bernard doesn\u2019t know, either. *\/\n!x.(x:PD[{Month}] => card(PD~[{x}]) > 1) &\n\n\/* Bernard: I didn\u2019t know originally, *\/\n card(PD~[{Day}]) > 1  &\n\/* but now I do. *\/\n PD2 = {m,d| (m|->d):PD &  !x.(x:PD[{m}] => card(PD~[{x}]) > 1 ) } &\n card(PD2~[{Day}]) = 1&\n \n \/* Albert: Well, now I know, too! *\/\n  card({d|Month|->d : PD2 & card(PD2~[{d}]) = 1})=1","BBook Page82":"\/* Translation of example from page 82 of Abrial's B-Book *\/\n p = {3|->5, 3|->9, 6|->3, 9|->2} &\n q = {2|->7, 3|->4, 5|->1, 9|->5} &\n u = {1,2,3} &\n s = {4,7,3} &\n t = {4,8,1} &\n\n\/* and now some assertions about the above: *\/\n p~ = {5|->3, 9|->3, 3|->6, 2|->9} &\n dom(p) = {3,6,9} &\n ran(p) = {5,9,3,2} &\n (p;q) = {3|->1, 3|->5, 6|->4, 9|->7} &\n id(u) = {1|->1, 2|->2, 3|->3} &\n s <|p = {3|->5, 3|->9} &\n p |> t = {} &\n s <<| p = {6|->3, 9|->2} &\n p |>> t = {3|->5, 3|->9, 6|->3, 9|->2}","Sudoku":" DOM = 1..9 & \n SUBSQ = { {1,2,3}, {4,5,6}, {7,8,9} } &\n Board : DOM --> (DOM --> DOM)   &\n  !y.(y:DOM => !(x1,x2).(x1:DOM & x1<x2 & x2:DOM  => (Board(x1)(y) \/= Board(x2)(y) &\n                                                      Board(y)(x1) \/= Board(y)(x2)))) &\n  !(s1,s2).(s1:SUBSQ & s2:SUBSQ =>\n             !(x1,y1,x2,y2).( (x1:s1 & x2:s1 & x1>=x2 & (x1=x2 => y1>y2) &\n                               y1:s2 & y2:s2 & (x1,y1) \/= (x2,y2))\n                              =>\n                              Board(x1)(y1) \/= Board(x2)(y2)\n                            ))\n                            \n   & \/* PUZZLE CONSTRAINTS : *\/\n   \n   Board(1)(1)=7 & Board(1)(2)=8  & Board(1)(3)=1 & Board(1)(4)=6 & Board(1)(6)=2 \n                 & Board(1)(7)=9 & Board(1)(9) = 5 &\n   Board(2)(1)=9 & Board(2)(3)=2 & Board(2)(4)=7 & Board(2)(5)=1 &\n   Board(3)(3)=6 & Board(3)(4)=8 & Board(3)(8)=1 & Board(3)(9)=2 &\n   \n   Board(4)(1)=2 & Board(4)(4)=3 & Board(4)(7)=8 & Board(4)(8)=5 & Board(4)(9)=1 &\n   Board(5)(2)=7 & Board(5)(3)=3 & Board(5)(4)=5 & Board(5)(9)=4 &\n   Board(6)(3)=8 & Board(6)(6)=9 & Board(6)(7)=3 & Board(6)(8)=6 &\n   \n   Board(7)(1)=1 & Board(7)(2)=9 & Board(7)(6)=7 & Board(7)(8)=8 &\n   Board(8)(1)=8 & Board(8)(2)=6 & Board(8)(3)=7 & Board(8)(6)=3 & Board(8)(7)=4 & Board(8)(9)=9 &\n   Board(9)(3)=5 & Board(9)(7)=1","SimpleAddition":"2 + 18"},"tla":{"Pex_NonlinearArithmetic":"\nx >= 0 \/\\ x <= 100 \/\\\ny >= 0 \/\\ y <= 100 \/\\\nx * y - 37 * y + 71 * x - 2627 = 0\n        \n\\* Source: http:\/\/pexforfun.com:80\/default.aspx?language=CSharp&sample=NonLinearArithmetic *\\\n","Functions":"LET\r\n\tf[x \\in 1..10] == x+x\r\n\t\r\n\tg == [x \\in 1..10 |-> x * x]\r\n\t\r\n\th == [g EXCEPT ![3] = 6]\r\n\t\r\n\tdom == DOMAIN f\r\n\t\r\n\trange == {f[x] : x \\in dom}\r\nIN  \r\n\tf[2] = g[2] \/\\ f[3] = h[3] \/\\ f \\in [dom -> range]","HourClock":"\\* Calculating the next state of the hour clock *\\\r\nLET\r\n\tCurrent == hr = 12\r\n\t\r\n\tInv == hr \\in 1..12\r\n\t\r\n\tNext == hr' = IF hr # 12 THEN hr + 1 ELSE 1\r\nIN \r\n\tCurrent \/\\ Inv  \/\\ Next","PredicateLogic":"LET\r\n\tS == {1,2,3,4}\r\n\tT == 1..10\r\n\r\nIN\r\n\tS \\subseteq T  <=>  S \\ T = {}","SimpleConstraint":"CHOOSE x \\in 0..100: x^3 - 20*x^2 + 7*x = 14388\n(* Example from https:\/\/buttondown.email\/hillelwayne\/archive\/creatively-misusing-tla\/ *)","PredicateLogic3":"LET\r\n\tS == 2..8\r\n\tP(x) == x > 3\r\n\tQ(x) == x < 6\r\n\r\nIN\r\n\t(\\A x \\in S : P(x) \/\\ Q(x)) <=> (\\A x \\in S : P(x)) \/\\ (\\A x \\in S : Q(x))\r\n\t","SendMoreMoney":"{S,E,N,D, M,O,R, Y} \\subseteq 0..9 \/\\\n   S >0 \/\\ M >0 \/\\ \n   Cardinality({S,E,N,D, M,O,R, Y}) = 8 \/\\ \n   S*1000 + E*100 + N*10 + D +\n   M*1000 + O*100 + R*10 + E =\n   M*10000 + O*1000 + N*100 + E*10 + Y\n   ","Queens":"LET\r\n    N==8\r\n\tSolve == \/\\ Queens \\in [1..N -> 1..N]\r\n\t\t\t \/\\ \\A i \\in 1..N :\r\n\t\t\t\t\t\\A j \\in 2..N :i<j => \r\n\t\t\t\t\t\t\/\\ Queens[i] # Queens[j]\r\n\t\t\t\t\t\t\/\\ Queens[i]+i-j # Queens[j]\r\n\t\t\t\t\t\t\/\\ Queens[i]-i+j # Queens[j]\r\nIN\r\n\tSolve\r\n      ","PredicateLogic2":"LET \r\n\tS == 2..7\r\n\tP(x) == x % 2 = 0\r\n\r\nIN\r\n\t(S # {}) \/\\ (\\A x \\in S : P(x)) => (\\E x \\in S : P(x))","SimpleMath":"(* Examples from SimpleMath.tla (TLA+ tools distribution) *)\r\n\r\nLET \r\n(***************************************************************************)\r\n(* This example shows how you can check propositional logic tautologies.   *)\r\n(***************************************************************************)\r\nd1 ==  \\A F, G \\in {TRUE, FALSE} : (F => G) <=> ~F \\\/ G\r\n  \r\n\r\n(***************************************************************************)\r\n(* Here is an example showing how you can check that a formula is NOT a    *)\r\n(* tautology of propositional logic.                                       *)\r\n(***************************************************************************)\r\nd2 ==  ~ \\A F, G \\in {TRUE, FALSE} : (F \\\/ G) => (F \/\\ G)\r\n\r\nIN d1 \/\\ d2","Sets":"LET\r\n\td1 == {1,2,3} = {1,2,2,3,3}\r\n\td2 == {1,2} # {1}\r\n\td3 == 1 \\in {1}\r\n\td4 == 1 \\notin {2}\r\n\td5 == {1} \\cup {2} = {1,2}\r\n\td6 == {1,2,3} \\cap {2,3,4} = {2,3}\r\n\td7 == {1,2} \\subseteq {1,2,3}\r\n\td8 == {1,2} \\ {1} = {2}\r\n\td9 == {x \\in 1..10 : x % 2 = 0} = {2*x : x \\in 1..5 }\r\n\td10 == SUBSET {1,2} = {{},{1},{2},{1,2}}\r\n\td11 == UNION {{},{1},{2},{1,2}} = {1,2}\r\nIN \r\n\td1 \/\\ d2 \/\\ d3 \/\\ d4 \/\\ d5 \/\\ d6 \/\\ d7 \/\\ d8 \/\\ d9 \/\\ d10 \/\\ d11","KnightsKnaves":"\\* Knights-Knaves Puzzle from Smullyan *\\\n\\* Knights always tell the truth, Knaves always lie *\\\n\\* A,B,C are knights or knaves *\\\n\n\\* A says: B or C is a knave *\\\n (A <=> (~B \\\/ ~C)) \n \/\\\n\\* B says: A is a knight *\\\n (B <=> A)\n","KissPassionPuzzle":"(* KISS  KISS = PASSION Puzzle *)\n\n(* Find a different digit (between 0 and 9) for each capital letter in the following equation: *)\n(* K I S S * K I S S = P A S S I O N *)\n(* More complicated than the classical SEND+MORE=MONEY puzzle *)\n\n       K \\in (1 .. 9)\n\t\/\\ P \\in (1 .. 9)\n\t\/\\ {I, S, A, O, N} \\subseteq (0..9)\n\t\/\\ (1000 * K + 100 * I + 10 * S + S) * \n       (1000 * K + 100 * I + 10 * S + S) \n       = \n       1000000 * P + 100000 * A + 10000 * S + 1000 * S + 100 * I + 10 * O + N\n    \/\\ Cardinality({K, I, S, P, A, O, N}) = 7"}}