Solving ../../benchmarks/true/timbuk_memberTree.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:
{
(swap, F:
{() -> swap([leaf, leaf])
(swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)])}
(swap([_oh, _ph]) /\ swap([_oh, _qh])) -> eq_elt_bin_tree([_ph, _qh])
)
(member, P:
{() -> member([e2, node(e2, t1, t2)])
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)])
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)])
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2])
(member([e, leaf])) -> BOT}
)
}

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


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

Clause system for inference is:

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


Solving took 30.013467 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253, q_gen_6258, q_gen_6259, q_gen_6260, q_gen_6261, q_gen_6262, q_gen_6263, q_gen_6264, q_gen_6265, q_gen_6266, q_gen_6267, q_gen_6268, q_gen_6269, q_gen_6274, q_gen_6275, q_gen_6276, q_gen_6277, q_gen_6278, q_gen_6279, q_gen_6287, q_gen_6288, q_gen_6289},
Q_f={},
Delta=
{
<leaf>() -> q_gen_6252
<b>() -> q_gen_6253
<node>(q_gen_6253, q_gen_6252, q_gen_6260) -> q_gen_6259
<node>(q_gen_6262, q_gen_6252, q_gen_6261) -> q_gen_6260
<node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6261
<a>() -> q_gen_6262
<node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6264
<node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6265
<node>(q_gen_6262, q_gen_6264, q_gen_6264) -> q_gen_6278
<node>(q_gen_6253, q_gen_6264, q_gen_6264) -> q_gen_6289
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6258
<b, node>(q_gen_6262, q_gen_6265, q_gen_6264) -> q_gen_6263
<b, leaf>() -> q_gen_6266
<b, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6267
<b, node>(q_gen_6262, q_gen_6264, q_gen_6252) -> q_gen_6268
<a, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6269
<b, node>(q_gen_6262, q_gen_6252, q_gen_6264) -> q_gen_6274
<b, node>(q_gen_6262, q_gen_6261, q_gen_6252) -> q_gen_6275
<b, node>(q_gen_6262, q_gen_6264, q_gen_6264) -> q_gen_6276
<b, node>(q_gen_6262, q_gen_6278, q_gen_6264) -> q_gen_6277
<b, node>(q_gen_6253, q_gen_6264, q_gen_6252) -> q_gen_6279
<b, node>(q_gen_6253, q_gen_6264, q_gen_6264) -> q_gen_6287
<b, node>(q_gen_6262, q_gen_6261, q_gen_6289) -> q_gen_6288
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  swap -> 
{{{
Q={q_gen_6250, q_gen_6254, q_gen_6255, q_gen_6256, q_gen_6257, q_gen_6270, q_gen_6271, q_gen_6272, q_gen_6273, q_gen_6280, q_gen_6281, q_gen_6282, q_gen_6283, q_gen_6284, q_gen_6285, q_gen_6286},
Q_f={},
Delta=
{
<leaf>() -> q_gen_6282
<b>() -> q_gen_6283
<leaf, leaf>() -> q_gen_6250
<node, node>(q_gen_6257, q_gen_6256, q_gen_6256, q_gen_6255, q_gen_6250, q_gen_6250, q_gen_6255, q_gen_6250, q_gen_6250) -> q_gen_6254
<leaf, b>() -> q_gen_6255
<b, leaf>() -> q_gen_6256
<b, b>() -> q_gen_6257
<node, node>(q_gen_6273, q_gen_6272, q_gen_6272, q_gen_6271, q_gen_6250, q_gen_6250, q_gen_6271, q_gen_6250, q_gen_6250) -> q_gen_6270
<leaf, a>() -> q_gen_6271
<a, leaf>() -> q_gen_6272
<a, a>() -> q_gen_6273
<node, node>(q_gen_6257, q_gen_6286, q_gen_6256, q_gen_6255, q_gen_6285, q_gen_6250, q_gen_6284, q_gen_6254, q_gen_6281) -> q_gen_6280
<node, leaf>(q_gen_6283, q_gen_6282, q_gen_6282) -> q_gen_6281
<node, b>(q_gen_6283, q_gen_6282, q_gen_6282) -> q_gen_6284
<leaf, node>(q_gen_6283, q_gen_6282, q_gen_6282) -> q_gen_6285
<b, node>(q_gen_6283, q_gen_6282, q_gen_6282) -> q_gen_6286
}

Datatype: <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.003448 s (model generation: 0.003240,  model checking: 0.000208):

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

}

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

}

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 3  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 1  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 1  ;  (member([e, leaf])) -> BOT -> 1  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 1
}
Sat witness: Yes: (() -> swap([leaf, leaf]), {

})

-------------------------------------------
Step 1, which took 0.003472 s (model generation: 0.003415,  model checking: 0.000057):

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

}

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

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 3  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 1  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 1  ;  (member([e, leaf])) -> BOT -> 1  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 1
}
Sat witness: Yes: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 2, which took 0.003609 s (model generation: 0.003304,  model checking: 0.000305):

