Solving ../../benchmarks/smtlib/false/tree_subtree_height_error.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:
{
(leq_nat, P:
{
leq_nat(z, n2) <= True
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2)
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2))
False <= leq_nat(s(nn1), z)
}
)
(le_nat, P:
{
le_nat(z, s(nn2)) <= True
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2)
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2))
False <= le_nat(s(nn1), z)
False <= le_nat(z, z)
}
)
(subtree, P:
{
subtree(leaf, t) <= True
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))
False <= subtree(node(ea, ta1, ta2), leaf)
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))
}
)
(max, F:
{
le_nat(n, m) \/ max(n, m, n) <= True
max(n, m, m) <= le_nat(n, m)
}
eq_nat(_vdb, _wdb) <= max(_tdb, _udb, _vdb) /\ max(_tdb, _udb, _wdb)
)
(height, F:
{
height(leaf, z) <= True
height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb)
height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb)
}
eq_nat(_ceb, _deb) <= height(_beb, _ceb) /\ height(_beb, _deb)
)
}

properties:
{
subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb)
}


over-approximation: {height, leq_nat, max}
under-approximation: {max, subtree}

Clause system for inference is:

{
height(leaf, z) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb) -> 0
subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb) -> 0
height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}


Solving took 0.160588 seconds.
No: Contradictory set of ground constraints:
{
False <= True
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
height(node(b, leaf, node(a, leaf, leaf)), s(s(z))) <= True
le_nat(s(z), s(s(z))) <= True
le_nat(z, s(z)) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
subtree(node(b, leaf, leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
subtree(node(a, node(b, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ height(node(a, node(b, leaf, leaf), leaf), s(z))
False <= height(node(b, leaf, leaf), s(z))
False <= le_nat(s(s(z)), s(z))
False <= le_nat(s(z), s(z))
False <= le_nat(s(z), z)
False <= le_nat(z, z)
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
subtree(node(a, node(a, node(b, leaf, leaf), leaf), leaf), node(a, node(a, leaf, node(b, leaf, node(a, leaf, leaf))), node(b, leaf, leaf))) <= subtree(leaf, node(b, leaf, leaf)) /\ subtree(node(a, node(b, leaf, leaf), leaf), node(a, leaf, node(b, leaf, node(a, leaf, leaf))))
False <= subtree(node(a, leaf, leaf), leaf)
False <= subtree(node(a, leaf, leaf), node(b, leaf, node(a, leaf, leaf)))
False <= subtree(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf))))
False <= subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(b, leaf, leaf), node(b, leaf, leaf)) <= subtree(node(a, node(b, leaf, leaf), leaf), node(a, node(b, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
False <= subtree(node(b, leaf, node(a, leaf, leaf)), node(b, leaf, leaf))
subtree(node(b, leaf, leaf), leaf) <= subtree(node(b, node(b, leaf, leaf), leaf), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
}
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005995 s (model generation: 0.005894,  model checking: 0.000101):

Clauses:
{
height(leaf, z) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb) -> 0
subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb) -> 0
height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

height ->
[
height : <etree * nat>
{
  
}
]


;
le_nat ->
[
le_nat : <nat * nat>
{
  
}
]


;
leq_nat ->
[
leq_nat : <nat * nat>
{
  
}
]


;
subtree ->
[
subtree : <etree * etree>
{
  
}
]



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




Answer of teacher:

height(leaf, z) <= True  :
Yes: {

}

le_nat(z, s(nn2)) <= True  :
Yes: {

}

leq_nat(z, n2) <= True  :
Yes: {
n2 -> z
}

height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb)  :
No: ()

subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb)  :
No: ()

height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb)  :
No: ()

le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2)  :
No: ()

le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2))  :
No: ()

False <= le_nat(s(nn1), z)  :
No: ()

False <= le_nat(z, z)  :
No: ()

leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2)  :
No: ()

leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2))  :
No: ()

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


-------------------------------------------
Step 1, which took 0.008081 s (model generation: 0.007884,  model checking: 0.000197):

Clauses:
{
height(leaf, z) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb) -> 0
subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb) -> 0
height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
le_nat(z, s(z)) <= True
leq_nat(z, z) <= True
}

Current best model:
|_
name: None

height ->
[
height : <etree * nat>
{
  height(leaf, z) <= True
}
]


;
le_nat ->
[
le_nat : <nat * nat>
{
  le_nat(z, s(x_1_0)) <= True
}
]


