Solving ../../benchmarks/true/isaplanner_prop40.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, _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 1.752149 seconds.
Proved
Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996, q_gen_2021, q_gen_2022},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<cons>(q_gen_1996, q_gen_1995) -> q_gen_1995
<nil>() -> q_gen_1995
<a>() -> q_gen_1996
<b>() -> q_gen_1996
<s, cons>(q_gen_2022, q_gen_2021) -> q_gen_2021
<s, nil>(q_gen_1989) -> q_gen_2021
<z, cons>(q_gen_1996, q_gen_1995) -> q_gen_2021
<z, nil>() -> q_gen_2021
<s, a>(q_gen_1989) -> q_gen_2022
<s, b>(q_gen_1989) -> q_gen_2022
<z, a>() -> q_gen_2022
<z, b>() -> q_gen_2022
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<s, cons, a>(q_gen_2022, q_gen_2021) -> q_gen_1991
<s, cons, b>(q_gen_2022, q_gen_2021) -> q_gen_1991
<s, nil, a>(q_gen_1989) -> q_gen_1991
<s, nil, b>(q_gen_1989) -> q_gen_1991
<z, cons, a>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, cons, b>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, nil, a>() -> q_gen_1991
<z, nil, b>() -> q_gen_1991
<s, a, cons>(q_gen_2022, q_gen_2021) -> q_gen_1992
<s, a, nil>(q_gen_1989) -> q_gen_1992
<s, b, cons>(q_gen_2022, q_gen_2021) -> q_gen_1992
<s, b, nil>(q_gen_1989) -> q_gen_1992
<z, a, nil>() -> q_gen_1992
<z, b, nil>() -> q_gen_1992
<s, a, a>(q_gen_1989) -> q_gen_1993
<s, b, b>(q_gen_1989) -> q_gen_1993
<z, a, a>() -> q_gen_1993
<z, b, b>() -> q_gen_1993
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004206 s (model generation: 0.003756,  model checking: 0.000450):

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

-------------------------------------------
Step 1, which took 0.004861 s (model generation: 0.004519,  model checking: 0.000342):

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

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

