pub fn proofs( tree: &Tree, rules: &[Clause], goal: &Vec<Literal<IRTerm>>) -> HashMap<Vec<Literal<IRTerm>>, Proof>
