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, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)])}
(take([_dd, _ed, _fd]) /\ take([_dd, _ed, _gd])) -> eq_eltlist([_fd, _gd])
)
}

properties:
{(take([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)])}


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

Clause system for inference is:

{
() -> take([s(u), nil, nil]) -> 0
() -> take([z, y, nil]) -> 0
(take([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 0
(take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 0
}


Solving took 0.093615 seconds.
Proved
Model:
|_
{
take -> 
{{{
Q={q_gen_743, q_gen_745, q_gen_747, q_gen_749, q_gen_750},
Q_f={q_gen_743},
Delta=
{
<s>(q_gen_745) -> q_gen_745
<z>() -> q_gen_745
<cons>(q_gen_750, q_gen_749) -> q_gen_749
<nil>() -> q_gen_749
<a>() -> q_gen_750
<b>() -> q_gen_750
<a, a>() -> q_gen_747
<b, b>() -> q_gen_747
<s, cons, cons>(q_gen_747, q_gen_743) -> q_gen_743
<s, nil, nil>(q_gen_745) -> q_gen_743
<z, cons, nil>(q_gen_750, q_gen_749) -> q_gen_743
<z, nil, nil>() -> q_gen_743
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005570 s (model generation: 0.005264,  model checking: 0.000306):

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([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 1
(take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 1
}
Sat witness: Found: (() -> take([z, y, nil]), {
y -> nil
})

-------------------------------------------
Step 1, which took 0.004457 s (model generation: 0.004125,  model checking: 0.000332):

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

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([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 1
(take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 1
}
Sat witness: Found: (() -> take([s(u), nil, nil]), {
u -> z
})

-------------------------------------------
Step 2, which took 0.006911 s (model generation: 0.004801,  model checking: 0.002110):

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

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([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 1
(take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 4
}
Sat witness: Found: ((take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]), {
_cd -> nil  ;  u -> z  ;  x2 -> b  ;  x3 -> nil
})

-------------------------------------------
Step 3, which took 0.013166 s (model generation: 0.010859,  model checking: 0.002307):

Model:
|_
{
take -> 
{{{
Q={q_gen_743, q_gen_745, q_gen_747},
Q_f={q_gen_743},
Delta=
{
<z>() -> q_gen_745
<b, b>() -> q_gen_747
<s, cons, cons>(q_gen_747, q_gen_743) -> q_gen_743
<s, nil, nil>(q_gen_745) -> q_gen_743
<z, nil, nil>() -> q_gen_743
}

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([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 2
(take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 4
}
Sat witness: Found: (() -> take([z, y, nil]), {
y -> cons(b, nil)
})

-------------------------------------------
Step 4, which took 0.014202 s (model generation: 0.011280,  model checking: 0.002922):

Model:
|_
{
take -> 
{{{
Q={q_gen_743, q_gen_745, q_gen_747, q_gen_749, q_gen_750},
Q_f={q_gen_743},
Delta=
{
<z>() -> q_gen_745
<nil>() -> q_gen_749
<b>() -> q_gen_750
<b, b>() -> q_gen_747
<s, cons, cons>(q_gen_747, q_gen_743) -> q_gen_743
<s, nil, nil>(q_gen_745) -> q_gen_743
<z, cons, nil>(q_gen_750, q_gen_749) -> q_gen_743
<z, nil, nil>() -> q_gen_743
}

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([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 3
(take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 4
}
Sat witness: Found: (() -> take([s(u), nil, nil]), {
u -> s(z)
})

-------------------------------------------
Step 5, which took 0.014687 s (model generation: 0.011598,  model checking: 0.003089):

Model:
|_
{
take -> 
{{{
Q={q_gen_743, q_gen_745, q_gen_747, q_gen_749, q_gen_750},
Q_f={q_gen_743},
Delta=
{
<s>(q_gen_745) -> q_gen_745
<z>() -> q_gen_745
<nil>() -> q_gen_749
<b>() -> q_gen_750
<b, b>() -> q_gen_747
<s, cons, cons>(q_gen_747, q_gen_743) -> q_gen_743
<s, nil, nil>(q_gen_745) -> q_gen_743
<z, cons, nil>(q_gen_750, q_gen_749) -> q_gen_743
<z, nil, nil>() -> q_gen_743
}

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([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 4
(take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 7
}
Sat witness: Found: ((take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]), {
_cd -> nil  ;  u -> z  ;  x2 -> a  ;  x3 -> nil
})

-------------------------------------------
Step 6, which took 0.015756 s (model generation: 0.012086,  model checking: 0.003670):

Model:
|_
{
take -> 
{{{
Q={q_gen_743, q_gen_745, q_gen_747, q_gen_749, q_gen_750},
Q_f={q_gen_743},
Delta=
{
<s>(q_gen_745) -> q_gen_745
<z>() -> q_gen_745
<nil>() -> q_gen_749
<b>() -> q_gen_750
<a, a>() -> q_gen_747
<b, b>() -> q_gen_747
<s, cons, cons>(q_gen_747, q_gen_743) -> q_gen_743
<s, nil, nil>(q_gen_745) -> q_gen_743
<z, cons, nil>(q_gen_750, q_gen_749) -> q_gen_743
<z, nil, nil>() -> q_gen_743
}

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([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 5
(take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 7
}
Sat witness: Found: (() -> take([z, y, nil]), {
y -> cons(a, cons(a, nil))
})

Total time: 0.093615
Reason for stopping: Proved