Solving ../../benchmarks/smtlib/false/tree_shallow_leq_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)
}
)
(max, F:
{
leq_nat(n, m) \/ max(n, m, n) <= True
max(n, m, m) <= leq_nat(n, m)
}
eq_nat(_pab, _qab) <= max(_nab, _oab, _pab) /\ max(_nab, _oab, _qab)
)
(height, F:
{
height(leaf, z) <= True
height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab)
height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab)
}
eq_nat(_wab, _xab) <= height(_vab, _wab) /\ height(_vab, _xab)
)
(shallower, P:
{
shallower(leaf, n) <= True
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m)
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m))
shallower(t1, m) <= shallower(node(e, t1, t2), s(m))
False <= shallower(node(e, t1, t2), z)
}
)
(height_rel, P:
{
height_rel(leaf, z) <= True
shallower(t1, nn) <= height_rel(t1, nn) /\ height_rel(node(e, t1, t2), s(nn))
height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn)
height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn))
height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn)
False <= height_rel(leaf, s(nn))
height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn))
False <= height_rel(node(e, t1, t2), z)
}
)
}

properties:
{
eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab)
}


over-approximation: {height, height_rel, max}
under-approximation: {height}

Clause system for inference is:

{
height_rel(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
shallower(leaf, n) <= True -> 0
height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab) -> 0
height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab) -> 0
eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab) -> 0
height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn) -> 0
height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn)) -> 0
height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn) -> 0
height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn)) -> 0
max(n, m, m) <= leq_nat(n, m) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m) -> 0
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
False <= shallower(node(e, t1, t2), z) -> 0
}


Solving took 0.817152 seconds.
No: Contradictory set of ground constraints:
{
False <= True
height_rel(leaf, z) <= True
height_rel(node(a, leaf, leaf), s(z)) <= True
height_rel(node(a, leaf, leaf), z) <= True
height_rel(node(a, leaf, node(a, leaf, leaf)), s(z)) <= True
height_rel(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(z)) <= True
height_rel(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
height_rel(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(z)) <= True
height_rel(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(z)) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(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
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
shallower(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
False <= height_rel(leaf, s(z))
False <= height_rel(node(a, leaf, leaf), s(s(z)))
False <= height_rel(node(a, leaf, node(a, leaf, leaf)), z)
False <= height_rel(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z)))
False <= height_rel(node(a, node(a, leaf, leaf), leaf), s(z))
False <= height_rel(node(a, node(a, leaf, leaf), leaf), z)
height_rel(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) \/ shallower(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), z) <= height_rel(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), z) /\ height_rel(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))), s(z))
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= shallower(node(a, leaf, leaf), z)
False <= shallower(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= shallower(node(a, node(a, leaf, leaf), leaf), s(z))
}
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006174 s (model generation: 0.006031,  model checking: 0.000143):

Clauses:
{
height_rel(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
shallower(leaf, n) <= True -> 0
height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab) -> 0
height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab) -> 0
eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab) -> 0
height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn) -> 0
height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn)) -> 0
height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn) -> 0
height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn)) -> 0
max(n, m, m) <= leq_nat(n, m) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m) -> 0
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
False <= shallower(node(e, t1, t2), z) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


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


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


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



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




Answer of teacher:

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

}

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

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

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

height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab)  :
No: ()

height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab)  :
No: ()

eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab)  :
No: ()

height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn)  :
No: ()

height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn))  :
No: ()

height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn)  :
No: ()

height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn))  :
No: ()

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

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

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

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

shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m)  :
No: ()

shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m))  :
No: ()

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
No: ()

False <= shallower(node(e, t1, t2), z)  :
No: ()


-------------------------------------------
Step 1, which took 0.006791 s (model generation: 0.006439,  model checking: 0.000352):

