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:
{
(le, P:
{() -> le([z, s(nn2)])
(le([nn1, nn2])) -> le([s(nn1), s(nn2)])
(le([s(nn1), s(nn2)])) -> le([nn1, nn2])
(le([s(nn1), z])) -> BOT
(le([z, z])) -> BOT}
)
(length, F:
{() -> length([nil, z])
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)])}
(length([_np, _op]) /\ length([_np, _pp])) -> eq_nat([_op, _pp])
)
(fcons, F:
{() -> fcons([x, l, cons(x, l)])}
(fcons([_qp, _rp, _sp]) /\ fcons([_qp, _rp, _tp])) -> eq_eltlist([_sp, _tp])
)
}

properties:
{(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp])}


over-approximation: {fcons, length}
under-approximation: {le}

Clause system for inference is:

{
() -> fcons([x, l, cons(x, l)]) -> 0
() -> le([z, s(nn2)]) -> 0
() -> length([nil, z]) -> 0
(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 0
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 0
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 0
(le([s(nn1), z])) -> BOT -> 0
(le([z, z])) -> BOT -> 0
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 0
}


Solving took 0.178850 seconds.
Proved
Model:
|_
{
fcons -> 
{{{
Q={q_gen_3078, q_gen_3079, q_gen_3080, q_gen_3091, q_gen_3092},
Q_f={q_gen_3078},
Delta=
{
<nil>() -> q_gen_3079
<a>() -> q_gen_3080
<b>() -> q_gen_3080
<cons, cons>(q_gen_3092, q_gen_3091) -> q_gen_3091
<nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3091
<a, a>() -> q_gen_3092
<a, b>() -> q_gen_3092
<b, a>() -> q_gen_3092
<b, b>() -> q_gen_3092
<a, cons, cons>(q_gen_3092, q_gen_3091) -> q_gen_3078
<a, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
<b, cons, cons>(q_gen_3092, q_gen_3091) -> q_gen_3078
<b, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_3076, q_gen_3077},
Q_f={q_gen_3076},
Delta=
{
<s>(q_gen_3077) -> q_gen_3077
<z>() -> q_gen_3077
<s, s>(q_gen_3076) -> q_gen_3076
<z, s>(q_gen_3077) -> q_gen_3076
}

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010075 s (model generation: 0.009795,  model checking: 0.000280):

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 0
() -> le([z, s(nn2)]) -> 0
() -> length([nil, z]) -> 3
(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 1
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1
(le([s(nn1), z])) -> BOT -> 1
(le([z, z])) -> BOT -> 1
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 1
}
Sat witness: Found: (() -> length([nil, z]), {

})

-------------------------------------------
Step 1, which took 0.010171 s (model generation: 0.010058,  model checking: 0.000113):

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 0
() -> le([z, s(nn2)]) -> 3
() -> length([nil, z]) -> 3
(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 1
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1
(le([s(nn1), z])) -> BOT -> 1
(le([z, z])) -> BOT -> 1
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 1
}
Sat witness: Found: (() -> le([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.011193 s (model generation: 0.010360,  model checking: 0.000833):

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

}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_3076, q_gen_3077},
Q_f={q_gen_3076},
Delta=
{
<z>() -> q_gen_3077
<z, s>(q_gen_3077) -> q_gen_3076
}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 3
() -> le([z, s(nn2)]) -> 3
() -> length([nil, z]) -> 3
(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 1
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1
(le([s(nn1), z])) -> BOT -> 1
(le([z, z])) -> BOT -> 1
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 1
}
Sat witness: Found: (() -> fcons([x, l, cons(x, l)]), {
l -> nil  ;  x -> b
})

-------------------------------------------
Step 3, which took 0.010597 s (model generation: 0.010406,  model checking: 0.000191):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3078, q_gen_3079, q_gen_3080},
Q_f={q_gen_3078},
Delta=
{
<nil>() -> q_gen_3079
<b>() -> q_gen_3080
<b, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_3076, q_gen_3077},
Q_f={q_gen_3076},
Delta=
{
<z>() -> q_gen_3077
<z, s>(q_gen_3077) -> q_gen_3076
}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 3
() -> le([z, s(nn2)]) -> 3
() -> length([nil, z]) -> 3
(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 1
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1
(le([s(nn1), z])) -> BOT -> 1
(le([z, z])) -> BOT -> 1
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 4
}
Sat witness: Found: ((length([ll, _mp])) -> length([cons(x, ll), s(_mp)]), {
_mp -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 4, which took 0.011066 s (model generation: 0.010825,  model checking: 0.000241):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3078, q_gen_3079, q_gen_3080},
Q_f={q_gen_3078},
Delta=
{
<nil>() -> q_gen_3079
<b>() -> q_gen_3080
<b, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_3076, q_gen_3077},
Q_f={q_gen_3076},
Delta=
{
<z>() -> q_gen_3077
<z, s>(q_gen_3077) -> q_gen_3076
}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 3
() -> le([z, s(nn2)]) -> 3
() -> length([nil, z]) -> 3
(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 1
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 2
(le([s(nn1), z])) -> BOT -> 2
(le([z, z])) -> BOT -> 2
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 4
}
Sat witness: Found: ((le([nn1, nn2])) -> le([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> s(z)
})

-------------------------------------------
Step 5, which took 0.011487 s (model generation: 0.010928,  model checking: 0.000559):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3078, q_gen_3079, q_gen_3080},
Q_f={q_gen_3078},
Delta=
{
<nil>() -> q_gen_3079
<b>() -> q_gen_3080
<b, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_3076, q_gen_3077},
Q_f={q_gen_3076},
Delta=
{
<z>() -> q_gen_3077
<s, s>(q_gen_3076) -> q_gen_3076
<z, s>(q_gen_3077) -> q_gen_3076
}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 3
() -> le([z, s(nn2)]) -> 6
() -> length([nil, z]) -> 4
(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 2
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 3
(le([s(nn1), z])) -> BOT -> 3
(le([z, z])) -> BOT -> 3
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 4
}
Sat witness: Found: (() -> le([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 6, which took 0.012688 s (model generation: 0.012031,  model checking: 0.000657):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3078, q_gen_3079, q_gen_3080},
Q_f={q_gen_3078},
Delta=
{
<nil>() -> q_gen_3079
<b>() -> q_gen_3080
<b, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_3076, q_gen_3077},
Q_f={q_gen_3076},
Delta=
{
<s>(q_gen_3077) -> q_gen_3077
<z>() -> q_gen_3077
<s, s>(q_gen_3076) -> q_gen_3076
<z, s>(q_gen_3077) -> q_gen_3076
}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 6
() -> le([z, s(nn2)]) -> 6
() -> length([nil, z]) -> 4
(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 3
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 4
(le([s(nn1), z])) -> BOT -> 4
(le([z, z])) -> BOT -> 4
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 4
}
Sat witness: Found: (() -> fcons([x, l, cons(x, l)]), {
l -> nil  ;  x -> a
})

-------------------------------------------
Step 7, which took 0.012153 s (model generation: 0.011780,  model checking: 0.000373):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3078, q_gen_3079, q_gen_3080},
Q_f={q_gen_3078},
Delta=
{
<nil>() -> q_gen_3079
<a>() -> q_gen_3080
<b>() -> q_gen_3080
<a, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
<b, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_3076, q_gen_3077},
Q_f={q_gen_3076},
Delta=
{
<s>(q_gen_3077) -> q_gen_3077
<z>() -> q_gen_3077
<s, s>(q_gen_3076) -> q_gen_3076
<z, s>(q_gen_3077) -> q_gen_3076
}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 6
() -> le([z, s(nn2)]) -> 6
() -> length([nil, z]) -> 4
(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 4
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 4
(le([s(nn1), z])) -> BOT -> 4
(le([z, z])) -> BOT -> 4
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 7
}
Sat witness: Found: ((length([ll, _mp])) -> length([cons(x, ll), s(_mp)]), {
_mp -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 8, which took 0.013695 s (model generation: 0.012087,  model checking: 0.001608):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3078, q_gen_3079, q_gen_3080},
Q_f={q_gen_3078},
Delta=
{
<nil>() -> q_gen_3079
<a>() -> q_gen_3080
<b>() -> q_gen_3080
<a, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
<b, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_3076, q_gen_3077},
Q_f={q_gen_3076},
Delta=
{
<s>(q_gen_3077) -> q_gen_3077
<z>() -> q_gen_3077
<s, s>(q_gen_3076) -> q_gen_3076
<z, s>(q_gen_3077) -> q_gen_3076
}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 9
() -> le([z, s(nn2)]) -> 7
() -> length([nil, z]) -> 5
(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 5
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 5
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 5
(le([s(nn1), z])) -> BOT -> 5
(le([z, z])) -> BOT -> 5
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 7
}
Sat witness: Found: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(b, nil)  ;  x -> a
})

-------------------------------------------
Step 9, which took 0.014150 s (model generation: 0.012559,  model checking: 0.001591):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3078, q_gen_3079, q_gen_3080, q_gen_3091, q_gen_3092},
Q_f={q_gen_3078},
Delta=
{
<nil>() -> q_gen_3079
<a>() -> q_gen_3080
<b>() -> q_gen_3080
<nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3091
<b, a>() -> q_gen_3092
<a, cons, cons>(q_gen_3092, q_gen_3091) -> q_gen_3078
<a, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
<b, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_3076, q_gen_3077},
Q_f={q_gen_3076},
Delta=
{
<s>(q_gen_3077) -> q_gen_3077
<z>() -> q_gen_3077
<s, s>(q_gen_3076) -> q_gen_3076
<z, s>(q_gen_3077) -> q_gen_3076
}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 12
() -> le([z, s(nn2)]) -> 8
() -> length([nil, z]) -> 6
(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 6
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 6
(le([s(nn1), z])) -> BOT -> 6
(le([z, z])) -> BOT -> 6
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 8
}
Sat witness: Found: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 10, which took 0.014406 s (model generation: 0.012751,  model checking: 0.001655):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3078, q_gen_3079, q_gen_3080, q_gen_3091, q_gen_3092},
Q_f={q_gen_3078},
Delta=
{
<nil>() -> q_gen_3079
<a>() -> q_gen_3080
<b>() -> q_gen_3080
<nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3091
<b, a>() -> q_gen_3092
<b, b>() -> q_gen_3092
<a, cons, cons>(q_gen_3092, q_gen_3091) -> q_gen_3078
<a, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
<b, cons, cons>(q_gen_3092, q_gen_3091) -> q_gen_3078
<b, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_3076, q_gen_3077},
Q_f={q_gen_3076},
Delta=
{
<s>(q_gen_3077) -> q_gen_3077
<z>() -> q_gen_3077
<s, s>(q_gen_3076) -> q_gen_3076
<z, s>(q_gen_3077) -> q_gen_3076
}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 15
() -> le([z, s(nn2)]) -> 9
() -> length([nil, z]) -> 7
(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 7
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 7
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 7
(le([s(nn1), z])) -> BOT -> 7
(le([z, z])) -> BOT -> 7
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 9
}
Sat witness: Found: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 11, which took 0.015128 s (model generation: 0.013466,  model checking: 0.001662):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3078, q_gen_3079, q_gen_3080, q_gen_3091, q_gen_3092},
Q_f={q_gen_3078},
Delta=
{
<nil>() -> q_gen_3079
<a>() -> q_gen_3080
<b>() -> q_gen_3080
<nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3091
<a, b>() -> q_gen_3092
<b, a>() -> q_gen_3092
<b, b>() -> q_gen_3092
<a, cons, cons>(q_gen_3092, q_gen_3091) -> q_gen_3078
<a, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
<b, cons, cons>(q_gen_3092, q_gen_3091) -> q_gen_3078
<b, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_3076, q_gen_3077},
Q_f={q_gen_3076},
Delta=
{
<s>(q_gen_3077) -> q_gen_3077
<z>() -> q_gen_3077
<s, s>(q_gen_3076) -> q_gen_3076
<z, s>(q_gen_3077) -> q_gen_3076
}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 18
() -> le([z, s(nn2)]) -> 10
() -> length([nil, z]) -> 8
(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 8
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 8
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 8
(le([s(nn1), z])) -> BOT -> 8
(le([z, z])) -> BOT -> 8
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 10
}
Sat witness: Found: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(a, nil)  ;  x -> a
})

-------------------------------------------
Step 12, which took 0.015373 s (model generation: 0.013917,  model checking: 0.001456):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3078, q_gen_3079, q_gen_3080, q_gen_3091, q_gen_3092},
Q_f={q_gen_3078},
Delta=
{
<nil>() -> q_gen_3079
<a>() -> q_gen_3080
<b>() -> q_gen_3080
<nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3091
<a, a>() -> q_gen_3092
<a, b>() -> q_gen_3092
<b, a>() -> q_gen_3092
<b, b>() -> q_gen_3092
<a, cons, cons>(q_gen_3092, q_gen_3091) -> q_gen_3078
<a, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
<b, cons, cons>(q_gen_3092, q_gen_3091) -> q_gen_3078
<b, nil, cons>(q_gen_3080, q_gen_3079) -> q_gen_3078
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_3076, q_gen_3077},
Q_f={q_gen_3076},
Delta=
{
<s>(q_gen_3077) -> q_gen_3077
<z>() -> q_gen_3077
<s, s>(q_gen_3076) -> q_gen_3076
<z, s>(q_gen_3077) -> q_gen_3076
}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 21
() -> le([z, s(nn2)]) -> 11
() -> length([nil, z]) -> 9
(fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 9
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 9
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 9
(le([s(nn1), z])) -> BOT -> 9
(le([z, z])) -> BOT -> 9
(length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 11
}
Sat witness: Found: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(a, cons(b, nil))  ;  x -> a
})

Total time: 0.178850
Reason for stopping: Proved