;
leq_nat ->
[
leq_nat : <nat * nat>
{
  leq_nat(z, z) <= True
}
]


;
subtree ->
[
subtree : <etree * etree>
{
  
}
]



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




Answer of teacher:

height(leaf, z) <= True  :
No: ()

le_nat(z, s(nn2)) <= True  :
No: ()

leq_nat(z, n2) <= True  :
Yes: {
n2 -> s(_sjmuw_0)
}

height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb)  :
Yes: {
_aeb -> z  ;  _xdb -> z  ;  _ydb -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb)  :
Yes: {
_eeb -> z  ;  _feb -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb)  :
No: ()

le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2)  :
Yes: {
nn1 -> z  ;  nn2 -> s(_dkmuw_0)
}

le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2))  :
No: ()

False <= le_nat(s(nn1), z)  :
No: ()

False <= le_nat(z, z)  :
No: ()

leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2)  :
Yes: {
nn1 -> z  ;  nn2 -> z
}

leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2))  :
No: ()

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


-------------------------------------------
Step 2, which took 0.015318 s (model generation: 0.015052,  model checking: 0.000266):

Clauses:
{
height(leaf, z) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb) -> 0
subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb) -> 0
height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) \/ le_nat(z, z) <= True
le_nat(s(z), s(s(z))) <= True
le_nat(z, s(z)) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
subtree(leaf, leaf) <= True
}

Current best model:
|_
name: None

height ->
[
height : <etree * nat>
{
  height(leaf, z) <= True
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


;
le_nat ->
[
le_nat : <nat * nat>
{
  le_nat(s(x_0_0), s(x_1_0)) <= True
  le_nat(z, s(x_1_0)) <= True
  le_nat(z, z) <= True
}
]


;
leq_nat ->
[
leq_nat : <nat * nat>
{
  leq_nat(s(x_0_0), s(x_1_0)) <= True
  leq_nat(z, s(x_1_0)) <= True
  leq_nat(z, z) <= True
}
]


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



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




Answer of teacher:

height(leaf, z) <= True  :
No: ()

le_nat(z, s(nn2)) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb)  :
No: ()

subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb)  :
Yes: {
_eeb -> z  ;  _feb -> s(_hkmuw_0)  ;  t1 -> leaf  ;  t2 -> node(_jkmuw_0, _jkmuw_1, _jkmuw_2)
}

height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb)  :
No: ()

le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2)  :
No: ()

le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2))  :
Yes: {
nn1 -> s(_okmuw_0)  ;  nn2 -> z
}

False <= le_nat(s(nn1), z)  :
No: ()

False <= le_nat(z, z)  :
Yes: {

}

leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2)  :
No: ()

leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2))  :
Yes: {
nn1 -> s(_qkmuw_0)  ;  nn2 -> z
}

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
Yes: {
ta1 -> leaf  ;  ta2 -> leaf  ;  tb1 -> leaf  ;  tb2 -> leaf
}

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


-------------------------------------------
Step 3, which took 0.019027 s (model generation: 0.018793,  model checking: 0.000234):

Clauses:
{
height(leaf, z) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb) -> 0
subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb) -> 0
height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
le_nat(s(z), s(s(z))) <= True
le_nat(z, s(z)) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
le_nat(s(z), z) <= le_nat(s(s(z)), s(z))
False <= le_nat(z, z)
leq_nat(s(z), z) <= leq_nat(s(s(z)), s(z))
}

Current best model:
|_
name: None

height ->
[
height : <etree * nat>
{
  height(leaf, z) <= True
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


;
le_nat ->
[
le_nat : <nat * nat>
{
  le_nat(s(x_0_0), s(x_1_0)) <= True
  le_nat(s(x_0_0), z) <= True
  le_nat(z, s(x_1_0)) <= True
}
]


;
leq_nat ->
[
leq_nat : <nat * nat>
{
  leq_nat(s(x_0_0), s(x_1_0)) <= True
  leq_nat(s(x_0_0), z) <= True
  leq_nat(z, s(x_1_0)) <= True
  leq_nat(z, z) <= True
}
]


;
subtree ->
[
subtree : <etree * etree>
{
  subtree(leaf, leaf) <= True
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True
}
]



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




Answer of teacher:

height(leaf, z) <= True  :
No: ()

le_nat(z, s(nn2)) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb)  :
No: ()

subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb)  :
Yes: {
_eeb -> s(_wkmuw_0)  ;  _feb -> z  ;  t1 -> node(_ykmuw_0, _ykmuw_1, _ykmuw_2)  ;  t2 -> leaf
}

