Solving ../../benchmarks/true/timbuk_replaceTree.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


Learning problem is:

env: {
elt -> {a, b}  ;  elt_bin_tree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(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}
)
(replace, F:
{() -> replace([e1, e2, leaf, leaf])
(replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)])
(replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)])}
(replace([_gfa, _hfa, _ifa, _jfa]) /\ replace([_gfa, _hfa, _ifa, _kfa])) -> eq_elt_bin_tree([_jfa, _kfa])
)
}

properties:
{(member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT}


over-approximation: {member, replace}
under-approximation: {}

Clause system for inference is:

{
() -> member([e2, node(e2, t1, t2)]) -> 0  ;  () -> replace([e1, e2, leaf, leaf]) -> 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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 0  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 0  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 0
}


Solving took 30.025023 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6341, q_gen_6342, q_gen_6343, q_gen_6344, q_gen_6345, q_gen_6346, q_gen_6347, q_gen_6348, q_gen_6349, q_gen_6351, q_gen_6362, q_gen_6363, q_gen_6364, q_gen_6365, q_gen_6366, q_gen_6368, q_gen_6375, q_gen_6377, q_gen_6378, q_gen_6379, q_gen_6381},
Q_f={},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6342
<a>() -> q_gen_6343
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6345
<node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6346
<node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6364
<node>(q_gen_6343, q_gen_6330, q_gen_6364) -> q_gen_6379
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6346, q_gen_6345) -> q_gen_6344
<b, leaf>() -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6348
<b, node>(q_gen_6343, q_gen_6345, q_gen_6330) -> q_gen_6349
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6351
<b, node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6362
<b, node>(q_gen_6343, q_gen_6342, q_gen_6364) -> q_gen_6363
<b, node>(q_gen_6343, q_gen_6342, q_gen_6330) -> q_gen_6365
<a, node>(q_gen_6331, q_gen_6342, q_gen_6330) -> q_gen_6366
<b, node>(q_gen_6331, q_gen_6345, q_gen_6345) -> q_gen_6368
<a, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6375
<b, node>(q_gen_6343, q_gen_6330, q_gen_6364) -> q_gen_6377
<b, node>(q_gen_6343, q_gen_6342, q_gen_6379) -> q_gen_6378
<b, node>(q_gen_6331, q_gen_6345, q_gen_6330) -> q_gen_6381
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6332, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6337, q_gen_6338, q_gen_6339, q_gen_6340, q_gen_6350, q_gen_6352, q_gen_6353, q_gen_6354, q_gen_6355, q_gen_6356, q_gen_6357, q_gen_6358, q_gen_6359, q_gen_6360, q_gen_6361, q_gen_6367, q_gen_6369, q_gen_6370, q_gen_6371, q_gen_6372, q_gen_6373, q_gen_6374, q_gen_6376, q_gen_6380, q_gen_6382},
Q_f={},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, b>() -> q_gen_6334
<b, leaf>() -> q_gen_6335
<b, b>() -> q_gen_6336
<leaf, a>() -> q_gen_6338
<a, leaf>() -> q_gen_6339
<a, a>() -> q_gen_6340
<b, a>() -> q_gen_6353
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6355
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6358
<node, node>(q_gen_6340, q_gen_6339, q_gen_6339, q_gen_6338, q_gen_6333, q_gen_6333, q_gen_6338, q_gen_6333, q_gen_6333) -> q_gen_6359
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6360
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6361
<a, b>() -> q_gen_6370
<node, b>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6373
<b, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6374
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6332
<b, b, node, node>(q_gen_6340, q_gen_6339, q_gen_6339, q_gen_6338, q_gen_6333, q_gen_6333, q_gen_6338, q_gen_6333, q_gen_6333) -> q_gen_6337
<b, a, leaf, leaf>() -> q_gen_6350
<b, a, node, node>(q_gen_6353, q_gen_6335, q_gen_6335, q_gen_6338, q_gen_6333, q_gen_6333, q_gen_6338, q_gen_6333, q_gen_6333) -> q_gen_6352
<b, b, node, node>(q_gen_6340, q_gen_6361, q_gen_6339, q_gen_6360, q_gen_6359, q_gen_6358, q_gen_6338, q_gen_6355, q_gen_6333) -> q_gen_6354
<a, b, leaf, leaf>() -> q_gen_6367
<a, b, node, node>(q_gen_6370, q_gen_6339, q_gen_6339, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6369
<a, b, node, node>(q_gen_6340, q_gen_6339, q_gen_6339, q_gen_6338, q_gen_6333, q_gen_6333, q_gen_6338, q_gen_6333, q_gen_6333) -> q_gen_6371
<a, b, node, node>(q_gen_6336, q_gen_6374, q_gen_6335, q_gen_6373, q_gen_6359, q_gen_6358, q_gen_6334, q_gen_6355, q_gen_6333) -> q_gen_6372
<a, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6376
<a, a, leaf, leaf>() -> q_gen_6380
<a, a, node, node>(q_gen_6340, q_gen_6339, q_gen_6339, q_gen_6338, q_gen_6333, q_gen_6333, q_gen_6338, q_gen_6333, q_gen_6333) -> q_gen_6382
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006247 s (model generation: 0.005015,  model checking: 0.001232):

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

}

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

}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 3  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 1  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 1  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 1
}
Sat witness: Yes: (() -> replace([e1, e2, leaf, leaf]), {
e1 -> b  ;  e2 -> b
})

