Inference procedure has parameters:
Ice fuel: 200
Timeout: 60s
Convolution: right


Learning problem is:

env: {
elt -> {a, b}  ;  elt_bin_tree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(swap, F:
{() -> swap([leaf, leaf])
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)])}
(swap([_oh, _ph]) /\ swap([_oh, _qh])) -> eq_elt_bin_tree([_ph, _qh])
)
(member, P:
{() -> member([e2, node(e2, t1, t2)])
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)])
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)])
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2])
(member([e, leaf])) -> BOT}
)
}

properties:
{(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh])}


over-approximation: {swap}
under-approximation: {}

Clause system for inference is:

{
() -> member([e2, node(e2, t1, t2)]) -> 0
() -> swap([leaf, leaf]) -> 0
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 0
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 0
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 0
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 0
(member([e, leaf])) -> BOT -> 0
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 0
}


Solving took 60.000930 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661, q_gen_1664, q_gen_1665, q_gen_1666, q_gen_1667, q_gen_1668, q_gen_1669, q_gen_1670, q_gen_1671, q_gen_1672, q_gen_1673, q_gen_1674, q_gen_1675, q_gen_1676, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1689, q_gen_1690, q_gen_1691},
Q_f={},
Delta=
{
<leaf>() -> q_gen_1660
<b>() -> q_gen_1661
<node>(q_gen_1667, q_gen_1660, q_gen_1666) -> q_gen_1665
<node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1666
<a>() -> q_gen_1667
<node>(q_gen_1661, q_gen_1660, q_gen_1669) -> q_gen_1668
<node>(q_gen_1661, q_gen_1666, q_gen_1660) -> q_gen_1669
<node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1671
<node>(q_gen_1667, q_gen_1668, q_gen_1665) -> q_gen_1672
<node>(q_gen_1667, q_gen_1666, q_gen_1666) -> q_gen_1681
<node>(q_gen_1661, q_gen_1660, q_gen_1666) -> q_gen_1691
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1668, q_gen_1665) -> q_gen_1664
<b, node>(q_gen_1667, q_gen_1672, q_gen_1671) -> q_gen_1670
<b, leaf>() -> q_gen_1673
<b, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1674
<b, node>(q_gen_1667, q_gen_1671, q_gen_1660) -> q_gen_1675
<a, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1676
<b, node>(q_gen_1667, q_gen_1666, q_gen_1666) -> q_gen_1679
<b, node>(q_gen_1667, q_gen_1660, q_gen_1681) -> q_gen_1680
<b, node>(q_gen_1667, q_gen_1671, q_gen_1671) -> q_gen_1682
<b, node>(q_gen_1661, q_gen_1671, q_gen_1671) -> q_gen_1683
<b, node>(q_gen_1661, q_gen_1660, q_gen_1666) -> q_gen_1689
<b, node>(q_gen_1667, q_gen_1666, q_gen_1691) -> q_gen_1690
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658, q_gen_1662, q_gen_1663, q_gen_1677, q_gen_1678, q_gen_1684, q_gen_1685, q_gen_1686, q_gen_1687, q_gen_1688},
Q_f={},
Delta=
{
<leaf>() -> q_gen_1686
<b>() -> q_gen_1687
<leaf, leaf>() -> q_gen_1658
<node, node>(q_gen_1663, q_gen_1658, q_gen_1658) -> q_gen_1662
<b, b>() -> q_gen_1663
<node, node>(q_gen_1678, q_gen_1658, q_gen_1658) -> q_gen_1677
<a, a>() -> q_gen_1678
<node, node>(q_gen_1663, q_gen_1688, q_gen_1685) -> q_gen_1684
<node, leaf>(q_gen_1687, q_gen_1686, q_gen_1686) -> q_gen_1685
<leaf, node>(q_gen_1687, q_gen_1686, q_gen_1686) -> q_gen_1688
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005114 s (model generation: 0.004775,  model checking: 0.000339):

Model:
|_
{
member -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 0
() -> swap([leaf, leaf]) -> 3
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 1
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 1
(member([e, leaf])) -> BOT -> 1
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 1
}
Sat witness: Found: (() -> swap([leaf, leaf]), {

})

-------------------------------------------
Step 1, which took 0.004607 s (model generation: 0.004462,  model checking: 0.000145):

Model:
|_
{
member -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658},
Q_f={q_gen_1658},
Delta=
{
<leaf, leaf>() -> q_gen_1658
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> swap([leaf, leaf]) -> 3
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 1
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 1
(member([e, leaf])) -> BOT -> 1
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 1
}
Sat witness: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 2, which took 0.004456 s (model generation: 0.004345,  model checking: 0.000111):

Model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661},
Q_f={q_gen_1659},
Delta=
{
<leaf>() -> q_gen_1660
<b>() -> q_gen_1661
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658},
Q_f={q_gen_1658},
Delta=
{
<leaf, leaf>() -> q_gen_1658
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> swap([leaf, leaf]) -> 3
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 1
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 1
(member([e, leaf])) -> BOT -> 1
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 4
}
Sat witness: Found: ((swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]), {
_mh -> leaf  ;  _nh -> leaf  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 3, which took 0.077885 s (model generation: 0.005298,  model checking: 0.072587):

Model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661},
Q_f={q_gen_1659},
Delta=
{
<leaf>() -> q_gen_1660
<b>() -> q_gen_1661
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658, q_gen_1663},
Q_f={q_gen_1658},
Delta=
{
<leaf, leaf>() -> q_gen_1658
<node, node>(q_gen_1663, q_gen_1658, q_gen_1658) -> q_gen_1658
<b, b>() -> q_gen_1663
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> swap([leaf, leaf]) -> 3
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 1
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 2
(member([e, leaf])) -> BOT -> 2
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 4
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(a, node(b, leaf, node(b, node(a, leaf, leaf), leaf)), node(a, leaf, node(a, leaf, leaf)))  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 4, which took 0.006803 s (model generation: 0.006412,  model checking: 0.000391):

Model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661},
Q_f={q_gen_1659},
Delta=
{
<leaf>() -> q_gen_1660
<node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1660
<a>() -> q_gen_1661
<b>() -> q_gen_1661
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658, q_gen_1663},
Q_f={q_gen_1658},
Delta=
{
<leaf, leaf>() -> q_gen_1658
<node, node>(q_gen_1663, q_gen_1658, q_gen_1658) -> q_gen_1658
<b, b>() -> q_gen_1663
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> swap([leaf, leaf]) -> 3
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 2
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 2
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 3
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 4
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]), {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 5, which took 0.006715 s (model generation: 0.006392,  model checking: 0.000323):

Model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661},
Q_f={q_gen_1659},
Delta=
{
<leaf>() -> q_gen_1660
<node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1660
<a>() -> q_gen_1661
<b>() -> q_gen_1661
<b, leaf>() -> q_gen_1659
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658, q_gen_1663},
Q_f={q_gen_1658},
Delta=
{
<leaf, leaf>() -> q_gen_1658
<node, node>(q_gen_1663, q_gen_1658, q_gen_1658) -> q_gen_1658
<b, b>() -> q_gen_1663
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> swap([leaf, leaf]) -> 3
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 3
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 3
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 6
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 4
}
Sat witness: Found: ((member([e, leaf])) -> BOT, {
e -> b
})