height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb)  :
No: ()

le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2)  :
No: ()

le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2))  :
Yes: {
nn1 -> z  ;  nn2 -> z
}

False <= le_nat(s(nn1), z)  :
Yes: {

}

False <= le_nat(z, z)  :
No: ()

leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2)  :
No: ()

leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2))  :
No: ()

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_klmuw_0, _klmuw_1, _klmuw_2)  ;  ta2 -> node(_llmuw_0, _llmuw_1, _llmuw_2)  ;  tb1 -> node(_mlmuw_0, _mlmuw_1, _mlmuw_2)  ;  tb2 -> leaf
}

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ea -> b  ;  eb -> a
}

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_slmuw_0, _slmuw_1, _slmuw_2)  ;  tb1 -> leaf
}


-------------------------------------------
Step 4, which took 0.020014 s (model generation: 0.019596,  model checking: 0.000418):

Clauses:
{
height(leaf, z) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb) -> 0
subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb) -> 0
height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
le_nat(s(z), s(s(z))) <= True
le_nat(z, s(z)) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
False <= le_nat(s(s(z)), s(z))
False <= le_nat(s(z), s(z))
False <= le_nat(s(z), z)
False <= le_nat(z, z)
leq_nat(s(z), z) <= leq_nat(s(s(z)), s(z))
subtree(node(a, leaf, leaf), leaf) <= leq_nat(s(z), z)
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
}

Current best model:
|_
name: None

height ->
[
height : <etree * nat>
{
  height(leaf, z) <= True
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


;
le_nat ->
[
le_nat : <nat * nat>
{
  le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0)
  le_nat(z, s(x_1_0)) <= True
}
]


;
leq_nat ->
[
leq_nat : <nat * nat>
{
  leq_nat(s(x_0_0), s(x_1_0)) <= True
  leq_nat(s(x_0_0), z) <= True
  leq_nat(z, s(x_1_0)) <= True
  leq_nat(z, z) <= True
}
]


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



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




Answer of teacher:

height(leaf, z) <= True  :
No: ()

le_nat(z, s(nn2)) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb)  :
No: ()

subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb)  :
Yes: {
_eeb -> s(_ulmuw_0)  ;  _feb -> s(_vlmuw_0)  ;  t1 -> node(b, _wlmuw_1, _wlmuw_2)  ;  t2 -> node(b, _xlmuw_1, _xlmuw_2)
}

height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb)  :
No: ()

le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2)  :
No: ()

le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2))  :
No: ()

False <= le_nat(s(nn1), z)  :
No: ()

False <= le_nat(z, z)  :
No: ()

leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2)  :
No: ()

leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2))  :
No: ()

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
Yes: {
eb -> b  ;  ta1 -> node(_wnmuw_0, _wnmuw_1, _wnmuw_2)  ;  ta2 -> node(_xnmuw_0, _xnmuw_1, _xnmuw_2)  ;  tb1 -> leaf  ;  tb2 -> leaf
}

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
eb -> a  ;  ta1 -> node(_cpmuw_0, _cpmuw_1, _cpmuw_2)  ;  ta2 -> node(b, _dpmuw_1, _dpmuw_2)  ;  tb1 -> leaf  ;  tb2 -> node(b, _fpmuw_1, _fpmuw_2)
}

False <= subtree(node(ea, ta1, ta2), leaf)  :
Yes: {

}

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
eb -> a  ;  ta1 -> node(b, _opmuw_1, _opmuw_2)  ;  tb1 -> node(b, _ppmuw_1, _ppmuw_2)
}


-------------------------------------------
Step 5, which took 0.021157 s (model generation: 0.020263,  model checking: 0.000894):