-------------------------------------------
Step 1, which took 0.008957 s (model generation: 0.008764,  model checking: 0.000193):

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

}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328},
Q_f={q_gen_6328},
Delta=
{
<b, b, leaf, leaf>() -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 3  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 1  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 1  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 1
}
Sat witness: Yes: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 2, which took 0.011965 s (model generation: 0.010728,  model checking: 0.001237):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328},
Q_f={q_gen_6328},
Delta=
{
<b, b, leaf, leaf>() -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 3  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 1  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 1  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 4
}
Sat witness: Yes: ((replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]), {
_cfa -> leaf  ;  _dfa -> leaf  ;  e2 -> b  ;  e3 -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 3, which took 0.179134 s (model generation: 0.012019,  model checking: 0.167115):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336},
Q_f={q_gen_6328},
Delta=
{
<leaf, leaf>() -> q_gen_6333
<leaf, b>() -> q_gen_6334
<b, leaf>() -> q_gen_6335
<b, b>() -> q_gen_6336
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 3  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 1  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 4  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 4
}
Sat witness: Yes: ((replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]), {
_efa -> leaf  ;  _ffa -> leaf  ;  e1 -> b  ;  e2 -> b  ;  e3 -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 4, which took 0.080173 s (model generation: 0.004850,  model checking: 0.075323):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336},
Q_f={q_gen_6328},
Delta=
{
<leaf, leaf>() -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<a, leaf>() -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 3  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 2  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 4  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 4
}
Sat witness: Yes: ((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 5, which took 0.005273 s (model generation: 0.005056,  model checking: 0.000217):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6330
<a>() -> q_gen_6331
<b>() -> q_gen_6331
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336},
Q_f={q_gen_6328},
Delta=
{
<leaf, leaf>() -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<a, leaf>() -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 3  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 3  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 4  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 4
}
Sat witness: Yes: ((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 6, which took 0.004873 s (model generation: 0.004802,  model checking: 0.000071):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6330
<a>() -> q_gen_6331
<b>() -> q_gen_6331
<b, leaf>() -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336},
Q_f={q_gen_6328},
Delta=
{
<leaf, leaf>() -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<a, leaf>() -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 4  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 4  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 4
}
Sat witness: Yes: ((member([e, leaf])) -> BOT, {
e -> b
})

-------------------------------------------
Step 7, which took 0.009731 s (model generation: 0.004542,  model checking: 0.005189):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6342, q_gen_6343, q_gen_6347},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6342
<a>() -> q_gen_6343
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6342) -> q_gen_6329
<b, leaf>() -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6347
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336},
Q_f={q_gen_6328},
Delta=
{
<leaf, leaf>() -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<a, leaf>() -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 4  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 4  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 4
}
Sat witness: Yes: ((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 8, which took 0.015522 s (model generation: 0.004766,  model checking: 0.010756):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6342, q_gen_6343, q_gen_6347},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6342
<a>() -> q_gen_6343
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6342) -> q_gen_6329
<b, leaf>() -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6347
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336},
Q_f={q_gen_6328},
Delta=
{
<leaf, leaf>() -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<a, leaf>() -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 6  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 4  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 4  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 4
}
Sat witness: Yes: (() -> replace([e1, e2, leaf, leaf]), {
e1 -> b  ;  e2 -> a
})

