Solving ../../benchmarks/true/length_fun_le_cons_ab.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:
{
(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.227386 seconds.
Proved
Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359, q_gen_3370, q_gen_3371, q_gen_3372, q_gen_3373},
Q_f={q_gen_3357},
Delta=
{
<cons>(q_gen_3359, q_gen_3358) -> q_gen_3358
<nil>() -> q_gen_3358
<a>() -> q_gen_3359
<b>() -> q_gen_3359
<cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3370
<nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3370
<cons, a>(q_gen_3359, q_gen_3358) -> q_gen_3371
<cons, b>(q_gen_3359, q_gen_3358) -> q_gen_3371
<nil, a>() -> q_gen_3371
<nil, b>() -> q_gen_3371
<a, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<b, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<a, a>() -> q_gen_3373
<a, b>() -> q_gen_3373
<b, a>() -> q_gen_3373
<b, b>() -> q_gen_3373
<a, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<a, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
<b, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<s>(q_gen_3356) -> q_gen_3356
<z>() -> q_gen_3356
<s, s>(q_gen_3355) -> q_gen_3355
<z, s>(q_gen_3356) -> q_gen_3355
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3354, q_gen_3361, q_gen_3376},
Q_f={q_gen_3354},
Delta=
{
<s>(q_gen_3376) -> q_gen_3376
<z>() -> q_gen_3376
<cons, s>(q_gen_3361, q_gen_3354) -> q_gen_3354
<nil, z>() -> q_gen_3354
<a, s>(q_gen_3376) -> q_gen_3361
<a, z>() -> q_gen_3361
<b, s>(q_gen_3376) -> q_gen_3361
<b, z>() -> q_gen_3361
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.003603 s (model generation: 0.003475,  model checking: 0.000128):

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

}

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

}

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

}

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

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

})

-------------------------------------------
Step 1, which took 0.003419 s (model generation: 0.003383,  model checking: 0.000036):

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

}

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

}

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

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

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

-------------------------------------------
Step 2, which took 0.003686 s (model generation: 0.003404,  model checking: 0.000282):

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

}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<z>() -> q_gen_3356
<z, s>(q_gen_3356) -> q_gen_3355
}

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

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

}
--
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: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> nil  ;  x -> b
})

-------------------------------------------
Step 3, which took 0.003747 s (model generation: 0.003659,  model checking: 0.000088):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359},
Q_f={q_gen_3357},
Delta=
{
<nil>() -> q_gen_3358
<b>() -> q_gen_3359
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<z>() -> q_gen_3356
<z, s>(q_gen_3356) -> q_gen_3355
}

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

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

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

-------------------------------------------
Step 4, which took 0.005246 s (model generation: 0.005084,  model checking: 0.000162):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359},
Q_f={q_gen_3357},
Delta=
{
<nil>() -> q_gen_3358
<b>() -> q_gen_3359
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<z>() -> q_gen_3356
<z, s>(q_gen_3356) -> q_gen_3355
}

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

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

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

-------------------------------------------
Step 5, which took 0.006324 s (model generation: 0.005966,  model checking: 0.000358):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359},
Q_f={q_gen_3357},
Delta=
{
<nil>() -> q_gen_3358
<b>() -> q_gen_3359
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<z>() -> q_gen_3356
<s, s>(q_gen_3355) -> q_gen_3355
<z, s>(q_gen_3356) -> q_gen_3355
}

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

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

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

-------------------------------------------
Step 6, which took 0.008742 s (model generation: 0.007953,  model checking: 0.000789):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359},
Q_f={q_gen_3357},
Delta=
{
<nil>() -> q_gen_3358
<b>() -> q_gen_3359
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<s>(q_gen_3356) -> q_gen_3356
<z>() -> q_gen_3356
<s, s>(q_gen_3355) -> q_gen_3355
<z, s>(q_gen_3356) -> q_gen_3355
}

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

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

}
--
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: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> nil  ;  x -> a
})

-------------------------------------------
Step 7, which took 0.009953 s (model generation: 0.009721,  model checking: 0.000232):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359},
Q_f={q_gen_3357},
Delta=
{
<nil>() -> q_gen_3358
<a>() -> q_gen_3359
<b>() -> q_gen_3359
<a, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<s>(q_gen_3356) -> q_gen_3356
<z>() -> q_gen_3356
<s, s>(q_gen_3355) -> q_gen_3355
<z, s>(q_gen_3356) -> q_gen_3355
}

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

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

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

