A1: ~Man(x34) v Mortal(x34)
A2: ~Mortal(x36) v Boring(x36)
A3: ~Boring(CHera)
A4: Man(x38)
S5: ~Man(x43) v Boring(x43)      Res(1,2) {x34/x36}
S6: ~Man(CHera)      Res(5,3) {x43/CHera}
S7: F      Res(6,4) {x38/CHera}