-------------------------------------------
Step 6, which took 0.008216 s (model generation: 0.006032,  model checking: 0.002184):

Model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661, q_gen_1664, q_gen_1667, q_gen_1669},
Q_f={q_gen_1659},
Delta=
{
<leaf>() -> q_gen_1660
<node>(q_gen_1661, q_gen_1660, q_gen_1669) -> q_gen_1660
<node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1660
<b>() -> q_gen_1661
<a>() -> q_gen_1667
<node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1669
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1660, q_gen_1669) -> q_gen_1659
<b, leaf>() -> q_gen_1664
<b, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1664
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658, q_gen_1663},
Q_f={q_gen_1658},
Delta=
{
<leaf, leaf>() -> q_gen_1658
<node, node>(q_gen_1663, q_gen_1658, q_gen_1658) -> q_gen_1658
<b, b>() -> q_gen_1663
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> swap([leaf, leaf]) -> 3
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 3
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 6
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 4
}
Sat witness: Found: ((member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 7, which took 0.011477 s (model generation: 0.007292,  model checking: 0.004185):

Model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661, q_gen_1664, q_gen_1667, q_gen_1669},
Q_f={q_gen_1659},
Delta=
{
<leaf>() -> q_gen_1660
<node>(q_gen_1661, q_gen_1660, q_gen_1669) -> q_gen_1660
<node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1660
<b>() -> q_gen_1661
<a>() -> q_gen_1667
<node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1669
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1660, q_gen_1669) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1669, q_gen_1660) -> q_gen_1659
<b, leaf>() -> q_gen_1664
<b, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1664
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658, q_gen_1663},
Q_f={q_gen_1658},
Delta=
{
<leaf, leaf>() -> q_gen_1658
<node, node>(q_gen_1663, q_gen_1658, q_gen_1658) -> q_gen_1658
<b, b>() -> q_gen_1663
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> swap([leaf, leaf]) -> 4
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 4
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 6
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 4
}
Sat witness: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 8, which took 0.011981 s (model generation: 0.010434,  model checking: 0.001547):

