Solving ../../benchmarks/smtlib/true/tree_flip_heightRB_heightLB.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)
}
)
(height_rb, F:
{
height_rb(leaf, z) <= True
height_rb(node(e, t1, t2), s(_iq)) <= height_rb(t2, _iq)
}
eq_nat(_kq, _lq) <= height_rb(_jq, _kq) /\ height_rb(_jq, _lq)
)
(height_lb, F:
{
height_lb(leaf, z) <= True
height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq)
}
eq_nat(_oq, _pq) <= height_lb(_nq, _oq) /\ height_lb(_nq, _pq)
)
(flip, F:
{
flip(leaf, leaf) <= True
flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq)
}
eq_etree(_tq, _uq) <= flip(_sq, _tq) /\ flip(_sq, _uq)
)
}

properties:
{
eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq)
}


over-approximation: {flip, height_lb, height_rb, leq_nat}
under-approximation: {leq_nat}

Clause system for inference is:

{
flip(leaf, leaf) <= True -> 0
height_lb(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq) -> 0
eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq) -> 0
height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq) -> 0
height_rb(node(e, t1, t2), s(_iq)) <= height_rb(t2, _iq) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}


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

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


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


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



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

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_lb(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq) -> 0
eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq) -> 0
height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq) -> 0
height_rb(node(e, t1, t2), s(_iq)) <= height_rb(t2, _iq) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  
}
]


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


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


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



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




Answer of teacher:

flip(leaf, leaf) <= True  :
Yes: {

}

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

}

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

}

flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq)  :
No: ()

eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq)  :
No: ()

height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq)  :
No: ()

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

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

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


-------------------------------------------
Step 1, which took 0.007833 s (model generation: 0.007753,  model checking: 0.000080):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_lb(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq) -> 0
eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq) -> 0
height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq) -> 0
height_rb(node(e, t1, t2), s(_iq)) <= height_rb(t2, _iq) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
height_lb(leaf, z) <= True
height_rb(leaf, z) <= True
}

Current best model:
|_
name: None

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


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


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


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



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




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

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

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

flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq)  :
Yes: {
_qq -> leaf  ;  _rq -> leaf  ;  t1 -> leaf  ;  t2 -> leaf
}

eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq)  :
No: ()

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

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


-------------------------------------------
Step 2, which took 0.008867 s (model generation: 0.008759,  model checking: 0.000108):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_lb(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq) -> 0
eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq) -> 0
height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq) -> 0
height_rb(node(e, t1, t2), s(_iq)) <= height_rb(t2, _iq) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

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

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

flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq)  :
No: ()

eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq)  :
Yes: {
_vq -> s(z)  ;  _wq -> node(_oxxve_0, _oxxve_1, _oxxve_2)  ;  _xq -> s(s(_wxxve_0))  ;  t1 -> node(_qxxve_0, _qxxve_1, _qxxve_2)
}

height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq)  :
No: ()

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

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

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


-------------------------------------------
Step 3, which took 0.009024 s (model generation: 0.008906,  model checking: 0.000118):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_lb(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq) -> 0
eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq) -> 0
height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq) -> 0
height_rb(node(e, t1, t2), s(_iq)) <= height_rb(t2, _iq) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

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

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

flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq)  :
No: ()

eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq)  :
Yes: {
_vq -> s(z)  ;  _wq -> node(_yxxve_0, node(_lyxve_0, _lyxve_1, _lyxve_2), _yxxve_2)  ;  _xq -> s(s(_myxve_0))  ;  t1 -> node(_ayxve_0, _ayxve_1, _ayxve_2)
}

height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq)  :
No: ()

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

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

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


-------------------------------------------
Step 4, which took 0.009843 s (model generation: 0.009707,  model checking: 0.000136):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_lb(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq) -> 0
eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq) -> 0
height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq) -> 0
height_rb(node(e, t1, t2), s(_iq)) <= height_rb(t2, _iq) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

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

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

flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq)  :
No: ()

eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq)  :
Yes: {
_vq -> s(z)  ;  _wq -> node(_pyxve_0, _pyxve_1, node(_czxve_0, _czxve_1, _czxve_2))  ;  _xq -> s(s(_dzxve_0))  ;  t1 -> node(_ryxve_0, _ryxve_1, _ryxve_2)
}

height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq)  :
Yes: {
_mq -> z  ;  t1 -> leaf  ;  t2 -> node(_fzxve_0, _fzxve_1, _fzxve_2)
}

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

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

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


-------------------------------------------
Step 5, which took 0.011707 s (model generation: 0.011455,  model checking: 0.000252):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_lb(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq) -> 0
eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq) -> 0
height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq) -> 0
height_rb(node(e, t1, t2), s(_iq)) <= height_rb(t2, _iq) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

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

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

flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq)  :
No: ()

eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq)  :
Yes: {
_vq -> s(_kzxve_0)  ;  _wq -> node(_lzxve_0, _lzxve_1, _lzxve_2)  ;  _xq -> z  ;  t1 -> node(_nzxve_0, _nzxve_1, _nzxve_2)
}

height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq)  :
Yes: {
_mq -> s(z)  ;  t1 -> node(_xzxve_0, node(_iayve_0, _iayve_1, _iayve_2), node(_iayve_0, _iayve_1, _iayve_2))  ;  t2 -> leaf
}

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

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

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


-------------------------------------------
Step 6, which took 0.012717 s (model generation: 0.012464,  model checking: 0.000253):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_lb(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq) -> 0
eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq) -> 0
height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq) -> 0
height_rb(node(e, t1, t2), s(_iq)) <= height_rb(t2, _iq) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

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

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

flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq)  :
No: ()

eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq)  :
Yes: {
_vq -> s(z)  ;  _wq -> node(_sbyve_0, node(_mcyve_0, leaf, _mcyve_2), _sbyve_2)  ;  _xq -> s(s(_ncyve_0))  ;  t1 -> node(_ubyve_0, _ubyve_1, node(_lcyve_0, _lcyve_1, leaf))
}

height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq)  :
No: ()

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

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

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


-------------------------------------------
Step 7, which took 0.013263 s (model generation: 0.013072,  model checking: 0.000191):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_lb(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq) -> 0
eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq) -> 0
height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq) -> 0
height_rb(node(e, t1, t2), s(_iq)) <= height_rb(t2, _iq) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

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

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

flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq)  :
Yes: {
_qq -> leaf  ;  _rq -> node(_cdyve_0, leaf, _cdyve_2)  ;  t1 -> node(_ddyve_0, leaf, _ddyve_2)  ;  t2 -> leaf
}

eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq)  :
Yes: {
_vq -> s(s(_udyve_0))  ;  _wq -> node(_kdyve_0, leaf, _kdyve_2)  ;  _xq -> s(z)  ;  t1 -> node(_mdyve_0, leaf, _mdyve_2)
}

height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq)  :
No: ()

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

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

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


-------------------------------------------
Step 8, which took 0.014919 s (model generation: 0.014553,  model checking: 0.000366):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_lb(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq) -> 0
eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq) -> 0
height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq) -> 0
height_rb(node(e, t1, t2), s(_iq)) <= height_rb(t2, _iq) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

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

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

flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq)  :
Yes: {
_qq -> node(_peyve_0, leaf, _peyve_2)  ;  _rq -> leaf  ;  t1 -> leaf  ;  t2 -> node(_seyve_0, node(_zhyve_0, _zhyve_1, _zhyve_2), _seyve_2)
}

eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq)  :
Yes: {
_vq -> s(z)  ;  _wq -> leaf  ;  _xq -> z  ;  t1 -> node(_ufyve_0, node(_rgyve_0, _rgyve_1, _rgyve_2), _ufyve_2)
}

height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq)  :
No: ()

height_rb(node(e, t1, t2), s(_iq)) <= height_rb(t2, _iq)  :
Yes: {
_iq -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_kgyve_0, node(_hhyve_0, _hhyve_1, _hhyve_2), _kgyve_2)
}

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

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


-------------------------------------------
Step 9, which took 0.019798 s (model generation: 0.019561,  model checking: 0.000237):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_lb(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq) -> 0
eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq) -> 0
height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq) -> 0
height_rb(node(e, t1, t2), s(_iq)) <= height_rb(t2, _iq) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}

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

Current best model:
|_
name: None

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


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


;
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)
  height_rb(node(x_0_0, x_0_1, x_0_2), z) <= True
}
]


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



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




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

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

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

flip(node(e, t1, t2), node(e, _qq, _rq)) <= flip(t1, _rq) /\ flip(t2, _qq)  :
No: ()

eq_nat(_vq, _xq) <= flip(t1, _wq) /\ height_lb(_wq, _xq) /\ height_rb(t1, _vq)  :
Yes: {
_vq -> z  ;  _wq -> node(_iiyve_0, leaf, node(_ejyve_0, _ejyve_1, _ejyve_2))  ;  _xq -> s(z)  ;  t1 -> node(_kiyve_0, _kiyve_1, _kiyve_2)
}

height_lb(node(e, t1, t2), s(_mq)) <= height_lb(t1, _mq)  :
Yes: {
_mq -> s(z)  ;  t1 -> node(_siyve_0, leaf, node(_pjyve_0, _pjyve_1, _pjyve_2))  ;  t2 -> leaf
}

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

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

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


Total time: 0.137338
Learner time: 0.112565
Teacher time: 0.001799
Reasons for stopping: Yes: |_
name: None

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


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


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



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