Function prove 

pub fn prove<'a, Unbound: Ord + Clone, Bound: Ord + Clone>(
    premises: &'a [[Bound; 4]],
    to_prove: &'a [[Bound; 4]],
    rules: &'a [Rule<Unbound, Bound>],
) -> Result<Vec<RuleApplication<Bound>>, CantProve>

Locate a proof of some composite claims given the provided premises and rules.

use rify::{
    prove,
    Entity::{Unbound, Bound},
    Rule, RuleApplication,
};

// (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome)
let awesome_score_axiom = Rule::create(
    vec![
        // if someone is awesome
        [Unbound("a"), Bound("is"), Bound("awesome"), Bound("default_graph")],
        // and they have some score
        [Unbound("a"), Bound("score"), Unbound("s"), Bound("default_graph")],
    ],
    vec![
        // then they must have an awesome score
        [Unbound("a"), Bound("score"), Bound("awesome"), Bound("default_graph")]
    ],
)?;

assert_eq!(
    prove::<&str, &str>(
        // list of already known facts (premises)
        &[
            ["you", "score", "unspecified", "default_graph"],
            ["you", "is", "awesome", "default_graph"]
        ],
        // the thing we want to prove
        &[["you", "score", "awesome", "default_graph"]],
        // ordered list of logical rules
        &[awesome_score_axiom]
    )?,
    &[
        // the desired statement is be proven by instatiating the `awesome_score_axiom`
        // (you is awesome) ∧ (you score unspecified) -> (you score awesome)
        RuleApplication {
            rule_index: 0,
            instantiations: vec!["you", "unspecified"]
        }
    ]
);