Model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661, q_gen_1665, q_gen_1667, q_gen_1673},
Q_f={q_gen_1659},
Delta=
{
<leaf>() -> q_gen_1660
<node>(q_gen_1667, q_gen_1665, q_gen_1665) -> q_gen_1660
<b>() -> q_gen_1661
<node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1665
<node>(q_gen_1661, q_gen_1660, q_gen_1665) -> q_gen_1665
<node>(q_gen_1661, q_gen_1665, q_gen_1660) -> q_gen_1665
<node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1665
<node>(q_gen_1667, q_gen_1660, q_gen_1665) -> q_gen_1665
<a>() -> q_gen_1667
<a, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1660, q_gen_1665) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1665, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1665, q_gen_1665) -> q_gen_1659
<b, leaf>() -> q_gen_1673
<b, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1673
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658, q_gen_1663},
Q_f={q_gen_1658},
Delta=
{
<leaf, leaf>() -> q_gen_1658
<node, node>(q_gen_1663, q_gen_1658, q_gen_1658) -> q_gen_1658
<b, b>() -> q_gen_1663
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> swap([leaf, leaf]) -> 4
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 4
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 6
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 7
}
Sat witness: Found: ((swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]), {
_mh -> leaf  ;  _nh -> leaf  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 9, which took 0.068092 s (model generation: 0.016417,  model checking: 0.051675):

Model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661, q_gen_1665, q_gen_1667, q_gen_1673},
Q_f={q_gen_1659},
Delta=
{
<leaf>() -> q_gen_1660
<node>(q_gen_1667, q_gen_1665, q_gen_1665) -> q_gen_1660
<b>() -> q_gen_1661
<node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1665
<node>(q_gen_1661, q_gen_1660, q_gen_1665) -> q_gen_1665
<node>(q_gen_1661, q_gen_1665, q_gen_1660) -> q_gen_1665
<node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1665
<node>(q_gen_1667, q_gen_1660, q_gen_1665) -> q_gen_1665
<a>() -> q_gen_1667
<a, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1660, q_gen_1665) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1665, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1665, q_gen_1665) -> q_gen_1659
<b, leaf>() -> q_gen_1673
<b, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1673
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658, q_gen_1663},
Q_f={q_gen_1658},
Delta=
{
<leaf, leaf>() -> q_gen_1658
<node, node>(q_gen_1663, q_gen_1658, q_gen_1658) -> q_gen_1658
<a, a>() -> q_gen_1663
<b, b>() -> q_gen_1663
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> swap([leaf, leaf]) -> 4
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 4
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 6
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 7
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> node(a, node(a, leaf, leaf), node(a, leaf, leaf))
})

-------------------------------------------
Step 10, which took 0.022206 s (model generation: 0.010643,  model checking: 0.011563):