Clauses:
{
height_rel(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
shallower(leaf, n) <= True -> 0
height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab) -> 0
height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab) -> 0
eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab) -> 0
height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn) -> 0
height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn)) -> 0
height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn) -> 0
height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn)) -> 0
max(n, m, m) <= leq_nat(n, m) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m) -> 0
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
False <= shallower(node(e, t1, t2), z) -> 0
}

Accumulated learning constraints:
{
height_rel(leaf, z) <= True
leq_nat(z, z) <= True
shallower(leaf, z) <= True
}

Current best model:
|_
name: None

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


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


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


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


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



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




Answer of teacher:

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

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

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

shallower(leaf, n) <= True  :
Yes: {
n -> s(_zfuqw_0)
}

height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab)  :
No: ()

height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab)  :
No: ()

eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab)  :
No: ()

height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn)  :
Yes: {
nn -> z  ;  t1 -> leaf
}

height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn))  :
No: ()

height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn)  :
Yes: {
nn -> z  ;  t1 -> node(_dguqw_0, _dguqw_1, _dguqw_2)  ;  t2 -> leaf
}

height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn))  :
No: ()

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

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: ()

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

shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m)  :
Yes: {
m -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m))  :
No: ()

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
No: ()

False <= shallower(node(e, t1, t2), z)  :
No: ()


-------------------------------------------
Step 2, which took 0.011239 s (model generation: 0.010907,  model checking: 0.000332):

Clauses:
{
height_rel(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
shallower(leaf, n) <= True -> 0
height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab) -> 0
height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab) -> 0
eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab) -> 0
height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn) -> 0
height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn)) -> 0
height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn) -> 0
height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn)) -> 0
max(n, m, m) <= leq_nat(n, m) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m) -> 0
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
False <= shallower(node(e, t1, t2), z) -> 0
}

Accumulated learning constraints:
{
height_rel(leaf, z) <= True
height_rel(node(a, leaf, leaf), s(z)) <= True
height_rel(node(a, leaf, leaf), z) \/ height_rel(node(a, node(a, leaf, leaf), leaf), s(z)) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(s(z), z) \/ max(s(z), z, s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
max(z, z, z) <= True
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
}

Current best model:
|_
name: None

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


;
height_rel ->
[
height_rel : <etree * nat>
{
  height_rel(leaf, z) <= True
  height_rel(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  height_rel(node(x_0_0, x_0_1, x_0_2), z) <= 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
}
]


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


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



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




Answer of teacher:

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

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

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

shallower(leaf, n) <= True  :
No: ()

height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab)  :
No: ()

height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab)  :
No: ()

eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab)  :
Yes: {
_yab -> z  ;  m -> z  ;  n -> z  ;  t1 -> node(_riuqw_0, _riuqw_1, _riuqw_2)  ;  t2 -> leaf  ;  u -> z
}

height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn)  :
No: ()

height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn))  :
No: ()

height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn)  :
No: ()

height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn))  :
Yes: {
nn -> s(_gjuqw_0)  ;  t1 -> leaf  ;  t2 -> leaf
}

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

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

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

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

}

shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m)  :
No: ()

shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m))  :
Yes: {
m -> z  ;  t1 -> leaf  ;  t2 -> node(_rjuqw_0, _rjuqw_1, _rjuqw_2)
}

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
Yes: {
m -> z  ;  t1 -> node(_tjuqw_0, _tjuqw_1, _tjuqw_2)
}

False <= shallower(node(e, t1, t2), z)  :
No: ()


-------------------------------------------
Step 3, which took 0.012083 s (model generation: 0.011646,  model checking: 0.000437):

Clauses:
{
height_rel(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
shallower(leaf, n) <= True -> 0
height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab) -> 0
height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab) -> 0
eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab) -> 0
height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn) -> 0
height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn)) -> 0
height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn) -> 0
height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn)) -> 0
max(n, m, m) <= leq_nat(n, m) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m) -> 0
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
False <= shallower(node(e, t1, t2), z) -> 0
}

