ostap

¬ S ∧ P

P ∧ R

¬ ¬ P

P ∧ ¬ R

¬ P ∧ ¬ S

P ∨ Q

(P ∨ Q) ∧ ¬ (P ∧ Q)

¬ S ∨ (P ∧ R)
(¬ S ∨ P) ∧ R

	graph TD;
	A("((P ∧ (Q ∧ ¬R)) ∨ ¬¬¬(R ∧ Q)) ∨ (P ∧ R)") --> B1("(P ∧ (Q ∧ ¬R)) ∨ ¬¬¬(R ∧ Q)");
	A("((P ∧ (Q ∧ ¬R)) ∨ ¬¬¬(R ∧ Q)) ∨ (P ∧ R)") --> B2("P ∧ R");
	B1 --> C1("P ∧ (Q ∧ ¬R)");
	B1 --> C2("¬¬¬(R ∧ Q)");
	C1 --> D1((P));
	C1 --> D2("(Q ∧ ¬R)");
	D2 --> E1((Q));
	D2 --> E2((¬R)); 
	E2 --> E3("R");
	C2 --> F1("¬¬(R ∧ Q)");
	F1 --> G1("¬(R ∧ Q)");
	G1 --> H1((R ∧ Q)); 
	H1 --> H2("R");
	H1 --> H3("Q");
	B2 --> I1((P)); 
	B2 --> I2((R));