Solving ../../benchmarks/smtlib/false/tree_depth_le_error.smt2...

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



Learning problem is:

env: {
elt -> {a, b}  ;  etree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(leq_nat, P:
{
leq_nat(z, n2) <= True
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2)
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2))
False <= leq_nat(s(nn1), z)
}
)
(le_nat, P:
{
le_nat(z, s(nn2)) <= True
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2)
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2))
False <= le_nat(s(nn1), z)
False <= le_nat(z, z)
}
)
(max, F:
{
leq_nat(n, m) \/ max(n, m, n) <= True
max(n, m, m) <= leq_nat(n, m)
}
eq_nat(_seb, _teb) <= max(_qeb, _reb, _seb) /\ max(_qeb, _reb, _teb)
)
(plus, F:
{
plus(n, z, n) <= True
plus(n, s(mm), s(_ueb)) <= plus(n, mm, _ueb)
}
eq_nat(_xeb, _yeb) <= plus(_veb, _web, _xeb) /\ plus(_veb, _web, _yeb)
)
(height, F:
{
height(leaf, z) <= True
height(node(e, t1, t2), s(_bfb)) <= height(t1, _zeb) /\ height(t2, _afb) /\ max(_zeb, _afb, _bfb)
}
eq_nat(_dfb, _efb) <= height(_cfb, _dfb) /\ height(_cfb, _efb)
)
(numnodes, F:
{
numnodes(leaf, z) <= True
numnodes(node(e, t1, t2), s(_hfb)) <= numnodes(t1, _ffb) /\ numnodes(t2, _gfb) /\ plus(_ffb, _gfb, _hfb)
}
eq_nat(_jfb, _kfb) <= numnodes(_ifb, _jfb) /\ numnodes(_ifb, _kfb)
)
}

properties:
{
le_nat(_lfb, _mfb) <= height(t1, _lfb) /\ numnodes(t1, _mfb)
}


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

Clause system for inference is:

{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
le_nat(_lfb, _mfb) <= height(t1, _lfb) /\ numnodes(t1, _mfb) -> 0
height(node(e, t1, t2), s(_bfb)) <= height(t1, _zeb) /\ height(t2, _afb) /\ max(_zeb, _afb, _bfb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
max(n, m, m) <= leq_nat(n, m) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_hfb)) <= numnodes(t1, _ffb) /\ numnodes(t2, _gfb) /\ plus(_ffb, _gfb, _hfb) -> 0
plus(n, s(mm), s(_ueb)) <= plus(n, mm, _ueb) -> 0
}


Solving took 0.112034 seconds.
No: Contradictory set of ground constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
le_nat(z, z) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
max(s(z), z, s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= le_nat(z, z)
False <= leq_nat(s(z), z)
}
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006357 s (model generation: 0.006178,  model checking: 0.000179):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
le_nat(_lfb, _mfb) <= height(t1, _lfb) /\ numnodes(t1, _mfb) -> 0
height(node(e, t1, t2), s(_bfb)) <= height(t1, _zeb) /\ height(t2, _afb) /\ max(_zeb, _afb, _bfb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
max(n, m, m) <= leq_nat(n, m) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_hfb)) <= numnodes(t1, _ffb) /\ numnodes(t2, _gfb) /\ plus(_ffb, _gfb, _hfb) -> 0
plus(n, s(mm), s(_ueb)) <= plus(n, mm, _ueb) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


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


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


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


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



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




Answer of teacher:

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

}

leq_nat(n, m) \/ max(n, m, n) <= True  :
Yes: {
m -> z  ;  n -> z
}

leq_nat(z, n2) <= True  :
Yes: {
n2 -> z
}

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

}

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

le_nat(_lfb, _mfb) <= height(t1, _lfb) /\ numnodes(t1, _mfb)  :
No: ()

height(node(e, t1, t2), s(_bfb)) <= height(t1, _zeb) /\ height(t2, _afb) /\ max(_zeb, _afb, _bfb)  :
No: ()

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

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

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

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

max(n, m, m) <= leq_nat(n, m)  :
No: ()

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

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

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

