Solving ../../benchmarks/smtlib/false/tree_height_numnodes_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:
{
(not_empty, P:
{
not_empty(node(e, t1, t2)) <= True
False <= not_empty(leaf)
}
)
(leq_nat, P:
{
leq_nat(z, n2) <= True
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2)
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2))
False <= leq_nat(s(nn1), z)
}
)
(le_nat, P:
{
le_nat(z, s(nn2)) <= True
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2)
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2))
False <= le_nat(s(nn1), z)
False <= le_nat(z, z)
}
)
(max, F:
{
max(s(nn), z, s(nn)) <= True
max(z, m, m) <= True
max(s(nn), s(mm), s(_kjb)) <= max(nn, mm, _kjb)
}
eq_nat(_njb, _ojb) <= max(_ljb, _mjb, _njb) /\ max(_ljb, _mjb, _ojb)
)
(height, F:
{
height(leaf, z) <= True
height(node(e, t1, t2), s(_rjb)) <= height(t1, _pjb) /\ height(t2, _qjb) /\ max(_pjb, _qjb, _rjb)
}
eq_nat(_tjb, _ujb) <= height(_sjb, _tjb) /\ height(_sjb, _ujb)
)
(plus, F:
{
plus(n, z, n) <= True
plus(n, s(mm), s(_vjb)) <= plus(n, mm, _vjb)
}
eq_nat(_yjb, _zjb) <= plus(_wjb, _xjb, _yjb) /\ plus(_wjb, _xjb, _zjb)
)
(numnodes, F:
{
numnodes(leaf, z) <= True
numnodes(node(e, t1, t2), s(_ckb)) <= numnodes(t1, _akb) /\ numnodes(t2, _bkb) /\ plus(_akb, _bkb, _ckb)
}
eq_nat(_ekb, _fkb) <= numnodes(_dkb, _ekb) /\ numnodes(_dkb, _fkb)
)
}

properties:
{
le_nat(_gkb, _hkb) <= height(t, _gkb) /\ not_empty(t) /\ numnodes(t, _hkb)
}


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

Clause system for inference is:

