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


Learning problem is:

env: {
elt -> {a, b}  ;  elt_bin_tree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(swap, F:
{() -> swap([leaf, leaf])
(swap([t1, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)])}
(swap([_vi, _wi]) /\ swap([_vi, _xi])) -> eq_elt_bin_tree([_wi, _xi])
)
(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, _yi])) -> member([e, _yi])}


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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 0
}


Solving took 60.001331 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212, q_gen_2215, q_gen_2216, q_gen_2217, q_gen_2218, q_gen_2219, q_gen_2220, q_gen_2221, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2239, q_gen_2240, q_gen_2241, q_gen_2242, q_gen_2243},
Q_f={},
Delta=
{
<leaf>() -> q_gen_2211
<b>() -> q_gen_2212
<node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2216
<a>() -> q_gen_2217
<node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2219
<node>(q_gen_2217, q_gen_2211, q_gen_2216) -> q_gen_2220
<node>(q_gen_2217, q_gen_2219, q_gen_2219) -> q_gen_2225
<node>(q_gen_2217, q_gen_2211, q_gen_2219) -> q_gen_2231
<node>(q_gen_2212, q_gen_2211, q_gen_2216) -> q_gen_2240
<node>(q_gen_2217, q_gen_2240, q_gen_2240) -> q_gen_2241
<node>(q_gen_2212, q_gen_2241, q_gen_2240) -> q_gen_2243
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2211, q_gen_2216) -> q_gen_2215
<b, node>(q_gen_2217, q_gen_2220, q_gen_2219) -> q_gen_2218
<b, leaf>() -> q_gen_2221
<b, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2222
<b, node>(q_gen_2217, q_gen_2219, q_gen_2219) -> q_gen_2223
<b, node>(q_gen_2217, q_gen_2225, q_gen_2211) -> q_gen_2224
<a, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2226
<b, node>(q_gen_2217, q_gen_2211, q_gen_2219) -> q_gen_2229
<b, node>(q_gen_2217, q_gen_2211, q_gen_2231) -> q_gen_2230
<b, node>(q_gen_2217, q_gen_2216, q_gen_2211) -> q_gen_2232
<b, node>(q_gen_2212, q_gen_2219, q_gen_2219) -> q_gen_2233
<b, node>(q_gen_2212, q_gen_2241, q_gen_2240) -> q_gen_2239
<b, node>(q_gen_2217, q_gen_2216, q_gen_2243) -> q_gen_2242
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  swap -> 
{{{
Q={q_gen_2209, q_gen_2213, q_gen_2214, q_gen_2227, q_gen_2228, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2237, q_gen_2238},
Q_f={},
Delta=
{
<leaf>() -> q_gen_2236
<b>() -> q_gen_2237
<leaf, leaf>() -> q_gen_2209
<node, node>(q_gen_2214, q_gen_2209, q_gen_2209) -> q_gen_2213
<b, b>() -> q_gen_2214
<node, node>(q_gen_2228, q_gen_2209, q_gen_2209) -> q_gen_2227
<a, a>() -> q_gen_2228
<node, node>(q_gen_2214, q_gen_2238, q_gen_2235) -> q_gen_2234
<node, leaf>(q_gen_2237, q_gen_2236, q_gen_2236) -> q_gen_2235
<leaf, node>(q_gen_2237, q_gen_2236, q_gen_2236) -> q_gen_2238
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007659 s (model generation: 0.007348,  model checking: 0.000311):

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

}

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

}

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 1
}
Sat witness: Found: (() -> swap([leaf, leaf]), {

})

-------------------------------------------
Step 1, which took 0.007274 s (model generation: 0.007178,  model checking: 0.000096):

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

}

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

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 1
}
Sat witness: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 2, which took 0.008791 s (model generation: 0.007896,  model checking: 0.000895):