-------------------------------------------
Step 9, which took 0.005291 s (model generation: 0.004831,  model checking: 0.000460):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6342, q_gen_6343, q_gen_6347},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6342
<a>() -> q_gen_6343
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6342) -> q_gen_6329
<b, leaf>() -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6347
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336},
Q_f={q_gen_6328},
Delta=
{
<leaf, leaf>() -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<a, leaf>() -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<b, a, leaf, leaf>() -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 6  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 4  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 4  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 4
}
Sat witness: Yes: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 10, which took 0.161327 s (model generation: 0.005060,  model checking: 0.156267):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6342, q_gen_6343, q_gen_6347},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6342
<a>() -> q_gen_6343
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6342) -> q_gen_6329
<b, leaf>() -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6347
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336},
Q_f={q_gen_6328},
Delta=
{
<leaf, leaf>() -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<a, leaf>() -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<b, a, leaf, leaf>() -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 6  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 4  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 4  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 7
}
Sat witness: Yes: ((replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]), {
_cfa -> leaf  ;  _dfa -> leaf  ;  e2 -> a  ;  e3 -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 11, which took 0.436881 s (model generation: 0.006103,  model checking: 0.430778):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6342, q_gen_6343, q_gen_6347},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6342
<a>() -> q_gen_6343
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6342) -> q_gen_6329
<b, leaf>() -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6347
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336},
Q_f={q_gen_6328},
Delta=
{
<leaf, leaf>() -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<a, leaf>() -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 6  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 4  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 7  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 7
}
Sat witness: Yes: ((replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]), {
_efa -> node(a, leaf, leaf)  ;  _ffa -> leaf  ;  e1 -> b  ;  e2 -> b  ;  e3 -> a  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 12, which took 0.015992 s (model generation: 0.006751,  model checking: 0.009241):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6342, q_gen_6343, q_gen_6347},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6342
<a>() -> q_gen_6343
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6342) -> q_gen_6329
<b, leaf>() -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6347
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6356, q_gen_6357},
Q_f={q_gen_6328},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<a, leaf>() -> q_gen_6335
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 6  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 5  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 7  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 7
}
Sat witness: Yes: ((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(a, node(b, leaf, leaf), node(b, leaf, leaf))
})

-------------------------------------------
Step 13, which took 0.008602 s (model generation: 0.006726,  model checking: 0.001876):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6342, q_gen_6343, q_gen_6347},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6330
<b>() -> q_gen_6331
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6342, q_gen_6342) -> q_gen_6342
<a>() -> q_gen_6343
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6330) -> q_gen_6329
<b, leaf>() -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6342, q_gen_6342) -> q_gen_6347
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6356, q_gen_6357},
Q_f={q_gen_6328},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<a, leaf>() -> q_gen_6335
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 6  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 6  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 7  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 7
}
Sat witness: Yes: ((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 14, which took 0.008594 s (model generation: 0.007170,  model checking: 0.001424):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6341, q_gen_6343, q_gen_6345},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6330
<b>() -> q_gen_6331
<a>() -> q_gen_6343
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6345
<node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6345
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, leaf>() -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6341
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6356, q_gen_6357},
Q_f={q_gen_6328},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<a, leaf>() -> q_gen_6335
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 7  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 7  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 7
}
Sat witness: Yes: ((member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> a  ;  e2 -> b  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 15, which took 0.020511 s (model generation: 0.007790,  model checking: 0.012721):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6341, q_gen_6343, q_gen_6345},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6330
<b>() -> q_gen_6331
<a>() -> q_gen_6343
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6345
<node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6345
<a, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, leaf>() -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6341
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6356, q_gen_6357},
Q_f={q_gen_6328},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<a, leaf>() -> q_gen_6335
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 9  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 7  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 7  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 7
}
Sat witness: Yes: (() -> replace([e1, e2, leaf, leaf]), {
e1 -> a  ;  e2 -> b
})

