Solving ../../benchmarks/smtlib/true/tree_heightMIDDLE.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: {
direction -> {left, right}  ;  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_mid, F:
{
height_mid(leaf, d, z) <= True
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)
}
eq_nat(_il, _jl) <= height_mid(_gl, _hl, _il) /\ height_mid(_gl, _hl, _jl)
)
(flip, F:
{
flip(leaf, leaf) <= True
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)
}
eq_etree(_nl, _ol) <= flip(_ml, _nl) /\ flip(_ml, _ol)
)
}

properties:
{
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)
}


over-approximation: {flip, height_mid, leq_nat}
under-approximation: {leq_nat}

Clause system for inference is:

{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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 1.817608 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_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
height_mid ->
[
height_mid : <etree * direction * nat>
{
  _r_1(leaf, z) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0)
  _r_2(leaf, z) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0)
  height_mid(leaf, left, z) <= True
  height_mid(leaf, right, z) <= True
  height_mid(node(x_0_0, x_0_1, x_0_2), left, s(x_2_0)) <= _r_1(x_0_1, x_2_0)
  height_mid(node(x_0_0, x_0_1, x_0_2), right, s(x_2_0)) <= _r_2(x_0_2, x_2_0)
}
]


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



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

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid ->
[
height_mid : <etree * direction * nat>
{
  
}
]


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



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




Answer of teacher:

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

}