Model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212},
Q_f={q_gen_2210},
Delta=
{
<leaf>() -> q_gen_2211
<b>() -> q_gen_2212
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
}

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

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 4
}
Sat witness: Found: ((swap([t1, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]), {
_ti -> leaf  ;  _ui -> leaf  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 3, which took 0.129668 s (model generation: 0.008026,  model checking: 0.121642):

Model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212},
Q_f={q_gen_2210},
Delta=
{
<leaf>() -> q_gen_2211
<b>() -> q_gen_2212
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  swap -> 
{{{
Q={q_gen_2209, q_gen_2214},
Q_f={q_gen_2209},
Delta=
{
<leaf, leaf>() -> q_gen_2209
<node, node>(q_gen_2214, q_gen_2209, q_gen_2209) -> q_gen_2209
<b, b>() -> q_gen_2214
}

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 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, leaf, node(a, leaf, leaf))  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 4, which took 0.010853 s (model generation: 0.010449,  model checking: 0.000404):

Model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212},
Q_f={q_gen_2210},
Delta=
{
<leaf>() -> q_gen_2211
<node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2211
<a>() -> q_gen_2212
<b>() -> q_gen_2212
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  swap -> 
{{{
Q={q_gen_2209, q_gen_2214},
Q_f={q_gen_2209},
Delta=
{
<leaf, leaf>() -> q_gen_2209
<node, node>(q_gen_2214, q_gen_2209, q_gen_2209) -> q_gen_2209
<b, b>() -> q_gen_2214
}

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 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.009881 s (model generation: 0.009678,  model checking: 0.000203):

Model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212},
Q_f={q_gen_2210},
Delta=
{
<leaf>() -> q_gen_2211
<node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2211
<a>() -> q_gen_2212
<b>() -> q_gen_2212
<b, leaf>() -> q_gen_2210
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  swap -> 
{{{
Q={q_gen_2209, q_gen_2214},
Q_f={q_gen_2209},
Delta=
{
<leaf, leaf>() -> q_gen_2209
<node, node>(q_gen_2214, q_gen_2209, q_gen_2209) -> q_gen_2209
<b, b>() -> q_gen_2214
}

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 4
}
Sat witness: Found: ((member([e, leaf])) -> BOT, {
e -> b
})

-------------------------------------------
Step 6, which took 0.016180 s (model generation: 0.009981,  model checking: 0.006199):

Model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212, q_gen_2216, q_gen_2217, q_gen_2221},
Q_f={q_gen_2210},
Delta=
{
<leaf>() -> q_gen_2211
<b>() -> q_gen_2212
<node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2216
<node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2216
<node>(q_gen_2217, q_gen_2211, q_gen_2216) -> q_gen_2216
<a>() -> q_gen_2217
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2211, q_gen_2216) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2216, q_gen_2216) -> q_gen_2210
<b, leaf>() -> q_gen_2221
<b, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2221
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  swap -> 
{{{
Q={q_gen_2209, q_gen_2214},
Q_f={q_gen_2209},
Delta=
{
<leaf, leaf>() -> q_gen_2209
<node, node>(q_gen_2214, q_gen_2209, q_gen_2209) -> q_gen_2209
<b, b>() -> q_gen_2214
}

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 4
}
Sat witness: Found: ((member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(a, node(b, leaf, leaf), node(b, leaf, leaf))  ;  t2 -> leaf
})

-------------------------------------------
Step 7, which took 0.015027 s (model generation: 0.011752,  model checking: 0.003275):

Model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212, q_gen_2216, q_gen_2217, q_gen_2221},
Q_f={q_gen_2210},
Delta=
{
<leaf>() -> q_gen_2211
<node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2211
<b>() -> q_gen_2212
<node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2216
<node>(q_gen_2217, q_gen_2211, q_gen_2216) -> q_gen_2216
<a>() -> q_gen_2217
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2211, q_gen_2216) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2216, q_gen_2211) -> q_gen_2210
<b, leaf>() -> q_gen_2221
<b, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2221
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  swap -> 
{{{
Q={q_gen_2209, q_gen_2214},
Q_f={q_gen_2209},
Delta=
{
<leaf, leaf>() -> q_gen_2209
<node, node>(q_gen_2214, q_gen_2209, q_gen_2209) -> q_gen_2209
<b, b>() -> q_gen_2214
}

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 4
}
Sat witness: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 8, which took 0.013455 s (model generation: 0.012725,  model checking: 0.000730):

Model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212, q_gen_2216, q_gen_2217, q_gen_2221},
Q_f={q_gen_2210},
Delta=
{
<leaf>() -> q_gen_2211
<node>(q_gen_2217, q_gen_2211, q_gen_2216) -> q_gen_2211
<node>(q_gen_2217, q_gen_2216, q_gen_2216) -> q_gen_2211
<b>() -> q_gen_2212
<node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2216
<node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2216
<a>() -> q_gen_2217
<a, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2211, q_gen_2216) -> q_gen_2210
<b, leaf>() -> q_gen_2221
<b, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2221
<b, node>(q_gen_2217, q_gen_2216, q_gen_2216) -> q_gen_2221
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  swap -> 
{{{
Q={q_gen_2209, q_gen_2214},
Q_f={q_gen_2209},
Delta=
{
<leaf, leaf>() -> q_gen_2209
<node, node>(q_gen_2214, q_gen_2209, q_gen_2209) -> q_gen_2209
<b, b>() -> q_gen_2214
}

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 7
}
Sat witness: Found: ((swap([t1, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]), {
_ti -> leaf  ;  _ui -> leaf  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 9, which took 0.021835 s (model generation: 0.016990,  model checking: 0.004845):

Model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212, q_gen_2216, q_gen_2217, q_gen_2221},
Q_f={q_gen_2210},
Delta=
{
<leaf>() -> q_gen_2211
<node>(q_gen_2217, q_gen_2211, q_gen_2216) -> q_gen_2211
<node>(q_gen_2217, q_gen_2216, q_gen_2216) -> q_gen_2211
<b>() -> q_gen_2212
<node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2216
<node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2216
<a>() -> q_gen_2217
<a, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2211, q_gen_2216) -> q_gen_2210
<b, leaf>() -> q_gen_2221
<b, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2221
<b, node>(q_gen_2217, q_gen_2216, q_gen_2216) -> q_gen_2221
}

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

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 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, leaf, node(b, leaf, leaf))
})

-------------------------------------------
Step 10, which took 0.018741 s (model generation: 0.014572,  model checking: 0.004169):

Model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212, q_gen_2216, q_gen_2217, q_gen_2221},
Q_f={q_gen_2210},
Delta=
{
<leaf>() -> q_gen_2211
<node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2211
<b>() -> q_gen_2212
<node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2216
<node>(q_gen_2217, q_gen_2211, q_gen_2216) -> q_gen_2216
<a>() -> q_gen_2217
<a, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2211, q_gen_2216) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2216, q_gen_2211) -> q_gen_2210
<b, leaf>() -> q_gen_2221
<b, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2221
}

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

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 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 -> leaf
})

-------------------------------------------
Step 11, which took 0.021771 s (model generation: 0.017051,  model checking: 0.004720):

Model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212, q_gen_2215, q_gen_2217, q_gen_2219},
Q_f={q_gen_2210},
Delta=
{
<leaf>() -> q_gen_2211
<node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2211
<b>() -> q_gen_2212
<a>() -> q_gen_2217
<node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2219
<node>(q_gen_2217, q_gen_2211, q_gen_2219) -> q_gen_2219
<node>(q_gen_2217, q_gen_2219, q_gen_2219) -> q_gen_2219
<a, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2211, q_gen_2219) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2219, q_gen_2211) -> q_gen_2210
<b, leaf>() -> q_gen_2215
<b, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2215
<b, node>(q_gen_2217, q_gen_2219, q_gen_2219) -> q_gen_2215
}

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

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 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.021027 s (model generation: 0.016544,  model checking: 0.004483):

Model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212, q_gen_2215, q_gen_2217, q_gen_2219},
Q_f={q_gen_2210},
Delta=
{
<leaf>() -> q_gen_2211
<node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2211
<b>() -> q_gen_2212
<a>() -> q_gen_2217
<node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2219
<node>(q_gen_2217, q_gen_2211, q_gen_2219) -> q_gen_2219
<node>(q_gen_2217, q_gen_2219, q_gen_2219) -> q_gen_2219
<a, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2211, q_gen_2219) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2219, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2219, q_gen_2219) -> q_gen_2210
<b, leaf>() -> q_gen_2215
<b, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2215
}

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

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 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.020733 s (model generation: 0.019266,  model checking: 0.001467):

