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

Inference procedure has parameters:
Ice fuel: 200
Timeout: Some(60.) (sec)
Teacher_type: Checks all clauses every time
Approximation method: remove every clause that can be safely removed



Learning problem is:

env: {
elt -> {a, b}  ;  etree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(member, P:
{
member(e2, node(e2, t1, t2)) <= True
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)
False <= member(e, leaf)
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))
}
)
(replace, F:
{
replace(e1, e2, leaf, leaf) <= True
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)
}
eq_etree(_kxa, _lxa) <= replace(_hxa, _ixa, _jxa, _kxa) /\ replace(_hxa, _ixa, _jxa, _lxa)
)
}

properties:
{
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)
}


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

Clause system for inference is:

{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}


Solving took 36.306327 seconds.
Yes: |_
name: None

member ->
[
member : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_1)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_2)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  _r_2(leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1) /\ _r_2(x_0_2) /\ _r_4(x_0_0)
  _r_4(b) <= True
  replace(a, a, leaf, leaf) <= True
  replace(a, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(a, b, leaf, leaf) <= True
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_2(x_3_1) /\ _r_2(x_3_2) /\ _r_4(x_3_0)
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005950 s (model generation: 0.005885,  model checking: 0.000065):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
Yes: {
e2 -> b
}

replace(e1, e2, leaf, leaf) <= True  :
Yes: {
e1 -> b  ;  e2 -> b
}

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
No: ()

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
No: ()

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
No: ()


-------------------------------------------
Step 1, which took 0.006485 s (model generation: 0.006349,  model checking: 0.000136):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(b, node(b, leaf, leaf)) <= True
replace(b, b, leaf, leaf) <= True
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  replace(b, b, leaf, leaf) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
Yes: {
e2 -> a
}

replace(e1, e2, leaf, leaf) <= True  :
Yes: {
e1 -> b  ;  e2 -> a
}

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> leaf
}

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
No: ()

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
Yes: {
_fxa -> leaf  ;  _gxa -> leaf  ;  e1 -> b  ;  e2 -> b  ;  e3 -> a  ;  t1 -> leaf  ;  t2 -> leaf
}

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
Yes: {
_dxa -> leaf  ;  _exa -> leaf  ;  e2 -> b  ;  e3 -> b  ;  t1 -> leaf  ;  t2 -> leaf
}


-------------------------------------------
Step 2, which took 0.009667 s (model generation: 0.009578,  model checking: 0.000089):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
replace(b, a, leaf, leaf) <= True
replace(b, b, leaf, leaf) <= True
replace(b, b, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
member(b, leaf) <= member(b, node(a, leaf, leaf))
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  member(a, node(x_1_0, x_1_1, x_1_2)) <= True
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  replace(b, a, leaf, leaf) <= True
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

replace(e1, e2, leaf, leaf) <= True  :
Yes: {
e1 -> a  ;  e2 -> b
}

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> leaf  ;  t2 -> leaf
}

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
No: ()

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
Yes: {
_fxa -> leaf  ;  _gxa -> leaf  ;  e1 -> b  ;  e2 -> a  ;  e3 -> a  ;  t1 -> leaf  ;  t2 -> leaf
}

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
Yes: {
_dxa -> leaf  ;  _exa -> leaf  ;  e2 -> a  ;  e3 -> b  ;  t1 -> leaf  ;  t2 -> leaf
}


