Solving ../../benchmarks/true/length_count.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


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.314511 seconds.
Proved
Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113, q_gen_3115, q_gen_3116, q_gen_3138},
Q_f={q_gen_3107},
Delta=
{
<cons>(q_gen_3113, q_gen_3112) -> q_gen_3112
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<b>() -> q_gen_3113
<s>(q_gen_3138) -> q_gen_3138
<z>() -> q_gen_3138
<cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3115
<cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3115
<nil, z>() -> q_gen_3115
<a, s>(q_gen_3138) -> q_gen_3116
<a, z>() -> q_gen_3116
<b, s>(q_gen_3138) -> q_gen_3116
<b, z>() -> q_gen_3116
<a, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<a, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<a, nil, z>() -> q_gen_3107
<b, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3106, q_gen_3110, q_gen_3128},
Q_f={q_gen_3106},
Delta=
{
<s>(q_gen_3128) -> q_gen_3128
<z>() -> q_gen_3128
<cons, s>(q_gen_3110, q_gen_3106) -> q_gen_3106
<nil, z>() -> q_gen_3106
<a, s>(q_gen_3128) -> q_gen_3110
<a, z>() -> q_gen_3110
<b, s>(q_gen_3128) -> q_gen_3110
<b, z>() -> q_gen_3110
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3105) -> q_gen_3105
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007497 s (model generation: 0.007287,  model checking: 0.000210):

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

}

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

}

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

}

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

}
--
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: Yes: (() -> leq([z, z]), {

})

-------------------------------------------
Step 1, which took 0.006516 s (model generation: 0.006390,  model checking: 0.000126):

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

}

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

}

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

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

}
--
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: Yes: (() -> leq([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.010999 s (model generation: 0.010432,  model checking: 0.000567):

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

}

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

}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<z>() -> q_gen_3105
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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: Yes: (() -> length([nil, z]), {

})

-------------------------------------------
Step 3, which took 0.010989 s (model generation: 0.010743,  model checking: 0.000246):

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

}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<z>() -> q_gen_3105
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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: Yes: (() -> count([x, nil, z]), {
x -> b
})

