https://incredible.pm/ is better

Is there any instructions on how to use this, or what is being asked for?

The top block gives some premises and a conclusion which we're meant to prove. The smaller blocks on the bottom are inference rules which can be used in the proof. I haven't figured out what the colors mean. I think there's also some kind of cursor/state, which I don't understand -- but when you click a rule, I don't understand how you control which expression matches to which term in the rule.

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/

A big problem is it's practically unusable on mobile (at least for me) Clicking once via finger tap often results in multiple clicks being applied.