Solving ../../benchmarks/true/isaplanner_prop42.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:
{
(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 1.526829 seconds.
Proved
Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057, q_gen_2082, q_gen_2083},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<cons>(q_gen_2057, q_gen_2056) -> q_gen_2056
<nil>() -> q_gen_2056
<a>() -> q_gen_2057
<b>() -> q_gen_2057
<s, cons>(q_gen_2083, q_gen_2082) -> q_gen_2082
<s, nil>(q_gen_2050) -> q_gen_2082
<z, cons>(q_gen_2057, q_gen_2056) -> q_gen_2082
<z, nil>() -> q_gen_2082
<s, a>(q_gen_2050) -> q_gen_2083
<s, b>(q_gen_2050) -> q_gen_2083
<z, a>() -> q_gen_2083
<z, b>() -> q_gen_2083
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<s, cons, a>(q_gen_2083, q_gen_2082) -> q_gen_2052
<s, cons, b>(q_gen_2083, q_gen_2082) -> q_gen_2052
<s, nil, a>(q_gen_2050) -> q_gen_2052
<s, nil, b>(q_gen_2050) -> q_gen_2052
<z, cons, a>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, cons, b>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, nil, a>() -> q_gen_2052
<z, nil, b>() -> q_gen_2052
<s, a, cons>(q_gen_2083, q_gen_2082) -> q_gen_2053
<s, a, nil>(q_gen_2050) -> q_gen_2053
<s, b, cons>(q_gen_2083, q_gen_2082) -> q_gen_2053
<s, b, nil>(q_gen_2050) -> q_gen_2053
<z, a, nil>() -> q_gen_2053
<z, b, nil>() -> q_gen_2053
<s, a, a>(q_gen_2050) -> q_gen_2054
<s, b, b>(q_gen_2050) -> q_gen_2054
<z, a, a>() -> q_gen_2054
<z, b, b>() -> q_gen_2054
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004274 s (model generation: 0.003637,  model checking: 0.000637):

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

}

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

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

-------------------------------------------
Step 1, which took 0.003612 s (model generation: 0.003409,  model checking: 0.000203):

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

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

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

-------------------------------------------
Step 2, which took 0.004049 s (model generation: 0.003463,  model checking: 0.000586):

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

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

}
--
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: Yes: ((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.004118 s (model generation: 0.003537,  model checking: 0.000581):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054},
Q_f={q_gen_2048},
Delta=
{
<z>() -> q_gen_2050
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<z, nil, b>() -> q_gen_2052
<z, b, nil>() -> q_gen_2053
<z, b, b>() -> q_gen_2054
}

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

}
--
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: Yes: (() -> take([z, y, nil]), {
y -> cons(b, nil)
})

-------------------------------------------
Step 4, which took 0.005593 s (model generation: 0.004308,  model checking: 0.001285):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057},
Q_f={q_gen_2048},
Delta=
{
<z>() -> q_gen_2050
<nil>() -> q_gen_2056
<b>() -> q_gen_2057
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<z, nil, b>() -> q_gen_2052
<z, b, nil>() -> q_gen_2053
<z, b, b>() -> q_gen_2054
}

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

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

-------------------------------------------
Step 5, which took 0.009018 s (model generation: 0.006042,  model checking: 0.002976):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<nil>() -> q_gen_2056
<b>() -> q_gen_2057
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<z, nil, b>() -> q_gen_2052
<z, b, nil>() -> q_gen_2053
<z, b, b>() -> q_gen_2054
}

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

}
--
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: Yes: ((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.008414 s (model generation: 0.006612,  model checking: 0.001802):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<nil>() -> q_gen_2056
<b>() -> q_gen_2057
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<z, nil, a>() -> q_gen_2052
<z, nil, b>() -> q_gen_2052
<z, a, nil>() -> q_gen_2053
<z, b, nil>() -> q_gen_2053
<z, a, a>() -> q_gen_2054
<z, b, b>() -> q_gen_2054
}

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

}
--
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: Yes: (() -> take([z, y, nil]), {
y -> cons(a, nil)
})