-------------------------------------------
Step 4, which took 0.011441 s (model generation: 0.011333,  model checking: 0.000108):

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

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<z>() -> q_gen_3105
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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: Yes: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 5, which took 0.003990 s (model generation: 0.003760,  model checking: 0.000230):

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

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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: Yes: ((length([ll, _qq])) -> length([cons(x, ll), s(_qq)]), {
_qq -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 6, which took 0.011583 s (model generation: 0.011277,  model checking: 0.000306):

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

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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: Yes: ((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.012574 s (model generation: 0.012184,  model checking: 0.000390):

Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113},
Q_f={q_gen_3107},
Delta=
{
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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: Yes: ((count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]), {
_uq -> z  ;  t1 -> nil  ;  x -> b
})

-------------------------------------------
Step 8, which took 0.012441 s (model generation: 0.011850,  model checking: 0.000591):

Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113, q_gen_3115, q_gen_3116},
Q_f={q_gen_3107},
Delta=
{
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<nil, z>() -> q_gen_3115
<b, z>() -> q_gen_3116
<b, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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: Yes: (() -> leq([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 9, which took 0.013578 s (model generation: 0.012776,  model checking: 0.000802):

Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113, q_gen_3115, q_gen_3116},
Q_f={q_gen_3107},
Delta=
{
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<nil, z>() -> q_gen_3115
<b, z>() -> q_gen_3116
<b, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3105) -> q_gen_3105
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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: Yes: (() -> count([x, nil, z]), {
x -> a
})

-------------------------------------------
Step 10, which took 0.013306 s (model generation: 0.012506,  model checking: 0.000800):

Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113, q_gen_3115, q_gen_3116},
Q_f={q_gen_3107},
Delta=
{
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<nil, z>() -> q_gen_3115
<b, z>() -> q_gen_3116
<a, nil, z>() -> q_gen_3107
<b, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3105) -> q_gen_3105
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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: Yes: ((length([ll, _qq])) -> length([cons(x, ll), s(_qq)]), {
_qq -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 11, which took 0.013347 s (model generation: 0.012601,  model checking: 0.000746):

Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113, q_gen_3115, q_gen_3116},
Q_f={q_gen_3107},
Delta=
{
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<nil, z>() -> q_gen_3115
<b, z>() -> q_gen_3116
<a, nil, z>() -> q_gen_3107
<b, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3105) -> q_gen_3105
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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: Yes: ((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.014075 s (model generation: 0.013197,  model checking: 0.000878):

Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113, q_gen_3115, q_gen_3116},
Q_f={q_gen_3107},
Delta=
{
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<b>() -> q_gen_3113
<nil, z>() -> q_gen_3115
<b, z>() -> q_gen_3116
<a, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<a, nil, z>() -> q_gen_3107
<b, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3105) -> q_gen_3105
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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: Yes: ((count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]), {
_uq -> z  ;  t1 -> nil  ;  x -> a
})

-------------------------------------------
Step 13, which took 0.015277 s (model generation: 0.013524,  model checking: 0.001753):

Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113, q_gen_3115, q_gen_3116},
Q_f={q_gen_3107},
Delta=
{
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<b>() -> q_gen_3113
<nil, z>() -> q_gen_3115
<a, z>() -> q_gen_3116
<b, z>() -> q_gen_3116
<a, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<a, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<a, nil, z>() -> q_gen_3107
<b, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3105) -> q_gen_3105
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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]) -> 7  ;  (length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 10  ;  (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: Yes: ((length([ll, _qq])) -> length([cons(x, ll), s(_qq)]), {
_qq -> s(z)  ;  ll -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 14, which took 0.015695 s (model generation: 0.014270,  model checking: 0.001425):

Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113, q_gen_3115, q_gen_3116},
Q_f={q_gen_3107},
Delta=
{
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<b>() -> q_gen_3113
<nil, z>() -> q_gen_3115
<a, z>() -> q_gen_3116
<b, z>() -> q_gen_3116
<a, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<a, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<a, nil, z>() -> q_gen_3107
<b, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3106, q_gen_3110, q_gen_3128},
Q_f={q_gen_3106},
Delta=
{
<z>() -> q_gen_3128
<cons, s>(q_gen_3110, q_gen_3106) -> q_gen_3106
<nil, z>() -> q_gen_3106
<a, z>() -> q_gen_3110
<b, s>(q_gen_3128) -> q_gen_3110
<b, z>() -> q_gen_3110
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3105) -> q_gen_3105
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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)]) -> 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)]) -> 10  ;  (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: Yes: ((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
})

-------------------------------------------
Step 15, which took 0.015784 s (model generation: 0.014529,  model checking: 0.001255):

Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113, q_gen_3115, q_gen_3116},
Q_f={q_gen_3107},
Delta=
{
<cons>(q_gen_3113, q_gen_3112) -> q_gen_3112
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<b>() -> q_gen_3113
<nil, z>() -> q_gen_3115
<a, z>() -> q_gen_3116
<b, z>() -> q_gen_3116
<a, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<a, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<a, nil, z>() -> q_gen_3107
<b, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3106, q_gen_3110, q_gen_3128},
Q_f={q_gen_3106},
Delta=
{
<z>() -> q_gen_3128
<cons, s>(q_gen_3110, q_gen_3106) -> q_gen_3106
<nil, z>() -> q_gen_3106
<a, z>() -> q_gen_3110
<b, s>(q_gen_3128) -> q_gen_3110
<b, z>() -> q_gen_3110
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3105) -> q_gen_3105
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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]) -> 7  ;  () -> leq([z, s(nn2)]) -> 7  ;  () -> 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]) -> 10  ;  (length([ll, _qq])) -> length([cons(x, ll), s(_qq)]) -> 10  ;  (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: Yes: ((count([x, t1, _uq])) -> count([x, cons(x, t1), s(_uq)]), {
_uq -> z  ;  t1 -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 16, which took 0.014722 s (model generation: 0.013074,  model checking: 0.001648):

Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113, q_gen_3115, q_gen_3116},
Q_f={q_gen_3107},
Delta=
{
<cons>(q_gen_3113, q_gen_3112) -> q_gen_3112
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<b>() -> q_gen_3113
<cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3115
<nil, z>() -> q_gen_3115
<a, z>() -> q_gen_3116
<b, z>() -> q_gen_3116
<a, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<a, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<a, nil, z>() -> q_gen_3107
<b, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3106, q_gen_3110, q_gen_3128},
Q_f={q_gen_3106},
Delta=
{
<z>() -> q_gen_3128
<cons, s>(q_gen_3110, q_gen_3106) -> q_gen_3106
<nil, z>() -> q_gen_3106
<a, z>() -> q_gen_3110
<b, s>(q_gen_3128) -> q_gen_3110
<b, z>() -> q_gen_3110
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3105) -> q_gen_3105
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

}
--
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]) -> 8  ;  () -> leq([z, s(nn2)]) -> 8  ;  () -> leq([z, z]) -> 8  ;  (count([x, l, _ar]) /\ length([l, _br])) -> leq([_ar, _br]) -> 8  ;  (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)]) -> 13  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9  ;  (leq([s(nn1), z])) -> BOT -> 9
}
Sat witness: Yes: ((length([ll, _qq])) -> length([cons(x, ll), s(_qq)]), {
_qq -> s(z)  ;  ll -> cons(b, nil)  ;  x -> a
})