Model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253},
Q_f={q_gen_6251},
Delta=
{
<leaf>() -> q_gen_6252
<b>() -> q_gen_6253
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
}

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

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 3  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 1  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 1  ;  (member([e, leaf])) -> BOT -> 1  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 4
}
Sat witness: Yes: ((swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]), {
_mh -> leaf  ;  _nh -> leaf  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 3, which took 0.073865 s (model generation: 0.004144,  model checking: 0.069721):

Model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253},
Q_f={q_gen_6251},
Delta=
{
<leaf>() -> q_gen_6252
<b>() -> q_gen_6253
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  swap -> 
{{{
Q={q_gen_6250, q_gen_6255, q_gen_6256, q_gen_6257},
Q_f={q_gen_6250},
Delta=
{
<leaf, leaf>() -> q_gen_6250
<node, node>(q_gen_6257, q_gen_6256, q_gen_6256, q_gen_6255, q_gen_6250, q_gen_6250, q_gen_6255, q_gen_6250, q_gen_6250) -> q_gen_6250
<leaf, b>() -> q_gen_6255
<b, leaf>() -> q_gen_6256
<b, b>() -> q_gen_6257
}

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 3  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 1  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 2  ;  (member([e, leaf])) -> BOT -> 2  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 4
}
Sat witness: 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(b, node(b, leaf, node(a, leaf, node(a, leaf, leaf))), node(b, leaf, node(a, leaf, node(a, leaf, leaf))))  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 4, which took 0.005441 s (model generation: 0.005213,  model checking: 0.000228):

Model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253},
Q_f={q_gen_6251},
Delta=
{
<leaf>() -> q_gen_6252
<node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6252
<a>() -> q_gen_6253
<b>() -> q_gen_6253
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  swap -> 
{{{
Q={q_gen_6250, q_gen_6255, q_gen_6256, q_gen_6257},
Q_f={q_gen_6250},
Delta=
{
<leaf, leaf>() -> q_gen_6250
<node, node>(q_gen_6257, q_gen_6256, q_gen_6256, q_gen_6255, q_gen_6250, q_gen_6250, q_gen_6255, q_gen_6250, q_gen_6250) -> q_gen_6250
<leaf, b>() -> q_gen_6255
<b, leaf>() -> q_gen_6256
<b, b>() -> q_gen_6257
}

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 3  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 2  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 2  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5  ;  (member([e, leaf])) -> BOT -> 3  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 4
}
Sat witness: 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 5, which took 0.005017 s (model generation: 0.004909,  model checking: 0.000108):

Model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253},
Q_f={q_gen_6251},
Delta=
{
<leaf>() -> q_gen_6252
<node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6252
<a>() -> q_gen_6253
<b>() -> q_gen_6253
<b, leaf>() -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  swap -> 
{{{
Q={q_gen_6250, q_gen_6255, q_gen_6256, q_gen_6257},
Q_f={q_gen_6250},
Delta=
{
<leaf, leaf>() -> q_gen_6250
<node, node>(q_gen_6257, q_gen_6256, q_gen_6256, q_gen_6255, q_gen_6250, q_gen_6250, q_gen_6255, q_gen_6250, q_gen_6250) -> q_gen_6250
<leaf, b>() -> q_gen_6255
<b, leaf>() -> q_gen_6256
<b, b>() -> q_gen_6257
}

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 3  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 3  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 3  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5  ;  (member([e, leaf])) -> BOT -> 6  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 4
}
Sat witness: Yes: ((member([e, leaf])) -> BOT, {
e -> b
})

-------------------------------------------
Step 6, which took 0.005005 s (model generation: 0.004640,  model checking: 0.000365):

Model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253, q_gen_6262, q_gen_6263},
Q_f={q_gen_6251},
Delta=
{
<leaf>() -> q_gen_6252
<node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6252
<node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6252
<b>() -> q_gen_6253
<a>() -> q_gen_6262
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, leaf>() -> q_gen_6263
<b, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6263
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  swap -> 
{{{
Q={q_gen_6250, q_gen_6255, q_gen_6256, q_gen_6257},
Q_f={q_gen_6250},
Delta=
{
<leaf, leaf>() -> q_gen_6250
<node, node>(q_gen_6257, q_gen_6256, q_gen_6256, q_gen_6255, q_gen_6250, q_gen_6250, q_gen_6255, q_gen_6250, q_gen_6250) -> q_gen_6250
<leaf, b>() -> q_gen_6255
<b, leaf>() -> q_gen_6256
<b, b>() -> q_gen_6257
}

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 3  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 3  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5  ;  (member([e, leaf])) -> BOT -> 6  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 4
}
Sat witness: 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 7, which took 0.018707 s (model generation: 0.004820,  model checking: 0.013887):

Model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253, q_gen_6259, q_gen_6262, q_gen_6266},
Q_f={q_gen_6251},
Delta=
{
<leaf>() -> q_gen_6252
<b>() -> q_gen_6253
<node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6259
<node>(q_gen_6253, q_gen_6252, q_gen_6259) -> q_gen_6259
<node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6259
<node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6259
<node>(q_gen_6262, q_gen_6252, q_gen_6259) -> q_gen_6259
<a>() -> q_gen_6262
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, leaf>() -> q_gen_6266
<b, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6266
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  swap -> 
{{{
Q={q_gen_6250, q_gen_6255, q_gen_6256, q_gen_6257},
Q_f={q_gen_6250},
Delta=
{
<leaf, leaf>() -> q_gen_6250
<node, node>(q_gen_6257, q_gen_6256, q_gen_6256, q_gen_6255, q_gen_6250, q_gen_6250, q_gen_6255, q_gen_6250, q_gen_6250) -> q_gen_6250
<leaf, b>() -> q_gen_6255
<b, leaf>() -> q_gen_6256
<b, b>() -> q_gen_6257
}

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 4  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 4  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5  ;  (member([e, leaf])) -> BOT -> 6  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 4
}
Sat witness: Yes: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 8, which took 0.125327 s (model generation: 0.004979,  model checking: 0.120348):

Model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253, q_gen_6259, q_gen_6262, q_gen_6266},
Q_f={q_gen_6251},
Delta=
{
<leaf>() -> q_gen_6252
<b>() -> q_gen_6253
<node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6259
<node>(q_gen_6253, q_gen_6252, q_gen_6259) -> q_gen_6259
<node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6259
<node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6259
<node>(q_gen_6262, q_gen_6252, q_gen_6259) -> q_gen_6259
<a>() -> q_gen_6262
<a, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, leaf>() -> q_gen_6266
<b, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6266
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  swap -> 
{{{
Q={q_gen_6250, q_gen_6255, q_gen_6256, q_gen_6257},
Q_f={q_gen_6250},
Delta=
{
<leaf, leaf>() -> q_gen_6250
<node, node>(q_gen_6257, q_gen_6256, q_gen_6256, q_gen_6255, q_gen_6250, q_gen_6250, q_gen_6255, q_gen_6250, q_gen_6250) -> q_gen_6250
<leaf, b>() -> q_gen_6255
<b, leaf>() -> q_gen_6256
<b, b>() -> q_gen_6257
}

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 4  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 4  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5  ;  (member([e, leaf])) -> BOT -> 6  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 7
}
Sat witness: Yes: ((swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]), {
_mh -> leaf  ;  _nh -> leaf  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 9, which took 0.016807 s (model generation: 0.006052,  model checking: 0.010755):

Model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253, q_gen_6259, q_gen_6262, q_gen_6266},
Q_f={q_gen_6251},
Delta=
{
<leaf>() -> q_gen_6252
<b>() -> q_gen_6253
<node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6259
<node>(q_gen_6253, q_gen_6252, q_gen_6259) -> q_gen_6259
<node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6259
<node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6259
<node>(q_gen_6262, q_gen_6252, q_gen_6259) -> q_gen_6259
<a>() -> q_gen_6262
<a, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, leaf>() -> q_gen_6266
<b, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6266
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  swap -> 
{{{
Q={q_gen_6250, q_gen_6255, q_gen_6256, q_gen_6257},
Q_f={q_gen_6250},
Delta=
{
<leaf, leaf>() -> q_gen_6250
<node, node>(q_gen_6257, q_gen_6256, q_gen_6256, q_gen_6255, q_gen_6250, q_gen_6250, q_gen_6255, q_gen_6250, q_gen_6250) -> q_gen_6250
<leaf, a>() -> q_gen_6255
<leaf, b>() -> q_gen_6255
<a, leaf>() -> q_gen_6256
<b, leaf>() -> q_gen_6256
<a, a>() -> q_gen_6257
<b, b>() -> q_gen_6257
}

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 4  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 4  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5  ;  (member([e, leaf])) -> BOT -> 6  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 7
}
Sat witness: Yes: ((not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 10, which took 0.027111 s (model generation: 0.005863,  model checking: 0.021248):

Model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253, q_gen_6259, q_gen_6262, q_gen_6266},
Q_f={q_gen_6251},
Delta=
{
<leaf>() -> q_gen_6252
<b>() -> q_gen_6253
<node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6259
<node>(q_gen_6253, q_gen_6252, q_gen_6259) -> q_gen_6259
<node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6259
<node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6259
<node>(q_gen_6262, q_gen_6252, q_gen_6259) -> q_gen_6259
<a>() -> q_gen_6262
<a, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6252, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, leaf>() -> q_gen_6266
<b, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6266
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  swap -> 
{{{
Q={q_gen_6250, q_gen_6255, q_gen_6256, q_gen_6257},
Q_f={q_gen_6250},
Delta=
{
<leaf, leaf>() -> q_gen_6250
<node, node>(q_gen_6257, q_gen_6256, q_gen_6256, q_gen_6255, q_gen_6250, q_gen_6250, q_gen_6255, q_gen_6250, q_gen_6250) -> q_gen_6250
<leaf, a>() -> q_gen_6255
<leaf, b>() -> q_gen_6255
<a, leaf>() -> q_gen_6256
<b, leaf>() -> q_gen_6256
<a, a>() -> q_gen_6257
<b, b>() -> q_gen_6257
}

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 5  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 5  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8  ;  (member([e, leaf])) -> BOT -> 6  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 7
}
Sat witness: 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 11, which took 0.041372 s (model generation: 0.006056,  model checking: 0.035316):

Model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253, q_gen_6259, q_gen_6262, q_gen_6266},
Q_f={q_gen_6251},
Delta=
{
<leaf>() -> q_gen_6252
<node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6252
<b>() -> q_gen_6253
<node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6259
<node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6259
<a>() -> q_gen_6262
<a, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6252, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, leaf>() -> q_gen_6266
<b, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6266
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  swap -> 
{{{
Q={q_gen_6250, q_gen_6255, q_gen_6256, q_gen_6257},
Q_f={q_gen_6250},
Delta=
{
<leaf, leaf>() -> q_gen_6250
<node, node>(q_gen_6257, q_gen_6256, q_gen_6256, q_gen_6255, q_gen_6250, q_gen_6250, q_gen_6255, q_gen_6250, q_gen_6250) -> q_gen_6250
<leaf, a>() -> q_gen_6255
<leaf, b>() -> q_gen_6255
<a, leaf>() -> q_gen_6256
<b, leaf>() -> q_gen_6256
<a, a>() -> q_gen_6257
<b, b>() -> q_gen_6257
}

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 6  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 6  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8  ;  (member([e, leaf])) -> BOT -> 7  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 7
}
Sat witness: Yes: ((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 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 12, which took 0.063873 s (model generation: 0.007191,  model checking: 0.056682):

Model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253, q_gen_6259, q_gen_6262, q_gen_6266},
Q_f={q_gen_6251},
Delta=
{
<leaf>() -> q_gen_6252
<node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6252
<node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6252
<node>(q_gen_6262, q_gen_6259, q_gen_6259) -> q_gen_6252
<b>() -> q_gen_6253
<node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6259
<a>() -> q_gen_6262
<a, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6252, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, leaf>() -> q_gen_6266
<b, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6266
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  swap -> 
{{{
Q={q_gen_6250, q_gen_6255, q_gen_6256, q_gen_6257},
Q_f={q_gen_6250},
Delta=
{
<leaf, leaf>() -> q_gen_6250
<node, node>(q_gen_6257, q_gen_6256, q_gen_6256, q_gen_6255, q_gen_6250, q_gen_6250, q_gen_6255, q_gen_6250, q_gen_6250) -> q_gen_6250
<leaf, a>() -> q_gen_6255
<leaf, b>() -> q_gen_6255
<a, leaf>() -> q_gen_6256
<b, leaf>() -> q_gen_6256
<a, a>() -> q_gen_6257
<b, b>() -> q_gen_6257
}

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 7  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 7  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8  ;  (member([e, leaf])) -> BOT -> 7  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 7
}
Sat witness: Yes: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 13, which took 1.081661 s (model generation: 0.008468,  model checking: 1.073193):

Model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253, q_gen_6259, q_gen_6262, q_gen_6266},
Q_f={q_gen_6251},
Delta=
{
<leaf>() -> q_gen_6252
<node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6252
<node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6252
<node>(q_gen_6262, q_gen_6259, q_gen_6259) -> q_gen_6252
<b>() -> q_gen_6253
<node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6259
<a>() -> q_gen_6262
<a, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6259, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6252, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, leaf>() -> q_gen_6266
<b, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6266
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  swap -> 
{{{
Q={q_gen_6250, q_gen_6255, q_gen_6256, q_gen_6257},
Q_f={q_gen_6250},
Delta=
{
<leaf, leaf>() -> q_gen_6250
<node, node>(q_gen_6257, q_gen_6256, q_gen_6256, q_gen_6255, q_gen_6250, q_gen_6250, q_gen_6255, q_gen_6250, q_gen_6250) -> q_gen_6250
<leaf, a>() -> q_gen_6255
<leaf, b>() -> q_gen_6255
<a, leaf>() -> q_gen_6256
<b, leaf>() -> q_gen_6256
<a, a>() -> q_gen_6257
<b, b>() -> q_gen_6257
}

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 7  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 7  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8  ;  (member([e, leaf])) -> BOT -> 7  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 10
}
Sat witness: Yes: ((swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]), {
_mh -> node(b, leaf, leaf)  ;  _nh -> leaf  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 14, which took 0.016510 s (model generation: 0.009267,  model checking: 0.007243):

Model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253, q_gen_6259, q_gen_6262, q_gen_6266},
Q_f={q_gen_6251},
Delta=
{
<leaf>() -> q_gen_6252
<node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6252
<node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6252
<node>(q_gen_6262, q_gen_6259, q_gen_6259) -> q_gen_6252
<b>() -> q_gen_6253
<node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6259
<a>() -> q_gen_6262
<a, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6259, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6252, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, leaf>() -> q_gen_6266
<b, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6266
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  swap -> 
{{{
Q={q_gen_6250, q_gen_6255, q_gen_6256, q_gen_6257, q_gen_6282, q_gen_6283},
Q_f={q_gen_6250},
Delta=
{
<leaf>() -> q_gen_6282
<b>() -> q_gen_6283
<leaf, leaf>() -> q_gen_6250
<leaf, node>(q_gen_6283, q_gen_6282, q_gen_6282) -> q_gen_6250
<node, leaf>(q_gen_6283, q_gen_6282, q_gen_6282) -> q_gen_6250
<node, node>(q_gen_6257, q_gen_6256, q_gen_6256, q_gen_6255, q_gen_6250, q_gen_6250, q_gen_6255, q_gen_6250, q_gen_6250) -> q_gen_6250
<leaf, a>() -> q_gen_6255
<leaf, b>() -> q_gen_6255
<node, b>(q_gen_6283, q_gen_6282, q_gen_6282) -> q_gen_6255
<a, leaf>() -> q_gen_6256
<b, leaf>() -> q_gen_6256
<b, node>(q_gen_6283, q_gen_6282, q_gen_6282) -> q_gen_6256
<a, a>() -> q_gen_6257
<b, b>() -> q_gen_6257
}

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 7  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 7  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 10  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8  ;  (member([e, leaf])) -> BOT -> 8  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 10
}
Sat witness: 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(b, node(b, leaf, leaf), node(b, leaf, leaf))
})

-------------------------------------------
Step 15, which took 0.010705 s (model generation: 0.010097,  model checking: 0.000608):

Model:
|_
{
member -> 
{{{
Q={q_gen_6251, q_gen_6252, q_gen_6253, q_gen_6259, q_gen_6262, q_gen_6266},
Q_f={q_gen_6251},
Delta=
{
<leaf>() -> q_gen_6252
<node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6252
<b>() -> q_gen_6253
<node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6259
<node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6259
<node>(q_gen_6262, q_gen_6259, q_gen_6259) -> q_gen_6259
<a>() -> q_gen_6262
<a, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6252, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6259, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6253, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6252, q_gen_6259) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6252) -> q_gen_6251
<b, node>(q_gen_6262, q_gen_6259, q_gen_6259) -> q_gen_6251
<b, leaf>() -> q_gen_6266
<b, node>(q_gen_6262, q_gen_6252, q_gen_6252) -> q_gen_6266
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  swap -> 
{{{
Q={q_gen_6250, q_gen_6255, q_gen_6256, q_gen_6257, q_gen_6282, q_gen_6283},
Q_f={q_gen_6250},
Delta=
{
<leaf>() -> q_gen_6282
<b>() -> q_gen_6283
<leaf, leaf>() -> q_gen_6250
<leaf, node>(q_gen_6283, q_gen_6282, q_gen_6282) -> q_gen_6250
<node, leaf>(q_gen_6283, q_gen_6282, q_gen_6282) -> q_gen_6250
<node, node>(q_gen_6257, q_gen_6256, q_gen_6256, q_gen_6255, q_gen_6250, q_gen_6250, q_gen_6255, q_gen_6250, q_gen_6250) -> q_gen_6250
<leaf, a>() -> q_gen_6255
<leaf, b>() -> q_gen_6255
<node, b>(q_gen_6283, q_gen_6282, q_gen_6282) -> q_gen_6255
<a, leaf>() -> q_gen_6256
<b, leaf>() -> q_gen_6256
<b, node>(q_gen_6283, q_gen_6282, q_gen_6282) -> q_gen_6256
<a, a>() -> q_gen_6257
<b, b>() -> q_gen_6257
}

Datatype: <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  ;  () -> swap([leaf, leaf]) -> 7  ;  (member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]) -> 10  ;  (member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9  ;  (not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 10  ;  (not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8  ;  (member([e, leaf])) -> BOT -> 8  ;  (swap([t1, _nh]) /\ swap([t2, _mh])) -> swap([node(e, t1, t2), node(e, _mh, _nh)]) -> 10
}
Sat witness: Yes: ((member([e, t1]) /\ swap([t1, _rh])) -> member([e, _rh]), {
_rh -> leaf  ;  e -> b  ;  t1 -> node(b, leaf, leaf)
})

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