diff --git a/Einstein/Houses.svg b/Einstein/Houses.svg
new file mode 100644
index 0000000000000000000000000000000000000000..057863434da804f7422f7802a74296f6f6ced892
--- /dev/null
+++ b/Einstein/Houses.svg
@@ -0,0 +1,82 @@
+<svg xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+xmlns:svg="http://www.w3.org/2000/svg"
+xmlns="http://www.w3.org/2000/svg"
+width="1024" height="512"
+version="1.1" id="svg2">
+ <g transform="translate(0,122) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="red"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-122)"
+ id = "house1"
+ />
+ </g>
+ <g transform="translate(125,122) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="green"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-122)"
+ id = "house2"
+ />
+ </g>
+ <g transform="translate(250,122) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="blue"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-122)"
+ id = "house3"
+ />
+ </g>
+ <g transform="translate(375,122) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="white"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-122)"
+ id = "house4"
+ />
+ </g>
+ <g transform="translate(500,122) scale(0.25 0.25)">
+ <path
+ style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
+ fill="orange"
+ d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
+ transform="translate(0,-122)"
+ id = "house5"
+ />
+ </g>
+
+
+ <text x="0" y="60" font-size ="12" font-family="sans-serif">
+ <tspan x="52" dy = "0.0em" id="nationality1">nationality</tspan>
+ <tspan x="175" dy = "0.0em" id="nationality2">nationality</tspan>
+ <tspan x="300" dy = "0.0em" id="nationality3">nationality</tspan>
+ <tspan x="425" dy = "0.0em" id="nationality4">nationality</tspan>
+ <tspan x="550" dy = "0.0em" id="nationality5">nationality</tspan>
+ </text>
+ <text x="0" y="230" font-size ="12" font-family="sans-serif">
+ <tspan x="52" dy = "0.0em" id="pet1">Pet</tspan>
+ <tspan x="175" dy = "0.0em" id="pet2">Pet</tspan>
+ <tspan x="300" dy = "0.0em" id="pet3">Pet</tspan>
+ <tspan x="425" dy = "0.0em" id="pet4">Pet</tspan>
+ <tspan x="550" dy = "0.0em" id="pet5">Pet</tspan>
+ </text>
+ <text x="0" y="250" font-size ="12" font-family="sans-serif">
+ <tspan x="52" dy = "0.0em" id="cigarette1">cigarette</tspan>
+ <tspan x="175" dy = "0.0em" id="cigarette2">cigarette</tspan>
+ <tspan x="300" dy = "0.0em" id="cigarette3">cigarette</tspan>
+ <tspan x="425" dy = "0.0em" id="cigarette4">cigarette</tspan>
+ <tspan x="550" dy = "0.0em" id="cigarette5">cigarette</tspan>
+ </text>
+ <text x="0" y="270" font-size ="12" font-family="sans-serif">
+ <tspan x="52" dy = "0.0em" id="drink1">drink</tspan>
+ <tspan x="175" dy = "0.0em" id="drink2">drink</tspan>
+ <tspan x="300" dy = "0.0em" id="drink3">drink</tspan>
+ <tspan x="425" dy = "0.0em" id="drink4">drink</tspan>
+ <tspan x="550" dy = "0.0em" id="drink5">drink</tspan>
+ </text>
+
+</svg>
\ No newline at end of file
diff --git a/Einstein/einstein_puzzle_als.json b/Einstein/einstein_puzzle_als.json
new file mode 100644
index 0000000000000000000000000000000000000000..40379cb7214b6d0bf8347c3e5f78232d4c594c3b
--- /dev/null
+++ b/Einstein/einstein_puzzle_als.json
@@ -0,0 +1,18 @@
+{
+ "svg": "Houses.svg",
+ "items": [
+ {
+ "for": {"from":1, "to":5},
+ "id": "house%0",
+ "attr": "fill",
+ "value" :"color_House(%0-1)"
+ },
+ {
+ "for": {"from":1, "to":5},
+ "repeat": ["pet","nationality","cigarette","drink"],
+ "id": "%1%0",
+ "attr": "text",
+ "value" :"%1_House(%0-1)"
+ }
+ ]
+}
\ No newline at end of file
diff --git a/Einstein/einsteins_puzzle.als b/Einstein/einsteins_puzzle.als
new file mode 100644
index 0000000000000000000000000000000000000000..71e081b6434e24a097bfbd60c5bdfde9fc9d9f54
--- /dev/null
+++ b/Einstein/einsteins_puzzle.als
@@ -0,0 +1,76 @@
+open util/ordering[House]
+sig House {
+ color: Color,
+ nationality: Nationality,
+ drink: Drink,
+ cigarette: Cigarette,
+ pet: Pet
+}
+abstract sig Color {}
+one sig red extends Color {}
+one sig green extends Color {}
+one sig yellow extends Color {}
+one sig blue extends Color {}
+one sig white extends Color {}
+abstract sig Nationality {}
+one sig Englishman extends Nationality {}
+one sig Swede extends Nationality {}
+one sig Dane extends Nationality {}
+one sig German extends Nationality {}
+one sig Norwegian extends Nationality {}
+abstract sig Drink {}
+one sig tea extends Drink {}
+one sig coffee extends Drink {}
+one sig milk extends Drink {}
+one sig beer extends Drink {}
+one sig water extends Drink {}
+abstract sig Cigarette {}
+one sig Pall_Mall extends Cigarette {}
+one sig Dunhills extends Cigarette {}
+one sig Blend extends Cigarette {}
+one sig Blue_Masters extends Cigarette {}
+one sig Prince extends Cigarette {}
+abstract sig Pet {}
+one sig dog extends Pet {}
+one sig bird extends Pet {}
+one sig horse extends Pet {}
+one sig cat extends Pet {}
+one sig fish extends Pet {}
+fact constraints {
+ // There are five houses, each of a different color.
+ some disj h1, h2, h3, h4, h5: House | h1.color = red and h2.color = green and h3.color = yellow and
+ h4.color = blue and h5.color = white
+ // In each house lives a man of a different nationality.
+ no disj h,h': House | h.nationality = h'.nationality
+ // 1. The Englishman lives in the red house.
+ some h: House | (h.nationality = Englishman) and (h.color = red)
+ // 2. The Swede keeps dogs.
+ some h: House | (h.nationality = Swede) and (h.pet = dog)
+ // 3. The Dane drinks tea.
+ some h: House | (h.nationality = Dane) and (h.drink = tea)
+ // 4. The green house is just to the left of the white one.
+ some disj h, h': House | (h.color = green) and (h'.color = white) and (h'.prev = h)
+ // 5. The owner of the green house drinks coffee.
+ some h: House | (h.color = green) and (h.drink = coffee)
+ // 6. The Pall Mall smoker keeps birds.
+ some h: House | (h.cigarette = Pall_Mall) and (h.pet = bird)
+ // 7. The owner of the yellow house smokes Dunhills.
+ some h: House | (h.color = yellow) and (h.cigarette = Dunhills)
+ // 8. The man in the center house drinks milk.
+ some h: House | (some h.prev.prev) and (some h.next.next) and (h.drink = milk)
+ // 9. The Norwegian lives in the first house.
+ some h: House | (h = first) and (h.nationality = Norwegian)
+ // 10. The Blend smoker has a neighbor who keeps cats.
+ some disj h,h': House | (h.cigarette = Blend) and (h'.pet = cat) and ((h.prev = h') or (h.next = h'))
+ // 11. The man who smokes Blue Masters drinks beer.
+ some h: House | (h.cigarette = Blue_Masters) and (h.drink = beer)
+ // 12. The man who keeps horses lives next to the Dunhill smoker.
+ some disj h,h': House | (h.pet = horse) and (h'.cigarette = Dunhills) and ((h.next = h') or (h.prev = h'))
+ // 13. The German smokes Prince.
+ some h: House | (h.nationality = German) and (h.cigarette = Prince)
+ // 14. The Norwegian lives next to the blue house.
+ some disjoint h,h': House | (h.nationality = Norwegian) and (h'.color= blue) and (h.next = h')
+ // 15. The Blend smoker has a neighbor who drinks water.
+ some disj h,h': House | (h.cigarette = Blend) and (h'.drink = water) and ((h.next = h') or (h.prev = h'))
+}
+run {} for 5
\ No newline at end of file