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


Learning problem is:

env: {
elt -> {a, b}  ;  elt_bin_tree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(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 60.001406 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095, q_gen_6101, q_gen_6102, q_gen_6103, q_gen_6104, q_gen_6105, q_gen_6106, q_gen_6107, q_gen_6108, q_gen_6109, q_gen_6110, q_gen_6111, q_gen_6112, q_gen_6114, q_gen_6120, q_gen_6121, q_gen_6122, q_gen_6123, q_gen_6125},
Q_f={},
Delta=
{
<leaf>() -> q_gen_6094
<b>() -> q_gen_6095
<node>(q_gen_6095, q_gen_6094, q_gen_6103) -> q_gen_6102
<node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6103
<a>() -> q_gen_6104
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6106
<node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6107
<node>(q_gen_6104, q_gen_6106, q_gen_6106) -> q_gen_6112
<node>(q_gen_6104, q_gen_6106, q_gen_6094) -> q_gen_6122
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6101
<b, node>(q_gen_6104, q_gen_6107, q_gen_6106) -> q_gen_6105
<b, leaf>() -> q_gen_6108
<b, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6109
<b, node>(q_gen_6104, q_gen_6106, q_gen_6106) -> q_gen_6110
<b, node>(q_gen_6104, q_gen_6112, q_gen_6094) -> q_gen_6111
<a, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6114
<b, node>(q_gen_6104, q_gen_6106, q_gen_6094) -> q_gen_6120
<b, node>(q_gen_6104, q_gen_6103, q_gen_6122) -> q_gen_6121
<b, node>(q_gen_6104, q_gen_6103, q_gen_6094) -> q_gen_6123
<b, node>(q_gen_6095, q_gen_6106, q_gen_6106) -> q_gen_6125
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6096, q_gen_6097, q_gen_6098, q_gen_6099, q_gen_6100, q_gen_6113, q_gen_6115, q_gen_6116, q_gen_6117, q_gen_6118, q_gen_6119, q_gen_6124, q_gen_6126, q_gen_6127, q_gen_6128},
Q_f={},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<b, b>() -> q_gen_6098
<a, a>() -> q_gen_6100
<b, a>() -> q_gen_6116
<node, node>(q_gen_6100, q_gen_6097, q_gen_6097) -> q_gen_6119
<a, b>() -> q_gen_6127
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6096
<b, b, node, node>(q_gen_6100, q_gen_6097, q_gen_6097) -> q_gen_6099
<b, a, leaf, leaf>() -> q_gen_6113
<b, a, node, node>(q_gen_6116, q_gen_6097, q_gen_6097) -> q_gen_6115
<b, a, node, node>(q_gen_6100, q_gen_6097, q_gen_6097) -> q_gen_6117
<b, a, node, node>(q_gen_6100, q_gen_6119, q_gen_6097) -> q_gen_6118
<a, b, leaf, leaf>() -> q_gen_6124
<a, b, node, node>(q_gen_6127, q_gen_6097, q_gen_6097) -> q_gen_6126
<a, b, node, node>(q_gen_6116, q_gen_6097, q_gen_6097) -> q_gen_6128
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006010 s (model generation: 0.005254,  model checking: 0.000756):

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 0
() -> 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: Found: (() -> replace([e1, e2, leaf, leaf]), {
e1 -> b  ;  e2 -> b
})

-------------------------------------------
Step 1, which took 0.004126 s (model generation: 0.004009,  model checking: 0.000117):

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> 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: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 2, which took 0.004960 s (model generation: 0.004605,  model checking: 0.000355):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<b>() -> q_gen_6095
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
}

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

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> 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: Found: ((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.005371 s (model generation: 0.004501,  model checking: 0.000870):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<b>() -> q_gen_6095
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<b, b>() -> q_gen_6098
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> 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: Found: ((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.082723 s (model generation: 0.004778,  model checking: 0.077945):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<b>() -> q_gen_6095
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<a, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> 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: Found: ((not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(a, node(b, leaf, node(a, leaf, leaf)), leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 5, which took 0.006971 s (model generation: 0.006345,  model checking: 0.000626):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6094
<a>() -> q_gen_6095
<b>() -> q_gen_6095
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<a, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> 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: 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 6, which took 0.006457 s (model generation: 0.006194,  model checking: 0.000263):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6094
<a>() -> q_gen_6095
<b>() -> q_gen_6095
<b, leaf>() -> q_gen_6093
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<a, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> 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: Found: ((member([e, leaf])) -> BOT, {
e -> b
})

-------------------------------------------
Step 7, which took 0.014940 s (model generation: 0.005871,  model checking: 0.009069):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095, q_gen_6102, q_gen_6104, q_gen_6108},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<b>() -> q_gen_6095
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6095, q_gen_6094, q_gen_6102) -> q_gen_6102
<node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6102
<a>() -> q_gen_6104
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6102) -> q_gen_6093
<b, leaf>() -> q_gen_6108
<b, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6108
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<a, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> 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: 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 8, which took 0.007558 s (model generation: 0.007264,  model checking: 0.000294):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095, q_gen_6102, q_gen_6104, q_gen_6108},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6094
<b>() -> q_gen_6095
<node>(q_gen_6095, q_gen_6094, q_gen_6102) -> q_gen_6102
<node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6102
<a>() -> q_gen_6104
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6093
<b, leaf>() -> q_gen_6108
<b, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6108
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<a, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> 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: Found: (() -> replace([e1, e2, leaf, leaf]), {
e1 -> b  ;  e2 -> a
})

-------------------------------------------
Step 9, which took 0.011009 s (model generation: 0.009979,  model checking: 0.001030):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095, q_gen_6102, q_gen_6104, q_gen_6108},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6094
<b>() -> q_gen_6095
<node>(q_gen_6095, q_gen_6094, q_gen_6102) -> q_gen_6102
<node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6102
<a>() -> q_gen_6104
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6093
<b, leaf>() -> q_gen_6108
<b, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6108
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<a, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<b, a, leaf, leaf>() -> q_gen_6092
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> 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: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 10, which took 0.010800 s (model generation: 0.009995,  model checking: 0.000805):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095, q_gen_6102, q_gen_6104, q_gen_6108},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6094
<b>() -> q_gen_6095
<node>(q_gen_6095, q_gen_6094, q_gen_6102) -> q_gen_6102
<node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6102
<a>() -> q_gen_6104
<a, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6093
<b, leaf>() -> q_gen_6108
<b, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6108
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<a, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<b, a, leaf, leaf>() -> q_gen_6092
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> 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: Found: ((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.013277 s (model generation: 0.011546,  model checking: 0.001731):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095, q_gen_6102, q_gen_6104, q_gen_6108},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6094
<b>() -> q_gen_6095
<node>(q_gen_6095, q_gen_6094, q_gen_6102) -> q_gen_6102
<node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6102
<a>() -> q_gen_6104
<a, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6093
<b, leaf>() -> q_gen_6108
<b, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6108
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<a, a>() -> q_gen_6098
<b, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<b, a, leaf, leaf>() -> q_gen_6092
<b, a, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> 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: Found: ((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 -> a  ;  e3 -> a  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 12, which took 0.057668 s (model generation: 0.014346,  model checking: 0.043322):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095, q_gen_6102, q_gen_6104, q_gen_6105},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<b>() -> q_gen_6095
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6095, q_gen_6094, q_gen_6102) -> q_gen_6102
<node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6102) -> q_gen_6102
<a>() -> q_gen_6104
<a, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6093
<b, leaf>() -> q_gen_6105
<b, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6105
<b, node>(q_gen_6104, q_gen_6102, q_gen_6102) -> q_gen_6105
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6097
<a, a>() -> q_gen_6098
<b, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<b, a, leaf, leaf>() -> q_gen_6092
<b, a, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> 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: 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(a, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 13, which took 0.026452 s (model generation: 0.023299,  model checking: 0.003153):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095, q_gen_6102, q_gen_6104, q_gen_6108},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6094
<b>() -> q_gen_6095
<node>(q_gen_6095, q_gen_6094, q_gen_6102) -> q_gen_6102
<node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6102
<a>() -> q_gen_6104
<a, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6102) -> q_gen_6093
<b, leaf>() -> q_gen_6108
<b, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6108
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6097
<a, a>() -> q_gen_6098
<b, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<b, a, leaf, leaf>() -> q_gen_6092
<b, a, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> 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: 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 14, which took 0.027535 s (model generation: 0.024085,  model checking: 0.003450):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095, q_gen_6101, q_gen_6102, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6094
<b>() -> q_gen_6095
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6095, q_gen_6094, q_gen_6102) -> q_gen_6102
<node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6102) -> q_gen_6102
<a>() -> q_gen_6104
<a, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6094, q_gen_6102) -> q_gen_6093
<b, leaf>() -> q_gen_6101
<b, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6101
<b, node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6101
<b, node>(q_gen_6104, q_gen_6102, q_gen_6102) -> q_gen_6101
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6097
<a, a>() -> q_gen_6098
<b, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<b, a, leaf, leaf>() -> q_gen_6092
<b, a, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> 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: Found: ((member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 15, which took 0.026013 s (model generation: 0.025226,  model checking: 0.000787):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095, q_gen_6102, q_gen_6104, q_gen_6108},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6094
<b>() -> q_gen_6095
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6102) -> q_gen_6102
<a>() -> q_gen_6104
<a, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6094, q_gen_6102) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6102) -> q_gen_6093
<b, leaf>() -> q_gen_6108
<b, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6108
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6097
<a, a>() -> q_gen_6098
<b, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<b, a, leaf, leaf>() -> q_gen_6092
<b, a, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> 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: Found: (() -> replace([e1, e2, leaf, leaf]), {
e1 -> a  ;  e2 -> b
})

