1use vampire_prover::{Function, Options, Predicate, Problem};
2
3fn main() {
4 let x1 = Function::new("x", 0);
5 let x2 = Function::new("x", 0);
6
7 dbg!(x1, x2);
8 dbg!(x1 == x2);
9
10 let y1 = Function::new("y", 0);
11 let y2 = Function::new("y", 1);
12
13 dbg!(y1, y2);
14
15 let z1 = Function::new("z", 0);
16 let z2 = Predicate::new("z", 0);
17
18 dbg!(z1, z2);
19
20 let solution = Problem::new(Options::new())
21 .with_axiom(y1.with(&[]).eq(y2.with(&[y1.with(&[])])))
22 .solve();
23
24 dbg!(solution);
25}