-------------------------------------------
Step 17, which took 0.019335 s (model generation: 0.016239,  model checking: 0.003096):

Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113, q_gen_3115, q_gen_3116},
Q_f={q_gen_3107},
Delta=
{
<cons>(q_gen_3113, q_gen_3112) -> q_gen_3112
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<b>() -> q_gen_3113
<cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3115
<nil, z>() -> q_gen_3115
<a, z>() -> q_gen_3116
<b, z>() -> q_gen_3116
<a, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<a, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<a, nil, z>() -> q_gen_3107
<b, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3106, q_gen_3110, q_gen_3128},
Q_f={q_gen_3106},
Delta=
{
<z>() -> q_gen_3128
<cons, s>(q_gen_3110, q_gen_3106) -> q_gen_3106
<nil, z>() -> q_gen_3106
<a, s>(q_gen_3128) -> q_gen_3110
<a, z>() -> q_gen_3110
<b, s>(q_gen_3128) -> q_gen_3110
<b, z>() -> q_gen_3110
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3105) -> q_gen_3105
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

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

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

-------------------------------------------
Step 18, which took 0.017745 s (model generation: 0.016011,  model checking: 0.001734):

Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113, q_gen_3115, q_gen_3116, q_gen_3138},
Q_f={q_gen_3107},
Delta=
{
<cons>(q_gen_3113, q_gen_3112) -> q_gen_3112
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<b>() -> q_gen_3113
<z>() -> q_gen_3138
<cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3115
<cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3115
<nil, z>() -> q_gen_3115
<a, z>() -> q_gen_3116
<b, s>(q_gen_3138) -> q_gen_3116
<b, z>() -> q_gen_3116
<a, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<a, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<a, nil, z>() -> q_gen_3107
<b, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3106, q_gen_3110, q_gen_3128},
Q_f={q_gen_3106},
Delta=
{
<z>() -> q_gen_3128
<cons, s>(q_gen_3110, q_gen_3106) -> q_gen_3106
<nil, z>() -> q_gen_3106
<a, s>(q_gen_3128) -> q_gen_3110
<a, z>() -> q_gen_3110
<b, s>(q_gen_3128) -> q_gen_3110
<b, z>() -> q_gen_3110
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3105) -> q_gen_3105
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

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

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

-------------------------------------------
Step 19, which took 0.020504 s (model generation: 0.018711,  model checking: 0.001793):

Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113, q_gen_3115, q_gen_3116, q_gen_3138},
Q_f={q_gen_3107},
Delta=
{
<cons>(q_gen_3113, q_gen_3112) -> q_gen_3112
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<b>() -> q_gen_3113
<z>() -> q_gen_3138
<cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3115
<cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3115
<nil, z>() -> q_gen_3115
<a, s>(q_gen_3138) -> q_gen_3116
<a, z>() -> q_gen_3116
<b, s>(q_gen_3138) -> q_gen_3116
<b, z>() -> q_gen_3116
<a, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<a, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<a, nil, z>() -> q_gen_3107
<b, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3106, q_gen_3110, q_gen_3128},
Q_f={q_gen_3106},
Delta=
{
<z>() -> q_gen_3128
<cons, s>(q_gen_3110, q_gen_3106) -> q_gen_3106
<nil, z>() -> q_gen_3106
<a, s>(q_gen_3128) -> q_gen_3110
<a, z>() -> q_gen_3110
<b, s>(q_gen_3128) -> q_gen_3110
<b, z>() -> q_gen_3110
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3105) -> q_gen_3105
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

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

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

-------------------------------------------
Step 20, which took 0.028108 s (model generation: 0.021309,  model checking: 0.006799):

Model:
|_
{
count -> 
{{{
Q={q_gen_3107, q_gen_3112, q_gen_3113, q_gen_3115, q_gen_3116, q_gen_3138},
Q_f={q_gen_3107},
Delta=
{
<cons>(q_gen_3113, q_gen_3112) -> q_gen_3112
<nil>() -> q_gen_3112
<a>() -> q_gen_3113
<b>() -> q_gen_3113
<z>() -> q_gen_3138
<cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3115
<cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3115
<nil, z>() -> q_gen_3115
<a, s>(q_gen_3138) -> q_gen_3116
<a, z>() -> q_gen_3116
<b, s>(q_gen_3138) -> q_gen_3116
<b, z>() -> q_gen_3116
<a, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<a, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<a, nil, z>() -> q_gen_3107
<b, cons, s>(q_gen_3116, q_gen_3115) -> q_gen_3107
<b, cons, z>(q_gen_3113, q_gen_3112) -> q_gen_3107
<b, nil, z>() -> q_gen_3107
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3106, q_gen_3110, q_gen_3128},
Q_f={q_gen_3106},
Delta=
{
<s>(q_gen_3128) -> q_gen_3128
<z>() -> q_gen_3128
<cons, s>(q_gen_3110, q_gen_3106) -> q_gen_3106
<nil, z>() -> q_gen_3106
<a, s>(q_gen_3128) -> q_gen_3110
<a, z>() -> q_gen_3110
<b, s>(q_gen_3128) -> q_gen_3110
<b, z>() -> q_gen_3110
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_3103, q_gen_3105},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3105) -> q_gen_3105
<z>() -> q_gen_3105
<s, s>(q_gen_3103) -> q_gen_3103
<z, s>(q_gen_3105) -> q_gen_3103
<z, z>() -> q_gen_3103
}

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

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

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

Total time: 0.314511
Reason for stopping: Proved