Inference procedure has parameters:
Ice fuel: 200
Timeout: 60s
Convolution: right


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{() -> leq([z, s(nn2)])
() -> leq([z, z])
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)])
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2])
(leq([s(nn1), z])) -> BOT}
)
(length, F:
{() -> length([nil, z])
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)])}
(length([_rq, _sq]) /\ length([_rq, _tq])) -> eq_nat([_sq, _tq])
)
(count, F:
{() -> count([x, nil, z])
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)])
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq])}
(count([_wq, _xq, _yq]) /\ count([_wq, _xq, _zq])) -> eq_nat([_yq, _zq])
)
}

properties:
{(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br])}


over-approximation: {count, length}
under-approximation: {leq}

Clause system for inference is:

{
() -> count([x, nil, z]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 0
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 0
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 0
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 0
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 0
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0
(leq([s(nn1), z])) -> BOT -> 0
}


Solving took 0.111358 seconds.
Proved
Model:
|_
{
count -> 
{{{
Q={q_gen_3218, q_gen_3223, q_gen_3224, q_gen_3226},
Q_f={q_gen_3218},
Delta=
{
<cons>(q_gen_3224, q_gen_3223) -> q_gen_3223
<nil>() -> q_gen_3223
<a>() -> q_gen_3224
<b>() -> q_gen_3224
<cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3226
<cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3226
<nil, z>() -> q_gen_3226
<a, cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3218
<a, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<a, nil, z>() -> q_gen_3218
<b, cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3218
<b, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<b, nil, z>() -> q_gen_3218
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_3217, q_gen_3221},
Q_f={q_gen_3217},
Delta=
{
<a>() -> q_gen_3221
<b>() -> q_gen_3221
<cons, s>(q_gen_3221, q_gen_3217) -> q_gen_3217
<nil, z>() -> q_gen_3217
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<s>(q_gen_3216) -> q_gen_3216
<z>() -> q_gen_3216
<s, s>(q_gen_3214) -> q_gen_3214
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.012198 s (model generation: 0.011508,  model checking: 0.000690):

Model:
|_
{
count -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 3
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 1
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 1
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 1
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([z, z]), {

})

-------------------------------------------
Step 1, which took 0.007731 s (model generation: 0.006690,  model checking: 0.001041):

Model:
|_
{
count -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214},
Q_f={q_gen_3214},
Delta=
{
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 1
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 1
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 1
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.005953 s (model generation: 0.005872,  model checking: 0.000081):

Model:
|_
{
count -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<z>() -> q_gen_3216
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 0
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 1
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 1
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 1
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> length([nil, z]), {

})

-------------------------------------------
Step 3, which took 0.004686 s (model generation: 0.004606,  model checking: 0.000080):

Model:
|_
{
count -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_3217},
Q_f={q_gen_3217},
Delta=
{
<nil, z>() -> q_gen_3217
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<z>() -> q_gen_3216
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 1
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 1
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 1
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> count([x, nil, z]), {
x -> b
})

-------------------------------------------
Step 4, which took 0.004866 s (model generation: 0.004722,  model checking: 0.000144):

Model:
|_
{
count -> 
{{{
Q={q_gen_3218},
Q_f={q_gen_3218},
Delta=
{
<b, nil, z>() -> q_gen_3218
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_3217},
Q_f={q_gen_3217},
Delta=
{
<nil, z>() -> q_gen_3217
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<z>() -> q_gen_3216
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 1
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 1
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 1
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 5, which took 0.005230 s (model generation: 0.005126,  model checking: 0.000104):

Model:
|_
{
count -> 
{{{
Q={q_gen_3218},
Q_f={q_gen_3218},
Delta=
{
<b, nil, z>() -> q_gen_3218
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_3217},
Q_f={q_gen_3217},
Delta=
{
<nil, z>() -> q_gen_3217
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<z>() -> q_gen_3216
<s, s>(q_gen_3214) -> q_gen_3214
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 1
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 1
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 1
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((length([ll, _qq])) -> length([cons(x, ll), s(_qq)]), {
_qq -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 6, which took 0.004566 s (model generation: 0.004179,  model checking: 0.000387):

Model:
|_
{
count -> 
{{{
Q={q_gen_3218},
Q_f={q_gen_3218},
Delta=
{
<b, nil, z>() -> q_gen_3218
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_3217, q_gen_3221},
Q_f={q_gen_3217},
Delta=
{
<b>() -> q_gen_3221
<cons, s>(q_gen_3221, q_gen_3217) -> q_gen_3217
<nil, z>() -> q_gen_3217
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<z>() -> q_gen_3216
<s, s>(q_gen_3214) -> q_gen_3214
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 1
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 1
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 4
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]), {
_vq -> z  ;  h1 -> a  ;  t1 -> nil  ;  x -> b
})

-------------------------------------------
Step 7, which took 0.006069 s (model generation: 0.005618,  model checking: 0.000451):

Model:
|_
{
count -> 
{{{
Q={q_gen_3218, q_gen_3223, q_gen_3224},
Q_f={q_gen_3218},
Delta=
{
<nil>() -> q_gen_3223
<a>() -> q_gen_3224
<b, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<b, nil, z>() -> q_gen_3218
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_3217, q_gen_3221},
Q_f={q_gen_3217},
Delta=
{
<b>() -> q_gen_3221
<cons, s>(q_gen_3221, q_gen_3217) -> q_gen_3217
<nil, z>() -> q_gen_3217
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<z>() -> q_gen_3216
<s, s>(q_gen_3214) -> q_gen_3214
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 1
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 4
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 4
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]), {
_uq -> z  ;  t1 -> nil  ;  x -> b
})

-------------------------------------------
Step 8, which took 0.006207 s (model generation: 0.005621,  model checking: 0.000586):

Model:
|_
{
count -> 
{{{
Q={q_gen_3218, q_gen_3223, q_gen_3224, q_gen_3226},
Q_f={q_gen_3218},
Delta=
{
<nil>() -> q_gen_3223
<a>() -> q_gen_3224
<b>() -> q_gen_3224
<nil, z>() -> q_gen_3226
<b, cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3218
<b, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<b, nil, z>() -> q_gen_3218
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_3217, q_gen_3221},
Q_f={q_gen_3217},
Delta=
{
<b>() -> q_gen_3221
<cons, s>(q_gen_3221, q_gen_3217) -> q_gen_3217
<nil, z>() -> q_gen_3217
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<z>() -> q_gen_3216
<s, s>(q_gen_3214) -> q_gen_3214
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 2
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 4
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 4
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3
(leq([s(nn1), z])) -> BOT -> 3
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 9, which took 0.006148 s (model generation: 0.005372,  model checking: 0.000776):

Model:
|_
{
count -> 
{{{
Q={q_gen_3218, q_gen_3223, q_gen_3224, q_gen_3226},
Q_f={q_gen_3218},
Delta=
{
<nil>() -> q_gen_3223
<a>() -> q_gen_3224
<b>() -> q_gen_3224
<nil, z>() -> q_gen_3226
<b, cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3218
<b, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<b, nil, z>() -> q_gen_3218
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_3217, q_gen_3221},
Q_f={q_gen_3217},
Delta=
{
<b>() -> q_gen_3221
<cons, s>(q_gen_3221, q_gen_3217) -> q_gen_3217
<nil, z>() -> q_gen_3217
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<s>(q_gen_3216) -> q_gen_3216
<z>() -> q_gen_3216
<s, s>(q_gen_3214) -> q_gen_3214
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 6
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 3
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 4
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 4
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
}
Sat witness: Found: (() -> count([x, nil, z]), {
x -> a
})

-------------------------------------------
Step 10, which took 0.006508 s (model generation: 0.005582,  model checking: 0.000926):

Model:
|_
{
count -> 
{{{
Q={q_gen_3218, q_gen_3223, q_gen_3224, q_gen_3226},
Q_f={q_gen_3218},
Delta=
{
<nil>() -> q_gen_3223
<a>() -> q_gen_3224
<b>() -> q_gen_3224
<nil, z>() -> q_gen_3226
<a, nil, z>() -> q_gen_3218
<b, cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3218
<b, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<b, nil, z>() -> q_gen_3218
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_3217, q_gen_3221},
Q_f={q_gen_3217},
Delta=
{
<b>() -> q_gen_3221
<cons, s>(q_gen_3221, q_gen_3217) -> q_gen_3217
<nil, z>() -> q_gen_3217
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<s>(q_gen_3216) -> q_gen_3216
<z>() -> q_gen_3216
<s, s>(q_gen_3214) -> q_gen_3214
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 6
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 4
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 4
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 4
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5
(leq([s(nn1), z])) -> BOT -> 5
}
Sat witness: Found: ((length([ll, _qq])) -> length([cons(x, ll), s(_qq)]), {
_qq -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 11, which took 0.006501 s (model generation: 0.006046,  model checking: 0.000455):

Model:
|_
{
count -> 
{{{
Q={q_gen_3218, q_gen_3223, q_gen_3224, q_gen_3226},
Q_f={q_gen_3218},
Delta=
{
<nil>() -> q_gen_3223
<a>() -> q_gen_3224
<b>() -> q_gen_3224
<nil, z>() -> q_gen_3226
<a, nil, z>() -> q_gen_3218
<b, cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3218
<b, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<b, nil, z>() -> q_gen_3218
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_3217, q_gen_3221},
Q_f={q_gen_3217},
Delta=
{
<a>() -> q_gen_3221
<b>() -> q_gen_3221
<cons, s>(q_gen_3221, q_gen_3217) -> q_gen_3217
<nil, z>() -> q_gen_3217
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<s>(q_gen_3216) -> q_gen_3216
<z>() -> q_gen_3216
<s, s>(q_gen_3214) -> q_gen_3214
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 6
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 4
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 4
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 7
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5
(leq([s(nn1), z])) -> BOT -> 5
}
Sat witness: Found: ((count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]), {
_vq -> z  ;  h1 -> b  ;  t1 -> nil  ;  x -> a
})

-------------------------------------------
Step 12, which took 0.005913 s (model generation: 0.005593,  model checking: 0.000320):

Model:
|_
{
count -> 
{{{
Q={q_gen_3218, q_gen_3223, q_gen_3224, q_gen_3226},
Q_f={q_gen_3218},
Delta=
{
<nil>() -> q_gen_3223
<a>() -> q_gen_3224
<b>() -> q_gen_3224
<nil, z>() -> q_gen_3226
<a, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<a, nil, z>() -> q_gen_3218
<b, cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3218
<b, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<b, nil, z>() -> q_gen_3218
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_3217, q_gen_3221},
Q_f={q_gen_3217},
Delta=
{
<a>() -> q_gen_3221
<b>() -> q_gen_3221
<cons, s>(q_gen_3221, q_gen_3217) -> q_gen_3217
<nil, z>() -> q_gen_3217
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<s>(q_gen_3216) -> q_gen_3216
<z>() -> q_gen_3216
<s, s>(q_gen_3214) -> q_gen_3214
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 6
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 4
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 7
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 7
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5
(leq([s(nn1), z])) -> BOT -> 5
}
Sat witness: Found: ((count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]), {
_uq -> z  ;  t1 -> nil  ;  x -> a
})

-------------------------------------------
Step 13, which took 0.006580 s (model generation: 0.005983,  model checking: 0.000597):

Model:
|_
{
count -> 
{{{
Q={q_gen_3218, q_gen_3223, q_gen_3224, q_gen_3226},
Q_f={q_gen_3218},
Delta=
{
<nil>() -> q_gen_3223
<a>() -> q_gen_3224
<b>() -> q_gen_3224
<nil, z>() -> q_gen_3226
<a, cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3218
<a, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<a, nil, z>() -> q_gen_3218
<b, cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3218
<b, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<b, nil, z>() -> q_gen_3218
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_3217, q_gen_3221},
Q_f={q_gen_3217},
Delta=
{
<a>() -> q_gen_3221
<b>() -> q_gen_3221
<cons, s>(q_gen_3221, q_gen_3217) -> q_gen_3217
<nil, z>() -> q_gen_3217
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<s>(q_gen_3216) -> q_gen_3216
<z>() -> q_gen_3216
<s, s>(q_gen_3214) -> q_gen_3214
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 7
() -> length([nil, z]) -> 5
() -> leq([z, s(nn2)]) -> 7
() -> leq([z, z]) -> 5
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 5
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 7
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 10
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 8
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 6
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6
(leq([s(nn1), z])) -> BOT -> 6
}
Sat witness: Found: ((count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]), {
_vq -> s(z)  ;  h1 -> b  ;  t1 -> cons(b, nil)  ;  x -> a
})

-------------------------------------------
Step 14, which took 0.007522 s (model generation: 0.006936,  model checking: 0.000586):

Model:
|_
{
count -> 
{{{
Q={q_gen_3218, q_gen_3223, q_gen_3224, q_gen_3226},
Q_f={q_gen_3218},
Delta=
{
<nil>() -> q_gen_3223
<a>() -> q_gen_3224
<b>() -> q_gen_3224
<cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3226
<nil, z>() -> q_gen_3226
<a, cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3218
<a, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<a, nil, z>() -> q_gen_3218
<b, cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3218
<b, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<b, nil, z>() -> q_gen_3218
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_3217, q_gen_3221},
Q_f={q_gen_3217},
Delta=
{
<a>() -> q_gen_3221
<b>() -> q_gen_3221
<cons, s>(q_gen_3221, q_gen_3217) -> q_gen_3217
<nil, z>() -> q_gen_3217
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<s>(q_gen_3216) -> q_gen_3216
<z>() -> q_gen_3216
<s, s>(q_gen_3214) -> q_gen_3214
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 7
() -> length([nil, z]) -> 6
() -> leq([z, s(nn2)]) -> 7
() -> leq([z, z]) -> 6
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 6
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 10
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 10
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 8
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 7
}
Sat witness: Found: ((count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]), {
_uq -> s(z)  ;  t1 -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 15, which took 0.007181 s (model generation: 0.006329,  model checking: 0.000852):

Model:
|_
{
count -> 
{{{
Q={q_gen_3218, q_gen_3223, q_gen_3224, q_gen_3226},
Q_f={q_gen_3218},
Delta=
{
<nil>() -> q_gen_3223
<a>() -> q_gen_3224
<b>() -> q_gen_3224
<cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3226
<cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3226
<nil, z>() -> q_gen_3226
<a, cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3218
<a, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<a, nil, z>() -> q_gen_3218
<b, cons, s>(q_gen_3224, q_gen_3226) -> q_gen_3218
<b, cons, z>(q_gen_3224, q_gen_3223) -> q_gen_3218
<b, nil, z>() -> q_gen_3218
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_3217, q_gen_3221},
Q_f={q_gen_3217},
Delta=
{
<a>() -> q_gen_3221
<b>() -> q_gen_3221
<cons, s>(q_gen_3221, q_gen_3217) -> q_gen_3217
<nil, z>() -> q_gen_3217
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_3214, q_gen_3216},
Q_f={q_gen_3214},
Delta=
{
<s>(q_gen_3216) -> q_gen_3216
<z>() -> q_gen_3216
<s, s>(q_gen_3214) -> q_gen_3214
<z, s>(q_gen_3216) -> q_gen_3214
<z, z>() -> q_gen_3214
}

Datatype: <nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 8
() -> length([nil, z]) -> 7
() -> leq([z, s(nn2)]) -> 8
() -> leq([z, z]) -> 7
(count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 7
(count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]) -> 10
(count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]) -> 13
(length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 9
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8
(leq([s(nn1), z])) -> BOT -> 8
}
Sat witness: Found: ((count([x, t1, _vq]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _vq]), {
_vq -> z  ;  h1 -> b  ;  t1 -> cons(b, nil)  ;  x -> a
})

Total time: 0.111358
Reason for stopping: Proved