-------------------------------------------
Step 16, which took 0.007867 s (model generation: 0.007287,  model checking: 0.000580):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6341, q_gen_6343, q_gen_6345},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6330
<b>() -> q_gen_6331
<a>() -> q_gen_6343
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6345
<node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6345
<a, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, leaf>() -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6341
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6356, q_gen_6357},
Q_f={q_gen_6328},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<a, leaf>() -> q_gen_6335
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<a, b, leaf, leaf>() -> q_gen_6328
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 9  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 7  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 7  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 7
}
Sat witness: Yes: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 17, which took 0.296570 s (model generation: 0.009004,  model checking: 0.287566):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6341, q_gen_6343, q_gen_6345},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6330
<b>() -> q_gen_6331
<a>() -> q_gen_6343
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6345
<node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6345
<a, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, leaf>() -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6341
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6356, q_gen_6357},
Q_f={q_gen_6328},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<a, leaf>() -> q_gen_6335
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<a, b, leaf, leaf>() -> q_gen_6328
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 9  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 7  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 7  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 10
}
Sat witness: Yes: ((replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]), {
_cfa -> leaf  ;  _dfa -> leaf  ;  e2 -> b  ;  e3 -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 18, which took 0.413528 s (model generation: 0.009018,  model checking: 0.404510):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6341, q_gen_6343, q_gen_6345},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6330
<b>() -> q_gen_6331
<a>() -> q_gen_6343
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6345
<node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6345
<a, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, leaf>() -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6341
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6356, q_gen_6357},
Q_f={q_gen_6328},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<a, leaf>() -> q_gen_6335
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<b, leaf>() -> q_gen_6335
<a, a>() -> q_gen_6336
<a, b>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<a, b, leaf, leaf>() -> q_gen_6328
<a, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 9  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 7  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 10  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 10
}
Sat witness: Yes: ((replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]), {
_efa -> node(a, leaf, leaf)  ;  _ffa -> leaf  ;  e1 -> a  ;  e2 -> b  ;  e3 -> b  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 19, which took 0.012159 s (model generation: 0.009820,  model checking: 0.002339):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6341, q_gen_6343, q_gen_6345},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6330
<b>() -> q_gen_6331
<a>() -> q_gen_6343
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6345
<node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6345
<a, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, leaf>() -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6341
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6356, q_gen_6357},
Q_f={q_gen_6328},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<node, b>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<a, leaf>() -> q_gen_6335
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<b, leaf>() -> q_gen_6335
<b, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<a, a>() -> q_gen_6336
<a, b>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<a, b, leaf, leaf>() -> q_gen_6328
<a, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 9  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 10  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 10  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 10
}
Sat witness: Yes: ((member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT, {
_lfa -> node(b, leaf, leaf)  ;  t1 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 20, which took 0.051889 s (model generation: 0.009763,  model checking: 0.042126):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6342, q_gen_6343, q_gen_6345, q_gen_6347},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6342
<node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6342
<a>() -> q_gen_6343
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6345
<a, node>(q_gen_6331, q_gen_6342, q_gen_6330) -> q_gen_6329
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6330) -> q_gen_6329
<a, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6347
<b, leaf>() -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6342, q_gen_6330) -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6342, q_gen_6342) -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6347
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6356, q_gen_6357},
Q_f={q_gen_6328},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<node, b>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<a, leaf>() -> q_gen_6335
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<b, leaf>() -> q_gen_6335
<b, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<a, a>() -> q_gen_6336
<a, b>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<a, b, leaf, leaf>() -> q_gen_6328
<a, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 9  ;  (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  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 10  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 10  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 10
}
Sat witness: Yes: ((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(a, leaf, node(a, node(b, leaf, leaf), node(b, leaf, leaf)))
})

