p(X) | ~q(X,Y) | ~s
q(X,b) | r(X)
~r(a) | t(Z)
s
~p(X) | ~s
~t(X) | ~s

Splitting
p(X) | ~q(X,Y)         {sp1}
~s                     {sp2}
q(X,b) | r(X)          {}
~r(a)                  {sp3}
t(Z)                   {sp4}
s                      {}
~p(X)                  {sp5}
~t(X)                  {sp6}

sp1 | sp2
sp3 | sp4
sp5 | sp2
sp6 | sp2
Model = [sp2,sp3]

q(X,b) | r(X)          {}
s                      {}
~s                     {sp2}
~r(a)                  {sp3}
FALSE                  {sp2}

sp1 | sp2
sp3 | sp4
sp5 | sp2
sp6 | sp2
~sp2
Model = [sp1,sp3,sp5,sp6]

1. q(X,b) | r(X)          {}
2. s                      {}
3. p(X) | ~q(X,Y)         {sp1}
4. ~r(a)                  {sp3}
5. ~p(X)                  {sp5}
6. ~t(X)                  {sp6}
7. 1+3 = p(X) | r(X)      {sp1}
8. 7+5 = r(X)             {sp1,sp5}
8+4 = FALSE               {sp1,sp3,sp5}

sp1 | sp2
sp3 | sp4
sp5 | sp2
sp6 | sp2
~sp2
~sp1 | ~sp3 | ~sp5
Model = [sp1,sp4,sp5,sp6]

q(X,b) | r(X)          {}
s                      {}
p(X) | ~q(X,Y)         {sp1}
t(Z)                   {sp4}
~p(X)                  {sp5}
~t(X)                  {sp6}
FALSE                  {sp4,sp6}

sp1 | sp2
sp3 | sp4
sp5 | sp2
sp6 | sp2
~sp2
~sp1 | ~sp3 | ~sp5
~sp4 | ~sp6
Model = [sp1,sp5,sp6 ....  e = mc^2]