Solving ../../benchmarks/smtlib/false/tree_heightMIDDLE_error.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: Some(60.) (sec)
Teacher_type: Checks all clauses every time
Approximation method: remove every clause that can be safely removed



Learning problem is:

env: {
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(_rgb)) <= height_mid(t1, right, _rgb)
height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb)
}
eq_nat(_vgb, _wgb) <= height_mid(_tgb, _ugb, _vgb) /\ height_mid(_tgb, _ugb, _wgb)
)
(flip, F:
{
flip(leaf, leaf) <= True
flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb)
}
eq_etree(_ahb, _bhb) <= flip(_zgb, _ahb) /\ flip(_zgb, _bhb)
)
}

properties:
{
eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb)
}


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
eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb) -> 0
flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb) -> 0
height_mid(node(e, t1, t2), left, s(_rgb)) <= height_mid(t1, right, _rgb) -> 0
height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb) -> 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.246661 seconds.
No: Contradictory set of ground constraints:
{
False <= True
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, 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, node(a, leaf, leaf), leaf), left, s(s(z))) <= True
height_mid(node(a, node(a, leaf, leaf), leaf), right, s(z)) <= True
False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
flip(node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(s(z))))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(s(z))) /\ 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, node(a, leaf, leaf)), left, s(z))
}
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006192 s (model generation: 0.006025,  model checking: 0.000167):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb) -> 0
flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb) -> 0
height_mid(node(e, t1, t2), left, s(_rgb)) <= height_mid(t1, right, _rgb) -> 0
height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb) -> 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
}

eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb)  :
No: ()

flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb)  :
No: ()

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

height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb)  :
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.006405 s (model generation: 0.006325,  model checking: 0.000080):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb) -> 0
flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb) -> 0
height_mid(node(e, t1, t2), left, s(_rgb)) <= height_mid(t1, right, _rgb) -> 0
height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb) -> 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
}

eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb)  :
No: ()

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

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

height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb)  :
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.008666 s (model generation: 0.008563,  model checking: 0.000103):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb) -> 0
flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb) -> 0
height_mid(node(e, t1, t2), left, s(_rgb)) <= height_mid(t1, right, _rgb) -> 0
height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb) -> 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: ()

eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb)  :
Yes: {
_chb -> s(z)  ;  _dhb -> node(_ootqw_0, _ootqw_1, _ootqw_2)  ;  _ehb -> s(s(_aptqw_0))  ;  t1 -> node(_qotqw_0, _qotqw_1, _qotqw_2)
}

flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb)  :
No: ()

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

height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb)  :
Yes: {
_sgb -> 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.014301 s (model generation: 0.014139,  model checking: 0.000162):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb) -> 0
flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb) -> 0
height_mid(node(e, t1, t2), left, s(_rgb)) <= height_mid(t1, right, _rgb) -> 0
height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb) -> 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), 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)) <= 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)) <= _r_1(x_2_0)
  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: ()

eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb)  :
No: ()

flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb)  :
No: ()

height_mid(node(e, t1, t2), left, s(_rgb)) <= height_mid(t1, right, _rgb)  :
Yes: {
_rgb -> s(_hptqw_0)  ;  t1 -> node(_iptqw_0, _iptqw_1, _iptqw_2)
}

height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb)  :
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.015336 s (model generation: 0.015175,  model checking: 0.000161):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb) -> 0
flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb) -> 0
height_mid(node(e, t1, t2), left, s(_rgb)) <= height_mid(t1, right, _rgb) -> 0
height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb) -> 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, node(a, leaf, leaf), leaf), left, s(s(z))) <= True
False <= height_mid(node(a, 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)) <= 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_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: ()

eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb)  :
Yes: {
_chb -> s(s(_aqtqw_0))  ;  _dhb -> node(_kptqw_0, leaf, _kptqw_2)  ;  _ehb -> s(z)  ;  t1 -> node(_mptqw_0, node(_zptqw_0, _zptqw_1, _zptqw_2), _mptqw_2)
}

flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb)  :
No: ()

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

height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb)  :
Yes: {
_sgb -> z  ;  t1 -> node(_hqtqw_0, _hqtqw_1, _hqtqw_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 5, which took 0.017152 s (model generation: 0.016887,  model checking: 0.000265):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb) -> 0
flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb) -> 0
height_mid(node(e, t1, t2), left, s(_rgb)) <= height_mid(t1, right, _rgb) -> 0
height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb) -> 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, node(a, leaf, leaf), leaf), left, s(s(z))) <= True
height_mid(node(a, node(a, leaf, leaf), leaf), right, s(z)) <= True
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= height_mid(node(a, 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_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)) <= True
  height_mid(node(x_0_0, x_0_1, x_0_2), right, s(x_2_0)) <= _r_1(x_0_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: ()

eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb)  :
Yes: {
_chb -> s(s(z))  ;  _dhb -> node(_jqtqw_0, node(_krtqw_0, leaf, _krtqw_2), _jqtqw_2)  ;  _ehb -> s(s(s(_zrtqw_0)))  ;  t1 -> node(_lqtqw_0, node(_irtqw_0, leaf, _irtqw_2), _lqtqw_2)
}

flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb)  :
Yes: {
_xgb -> leaf  ;  _ygb -> node(_vqtqw_0, node(_trtqw_0, leaf, _trtqw_2), _vqtqw_2)  ;  t1 -> node(_wqtqw_0, node(_srtqw_0, leaf, _srtqw_2), _wqtqw_2)  ;  t2 -> leaf
}

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

