:-dynamic r/4.
:-dynamic info/4.

info(1,[p],5,[i,d,e,sc,sd]).

r(init,p(s_s,I,D,E,SC,SD),{I>=1,D=0,E=0,SC=0,SD=0},1).

r(p(s_s,I,D,E,SC,SD),p(s_s,I,D,E,SC,SD), 
  {I>=0,D>=0,SC>=0,SD>=0,E>=0, 
     D+SC+SD+E>=1},2).

r(p(s_s,I,D,E,SC,SD),p(s_s,I1,D,E1,SC,SD), 
  {I>=1,D=0,SC=0,SD=0,E=0,      
      I1=I-1,E1=E+1},3).  

r(p(s_s,I,D,E,SC,SD),p(s_s,I1,D,E1,SC1,SD1), 
  {I>=1,D=0,SC>=0,E>=0,SD>=0, SC+E+SD>=1,         
      I1=I-1,SC1=SC+SD+E+1,E1=0,SD1=0},4).  

r(p(s_s,I,D,E,SC,SD),p(s_s,I,D,E,SC,SD), 
  {D>=1,I>=0,E>=0,SC>=0,SD>=0},5).  

r(p(s_s,I,D,E,SC,SD),p(s_s,I,D1,E1,SC,SD), 
  {E>=1,I>=0,SC>=0,SD>=0,D>=0,  
    D1=D+1,E1=E-1},6).  

r(p(s_s,I,D,E,SC,SD),p(s_s,I,D1,E,SC,SD1), 
  {E>=0,I>=0,D>=0,SD=1,SC=0,    
    SD1=SD-1,D1=D+1},7).  

r(p(s_s,I,D,E,SC,SD),p(s_s,I,D1,E,SC1,SD), 
  {E>=0,I>=0,D>=0,SC=1,SD=0,    
    SC1=SC-1,D1=D+1},8).  

r(p(s_s,I,D,E,SC,SD),p(s_s,I,D,E,SC1,SD1), 
  {E>=0,I>=0,D>=0,SC+SD>=2,SC>=0,SD>=0,    
      SC1=SC+SD-1,SD1=1},9).  

r(p(s_s,I,D,E,SC,SD),p(s_s,I1,D1,E,SC,SD), 
  {I>=1,D=0,E=0,SC=0,SD=0,I1=I-1,D1=D+1},10).  

r(p(s_s,I,D,E,SC,SD),p(s_s,I1,D,E1,SC1,SD1), 
  {I>=1,D=0,SC+E+SD>=1,SC>=0,E>=0,SD>=0,         
      I1=I-1,SC1=SC+SD+E,E1=0,SD1=1},11).  

r(p(s_s,I,D,E,SC,SD),p(s_s,I1,D1,E,SC,SD), 
  {D>=1, I>=0,SC>=0,SD>=0,E>=0, 
     I1=I+1,D1=D-1},12).  

r(p(s_s,I,D,E,SC,SD),p(s_s,I1,D,E,SC1,SD), 
  {SC>=1, I>=0,D>=0,SD>=0,E>=0, 
     I1=I+1,SC1=SC-1},13).  

r(p(s_s,I,D,E,SC,SD),p(s_s,I1,D,E,SC,SD1), 
  {SD>=1, I>=0,SC>=0,D>=0,E>=0, 
    I1=I+1,SD1=SD-1},14).  

r(p(s_s,I,D,E,SC,SD),p(s_s,I1,D,E1,SC,SD), 
  {E>=1, I>=0,SC>=0,SD>=0,D>=0, 
    I1=I+1,E1=E-1},15).  

%prop(unsafe,p:s * (sc+sd>=1) * (i>=0) *  (d>=0) * (e>=1) * (sd>=0) *  (sc>=0)). 
% 0.7 1
%prop(unsafe,p:s * (sc+sd+e>=1) * (i>=0) *  (d>=1) * (e>=0) * (sd>=0) * (sc>=0)). 
% 2.2s 2
%prop(unsafe,p:s * (sc>=0) * (i>=0) *  (d>=0) * (e>=2) * (sd>=0)).
% 0.6s 1
%prop(unsafe,p:s * (sc>=0) * (i>=0) *  (d>=2) * (e>=0) * (sd>=0)).
% 81.1s 6


prop(unsafe,
(sc+sd>=1) * (i>=0) *  (d>=0) * (e>=1)   * (sd>=0) * (sc>=0) +  
(sc+sd+e>=1) * (i>=0) *  (d>=1) * (e>=0) * (sd>=0) * (sc>=0) +
(sc>=0) * (i>=0) *  (d>=0) * (e>=2) * (sd>=0) +
(sc>=0) * (i>=0) *  (d>=2) * (e>=0) * (sd>=0)
).

% 5s 2