-------------------------------------------
Step 16, which took 0.026030 s (model generation: 0.024458,  model checking: 0.001572):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095, q_gen_6102, q_gen_6104, q_gen_6108},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6094
<b>() -> q_gen_6095
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6102) -> q_gen_6102
<a>() -> q_gen_6104
<a, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6094, q_gen_6102) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6102) -> q_gen_6093
<b, leaf>() -> q_gen_6108
<b, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6108
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6097
<a, a>() -> q_gen_6098
<b, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<a, b, leaf, leaf>() -> q_gen_6092
<b, a, leaf, leaf>() -> q_gen_6092
<b, a, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 9
() -> 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: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 17, which took 0.028873 s (model generation: 0.025304,  model checking: 0.003569):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095, q_gen_6102, q_gen_6104, q_gen_6108},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6094
<b>() -> q_gen_6095
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6102) -> q_gen_6102
<a>() -> q_gen_6104
<a, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6095, q_gen_6102, q_gen_6102) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6094, q_gen_6102) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6102) -> q_gen_6093
<b, leaf>() -> q_gen_6108
<b, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6108
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6097
<a, a>() -> q_gen_6098
<b, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<a, b, leaf, leaf>() -> q_gen_6092
<b, a, leaf, leaf>() -> q_gen_6092
<b, a, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 9
() -> 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: Found: ((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.032258 s (model generation: 0.026410,  model checking: 0.005848):

Model:
|_
{
member -> 
{{{
Q={q_gen_6093, q_gen_6094, q_gen_6095, q_gen_6102, q_gen_6104, q_gen_6105},
Q_f={q_gen_6093},
Delta=
{
<leaf>() -> q_gen_6094
<node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6094
<node>(q_gen_6104, q_gen_6102, q_gen_6102) -> q_gen_6094
<b>() -> q_gen_6095
<node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6102
<node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6102
<a>() -> q_gen_6104
<a, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6095, q_gen_6094, q_gen_6094) -> q_gen_6093
<b, node>(q_gen_6095, q_gen_6102, q_gen_6102) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6094, q_gen_6102) -> q_gen_6093
<b, node>(q_gen_6104, q_gen_6102, q_gen_6094) -> q_gen_6093
<b, leaf>() -> q_gen_6105
<b, node>(q_gen_6104, q_gen_6094, q_gen_6094) -> q_gen_6105
<b, node>(q_gen_6104, q_gen_6102, q_gen_6102) -> q_gen_6105
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  replace -> 
{{{
Q={q_gen_6092, q_gen_6097, q_gen_6098},
Q_f={q_gen_6092},
Delta=
{
<leaf, leaf>() -> q_gen_6097
<node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6097
<a, a>() -> q_gen_6098
<a, b>() -> q_gen_6098
<b, a>() -> q_gen_6098
<b, b>() -> q_gen_6098
<a, b, leaf, leaf>() -> q_gen_6092
<a, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
<b, a, leaf, leaf>() -> q_gen_6092
<b, a, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
<b, b, leaf, leaf>() -> q_gen_6092
<b, b, node, node>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6092
}

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

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

Teacher's answer:
New clause system:
{
() -> member([e2, node(e2, t1, t2)]) -> 9
() -> 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)]) -> 8
(replace([e3, e2, t1, _cfa]) /\ replace([e3, e2, t2, _dfa])) -> replace([e3, e2, node(e3, t1, t2), node(e2, _cfa, _dfa)]) -> 10
}
Sat witness: Found: ((member([a, _lfa]) /\ replace([a, b, t1, _lfa])) -> BOT, {
_lfa -> node(a, leaf, leaf)  ;  t1 -> node(b, leaf, leaf)
})

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