-------------------------------------------
Step 3, which took 0.014868 s (model generation: 0.014760,  model checking: 0.000108):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
replace(a, b, leaf, leaf) <= True
replace(b, a, leaf, leaf) <= True
replace(b, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, a, node(b, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, leaf, leaf) <= True
replace(b, b, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
member(a, leaf) <= member(a, node(b, leaf, leaf))
member(b, leaf) <= member(b, node(a, leaf, leaf))
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  member(a, leaf) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= True
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  replace(a, b, leaf, leaf) <= True
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

replace(e1, e2, leaf, leaf) <= True  :
Yes: {
e1 -> a  ;  e2 -> a
}

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
Yes: {
_mxa -> leaf  ;  t1 -> leaf
}

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
Yes: {
_fxa -> leaf  ;  _gxa -> leaf  ;  e1 -> a  ;  e2 -> b  ;  e3 -> b  ;  t1 -> leaf  ;  t2 -> leaf
}

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
Yes: {
_dxa -> leaf  ;  _exa -> leaf  ;  e2 -> b  ;  e3 -> a  ;  t1 -> leaf  ;  t2 -> leaf
}


-------------------------------------------
Step 4, which took 0.025392 s (model generation: 0.025181,  model checking: 0.000211):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
replace(a, a, leaf, leaf) <= True
replace(a, b, leaf, leaf) <= True
replace(a, b, node(a, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(b, a, leaf, leaf) <= True
replace(b, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, a, node(b, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, leaf, leaf) <= True
replace(b, b, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
False <= member(a, leaf)
False <= member(a, node(b, leaf, leaf))
member(b, leaf) <= member(b, node(a, leaf, leaf))
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  _r_1(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_0)
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  replace(a, a, leaf, leaf) <= True
  replace(a, b, leaf, leaf) <= True
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

replace(e1, e2, leaf, leaf) <= True  :
No: ()

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> node(a, _wwqbd_1, _wwqbd_2)
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> leaf  ;  t2 -> node(a, _axqbd_1, _axqbd_2)
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
Yes: {
_mxa -> node(a, _vxqbd_1, _vxqbd_2)  ;  t1 -> node(_wxqbd_0, _wxqbd_1, _wxqbd_2)
}

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
Yes: {
_fxa -> leaf  ;  _gxa -> leaf  ;  e1 -> a  ;  e2 -> a  ;  e3 -> b  ;  t1 -> leaf  ;  t2 -> leaf
}

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
Yes: {
_dxa -> leaf  ;  _exa -> leaf  ;  e2 -> a  ;  e3 -> a  ;  t1 -> leaf  ;  t2 -> leaf
}


-------------------------------------------
Step 5, which took 0.072366 s (model generation: 0.071289,  model checking: 0.001077):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, leaf, node(a, leaf, leaf))) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
replace(a, a, leaf, leaf) <= True
replace(a, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(a, a, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, leaf, leaf) <= True
replace(a, b, node(a, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(b, a, leaf, leaf) <= True
replace(b, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, a, node(b, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, leaf, leaf) <= True
replace(b, b, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
False <= member(a, leaf)
False <= member(a, node(b, leaf, leaf))
member(b, leaf) <= member(b, node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(a, leaf, leaf))
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= True
  _r_2(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_0)
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  _r_3(b) <= True
  replace(a, a, leaf, leaf) <= True
  replace(a, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(a, b, leaf, leaf) <= True
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_3(x_3_0)
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

replace(e1, e2, leaf, leaf) <= True  :
No: ()

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
}

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
Yes: {
_mxa -> node(b, _sbrbd_1, node(_xdrbd_0, _xdrbd_1, _xdrbd_2))  ;  t1 -> node(_tbrbd_0, _tbrbd_1, _tbrbd_2)
}

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
No: ()

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
No: ()


-------------------------------------------
Step 6, which took 0.118688 s (model generation: 0.117283,  model checking: 0.001405):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, leaf, node(a, leaf, leaf))) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
replace(a, a, leaf, leaf) <= True
replace(a, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(a, a, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, leaf, leaf) <= True
replace(a, b, node(a, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(b, a, leaf, leaf) <= True
replace(b, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, a, node(b, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, leaf, leaf) <= True
replace(b, b, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
False <= member(a, leaf)
False <= member(a, node(b, leaf, leaf))
False <= member(a, node(b, node(b, leaf, leaf), leaf))
member(b, leaf) <= member(b, node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(a, leaf, leaf)))
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  _r_2(leaf) <= True
  _r_4(b) <= True
  replace(a, a, leaf, leaf) <= True
  replace(a, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(a, b, leaf, leaf) <= True
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_2(x_3_2) /\ _r_4(x_3_0)
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

replace(e1, e2, leaf, leaf) <= True  :
No: ()

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> node(b, _jerbd_1, node(a, _slrbd_1, _slrbd_2))  ;  t2 -> leaf
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> leaf  ;  t2 -> node(b, _uerbd_1, node(a, _slrbd_1, _slrbd_2))
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
Yes: {
_mxa -> node(b, node(a, _plrbd_1, _plrbd_2), leaf)  ;  t1 -> node(_ihrbd_0, _ihrbd_1, _ihrbd_2)
}

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
Yes: {
_fxa -> node(b, _djrbd_1, leaf)  ;  _gxa -> node(b, _ejrbd_1, leaf)  ;  e1 -> a  ;  e2 -> b  ;  e3 -> b  ;  t1 -> node(_ijrbd_0, _ijrbd_1, _ijrbd_2)  ;  t2 -> node(_jjrbd_0, _jjrbd_1, _jjrbd_2)
}

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
Yes: {
_dxa -> node(b, _blrbd_1, leaf)  ;  _exa -> node(b, _clrbd_1, leaf)  ;  e2 -> b  ;  e3 -> a  ;  t1 -> node(_flrbd_0, _flrbd_1, _flrbd_2)  ;  t2 -> node(_glrbd_0, _glrbd_1, _glrbd_2)
}


-------------------------------------------
Step 7, which took 0.360489 s (model generation: 0.358912,  model checking: 0.001577):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, leaf, node(a, leaf, leaf))) <= True
member(a, node(b, leaf, node(b, leaf, node(a, leaf, leaf)))) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(a, node(b, node(b, leaf, node(a, leaf, leaf)), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
replace(a, a, leaf, leaf) <= True
replace(a, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(a, a, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, leaf, leaf) <= True
replace(a, b, node(a, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(a, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(b, a, leaf, leaf) <= True
replace(b, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, a, node(b, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, leaf, leaf) <= True
replace(b, b, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
False <= member(a, leaf)
False <= member(a, node(b, leaf, leaf))
False <= member(a, node(b, node(b, leaf, leaf), leaf))
member(b, leaf) <= member(b, node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(a, leaf, leaf)))
False <= replace(a, b, node(a, leaf, leaf), node(b, node(a, leaf, leaf), leaf))
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_2)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_4(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  _r_1(leaf, leaf) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True
  _r_3(b) <= True
  replace(a, a, leaf, leaf) <= True
  replace(a, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(a, b, leaf, leaf) <= True
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_1, x_3_1) /\ _r_1(x_2_1, x_3_2) /\ _r_3(x_3_0)
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_1, x_3_1)
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

replace(e1, e2, leaf, leaf) <= True  :
No: ()

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> node(b, node(a, _gyrbd_1, _gyrbd_2), leaf)  ;  t2 -> leaf
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> leaf  ;  t2 -> node(b, node(a, _gyrbd_1, _gyrbd_2), leaf)
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
Yes: {
_mxa -> node(b, node(a, _nyrbd_1, _nyrbd_2), node(_myrbd_0, _myrbd_1, _myrbd_2))  ;  t1 -> node(_qprbd_0, node(_lyrbd_0, _lyrbd_1, _lyrbd_2), _qprbd_2)
}

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
Yes: {
_fxa -> node(b, node(_tyrbd_0, _tyrbd_1, _tyrbd_2), node(_tyrbd_0, _tyrbd_1, _tyrbd_2))  ;  _gxa -> leaf  ;  e1 -> a  ;  e2 -> b  ;  e3 -> b  ;  t1 -> node(_xrrbd_0, node(_syrbd_0, _syrbd_1, _syrbd_2), _xrrbd_2)  ;  t2 -> leaf
}

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
Yes: {
_dxa -> node(b, node(_tyrbd_0, _tyrbd_1, _tyrbd_2), node(_tyrbd_0, _tyrbd_1, _tyrbd_2))  ;  _exa -> leaf  ;  e2 -> b  ;  e3 -> a  ;  t1 -> node(_xvrbd_0, node(_syrbd_0, _syrbd_1, _syrbd_2), _xvrbd_2)  ;  t2 -> leaf
}


-------------------------------------------
Step 8, which took 0.975184 s (model generation: 0.973355,  model checking: 0.001829):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, leaf, node(a, leaf, leaf))) <= True
member(a, node(b, leaf, node(b, leaf, node(a, leaf, leaf)))) <= True
member(a, node(b, leaf, node(b, node(a, leaf, leaf), leaf))) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(a, node(b, node(b, leaf, node(a, leaf, leaf)), leaf)) <= True
member(a, node(b, node(b, node(a, leaf, leaf), leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
replace(a, a, leaf, leaf) <= True
replace(a, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(a, a, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, leaf, leaf) <= True
replace(a, b, node(a, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(a, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(b, a, leaf, leaf) <= True
replace(b, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, a, node(b, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, leaf, leaf) <= True
replace(b, b, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
False <= member(a, leaf)
False <= member(a, node(b, leaf, leaf))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(b, leaf, leaf), leaf))
member(b, leaf) <= member(b, node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(a, leaf, leaf)))
False <= replace(a, b, node(a, leaf, leaf), node(b, node(a, leaf, leaf), leaf))
replace(a, b, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
replace(a, b, node(b, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_2)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  _r_1(leaf, leaf) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True
  _r_4(b) <= True
  replace(a, a, leaf, leaf) <= True
  replace(a, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(a, b, leaf, leaf) <= True
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_1, x_3_1) /\ _r_1(x_2_2, x_3_2) /\ _r_4(x_3_0)
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

replace(e1, e2, leaf, leaf) <= True  :
No: ()

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
Yes: {
_mxa -> node(b, node(_qjsbd_0, _qjsbd_1, _qjsbd_2), node(a, _fksbd_1, _fksbd_2))  ;  t1 -> node(_idsbd_0, node(_pjsbd_0, _pjsbd_1, _pjsbd_2), node(_eksbd_0, _eksbd_1, _eksbd_2))
}

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
No: ()

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
No: ()


-------------------------------------------
Step 9, which took 0.932311 s (model generation: 0.930756,  model checking: 0.001555):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, leaf, node(a, leaf, leaf))) <= True
member(a, node(b, leaf, node(b, leaf, node(a, leaf, leaf)))) <= True
member(a, node(b, leaf, node(b, node(a, leaf, leaf), leaf))) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(a, node(b, node(b, leaf, node(a, leaf, leaf)), leaf)) <= True
member(a, node(b, node(b, node(a, leaf, leaf), leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
replace(a, a, leaf, leaf) <= True
replace(a, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(a, a, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, leaf, leaf) <= True
replace(a, b, node(a, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(a, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(b, a, leaf, leaf) <= True
replace(b, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, a, node(b, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, leaf, leaf) <= True
replace(b, b, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
False <= member(a, leaf)
False <= member(a, node(b, leaf, leaf))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(b, leaf, leaf), leaf))
member(b, leaf) <= member(b, node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(a, leaf, leaf)))
False <= replace(a, b, node(a, leaf, leaf), node(b, node(a, leaf, leaf), leaf))
replace(a, b, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
replace(a, b, node(b, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_1)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_2)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_4(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  _r_2(leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(b) <= True
  replace(a, a, leaf, leaf) <= True
  replace(a, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(a, b, leaf, leaf) <= True
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_2(x_3_1) /\ _r_2(x_3_2) /\ _r_3(x_3_0)
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

replace(e1, e2, leaf, leaf) <= True  :
No: ()

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
Yes: {
_mxa -> node(b, leaf, node(b, _ewsbd_1, node(a, _uwsbd_1, _uwsbd_2)))  ;  t1 -> node(_npsbd_0, _npsbd_1, _npsbd_2)
}

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
No: ()

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
No: ()


-------------------------------------------
Step 10, which took 1.002514 s (model generation: 1.000529,  model checking: 0.001985):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, leaf, node(a, leaf, leaf))) <= True
member(a, node(b, leaf, node(b, leaf, node(a, leaf, leaf)))) <= True
member(a, node(b, leaf, node(b, node(a, leaf, leaf), leaf))) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(a, node(b, node(b, leaf, node(a, leaf, leaf)), leaf)) <= True
member(a, node(b, node(b, node(a, leaf, leaf), leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
replace(a, a, leaf, leaf) <= True
replace(a, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(a, a, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, leaf, leaf) <= True
replace(a, b, node(a, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(a, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(b, a, leaf, leaf) <= True
replace(b, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, a, node(b, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, leaf, leaf) <= True
replace(b, b, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
False <= member(a, leaf)
False <= member(a, node(b, leaf, leaf))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(b, leaf, leaf), leaf))
member(b, leaf) <= member(b, node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(a, leaf, leaf)))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
False <= replace(a, b, node(a, leaf, leaf), node(b, node(a, leaf, leaf), leaf))
replace(a, b, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
replace(a, b, node(b, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_2)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_4(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  _r_1(leaf, leaf) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  _r_3(b) <= True
  replace(a, a, leaf, leaf) <= True
  replace(a, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(a, b, leaf, leaf) <= True
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_1, x_3_1) /\ _r_1(x_2_2, x_3_2) /\ _r_3(x_3_0)
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

replace(e1, e2, leaf, leaf) <= True  :
No: ()

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
Yes: {
_mxa -> node(b, leaf, node(b, _uitbd_1, node(a, _tjtbd_1, _tjtbd_2)))  ;  t1 -> node(_zbtbd_0, leaf, node(_titbd_0, _titbd_1, _titbd_2))
}

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
No: ()

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
No: ()


-------------------------------------------
Step 11, which took 1.100791 s (model generation: 1.097897,  model checking: 0.002894):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, leaf, node(a, leaf, leaf))) <= True
member(a, node(b, leaf, node(b, leaf, node(a, leaf, leaf)))) <= True
member(a, node(b, leaf, node(b, node(a, leaf, leaf), leaf))) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(a, node(b, node(b, leaf, node(a, leaf, leaf)), leaf)) <= True
member(a, node(b, node(b, node(a, leaf, leaf), leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
replace(a, a, leaf, leaf) <= True
replace(a, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(a, a, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, leaf, leaf) <= True
replace(a, b, node(a, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(a, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(b, a, leaf, leaf) <= True
replace(b, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, a, node(b, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, leaf, leaf) <= True
replace(b, b, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
False <= member(a, leaf)
False <= member(a, node(b, leaf, leaf))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(b, leaf, leaf), leaf))
member(b, leaf) <= member(b, node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(a, leaf, leaf)))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
False <= replace(a, b, node(a, leaf, leaf), node(b, node(a, leaf, leaf), leaf))
False <= replace(a, b, node(a, leaf, node(a, leaf, leaf)), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
replace(a, b, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
replace(a, b, node(b, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_2)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  _r_1(leaf, leaf) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), leaf) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
  _r_4(b) <= True
  replace(a, a, leaf, leaf) <= True
  replace(a, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(a, b, leaf, leaf) <= True
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_1, x_3_1) /\ _r_1(x_2_1, x_3_2) /\ _r_4(x_3_0)
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_1, x_3_2)
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

replace(e1, e2, leaf, leaf) <= True  :
No: ()

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
Yes: {
_mxa -> node(b, leaf, node(b, _haubd_1, node(a, _mytbd_1, _mytbd_2)))  ;  t1 -> node(_yotbd_0, node(_gaubd_0, _gaubd_1, _gaubd_2), _yotbd_2)
}

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
Yes: {
_fxa -> leaf  ;  _gxa -> node(_pstbd_0, _pstbd_1, node(b, _sytbd_1, _sytbd_2))  ;  e1 -> b  ;  e2 -> a  ;  e3 -> a  ;  t1 -> leaf  ;  t2 -> node(_ustbd_0, node(_rytbd_0, _rytbd_1, _rytbd_2), _ustbd_2)
}

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
Yes: {
_dxa -> leaf  ;  _exa -> node(_kwtbd_0, _kwtbd_1, node(b, _sytbd_1, _sytbd_2))  ;  e2 -> a  ;  e3 -> b  ;  t1 -> leaf  ;  t2 -> node(_owtbd_0, node(_rytbd_0, _rytbd_1, _rytbd_2), _owtbd_2)
}


-------------------------------------------
Step 12, which took 1.337331 s (model generation: 1.335099,  model checking: 0.002232):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, leaf, node(a, leaf, leaf))) <= True
member(a, node(b, leaf, node(b, leaf, node(a, leaf, leaf)))) <= True
member(a, node(b, leaf, node(b, node(a, leaf, leaf), leaf))) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(a, node(b, node(b, leaf, node(a, leaf, leaf)), leaf)) <= True
member(a, node(b, node(b, node(a, leaf, leaf), leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
replace(a, a, leaf, leaf) <= True
replace(a, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(a, a, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, leaf, leaf) <= True
replace(a, b, node(a, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(a, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(b, a, leaf, leaf) <= True
replace(b, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, a, node(b, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, leaf, leaf) <= True
replace(b, b, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
False <= member(a, leaf)
False <= member(a, node(b, leaf, leaf))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(b, leaf, leaf), leaf))
member(b, leaf) <= member(b, node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(a, leaf, leaf)))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
False <= replace(a, b, node(a, leaf, leaf), node(b, node(a, leaf, leaf), leaf))
False <= replace(a, b, node(a, leaf, node(a, leaf, leaf)), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
False <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
replace(a, b, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
replace(a, b, node(b, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
replace(b, a, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, leaf, node(a, leaf, node(b, leaf, leaf)))) <= replace(b, a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(b, leaf, leaf)))
replace(b, a, node(b, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, leaf, node(a, leaf, node(b, leaf, leaf)))) <= replace(b, a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(b, leaf, leaf)))
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_4(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  _r_1(leaf, leaf) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_0, x_1_0)
  _r_2(a, b) <= True
  _r_2(b, a) <= True
  _r_2(b, b) <= True
  replace(a, a, leaf, leaf) <= True
  replace(a, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(a, b, leaf, leaf) <= True
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_1, x_3_1) /\ _r_1(x_2_1, x_3_2) /\ _r_2(x_2_0, x_3_0)
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_2(x_2_0, x_3_0)
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_1, x_3_1)
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

replace(e1, e2, leaf, leaf) <= True  :
No: ()

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
Yes: {
_mxa -> node(a, leaf, leaf)  ;  t1 -> node(b, leaf, _reubd_2)
}

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
Yes: {
_fxa -> node(a, node(b, _rnubd_1, _rnubd_2), _tiubd_2)  ;  _gxa -> node(_uiubd_0, leaf, _uiubd_2)  ;  e1 -> b  ;  e2 -> b  ;  e3 -> a  ;  t1 -> node(a, node(b, _qnubd_1, _qnubd_2), _yiubd_2)  ;  t2 -> node(_ziubd_0, leaf, _ziubd_2)
}

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
Yes: {
_dxa -> node(a, node(b, _rnubd_1, _rnubd_2), _mmubd_2)  ;  _exa -> node(_nmubd_0, leaf, _nmubd_2)  ;  e2 -> b  ;  e3 -> b  ;  t1 -> node(a, node(b, _qnubd_1, _qnubd_2), _qmubd_2)  ;  t2 -> node(_rmubd_0, leaf, _rmubd_2)
}


-------------------------------------------
Step 13, which took 4.953863 s (model generation: 4.948178,  model checking: 0.005685):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, leaf, node(a, leaf, leaf))) <= True
member(a, node(b, leaf, node(b, leaf, node(a, leaf, leaf)))) <= True
member(a, node(b, leaf, node(b, node(a, leaf, leaf), leaf))) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(a, node(b, node(b, leaf, node(a, leaf, leaf)), leaf)) <= True
member(a, node(b, node(b, node(a, leaf, leaf), leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
replace(a, a, leaf, leaf) <= True
replace(a, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(a, a, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, leaf, leaf) <= True
replace(a, b, node(a, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(a, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(b, a, leaf, leaf) <= True
replace(b, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, a, node(b, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, leaf, leaf) <= True
replace(b, b, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
False <= member(a, leaf)
False <= member(a, node(b, leaf, leaf))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(b, leaf, leaf), leaf))
member(b, leaf) <= member(b, node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(a, leaf, leaf)))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
False <= replace(a, b, node(a, leaf, leaf), node(b, node(a, leaf, leaf), leaf))
False <= replace(a, b, node(a, leaf, node(a, leaf, leaf)), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
False <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
replace(a, b, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
replace(a, b, node(b, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= replace(a, b, node(b, leaf, leaf), node(a, leaf, leaf))
replace(b, a, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, leaf, node(a, leaf, node(b, leaf, leaf)))) <= replace(b, a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(b, leaf, leaf)))
replace(b, a, node(b, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, leaf, node(a, leaf, node(b, leaf, leaf)))) <= replace(b, a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(b, leaf, leaf)))
replace(b, b, node(a, node(a, node(b, leaf, leaf), leaf), node(a, leaf, leaf)), node(a, node(a, node(b, leaf, leaf), leaf), node(a, leaf, leaf))) <= replace(b, b, node(a, node(b, leaf, leaf), leaf), node(a, node(b, leaf, leaf), leaf))
replace(b, b, node(b, node(a, node(b, leaf, leaf), leaf), node(a, leaf, leaf)), node(b, node(a, node(b, leaf, leaf), leaf), node(a, leaf, leaf))) <= replace(b, b, node(a, node(b, leaf, leaf), leaf), node(a, node(b, leaf, leaf), leaf))
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_2)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  _r_1(leaf, leaf) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
  _r_4(b) <= True
  replace(a, a, leaf, leaf) <= True
  replace(a, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(a, b, leaf, leaf) <= True
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_2, x_3_1) /\ _r_1(x_2_2, x_3_2) /\ _r_4(x_3_0)
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_2, x_3_1) /\ _r_4(x_2_0) /\ _r_4(x_3_0)
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

replace(e1, e2, leaf, leaf) <= True  :
No: ()

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
Yes: {
_mxa -> node(b, node(b, node(a, _odwbd_1, _odwbd_2), _zdwbd_2), _wsubd_2)  ;  t1 -> node(b, _xsubd_1, node(_ydwbd_0, _ydwbd_1, _ydwbd_2))
}

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
Yes: {
_fxa -> leaf  ;  _gxa -> node(b, node(b, _hewbd_1, _hewbd_2), node(b, _hewbd_1, _hewbd_2))  ;  e1 -> a  ;  e2 -> b  ;  e3 -> b  ;  t1 -> leaf  ;  t2 -> node(_qvubd_0, _qvubd_1, node(_gewbd_0, _gewbd_1, _gewbd_2))
}

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
Yes: {
_dxa -> leaf  ;  _exa -> node(b, node(b, _hewbd_1, _hewbd_2), node(b, _hewbd_1, _hewbd_2))  ;  e2 -> b  ;  e3 -> a  ;  t1 -> leaf  ;  t2 -> node(_dpvbd_0, _dpvbd_1, node(_gewbd_0, _gewbd_1, _gewbd_2))
}


-------------------------------------------
Step 14, which took 4.758816 s (model generation: 4.702026,  model checking: 0.056790):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, leaf, node(a, leaf, leaf))) <= True
member(a, node(b, leaf, node(b, leaf, node(a, leaf, leaf)))) <= True
member(a, node(b, leaf, node(b, node(a, leaf, leaf), leaf))) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(a, node(b, node(b, leaf, node(a, leaf, leaf)), leaf)) <= True
member(a, node(b, node(b, node(a, leaf, leaf), leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
replace(a, a, leaf, leaf) <= True
replace(a, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(a, a, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, leaf, leaf) <= True
replace(a, b, node(a, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(a, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(b, a, leaf, leaf) <= True
replace(b, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, a, node(b, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, leaf, leaf) <= True
replace(b, b, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
False <= member(a, leaf)
False <= member(a, node(b, leaf, leaf))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(b, leaf, leaf), leaf))
member(b, leaf) <= member(b, node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(a, leaf, leaf)))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
False <= replace(a, b, node(a, leaf, leaf), node(b, node(a, leaf, leaf), leaf))
False <= replace(a, b, node(a, leaf, node(a, leaf, leaf)), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
replace(a, b, node(a, leaf, node(a, leaf, node(a, leaf, leaf))), node(b, leaf, node(b, node(b, leaf, leaf), node(b, leaf, leaf)))) <= replace(a, b, node(a, leaf, node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf)))
replace(a, b, node(b, leaf, node(a, leaf, node(a, leaf, leaf))), node(b, leaf, node(b, node(b, leaf, leaf), node(b, leaf, leaf)))) <= replace(a, b, node(a, leaf, node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf)))
False <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
replace(a, b, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
replace(a, b, node(b, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= replace(a, b, node(b, leaf, leaf), node(a, leaf, leaf))
False <= replace(a, b, node(b, leaf, node(a, leaf, leaf)), node(b, node(b, node(a, leaf, leaf), leaf), leaf))
replace(b, a, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, leaf, node(a, leaf, node(b, leaf, leaf)))) <= replace(b, a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(b, leaf, leaf)))
replace(b, a, node(b, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, leaf, node(a, leaf, node(b, leaf, leaf)))) <= replace(b, a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(b, leaf, leaf)))
replace(b, b, node(a, node(a, node(b, leaf, leaf), leaf), node(a, leaf, leaf)), node(a, node(a, node(b, leaf, leaf), leaf), node(a, leaf, leaf))) <= replace(b, b, node(a, node(b, leaf, leaf), leaf), node(a, node(b, leaf, leaf), leaf))
replace(b, b, node(b, node(a, node(b, leaf, leaf), leaf), node(a, leaf, leaf)), node(b, node(a, node(b, leaf, leaf), leaf), node(a, leaf, leaf))) <= replace(b, b, node(a, node(b, leaf, leaf), leaf), node(a, node(b, leaf, leaf), leaf))
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  _r_2(leaf) <= True
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_4(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1) /\ _r_3(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2) /\ _r_3(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  _r_1(a, b) <= True
  _r_1(b, b) <= True
  _r_2(leaf) <= True
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_4(a) <= True
  replace(a, a, leaf, leaf) <= True
  replace(a, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(a, b, leaf, leaf) <= True
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_0, x_3_0) /\ _r_2(x_3_1) /\ _r_2(x_3_2)
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_0, x_3_0) /\ _r_2(x_3_2) /\ _r_3(x_2_1) /\ _r_3(x_3_1)
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_2(x_3_2) /\ _r_3(x_2_1)
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_3(x_2_1) /\ _r_3(x_2_2)
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

replace(e1, e2, leaf, leaf) <= True  :
No: ()

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> node(_rgwbd_0, leaf, node(a, _wpkcd_1, _wpkcd_2))  ;  t2 -> node(b, leaf, leaf)
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(a, _mqwbd_1, _mqwbd_2)
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> node(b, node(b, leaf, leaf), node(a, _wpkcd_1, _wpkcd_2))  ;  t2 -> leaf
}

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
Yes: {
_mxa -> node(_zcxbd_0, node(a, _wpkcd_1, _wpkcd_2), leaf)  ;  t1 -> node(_adxbd_0, node(a, _aqkcd_1, _aqkcd_2), _adxbd_2)
}

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
Yes: {
_fxa -> leaf  ;  _gxa -> node(_qwccd_0, _qwccd_1, _qwccd_2)  ;  e1 -> a  ;  e2 -> b  ;  e3 -> b  ;  t1 -> leaf  ;  t2 -> node(_vwccd_0, node(a, _aqkcd_1, _aqkcd_2), node(a, _aqkcd_1, _aqkcd_2))
}

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
Yes: {
_dxa -> leaf  ;  _exa -> node(_wyjcd_0, _wyjcd_1, leaf)  ;  e2 -> b  ;  e3 -> a  ;  t1 -> leaf  ;  t2 -> node(_azjcd_0, node(a, _aqkcd_1, _aqkcd_2), _azjcd_2)
}


-------------------------------------------
Step 15, which took 9.127688 s (model generation: 9.123821,  model checking: 0.003867):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
replace(e1, e2, leaf, leaf) <= True -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
False <= member(a, _mxa) /\ replace(a, b, t1, _mxa) -> 0
eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa) -> 0
replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, leaf, node(a, leaf, leaf))) <= True
member(a, node(b, leaf, node(b, leaf, node(a, leaf, leaf)))) <= True
member(a, node(b, leaf, node(b, node(a, leaf, leaf), leaf))) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(a, node(b, node(b, leaf, leaf), node(a, leaf, leaf))) <= True
member(a, node(b, node(b, leaf, node(a, leaf, leaf)), leaf)) <= True
member(a, node(b, node(b, node(a, leaf, leaf), leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
replace(a, a, leaf, leaf) <= True
replace(a, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(a, a, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, leaf, leaf) <= True
replace(a, b, node(a, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(a, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
replace(a, b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))) <= True
replace(b, a, leaf, leaf) <= True
replace(b, a, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, a, node(b, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, leaf, leaf) <= True
replace(b, b, node(a, leaf, leaf), node(a, leaf, leaf)) <= True
replace(b, b, node(b, leaf, leaf), node(b, leaf, leaf)) <= True
False <= member(a, leaf)
member(a, node(b, node(a, leaf, node(a, leaf, leaf)), node(b, leaf, leaf))) <= member(a, node(a, leaf, node(a, leaf, leaf)))
False <= member(a, node(a, node(a, leaf, leaf), leaf)) /\ replace(a, b, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= member(a, node(b, leaf, leaf))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(a, leaf, leaf), node(a, leaf, leaf))) /\ replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= member(a, node(b, node(b, leaf, leaf), leaf))
member(b, leaf) <= member(b, node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(a, leaf, leaf))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(a, leaf, leaf)))
False <= replace(a, b, node(a, leaf, leaf), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
False <= replace(a, b, node(a, leaf, leaf), node(b, node(a, leaf, leaf), leaf))
False <= replace(a, b, node(a, leaf, node(a, leaf, leaf)), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
replace(a, b, node(a, leaf, node(a, leaf, node(a, leaf, leaf))), node(b, leaf, node(b, node(b, leaf, leaf), node(b, leaf, leaf)))) <= replace(a, b, node(a, leaf, node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf)))
replace(a, b, node(b, leaf, node(a, leaf, node(a, leaf, leaf))), node(b, leaf, node(b, node(b, leaf, leaf), node(b, leaf, leaf)))) <= replace(a, b, node(a, leaf, node(a, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf)))
replace(a, b, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(b, leaf, node(a, leaf, leaf))) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
replace(a, b, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
replace(a, b, node(b, node(a, node(a, leaf, leaf), leaf), leaf), node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)) <= replace(a, b, node(a, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
replace(a, b, node(b, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf))), node(b, leaf, node(a, leaf, leaf))) <= replace(a, b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, leaf))
False <= replace(a, b, node(b, leaf, leaf), node(a, leaf, leaf))
False <= replace(a, b, node(b, leaf, node(a, leaf, leaf)), node(b, node(b, node(a, leaf, leaf), leaf), leaf))
replace(b, a, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, leaf, node(a, leaf, node(b, leaf, leaf)))) <= replace(b, a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(b, leaf, leaf)))
replace(b, a, node(b, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, leaf, node(a, leaf, node(b, leaf, leaf)))) <= replace(b, a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(b, leaf, leaf)))
replace(b, b, node(a, node(a, node(b, leaf, leaf), leaf), node(a, leaf, leaf)), node(a, node(a, node(b, leaf, leaf), leaf), node(a, leaf, leaf))) <= replace(b, b, node(a, node(b, leaf, leaf), leaf), node(a, node(b, leaf, leaf), leaf))
replace(b, b, node(b, node(a, node(b, leaf, leaf), leaf), node(a, leaf, leaf)), node(b, node(a, node(b, leaf, leaf), leaf), node(a, leaf, leaf))) <= replace(b, b, node(a, node(b, leaf, leaf), leaf), node(a, node(b, leaf, leaf), leaf))
}

Current best model:
|_
name: None

member ->
[
member : <elt * etree>
{
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_2)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  _r_1(leaf, leaf) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
  _r_4(b) <= True
  replace(a, a, leaf, leaf) <= True
  replace(a, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_1, x_3_2)
  replace(a, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_2, x_3_1) /\ _r_1(x_2_2, x_3_2)
  replace(a, b, leaf, leaf) <= True
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_1(x_2_1, x_3_2) /\ _r_1(x_2_2, x_3_1) /\ _r_1(x_2_2, x_3_2) /\ _r_4(x_3_0)
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

replace(e1, e2, leaf, leaf) <= True  :
No: ()

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

False <= member(a, _mxa) /\ replace(a, b, t1, _mxa)  :
Yes: {
_mxa -> node(b, node(b, _vqlcd_1, _vqlcd_2), node(b, _uqlcd_1, node(a, _zolcd_1, _zolcd_2)))  ;  t1 -> node(_hwkcd_0, node(_wqlcd_0, _wqlcd_1, _wqlcd_2), node(_tqlcd_0, _tqlcd_1, _tqlcd_2))
}

eq_elt(e1, e3) \/ replace(e1, e2, node(e3, t1, t2), node(e3, _fxa, _gxa)) <= replace(e1, e2, t1, _fxa) /\ replace(e1, e2, t2, _gxa)  :
Yes: {
_fxa -> leaf  ;  _gxa -> node(a, _gxkcd_1, node(b, _dplcd_1, _dplcd_2))  ;  e1 -> a  ;  e2 -> a  ;  e3 -> b  ;  t1 -> leaf  ;  t2 -> node(_lxkcd_0, node(_cplcd_0, _cplcd_1, _cplcd_2), _lxkcd_2)
}

replace(e3, e2, node(e3, t1, t2), node(e2, _dxa, _exa)) <= replace(e3, e2, t1, _dxa) /\ replace(e3, e2, t2, _exa)  :
Yes: {
_dxa -> leaf  ;  _exa -> node(a, _hglcd_1, node(b, _dplcd_1, _dplcd_2))  ;  e2 -> a  ;  e3 -> a  ;  t1 -> leaf  ;  t2 -> node(_lglcd_0, node(_cplcd_0, _cplcd_1, _cplcd_2), _lglcd_2)
}


Total time: 36.306327
Learner time: 24.720898
Teacher time: 0.081505
Reasons for stopping: Yes: |_
name: None

member ->
[
member : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_1)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_2)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
replace ->
[
replace : <elt * elt * etree * etree>
{
  _r_2(leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1) /\ _r_2(x_0_2) /\ _r_4(x_0_0)
  _r_4(b) <= True
  replace(a, a, leaf, leaf) <= True
  replace(a, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(a, b, leaf, leaf) <= True
  replace(a, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= _r_2(x_3_1) /\ _r_2(x_3_2) /\ _r_4(x_3_0)
  replace(b, a, leaf, leaf) <= True
  replace(b, a, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
  replace(b, b, leaf, leaf) <= True
  replace(b, b, node(x_2_0, x_2_1, x_2_2), node(x_3_0, x_3_1, x_3_2)) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|