-------------------------------------------
Step 8, which took 0.007519 s (model generation: 0.005941,  model checking: 0.001578):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359},
Q_f={q_gen_3357},
Delta=
{
<nil>() -> q_gen_3358
<a>() -> q_gen_3359
<b>() -> q_gen_3359
<a, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<s>(q_gen_3356) -> q_gen_3356
<z>() -> q_gen_3356
<s, s>(q_gen_3355) -> q_gen_3355
<z, s>(q_gen_3356) -> q_gen_3355
}

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

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

}
--
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: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 9, which took 0.011490 s (model generation: 0.011149,  model checking: 0.000341):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359, q_gen_3370, q_gen_3371, q_gen_3372, q_gen_3373},
Q_f={q_gen_3357},
Delta=
{
<nil>() -> q_gen_3358
<a>() -> q_gen_3359
<b>() -> q_gen_3359
<nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3370
<nil, b>() -> q_gen_3371
<b, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<b, b>() -> q_gen_3373
<a, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
<b, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<s>(q_gen_3356) -> q_gen_3356
<z>() -> q_gen_3356
<s, s>(q_gen_3355) -> q_gen_3355
<z, s>(q_gen_3356) -> q_gen_3355
}

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

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

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

-------------------------------------------
Step 10, which took 0.015236 s (model generation: 0.009950,  model checking: 0.005286):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359, q_gen_3370, q_gen_3371, q_gen_3372, q_gen_3373},
Q_f={q_gen_3357},
Delta=
{
<nil>() -> q_gen_3358
<a>() -> q_gen_3359
<b>() -> q_gen_3359
<nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3370
<nil, b>() -> q_gen_3371
<b, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<b, b>() -> q_gen_3373
<a, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
<b, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<s>(q_gen_3356) -> q_gen_3356
<z>() -> q_gen_3356
<s, s>(q_gen_3355) -> q_gen_3355
<z, s>(q_gen_3356) -> q_gen_3355
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3354, q_gen_3361, q_gen_3376},
Q_f={q_gen_3354},
Delta=
{
<z>() -> q_gen_3376
<cons, s>(q_gen_3361, q_gen_3354) -> q_gen_3354
<nil, z>() -> q_gen_3354
<a, z>() -> q_gen_3361
<b, s>(q_gen_3376) -> q_gen_3361
<b, z>() -> q_gen_3361
}

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

}
--
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]) -> 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)]) -> 10
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(a, nil)  ;  x -> a
})

-------------------------------------------
Step 11, which took 0.015125 s (model generation: 0.013874,  model checking: 0.001251):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359, q_gen_3370, q_gen_3371, q_gen_3372, q_gen_3373},
Q_f={q_gen_3357},
Delta=
{
<nil>() -> q_gen_3358
<a>() -> q_gen_3359
<b>() -> q_gen_3359
<nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3370
<nil, a>() -> q_gen_3371
<nil, b>() -> q_gen_3371
<a, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<b, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<a, a>() -> q_gen_3373
<b, b>() -> q_gen_3373
<a, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<a, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
<b, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<s>(q_gen_3356) -> q_gen_3356
<z>() -> q_gen_3356
<s, s>(q_gen_3355) -> q_gen_3355
<z, s>(q_gen_3356) -> q_gen_3355
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3354, q_gen_3361, q_gen_3376},
Q_f={q_gen_3354},
Delta=
{
<z>() -> q_gen_3376
<cons, s>(q_gen_3361, q_gen_3354) -> q_gen_3354
<nil, z>() -> q_gen_3354
<a, z>() -> q_gen_3361
<b, s>(q_gen_3376) -> q_gen_3361
<b, z>() -> q_gen_3361
}

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

}
--
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)]) -> 9  ;  () -> 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)]) -> 13
}
Sat witness: Yes: ((length([ll, _mp])) -> length([cons(x, ll), s(_mp)]), {
_mp -> s(z)  ;  ll -> cons(b, nil)  ;  x -> a
})