Model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661, q_gen_1665, q_gen_1667, q_gen_1673},
Q_f={q_gen_1659},
Delta=
{
<leaf>() -> q_gen_1660
<b>() -> q_gen_1661
<node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1665
<node>(q_gen_1661, q_gen_1660, q_gen_1665) -> q_gen_1665
<node>(q_gen_1661, q_gen_1665, q_gen_1660) -> q_gen_1665
<node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1665
<node>(q_gen_1667, q_gen_1660, q_gen_1665) -> q_gen_1665
<node>(q_gen_1667, q_gen_1665, q_gen_1665) -> q_gen_1665
<a>() -> q_gen_1667
<a, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1660, q_gen_1665) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1665, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1665, q_gen_1665) -> q_gen_1659
<b, leaf>() -> q_gen_1673
<b, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1673
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658, q_gen_1663},
Q_f={q_gen_1658},
Delta=
{
<leaf, leaf>() -> q_gen_1658
<node, node>(q_gen_1663, q_gen_1658, q_gen_1658) -> q_gen_1658
<a, a>() -> q_gen_1663
<b, b>() -> q_gen_1663
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> swap([leaf, leaf]) -> 5
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 5
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8
(member([e, leaf])) -> BOT -> 6
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 7
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]), {
e -> b  ;  e2 -> a  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(a, leaf, leaf)
})

-------------------------------------------
Step 11, which took 0.038750 s (model generation: 0.017313,  model checking: 0.021437):

Model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661, q_gen_1666, q_gen_1667, q_gen_1673},
Q_f={q_gen_1659},
Delta=
{
<leaf>() -> q_gen_1660
<node>(q_gen_1667, q_gen_1660, q_gen_1666) -> q_gen_1660
<node>(q_gen_1667, q_gen_1666, q_gen_1660) -> q_gen_1660
<node>(q_gen_1667, q_gen_1666, q_gen_1666) -> q_gen_1660
<b>() -> q_gen_1661
<node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1666
<node>(q_gen_1661, q_gen_1660, q_gen_1666) -> q_gen_1666
<node>(q_gen_1661, q_gen_1666, q_gen_1660) -> q_gen_1666
<node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1666
<a>() -> q_gen_1667
<a, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1660, q_gen_1666) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1666, q_gen_1660) -> q_gen_1659
<b, leaf>() -> q_gen_1673
<b, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1673
<b, node>(q_gen_1667, q_gen_1666, q_gen_1666) -> q_gen_1673
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658, q_gen_1663},
Q_f={q_gen_1658},
Delta=
{
<leaf, leaf>() -> q_gen_1658
<node, node>(q_gen_1663, q_gen_1658, q_gen_1658) -> q_gen_1658
<a, a>() -> q_gen_1663
<b, b>() -> q_gen_1663
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> swap([leaf, leaf]) -> 6
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 6
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8
(member([e, leaf])) -> BOT -> 7
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 7
}
Sat witness: Found: ((member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 12, which took 0.030353 s (model generation: 0.020284,  model checking: 0.010069):

Model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661, q_gen_1667, q_gen_1668, q_gen_1673},
Q_f={q_gen_1659},
Delta=
{
<leaf>() -> q_gen_1660
<node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1660
<b>() -> q_gen_1661
<a>() -> q_gen_1667
<node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1668
<node>(q_gen_1661, q_gen_1660, q_gen_1668) -> q_gen_1668
<node>(q_gen_1667, q_gen_1668, q_gen_1660) -> q_gen_1668
<a, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1668, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1668, q_gen_1668) -> q_gen_1659
<b, leaf>() -> q_gen_1673
<b, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1673
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658, q_gen_1663},
Q_f={q_gen_1658},
Delta=
{
<leaf, leaf>() -> q_gen_1658
<node, node>(q_gen_1663, q_gen_1658, q_gen_1658) -> q_gen_1658
<a, a>() -> q_gen_1663
<b, b>() -> q_gen_1663
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 9
() -> swap([leaf, leaf]) -> 7
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 7
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8
(member([e, leaf])) -> BOT -> 7
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 7
}
Sat witness: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 13, which took 0.025482 s (model generation: 0.023106,  model checking: 0.002376):

