Solving ../../benchmarks/smtlib/true/tree_heightRB_subtree.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)
}
)
(subtree, P:
{
subtree(leaf, t) <= True
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))
False <= subtree(node(ea, ta1, ta2), leaf)
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))
}
)
(height_rb, F:
{
height_rb(leaf, z) <= True
height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur)
}
eq_nat(_wr, _xr) <= height_rb(_vr, _wr) /\ height_rb(_vr, _xr)
)
}

properties:
{
leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2)
}


over-approximation: {height_rb, subtree}
under-approximation: {leq_nat}

Clause system for inference is:

{
height_rb(leaf, z) <= True -> 0
subtree(leaf, t) <= True -> 0
leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2) -> 0
height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur) -> 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
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}


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

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


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



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

Clauses:
{
height_rb(leaf, z) <= True -> 0
subtree(leaf, t) <= True -> 0
leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2) -> 0
height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur) -> 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
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

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

}

subtree(leaf, t) <= True  :
Yes: {
t -> node(_cdlhp_0, _cdlhp_1, _cdlhp_2)
}

leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2)  :
No: ()

height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur)  :
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: ()

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

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

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


-------------------------------------------
Step 1, which took 0.017094 s (model generation: 0.016862,  model checking: 0.000232):

Clauses:
{
height_rb(leaf, z) <= True -> 0
subtree(leaf, t) <= True -> 0
leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2) -> 0
height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur) -> 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
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
height_rb(leaf, z) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
}

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
Yes: {
t -> leaf
}

leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2)  :
No: ()

height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur)  :
Yes: {
_ur -> z  ;  t2 -> leaf
}

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

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
Yes: {
ta1 -> leaf  ;  ta2 -> leaf  ;  tb1 -> node(_idlhp_0, _idlhp_1, _idlhp_2)  ;  tb2 -> node(_jdlhp_0, _jdlhp_1, _jdlhp_2)
}

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

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


-------------------------------------------
Step 2, which took 0.010821 s (model generation: 0.010627,  model checking: 0.000194):

Clauses:
{
height_rb(leaf, z) <= True -> 0
subtree(leaf, t) <= True -> 0
leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2) -> 0
height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur) -> 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
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
height_rb(leaf, z) <= True
height_rb(node(a, leaf, leaf), s(z)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
}

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2)  :
Yes: {
_yr -> z  ;  _zr -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur)  :
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: ()

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

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_eelhp_0, _eelhp_1, _eelhp_2)  ;  ta2 -> node(_felhp_0, _felhp_1, _felhp_2)  ;  tb1 -> node(_gelhp_0, _gelhp_1, _gelhp_2)  ;  tb2 -> leaf
}

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


-------------------------------------------
Step 3, which took 0.009855 s (model generation: 0.009768,  model checking: 0.000087):

Clauses:
{
height_rb(leaf, z) <= True -> 0
subtree(leaf, t) <= True -> 0
leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2) -> 0
height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur) -> 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
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2)  :
Yes: {
_yr -> z  ;  _zr -> s(_lelhp_0)  ;  t1 -> leaf  ;  t2 -> node(_nelhp_0, _nelhp_1, _nelhp_2)
}

height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur)  :
No: ()

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

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

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

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

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

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


-------------------------------------------
Step 4, which took 0.010831 s (model generation: 0.010557,  model checking: 0.000274):

Clauses:
{
height_rb(leaf, z) <= True -> 0
subtree(leaf, t) <= True -> 0
leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2) -> 0
height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur) -> 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
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
height_rb(leaf, z) <= True
height_rb(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
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
}

Current best model:
|_
name: None

height_rb ->
[
height_rb : <etree * nat>
{
  height_rb(leaf, z) <= True
  height_rb(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
}
]


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2)  :
Yes: {
_yr -> s(_yelhp_0)  ;  _zr -> z  ;  t1 -> node(_aflhp_0, _aflhp_1, _aflhp_2)  ;  t2 -> leaf
}

height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur)  :
No: ()

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

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

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

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

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

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


-------------------------------------------
Step 5, which took 0.014847 s (model generation: 0.014782,  model checking: 0.000065):