-------------------------------------------
Step 2, which took 0.008237 s (model generation: 0.006808,  model checking: 0.001429):

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

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([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 4  ;  (take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 2
}
Sat witness: Yes: ((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.010941 s (model generation: 0.010558,  model checking: 0.000383):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993},
Q_f={q_gen_1987},
Delta=
{
<z>() -> q_gen_1989
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<z, nil, b>() -> q_gen_1991
<z, b, nil>() -> q_gen_1992
<z, b, b>() -> q_gen_1993
}

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

-------------------------------------------
Step 4, which took 0.007735 s (model generation: 0.006280,  model checking: 0.001455):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996},
Q_f={q_gen_1987},
Delta=
{
<z>() -> q_gen_1989
<nil>() -> q_gen_1995
<b>() -> q_gen_1996
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<z, nil, b>() -> q_gen_1991
<z, b, nil>() -> q_gen_1992
<z, b, b>() -> q_gen_1993
}

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

-------------------------------------------
Step 5, which took 0.014321 s (model generation: 0.012241,  model checking: 0.002080):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<nil>() -> q_gen_1995
<b>() -> q_gen_1996
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<z, nil, b>() -> q_gen_1991
<z, b, nil>() -> q_gen_1992
<z, b, b>() -> q_gen_1993
}

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([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 7  ;  (take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 5
}
Sat witness: Yes: ((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.014672 s (model generation: 0.012904,  model checking: 0.001768):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<nil>() -> q_gen_1995
<b>() -> q_gen_1996
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<z, nil, a>() -> q_gen_1991
<z, nil, b>() -> q_gen_1991
<z, a, nil>() -> q_gen_1992
<z, b, nil>() -> q_gen_1992
<z, a, a>() -> q_gen_1993
<z, b, b>() -> q_gen_1993
}

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

-------------------------------------------
Step 7, which took 0.013949 s (model generation: 0.011247,  model checking: 0.002702):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<nil>() -> q_gen_1995
<a>() -> q_gen_1996
<b>() -> q_gen_1996
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<z, nil, a>() -> q_gen_1991
<z, nil, b>() -> q_gen_1991
<z, a, nil>() -> q_gen_1992
<z, b, nil>() -> q_gen_1992
<z, a, a>() -> q_gen_1993
<z, b, b>() -> q_gen_1993
}

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([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 10  ;  (take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 7
}
Sat witness: Yes: ((take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]), {
_ou -> nil  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> nil
})

-------------------------------------------
Step 8, which took 0.009759 s (model generation: 0.008980,  model checking: 0.000779):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<nil>() -> q_gen_1995
<a>() -> q_gen_1996
<b>() -> q_gen_1996
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<s, nil, b>(q_gen_1989) -> q_gen_1991
<z, nil, a>() -> q_gen_1991
<z, nil, b>() -> q_gen_1991
<s, b, nil>(q_gen_1989) -> q_gen_1992
<z, a, nil>() -> q_gen_1992
<z, b, nil>() -> q_gen_1992
<s, b, b>(q_gen_1989) -> q_gen_1993
<z, a, a>() -> q_gen_1993
<z, b, b>() -> q_gen_1993
}

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([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 10  ;  (take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 8
}
Sat witness: Yes: (() -> take([z, y, nil]), {
y -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 9, which took 0.021503 s (model generation: 0.014441,  model checking: 0.007062):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<cons>(q_gen_1996, q_gen_1995) -> q_gen_1995
<nil>() -> q_gen_1995
<a>() -> q_gen_1996
<b>() -> q_gen_1996
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<s, nil, b>(q_gen_1989) -> q_gen_1991
<z, nil, a>() -> q_gen_1991
<z, nil, b>() -> q_gen_1991
<s, b, nil>(q_gen_1989) -> q_gen_1992
<z, a, nil>() -> q_gen_1992
<z, b, nil>() -> q_gen_1992
<s, b, b>(q_gen_1989) -> q_gen_1993
<z, a, a>() -> q_gen_1993
<z, b, b>() -> q_gen_1993
}

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([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 13  ;  (take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 9
}
Sat witness: Yes: ((take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]), {
_ou -> nil  ;  u -> s(z)  ;  x2 -> a  ;  x3 -> nil
})

-------------------------------------------
Step 10, which took 0.025078 s (model generation: 0.016184,  model checking: 0.008894):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<cons>(q_gen_1996, q_gen_1995) -> q_gen_1995
<nil>() -> q_gen_1995
<a>() -> q_gen_1996
<b>() -> q_gen_1996
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<s, nil, a>(q_gen_1989) -> q_gen_1991
<s, nil, b>(q_gen_1989) -> q_gen_1991
<z, nil, a>() -> q_gen_1991
<z, nil, b>() -> q_gen_1991
<s, a, nil>(q_gen_1989) -> q_gen_1992
<s, b, nil>(q_gen_1989) -> q_gen_1992
<z, a, nil>() -> q_gen_1992
<z, b, nil>() -> q_gen_1992
<s, a, a>(q_gen_1989) -> q_gen_1993
<s, b, b>(q_gen_1989) -> q_gen_1993
<z, a, a>() -> q_gen_1993
<z, b, b>() -> q_gen_1993
}

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([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 16  ;  (take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 10
}
Sat witness: Yes: ((take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]), {
_ou -> nil  ;  u -> z  ;  x2 -> b  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 11, which took 0.026037 s (model generation: 0.017259,  model checking: 0.008778):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<cons>(q_gen_1996, q_gen_1995) -> q_gen_1995
<nil>() -> q_gen_1995
<a>() -> q_gen_1996
<b>() -> q_gen_1996
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<s, nil, a>(q_gen_1989) -> q_gen_1991
<s, nil, b>(q_gen_1989) -> q_gen_1991
<z, cons, b>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, nil, a>() -> q_gen_1991
<z, nil, b>() -> q_gen_1991
<s, a, nil>(q_gen_1989) -> q_gen_1992
<s, b, nil>(q_gen_1989) -> q_gen_1992
<z, a, nil>() -> q_gen_1992
<z, b, nil>() -> q_gen_1992
<s, a, a>(q_gen_1989) -> q_gen_1993
<s, b, b>(q_gen_1989) -> q_gen_1993
<z, a, a>() -> q_gen_1993
<z, b, b>() -> q_gen_1993
}

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([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 19  ;  (take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 11
}
Sat witness: Yes: ((take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]), {
_ou -> nil  ;  u -> z  ;  x2 -> a  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 12, which took 0.041027 s (model generation: 0.019002,  model checking: 0.022025):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<cons>(q_gen_1996, q_gen_1995) -> q_gen_1995
<nil>() -> q_gen_1995
<a>() -> q_gen_1996
<b>() -> q_gen_1996
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<s, nil, a>(q_gen_1989) -> q_gen_1991
<s, nil, b>(q_gen_1989) -> q_gen_1991
<z, cons, a>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, cons, b>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, nil, a>() -> q_gen_1991
<z, nil, b>() -> q_gen_1991
<s, a, nil>(q_gen_1989) -> q_gen_1992
<s, b, nil>(q_gen_1989) -> q_gen_1992
<z, a, nil>() -> q_gen_1992
<z, b, nil>() -> q_gen_1992
<s, a, a>(q_gen_1989) -> q_gen_1993
<s, b, b>(q_gen_1989) -> q_gen_1993
<z, a, a>() -> q_gen_1993
<z, b, b>() -> q_gen_1993
}

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([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 22  ;  (take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 12
}
Sat witness: Yes: ((take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]), {
_ou -> cons(b, nil)  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(b, nil)
})

-------------------------------------------
Step 13, which took 0.167815 s (model generation: 0.006998,  model checking: 0.160817):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996, q_gen_2021, q_gen_2022},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<cons>(q_gen_1996, q_gen_1995) -> q_gen_1995
<nil>() -> q_gen_1995
<a>() -> q_gen_1996
<b>() -> q_gen_1996
<z, nil>() -> q_gen_2021
<z, b>() -> q_gen_2022
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<s, cons, b>(q_gen_2022, q_gen_2021) -> q_gen_1991
<s, nil, a>(q_gen_1989) -> q_gen_1991
<s, nil, b>(q_gen_1989) -> q_gen_1991
<z, cons, a>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, cons, b>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, nil, a>() -> q_gen_1991
<z, nil, b>() -> q_gen_1991
<s, a, nil>(q_gen_1989) -> q_gen_1992
<s, b, cons>(q_gen_2022, q_gen_2021) -> q_gen_1992
<s, b, nil>(q_gen_1989) -> q_gen_1992
<z, a, nil>() -> q_gen_1992
<z, b, nil>() -> q_gen_1992
<s, a, a>(q_gen_1989) -> q_gen_1993
<s, b, b>(q_gen_1989) -> q_gen_1993
<z, a, a>() -> q_gen_1993
<z, b, b>() -> q_gen_1993
}

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([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 25  ;  (take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 13
}
Sat witness: Yes: ((take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]), {
_ou -> cons(a, nil)  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 14, which took 0.159473 s (model generation: 0.008741,  model checking: 0.150732):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996, q_gen_2021, q_gen_2022},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<cons>(q_gen_1996, q_gen_1995) -> q_gen_1995
<nil>() -> q_gen_1995
<a>() -> q_gen_1996
<b>() -> q_gen_1996
<z, nil>() -> q_gen_2021
<z, a>() -> q_gen_2022
<z, b>() -> q_gen_2022
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<s, cons, b>(q_gen_2022, q_gen_2021) -> q_gen_1991
<s, nil, a>(q_gen_1989) -> q_gen_1991
<s, nil, b>(q_gen_1989) -> q_gen_1991
<z, cons, a>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, cons, b>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, nil, a>() -> q_gen_1991
<z, nil, b>() -> q_gen_1991
<s, a, nil>(q_gen_1989) -> q_gen_1992
<s, b, cons>(q_gen_2022, q_gen_2021) -> q_gen_1992
<s, b, nil>(q_gen_1989) -> q_gen_1992
<z, a, nil>() -> q_gen_1992
<z, b, nil>() -> q_gen_1992
<s, a, a>(q_gen_1989) -> q_gen_1993
<s, b, b>(q_gen_1989) -> q_gen_1993
<z, a, a>() -> q_gen_1993
<z, b, b>() -> q_gen_1993
}

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([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 28  ;  (take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 14
}
Sat witness: Yes: ((take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]), {
_ou -> cons(b, nil)  ;  u -> s(z)  ;  x2 -> a  ;  x3 -> cons(b, nil)
})

-------------------------------------------
Step 15, which took 0.175671 s (model generation: 0.009692,  model checking: 0.165979):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996, q_gen_2021, q_gen_2022},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<cons>(q_gen_1996, q_gen_1995) -> q_gen_1995
<nil>() -> q_gen_1995
<a>() -> q_gen_1996
<b>() -> q_gen_1996
<z, nil>() -> q_gen_2021
<z, a>() -> q_gen_2022
<z, b>() -> q_gen_2022
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<s, cons, a>(q_gen_2022, q_gen_2021) -> q_gen_1991
<s, cons, b>(q_gen_2022, q_gen_2021) -> q_gen_1991
<s, nil, a>(q_gen_1989) -> q_gen_1991
<s, nil, b>(q_gen_1989) -> q_gen_1991
<z, cons, a>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, cons, b>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, nil, a>() -> q_gen_1991
<z, nil, b>() -> q_gen_1991
<s, a, cons>(q_gen_2022, q_gen_2021) -> q_gen_1992
<s, a, nil>(q_gen_1989) -> q_gen_1992
<s, b, cons>(q_gen_2022, q_gen_2021) -> q_gen_1992
<s, b, nil>(q_gen_1989) -> q_gen_1992
<z, a, nil>() -> q_gen_1992
<z, b, nil>() -> q_gen_1992
<s, a, a>(q_gen_1989) -> q_gen_1993
<s, b, b>(q_gen_1989) -> q_gen_1993
<z, a, a>() -> q_gen_1993
<z, b, b>() -> q_gen_1993
}

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([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 31  ;  (take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 15
}
Sat witness: Yes: ((take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]), {
_ou -> cons(b, nil)  ;  u -> s(z)  ;  x2 -> a  ;  x3 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 16, which took 0.311891 s (model generation: 0.010681,  model checking: 0.301210):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996, q_gen_2021, q_gen_2022},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<cons>(q_gen_1996, q_gen_1995) -> q_gen_1995
<nil>() -> q_gen_1995
<a>() -> q_gen_1996
<b>() -> q_gen_1996
<z, cons>(q_gen_1996, q_gen_1995) -> q_gen_2021
<z, nil>() -> q_gen_2021
<z, a>() -> q_gen_2022
<z, b>() -> q_gen_2022
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<s, cons, a>(q_gen_2022, q_gen_2021) -> q_gen_1991
<s, cons, b>(q_gen_2022, q_gen_2021) -> q_gen_1991
<s, nil, a>(q_gen_1989) -> q_gen_1991
<s, nil, b>(q_gen_1989) -> q_gen_1991
<z, cons, a>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, cons, b>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, nil, a>() -> q_gen_1991
<z, nil, b>() -> q_gen_1991
<s, a, cons>(q_gen_2022, q_gen_2021) -> q_gen_1992
<s, a, nil>(q_gen_1989) -> q_gen_1992
<s, b, cons>(q_gen_2022, q_gen_2021) -> q_gen_1992
<s, b, nil>(q_gen_1989) -> q_gen_1992
<z, a, nil>() -> q_gen_1992
<z, b, nil>() -> q_gen_1992
<s, a, a>(q_gen_1989) -> q_gen_1993
<s, b, b>(q_gen_1989) -> q_gen_1993
<z, a, a>() -> q_gen_1993
<z, b, b>() -> q_gen_1993
}

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([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 34  ;  (take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 16
}
Sat witness: Yes: ((take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]), {
_ou -> cons(a, nil)  ;  u -> s(s(z))  ;  x2 -> a  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 17, which took 0.514524 s (model generation: 0.011774,  model checking: 0.502750):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996, q_gen_2021, q_gen_2022},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<cons>(q_gen_1996, q_gen_1995) -> q_gen_1995
<nil>() -> q_gen_1995
<a>() -> q_gen_1996
<b>() -> q_gen_1996
<s, nil>(q_gen_1989) -> q_gen_2021
<z, cons>(q_gen_1996, q_gen_1995) -> q_gen_2021
<z, nil>() -> q_gen_2021
<s, a>(q_gen_1989) -> q_gen_2022
<z, a>() -> q_gen_2022
<z, b>() -> q_gen_2022
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<s, cons, a>(q_gen_2022, q_gen_2021) -> q_gen_1991
<s, cons, b>(q_gen_2022, q_gen_2021) -> q_gen_1991
<s, nil, a>(q_gen_1989) -> q_gen_1991
<s, nil, b>(q_gen_1989) -> q_gen_1991
<z, cons, a>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, cons, b>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, nil, a>() -> q_gen_1991
<z, nil, b>() -> q_gen_1991
<s, a, cons>(q_gen_2022, q_gen_2021) -> q_gen_1992
<s, a, nil>(q_gen_1989) -> q_gen_1992
<s, b, cons>(q_gen_2022, q_gen_2021) -> q_gen_1992
<s, b, nil>(q_gen_1989) -> q_gen_1992
<z, a, nil>() -> q_gen_1992
<z, b, nil>() -> q_gen_1992
<s, a, a>(q_gen_1989) -> q_gen_1993
<s, b, b>(q_gen_1989) -> q_gen_1993
<z, a, a>() -> q_gen_1993
<z, b, b>() -> q_gen_1993
}

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([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 37  ;  (take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 17
}
Sat witness: Yes: ((take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]), {
_ou -> cons(b, nil)  ;  u -> s(s(z))  ;  x2 -> a  ;  x3 -> cons(b, nil)
})

-------------------------------------------
Step 18, which took 0.187071 s (model generation: 0.013045,  model checking: 0.174026):

Model:
|_
{
take -> 
{{{
Q={q_gen_1987, q_gen_1989, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1995, q_gen_1996, q_gen_2021, q_gen_2022},
Q_f={q_gen_1987},
Delta=
{
<s>(q_gen_1989) -> q_gen_1989
<z>() -> q_gen_1989
<cons>(q_gen_1996, q_gen_1995) -> q_gen_1995
<nil>() -> q_gen_1995
<a>() -> q_gen_1996
<b>() -> q_gen_1996
<s, nil>(q_gen_1989) -> q_gen_2021
<z, cons>(q_gen_1996, q_gen_1995) -> q_gen_2021
<z, nil>() -> q_gen_2021
<s, a>(q_gen_1989) -> q_gen_2022
<s, b>(q_gen_1989) -> q_gen_2022
<z, a>() -> q_gen_2022
<z, b>() -> q_gen_2022
<s, cons, cons>(q_gen_1993, q_gen_1992, q_gen_1991, q_gen_1987) -> q_gen_1987
<s, nil, nil>(q_gen_1989) -> q_gen_1987
<z, cons, nil>(q_gen_1996, q_gen_1995) -> q_gen_1987
<z, nil, nil>() -> q_gen_1987
<s, cons, a>(q_gen_2022, q_gen_2021) -> q_gen_1991
<s, cons, b>(q_gen_2022, q_gen_2021) -> q_gen_1991
<s, nil, a>(q_gen_1989) -> q_gen_1991
<s, nil, b>(q_gen_1989) -> q_gen_1991
<z, cons, a>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, cons, b>(q_gen_1996, q_gen_1995) -> q_gen_1991
<z, nil, a>() -> q_gen_1991
<z, nil, b>() -> q_gen_1991
<s, a, cons>(q_gen_2022, q_gen_2021) -> q_gen_1992
<s, a, nil>(q_gen_1989) -> q_gen_1992
<s, b, cons>(q_gen_2022, q_gen_2021) -> q_gen_1992
<s, b, nil>(q_gen_1989) -> q_gen_1992
<z, a, nil>() -> q_gen_1992
<z, b, nil>() -> q_gen_1992
<s, a, a>(q_gen_1989) -> q_gen_1993
<s, b, b>(q_gen_1989) -> q_gen_1993
<z, a, a>() -> q_gen_1993
<z, b, b>() -> q_gen_1993
}

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([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]) -> 40  ;  (take([z, xs, _tu])) -> eq_eltlist([_tu, nil]) -> 18
}
Sat witness: Yes: ((take([u, x3, _ou])) -> take([s(u), cons(x2, x3), cons(x2, _ou)]), {
_ou -> cons(b, cons(b, nil))  ;  u -> s(s(z))  ;  x2 -> a  ;  x3 -> cons(b, cons(b, nil))
})

Total time: 1.752149
Reason for stopping: Proved