-------------------------------------------
Step 21, which took 0.027632 s (model generation: 0.011301,  model checking: 0.016331):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6342, q_gen_6343, q_gen_6345, q_gen_6347},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6330
<b>() -> q_gen_6331
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6342
<a>() -> q_gen_6343
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6345
<a, node>(q_gen_6331, q_gen_6342, q_gen_6330) -> q_gen_6329
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6330) -> q_gen_6329
<a, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6347
<b, leaf>() -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6342, q_gen_6330) -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6342, q_gen_6342) -> q_gen_6347
<b, node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6347
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6356, q_gen_6357},
Q_f={q_gen_6328},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<node, b>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<a, leaf>() -> q_gen_6335
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<b, leaf>() -> q_gen_6335
<b, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<a, a>() -> q_gen_6336
<a, b>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<a, b, leaf, leaf>() -> q_gen_6328
<a, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 9  ;  (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]) -> 11  ;  (member([e, leaf])) -> BOT -> 9  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 10  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 10  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 10
}
Sat witness: Yes: ((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 -> node(a, leaf, leaf)
})

-------------------------------------------
Step 22, which took 0.012117 s (model generation: 0.011174,  model checking: 0.000943):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6341, q_gen_6342, q_gen_6343, q_gen_6345},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6342
<node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6342
<a>() -> q_gen_6343
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6345
<a, node>(q_gen_6331, q_gen_6342, q_gen_6330) -> q_gen_6329
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6330) -> q_gen_6329
<a, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6341
<b, leaf>() -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6342, q_gen_6330) -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6342, q_gen_6342) -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6341
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6356, q_gen_6357},
Q_f={q_gen_6328},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<node, b>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<a, leaf>() -> q_gen_6335
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<b, leaf>() -> q_gen_6335
<b, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<a, a>() -> q_gen_6336
<a, b>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<a, b, leaf, leaf>() -> q_gen_6328
<a, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 9  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 12  ;  (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]) -> 11  ;  (member([e, leaf])) -> BOT -> 10  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 10  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 10  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 10
}
Sat witness: Yes: ((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 23, which took 0.028763 s (model generation: 0.013665,  model checking: 0.015098):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6341, q_gen_6342, q_gen_6343, q_gen_6345},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6342
<a>() -> q_gen_6343
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6345
<node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6345
<a, node>(q_gen_6331, q_gen_6342, q_gen_6330) -> q_gen_6329
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6342) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6329
<a, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6341
<b, leaf>() -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6342, q_gen_6330) -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6342, q_gen_6345) -> q_gen_6341
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6356, q_gen_6357},
Q_f={q_gen_6328},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<node, b>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<a, leaf>() -> q_gen_6335
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<b, leaf>() -> q_gen_6335
<b, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<a, a>() -> q_gen_6336
<a, b>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<a, b, leaf, leaf>() -> q_gen_6328
<a, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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  ;  () -> replace([e1, e2, leaf, leaf]) -> 12  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 12  ;  (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]) -> 11  ;  (member([e, leaf])) -> BOT -> 10  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 10  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 10  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 10
}
Sat witness: Yes: (() -> replace([e1, e2, leaf, leaf]), {
e1 -> a  ;  e2 -> a
})

