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:
{
(take, F:
{() -> take([s(u), nil, nil])
() -> take([z, y, nil])
(take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)])}
(take([_pu, _qu, _ru]) /\ take([_pu, _qu, _su])) -> eq_eltlist([_ru, _su])
)
}

properties:
{(take([z, xs, _tu])) -> eq_eltlist([_tu, nil])}


over-approximation: {take}
under-approximation: {}

Clause system for inference is:

{
() -> take([s(u), nil, nil]) -> 0
() -> take([z, y, nil]) -> 0
(take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 0
(take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 0
}


Solving took 0.097096 seconds.
Proved
Model:
|_
{
take -> 
{{{
Q={q_gen_3946, q_gen_3948, q_gen_3950, q_gen_3952, q_gen_3953},
Q_f={q_gen_3946},
Delta=
{
<s>(q_gen_3948) -> q_gen_3948
<z>() -> q_gen_3948
<cons>(q_gen_3953, q_gen_3952) -> q_gen_3952
<nil>() -> q_gen_3952
<a>() -> q_gen_3953
<b>() -> q_gen_3953
<a, a>() -> q_gen_3950
<b, b>() -> q_gen_3950
<s, cons, cons>(q_gen_3950, q_gen_3946) -> q_gen_3946
<s, nil, nil>(q_gen_3948) -> q_gen_3946
<z, cons, nil>(q_gen_3953, q_gen_3952) -> q_gen_3946
<z, nil, nil>() -> q_gen_3946
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.011809 s (model generation: 0.009925,  model checking: 0.001884):

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

}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 0
() -> take([z, y, nil]) -> 3
(take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 1
(take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 1
}
Sat witness: Found: (() -> take([z, y, nil]), {
y -> nil
})

-------------------------------------------
Step 1, which took 0.010595 s (model generation: 0.010157,  model checking: 0.000438):

Model:
|_
{
take -> 
{{{
Q={q_gen_3946},
Q_f={q_gen_3946},
Delta=
{
<z, nil, nil>() -> q_gen_3946
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 3
() -> take([z, y, nil]) -> 3
(take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 1
(take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 1
}
Sat witness: Found: (() -> take([s(u), nil, nil]), {
u -> z
})

-------------------------------------------
Step 2, which took 0.011505 s (model generation: 0.010936,  model checking: 0.000569):

Model:
|_
{
take -> 
{{{
Q={q_gen_3946, q_gen_3948},
Q_f={q_gen_3946},
Delta=
{
<z>() -> q_gen_3948
<s, nil, nil>(q_gen_3948) -> q_gen_3946
<z, nil, nil>() -> q_gen_3946
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 3
() -> take([z, y, nil]) -> 3
(take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 4
(take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 2
}
Sat witness: Found: ((take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]), {
_ou -> nil  ;  u -> z  ;  x2 -> b  ;  x3 -> nil
})

-------------------------------------------
Step 3, which took 0.012148 s (model generation: 0.010951,  model checking: 0.001197):

Model:
|_
{
take -> 
{{{
Q={q_gen_3946, q_gen_3948, q_gen_3950},
Q_f={q_gen_3946},
Delta=
{
<z>() -> q_gen_3948
<b, b>() -> q_gen_3950
<s, cons, cons>(q_gen_3950, q_gen_3946) -> q_gen_3946
<s, nil, nil>(q_gen_3948) -> q_gen_3946
<z, nil, nil>() -> q_gen_3946
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 3
() -> take([z, y, nil]) -> 6
(take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 4
(take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 3
}
Sat witness: Found: (() -> take([z, y, nil]), {
y -> cons(b, nil)
})

-------------------------------------------
Step 4, which took 0.011801 s (model generation: 0.011105,  model checking: 0.000696):

Model:
|_
{
take -> 
{{{
Q={q_gen_3946, q_gen_3948, q_gen_3950, q_gen_3952, q_gen_3953},
Q_f={q_gen_3946},
Delta=
{
<z>() -> q_gen_3948
<nil>() -> q_gen_3952
<b>() -> q_gen_3953
<b, b>() -> q_gen_3950
<s, cons, cons>(q_gen_3950, q_gen_3946) -> q_gen_3946
<s, nil, nil>(q_gen_3948) -> q_gen_3946
<z, cons, nil>(q_gen_3953, q_gen_3952) -> q_gen_3946
<z, nil, nil>() -> q_gen_3946
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 6
() -> take([z, y, nil]) -> 6
(take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 4
(take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 4
}
Sat witness: Found: (() -> take([s(u), nil, nil]), {
u -> s(z)
})

-------------------------------------------
Step 5, which took 0.012938 s (model generation: 0.011636,  model checking: 0.001302):

Model:
|_
{
take -> 
{{{
Q={q_gen_3946, q_gen_3948, q_gen_3950, q_gen_3952, q_gen_3953},
Q_f={q_gen_3946},
Delta=
{
<s>(q_gen_3948) -> q_gen_3948
<z>() -> q_gen_3948
<nil>() -> q_gen_3952
<b>() -> q_gen_3953
<b, b>() -> q_gen_3950
<s, cons, cons>(q_gen_3950, q_gen_3946) -> q_gen_3946
<s, nil, nil>(q_gen_3948) -> q_gen_3946
<z, cons, nil>(q_gen_3953, q_gen_3952) -> q_gen_3946
<z, nil, nil>() -> q_gen_3946
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 6
() -> take([z, y, nil]) -> 6
(take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 7
(take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 5
}
Sat witness: Found: ((take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]), {
_ou -> nil  ;  u -> z  ;  x2 -> a  ;  x3 -> nil
})

-------------------------------------------
Step 6, which took 0.012708 s (model generation: 0.011993,  model checking: 0.000715):

Model:
|_
{
take -> 
{{{
Q={q_gen_3946, q_gen_3948, q_gen_3950, q_gen_3952, q_gen_3953},
Q_f={q_gen_3946},
Delta=
{
<s>(q_gen_3948) -> q_gen_3948
<z>() -> q_gen_3948
<nil>() -> q_gen_3952
<b>() -> q_gen_3953
<a, a>() -> q_gen_3950
<b, b>() -> q_gen_3950
<s, cons, cons>(q_gen_3950, q_gen_3946) -> q_gen_3946
<s, nil, nil>(q_gen_3948) -> q_gen_3946
<z, cons, nil>(q_gen_3953, q_gen_3952) -> q_gen_3946
<z, nil, nil>() -> q_gen_3946
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 6
() -> take([z, y, nil]) -> 9
(take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 7
(take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 6
}
Sat witness: Found: (() -> take([z, y, nil]), {
y -> cons(a, cons(a, nil))
})

Total time: 0.097096
Reason for stopping: Proved