│A ∧ B
│(C ∧ D) ∧ E1
├─
1 Ext│C ∧ D3
1 Ext│E
│
3 Ext││C
3 Ext││D
││
│├─
││C2
│
│││
││├─
│││B4
││
│││
││├─
│││D4
│├─
4 Cnj││B ∧ D2
├─
2 Cnj│C ∧ (B ∧ D)
derivation
4
A ∧ B, C, D, E / C
│
3
A ∧ B, C, D, E / C
│
2
A ∧ B, C ∧ D, E / C
A ∧ B, C ∧ D, E / B
A ∧ B, C ∧ D, E / D
└──────┬──────┘
A ∧ B, C ∧ D, E / B ∧ D
│
A ∧ B, C ∧ D, E / B ∧ D
└──────────┬──────────┘
1
A ∧ B, C ∧ D, E / C ∧ (B ∧ D)
│
A ∧ B, (C ∧ D) ∧ E / C ∧ (B ∧ D)
argument tree