height_mid(leaf, d, z) <= True  :
Yes: {
d -> right
}

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
No: ()

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
No: ()

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
No: ()

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
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.006273 s (model generation: 0.006204,  model checking: 0.000069):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, right, z) <= True
}

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
Yes: {
d -> left
}

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

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
No: ()

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
Yes: {
_el -> z  ;  t1 -> leaf
}

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
No: ()

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.012956 s (model generation: 0.012819,  model checking: 0.000137):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, 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_mid ->
[
height_mid : <etree * direction * nat>
{
  height_mid(leaf, left, z) <= True
  height_mid(leaf, right, z) <= True
  height_mid(node(x_0_0, x_0_1, x_0_2), left, s(x_2_0)) <= True
}
]


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
No: ()

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
No: ()

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
No: ()

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
Yes: {
_fl -> 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 3, which took 0.020240 s (model generation: 0.020135,  model checking: 0.000105):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, 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_mid ->
[
height_mid : <etree * direction * nat>
{
  height_mid(leaf, left, z) <= True
  height_mid(leaf, right, z) <= True
  height_mid(node(x_0_0, x_0_1, x_0_2), left, s(x_2_0)) <= True
  height_mid(node(x_0_0, x_0_1, x_0_2), right, s(x_2_0)) <= True
}
]


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
No: ()

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
Yes: {
_pl -> s(z)  ;  _ql -> node(_qfjhp_0, _qfjhp_1, _qfjhp_2)  ;  _rl -> s(s(_yfjhp_0))  ;  t1 -> node(_sfjhp_0, _sfjhp_1, _sfjhp_2)
}

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
No: ()

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
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.013132 s (model generation: 0.013022,  model checking: 0.000110):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, s(z)) <= True
False <= height_mid(node(a, leaf, leaf), right, 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_mid ->
[
height_mid : <etree * direction * nat>
{
  _r_1(z) <= True
  height_mid(leaf, left, z) <= True
  height_mid(leaf, right, z) <= True
  height_mid(node(x_0_0, x_0_1, x_0_2), left, s(x_2_0)) <= True
  height_mid(node(x_0_0, x_0_1, x_0_2), right, s(x_2_0)) <= _r_1(x_2_0)
}
]


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
No: ()

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
Yes: {
_pl -> s(s(_igjhp_0))  ;  _ql -> node(_agjhp_0, _agjhp_1, _agjhp_2)  ;  _rl -> s(z)  ;  t1 -> node(_cgjhp_0, _cgjhp_1, _cgjhp_2)
}

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
No: ()

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
Yes: {
_fl -> s(_fgjhp_0)  ;  t2 -> node(_ggjhp_0, _ggjhp_1, _ggjhp_2)
}

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.014268 s (model generation: 0.014078,  model checking: 0.000190):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(z))) <= True
False <= height_mid(node(a, leaf, leaf), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), right, 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_mid ->
[
height_mid : <etree * direction * nat>
{
  _r_1(leaf, z) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  height_mid(leaf, left, z) <= True
  height_mid(leaf, right, z) <= True
  height_mid(node(x_0_0, x_0_1, x_0_2), left, s(x_2_0)) <= _r_1(x_0_2, x_2_0)
  height_mid(node(x_0_0, x_0_1, x_0_2), right, s(x_2_0)) <= _r_1(x_0_2, x_2_0)
}
]


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
No: ()

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
Yes: {
_pl -> s(s(_ahjhp_0))  ;  _ql -> node(_kgjhp_0, _kgjhp_1, leaf)  ;  _rl -> s(z)  ;  t1 -> node(_mgjhp_0, _mgjhp_1, node(_zgjhp_0, _zgjhp_1, _zgjhp_2))
}

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
Yes: {
_el -> z  ;  t1 -> leaf  ;  t2 -> node(_hhjhp_0, _hhjhp_1, _hhjhp_2)
}

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
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.020653 s (model generation: 0.020378,  model checking: 0.000275):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(z))) <= True
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), right, 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_mid ->
[
height_mid : <etree * direction * nat>
{
  _r_1(leaf, z) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  height_mid(leaf, left, z) <= True
  height_mid(leaf, right, z) <= True
  height_mid(node(x_0_0, x_0_1, x_0_2), left, s(x_2_0)) <= _r_1(x_0_1, x_2_0)
  height_mid(node(x_0_0, x_0_1, x_0_2), right, s(x_2_0)) <= _r_1(x_0_2, x_2_0)
}
]


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
No: ()

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
Yes: {
_pl -> s(s(_zhjhp_0))  ;  _ql -> node(_jhjhp_0, _jhjhp_1, leaf)  ;  _rl -> s(z)  ;  t1 -> node(_lhjhp_0, node(_yhjhp_0, _yhjhp_1, _yhjhp_2), _lhjhp_2)
}

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
No: ()

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
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.021039 s (model generation: 0.020794,  model checking: 0.000245):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(z))) <= True
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), right, 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_mid ->
[
height_mid : <etree * direction * nat>
{
  _r_1(leaf, z) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), z) <= True
  height_mid(leaf, left, z) <= True
  height_mid(leaf, right, z) <= True
  height_mid(node(x_0_0, x_0_1, x_0_2), left, s(x_2_0)) <= _r_1(x_0_1, x_2_0) /\ _r_1(x_0_2, x_2_0)
  height_mid(node(x_0_0, x_0_1, x_0_2), right, s(x_2_0)) <= _r_1(x_0_2, x_2_0)
}
]


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
No: ()

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
Yes: {
_pl -> s(z)  ;  _ql -> node(_hijhp_0, _hijhp_1, node(_ojjhp_0, _ojjhp_1, _ojjhp_2))  ;  _rl -> s(s(_pjjhp_0))  ;  t1 -> node(_jijhp_0, node(_mjjhp_0, _mjjhp_1, _mjjhp_2), node(_mjjhp_0, _mjjhp_1, _mjjhp_2))
}

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
Yes: {
_el -> s(z)  ;  t1 -> node(_rijhp_0, _rijhp_1, node(_yjjhp_0, _yjjhp_1, _yjjhp_2))  ;  t2 -> leaf
}

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
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.022645 s (model generation: 0.022346,  model checking: 0.000299):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(z))) <= True
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(z))
False <= height_mid(node(a, leaf, leaf), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), right, s(s(z)))
height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(z))) <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, 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_2)
}
]


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


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
No: ()

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
Yes: {
_pl -> s(s(z))  ;  _ql -> node(_qkjhp_0, _qkjhp_1, node(_hljhp_0, _hljhp_1, leaf))  ;  _rl -> s(s(s(_oljhp_0)))  ;  t1 -> node(_skjhp_0, node(_fljhp_0, leaf, _fljhp_2), _skjhp_2)
}

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
No: ()

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
No: ()

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.022303 s (model generation: 0.022039,  model checking: 0.000264):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(z))) <= True
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) /\ height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(z))
False <= height_mid(node(a, leaf, leaf), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), right, s(s(z)))
height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(z))) <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, 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_mid ->
[
height_mid : <etree * direction * nat>
{
  _r_1(leaf, z) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  height_mid(leaf, left, z) <= True
  height_mid(leaf, right, z) <= True
  height_mid(node(x_0_0, x_0_1, x_0_2), left, s(x_2_0)) <= _r_1(x_0_1, x_2_0)
  height_mid(node(x_0_0, x_0_1, x_0_2), right, s(x_2_0)) <= _r_1(x_0_2, x_2_0)
}
]


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
Yes: {
_kl -> leaf  ;  _ll -> node(_cmjhp_0, leaf, _cmjhp_2)  ;  t1 -> node(_dmjhp_0, leaf, _dmjhp_2)  ;  t2 -> leaf
}

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
Yes: {
_pl -> s(z)  ;  _ql -> node(_kmjhp_0, leaf, node(_xmjhp_0, _xmjhp_1, _xmjhp_2))  ;  _rl -> s(s(_ymjhp_0))  ;  t1 -> node(_mmjhp_0, leaf, _mmjhp_2)
}

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
No: ()

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
No: ()

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

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