-------------------------------------------
Step 12, which took 0.021310 s (model generation: 0.014429,  model checking: 0.006881):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359, q_gen_3370, q_gen_3371, q_gen_3372, q_gen_3373},
Q_f={q_gen_3357},
Delta=
{
<nil>() -> q_gen_3358
<a>() -> q_gen_3359
<b>() -> q_gen_3359
<nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3370
<nil, a>() -> q_gen_3371
<nil, b>() -> q_gen_3371
<a, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<b, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<a, a>() -> q_gen_3373
<b, b>() -> q_gen_3373
<a, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<a, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
<b, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<s>(q_gen_3356) -> q_gen_3356
<z>() -> q_gen_3356
<s, s>(q_gen_3355) -> q_gen_3355
<z, s>(q_gen_3356) -> q_gen_3355
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3354, q_gen_3361, q_gen_3376},
Q_f={q_gen_3354},
Delta=
{
<z>() -> q_gen_3376
<cons, s>(q_gen_3361, q_gen_3354) -> q_gen_3354
<nil, z>() -> q_gen_3354
<a, s>(q_gen_3376) -> q_gen_3361
<a, z>() -> q_gen_3361
<b, s>(q_gen_3376) -> q_gen_3361
<b, z>() -> q_gen_3361
}

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

}
--
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)]) -> 10  ;  () -> 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)]) -> 13
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 13, which took 0.017146 s (model generation: 0.015273,  model checking: 0.001873):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359, q_gen_3370, q_gen_3371, q_gen_3372, q_gen_3373},
Q_f={q_gen_3357},
Delta=
{
<nil>() -> q_gen_3358
<a>() -> q_gen_3359
<b>() -> q_gen_3359
<nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3370
<nil, a>() -> q_gen_3371
<nil, b>() -> q_gen_3371
<a, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<b, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<a, a>() -> q_gen_3373
<a, b>() -> q_gen_3373
<b, b>() -> q_gen_3373
<a, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<a, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
<b, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<s>(q_gen_3356) -> q_gen_3356
<z>() -> q_gen_3356
<s, s>(q_gen_3355) -> q_gen_3355
<z, s>(q_gen_3356) -> q_gen_3355
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3354, q_gen_3361, q_gen_3376},
Q_f={q_gen_3354},
Delta=
{
<z>() -> q_gen_3376
<cons, s>(q_gen_3361, q_gen_3354) -> q_gen_3354
<nil, z>() -> q_gen_3354
<a, s>(q_gen_3376) -> q_gen_3361
<a, z>() -> q_gen_3361
<b, s>(q_gen_3376) -> q_gen_3361
<b, z>() -> q_gen_3361
}

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

}
--
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)]) -> 11  ;  () -> length([nil, z]) -> 10  ;  (fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 10  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 10  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 10  ;  (le([s(nn1), z])) -> BOT -> 10  ;  (le([z, z])) -> BOT -> 10  ;  (length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 16
}
Sat witness: Yes: ((length([ll, _mp])) -> length([cons(x, ll), s(_mp)]), {
_mp -> s(s(z))  ;  ll -> cons(b, cons(b, nil))  ;  x -> b
})

-------------------------------------------
Step 14, which took 0.024972 s (model generation: 0.016734,  model checking: 0.008238):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359, q_gen_3370, q_gen_3371, q_gen_3372, q_gen_3373},
Q_f={q_gen_3357},
Delta=
{
<nil>() -> q_gen_3358
<a>() -> q_gen_3359
<b>() -> q_gen_3359
<nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3370
<nil, a>() -> q_gen_3371
<nil, b>() -> q_gen_3371
<a, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<b, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<a, a>() -> q_gen_3373
<a, b>() -> q_gen_3373
<b, b>() -> q_gen_3373
<a, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<a, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
<b, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<s>(q_gen_3356) -> q_gen_3356
<z>() -> q_gen_3356
<s, s>(q_gen_3355) -> q_gen_3355
<z, s>(q_gen_3356) -> q_gen_3355
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3354, q_gen_3361, q_gen_3376},
Q_f={q_gen_3354},
Delta=
{
<s>(q_gen_3376) -> q_gen_3376
<z>() -> q_gen_3376
<cons, s>(q_gen_3361, q_gen_3354) -> q_gen_3354
<nil, z>() -> q_gen_3354
<a, s>(q_gen_3376) -> q_gen_3361
<a, z>() -> q_gen_3361
<b, s>(q_gen_3376) -> q_gen_3361
<b, z>() -> q_gen_3361
}

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

}
--
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)]) -> 12  ;  () -> length([nil, z]) -> 11  ;  (fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 11  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 11  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 11  ;  (le([s(nn1), z])) -> BOT -> 11  ;  (le([z, z])) -> BOT -> 11  ;  (length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 16
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(b, nil)  ;  x -> a
})