-------------------------------------------
Step 24, which took 0.013405 s (model generation: 0.011782,  model checking: 0.001623):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6341, q_gen_6342, q_gen_6343, q_gen_6345},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6342
<a>() -> q_gen_6343
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6345
<node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6345
<a, node>(q_gen_6331, q_gen_6342, q_gen_6330) -> q_gen_6329
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6342) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6329
<a, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6341
<b, leaf>() -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6342, q_gen_6330) -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6342, q_gen_6345) -> q_gen_6341
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6356, q_gen_6357},
Q_f={q_gen_6328},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<node, b>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<a, leaf>() -> q_gen_6335
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<b, leaf>() -> q_gen_6335
<b, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<a, a>() -> q_gen_6336
<a, b>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<a, a, leaf, leaf>() -> q_gen_6328
<a, b, leaf, leaf>() -> q_gen_6328
<a, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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)]) -> 12  ;  () -> replace([e1, e2, leaf, leaf]) -> 12  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 12  ;  (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]) -> 11  ;  (member([e, leaf])) -> BOT -> 10  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 10  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 10  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 10
}
Sat witness: Yes: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 25, which took 0.236962 s (model generation: 0.020745,  model checking: 0.216217):

Model:
|_
{
member -> 
{{{
Q={q_gen_6329, q_gen_6330, q_gen_6331, q_gen_6341, q_gen_6342, q_gen_6343, q_gen_6345},
Q_f={q_gen_6329},
Delta=
{
<leaf>() -> q_gen_6330
<b>() -> q_gen_6331
<node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6342
<node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6342
<a>() -> q_gen_6343
<node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6345
<node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6345
<a, node>(q_gen_6331, q_gen_6342, q_gen_6330) -> q_gen_6329
<a, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6345, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6331, q_gen_6345, q_gen_6345) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6342, q_gen_6342) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6330) -> q_gen_6329
<b, node>(q_gen_6343, q_gen_6345, q_gen_6345) -> q_gen_6329
<a, node>(q_gen_6331, q_gen_6330, q_gen_6330) -> q_gen_6341
<b, leaf>() -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6330, q_gen_6330) -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6330, q_gen_6342) -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6342, q_gen_6330) -> q_gen_6341
<b, node>(q_gen_6343, q_gen_6342, q_gen_6345) -> q_gen_6341
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  replace -> 
{{{
Q={q_gen_6328, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6356, q_gen_6357},
Q_f={q_gen_6328},
Delta=
{
<leaf>() -> q_gen_6356
<a>() -> q_gen_6357
<leaf, leaf>() -> q_gen_6333
<leaf, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, leaf>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6333
<node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6333
<leaf, a>() -> q_gen_6334
<leaf, b>() -> q_gen_6334
<node, a>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<node, b>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6334
<a, leaf>() -> q_gen_6335
<a, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<b, leaf>() -> q_gen_6335
<b, node>(q_gen_6357, q_gen_6356, q_gen_6356) -> q_gen_6335
<a, a>() -> q_gen_6336
<a, b>() -> q_gen_6336
<b, a>() -> q_gen_6336
<b, b>() -> q_gen_6336
<a, a, leaf, leaf>() -> q_gen_6328
<a, b, leaf, leaf>() -> q_gen_6328
<a, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, a, leaf, leaf>() -> q_gen_6328
<b, a, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
<b, b, leaf, leaf>() -> q_gen_6328
<b, b, node, node>(q_gen_6336, q_gen_6335, q_gen_6335, q_gen_6334, q_gen_6333, q_gen_6333, q_gen_6334, q_gen_6333, q_gen_6333) -> q_gen_6328
}

Datatype: <elt, elt, elt_bin_tree, elt_bin_tree>
Convolution form: complete
}}}

}
--
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)]) -> 12  ;  () -> replace([e1, e2, leaf, leaf]) -> 12  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 12  ;  (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]) -> 11  ;  (member([e, leaf])) -> BOT -> 10  ;  (member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT -> 10  ;  (replace([e1, e2, t1, _efa]) /\ replace([e1, e2, t2, _ffa]) /\ not eq_elt([e1, e3])) -> replace([e1, e2, node(e3, t1, t2), node(e3, _efa, _ffa)]) -> 10  ;  (replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 13
}
Sat witness: Yes: ((replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]), {
_cfa -> leaf  ;  _dfa -> leaf  ;  e2 -> a  ;  e3 -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

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