-------------------------------------------
Step 10, which took 0.026840 s (model generation: 0.026464,  model checking: 0.000376):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(z))) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(z))
False <= height_mid(node(a, leaf, leaf), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), right, s(s(z)))
False <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(z))) <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, 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_2)
}
]


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


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
No: ()

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
Yes: {
_pl -> s(s(z))  ;  _ql -> node(_fojhp_0, _fojhp_1, node(_wojhp_0, node(_dpjhp_0, leaf, _dpjhp_2), leaf))  ;  _rl -> s(s(s(z)))  ;  t1 -> node(_hojhp_0, node(_uojhp_0, leaf, _uojhp_2), _hojhp_2)
}

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
Yes: {
_el -> s(z)  ;  t1 -> node(_lojhp_0, node(_zpjhp_0, _zpjhp_1, _zpjhp_2), leaf)
}

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
No: ()

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

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


-------------------------------------------
Step 11, which took 0.033675 s (model generation: 0.033306,  model checking: 0.000369):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(z))) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) /\ height_mid(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(z))
False <= height_mid(node(a, leaf, leaf), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), right, s(s(z)))
False <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(z))) <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(z))
height_mid(node(a, node(a, node(a, leaf, leaf), leaf), leaf), left, s(s(z))) <= height_mid(node(a, node(a, leaf, leaf), leaf), right, 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_2)
}
]


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


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
No: ()

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
Yes: {
_pl -> s(s(s(z)))  ;  _ql -> node(_vqjhp_0, _vqjhp_1, node(_mrjhp_0, _mrjhp_1, leaf))  ;  _rl -> s(s(z))  ;  t1 -> node(_xqjhp_0, node(_krjhp_0, leaf, node(_qrjhp_0, _qrjhp_1, leaf)), _xqjhp_2)
}

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
No: ()

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
Yes: {
_fl -> s(z)  ;  t2 -> node(_frjhp_0, leaf, node(_psjhp_0, _psjhp_1, _psjhp_2))
}

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

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


-------------------------------------------
Step 12, which took 0.036415 s (model generation: 0.035807,  model checking: 0.000608):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(z))) <= True
height_mid(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), right, s(s(z))) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) /\ height_mid(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(z))
False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(s(z))))
False <= height_mid(node(a, leaf, leaf), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), right, s(s(z)))
False <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(z))) <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(z))
height_mid(node(a, node(a, node(a, leaf, leaf), leaf), leaf), left, s(s(z))) <= height_mid(node(a, node(a, leaf, leaf), leaf), right, 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_2) /\ flip(x_0_2, x_1_1)
}
]


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


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
No: ()

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
Yes: {
_pl -> s(z)  ;  _ql -> node(_bujhp_0, leaf, node(_mvjhp_0, leaf, leaf))  ;  _rl -> s(s(z))  ;  t1 -> node(_dujhp_0, node(_kvjhp_0, leaf, leaf), leaf)
}

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
No: ()

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
Yes: {
_fl -> s(s(z))  ;  t2 -> node(_lujhp_0, node(_yujhp_0, _yujhp_1, node(_wvjhp_0, _wvjhp_1, _wvjhp_2)), leaf)
}

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

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


-------------------------------------------
Step 13, which took 0.038630 s (model generation: 0.037694,  model checking: 0.000936):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(z))) <= True
height_mid(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), right, s(s(z))) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) /\ height_mid(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(z))
False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(s(z))))
False <= height_mid(node(a, leaf, leaf), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), right, s(s(z)))
False <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(z))) <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(z))
False <= height_mid(node(a, node(a, leaf, leaf), leaf), left, s(z))
height_mid(node(a, node(a, node(a, leaf, leaf), leaf), leaf), left, s(s(z))) <= height_mid(node(a, node(a, leaf, leaf), leaf), right, s(z))
height_mid(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), right, s(s(s(z)))) <= height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, 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)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


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


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
No: ()

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
Yes: {
_pl -> s(s(s(z)))  ;  _ql -> node(_czjhp_0, leaf, node(_sakhp_0, node(_wckhp_0, leaf, leaf), leaf))  ;  _rl -> s(s(z))  ;  t1 -> node(_ezjhp_0, node(_qakhp_0, leaf, node(_uckhp_0, leaf, leaf)), leaf)
}

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
No: ()

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
No: ()

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

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