Model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212, q_gen_2215, q_gen_2217, q_gen_2219},
Q_f={q_gen_2210},
Delta=
{
<leaf>() -> q_gen_2211
<node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2211
<b>() -> q_gen_2212
<a>() -> q_gen_2217
<node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2219
<node>(q_gen_2217, q_gen_2211, q_gen_2219) -> q_gen_2219
<node>(q_gen_2217, q_gen_2219, q_gen_2219) -> q_gen_2219
<a, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2212, q_gen_2219, q_gen_2219) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2211, q_gen_2219) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2219, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2219, q_gen_2219) -> q_gen_2210
<b, leaf>() -> q_gen_2215
<b, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2215
}

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

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 10
}
Sat witness: Found: ((swap([t1, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]), {
_ti -> node(b, leaf, leaf)  ;  _ui -> leaf  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 14, which took 8.693250 s (model generation: 0.025804,  model checking: 8.667446):

Model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212, q_gen_2215, q_gen_2217, q_gen_2219},
Q_f={q_gen_2210},
Delta=
{
<leaf>() -> q_gen_2211
<node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2211
<b>() -> q_gen_2212
<a>() -> q_gen_2217
<node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2219
<node>(q_gen_2217, q_gen_2211, q_gen_2219) -> q_gen_2219
<node>(q_gen_2217, q_gen_2219, q_gen_2219) -> q_gen_2219
<a, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2212, q_gen_2219, q_gen_2219) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2211, q_gen_2219) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2219, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2219, q_gen_2219) -> q_gen_2210
<b, leaf>() -> q_gen_2215
<b, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2215
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  swap -> 
{{{
Q={q_gen_2209, q_gen_2214, q_gen_2236, q_gen_2237},
Q_f={q_gen_2209},
Delta=
{
<leaf>() -> q_gen_2236
<b>() -> q_gen_2237
<leaf, leaf>() -> q_gen_2209
<leaf, node>(q_gen_2237, q_gen_2236, q_gen_2236) -> q_gen_2209
<node, leaf>(q_gen_2237, q_gen_2236, q_gen_2236) -> q_gen_2209
<node, node>(q_gen_2214, q_gen_2209, q_gen_2209) -> q_gen_2209
<a, a>() -> q_gen_2214
<b, b>() -> q_gen_2214
}

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 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, node(a, node(b, leaf, node(a, leaf, leaf)), node(b, leaf, node(a, leaf, leaf))), node(b, leaf, node(a, leaf, leaf)))
})