Accumulated learning constraints:
{
height_rel(leaf, z) <= True
height_rel(node(a, leaf, leaf), s(z)) <= True
height_rel(node(a, leaf, leaf), z) \/ height_rel(node(a, node(a, leaf, leaf), leaf), s(z)) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
max(s(z), z, s(z)) <= True
max(z, z, z) <= True
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
height_rel(leaf, s(z)) <= height_rel(node(a, leaf, leaf), s(s(z)))
False <= height_rel(node(a, leaf, leaf), z) /\ height_rel(node(a, node(a, leaf, leaf), leaf), z)
False <= leq_nat(s(z), z)
shallower(node(a, leaf, leaf), z) <= shallower(node(a, leaf, node(a, leaf, leaf)), s(z))
shallower(node(a, leaf, leaf), z) <= shallower(node(a, node(a, leaf, leaf), leaf), s(z))
}

Current best model:
|_
name: None

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


;
height_rel ->
[
height_rel : <etree * nat>
{
  height_rel(leaf, s(x_1_0)) <= True
  height_rel(leaf, z) <= True
  height_rel(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= 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
}
]


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


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



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




Answer of teacher:

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

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

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

shallower(leaf, n) <= True  :
No: ()

height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab)  :
No: ()

height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab)  :
No: ()

eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab)  :
Yes: {
_yab -> s(_ujuqw_0)  ;  m -> z  ;  n -> s(_wjuqw_0)  ;  t1 -> leaf  ;  t2 -> leaf  ;  u -> s(z)
}

height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn)  :
No: ()

height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn))  :
No: ()

height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn)  :
No: ()

height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn))  :
Yes: {
nn -> z  ;  t1 -> node(_nkuqw_0, _nkuqw_1, _nkuqw_2)  ;  t2 -> node(_okuqw_0, _okuqw_1, _okuqw_2)
}

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

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

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

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

shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m)  :
No: ()

shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m))  :
No: ()

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
No: ()

False <= shallower(node(e, t1, t2), z)  :
Yes: {

}


-------------------------------------------
Step 4, which took 0.087298 s (model generation: 0.017077,  model checking: 0.070221):

Clauses:
{
height_rel(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
shallower(leaf, n) <= True -> 0
height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab) -> 0
height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab) -> 0
eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab) -> 0
height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn) -> 0
height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn)) -> 0
height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn) -> 0
height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn)) -> 0
max(n, m, m) <= leq_nat(n, m) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m) -> 0
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
False <= shallower(node(e, t1, t2), z) -> 0
}

Accumulated learning constraints:
{
height_rel(leaf, z) <= True
height_rel(node(a, leaf, leaf), s(z)) <= True
height_rel(node(a, leaf, leaf), z) \/ height_rel(node(a, node(a, leaf, leaf), leaf), s(z)) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
False <= height_rel(leaf, s(z))
False <= height_rel(node(a, leaf, leaf), s(s(z)))
False <= height_rel(node(a, leaf, leaf), z) /\ height_rel(node(a, node(a, leaf, leaf), leaf), z)
height_rel(node(a, leaf, leaf), z) <= height_rel(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= shallower(node(a, leaf, leaf), z)
False <= shallower(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= shallower(node(a, node(a, leaf, leaf), leaf), s(z))
}

Current best model:
|_
name: None

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


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


;
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
}
]


;
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
}
]


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



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




Answer of teacher:

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

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

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

shallower(leaf, n) <= True  :
No: ()

height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab)  :
No: ()

height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab)  :
No: ()

eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab)  :
Yes: {
_yab -> s(_lluqw_0)  ;  m -> z  ;  n -> s(z)  ;  t1 -> node(_oluqw_0, _oluqw_1, leaf)  ;  t2 -> leaf  ;  u -> s(z)
}

height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn)  :
Yes: {
nn -> z  ;  t1 -> leaf  ;  t2 -> node(_ypuqw_0, _ypuqw_1, _ypuqw_2)
}

height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn))  :
Yes: {
nn -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_xluqw_0, node(_mquqw_0, _mquqw_1, _mquqw_2), leaf)
}

