Solving ../../benchmarks/smtlib/true/tree_depth_leq_size.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, P:
{
leq(z, n2) <= True
leq(s(nn1), s(nn2)) <= leq(nn1, nn2)
leq(nn1, nn2) <= leq(s(nn1), s(nn2))
False <= leq(s(nn1), z)
}
)
(max, F:
{
leq(n, m) \/ max(n, m, n) <= True
max(n, m, m) <= leq(n, m)
}
eq_nat(_hsa, _isa) <= max(_fsa, _gsa, _hsa) /\ max(_fsa, _gsa, _isa)
)
(plus, F:
{
plus(n, z, n) <= True
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)
}
eq_nat(_msa, _nsa) <= plus(_ksa, _lsa, _msa) /\ plus(_ksa, _lsa, _nsa)
)
(height, F:
{
height(leaf, z) <= True
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)
}
eq_nat(_ssa, _tsa) <= height(_rsa, _ssa) /\ height(_rsa, _tsa)
)
(numnodes, F:
{
numnodes(leaf, z) <= True
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)
}
eq_nat(_ysa, _zsa) <= numnodes(_xsa, _ysa) /\ numnodes(_xsa, _zsa)
)
}

properties:
{
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)
}


over-approximation: {height, max, numnodes, plus}
under-approximation: {}

Clause system for inference is:

{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}


Solving took 13.239238 seconds.
Yes: |_
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)) <= height(x_0_1, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), z) <= True
}
]


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


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


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


;
plus ->
[
plus : <nat * nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= leq(x_0_0, x_2_0) /\ leq(x_1_0, x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= leq(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= leq(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



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

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


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


;
numnodes ->
[
numnodes : <etree * nat>
{
  
}
]


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



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




Answer of teacher:

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

}

leq(n, m) \/ max(n, m, n) <= True  :
Yes: {
m -> z  ;  n -> z
}

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

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

}

plus(n, z, n) <= True  :
Yes: {
n -> z
}

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
No: ()

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
No: ()

max(n, m, m) <= leq(n, m)  :
No: ()

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
No: ()

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
No: ()


-------------------------------------------
Step 1, which took 0.007742 s (model generation: 0.007599,  model checking: 0.000143):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
leq(z, z) <= True
numnodes(leaf, z) <= True
plus(z, z, z) <= True
}

Current best model:
|_
name: None

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


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
Yes: {
m -> z  ;  n -> s(_sxgve_0)
}

leq(z, n2) <= True  :
Yes: {
n2 -> s(_vxgve_0)
}

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

plus(n, z, n) <= True  :
Yes: {
n -> s(_wxgve_0)
}

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
No: ()

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
No: ()

max(n, m, m) <= leq(n, m)  :
Yes: {
m -> z  ;  n -> z
}

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
Yes: {
_usa -> z  ;  _vsa -> z  ;  _wsa -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
Yes: {
_jsa -> z  ;  mm -> z  ;  n -> z
}


-------------------------------------------
Step 2, which took 0.009308 s (model generation: 0.009186,  model checking: 0.000122):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
leq(s(z), s(z)) <= True
leq(s(z), z) \/ max(s(z), z, s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
}

Current best model:
|_
name: None

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


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
No: ()

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
Yes: {
_osa -> z  ;  _psa -> z  ;  _qsa -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

max(n, m, m) <= leq(n, m)  :
Yes: {
m -> z  ;  n -> s(_rygve_0)
}

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

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

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

}

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
No: ()

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
Yes: {
_jsa -> s(_uygve_0)  ;  mm -> z  ;  n -> s(_wygve_0)
}


-------------------------------------------
Step 3, which took 0.012649 s (model generation: 0.012549,  model checking: 0.000100):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(z), z, s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= leq(s(z), 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
}
]


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
No: ()

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
No: ()

max(n, m, m) <= leq(n, m)  :
Yes: {
m -> s(_zygve_0)  ;  n -> z
}

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
No: ()

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
No: ()


-------------------------------------------
Step 4, which took 0.011727 s (model generation: 0.011491,  model checking: 0.000236):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= leq(s(s(z)), s(z))
False <= leq(s(z), 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
}
]


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
Yes: {
m -> s(z)  ;  n -> s(s(_wzgve_0))
}

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
Yes: {
_ata -> s(s(_wzgve_0))  ;  _bta -> s(z)  ;  t1 -> node(_hzgve_0, _hzgve_1, _hzgve_2)
}

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
No: ()