-------------------------------------------
Step 15, which took 0.025521 s (model generation: 0.025041,  model checking: 0.000480):

Model:
|_
{
member -> 
{{{
Q={q_gen_2210, q_gen_2211, q_gen_2212, q_gen_2215, q_gen_2217, q_gen_2219},
Q_f={q_gen_2210},
Delta=
{
<leaf>() -> q_gen_2211
<node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2211
<b>() -> q_gen_2212
<a>() -> q_gen_2217
<node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2219
<node>(q_gen_2212, q_gen_2219, q_gen_2219) -> q_gen_2219
<node>(q_gen_2217, q_gen_2211, q_gen_2219) -> q_gen_2219
<node>(q_gen_2217, q_gen_2219, q_gen_2219) -> q_gen_2219
<a, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2212, q_gen_2211, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2212, q_gen_2219, q_gen_2219) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2211, q_gen_2219) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2219, q_gen_2211) -> q_gen_2210
<b, node>(q_gen_2217, q_gen_2219, q_gen_2219) -> q_gen_2210
<b, leaf>() -> q_gen_2215
<b, node>(q_gen_2217, q_gen_2211, q_gen_2211) -> q_gen_2215
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  swap -> 
{{{
Q={q_gen_2209, q_gen_2214, q_gen_2236, q_gen_2237},
Q_f={q_gen_2209},
Delta=
{
<leaf>() -> q_gen_2236
<b>() -> q_gen_2237
<leaf, leaf>() -> q_gen_2209
<leaf, node>(q_gen_2237, q_gen_2236, q_gen_2236) -> q_gen_2209
<node, leaf>(q_gen_2237, q_gen_2236, q_gen_2236) -> q_gen_2209
<node, node>(q_gen_2214, q_gen_2209, q_gen_2209) -> q_gen_2209
<a, a>() -> q_gen_2214
<b, b>() -> q_gen_2214
}

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

}
--
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, _yi])) -> member([e, _yi]) -> 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, _ui]) /\ swap([t2, _ti])) -> swap([node(e, t1, t2), node(e, _ti, _ui)]) -> 10
}
Sat witness: Found: ((member([e, t1]) /\ swap([t1, _yi])) -> member([e, _yi]), {
_yi -> leaf  ;  e -> b  ;  t1 -> node(b, leaf, leaf)
})

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