height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn)  :
No: ()

height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn))  :
No: ()

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

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

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

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

shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m)  :
No: ()

shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m))  :
No: ()

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
No: ()

False <= shallower(node(e, t1, t2), z)  :
No: ()


-------------------------------------------
Step 5, which took 0.023052 s (model generation: 0.021188,  model checking: 0.001864):

Clauses:
{
height_rel(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
shallower(leaf, n) <= True -> 0
height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab) -> 0
height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab) -> 0
eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab) -> 0
height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn) -> 0
height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn)) -> 0
height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn) -> 0
height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn)) -> 0
max(n, m, m) <= leq_nat(n, m) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m) -> 0
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
False <= shallower(node(e, t1, t2), z) -> 0
}

Accumulated learning constraints:
{
height_rel(leaf, z) <= True
height_rel(node(a, leaf, leaf), s(z)) <= True
height_rel(node(a, leaf, leaf), z) <= True
height_rel(node(a, leaf, node(a, leaf, leaf)), s(z)) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(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
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
False <= height_rel(leaf, s(z))
False <= height_rel(node(a, leaf, leaf), s(s(z)))
False <= height_rel(node(a, node(a, leaf, leaf), leaf), s(z))
False <= height_rel(node(a, node(a, leaf, leaf), leaf), z)
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= shallower(node(a, leaf, leaf), z)
False <= shallower(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= shallower(node(a, node(a, leaf, leaf), leaf), s(z))
}

Current best model:
|_
name: None

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


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


;
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
}
]


;
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
}
]


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



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




Answer of teacher:

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

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

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

shallower(leaf, n) <= True  :
No: ()

height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab)  :
No: ()

height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab)  :
No: ()

eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab)  :
Yes: {
_yab -> z  ;  m -> z  ;  n -> z  ;  t1 -> leaf  ;  t2 -> node(_ajxqw_0, leaf, _ajxqw_2)  ;  u -> z
}

height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn)  :
Yes: {
nn -> z  ;  t1 -> leaf  ;  t2 -> node(_nrxqw_0, node(_lrxqw_0, _lrxqw_1, _lrxqw_2), _nrxqw_2)
}

height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn))  :
Yes: {
nn -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_jmxqw_0, leaf, node(_fsxqw_0, leaf, _fsxqw_2))
}

height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn)  :
Yes: {
nn -> z  ;  t1 -> node(_anxqw_0, node(_srxqw_0, _srxqw_1, _srxqw_2), _anxqw_2)  ;  t2 -> leaf
}

height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn))  :
No: ()

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

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

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

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

shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m)  :
Yes: {
m -> s(_upxqw_0)  ;  t1 -> leaf  ;  t2 -> node(_wpxqw_0, leaf, leaf)
}

shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m))  :
No: ()

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
No: ()

False <= shallower(node(e, t1, t2), z)  :
No: ()


-------------------------------------------
Step 6, which took 0.656103 s (model generation: 0.056780,  model checking: 0.599323):

Clauses:
{
height_rel(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
shallower(leaf, n) <= True -> 0
height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab) -> 0
height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab) -> 0
eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab) -> 0
height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn) -> 0
height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn)) -> 0
height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn) -> 0
height_rel(t1, nn) \/ height_rel(t2, nn) <= height_rel(node(e, t1, t2), s(nn)) -> 0
max(n, m, m) <= leq_nat(n, m) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m) -> 0
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
False <= shallower(node(e, t1, t2), z) -> 0
}