{
height(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
not_empty(node(e, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
le_nat(_gkb, _hkb) <= height(t, _gkb) /\ not_empty(t) /\ numnodes(t, _hkb) -> 0
height(node(e, t1, t2), s(_rjb)) <= height(t1, _pjb) /\ height(t2, _qjb) /\ max(_pjb, _qjb, _rjb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
max(s(nn), s(mm), s(_kjb)) <= max(nn, mm, _kjb) -> 0
numnodes(node(e, t1, t2), s(_ckb)) <= numnodes(t1, _akb) /\ numnodes(t2, _bkb) /\ plus(_akb, _bkb, _ckb) -> 0
plus(n, s(mm), s(_vjb)) <= plus(n, mm, _vjb) -> 0
}


Solving took 0.161999 seconds.
No: Contradictory set of ground constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
le_nat(s(z), s(z)) <= True
le_nat(z, 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
not_empty(node(a, leaf, leaf)) <= 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
le_nat(z, s(z)) <= le_nat(s(z), s(s(z)))
False <= le_nat(z, z)
}
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005874 s (model generation: 0.005763,  model checking: 0.000111):

Clauses:
{
height(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
not_empty(node(e, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
le_nat(_gkb, _hkb) <= height(t, _gkb) /\ not_empty(t) /\ numnodes(t, _hkb) -> 0
height(node(e, t1, t2), s(_rjb)) <= height(t1, _pjb) /\ height(t2, _qjb) /\ max(_pjb, _qjb, _rjb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
max(s(nn), s(mm), s(_kjb)) <= max(nn, mm, _kjb) -> 0
numnodes(node(e, t1, t2), s(_ckb)) <= numnodes(t1, _akb) /\ numnodes(t2, _bkb) /\ plus(_akb, _bkb, _ckb) -> 0
plus(n, s(mm), s(_vjb)) <= plus(n, mm, _vjb) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


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


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


;
not_empty ->
[
not_empty : <etree>
{
  
}
]


;
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: {

}

max(s(nn), z, s(nn)) <= True  :
Yes: {

}

max(z, m, m) <= True  :
Yes: {
m -> z
}

not_empty(node(e, t1, t2)) <= True  :
Yes: {

}

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

}

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

le_nat(_gkb, _hkb) <= height(t, _gkb) /\ not_empty(t) /\ numnodes(t, _hkb)  :
No: ()

height(node(e, t1, t2), s(_rjb)) <= height(t1, _pjb) /\ height(t2, _qjb) /\ max(_pjb, _qjb, _rjb)  :
No: ()

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

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

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

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

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

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

max(s(nn), s(mm), s(_kjb)) <= max(nn, mm, _kjb)  :
No: ()

numnodes(node(e, t1, t2), s(_ckb)) <= numnodes(t1, _akb) /\ numnodes(t2, _bkb) /\ plus(_akb, _bkb, _ckb)  :
No: ()

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


-------------------------------------------
Step 1, which took 0.007300 s (model generation: 0.007097,  model checking: 0.000203):

Clauses:
{
height(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
not_empty(node(e, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
le_nat(_gkb, _hkb) <= height(t, _gkb) /\ not_empty(t) /\ numnodes(t, _hkb) -> 0
height(node(e, t1, t2), s(_rjb)) <= height(t1, _pjb) /\ height(t2, _qjb) /\ max(_pjb, _qjb, _rjb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
max(s(nn), s(mm), s(_kjb)) <= max(nn, mm, _kjb) -> 0
numnodes(node(e, t1, t2), s(_ckb)) <= numnodes(t1, _akb) /\ numnodes(t2, _bkb) /\ plus(_akb, _bkb, _ckb) -> 0
plus(n, s(mm), s(_vjb)) <= plus(n, mm, _vjb) -> 0
}

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

Current best model:
|_
name: None

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


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


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


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


;
not_empty ->
[
not_empty : <etree>
{
  not_empty(node(x_0_0, x_0_1, x_0_2)) <= True
}
]


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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
Yes: {
m -> s(_vduqw_0)
}

not_empty(node(e, t1, t2)) <= True  :
No: ()

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

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

le_nat(_gkb, _hkb) <= height(t, _gkb) /\ not_empty(t) /\ numnodes(t, _hkb)  :
No: ()

height(node(e, t1, t2), s(_rjb)) <= height(t1, _pjb) /\ height(t2, _qjb) /\ max(_pjb, _qjb, _rjb)  :
Yes: {
_pjb -> z  ;  _qjb -> z  ;  _rjb -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

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

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

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

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

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

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

max(s(nn), s(mm), s(_kjb)) <= max(nn, mm, _kjb)  :
Yes: {
_kjb -> z  ;  mm -> z  ;  nn -> z
}

numnodes(node(e, t1, t2), s(_ckb)) <= numnodes(t1, _akb) /\ numnodes(t2, _bkb) /\ plus(_akb, _bkb, _ckb)  :
Yes: {
_akb -> z  ;  _bkb -> z  ;  _ckb -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

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


-------------------------------------------
Step 2, which took 0.009228 s (model generation: 0.009025,  model checking: 0.000203):

Clauses:
{
height(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
not_empty(node(e, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
le_nat(_gkb, _hkb) <= height(t, _gkb) /\ not_empty(t) /\ numnodes(t, _hkb) -> 0
height(node(e, t1, t2), s(_rjb)) <= height(t1, _pjb) /\ height(t2, _qjb) /\ max(_pjb, _qjb, _rjb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
max(s(nn), s(mm), s(_kjb)) <= max(nn, mm, _kjb) -> 0
numnodes(node(e, t1, t2), s(_ckb)) <= numnodes(t1, _akb) /\ numnodes(t2, _bkb) /\ plus(_akb, _bkb, _ckb) -> 0
plus(n, s(mm), s(_vjb)) <= plus(n, mm, _vjb) -> 0
}

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


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


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


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


;
not_empty ->
[
not_empty : <etree>
{
  not_empty(node(x_0_0, x_0_1, x_0_2)) <= 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: ()

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

not_empty(node(e, t1, t2)) <= True  :
No: ()

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

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

le_nat(_gkb, _hkb) <= height(t, _gkb) /\ not_empty(t) /\ numnodes(t, _hkb)  :
Yes: {
_gkb -> s(_qeuqw_0)  ;  _hkb -> s(_reuqw_0)  ;  t -> node(_seuqw_0, _seuqw_1, _seuqw_2)
}

height(node(e, t1, t2), s(_rjb)) <= height(t1, _pjb) /\ height(t2, _qjb) /\ max(_pjb, _qjb, _rjb)  :
No: ()

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

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

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

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

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

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

max(s(nn), s(mm), s(_kjb)) <= max(nn, mm, _kjb)  :
No: ()

numnodes(node(e, t1, t2), s(_ckb)) <= numnodes(t1, _akb) /\ numnodes(t2, _bkb) /\ plus(_akb, _bkb, _ckb)  :
No: ()

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


-------------------------------------------
Step 3, which took 0.010952 s (model generation: 0.010786,  model checking: 0.000166):

Clauses:
{
height(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
not_empty(node(e, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
le_nat(_gkb, _hkb) <= height(t, _gkb) /\ not_empty(t) /\ numnodes(t, _hkb) -> 0
height(node(e, t1, t2), s(_rjb)) <= height(t1, _pjb) /\ height(t2, _qjb) /\ max(_pjb, _qjb, _rjb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
max(s(nn), s(mm), s(_kjb)) <= max(nn, mm, _kjb) -> 0
numnodes(node(e, t1, t2), s(_ckb)) <= numnodes(t1, _akb) /\ numnodes(t2, _bkb) /\ plus(_akb, _bkb, _ckb) -> 0
plus(n, s(mm), s(_vjb)) <= plus(n, mm, _vjb) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
le_nat(s(z), 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
not_empty(node(a, leaf, leaf)) <= 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
}

Current best model:
|_
name: None

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


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


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


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


;
not_empty ->
[
not_empty : <etree>
{
  not_empty(node(x_0_0, x_0_1, x_0_2)) <= 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: ()

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

not_empty(node(e, t1, t2)) <= True  :
No: ()

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

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

le_nat(_gkb, _hkb) <= height(t, _gkb) /\ not_empty(t) /\ numnodes(t, _hkb)  :
No: ()

height(node(e, t1, t2), s(_rjb)) <= height(t1, _pjb) /\ height(t2, _qjb) /\ max(_pjb, _qjb, _rjb)  :
No: ()

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

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

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

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

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

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

max(s(nn), s(mm), s(_kjb)) <= max(nn, mm, _kjb)  :
No: ()

numnodes(node(e, t1, t2), s(_ckb)) <= numnodes(t1, _akb) /\ numnodes(t2, _bkb) /\ plus(_akb, _bkb, _ckb)  :
No: ()

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


-------------------------------------------
Step 4, which took 0.013621 s (model generation: 0.013309,  model checking: 0.000312):

Clauses:
{
height(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
not_empty(node(e, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
le_nat(_gkb, _hkb) <= height(t, _gkb) /\ not_empty(t) /\ numnodes(t, _hkb) -> 0
height(node(e, t1, t2), s(_rjb)) <= height(t1, _pjb) /\ height(t2, _qjb) /\ max(_pjb, _qjb, _rjb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
max(s(nn), s(mm), s(_kjb)) <= max(nn, mm, _kjb) -> 0
numnodes(node(e, t1, t2), s(_ckb)) <= numnodes(t1, _akb) /\ numnodes(t2, _bkb) /\ plus(_akb, _bkb, _ckb) -> 0
plus(n, s(mm), s(_vjb)) <= plus(n, mm, _vjb) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
le_nat(s(z), s(z)) <= True
le_nat(z, 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
not_empty(node(a, leaf, leaf)) <= 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
}

Current best model:
|_
name: None

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


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


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


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


;
not_empty ->
[
not_empty : <etree>
{
  not_empty(node(x_0_0, x_0_1, x_0_2)) <= 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: ()

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

not_empty(node(e, t1, t2)) <= True  :
No: ()

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

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

le_nat(_gkb, _hkb) <= height(t, _gkb) /\ not_empty(t) /\ numnodes(t, _hkb)  :
No: ()

height(node(e, t1, t2), s(_rjb)) <= height(t1, _pjb) /\ height(t2, _qjb) /\ max(_pjb, _qjb, _rjb)  :
No: ()

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

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

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

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

}

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

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

max(s(nn), s(mm), s(_kjb)) <= max(nn, mm, _kjb)  :
No: ()

numnodes(node(e, t1, t2), s(_ckb)) <= numnodes(t1, _akb) /\ numnodes(t2, _bkb) /\ plus(_akb, _bkb, _ckb)  :
No: ()

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


Total time: 0.161999
Learner time: 0.045980
Teacher time: 0.000995
Reasons for stopping: No: Contradictory set of ground constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
le_nat(s(z), s(z)) <= True
le_nat(z, 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
not_empty(node(a, leaf, leaf)) <= 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
le_nat(z, s(z)) <= le_nat(s(z), s(s(z)))
False <= le_nat(z, z)
}