Model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661, q_gen_1667, q_gen_1668, q_gen_1673},
Q_f={q_gen_1659},
Delta=
{
<leaf>() -> q_gen_1660
<node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1660
<b>() -> q_gen_1661
<a>() -> q_gen_1667
<node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1668
<node>(q_gen_1661, q_gen_1660, q_gen_1668) -> q_gen_1668
<node>(q_gen_1667, q_gen_1668, q_gen_1660) -> q_gen_1668
<a, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1661, q_gen_1668, q_gen_1668) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1668, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1668, q_gen_1668) -> q_gen_1659
<b, leaf>() -> q_gen_1673
<b, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1673
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658, q_gen_1663},
Q_f={q_gen_1658},
Delta=
{
<leaf, leaf>() -> q_gen_1658
<node, node>(q_gen_1663, q_gen_1658, q_gen_1658) -> q_gen_1658
<a, a>() -> q_gen_1663
<b, b>() -> q_gen_1663
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 9
() -> swap([leaf, leaf]) -> 7
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 7
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8
(member([e, leaf])) -> BOT -> 7
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 10
}
Sat witness: Found: ((swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]), {
_mh -> node(b, leaf, leaf)  ;  _nh -> leaf  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 14, which took 5.006401 s (model generation: 0.024244,  model checking: 4.982157):

Model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661, q_gen_1667, q_gen_1668, q_gen_1673},
Q_f={q_gen_1659},
Delta=
{
<leaf>() -> q_gen_1660
<node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1660
<b>() -> q_gen_1661
<a>() -> q_gen_1667
<node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1668
<node>(q_gen_1661, q_gen_1660, q_gen_1668) -> q_gen_1668
<node>(q_gen_1667, q_gen_1668, q_gen_1660) -> q_gen_1668
<a, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1661, q_gen_1668, q_gen_1668) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1668, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1668, q_gen_1668) -> q_gen_1659
<b, leaf>() -> q_gen_1673
<b, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1673
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658, q_gen_1663, q_gen_1686, q_gen_1687},
Q_f={q_gen_1658},
Delta=
{
<leaf>() -> q_gen_1686
<b>() -> q_gen_1687
<leaf, leaf>() -> q_gen_1658
<leaf, node>(q_gen_1687, q_gen_1686, q_gen_1686) -> q_gen_1658
<node, leaf>(q_gen_1687, q_gen_1686, q_gen_1686) -> q_gen_1658
<node, node>(q_gen_1663, q_gen_1658, q_gen_1658) -> q_gen_1658
<a, a>() -> q_gen_1663
<b, b>() -> q_gen_1663
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 9
() -> swap([leaf, leaf]) -> 7
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 7
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 10
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8
(member([e, leaf])) -> BOT -> 8
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 10
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(b, leaf, node(a, leaf, leaf))
})

-------------------------------------------
Step 15, which took 0.012282 s (model generation: 0.011732,  model checking: 0.000550):

Model:
|_
{
member -> 
{{{
Q={q_gen_1659, q_gen_1660, q_gen_1661, q_gen_1664, q_gen_1667, q_gen_1669},
Q_f={q_gen_1659},
Delta=
{
<leaf>() -> q_gen_1660
<node>(q_gen_1661, q_gen_1660, q_gen_1669) -> q_gen_1660
<node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1660
<b>() -> q_gen_1661
<a>() -> q_gen_1667
<node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1669
<a, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1661, q_gen_1660, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1661, q_gen_1669, q_gen_1669) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1660, q_gen_1669) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1669, q_gen_1660) -> q_gen_1659
<b, node>(q_gen_1667, q_gen_1669, q_gen_1669) -> q_gen_1659
<b, leaf>() -> q_gen_1664
<b, node>(q_gen_1667, q_gen_1660, q_gen_1660) -> q_gen_1664
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  swap -> 
{{{
Q={q_gen_1658, q_gen_1663, q_gen_1686, q_gen_1687},
Q_f={q_gen_1658},
Delta=
{
<leaf>() -> q_gen_1686
<b>() -> q_gen_1687
<leaf, leaf>() -> q_gen_1658
<leaf, node>(q_gen_1687, q_gen_1686, q_gen_1686) -> q_gen_1658
<node, leaf>(q_gen_1687, q_gen_1686, q_gen_1686) -> q_gen_1658
<node, node>(q_gen_1663, q_gen_1658, q_gen_1658) -> q_gen_1658
<a, a>() -> q_gen_1663
<b, b>() -> q_gen_1663
}

Datatype: <elt_bin_tree, elt_bin_tree>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 9
() -> swap([leaf, leaf]) -> 7
(member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 10
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 10
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8
(member([e, leaf])) -> BOT -> 8
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 10
}
Sat witness: Found: ((member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]), {
_rh -> leaf  ;  e -> b  ;  t1 -> node(b, leaf, leaf)
})

Total time: 60.000930
Reason for stopping: DontKnow. Stopped because: timeout