-------------------------------------------
Step 14, which took 0.182789 s (model generation: 0.182426,  model checking: 0.000363):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(z))) <= True
height_mid(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), right, s(s(z))) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) /\ height_mid(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(z))
False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(s(z))))
False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) /\ height_mid(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), right, s(s(z))) /\ height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(s(z))))
False <= height_mid(node(a, leaf, leaf), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), right, s(s(z)))
False <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(z))) <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(z))
False <= height_mid(node(a, node(a, leaf, leaf), leaf), left, s(z))
height_mid(node(a, node(a, node(a, leaf, leaf), leaf), leaf), left, s(s(z))) <= height_mid(node(a, node(a, leaf, leaf), leaf), right, s(z))
height_mid(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), right, s(s(s(z)))) <= height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, 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)) <= flip(x_0_1, x_1_2)
}
]


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


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
No: ()

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
No: ()

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
Yes: {
_el -> s(s(_ghkhp_0))  ;  t1 -> node(_qgkhp_0, _qgkhp_1, node(_fhkhp_0, _fhkhp_1, _fhkhp_2))
}

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
Yes: {
_fl -> z  ;  t1 -> node(_hhkhp_0, _hhkhp_1, _hhkhp_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: ()


-------------------------------------------
Step 15, which took 0.206775 s (model generation: 0.205965,  model checking: 0.000810):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(z))) <= True
height_mid(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), right, s(s(z))) <= True
height_mid(node(a, node(a, leaf, leaf), leaf), right, s(z)) <= True
height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(s(z)))) <= True
height_mid(node(a, node(a, node(a, leaf, leaf), leaf), leaf), left, s(s(z))) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) /\ height_mid(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(z))
False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) /\ height_mid(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), right, s(s(z)))
False <= height_mid(node(a, leaf, leaf), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), right, s(s(z)))
False <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(z))) <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(z))
False <= height_mid(node(a, node(a, leaf, leaf), leaf), left, s(z))
height_mid(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), right, s(s(s(z)))) <= height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, 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)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
height_mid ->
[
height_mid : <etree * direction * nat>
{
  _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  _r_2(leaf, z) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0)
  height_mid(leaf, left, z) <= True
  height_mid(leaf, right, z) <= True
  height_mid(node(x_0_0, x_0_1, x_0_2), left, s(x_2_0)) <= _r_1(x_0_1, x_2_0)
  height_mid(node(x_0_0, x_0_1, x_0_2), left, s(x_2_0)) <= _r_2(x_0_1, x_2_0)
  height_mid(node(x_0_0, x_0_1, x_0_2), right, s(x_2_0)) <= _r_2(x_0_2, x_2_0)
}
]


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
No: ()

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
Yes: {
_pl -> s(s(s(_llkhp_0)))  ;  _ql -> node(_tikhp_0, leaf, node(_glkhp_0, leaf, leaf))  ;  _rl -> s(s(z))  ;  t1 -> node(_vikhp_0, node(_elkhp_0, leaf, leaf), leaf)
}

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
No: ()

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
Yes: {
_fl -> s(s(z))  ;  t2 -> node(_hjkhp_0, node(_sjkhp_0, node(_ylkhp_0, _ylkhp_1, _ylkhp_2), _sjkhp_2), _hjkhp_2)
}

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

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


-------------------------------------------
Step 16, which took 0.221709 s (model generation: 0.220852,  model checking: 0.000857):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(z))) <= True
height_mid(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), right, s(s(z))) <= True
height_mid(node(a, leaf, node(a, node(a, node(a, leaf, leaf), leaf), leaf)), right, s(s(s(z)))) <= True
height_mid(node(a, node(a, leaf, leaf), leaf), right, s(z)) <= True
height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(s(z)))) <= True
height_mid(node(a, node(a, node(a, leaf, leaf), leaf), leaf), left, s(s(z))) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) /\ height_mid(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(z))
False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) /\ height_mid(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), right, s(s(z)))
False <= height_mid(node(a, leaf, leaf), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), right, s(s(z)))
False <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(z))) <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(z))
False <= height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(s(z))))
False <= height_mid(node(a, node(a, leaf, leaf), leaf), left, s(z))
height_mid(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), right, s(s(s(z)))) <= height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_2(leaf, leaf) <= True
  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)) <= _r_2(x_0_2, x_1_1) /\ flip(x_0_1, x_1_2)
}
]


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


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
Yes: {
_kl -> node(_ymkhp_0, leaf, node(_dskhp_0, leaf, leaf))  ;  _ll -> node(_zmkhp_0, leaf, leaf)  ;  t1 -> node(_ankhp_0, leaf, leaf)  ;  t2 -> node(_bnkhp_0, node(_cskhp_0, leaf, leaf), leaf)
}

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
Yes: {
_pl -> s(s(z))  ;  _ql -> node(_hnkhp_0, leaf, node(_uokhp_0, leaf, node(_rqkhp_0, leaf, leaf)))  ;  _rl -> s(s(s(z)))  ;  t1 -> node(_jnkhp_0, node(_sokhp_0, node(_wqkhp_0, leaf, leaf), leaf), leaf)
}

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
No: ()

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
No: ()

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

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


