Minimal case proofs for: in/unf

Leaf 25:
3, true=>s(a, b), s(a, c), rule #5
17, s(a, b)=>e(a, b), rule #16
18, e(a, b)=>e(b, a), rule #9
21, s(a, c)=>e(a, c), rule #16
23, e(b, a), e(a, c)=>e(b, c), rule #10
24, e(b, c)=>goal, rule #4
------------
Leaf 31:
3, true=>s(a, b), s(a, c), rule #5
17, s(a, b)=>e(a, b), rule #16
18, e(a, b)=>e(b, a), rule #9
21, s(a, c)=>dom(sk2), r(a, sk2), s(sk2, c), rule #16
29, e(b, a), r(a, sk2)=>r(b, sk2), rule #11
30, r(b, sk2)=>false, rule #6
------------
Leaf 42:
3, true=>s(a, b), s(a, c), rule #5
17, s(a, b)=>dom(sk3), r(a, sk3), s(sk3, b), rule #16
38, s(a, c)=>e(a, c), rule #16
39, e(a, c)=>e(c, a), rule #9
40, e(c, a), r(a, sk3)=>r(c, sk3), rule #11
41, r(c, sk3)=>false, rule #7
------------
Leaf 58:
3, true=>s(a, b), s(a, c), rule #5
11, s(a, b), s(a, c)=>dom(sk1), s(b, sk1), s(c, sk1), rule #15
49, s(b, sk1)=>e(b, sk1), rule #16
54, s(c, sk1)=>e(c, sk1), rule #16
55, e(c, sk1)=>e(sk1, c), rule #9
56, e(b, sk1), e(sk1, c)=>e(b, c), rule #10
57, e(b, c)=>goal, rule #4
------------
Leaf 62:
3, true=>s(a, b), s(a, c), rule #5
11, s(a, b), s(a, c)=>dom(sk1), s(b, sk1), s(c, sk1), rule #15
49, s(b, sk1)=>dom(c), r(b, c), s(c, sk1), rule #16
54, s(c, sk1)=>dom(sk5), r(c, sk5), s(sk5, sk1), rule #16
61, r(c, sk5)=>false, rule #7
------------
Leaf 66:
3, true=>s(a, b), s(a, c), rule #5
11, s(a, b), s(a, c)=>dom(sk1), s(b, sk1), s(c, sk1), rule #15
49, s(b, sk1)=>dom(sk6), r(b, sk6), s(sk6, sk1), rule #16
65, r(b, sk6)=>false, rule #6
------------