diff --git a/README.md b/README.md
index ad16cc5059d45d6c20464269f3e092e0c6337976..5a5d6f8996bc9f85a708fa745f429ab363876b43 100644
--- a/README.md
+++ b/README.md
@@ -59,11 +59,11 @@ To see the material, please visit https://mediaspace.epfl.ch , log in with your
 |      |     |            |   |   | Reading:                       | HandMC-Ch.10  |
 |      |     |            |   |   | Follow:                        | [Stainless Tutorial Videos](https://mediaspace.epfl.ch/playlist/dedicated/30542/0_t2ld6vzn/0_azxgetu9) and [materials](https://epfl-lara.github.io/asplos2022tutorial/)  |
 |      | Fri | 13.09.2024 | 13:15 | [INR219](https://plan.epfl.ch/?room==INR%20219) | [Lecture 3](https://mediaspace.epfl.ch/playlist/dedicated/30542/0_thr9uebs/0_tv48ew7w)                       | [What is a Formal Proof?](https://mediaspace.epfl.ch/playlist/dedicated/30542/0_thr9uebs/0_tv48ew7w) and [Propositional Resolution](https://mediaspace.epfl.ch/playlist/dedicated/30542/0_thr9uebs/0_lovmc46b) |
-| 2    | Thu | 19.09.2024 | 15:15 | GRA330 | [Lecture 4](https://mediaspace.epfl.ch/playlist/dedicated/30542/0_1c4580tg/0_lovmc46b) | continue [Propositional Resolution](https://mediaspace.epfl.ch/playlist/dedicated/30542/0_thr9uebs/0_lovmc46b) and  |
+| 2    | Thu | 19.09.2024 | 15:15 | GRA330 | [Lecture 4](https://mediaspace.epfl.ch/playlist/dedicated/30542/0_1c4580tg/0_lovmc46b) | continue [Propositional Resolution](https://mediaspace.epfl.ch/playlist/dedicated/30542/0_thr9uebs/0_lovmc46b) [PDF]() and  |
 |      |     |            | 17:15 | GRA330 | [Lab 1](labs/lab1/README.md) | |
 |      | Fri | 20.09.2024 | 13:15 | INR219 | [Exercises 1](exercises/Exercises1) | Propositional Logic |
 |      |     |            |   |   | Reading:                       | CalComp-Ch.1 ∨ HandAR-Ch.2 |
-| 3    | Thu | 26.09.2024 | 15:15 | GRA330 | [Lecture 5](https://mediaspace.epfl.ch/playlist/dedicated/30542/0_x3485b9h/0_hmbkv363) | SAT solving from [Propositional Resolution](https://mediaspace.epfl.ch/playlist/dedicated/30542/0_thr9uebs/0_lovmc46b). Start [Automating First-Order Logic Proofs Using Resolution ](https://mediaspace.epfl.ch/media/06-01%2C%20Automating%20First-Order%20Logic%20Proofs%20Using%20Resolution/0_hmbkv363) |
+| 3    | Thu | 26.09.2024 | 15:15 | GRA330 | [Lecture 5](https://mediaspace.epfl.ch/playlist/dedicated/30542/0_x3485b9h/0_hmbkv363) [PDF](lectures/fol.pdf) | SAT solving from [Propositional Resolution](https://mediaspace.epfl.ch/playlist/dedicated/30542/0_thr9uebs/0_lovmc46b). Start [Automating First-Order Logic Proofs Using Resolution ](https://mediaspace.epfl.ch/media/06-01%2C%20Automating%20First-Order%20Logic%20Proofs%20Using%20Resolution/0_hmbkv363) |
 |      |     |            | 17:15 | GRA330 | [Lab 2](labs/lab2/README.md) | A communication protocol in Stainless |
 |      | Fri | 27.09.2024 | 13:15 | INR219 | [Exercises 2](exercises/Exercises2) | Traces, SAT, models |
 | 4    | Thu | 03.10.2024 | 15:15 | GRA330 | | |
diff --git a/lectures/fol.pdf b/lectures/fol.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..495ff91c9420ca6d00739d0bcff84bc256f630f2
Binary files /dev/null and b/lectures/fol.pdf differ
diff --git a/lectures/lec05.pdf b/lectures/lecture-symbolic-model-checking.pdf
similarity index 100%
rename from lectures/lec05.pdf
rename to lectures/lecture-symbolic-model-checking.pdf
diff --git a/lectures/prop-resolution.pdf b/lectures/prop-resolution.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..a37b1c4fdd5ddf553c1df05d9074cb6b40593001
Binary files /dev/null and b/lectures/prop-resolution.pdf differ