-------------------------------------------
Step 17, which took 0.314080 s (model generation: 0.313113,  model checking: 0.000967):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl) -> 0
eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl) -> 0
height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el) -> 0
height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl) -> 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
flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) <= True
height_mid(leaf, left, z) <= True
height_mid(leaf, right, z) <= True
height_mid(node(a, leaf, leaf), left, s(z)) <= True
height_mid(node(a, leaf, leaf), right, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(z)) <= True
height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(z))) <= True
height_mid(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), right, s(s(z))) <= True
height_mid(node(a, leaf, node(a, node(a, node(a, leaf, leaf), leaf), leaf)), right, s(s(s(z)))) <= True
height_mid(node(a, node(a, leaf, leaf), leaf), right, s(z)) <= True
height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(s(z)))) <= True
height_mid(node(a, node(a, node(a, leaf, leaf), leaf), leaf), left, s(s(z))) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ height_mid(node(a, leaf, node(a, leaf, leaf)), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) /\ height_mid(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(z))
False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) /\ height_mid(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), right, s(s(z)))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf)))) /\ height_mid(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), right, s(s(s(z))))
False <= height_mid(node(a, leaf, leaf), left, s(s(z)))
False <= height_mid(node(a, leaf, leaf), right, s(s(z)))
False <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(z)))
height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(z))) <= height_mid(node(a, leaf, node(a, leaf, leaf)), right, s(z))
False <= height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(s(z))))
False <= height_mid(node(a, node(a, leaf, leaf), leaf), left, s(z))
height_mid(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), right, s(s(s(z)))) <= height_mid(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), left, s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_2(leaf, leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_2, x_1_1) /\ _r_2(x_0_2, x_1_2)
  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)) <= _r_2(x_0_1, x_1_2)
}
]


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


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



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




Answer of teacher:

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

height_mid(leaf, d, z) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _kl, _ll)) <= flip(t1, _ll) /\ flip(t2, _kl)  :
Yes: {
_kl -> node(_qskhp_0, _qskhp_1, leaf)  ;  _ll -> node(_rskhp_0, leaf, leaf)  ;  t1 -> node(_sskhp_0, leaf, node(_rxkhp_0, _rxkhp_1, _rxkhp_2))  ;  t2 -> node(_tskhp_0, leaf, _tskhp_2)
}

eq_nat(_pl, _rl) <= flip(t1, _ql) /\ height_mid(_ql, right, _rl) /\ height_mid(t1, left, _pl)  :
Yes: {
_pl -> s(s(s(z)))  ;  _ql -> node(_vskhp_0, _vskhp_1, node(_qtkhp_0, leaf, leaf))  ;  _rl -> s(s(z))  ;  t1 -> node(_xskhp_0, node(_otkhp_0, node(_uukhp_0, _uukhp_1, leaf), leaf), _xskhp_2)
}

height_mid(node(e, t1, t2), left, s(_el)) <= height_mid(t1, right, _el)  :
No: ()

height_mid(node(e, t1, t2), right, s(_fl)) <= height_mid(t2, left, _fl)  :
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: 1.817608
Learner time: 1.213609
Teacher time: 0.007038
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_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
height_mid ->
[
height_mid : <etree * direction * nat>
{
  _r_1(leaf, z) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0)
  _r_2(leaf, z) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0)
  height_mid(leaf, left, z) <= True
  height_mid(leaf, right, z) <= True
  height_mid(node(x_0_0, x_0_1, x_0_2), left, s(x_2_0)) <= _r_1(x_0_1, x_2_0)
  height_mid(node(x_0_0, x_0_1, x_0_2), right, s(x_2_0)) <= _r_2(x_0_2, x_2_0)
}
]


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



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