Inference procedure has parameters:
Ice fuel: 200
Timeout: 60s
Convolution: left


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, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)])}
(take([_sh, _th, _uh]) /\ take([_sh, _th, _vh])) -> eq_eltlist([_uh, _vh])
)
}

properties:
{(take([z, xs, _wh])) -> eq_eltlist([_wh, 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, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]) -> 0
(take([z, xs, _wh])) -> eq_eltlist([_wh, nil]) -> 0
}


Solving took 0.152189 seconds.
Proved
Model:
|_
{
take -> 
{{{
Q={q_gen_2070, q_gen_2072, q_gen_2074, q_gen_2075, q_gen_2077, q_gen_2078, q_gen_2095},
Q_f={q_gen_2070},
Delta=
{
<s>(q_gen_2072) -> q_gen_2072
<z>() -> q_gen_2072
<cons>(q_gen_2078, q_gen_2077) -> q_gen_2077
<nil>() -> q_gen_2077
<a>() -> q_gen_2078
<b>() -> q_gen_2078
<cons, cons>(q_gen_2095, q_gen_2074) -> q_gen_2074
<cons, nil>(q_gen_2078, q_gen_2077) -> q_gen_2074
<nil, nil>() -> q_gen_2074
<a, a>() -> q_gen_2095
<b, b>() -> q_gen_2095
<s, cons, cons>(q_gen_2075, q_gen_2074) -> q_gen_2070
<s, nil, nil>(q_gen_2072) -> q_gen_2070
<z, cons, nil>(q_gen_2078, q_gen_2077) -> q_gen_2070
<z, nil, nil>() -> q_gen_2070
<s, a, a>(q_gen_2072) -> q_gen_2075
<s, b, b>(q_gen_2072) -> q_gen_2075
<z, a, a>() -> q_gen_2075
<z, b, b>() -> q_gen_2075
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.008242 s (model generation: 0.007416,  model checking: 0.000826):

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

}

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

}
--
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, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]) -> 1
(take([z, xs, _wh])) -> eq_eltlist([_wh, nil]) -> 1
}
Sat witness: Found: (() -> take([z, y, nil]), {
y -> nil
})

-------------------------------------------
Step 1, which took 0.009121 s (model generation: 0.008907,  model checking: 0.000214):

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

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

}
--
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, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]) -> 1
(take([z, xs, _wh])) -> eq_eltlist([_wh, nil]) -> 1
}
Sat witness: Found: (() -> take([s(u), nil, nil]), {
u -> z
})

