It is very much like interactive theorem proving(like LEAN[1]) yellow blocks on top are your premises teal and dark-red blocks on the bottom of the solution-b

It is very much like interactive theorem proving(like LEAN[1]) yellow blocks on top are your premises teal and dark-red blocks on the bottom of the solution-block are your goals(dark red block is your current goal, to which you apply rules) First level can be solved in the following way: 1) replace conjunction (q and r) with q, r[rule 3]. Current goal becomes q 2) replace q with (?s and q) [rule 5]. Current goal becomes (?s and q) 3) apply your premise (p and q) to solve current goal (goal becomes r) 4) apply your premise (r) to solve current goal 5) congratulation! [1] https://lean-lang.org/ https://lean-lang.org/