max(n, m, m) <= leq(n, m)  :
Yes: {
m -> s(z)  ;  n -> s(z)
}

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
No: ()

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
No: ()


-------------------------------------------
Step 5, which took 0.011425 s (model generation: 0.011161,  model checking: 0.000264):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(node(a, leaf, leaf), s(s(z)))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), 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)) <= numnodes(x_0_2, x_1_0)
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
Yes: {
_ata -> s(s(_obhve_0))  ;  _bta -> s(z)  ;  t1 -> node(_gahve_0, _gahve_1, node(_qbhve_0, _qbhve_1, _qbhve_2))
}

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
Yes: {
_osa -> s(s(_ubhve_0))  ;  _psa -> z  ;  _qsa -> s(_tahve_0)  ;  t1 -> node(_uahve_0, _uahve_1, node(_tbhve_0, _tbhve_1, _tbhve_2))  ;  t2 -> leaf
}

max(n, m, m) <= leq(n, m)  :
No: ()

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
No: ()

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
No: ()


-------------------------------------------
Step 6, which took 0.014563 s (model generation: 0.014350,  model checking: 0.000213):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(node(a, leaf, leaf), s(s(z)))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) /\ max(s(s(z)), z, s(z))
False <= height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), 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)) <= numnodes(x_0_1, x_1_0)
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
Yes: {
_ata -> s(s(_fdhve_0))  ;  _bta -> s(z)  ;  t1 -> node(_xbhve_0, node(_hdhve_0, _hdhve_1, _hdhve_2), _xbhve_2)
}

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
Yes: {
_osa -> z  ;  _psa -> s(s(_ldhve_0))  ;  _qsa -> s(_fchve_0)  ;  t1 -> leaf  ;  t2 -> node(_hchve_0, node(_kdhve_0, _kdhve_1, _kdhve_2), _hchve_2)
}

max(n, m, m) <= leq(n, m)  :
No: ()

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
No: ()

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
No: ()


-------------------------------------------
Step 7, which took 0.015947 s (model generation: 0.015628,  model checking: 0.000319):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(node(a, leaf, leaf), s(s(z)))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) /\ max(s(s(z)), z, s(z))
False <= height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z))
False <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), 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)) <= height(x_0_1, x_1_0) /\ height(x_0_2, x_1_0)
}
]


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
Yes: {
_ata -> s(s(z))  ;  _bta -> s(z)  ;  t1 -> node(_odhve_0, node(_qfhve_0, leaf, leaf), node(_qfhve_0, leaf, leaf))
}

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
Yes: {
_osa -> z  ;  _psa -> s(z)  ;  _qsa -> s(_wdhve_0)  ;  t1 -> leaf  ;  t2 -> node(_ydhve_0, leaf, leaf)
}

max(n, m, m) <= leq(n, m)  :
No: ()

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
No: ()

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
No: ()


-------------------------------------------
Step 8, which took 0.017480 s (model generation: 0.017015,  model checking: 0.000465):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(node(a, leaf, leaf), s(s(z)))
height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z))
False <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= max(s(s(z)), z, s(z))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), 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)) <= height(x_0_1, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
}
]


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
No: ()

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
Yes: {
_osa -> z  ;  _psa -> s(z)  ;  _qsa -> s(s(_hkhve_0))  ;  t1 -> leaf  ;  t2 -> node(_rghve_0, leaf, leaf)
}

max(n, m, m) <= leq(n, m)  :
No: ()

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
Yes: {
_usa -> z  ;  _vsa -> s(z)  ;  _wsa -> s(_nihve_0)  ;  t1 -> leaf  ;  t2 -> node(_pihve_0, leaf, leaf)
}

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
No: ()


-------------------------------------------
Step 9, which took 0.021700 s (model generation: 0.021243,  model checking: 0.000457):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(node(a, leaf, leaf), s(s(z)))
height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z))
False <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= max(s(s(z)), z, s(z))
height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
}

Current best model:
|_
name: None

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


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
Yes: {
_ata -> s(_qkhve_0)  ;  _bta -> z  ;  t1 -> leaf
}

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
Yes: {
_osa -> z  ;  _psa -> s(_mlhve_0)  ;  _qsa -> s(_nlhve_0)  ;  t1 -> leaf  ;  t2 -> leaf
}