Clauses:
{
height_rb(leaf, z) <= True -> 0
subtree(leaf, t) <= True -> 0
leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2) -> 0
height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur) -> 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
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
height_rb(leaf, z) <= True
height_rb(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
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
leq_nat(s(z), z) <= leq_nat(s(s(z)), s(z))
leq_nat(s(z), z) <= subtree(node(a, leaf, leaf), leaf)
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
}

Current best model:
|_
name: None

height_rb ->
[
height_rb : <etree * nat>
{
  height_rb(leaf, z) <= True
  height_rb(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(s(x_0_0), z) <= True
  leq_nat(z, s(x_1_0)) <= True
  leq_nat(z, z) <= True
}
]


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2)  :
No: ()

height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur)  :
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)  :
Yes: {

}

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

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

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


-------------------------------------------
Step 6, which took 0.010467 s (model generation: 0.010073,  model checking: 0.000394):

Clauses:
{
height_rb(leaf, z) <= True -> 0
subtree(leaf, t) <= True -> 0
leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2) -> 0
height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur) -> 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
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

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

Current best model:
|_
name: None

height_rb ->
[
height_rb : <etree * nat>
{
  height_rb(leaf, z) <= True
  height_rb(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)) <= leq_nat(x_0_0, x_1_0)
  leq_nat(z, s(x_1_0)) <= True
  leq_nat(z, z) <= True
}
]


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2)  :
Yes: {
_yr -> s(s(_gilhp_0))  ;  _zr -> s(z)  ;  t1 -> node(_gflhp_0, leaf, _gflhp_2)  ;  t2 -> node(_hflhp_0, _hflhp_1, node(_milhp_0, _milhp_1, _milhp_2))
}

height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur)  :
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: ()

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
Yes: {
ta1 -> node(_qglhp_0, node(_zilhp_0, leaf, _zilhp_2), _qglhp_2)  ;  ta2 -> leaf  ;  tb1 -> node(_sglhp_0, _sglhp_1, node(_ajlhp_0, _ajlhp_1, node(_milhp_0, _milhp_1, _milhp_2)))  ;  tb2 -> leaf
}

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> leaf  ;  ta2 -> node(_lhlhp_0, _lhlhp_1, _lhlhp_2)  ;  tb1 -> node(_mhlhp_0, _mhlhp_1, _mhlhp_2)  ;  tb2 -> leaf
}

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_ailhp_0, leaf, _ailhp_2)  ;  tb1 -> leaf  ;  tb2 -> node(_iilhp_0, _iilhp_1, node(_milhp_0, _milhp_1, _milhp_2))
}


-------------------------------------------
Step 7, which took 0.013411 s (model generation: 0.012149,  model checking: 0.001262):

Clauses:
{
height_rb(leaf, z) <= True -> 0
subtree(leaf, t) <= True -> 0
leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2) -> 0
height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur) -> 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
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2)  :
No: ()

height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur)  :
Yes: {
_ur -> z  ;  t1 -> node(_jolhp_0, _jolhp_1, _jolhp_2)  ;  t2 -> leaf
}

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

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

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

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


-------------------------------------------
Step 8, which took 0.014618 s (model generation: 0.013168,  model checking: 0.001450):

Clauses:
{
height_rb(leaf, z) <= True -> 0
subtree(leaf, t) <= True -> 0
leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2) -> 0
height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur) -> 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
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

leq_nat(_yr, _zr) <= height_rb(t1, _yr) /\ height_rb(t2, _zr) /\ subtree(t1, t2)  :
Yes: {
_yr -> s(z)  ;  _zr -> z  ;  t1 -> node(_gtlhp_0, leaf, leaf)  ;  t2 -> node(_htlhp_0, node(_lzlhp_0, _lzlhp_1, _lzlhp_2), node(_lylhp_0, _lylhp_1, _lylhp_2))
}

height_rb(node(e, t1, t2), s(_ur)) <= height_rb(t2, _ur)  :
Yes: {
_ur -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_ltlhp_0, node(_wylhp_0, _wylhp_1, _wylhp_2), _ltlhp_2)
}

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

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

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

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


Total time: 0.127712
Learner time: 0.105998
Teacher time: 0.004081
Reasons for stopping: Yes: |_
name: None

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


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



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