-------------------------------------------
Step 2, which took 0.007848 s (model generation: 0.007552,  model checking: 0.000296):

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

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

}
--
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, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]) -> 4
(take([z, xs, _wh])) -> eq_eltlist([_wh, nil]) -> 2
}
Sat witness: Found: ((take([u, x3, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]), {
_rh -> nil  ;  u -> z  ;  x2 -> b  ;  x3 -> nil
})

-------------------------------------------
Step 3, which took 0.009668 s (model generation: 0.008629,  model checking: 0.001039):

Model:
|_
{
take -> 
{{{
Q={q_gen_2070, q_gen_2072, q_gen_2074, q_gen_2075},
Q_f={q_gen_2070},
Delta=
{
<z>() -> q_gen_2072
<nil, nil>() -> q_gen_2074
<s, cons, cons>(q_gen_2075, q_gen_2074) -> q_gen_2070
<s, nil, nil>(q_gen_2072) -> q_gen_2070
<z, nil, nil>() -> q_gen_2070
<z, b, b>() -> q_gen_2075
}

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

}
--
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, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]) -> 4
(take([z, xs, _wh])) -> eq_eltlist([_wh, nil]) -> 3
}
Sat witness: Found: (() -> take([z, y, nil]), {
y -> cons(b, nil)
})

-------------------------------------------
Step 4, which took 0.010539 s (model generation: 0.010100,  model checking: 0.000439):

Model:
|_
{
take -> 
{{{
Q={q_gen_2070, q_gen_2072, q_gen_2074, q_gen_2075, q_gen_2077, q_gen_2078},
Q_f={q_gen_2070},
Delta=
{
<z>() -> q_gen_2072
<nil>() -> q_gen_2077
<b>() -> q_gen_2078
<nil, nil>() -> q_gen_2074
<s, cons, cons>(q_gen_2075, q_gen_2074) -> q_gen_2070
<s, nil, nil>(q_gen_2072) -> q_gen_2070
<z, cons, nil>(q_gen_2078, q_gen_2077) -> q_gen_2070
<z, nil, nil>() -> q_gen_2070
<z, b, b>() -> q_gen_2075
}

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

}
--
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, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]) -> 4
(take([z, xs, _wh])) -> eq_eltlist([_wh, nil]) -> 4
}
Sat witness: Found: (() -> take([s(u), nil, nil]), {
u -> s(z)
})

-------------------------------------------
Step 5, which took 0.009441 s (model generation: 0.008364,  model checking: 0.001077):

Model:
|_
{
take -> 
{{{
Q={q_gen_2070, q_gen_2072, q_gen_2074, q_gen_2075, q_gen_2077, q_gen_2078},
Q_f={q_gen_2070},
Delta=
{
<s>(q_gen_2072) -> q_gen_2072
<z>() -> q_gen_2072
<nil>() -> q_gen_2077
<b>() -> q_gen_2078
<nil, nil>() -> q_gen_2074
<s, cons, cons>(q_gen_2075, q_gen_2074) -> q_gen_2070
<s, nil, nil>(q_gen_2072) -> q_gen_2070
<z, cons, nil>(q_gen_2078, q_gen_2077) -> q_gen_2070
<z, nil, nil>() -> q_gen_2070
<z, b, b>() -> q_gen_2075
}

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

}
--
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, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]) -> 7
(take([z, xs, _wh])) -> eq_eltlist([_wh, nil]) -> 5
}
Sat witness: Found: ((take([u, x3, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]), {
_rh -> nil  ;  u -> z  ;  x2 -> a  ;  x3 -> nil
})

-------------------------------------------
Step 6, which took 0.009395 s (model generation: 0.008990,  model checking: 0.000405):

Model:
|_
{
take -> 
{{{
Q={q_gen_2070, q_gen_2072, q_gen_2074, q_gen_2075, q_gen_2077, q_gen_2078},
Q_f={q_gen_2070},
Delta=
{
<s>(q_gen_2072) -> q_gen_2072
<z>() -> q_gen_2072
<nil>() -> q_gen_2077
<b>() -> q_gen_2078
<nil, nil>() -> q_gen_2074
<s, cons, cons>(q_gen_2075, q_gen_2074) -> q_gen_2070
<s, nil, nil>(q_gen_2072) -> q_gen_2070
<z, cons, nil>(q_gen_2078, q_gen_2077) -> q_gen_2070
<z, nil, nil>() -> q_gen_2070
<z, a, a>() -> q_gen_2075
<z, b, b>() -> q_gen_2075
}

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

}
--
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, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]) -> 7
(take([z, xs, _wh])) -> eq_eltlist([_wh, nil]) -> 6
}
Sat witness: Found: (() -> take([z, y, nil]), {
y -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 7, which took 0.010825 s (model generation: 0.010023,  model checking: 0.000802):

Model:
|_
{
take -> 
{{{
Q={q_gen_2070, q_gen_2072, q_gen_2074, q_gen_2075, q_gen_2077, q_gen_2078},
Q_f={q_gen_2070},
Delta=
{
<s>(q_gen_2072) -> q_gen_2072
<z>() -> q_gen_2072
<cons>(q_gen_2078, q_gen_2077) -> q_gen_2077
<nil>() -> q_gen_2077
<a>() -> q_gen_2078
<b>() -> q_gen_2078
<nil, nil>() -> q_gen_2074
<s, cons, cons>(q_gen_2075, q_gen_2074) -> q_gen_2070
<s, nil, nil>(q_gen_2072) -> q_gen_2070
<z, cons, nil>(q_gen_2078, q_gen_2077) -> q_gen_2070
<z, nil, nil>() -> q_gen_2070
<z, a, a>() -> q_gen_2075
<z, b, b>() -> q_gen_2075
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 7
() -> take([z, y, nil]) -> 9
(take([u, x3, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]) -> 10
(take([z, xs, _wh])) -> eq_eltlist([_wh, nil]) -> 7
}
Sat witness: Found: ((take([u, x3, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]), {
_rh -> nil  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> nil
})

-------------------------------------------
Step 8, which took 0.011808 s (model generation: 0.010730,  model checking: 0.001078):

Model:
|_
{
take -> 
{{{
Q={q_gen_2070, q_gen_2072, q_gen_2074, q_gen_2075, q_gen_2077, q_gen_2078},
Q_f={q_gen_2070},
Delta=
{
<s>(q_gen_2072) -> q_gen_2072
<z>() -> q_gen_2072
<cons>(q_gen_2078, q_gen_2077) -> q_gen_2077
<nil>() -> q_gen_2077
<a>() -> q_gen_2078
<b>() -> q_gen_2078
<nil, nil>() -> q_gen_2074
<s, cons, cons>(q_gen_2075, q_gen_2074) -> q_gen_2070
<s, nil, nil>(q_gen_2072) -> q_gen_2070
<z, cons, nil>(q_gen_2078, q_gen_2077) -> q_gen_2070
<z, nil, nil>() -> q_gen_2070
<s, b, b>(q_gen_2072) -> q_gen_2075
<z, a, a>() -> q_gen_2075
<z, b, b>() -> q_gen_2075
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 8
() -> take([z, y, nil]) -> 10
(take([u, x3, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]) -> 13
(take([z, xs, _wh])) -> eq_eltlist([_wh, nil]) -> 8
}
Sat witness: Found: ((take([u, x3, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]), {
_rh -> nil  ;  u -> s(z)  ;  x2 -> a  ;  x3 -> nil
})

-------------------------------------------
Step 9, which took 0.013235 s (model generation: 0.012189,  model checking: 0.001046):

Model:
|_
{
take -> 
{{{
Q={q_gen_2070, q_gen_2072, q_gen_2074, q_gen_2075, q_gen_2077, q_gen_2078},
Q_f={q_gen_2070},
Delta=
{
<s>(q_gen_2072) -> q_gen_2072
<z>() -> q_gen_2072
<cons>(q_gen_2078, q_gen_2077) -> q_gen_2077
<nil>() -> q_gen_2077
<a>() -> q_gen_2078
<b>() -> q_gen_2078
<nil, nil>() -> q_gen_2074
<s, cons, cons>(q_gen_2075, q_gen_2074) -> q_gen_2070
<s, nil, nil>(q_gen_2072) -> q_gen_2070
<z, cons, nil>(q_gen_2078, q_gen_2077) -> q_gen_2070
<z, nil, nil>() -> q_gen_2070
<s, a, a>(q_gen_2072) -> q_gen_2075
<s, b, b>(q_gen_2072) -> q_gen_2075
<z, a, a>() -> q_gen_2075
<z, b, b>() -> q_gen_2075
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 9
() -> take([z, y, nil]) -> 11
(take([u, x3, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]) -> 16
(take([z, xs, _wh])) -> eq_eltlist([_wh, nil]) -> 9
}
Sat witness: Found: ((take([u, x3, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]), {
_rh -> nil  ;  u -> z  ;  x2 -> b  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 10, which took 0.017137 s (model generation: 0.015452,  model checking: 0.001685):

Model:
|_
{
take -> 
{{{
Q={q_gen_2070, q_gen_2072, q_gen_2074, q_gen_2075, q_gen_2077, q_gen_2078},
Q_f={q_gen_2070},
Delta=
{
<s>(q_gen_2072) -> q_gen_2072
<z>() -> q_gen_2072
<cons>(q_gen_2078, q_gen_2077) -> q_gen_2077
<nil>() -> q_gen_2077
<a>() -> q_gen_2078
<b>() -> q_gen_2078
<cons, nil>(q_gen_2078, q_gen_2077) -> q_gen_2074
<nil, nil>() -> q_gen_2074
<s, cons, cons>(q_gen_2075, q_gen_2074) -> q_gen_2070
<s, nil, nil>(q_gen_2072) -> q_gen_2070
<z, cons, nil>(q_gen_2078, q_gen_2077) -> q_gen_2070
<z, nil, nil>() -> q_gen_2070
<s, a, a>(q_gen_2072) -> q_gen_2075
<s, b, b>(q_gen_2072) -> q_gen_2075
<z, a, a>() -> q_gen_2075
<z, b, b>() -> q_gen_2075
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 10
() -> take([z, y, nil]) -> 12
(take([u, x3, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]) -> 19
(take([z, xs, _wh])) -> eq_eltlist([_wh, nil]) -> 10
}
Sat witness: Found: ((take([u, x3, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]), {
_rh -> cons(a, nil)  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 11, which took 0.017215 s (model generation: 0.014893,  model checking: 0.002322):

Model:
|_
{
take -> 
{{{
Q={q_gen_2070, q_gen_2072, q_gen_2074, q_gen_2075, q_gen_2077, q_gen_2078, q_gen_2095},
Q_f={q_gen_2070},
Delta=
{
<s>(q_gen_2072) -> q_gen_2072
<z>() -> q_gen_2072
<cons>(q_gen_2078, q_gen_2077) -> q_gen_2077
<nil>() -> q_gen_2077
<a>() -> q_gen_2078
<b>() -> q_gen_2078
<cons, cons>(q_gen_2095, q_gen_2074) -> q_gen_2074
<cons, nil>(q_gen_2078, q_gen_2077) -> q_gen_2074
<nil, nil>() -> q_gen_2074
<a, a>() -> q_gen_2095
<s, cons, cons>(q_gen_2075, q_gen_2074) -> q_gen_2070
<s, nil, nil>(q_gen_2072) -> q_gen_2070
<z, cons, nil>(q_gen_2078, q_gen_2077) -> q_gen_2070
<z, nil, nil>() -> q_gen_2070
<s, a, a>(q_gen_2072) -> q_gen_2075
<s, b, b>(q_gen_2072) -> q_gen_2075
<z, a, a>() -> q_gen_2075
<z, b, b>() -> q_gen_2075
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 11
() -> take([z, y, nil]) -> 13
(take([u, x3, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]) -> 22
(take([z, xs, _wh])) -> eq_eltlist([_wh, nil]) -> 11
}
Sat witness: Found: ((take([u, x3, _rh])) -> take([s(u), cons(x2, x3), cons(x2, _rh)]), {
_rh -> cons(b, nil)  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(b, nil)
})

Total time: 0.152189
Reason for stopping: Proved