max(n, m, m) <= leq(n, m)  :
No: ()

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
Yes: {
_usa -> z  ;  _vsa -> s(z)  ;  _wsa -> s(s(_oohve_0))  ;  t1 -> leaf  ;  t2 -> node(_inhve_0, _inhve_1, leaf)
}

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
No: ()


-------------------------------------------
Step 10, which took 0.071133 s (model generation: 0.070159,  model checking: 0.000974):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(leaf, s(z))
False <= height(node(a, leaf, leaf), s(s(z)))
height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z))
False <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= max(s(s(z)), z, s(z))
height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

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


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
Yes: {
_ata -> s(s(s(_evhve_0)))  ;  _bta -> s(s(z))  ;  t1 -> node(_uohve_0, node(_ruhve_0, leaf, leaf), node(_ouhve_0, leaf, leaf))
}

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
No: ()

max(n, m, m) <= leq(n, m)  :
No: ()

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
Yes: {
_usa -> z  ;  _vsa -> s(s(z))  ;  _wsa -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_fthve_0, leaf, node(_cwhve_0, leaf, leaf))
}

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
No: ()


-------------------------------------------
Step 11, which took 0.121799 s (model generation: 0.121248,  model checking: 0.000551):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(leaf, s(z))
False <= height(node(a, leaf, leaf), s(s(z)))
height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z))
False <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
leq(s(s(s(z))), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= max(s(s(z)), z, s(z))
height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= plus(z, s(s(z)), s(z))
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(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)) <= numnodes(x_0_2, x_1_0)
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), z) <= True
}
]


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
Yes: {
m -> z  ;  n -> s(s(_gcive_0))
}

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
Yes: {
_ata -> s(z)  ;  _bta -> z  ;  t1 -> node(_azhve_0, _azhve_1, node(_lcive_0, _lcive_1, _lcive_2))
}

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
Yes: {
_osa -> s(z)  ;  _psa -> z  ;  _qsa -> s(_nzhve_0)  ;  t1 -> node(_ozhve_0, _ozhve_1, node(_ycive_0, _ycive_1, _ycive_2))  ;  t2 -> leaf
}

max(n, m, m) <= leq(n, m)  :
Yes: {
m -> s(s(_gcive_0))  ;  n -> z
}

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
Yes: {
_usa -> z  ;  _vsa -> z  ;  _wsa -> z  ;  t1 -> node(_ybive_0, _ybive_1, _ybive_2)  ;  t2 -> node(_zbive_0, _zbive_1, _zbive_2)
}

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
Yes: {
_jsa -> s(z)  ;  mm -> s(_bcive_0)  ;  n -> z
}


-------------------------------------------
Step 12, which took 0.121827 s (model generation: 0.120563,  model checking: 0.001264):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
leq(s(s(z)), s(s(z))) <= True
leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(leaf, s(z))
False <= height(node(a, leaf, leaf), s(s(z)))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, leaf, node(a, leaf, leaf)), z)
height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z))
False <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
leq(s(s(s(z))), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
max(z, s(s(z)), s(s(z))) <= leq(z, s(s(z)))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= max(s(s(z)), z, s(z))
height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) <= numnodes(node(a, leaf, leaf), z)
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= plus(z, s(s(z)), s(z))
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

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


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
Yes: {
_ata -> s(s(s(_ghive_0)))  ;  _bta -> s(s(z))  ;  t1 -> node(_ddive_0, leaf, node(_wgive_0, _wgive_1, _wgive_2))
}

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
Yes: {
_osa -> s(z)  ;  _psa -> s(s(_mhive_0))  ;  _qsa -> s(s(_eiive_0))  ;  t1 -> node(_qeive_0, leaf, leaf)  ;  t2 -> node(_reive_0, leaf, node(_lhive_0, _lhive_1, _lhive_2))
}

max(n, m, m) <= leq(n, m)  :
No: ()

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
Yes: {
_usa -> z  ;  _vsa -> s(_sfive_0)  ;  _wsa -> s(_tfive_0)  ;  t1 -> leaf  ;  t2 -> leaf
}

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
No: ()