Clauses:
{
height(leaf, z) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb) -> 0
subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb) -> 0
height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
le_nat(s(z), s(s(z))) <= True
le_nat(z, s(z)) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
subtree(node(b, leaf, leaf), node(b, leaf, leaf)) <= height(node(b, leaf, leaf), s(z))
False <= le_nat(s(s(z)), s(z))
False <= le_nat(s(z), s(z))
False <= le_nat(s(z), z)
False <= le_nat(z, z)
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= subtree(node(a, leaf, leaf), leaf)
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(b, leaf, leaf), node(b, leaf, leaf)) <= subtree(node(a, node(b, leaf, leaf), leaf), node(a, node(b, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
}

Current best model:
|_
name: None

height ->
[
height : <etree * nat>
{
  height(leaf, z) <= True
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


;
le_nat ->
[
le_nat : <nat * nat>
{
  le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0)
  le_nat(z, s(x_1_0)) <= True
}
]


;
leq_nat ->
[
leq_nat : <nat * nat>
{
  leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0)
  leq_nat(z, s(x_1_0)) <= True
  leq_nat(z, z) <= True
}
]


;
subtree ->
[
subtree : <etree * etree>
{
  _r_1(a, a) <= True
  _r_1(b, b) <= True
  subtree(leaf, leaf) <= True
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_0_0, x_1_0) /\ subtree(x_0_1, x_1_2)
}
]



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




Answer of teacher:

height(leaf, z) <= True  :
No: ()

le_nat(z, s(nn2)) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb)  :
No: ()

subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb)  :
Yes: {
_eeb -> s(z)  ;  _feb -> s(z)  ;  t1 -> node(b, _cqmuw_1, _cqmuw_2)  ;  t2 -> node(a, _dqmuw_1, _dqmuw_2)
}

height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb)  :
No: ()

le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2)  :
No: ()

le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2))  :
No: ()

False <= le_nat(s(nn1), z)  :
No: ()

False <= le_nat(z, z)  :
No: ()

leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2)  :
No: ()

leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2))  :
No: ()

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
Yes: {
ta1 -> node(a, node(b, leaf, _fxmuw_2), _ktmuw_2)  ;  ta2 -> leaf  ;  tb1 -> node(a, _mtmuw_1, node(b, _gxmuw_1, node(_kwmuw_0, _kwmuw_1, _kwmuw_2)))  ;  tb2 -> node(b, _ntmuw_1, _ntmuw_2)
}

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
eb -> b  ;  ta1 -> leaf  ;  ta2 -> node(_xtmuw_0, _xtmuw_1, _xtmuw_2)  ;  tb1 -> leaf  ;  tb2 -> leaf
}

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
eb -> b  ;  ta1 -> node(b, leaf, _kvmuw_2)  ;  tb1 -> leaf  ;  tb2 -> node(b, _gwmuw_1, node(_kwmuw_0, _kwmuw_1, _kwmuw_2))
}


-------------------------------------------
Step 6, which took 0.048815 s (model generation: 0.047981,  model checking: 0.000834):

Clauses:
{
height(leaf, z) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb) -> 0
subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb) -> 0
height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
le_nat(s(z), s(s(z))) <= True
le_nat(z, s(z)) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
False <= height(node(b, leaf, leaf), s(z))
False <= le_nat(s(s(z)), s(z))
False <= le_nat(s(z), s(z))
False <= le_nat(s(z), z)
False <= le_nat(z, z)
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
subtree(node(a, node(a, node(b, leaf, leaf), leaf), leaf), node(a, node(a, leaf, node(b, leaf, node(a, leaf, leaf))), node(b, leaf, leaf))) <= subtree(leaf, node(b, leaf, leaf)) /\ subtree(node(a, node(b, leaf, leaf), leaf), node(a, leaf, node(b, leaf, node(a, leaf, leaf))))
False <= subtree(node(a, leaf, leaf), leaf)
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(b, leaf, leaf), node(b, leaf, leaf)) <= subtree(node(a, node(b, leaf, leaf), leaf), node(a, node(b, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
False <= subtree(node(b, leaf, node(a, leaf, leaf)), node(b, leaf, leaf))
subtree(node(b, leaf, leaf), leaf) <= subtree(node(b, node(b, leaf, leaf), leaf), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
}

Current best model:
|_
name: None

height ->
[
height : <etree * nat>
{
  _r_1(a) <= True
  height(leaf, z) <= True
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_0)
}
]


;
le_nat ->
[
le_nat : <nat * nat>
{
  le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0)
  le_nat(z, s(x_1_0)) <= True
}
]


;
leq_nat ->
[
leq_nat : <nat * nat>
{
  leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0)
  leq_nat(z, s(x_1_0)) <= True
  leq_nat(z, z) <= True
}
]


;
subtree ->
[
subtree : <etree * etree>
{
  _r_1(a) <= True
  subtree(leaf, leaf) <= True
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_0_0) /\ subtree(x_0_1, x_1_2)
}
]



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




