let deliverToys idS d1 d2 d3 = ()
    (* deliver toys *);;
let study idS e1 e2 e3 = ()
    (* toy R&D *);;

def santas(idS::xs) & deerReady(d1,d2,d3) =
    santas(xs) &
    (deliverToys idS d1 d2 d3; 0) &
    donedelivering(idS,d1,d2,d3)

 or donedelivering(idS,d1,d2,d3) & deer(ds) & santas(xs) & counterD(deliveries) = 
    santas(idS::xs) & deer(d1::d2::d3::ds) & counterD(deliveries+1)

 or santas(idS::xs) & elvesReady(e1,e2,e3) = 
    santas(xs) &
    (study idS e1 e2 e3; 0) &
    donestudying(idS, e1, e2, e3)

 or donestudying(idS,e1,e2,e3) & elves(es) & santas(xs) & counterS(n) = 
    santas(idS::xs) & elves(e1::e2::e3::es) & counterS(n+1)

 or elves(id1::id2::id3::xs) = 
    elves(xs) & elvesReady(id1,id2,id3)

 or deer(id1::id2::id3::xs) = 
    deer(xs) & deerReady(id1,id2,id3)
 
 or wait_finished() & counterS(1000) = 
    reply n to wait_finished;;

let elfNo = 12;;
let deerNo = 9;; 
let santaNo = 12;;

let (--) i j = 
    let rec aux n acc = if n <= i then acc else aux (n-1) (n::acc)
    in aux j [];;

spawn santas (1--santaNo) & elves (1--elfNo) & deer (1--elfNo) & counterD(0) & counterS(0) ;;
let studied = wait_finished () ;;
print_int studied;;