-------------------------------------------
Step 13, which took 0.110341 s (model generation: 0.109716,  model checking: 0.000625):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
leq(s(s(z)), s(s(z))) <= True
leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(leaf, s(z))
False <= height(node(a, leaf, leaf), s(s(z)))
leq(s(s(s(z))), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, leaf, node(a, leaf, leaf)), z)
height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z))
False <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
leq(s(s(s(z))), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
max(z, s(s(z)), s(s(z))) <= leq(z, s(s(z)))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= max(s(s(z)), z, s(z))
height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) <= max(s(z), s(s(z)), s(s(z)))
height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
numnodes(node(a, leaf, leaf), s(s(z))) <= numnodes(leaf, s(z))
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) <= numnodes(node(a, leaf, leaf), z)
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= plus(z, s(s(z)), s(z))
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(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)) <= height(x_0_2, x_1_0)
}
]


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
Yes: {
_ata -> s(z)  ;  _bta -> s(s(_qlive_0))  ;  t1 -> node(_jiive_0, _jiive_1, leaf)
}

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
Yes: {
_osa -> s(z)  ;  _psa -> s(z)  ;  _qsa -> s(s(_wmive_0))  ;  t1 -> node(_cjive_0, _cjive_1, leaf)  ;  t2 -> node(_djive_0, _djive_1, leaf)
}

max(n, m, m) <= leq(n, m)  :
No: ()

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
Yes: {
_usa -> s(z)  ;  _vsa -> s(s(s(z)))  ;  _wsa -> s(z)  ;  t1 -> node(_hlive_0, _hlive_1, leaf)  ;  t2 -> node(_ilive_0, _ilive_1, node(_umive_0, _umive_1, node(_ynive_0, _ynive_1, leaf)))
}

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
Yes: {
_jsa -> s(s(_jmive_0))  ;  mm -> s(z)  ;  n -> z
}


-------------------------------------------
Step 14, which took 0.160110 s (model generation: 0.159426,  model checking: 0.000684):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
leq(s(s(z)), s(s(z))) <= True
leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True
leq(s(z), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(leaf, s(z))
False <= height(node(a, leaf, leaf), s(s(z)))
leq(s(s(s(z))), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, leaf, node(a, leaf, leaf)), z)
height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z))
False <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
leq(s(s(s(z))), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
max(z, s(s(z)), s(s(z))) <= leq(z, s(s(z)))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= max(s(s(z)), z, s(z))
height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) <= max(s(z), s(s(z)), s(s(z)))
height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z)))
height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
numnodes(node(a, leaf, leaf), s(s(z))) <= numnodes(leaf, s(z))
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) <= numnodes(node(a, leaf, leaf), z)
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ plus(s(z), s(s(s(z))), s(z))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= plus(z, s(s(z)), s(z))
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z)))
plus(z, s(s(z)), s(s(s(z)))) <= plus(z, s(z), s(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)) <= height(x_0_2, x_1_0)
}
]


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
No: ()

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
Yes: {
_osa -> s(z)  ;  _psa -> z  ;  _qsa -> s(z)  ;  t1 -> node(_voive_0, _voive_1, leaf)  ;  t2 -> leaf
}

max(n, m, m) <= leq(n, m)  :
Yes: {
m -> s(s(_hsive_0))  ;  n -> s(z)
}

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
Yes: {
_usa -> z  ;  _vsa -> s(s(s(s(z))))  ;  _wsa -> s(s(z))  ;  t1 -> leaf  ;  t2 -> node(_tqive_0, _tqive_1, node(_rtive_0, _rtive_1, node(_ztive_0, _ztive_1, node(_quive_0, _quive_1, leaf))))
}

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
Yes: {
_jsa -> s(_mrive_0)  ;  mm -> z  ;  n -> s(s(_zrive_0))
}