-------------------------------------------
Step 7, which took 0.016918 s (model generation: 0.009582,  model checking: 0.007336):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<nil>() -> q_gen_2056
<a>() -> q_gen_2057
<b>() -> q_gen_2057
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<z, nil, a>() -> q_gen_2052
<z, nil, b>() -> q_gen_2052
<z, a, nil>() -> q_gen_2053
<z, b, nil>() -> q_gen_2053
<z, a, a>() -> q_gen_2054
<z, b, b>() -> q_gen_2054
}

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

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

-------------------------------------------
Step 8, which took 0.010574 s (model generation: 0.009433,  model checking: 0.001141):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<nil>() -> q_gen_2056
<a>() -> q_gen_2057
<b>() -> q_gen_2057
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<s, nil, b>(q_gen_2050) -> q_gen_2052
<z, nil, a>() -> q_gen_2052
<z, nil, b>() -> q_gen_2052
<s, b, nil>(q_gen_2050) -> q_gen_2053
<z, a, nil>() -> q_gen_2053
<z, b, nil>() -> q_gen_2053
<s, b, b>(q_gen_2050) -> q_gen_2054
<z, a, a>() -> q_gen_2054
<z, b, b>() -> q_gen_2054
}

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

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

-------------------------------------------
Step 9, which took 0.018297 s (model generation: 0.011821,  model checking: 0.006476):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<cons>(q_gen_2057, q_gen_2056) -> q_gen_2056
<nil>() -> q_gen_2056
<a>() -> q_gen_2057
<b>() -> q_gen_2057
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<s, nil, b>(q_gen_2050) -> q_gen_2052
<z, nil, a>() -> q_gen_2052
<z, nil, b>() -> q_gen_2052
<s, b, nil>(q_gen_2050) -> q_gen_2053
<z, a, nil>() -> q_gen_2053
<z, b, nil>() -> q_gen_2053
<s, b, b>(q_gen_2050) -> q_gen_2054
<z, a, a>() -> q_gen_2054
<z, b, b>() -> q_gen_2054
}

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

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

-------------------------------------------
Step 10, which took 0.022692 s (model generation: 0.015922,  model checking: 0.006770):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<cons>(q_gen_2057, q_gen_2056) -> q_gen_2056
<nil>() -> q_gen_2056
<a>() -> q_gen_2057
<b>() -> q_gen_2057
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<s, nil, a>(q_gen_2050) -> q_gen_2052
<s, nil, b>(q_gen_2050) -> q_gen_2052
<z, nil, a>() -> q_gen_2052
<z, nil, b>() -> q_gen_2052
<s, a, nil>(q_gen_2050) -> q_gen_2053
<s, b, nil>(q_gen_2050) -> q_gen_2053
<z, a, nil>() -> q_gen_2053
<z, b, nil>() -> q_gen_2053
<s, a, a>(q_gen_2050) -> q_gen_2054
<s, b, b>(q_gen_2050) -> q_gen_2054
<z, a, a>() -> q_gen_2054
<z, b, b>() -> q_gen_2054
}

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

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

-------------------------------------------
Step 11, which took 0.021659 s (model generation: 0.012367,  model checking: 0.009292):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<cons>(q_gen_2057, q_gen_2056) -> q_gen_2056
<nil>() -> q_gen_2056
<a>() -> q_gen_2057
<b>() -> q_gen_2057
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<s, nil, a>(q_gen_2050) -> q_gen_2052
<s, nil, b>(q_gen_2050) -> q_gen_2052
<z, cons, b>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, nil, a>() -> q_gen_2052
<z, nil, b>() -> q_gen_2052
<s, a, nil>(q_gen_2050) -> q_gen_2053
<s, b, nil>(q_gen_2050) -> q_gen_2053
<z, a, nil>() -> q_gen_2053
<z, b, nil>() -> q_gen_2053
<s, a, a>(q_gen_2050) -> q_gen_2054
<s, b, b>(q_gen_2050) -> q_gen_2054
<z, a, a>() -> q_gen_2054
<z, b, b>() -> q_gen_2054
}

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

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