-------------------------------------------
Step 15, which took 0.027433 s (model generation: 0.013734,  model checking: 0.013699):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359, q_gen_3370, q_gen_3371, q_gen_3372, q_gen_3373},
Q_f={q_gen_3357},
Delta=
{
<nil>() -> q_gen_3358
<a>() -> q_gen_3359
<b>() -> q_gen_3359
<nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3370
<nil, a>() -> q_gen_3371
<nil, b>() -> q_gen_3371
<a, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<b, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<a, a>() -> q_gen_3373
<a, b>() -> q_gen_3373
<b, a>() -> q_gen_3373
<b, b>() -> q_gen_3373
<a, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<a, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
<b, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<s>(q_gen_3356) -> q_gen_3356
<z>() -> q_gen_3356
<s, s>(q_gen_3355) -> q_gen_3355
<z, s>(q_gen_3356) -> q_gen_3355
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3354, q_gen_3361, q_gen_3376},
Q_f={q_gen_3354},
Delta=
{
<s>(q_gen_3376) -> q_gen_3376
<z>() -> q_gen_3376
<cons, s>(q_gen_3361, q_gen_3354) -> q_gen_3354
<nil, z>() -> q_gen_3354
<a, s>(q_gen_3376) -> q_gen_3361
<a, z>() -> q_gen_3361
<b, s>(q_gen_3376) -> q_gen_3361
<b, z>() -> q_gen_3361
}

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

}
--
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)]) -> 13  ;  () -> length([nil, z]) -> 12  ;  (fcons([x, l, _vp]) /\ length([_vp, _wp]) /\ length([l, _up])) -> le([_up, _wp]) -> 12  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 12  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 12  ;  (le([s(nn1), z])) -> BOT -> 12  ;  (le([z, z])) -> BOT -> 12  ;  (length([ll, _mp])) -> length([cons(x, ll), s(_mp)]) -> 17
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(b, cons(b, nil))  ;  x -> a
})

-------------------------------------------
Step 16, which took 0.020541 s (model generation: 0.013070,  model checking: 0.007471):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3357, q_gen_3358, q_gen_3359, q_gen_3370, q_gen_3371, q_gen_3372, q_gen_3373},
Q_f={q_gen_3357},
Delta=
{
<cons>(q_gen_3359, q_gen_3358) -> q_gen_3358
<nil>() -> q_gen_3358
<a>() -> q_gen_3359
<b>() -> q_gen_3359
<cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3370
<nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3370
<cons, a>(q_gen_3359, q_gen_3358) -> q_gen_3371
<nil, a>() -> q_gen_3371
<nil, b>() -> q_gen_3371
<a, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<b, cons>(q_gen_3359, q_gen_3358) -> q_gen_3372
<a, a>() -> q_gen_3373
<a, b>() -> q_gen_3373
<b, a>() -> q_gen_3373
<b, b>() -> q_gen_3373
<a, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<a, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
<b, cons, cons>(q_gen_3373, q_gen_3372, q_gen_3371, q_gen_3370) -> q_gen_3357
<b, nil, cons>(q_gen_3359, q_gen_3358) -> q_gen_3357
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3355, q_gen_3356},
Q_f={q_gen_3355},
Delta=
{
<s>(q_gen_3356) -> q_gen_3356
<z>() -> q_gen_3356
<s, s>(q_gen_3355) -> q_gen_3355
<z, s>(q_gen_3356) -> q_gen_3355
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3354, q_gen_3361, q_gen_3376},
Q_f={q_gen_3354},
Delta=
{
<s>(q_gen_3376) -> q_gen_3376
<z>() -> q_gen_3376
<cons, s>(q_gen_3361, q_gen_3354) -> q_gen_3354
<nil, z>() -> q_gen_3354
<a, s>(q_gen_3376) -> q_gen_3361
<a, z>() -> q_gen_3361
<b, s>(q_gen_3376) -> q_gen_3361
<b, z>() -> q_gen_3361
}

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

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

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

Total time: 0.227386
Reason for stopping: Proved