Answer of teacher:

height(leaf, z) <= True  :
No: ()

le_nat(z, s(nn2)) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

height(node(e, t1, t2), s(_aeb)) \/ le_nat(_xdb, _ydb) <= height(t1, _aeb) /\ height(t1, _xdb) /\ height(t2, _ydb)  :
Yes: {
_aeb -> z  ;  _xdb -> z  ;  _ydb -> z  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
}

subtree(t1, t2) <= height(t1, _eeb) /\ height(t2, _feb) /\ leq_nat(_eeb, _feb)  :
Yes: {
_eeb -> s(z)  ;  _feb -> s(z)  ;  t1 -> node(a, node(b, _sfnuw_1, _sfnuw_2), _fzmuw_2)  ;  t2 -> node(a, _gzmuw_1, node(_tfnuw_0, _tfnuw_1, _tfnuw_2))
}

height(node(e, t1, t2), s(_zdb)) <= height(t1, _xdb) /\ height(t2, _ydb) /\ height(t2, _zdb) /\ le_nat(_xdb, _ydb)  :
Yes: {
_xdb -> z  ;  _ydb -> s(_izmuw_0)  ;  _zdb -> s(_jzmuw_0)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(a, _lzmuw_1, _lzmuw_2)
}

le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2)  :
No: ()

le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2))  :
No: ()

False <= le_nat(s(nn1), z)  :
No: ()

False <= le_nat(z, z)  :
No: ()

leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2)  :
No: ()

leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2))  :
No: ()

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
Yes: {
eb -> b  ;  ta1 -> leaf  ;  ta2 -> leaf  ;  tb1 -> node(_tbnuw_0, _tbnuw_1, _tbnuw_2)  ;  tb2 -> node(_ubnuw_0, _ubnuw_1, _ubnuw_2)
}

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
eb -> a  ;  ta1 -> leaf  ;  ta2 -> node(_sdnuw_0, _sdnuw_1, _sdnuw_2)  ;  tb1 -> node(_tdnuw_0, _tdnuw_1, _tdnuw_2)  ;  tb2 -> leaf
}

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ea -> a  ;  eb -> b  ;  ta1 -> leaf  ;  tb2 -> node(_nfnuw_0, _nfnuw_1, _nfnuw_2)
}

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
eb -> a  ;  ta1 -> node(a, leaf, _tenuw_2)  ;  tb1 -> leaf  ;  tb2 -> node(_jfnuw_0, _jfnuw_1, node(_nfnuw_0, _nfnuw_1, _nfnuw_2))
}


Total time: 0.160588
Learner time: 0.135463
Teacher time: 0.002944
Reasons for stopping: No: Contradictory set of ground constraints:
{
False <= True
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
height(node(b, leaf, node(a, leaf, leaf)), s(s(z))) <= True
le_nat(s(z), s(s(z))) <= True
le_nat(z, s(z)) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
subtree(node(b, leaf, leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
subtree(node(a, node(b, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ height(node(a, node(b, leaf, leaf), leaf), s(z))
False <= height(node(b, leaf, leaf), s(z))
False <= le_nat(s(s(z)), s(z))
False <= le_nat(s(z), s(z))
False <= le_nat(s(z), z)
False <= le_nat(z, z)
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
subtree(node(a, node(a, node(b, leaf, leaf), leaf), leaf), node(a, node(a, leaf, node(b, leaf, node(a, leaf, leaf))), node(b, leaf, leaf))) <= subtree(leaf, node(b, leaf, leaf)) /\ subtree(node(a, node(b, leaf, leaf), leaf), node(a, leaf, node(b, leaf, node(a, leaf, leaf))))
False <= subtree(node(a, leaf, leaf), leaf)
False <= subtree(node(a, leaf, leaf), node(b, leaf, node(a, leaf, leaf)))
False <= subtree(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf))))
False <= subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(b, leaf, leaf), node(b, leaf, leaf)) <= subtree(node(a, node(b, leaf, leaf), leaf), node(a, node(b, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
False <= subtree(node(b, leaf, node(a, leaf, leaf)), node(b, leaf, leaf))
subtree(node(b, leaf, leaf), leaf) <= subtree(node(b, node(b, leaf, leaf), leaf), node(b, leaf, node(b, leaf, node(a, leaf, leaf))))
}