-------------------------------------------
Step 15, which took 0.634932 s (model generation: 0.627606,  model checking: 0.007326):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) <= True
leq(s(s(z)), s(s(z))) <= True
leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True
leq(s(z), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(s(z)), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(leaf, s(z))
False <= height(node(a, leaf, leaf), s(s(z)))
leq(s(s(s(z))), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, leaf, node(a, leaf, leaf)), z)
leq(s(s(s(z))), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
max(z, s(s(z)), s(s(z))) <= leq(z, s(s(z)))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= max(s(s(z)), z, s(z))
height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z)))
height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z))
height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
numnodes(node(a, leaf, leaf), s(s(z))) <= numnodes(leaf, s(z))
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) <= numnodes(node(a, leaf, leaf), z)
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ plus(s(z), s(s(s(z))), s(z))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf))))), s(s(s(z)))) <= numnodes(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(s(s(z))))) /\ plus(z, s(s(s(s(z)))), s(s(z)))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
plus(s(s(z)), s(z), s(s(z))) <= plus(s(s(z)), z, s(z))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= plus(z, s(s(z)), s(z))
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z)))
plus(z, s(s(z)), s(s(s(z)))) <= plus(z, s(z), s(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)) <= height(x_0_1, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
}
]


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
Yes: {
_ata -> s(s(s(s(z))))  ;  _bta -> s(s(s(z)))  ;  t1 -> node(_dvive_0, leaf, node(_qkjve_0, node(_enjve_0, leaf, node(_wnjve_0, leaf, _wnjve_2)), _qkjve_2))
}

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
Yes: {
_osa -> s(z)  ;  _psa -> z  ;  _qsa -> s(s(_lnjve_0))  ;  t1 -> node(_zvive_0, leaf, leaf)  ;  t2 -> leaf
}

max(n, m, m) <= leq(n, m)  :
No: ()

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
Yes: {
_usa -> s(s(s(z)))  ;  _vsa -> z  ;  _wsa -> s(z)  ;  t1 -> node(_chjve_0, node(_etjve_0, node(_jukve_0, leaf, leaf), leaf), leaf)  ;  t2 -> leaf
}

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
No: ()


-------------------------------------------
Step 16, which took 0.489437 s (model generation: 0.486525,  model checking: 0.002912):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) <= True
leq(s(s(z)), s(s(z))) <= True
leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True
leq(s(z), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(s(z)), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(leaf, s(z))
False <= height(node(a, leaf, leaf), s(s(z)))
leq(s(s(s(z))), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, leaf, node(a, leaf, leaf)), z)
leq(s(s(s(s(z)))), s(s(s(z)))) <= height(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(s(z))))) /\ numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z))))
leq(s(s(s(z))), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
max(z, s(s(z)), s(s(z))) <= leq(z, s(s(z)))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= max(s(s(z)), z, s(z))
height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z)))
height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z)))
height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z))
height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
numnodes(node(a, leaf, leaf), s(s(z))) <= numnodes(leaf, s(z))
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) <= numnodes(node(a, leaf, leaf), z)
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ plus(s(z), s(s(s(z))), s(z))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf))))), s(s(s(z)))) <= numnodes(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(s(s(z))))) /\ plus(z, s(s(s(s(z)))), s(s(z)))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), z, s(z))
plus(s(s(z)), s(z), s(s(z))) <= plus(s(s(z)), z, s(z))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= plus(z, s(s(z)), s(z))
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z)))
plus(z, s(s(z)), s(s(s(z)))) <= plus(z, s(z), s(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)) <= height(x_0_1, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
}
]


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
No: ()

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
Yes: {
_osa -> z  ;  _psa -> s(s(z))  ;  _qsa -> s(s(s(_iamve_0)))  ;  t1 -> leaf  ;  t2 -> node(_bwkve_0, node(_tdlve_0, leaf, leaf), leaf)
}

max(n, m, m) <= leq(n, m)  :
No: ()

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
Yes: {
_usa -> s(s(z))  ;  _vsa -> s(z)  ;  _wsa -> s(z)  ;  t1 -> node(_eblve_0, leaf, node(_lnlve_0, leaf, leaf))  ;  t2 -> leaf
}

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
No: ()


-------------------------------------------
Step 17, which took 9.610078 s (model generation: 9.600128,  model checking: 0.009950):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) <= True
leq(s(s(z)), s(s(z))) <= True
leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True
leq(s(z), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(s(z)), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(leaf, s(z))
False <= height(node(a, leaf, leaf), s(s(z)))
leq(s(s(s(z))), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, leaf, node(a, leaf, leaf)), z)
leq(s(s(s(s(z)))), s(s(s(z)))) <= height(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(s(z))))) /\ numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z))))
leq(s(s(s(z))), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
max(z, s(s(z)), s(s(z))) <= leq(z, s(s(z)))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= max(s(s(z)), z, s(z))
height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z)))
height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z)))
height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(s(s(z))))) <= max(z, s(s(z)), s(s(s(z))))
height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z))
height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
numnodes(node(a, leaf, leaf), s(s(z))) <= numnodes(leaf, s(z))
numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ plus(s(s(z)), s(z), s(z))
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) <= numnodes(node(a, leaf, leaf), z)
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ plus(s(z), s(s(s(z))), s(z))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf))))), s(s(s(z)))) <= numnodes(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(s(s(z))))) /\ plus(z, s(s(s(s(z)))), s(s(z)))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), z, s(z))
plus(s(s(z)), s(z), s(s(z))) <= plus(s(s(z)), z, s(z))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= plus(z, s(s(z)), s(z))
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z)))
plus(z, s(s(z)), s(s(s(z)))) <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

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


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
Yes: {
_ata -> s(s(s(_emmve_0)))  ;  _bta -> s(z)  ;  t1 -> node(_cbmve_0, leaf, leaf)
}

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
Yes: {
_osa -> z  ;  _psa -> s(s(s(_emmve_0)))  ;  _qsa -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_wbmve_0, node(_hnmve_0, _hnmve_1, _hnmve_2), node(_sgove_0, _sgove_1, _sgove_2))
}