height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb)  :
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.026211 s (model generation: 0.025992,  model checking: 0.000219):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb) -> 0
flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb) -> 0
height_mid(node(e, t1, t2), left, s(_rgb)) <= height_mid(t1, right, _rgb) -> 0
height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb) -> 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, node(a, leaf, leaf), leaf), left, s(s(z))) <= True
height_mid(node(a, node(a, leaf, leaf), leaf), right, s(z)) <= True
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
flip(node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(s(z))))
False <= height_mid(node(a, 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(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)) <= 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: ()

eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb)  :
Yes: {
_chb -> s(z)  ;  _dhb -> node(_bstqw_0, node(_attqw_0, _attqw_1, _attqw_2), leaf)  ;  _ehb -> s(s(_bttqw_0))  ;  t1 -> node(_dstqw_0, leaf, _dstqw_2)
}

flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb)  :
No: ()

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

height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb)  :
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.027923 s (model generation: 0.027580,  model checking: 0.000343):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb) -> 0
flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb) -> 0
height_mid(node(e, t1, t2), left, s(_rgb)) <= height_mid(t1, right, _rgb) -> 0
height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb) -> 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, node(a, leaf, leaf), leaf), left, s(s(z))) <= True
height_mid(node(a, node(a, leaf, leaf), leaf), right, s(z)) <= True
False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
flip(node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(s(z))))
False <= height_mid(node(a, 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_1) /\ 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)) <= 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)) <= True
  height_mid(node(x_0_0, x_0_1, x_0_2), right, s(x_2_0)) <= _r_1(x_0_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: ()

eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb)  :
Yes: {
_chb -> s(s(z))  ;  _dhb -> node(_wttqw_0, node(_nvtqw_0, leaf, _nvtqw_2), _wttqw_2)  ;  _ehb -> s(s(s(_zvtqw_0)))  ;  t1 -> node(_yttqw_0, node(_lvtqw_0, leaf, leaf), node(_pvtqw_0, leaf, leaf))
}

flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb)  :
Yes: {
_xgb -> node(_hutqw_0, leaf, _hutqw_2)  ;  _ygb -> leaf  ;  t1 -> leaf  ;  t2 -> node(_kutqw_0, leaf, leaf)
}

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

height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb)  :
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.032123 s (model generation: 0.031707,  model checking: 0.000416):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb) -> 0
flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb) -> 0
height_mid(node(e, t1, t2), left, s(_rgb)) <= height_mid(t1, right, _rgb) -> 0
height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb) -> 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, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, 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, node(a, leaf, leaf), leaf), left, s(s(z))) <= True
height_mid(node(a, node(a, leaf, leaf), leaf), right, s(z)) <= True
False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
flip(node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(s(z))))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(s(z)))
False <= height_mid(node(a, 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)) <= 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)) <= 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: ()

eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb)  :
Yes: {
_chb -> s(z)  ;  _dhb -> node(_fwtqw_0, node(_uxtqw_0, leaf, leaf), leaf)  ;  _ehb -> s(s(_vxtqw_0))  ;  t1 -> node(_hwtqw_0, leaf, node(_wxtqw_0, leaf, leaf))
}

flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb)  :
No: ()

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

height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb)  :
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.077492 s (model generation: 0.077020,  model checking: 0.000472):

Clauses:
{
flip(leaf, leaf) <= True -> 0
height_mid(leaf, d, z) <= True -> 0
eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb) -> 0
flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb) -> 0
height_mid(node(e, t1, t2), left, s(_rgb)) <= height_mid(t1, right, _rgb) -> 0
height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb) -> 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, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, 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, node(a, leaf, leaf), leaf), left, s(s(z))) <= True
height_mid(node(a, node(a, leaf, leaf), leaf), right, s(z)) <= True
False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
flip(node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(s(z))))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, 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, node(a, leaf, leaf)), left, 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_2(node(x_0_0, x_0_1, x_0_2)) <= 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), left, s(x_2_0)) <= _r_2(x_0_1)
  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: ()

eq_nat(_chb, _ehb) <= flip(t1, _dhb) /\ height_mid(_dhb, left, _ehb) /\ height_mid(t1, left, _chb)  :
Yes: {
_chb -> s(z)  ;  _dhb -> node(_hauqw_0, node(_hcuqw_0, leaf, leaf), node(_qduqw_0, leaf, leaf))  ;  _ehb -> s(s(_fcuqw_0))  ;  t1 -> node(_jauqw_0, node(_pduqw_0, leaf, leaf), node(_icuqw_0, leaf, leaf))
}

flip(node(e, t1, t2), node(e, _xgb, _ygb)) <= flip(t1, _ygb) /\ flip(t2, _xgb)  :
No: ()

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

height_mid(node(e, t1, t2), right, s(_sgb)) <= height_mid(t2, left, _sgb)  :
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.246661
Learner time: 0.229413
Teacher time: 0.002387
Reasons for stopping: No: Contradictory set of ground constraints:
{
False <= True
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, 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, node(a, leaf, leaf), leaf), left, s(s(z))) <= True
height_mid(node(a, node(a, leaf, leaf), leaf), right, s(z)) <= True
False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
flip(node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(s(z))))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) /\ height_mid(node(a, node(a, leaf, leaf), leaf), left, s(s(s(z)))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ height_mid(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), left, s(s(z))) /\ 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, node(a, leaf, leaf)), left, s(z))
}