-------------------------------------------
Step 12, which took 0.031889 s (model generation: 0.012700,  model checking: 0.019189):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<cons>(q_gen_2057, q_gen_2056) -> q_gen_2056
<nil>() -> q_gen_2056
<a>() -> q_gen_2057
<b>() -> q_gen_2057
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<s, nil, a>(q_gen_2050) -> q_gen_2052
<s, nil, b>(q_gen_2050) -> q_gen_2052
<z, cons, a>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, cons, b>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, nil, a>() -> q_gen_2052
<z, nil, b>() -> q_gen_2052
<s, a, nil>(q_gen_2050) -> q_gen_2053
<s, b, nil>(q_gen_2050) -> q_gen_2053
<z, a, nil>() -> q_gen_2053
<z, b, nil>() -> q_gen_2053
<s, a, a>(q_gen_2050) -> q_gen_2054
<s, b, b>(q_gen_2050) -> q_gen_2054
<z, a, a>() -> q_gen_2054
<z, b, b>() -> q_gen_2054
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 12  ;  () -> take([z, y, nil]) -> 15  ;  (take([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 11  ;  (take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 22
}
Sat witness: Yes: ((take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]), {
_cd -> cons(b, nil)  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(b, nil)
})

-------------------------------------------
Step 13, which took 0.161627 s (model generation: 0.006851,  model checking: 0.154776):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057, q_gen_2082, q_gen_2083},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<cons>(q_gen_2057, q_gen_2056) -> q_gen_2056
<nil>() -> q_gen_2056
<a>() -> q_gen_2057
<b>() -> q_gen_2057
<z, nil>() -> q_gen_2082
<z, b>() -> q_gen_2083
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<s, cons, b>(q_gen_2083, q_gen_2082) -> q_gen_2052
<s, nil, a>(q_gen_2050) -> q_gen_2052
<s, nil, b>(q_gen_2050) -> q_gen_2052
<z, cons, a>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, cons, b>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, nil, a>() -> q_gen_2052
<z, nil, b>() -> q_gen_2052
<s, a, nil>(q_gen_2050) -> q_gen_2053
<s, b, cons>(q_gen_2083, q_gen_2082) -> q_gen_2053
<s, b, nil>(q_gen_2050) -> q_gen_2053
<z, a, nil>() -> q_gen_2053
<z, b, nil>() -> q_gen_2053
<s, a, a>(q_gen_2050) -> q_gen_2054
<s, b, b>(q_gen_2050) -> q_gen_2054
<z, a, a>() -> q_gen_2054
<z, b, b>() -> q_gen_2054
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 13  ;  () -> take([z, y, nil]) -> 16  ;  (take([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 12  ;  (take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 25
}
Sat witness: Yes: ((take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]), {
_cd -> cons(a, nil)  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 14, which took 0.162586 s (model generation: 0.008699,  model checking: 0.153887):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057, q_gen_2082, q_gen_2083},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<cons>(q_gen_2057, q_gen_2056) -> q_gen_2056
<nil>() -> q_gen_2056
<a>() -> q_gen_2057
<b>() -> q_gen_2057
<z, nil>() -> q_gen_2082
<z, a>() -> q_gen_2083
<z, b>() -> q_gen_2083
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<s, cons, b>(q_gen_2083, q_gen_2082) -> q_gen_2052
<s, nil, a>(q_gen_2050) -> q_gen_2052
<s, nil, b>(q_gen_2050) -> q_gen_2052
<z, cons, a>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, cons, b>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, nil, a>() -> q_gen_2052
<z, nil, b>() -> q_gen_2052
<s, a, nil>(q_gen_2050) -> q_gen_2053
<s, b, cons>(q_gen_2083, q_gen_2082) -> q_gen_2053
<s, b, nil>(q_gen_2050) -> q_gen_2053
<z, a, nil>() -> q_gen_2053
<z, b, nil>() -> q_gen_2053
<s, a, a>(q_gen_2050) -> q_gen_2054
<s, b, b>(q_gen_2050) -> q_gen_2054
<z, a, a>() -> q_gen_2054
<z, b, b>() -> q_gen_2054
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 14  ;  () -> take([z, y, nil]) -> 17  ;  (take([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 13  ;  (take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 28
}
Sat witness: Yes: ((take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]), {
_cd -> cons(b, nil)  ;  u -> s(z)  ;  x2 -> a  ;  x3 -> cons(b, nil)
})

-------------------------------------------
Step 15, which took 0.206164 s (model generation: 0.009891,  model checking: 0.196273):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057, q_gen_2082, q_gen_2083},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<cons>(q_gen_2057, q_gen_2056) -> q_gen_2056
<nil>() -> q_gen_2056
<a>() -> q_gen_2057
<b>() -> q_gen_2057
<z, nil>() -> q_gen_2082
<z, a>() -> q_gen_2083
<z, b>() -> q_gen_2083
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<s, cons, a>(q_gen_2083, q_gen_2082) -> q_gen_2052
<s, cons, b>(q_gen_2083, q_gen_2082) -> q_gen_2052
<s, nil, a>(q_gen_2050) -> q_gen_2052
<s, nil, b>(q_gen_2050) -> q_gen_2052
<z, cons, a>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, cons, b>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, nil, a>() -> q_gen_2052
<z, nil, b>() -> q_gen_2052
<s, a, cons>(q_gen_2083, q_gen_2082) -> q_gen_2053
<s, a, nil>(q_gen_2050) -> q_gen_2053
<s, b, cons>(q_gen_2083, q_gen_2082) -> q_gen_2053
<s, b, nil>(q_gen_2050) -> q_gen_2053
<z, a, nil>() -> q_gen_2053
<z, b, nil>() -> q_gen_2053
<s, a, a>(q_gen_2050) -> q_gen_2054
<s, b, b>(q_gen_2050) -> q_gen_2054
<z, a, a>() -> q_gen_2054
<z, b, b>() -> q_gen_2054
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 15  ;  () -> take([z, y, nil]) -> 18  ;  (take([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 14  ;  (take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 31
}
Sat witness: Yes: ((take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]), {
_cd -> cons(b, nil)  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 16, which took 0.344141 s (model generation: 0.010931,  model checking: 0.333210):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057, q_gen_2082, q_gen_2083},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<cons>(q_gen_2057, q_gen_2056) -> q_gen_2056
<nil>() -> q_gen_2056
<a>() -> q_gen_2057
<b>() -> q_gen_2057
<z, cons>(q_gen_2057, q_gen_2056) -> q_gen_2082
<z, nil>() -> q_gen_2082
<z, a>() -> q_gen_2083
<z, b>() -> q_gen_2083
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<s, cons, a>(q_gen_2083, q_gen_2082) -> q_gen_2052
<s, cons, b>(q_gen_2083, q_gen_2082) -> q_gen_2052
<s, nil, a>(q_gen_2050) -> q_gen_2052
<s, nil, b>(q_gen_2050) -> q_gen_2052
<z, cons, a>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, cons, b>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, nil, a>() -> q_gen_2052
<z, nil, b>() -> q_gen_2052
<s, a, cons>(q_gen_2083, q_gen_2082) -> q_gen_2053
<s, a, nil>(q_gen_2050) -> q_gen_2053
<s, b, cons>(q_gen_2083, q_gen_2082) -> q_gen_2053
<s, b, nil>(q_gen_2050) -> q_gen_2053
<z, a, nil>() -> q_gen_2053
<z, b, nil>() -> q_gen_2053
<s, a, a>(q_gen_2050) -> q_gen_2054
<s, b, b>(q_gen_2050) -> q_gen_2054
<z, a, a>() -> q_gen_2054
<z, b, b>() -> q_gen_2054
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 16  ;  () -> take([z, y, nil]) -> 19  ;  (take([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 15  ;  (take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 34
}
Sat witness: Yes: ((take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]), {
_cd -> cons(a, nil)  ;  u -> s(s(z))  ;  x2 -> b  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 17, which took 0.309110 s (model generation: 0.012251,  model checking: 0.296859):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057, q_gen_2082, q_gen_2083},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<cons>(q_gen_2057, q_gen_2056) -> q_gen_2056
<nil>() -> q_gen_2056
<a>() -> q_gen_2057
<b>() -> q_gen_2057
<s, nil>(q_gen_2050) -> q_gen_2082
<z, cons>(q_gen_2057, q_gen_2056) -> q_gen_2082
<z, nil>() -> q_gen_2082
<s, a>(q_gen_2050) -> q_gen_2083
<z, a>() -> q_gen_2083
<z, b>() -> q_gen_2083
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<s, cons, a>(q_gen_2083, q_gen_2082) -> q_gen_2052
<s, cons, b>(q_gen_2083, q_gen_2082) -> q_gen_2052
<s, nil, a>(q_gen_2050) -> q_gen_2052
<s, nil, b>(q_gen_2050) -> q_gen_2052
<z, cons, a>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, cons, b>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, nil, a>() -> q_gen_2052
<z, nil, b>() -> q_gen_2052
<s, a, cons>(q_gen_2083, q_gen_2082) -> q_gen_2053
<s, a, nil>(q_gen_2050) -> q_gen_2053
<s, b, cons>(q_gen_2083, q_gen_2082) -> q_gen_2053
<s, b, nil>(q_gen_2050) -> q_gen_2053
<z, a, nil>() -> q_gen_2053
<z, b, nil>() -> q_gen_2053
<s, a, a>(q_gen_2050) -> q_gen_2054
<s, b, b>(q_gen_2050) -> q_gen_2054
<z, a, a>() -> q_gen_2054
<z, b, b>() -> q_gen_2054
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 17  ;  () -> take([z, y, nil]) -> 20  ;  (take([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 16  ;  (take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 37
}
Sat witness: Yes: ((take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]), {
_cd -> cons(b, nil)  ;  u -> s(s(z))  ;  x2 -> b  ;  x3 -> cons(b, nil)
})

-------------------------------------------
Step 18, which took 0.140217 s (model generation: 0.013538,  model checking: 0.126679):

Model:
|_
{
take -> 
{{{
Q={q_gen_2048, q_gen_2050, q_gen_2052, q_gen_2053, q_gen_2054, q_gen_2056, q_gen_2057, q_gen_2082, q_gen_2083},
Q_f={q_gen_2048},
Delta=
{
<s>(q_gen_2050) -> q_gen_2050
<z>() -> q_gen_2050
<cons>(q_gen_2057, q_gen_2056) -> q_gen_2056
<nil>() -> q_gen_2056
<a>() -> q_gen_2057
<b>() -> q_gen_2057
<s, nil>(q_gen_2050) -> q_gen_2082
<z, cons>(q_gen_2057, q_gen_2056) -> q_gen_2082
<z, nil>() -> q_gen_2082
<s, a>(q_gen_2050) -> q_gen_2083
<s, b>(q_gen_2050) -> q_gen_2083
<z, a>() -> q_gen_2083
<z, b>() -> q_gen_2083
<s, cons, cons>(q_gen_2054, q_gen_2053, q_gen_2052, q_gen_2048) -> q_gen_2048
<s, nil, nil>(q_gen_2050) -> q_gen_2048
<z, cons, nil>(q_gen_2057, q_gen_2056) -> q_gen_2048
<z, nil, nil>() -> q_gen_2048
<s, cons, a>(q_gen_2083, q_gen_2082) -> q_gen_2052
<s, cons, b>(q_gen_2083, q_gen_2082) -> q_gen_2052
<s, nil, a>(q_gen_2050) -> q_gen_2052
<s, nil, b>(q_gen_2050) -> q_gen_2052
<z, cons, a>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, cons, b>(q_gen_2057, q_gen_2056) -> q_gen_2052
<z, nil, a>() -> q_gen_2052
<z, nil, b>() -> q_gen_2052
<s, a, cons>(q_gen_2083, q_gen_2082) -> q_gen_2053
<s, a, nil>(q_gen_2050) -> q_gen_2053
<s, b, cons>(q_gen_2083, q_gen_2082) -> q_gen_2053
<s, b, nil>(q_gen_2050) -> q_gen_2053
<z, a, nil>() -> q_gen_2053
<z, b, nil>() -> q_gen_2053
<s, a, a>(q_gen_2050) -> q_gen_2054
<s, b, b>(q_gen_2050) -> q_gen_2054
<z, a, a>() -> q_gen_2054
<z, b, b>() -> q_gen_2054
}

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

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

Teacher's answer:
New clause system:
{
() -> take([s(u), nil, nil]) -> 18  ;  () -> take([z, y, nil]) -> 21  ;  (take([n, xs, _id]) /\ take([s(n), cons(x, xs), _hd])) -> eq_eltlist([_hd, cons(x, _id)]) -> 17  ;  (take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]) -> 40
}
Sat witness: Yes: ((take([u, x3, _cd])) -> take([s(u), cons(x2, x3), cons(x2, _cd)]), {
_cd -> cons(a, cons(b, nil))  ;  u -> s(s(z))  ;  x2 -> a  ;  x3 -> cons(a, cons(b, nil))
})

Total time: 1.526829
Reason for stopping: Proved