max(n, m, m) <= leq(n, m)  :
No: ()

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
No: ()

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
No: ()


-------------------------------------------
Step 18, which took 0.607376 s (model generation: 0.585361,  model checking: 0.022015):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta) -> 0
height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa) -> 0
plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) <= True
leq(s(s(z)), s(s(z))) <= True
leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True
leq(s(z), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(s(z)), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(leaf, s(z))
leq(s(s(s(z))), s(z)) <= height(node(a, leaf, leaf), s(s(s(z))))
False <= height(node(a, leaf, leaf), s(s(z)))
False <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, leaf, node(a, leaf, leaf)), z)
leq(s(s(s(s(z)))), s(s(s(z)))) <= height(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(s(z))))) /\ numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z))))
height(node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) /\ max(z, s(s(s(z))), s(z))
False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= leq(s(s(s(z))), s(s(z)))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
max(z, s(s(z)), s(s(z))) <= leq(z, s(s(z)))
height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= max(s(s(z)), z, s(z))
height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z)))
height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z)))
height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(s(s(z))))) <= max(z, s(s(z)), s(s(s(z))))
height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z))
False <= max(z, s(z), s(s(z)))
numnodes(node(a, leaf, leaf), s(s(z))) <= numnodes(leaf, s(z))
numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ plus(s(s(z)), s(z), s(z))
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) <= numnodes(node(a, leaf, leaf), z)
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ plus(s(z), s(s(s(z))), s(z))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf))))), s(s(s(z)))) <= numnodes(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(s(s(z))))) /\ plus(z, s(s(s(s(z)))), s(s(z)))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), z, s(z))
plus(s(s(z)), s(z), s(s(z))) <= plus(s(s(z)), z, s(z))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= plus(z, s(s(z)), s(z))
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z)))
plus(z, s(s(z)), s(s(s(z)))) <= plus(z, s(z), s(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)) <= height(x_0_1, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), z) <= True
}
]


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


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


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


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



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




Answer of teacher:

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

leq(n, m) \/ max(n, m, n) <= True  :
No: ()

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

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

plus(n, z, n) <= True  :
No: ()

leq(_ata, _bta) <= height(t1, _ata) /\ numnodes(t1, _bta)  :
No: ()

height(node(e, t1, t2), s(_qsa)) <= height(t1, _osa) /\ height(t2, _psa) /\ max(_osa, _psa, _qsa)  :
No: ()

max(n, m, m) <= leq(n, m)  :
No: ()

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

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

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

numnodes(node(e, t1, t2), s(_wsa)) <= numnodes(t1, _usa) /\ numnodes(t2, _vsa) /\ plus(_usa, _vsa, _wsa)  :
Yes: {
_usa -> s(s(z))  ;  _vsa -> s(s(z))  ;  _wsa -> s(z)  ;  t1 -> node(_znove_0, leaf, node(_qvove_0, leaf, leaf))  ;  t2 -> leaf
}

plus(n, s(mm), s(_jsa)) <= plus(n, mm, _jsa)  :
Yes: {
_jsa -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
}


Total time: 13.239238
Learner time: 12.007211
Teacher time: 0.048723
Reasons for stopping: Yes: |_
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)) <= height(x_0_1, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), z) <= True
}
]


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


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


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


;
plus ->
[
plus : <nat * nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= leq(x_0_0, x_2_0) /\ leq(x_1_0, x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= leq(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= leq(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



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