numnodes(node(e, t1, t2), s(_hfb)) <= numnodes(t1, _ffb) /\ numnodes(t2, _gfb) /\ plus(_ffb, _gfb, _hfb)  :
No: ()

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


-------------------------------------------
Step 1, which took 0.006417 s (model generation: 0.006239,  model checking: 0.000178):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
le_nat(_lfb, _mfb) <= height(t1, _lfb) /\ numnodes(t1, _mfb) -> 0
height(node(e, t1, t2), s(_bfb)) <= height(t1, _zeb) /\ height(t2, _afb) /\ max(_zeb, _afb, _bfb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
max(n, m, m) <= leq_nat(n, m) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_hfb)) <= numnodes(t1, _ffb) /\ numnodes(t2, _gfb) /\ plus(_ffb, _gfb, _hfb) -> 0
plus(n, s(mm), s(_ueb)) <= plus(n, mm, _ueb) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
leq_nat(z, z) <= True
numnodes(leaf, z) <= True
plus(z, z, z) <= True
}

Current best model:
|_
name: None

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


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


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


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


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


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



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




Answer of teacher:

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

leq_nat(n, m) \/ max(n, m, n) <= True  :
Yes: {
m -> z  ;  n -> s(_sjtqw_0)
}

leq_nat(z, n2) <= True  :
Yes: {
n2 -> s(_vjtqw_0)
}

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

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

le_nat(_lfb, _mfb) <= height(t1, _lfb) /\ numnodes(t1, _mfb)  :
Yes: {
_lfb -> z  ;  _mfb -> z  ;  t1 -> leaf
}

height(node(e, t1, t2), s(_bfb)) <= height(t1, _zeb) /\ height(t2, _afb) /\ max(_zeb, _afb, _bfb)  :
No: ()

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

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

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

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

max(n, m, m) <= leq_nat(n, m)  :
Yes: {
m -> z  ;  n -> z
}

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

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

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

numnodes(node(e, t1, t2), s(_hfb)) <= numnodes(t1, _ffb) /\ numnodes(t2, _gfb) /\ plus(_ffb, _gfb, _hfb)  :
Yes: {
_ffb -> z  ;  _gfb -> z  ;  _hfb -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

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


-------------------------------------------
Step 2, which took 0.009299 s (model generation: 0.009165,  model checking: 0.000134):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
le_nat(_lfb, _mfb) <= height(t1, _lfb) /\ numnodes(t1, _mfb) -> 0
height(node(e, t1, t2), s(_bfb)) <= height(t1, _zeb) /\ height(t2, _afb) /\ max(_zeb, _afb, _bfb) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
max(n, m, m) <= leq_nat(n, m) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_hfb)) <= numnodes(t1, _ffb) /\ numnodes(t2, _gfb) /\ plus(_ffb, _gfb, _hfb) -> 0
plus(n, s(mm), s(_ueb)) <= plus(n, mm, _ueb) -> 0
}

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

Current best model:
|_
name: None

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


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


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


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


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


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



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




Answer of teacher:

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

leq_nat(n, m) \/ max(n, m, n) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

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

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

le_nat(_lfb, _mfb) <= height(t1, _lfb) /\ numnodes(t1, _mfb)  :
No: ()

height(node(e, t1, t2), s(_bfb)) <= height(t1, _zeb) /\ height(t2, _afb) /\ max(_zeb, _afb, _bfb)  :
Yes: {
_afb -> z  ;  _bfb -> z  ;  _zeb -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

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

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

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

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

}

max(n, m, m) <= leq_nat(n, m)  :
Yes: {
m -> z  ;  n -> s(_wktqw_0)
}

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

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

False <= leq_nat(s(nn1), z)  :
Yes: {

}

numnodes(node(e, t1, t2), s(_hfb)) <= numnodes(t1, _ffb) /\ numnodes(t2, _gfb) /\ plus(_ffb, _gfb, _hfb)  :
No: ()

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


Total time: 0.112034
Learner time: 0.021582
Teacher time: 0.000491
Reasons for stopping: No: Contradictory set of ground constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
le_nat(z, z) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
max(s(z), z, s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= le_nat(z, z)
False <= leq_nat(s(z), z)
}