Accumulated learning constraints:
{
height_rel(leaf, z) <= True
height_rel(node(a, leaf, leaf), s(z)) <= True
height_rel(node(a, leaf, leaf), z) <= True
height_rel(node(a, leaf, node(a, leaf, leaf)), s(z)) <= True
height_rel(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(z)) <= True
height_rel(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(z)) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(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
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
shallower(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
False <= height_rel(leaf, s(z))
False <= height_rel(node(a, leaf, leaf), s(s(z)))
False <= height_rel(node(a, leaf, node(a, leaf, leaf)), z)
False <= height_rel(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z)))
False <= height_rel(node(a, node(a, leaf, leaf), leaf), s(z))
False <= height_rel(node(a, node(a, leaf, leaf), leaf), z)
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= shallower(node(a, leaf, leaf), z)
False <= shallower(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= shallower(node(a, node(a, leaf, leaf), leaf), s(z))
}

Current best model:
|_
name: None

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


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


;
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
}
]


;
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
}
]


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



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




Answer of teacher:

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

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

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

shallower(leaf, n) <= True  :
No: ()

height(node(e, t1, t2), s(_uab)) \/ leq_nat(_rab, _sab) <= height(t1, _rab) /\ height(t1, _uab) /\ height(t2, _sab)  :
No: ()

height(node(e, t1, t2), s(_tab)) <= height(t1, _rab) /\ height(t2, _sab) /\ height(t2, _tab) /\ leq_nat(_rab, _sab)  :
No: ()

eq_nat(u, s(_yab)) <= height_rel(t1, n) /\ height_rel(t2, m) /\ height_rel(node(e, t1, t2), u) /\ max(n, m, _yab)  :
Yes: {
_yab -> z  ;  m -> z  ;  n -> z  ;  t1 -> leaf  ;  t2 -> leaf  ;  u -> z
}

height_rel(node(e, t1, t2), s(nn)) <= height_rel(t1, nn) /\ shallower(t1, nn)  :
Yes: {
nn -> s(z)  ;  t1 -> node(_vdyqw_0, leaf, leaf)
}

height_rel(t1, nn) \/ shallower(t2, nn) <= height_rel(t2, nn) /\ height_rel(node(e, t1, t2), s(nn))  :
Yes: {
nn -> z  ;  t1 -> node(_tlyqw_0, node(_bnzqw_0, _bnzqw_1, _bnzqw_2), node(_wlzqw_0, leaf, _wlzqw_2))  ;  t2 -> node(_ulyqw_0, node(_opzqw_0, node(_pxzqw_0, _pxzqw_1, _pxzqw_2), _opzqw_2), node(_npzqw_0, node(_drzqw_0, _drzqw_1, _drzqw_2), _npzqw_2))
}

height_rel(t1, nn) \/ height_rel(node(e, t1, t2), s(nn)) <= height_rel(t2, nn) /\ shallower(t2, nn)  :
Yes: {
nn -> z  ;  t1 -> node(_jwyqw_0, leaf, node(_cnzqw_0, leaf, _cnzqw_2))  ;  t2 -> leaf
}

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

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

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

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

shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m)  :
No: ()

shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m))  :
No: ()

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
No: ()

False <= shallower(node(e, t1, t2), z)  :
No: ()


Total time: 0.817152
Learner time: 0.130068
Teacher time: 0.672672
Reasons for stopping: No: Contradictory set of ground constraints:
{
False <= True
height_rel(leaf, z) <= True
height_rel(node(a, leaf, leaf), s(z)) <= True
height_rel(node(a, leaf, leaf), z) <= True
height_rel(node(a, leaf, node(a, leaf, leaf)), s(z)) <= True
height_rel(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(z)) <= True
height_rel(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
height_rel(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(z)) <= True
height_rel(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(z)) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(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
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
shallower(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
False <= height_rel(leaf, s(z))
False <= height_rel(node(a, leaf, leaf), s(s(z)))
False <= height_rel(node(a, leaf, node(a, leaf, leaf)), z)
False <= height_rel(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z)))
False <= height_rel(node(a, node(a, leaf, leaf), leaf), s(z))
False <= height_rel(node(a, node(a, leaf, leaf), leaf), z)
height_rel(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) \/ shallower(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), z) <= height_rel(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), z) /\ height_rel(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))), s(z))
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= shallower(node(a, leaf, leaf), z)
False <= shallower(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= shallower(node(a, node(a, leaf, leaf), leaf), s(z))
}