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, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)])}
(take([_sq, _tq, _uq]) /\ take([_sq, _tq, _vq])) -> eq_eltlist([_uq, _vq])
)
}

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


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

Clause system for inference is:

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


Solving took 64.700635 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4456, q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4460, q_gen_4461, q_gen_4462, q_gen_4463, q_gen_4464, q_gen_4465, q_gen_4466, q_gen_4467, q_gen_4468, q_gen_4469, q_gen_4470, q_gen_4471, q_gen_4472, q_gen_4473, q_gen_4474, q_gen_4475, q_gen_4476, q_gen_4477, q_gen_4478, q_gen_4479, q_gen_4480, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4484, q_gen_4485, q_gen_4486, q_gen_4487, q_gen_4488, q_gen_4489, q_gen_4490, q_gen_4491, q_gen_4492, q_gen_4493, q_gen_4494, q_gen_4495, q_gen_4496, q_gen_4497, q_gen_4498, q_gen_4499, q_gen_4500, q_gen_4501, q_gen_4502, q_gen_4503, q_gen_4504, q_gen_4505, q_gen_4506, q_gen_4507, q_gen_4508, q_gen_4509, q_gen_4510, q_gen_4511, q_gen_4512, q_gen_4513, q_gen_4514, q_gen_4515, q_gen_4516, q_gen_4517, q_gen_4518, q_gen_4519, q_gen_4520, q_gen_4521, q_gen_4522, q_gen_4523, q_gen_4524, q_gen_4525, q_gen_4526, q_gen_4527, q_gen_4528, q_gen_4529, q_gen_4530, q_gen_4531, q_gen_4532, q_gen_4533, q_gen_4534, q_gen_4535, q_gen_4536, q_gen_4537, q_gen_4538, q_gen_4539, q_gen_4540, q_gen_4541, q_gen_4542, q_gen_4543, q_gen_4544, q_gen_4545, q_gen_4546, q_gen_4547, q_gen_4548, q_gen_4549, q_gen_4550, q_gen_4551, q_gen_4552, q_gen_4553, q_gen_4554, q_gen_4555, q_gen_4556, q_gen_4557, q_gen_4558, q_gen_4559, q_gen_4560, q_gen_4561, q_gen_4562, q_gen_4563, q_gen_4564, q_gen_4565, q_gen_4566, q_gen_4567, q_gen_4568, q_gen_4569, q_gen_4570, q_gen_4571, q_gen_4572, q_gen_4573, q_gen_4574, q_gen_4575, q_gen_4576, q_gen_4577, q_gen_4578, q_gen_4579, q_gen_4580, q_gen_4581, q_gen_4582, q_gen_4583, q_gen_4584, q_gen_4585, q_gen_4586, q_gen_4587, q_gen_4588, q_gen_4589, q_gen_4590, q_gen_4591, q_gen_4592, q_gen_4593, q_gen_4594, q_gen_4595, q_gen_4596, q_gen_4597, q_gen_4598, q_gen_4599, q_gen_4600, q_gen_4601, q_gen_4602, q_gen_4603, q_gen_4604, q_gen_4605, q_gen_4606, q_gen_4607, q_gen_4608, q_gen_4609, q_gen_4610, q_gen_4611, q_gen_4612},
Q_f={},
Delta=
{
<z>() -> q_gen_4457
<nil>() -> q_gen_4462
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<cons>(q_gen_4470, q_gen_4462) -> q_gen_4469
<a>() -> q_gen_4470
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4486
<s>(q_gen_4465) -> q_gen_4510
<cons>(q_gen_4470, q_gen_4469) -> q_gen_4523
<cons>(q_gen_4470, q_gen_4486) -> q_gen_4532
<s>(q_gen_4510) -> q_gen_4551
<cons>(q_gen_4470, q_gen_4523) -> q_gen_4556
<cons>(q_gen_4463, q_gen_4486) -> q_gen_4583
<cons>(q_gen_4463, q_gen_4469) -> q_gen_4595
<cons>(q_gen_4463, q_gen_4523) -> q_gen_4599
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4479
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4479) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4496
<cons, cons>(q_gen_4491, q_gen_4496) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4503
<cons, cons>(q_gen_4491, q_gen_4498) -> q_gen_4508
<cons, nil>(q_gen_4463, q_gen_4486) -> q_gen_4512
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4515
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4518
<cons, cons>(q_gen_4491, q_gen_4518) -> q_gen_4520
<cons, cons>(q_gen_4482, q_gen_4493) -> q_gen_4530
<cons, cons>(q_gen_4491, q_gen_4537) -> q_gen_4536
<cons, cons>(q_gen_4482, q_gen_4512) -> q_gen_4537
<cons, cons>(q_gen_4482, q_gen_4541) -> q_gen_4540
<cons, cons>(q_gen_4491, q_gen_4479) -> q_gen_4541
<cons, cons>(q_gen_4491, q_gen_4503) -> q_gen_4554
<cons, cons>(q_gen_4482, q_gen_4518) -> q_gen_4559
<cons, cons>(q_gen_4491, q_gen_4562) -> q_gen_4561
<cons, cons>(q_gen_4491, q_gen_4563) -> q_gen_4562
<cons, cons>(q_gen_4491, q_gen_4564) -> q_gen_4563
<cons, nil>(q_gen_4470, q_gen_4486) -> q_gen_4564
<cons, cons>(q_gen_4491, q_gen_4567) -> q_gen_4566
<cons, cons>(q_gen_4491, q_gen_4493) -> q_gen_4567
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4570
<cons, cons>(q_gen_4491, q_gen_4501) -> q_gen_4572
<cons, nil>(q_gen_4470, q_gen_4469) -> q_gen_4574
<cons, cons>(q_gen_4491, q_gen_4559) -> q_gen_4579
<cons, cons>(q_gen_4491, q_gen_4520) -> q_gen_4581
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4585
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4593
<cons, cons>(q_gen_4491, q_gen_4572) -> q_gen_4597
<cons, cons>(q_gen_4491, q_gen_4606) -> q_gen_4605
<cons, cons>(q_gen_4491, q_gen_4541) -> q_gen_4606
<cons, cons>(q_gen_4482, q_gen_4520) -> q_gen_4610
<z, nil, nil>() -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4456
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4458
<z, b, b>() -> q_gen_4460
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4461
<s, nil, nil>(q_gen_4465) -> q_gen_4464
<s, cons, cons>(q_gen_4467, q_gen_4459) -> q_gen_4466
<z, a, a>() -> q_gen_4467
<z, cons, nil>(q_gen_4470, q_gen_4469) -> q_gen_4468
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4471
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4474, q_gen_4459) -> q_gen_4473
<s, a, a>(q_gen_4457) -> q_gen_4474
<z, cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4475
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4476
<s, cons, cons>(q_gen_4472, q_gen_4479) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4480
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4484
<z, cons, nil>(q_gen_4463, q_gen_4486) -> q_gen_4485
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4487
<s, cons, cons>(q_gen_4467, q_gen_4481) -> q_gen_4488
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4489
<s, cons, cons>(q_gen_4460, q_gen_4493) -> q_gen_4492
<z, cons, nil>(q_gen_4470, q_gen_4486) -> q_gen_4494
<s, cons, cons>(q_gen_4472, q_gen_4496) -> q_gen_4495
<s, cons, cons>(q_gen_4499, q_gen_4498) -> q_gen_4497
<s, b, b>(q_gen_4465) -> q_gen_4499
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4500
<s, cons, cons>(q_gen_4499, q_gen_4503) -> q_gen_4502
<s, cons, cons>(q_gen_4474, q_gen_4496) -> q_gen_4504
<s, cons, cons>(q_gen_4460, q_gen_4479) -> q_gen_4505
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4506
<s, cons, cons>(q_gen_4499, q_gen_4508) -> q_gen_4507
<s, nil, nil>(q_gen_4510) -> q_gen_4509
<s, cons, cons>(q_gen_4474, q_gen_4512) -> q_gen_4511
<s, cons, cons>(q_gen_4467, q_gen_4477) -> q_gen_4513
<s, cons, cons>(q_gen_4460, q_gen_4515) -> q_gen_4514
<z, cons, nil>(q_gen_4463, q_gen_4469) -> q_gen_4516
<s, cons, cons>(q_gen_4472, q_gen_4518) -> q_gen_4517
<s, cons, cons>(q_gen_4499, q_gen_4520) -> q_gen_4519
<s, cons, cons>(q_gen_4460, q_gen_4503) -> q_gen_4521
<z, cons, nil>(q_gen_4470, q_gen_4523) -> q_gen_4522
<s, cons, cons>(q_gen_4474, q_gen_4481) -> q_gen_4524
<s, cons, cons>(q_gen_4483, q_gen_4501) -> q_gen_4525
<s, cons, cons>(q_gen_4474, q_gen_4501) -> q_gen_4526
<s, cons, cons>(q_gen_4467, q_gen_4479) -> q_gen_4527
<s, cons, cons>(q_gen_4474, q_gen_4493) -> q_gen_4528
<s, cons, cons>(q_gen_4460, q_gen_4530) -> q_gen_4529
<z, cons, nil>(q_gen_4470, q_gen_4532) -> q_gen_4531
<s, cons, cons>(q_gen_4499, q_gen_4481) -> q_gen_4533
<s, cons, cons>(q_gen_4460, q_gen_4518) -> q_gen_4534
<s, cons, cons>(q_gen_4538, q_gen_4536) -> q_gen_4535
<s, a, a>(q_gen_4510) -> q_gen_4538
<s, cons, cons>(q_gen_4499, q_gen_4540) -> q_gen_4539
<s, cons, cons>(q_gen_4474, q_gen_4490) -> q_gen_4542
<s, cons, cons>(q_gen_4544, q_gen_4493) -> q_gen_4543
<s, b, b>(q_gen_4510) -> q_gen_4544
<s, cons, cons>(q_gen_4483, q_gen_4518) -> q_gen_4545
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4546
<s, cons, cons>(q_gen_4460, q_gen_4541) -> q_gen_4547
<s, cons, cons>(q_gen_4499, q_gen_4490) -> q_gen_4548
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4549
<s, nil, nil>(q_gen_4551) -> q_gen_4550
<s, cons, cons>(q_gen_4474, q_gen_4518) -> q_gen_4552
<s, cons, cons>(q_gen_4460, q_gen_4554) -> q_gen_4553
<z, cons, nil>(q_gen_4463, q_gen_4556) -> q_gen_4555
<s, cons, cons>(q_gen_4544, q_gen_4481) -> q_gen_4557
<s, cons, cons>(q_gen_4474, q_gen_4559) -> q_gen_4558
<s, cons, cons>(q_gen_4544, q_gen_4561) -> q_gen_4560
<s, cons, cons>(q_gen_4499, q_gen_4566) -> q_gen_4565
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4568
<s, cons, cons>(q_gen_4538, q_gen_4570) -> q_gen_4569
<s, cons, cons>(q_gen_4474, q_gen_4572) -> q_gen_4571
<s, cons, cons>(q_gen_4460, q_gen_4574) -> q_gen_4573
<s, cons, cons>(q_gen_4460, q_gen_4567) -> q_gen_4575
<z, cons, nil>(q_gen_4463, q_gen_4532) -> q_gen_4576
<s, cons, cons>(q_gen_4499, q_gen_4559) -> q_gen_4577
<s, cons, cons>(q_gen_4538, q_gen_4579) -> q_gen_4578
<s, cons, cons>(q_gen_4460, q_gen_4581) -> q_gen_4580
<z, cons, nil>(q_gen_4463, q_gen_4583) -> q_gen_4582
<s, cons, cons>(q_gen_4483, q_gen_4585) -> q_gen_4584
<s, cons, cons>(q_gen_4587, q_gen_4493) -> q_gen_4586
<s, a, a>(q_gen_4551) -> q_gen_4587
<s, cons, cons>(q_gen_4538, q_gen_4518) -> q_gen_4588
<s, cons, cons>(q_gen_4538, q_gen_4559) -> q_gen_4589
<s, cons, cons>(q_gen_4460, q_gen_4496) -> q_gen_4590
<s, cons, cons>(q_gen_4472, q_gen_4541) -> q_gen_4591
<s, cons, cons>(q_gen_4460, q_gen_4593) -> q_gen_4592
<z, cons, nil>(q_gen_4463, q_gen_4595) -> q_gen_4594
<s, cons, cons>(q_gen_4460, q_gen_4597) -> q_gen_4596
<z, cons, nil>(q_gen_4463, q_gen_4599) -> q_gen_4598
<s, cons, cons>(q_gen_4499, q_gen_4459) -> q_gen_4600
<s, cons, cons>(q_gen_4460, q_gen_4537) -> q_gen_4601
<z, cons, nil>(q_gen_4470, q_gen_4583) -> q_gen_4602
<s, cons, cons>(q_gen_4460, q_gen_4512) -> q_gen_4603
<s, cons, cons>(q_gen_4538, q_gen_4605) -> q_gen_4604
<s, cons, cons>(q_gen_4499, q_gen_4581) -> q_gen_4607
<s, cons, cons>(q_gen_4483, q_gen_4520) -> q_gen_4608
<s, cons, cons>(q_gen_4544, q_gen_4610) -> q_gen_4609
<s, cons, cons>(q_gen_4460, q_gen_4572) -> q_gen_4611
<z, cons, nil>(q_gen_4463, q_gen_4523) -> q_gen_4612
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.021995 s (model generation: 0.021075,  model checking: 0.000920):

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

-------------------------------------------
Step 1, which took 0.010975 s (model generation: 0.010757,  model checking: 0.000218):

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

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

-------------------------------------------
Step 2, which took 0.013886 s (model generation: 0.013580,  model checking: 0.000306):

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

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

-------------------------------------------
Step 3, which took 0.015605 s (model generation: 0.013754,  model checking: 0.001851):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<nil, nil>() -> q_gen_4459
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, b, b>() -> q_gen_4460
}

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

-------------------------------------------
Step 4, which took 0.012238 s (model generation: 0.011234,  model checking: 0.001004):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<nil>() -> q_gen_4462
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, b, b>() -> q_gen_4460
}

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

-------------------------------------------
Step 5, which took 0.011166 s (model generation: 0.010137,  model checking: 0.001029):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<nil>() -> q_gen_4462
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, b, b>() -> q_gen_4460
}

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

-------------------------------------------
Step 6, which took 0.015308 s (model generation: 0.014140,  model checking: 0.001168):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<nil>() -> q_gen_4462
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
}

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

-------------------------------------------
Step 7, which took 0.013063 s (model generation: 0.011595,  model checking: 0.001468):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
}

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

-------------------------------------------
Step 8, which took 0.016967 s (model generation: 0.015307,  model checking: 0.001660):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<s, b, b>(q_gen_4457) -> q_gen_4460
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
}

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

-------------------------------------------
Step 9, which took 0.015621 s (model generation: 0.013822,  model checking: 0.001799):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<s, a, a>(q_gen_4457) -> q_gen_4460
<s, b, b>(q_gen_4457) -> q_gen_4460
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
}

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([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 8
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 16
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> nil  ;  u -> z  ;  x2 -> b  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 10, which took 0.015617 s (model generation: 0.014205,  model checking: 0.001412):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<s, a, a>(q_gen_4457) -> q_gen_4460
<s, b, b>(q_gen_4457) -> q_gen_4460
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
}

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([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 11
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 16
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, nil)  ;  _xq -> cons(b, nil)  ;  n -> s(z)  ;  x -> b  ;  xs -> cons(b, nil)
})

-------------------------------------------
Step 11, which took 0.021686 s (model generation: 0.016196,  model checking: 0.005490):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4472, q_gen_4477, q_gen_4478},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
}

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([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 12
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 19
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(a, nil)  ;  u -> s(s(z))  ;  x2 -> a  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 12, which took 0.024586 s (model generation: 0.021355,  model checking: 0.003231):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4467, q_gen_4477, q_gen_4478, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<a, a>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4467, q_gen_4459) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<s, a, a>(q_gen_4457) -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, b, b>(q_gen_4457) -> q_gen_4467
<z, a, a>() -> q_gen_4467
<s, cons, cons>(q_gen_4467, q_gen_4477) -> q_gen_4478
}

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]) -> 12
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 15
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 19
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(a, nil))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(a, nil)
})

-------------------------------------------
Step 13, which took 0.018733 s (model generation: 0.017620,  model checking: 0.001113):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4470, q_gen_4474, q_gen_4478, q_gen_4479, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4470, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<b>() -> q_gen_4463
<a>() -> q_gen_4470
<cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4479
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4479
<a, a>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4479) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<s, b, b>(q_gen_4457) -> q_gen_4460
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4474
<s, cons, cons>(q_gen_4460, q_gen_4479) -> q_gen_4478
}

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]) -> 12
() -> take([z, y, nil]) -> 15
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 15
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 19
}
Sat witness: Found: (() -> take([z, y, nil]), {
y -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 14, which took 0.022626 s (model generation: 0.017946,  model checking: 0.004680):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4470, q_gen_4474, q_gen_4478, q_gen_4479, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<cons>(q_gen_4470, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<b>() -> q_gen_4463
<a>() -> q_gen_4470
<cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4479
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4479
<a, a>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4479) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<s, b, b>(q_gen_4457) -> q_gen_4460
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4474
<s, cons, cons>(q_gen_4460, q_gen_4479) -> q_gen_4478
}

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]) -> 13
() -> take([z, y, nil]) -> 15
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 18
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 19
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(a, nil)  ;  _xq -> cons(a, nil)  ;  n -> s(s(z))  ;  x -> a  ;  xs -> cons(a, nil)
})

-------------------------------------------
Step 15, which took 0.025666 s (model generation: 0.021631,  model checking: 0.004035):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4467, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4467, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4467, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4467
<s, b, b>(q_gen_4457) -> q_gen_4467
<z, a, a>() -> q_gen_4467
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4467, q_gen_4477) -> q_gen_4478
}

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]) -> 14
() -> take([z, y, nil]) -> 16
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 21
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 19
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(a, cons(a, nil))  ;  _xq -> nil  ;  n -> z  ;  x -> a  ;  xs -> cons(a, nil)
})

-------------------------------------------
Step 16, which took 0.024550 s (model generation: 0.021122,  model checking: 0.003428):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
}

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]) -> 15
() -> take([z, y, nil]) -> 17
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 21
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 22
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(b, nil)  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 17, which took 0.024635 s (model generation: 0.023672,  model checking: 0.000963):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4469, q_gen_4470, q_gen_4475, q_gen_4477, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<nil>() -> q_gen_4462
<b>() -> q_gen_4463
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4469
<cons>(q_gen_4470, q_gen_4462) -> q_gen_4469
<a>() -> q_gen_4470
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4477
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4469) -> q_gen_4455
<z, cons, nil>(q_gen_4470, q_gen_4469) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<s, a, a>(q_gen_4457) -> q_gen_4460
<s, b, b>(q_gen_4457) -> q_gen_4460
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4475
<z, cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4475
}

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]) -> 16
() -> take([z, y, nil]) -> 20
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 21
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 22
}
Sat witness: Found: (() -> take([z, y, nil]), {
y -> cons(a, nil)
})

-------------------------------------------
Step 18, which took 0.026959 s (model generation: 0.022659,  model checking: 0.004300):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
}

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]) -> 17
() -> take([z, y, nil]) -> 21
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 24
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 22
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(a, nil))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 19, which took 0.030225 s (model generation: 0.024682,  model checking: 0.005543):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
}

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]) -> 18
() -> take([z, y, nil]) -> 22
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 24
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 25
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(b, cons(a, nil))  ;  u -> s(s(z))  ;  x2 -> b  ;  x3 -> cons(b, cons(a, cons(a, nil)))
})

-------------------------------------------
Step 20, which took 0.032527 s (model generation: 0.028029,  model checking: 0.004498):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
}

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]) -> 19
() -> take([z, y, nil]) -> 23
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 27
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 25
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(a, cons(a, nil)))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 21, which took 0.052715 s (model generation: 0.034427,  model checking: 0.018288):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
}

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]) -> 20
() -> take([z, y, nil]) -> 24
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 30
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 26
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(a, cons(a, cons(a, nil))))  ;  _xq -> cons(a, cons(a, nil))  ;  n -> s(s(z))  ;  x -> b  ;  xs -> cons(a, cons(a, cons(a, nil)))
})

-------------------------------------------
Step 22, which took 0.040020 s (model generation: 0.038467,  model checking: 0.001553):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4470, q_gen_4474, q_gen_4477, q_gen_4478, q_gen_4479, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<cons>(q_gen_4470, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<b>() -> q_gen_4463
<a>() -> q_gen_4470
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4477
<cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4479
<cons, cons>(q_gen_4482, q_gen_4479) -> q_gen_4479
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4479
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4479) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<s, b, b>(q_gen_4457) -> q_gen_4460
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4474
<s, cons, cons>(q_gen_4460, q_gen_4479) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4477) -> q_gen_4478
}

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]) -> 21
() -> take([z, y, nil]) -> 25
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 30
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 29
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> nil  ;  u -> z  ;  x2 -> b  ;  x3 -> cons(b, nil)
})

-------------------------------------------
Step 23, which took 0.043170 s (model generation: 0.040350,  model checking: 0.002820):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4498},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
}

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]) -> 22
() -> take([z, y, nil]) -> 26
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 30
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 32
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(b, cons(b, cons(a, nil)))  ;  u -> s(s(z))  ;  x2 -> b  ;  x3 -> cons(b, cons(b, cons(a, cons(a, nil))))
})

-------------------------------------------
Step 24, which took 0.049990 s (model generation: 0.049534,  model checking: 0.000456):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<s, a, a>(q_gen_4457) -> q_gen_4460
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4465) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4465) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
}

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]) -> 25
() -> take([z, y, nil]) -> 26
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 30
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 32
}
Sat witness: Found: (() -> take([s(u), nil, nil]), {
u -> s(s(z))
})

-------------------------------------------
Step 25, which took 0.057221 s (model generation: 0.050769,  model checking: 0.006452):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<s, a, a>(q_gen_4457) -> q_gen_4460
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4465) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4465) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
}

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]) -> 26
() -> take([z, y, nil]) -> 27
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 33
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 32
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(a, nil)  ;  _xq -> cons(b, nil)  ;  n -> s(z)  ;  x -> a  ;  xs -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 26, which took 0.057721 s (model generation: 0.055435,  model checking: 0.002286):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4467, q_gen_4474, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4490},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4490
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4467, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4467, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, b, b>() -> q_gen_4460
<s, b, b>(q_gen_4457) -> q_gen_4467
<z, a, a>() -> q_gen_4467
<s, a, a>(q_gen_4457) -> q_gen_4474
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4467, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4467, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4490) -> q_gen_4478
}

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]) -> 27
() -> take([z, y, nil]) -> 28
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 33
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 35
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> nil  ;  u -> z  ;  x2 -> a  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 27, which took 0.065149 s (model generation: 0.059286,  model checking: 0.005863):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4490, q_gen_4491},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
}

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]) -> 28
() -> take([z, y, nil]) -> 29
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 36
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 35
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(b, cons(a, nil)))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 28, which took 0.068576 s (model generation: 0.064904,  model checking: 0.003672):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4490, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
}

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]) -> 29
() -> take([z, y, nil]) -> 30
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 36
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 38
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(b, cons(b, nil))  ;  u -> s(s(z))  ;  x2 -> b  ;  x3 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 29, which took 0.086889 s (model generation: 0.078848,  model checking: 0.008041):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4490, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
}

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]) -> 30
() -> take([z, y, nil]) -> 31
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 39
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 38
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(a, cons(a, cons(a, nil))))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(a, cons(a, cons(a, nil)))
})

-------------------------------------------
Step 30, which took 0.093904 s (model generation: 0.089949,  model checking: 0.003955):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4491, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
}

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]) -> 31
() -> take([z, y, nil]) -> 32
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 39
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 41
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(a, cons(a, nil))  ;  u -> s(s(z))  ;  x2 -> a  ;  x3 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 31, which took 0.115112 s (model generation: 0.104760,  model checking: 0.010352):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4472, q_gen_4474, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4490},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4457) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4490
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4490) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, a, a>(q_gen_4457) -> q_gen_4474
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4477) -> q_gen_4478
}

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]) -> 32
() -> take([z, y, nil]) -> 33
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 42
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 41
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(a, cons(a, cons(a, nil)))  ;  _xq -> cons(a, nil)  ;  n -> s(z)  ;  x -> a  ;  xs -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 32, which took 0.112908 s (model generation: 0.110998,  model checking: 0.001910):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4469, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4469) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4469
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4481
<cons, nil>(q_gen_4463, q_gen_4469) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4469) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<s, a, a>(q_gen_4457) -> q_gen_4460
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4465) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4465) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
}

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]) -> 33
() -> take([z, y, nil]) -> 34
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 42
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 44
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(a, nil)  ;  u -> s(z)  ;  x2 -> a  ;  x3 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 33, which took 0.228604 s (model generation: 0.220727,  model checking: 0.007877):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4465) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<s, b, b>(q_gen_4465) -> q_gen_4460
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
}

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]) -> 34
() -> take([z, y, nil]) -> 35
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 45
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 44
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(a, cons(a, nil)))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(a, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 34, which took 0.158856 s (model generation: 0.155781,  model checking: 0.003075):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4490
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4465) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
}

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]) -> 35
() -> take([z, y, nil]) -> 36
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 45
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 47
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(a, nil)  ;  u -> s(s(z))  ;  x2 -> b  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 35, which took 0.450598 s (model generation: 0.437639,  model checking: 0.012959):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4474, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4491, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4465) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, a, a>(q_gen_4457) -> q_gen_4474
<s, b, b>(q_gen_4465) -> q_gen_4474
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4501) -> q_gen_4478
}

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]) -> 36
() -> take([z, y, nil]) -> 37
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 48
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 47
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(b, nil))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(b, nil)
})

-------------------------------------------
Step 36, which took 0.322221 s (model generation: 0.319032,  model checking: 0.003189):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4467, q_gen_4470, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4479, q_gen_4481, q_gen_4482},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<cons>(q_gen_4470, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<a>() -> q_gen_4470
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4479
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4479) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4479) -> q_gen_4455
<s, cons, cons>(q_gen_4467, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4467, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4467
<z, a, a>() -> q_gen_4467
<s, a, a>(q_gen_4465) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4465) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4467, q_gen_4479) -> q_gen_4478
<s, cons, cons>(q_gen_4467, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4479) -> q_gen_4478
}

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]) -> 37
() -> take([z, y, nil]) -> 38
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 48
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 50
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> nil  ;  u -> z  ;  x2 -> a  ;  x3 -> cons(b, nil)
})

-------------------------------------------
Step 37, which took 0.258178 s (model generation: 0.256860,  model checking: 0.001318):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4470, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4479, q_gen_4481, q_gen_4482, q_gen_4486},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4470, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<a>() -> q_gen_4470
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4486
<cons>(q_gen_4470, q_gen_4486) -> q_gen_4486
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4482, q_gen_4479) -> q_gen_4477
<cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4479
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4481
<cons, nil>(q_gen_4463, q_gen_4486) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4479) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4486) -> q_gen_4455
<z, cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<s, a, a>(q_gen_4457) -> q_gen_4460
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4465) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4465) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4479) -> q_gen_4478
<z, cons, nil>(q_gen_4470, q_gen_4486) -> q_gen_4478
}

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]) -> 38
() -> take([z, y, nil]) -> 41
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 48
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 50
}
Sat witness: Found: (() -> take([z, y, nil]), {
y -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 38, which took 0.175979 s (model generation: 0.159488,  model checking: 0.016491):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4501) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 39
() -> take([z, y, nil]) -> 42
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 51
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 50
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(a, cons(b, cons(a, nil)))  ;  _xq -> cons(b, cons(a, cons(b, nil)))  ;  n -> s(s(s(z)))  ;  x -> a  ;  xs -> cons(b, cons(a, cons(b, cons(b, nil))))
})

-------------------------------------------
Step 39, which took 0.266527 s (model generation: 0.263131,  model checking: 0.003396):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4474, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4490, q_gen_4491},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4465) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4465) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, a, a>(q_gen_4457) -> q_gen_4474
<s, b, b>(q_gen_4465) -> q_gen_4474
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4490) -> q_gen_4478
}

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]) -> 40
() -> take([z, y, nil]) -> 43
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 51
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 53
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(b, nil)  ;  u -> s(z)  ;  x2 -> a  ;  x3 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 40, which took 0.316534 s (model generation: 0.301123,  model checking: 0.015411):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4498, q_gen_4503},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4465) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4503
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4503) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4503) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 41
() -> take([z, y, nil]) -> 44
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 54
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 53
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(a, nil))  ;  _xq -> cons(a, cons(b, nil))  ;  n -> s(s(s(z)))  ;  x -> b  ;  xs -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 41, which took 0.370650 s (model generation: 0.367386,  model checking: 0.003264):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4491, q_gen_4493, q_gen_4498},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4465) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4459
<cons, cons>(q_gen_4491, q_gen_4498) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4493
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4493) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4493) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4493) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4493) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4493) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 42
() -> take([z, y, nil]) -> 45
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 54
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 56
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> nil  ;  u -> s(s(z))  ;  x2 -> a  ;  x3 -> nil
})

-------------------------------------------
Step 42, which took 0.403744 s (model generation: 0.389370,  model checking: 0.014374):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4491, q_gen_4493, q_gen_4498},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4465) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4491, q_gen_4498) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4493) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4493
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4493) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4493) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4493) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4493) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 43
() -> take([z, y, nil]) -> 46
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 57
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 56
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(b, nil))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 43, which took 0.454463 s (model generation: 0.446605,  model checking: 0.007858):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4469, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4498},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4469) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4469
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, nil>(q_gen_4463, q_gen_4469) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4469) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 44
() -> take([z, y, nil]) -> 47
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 57
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 59
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(b, nil)  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(b, nil)
})

-------------------------------------------
Step 44, which took 0.542738 s (model generation: 0.429247,  model checking: 0.113491):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4491, q_gen_4493, q_gen_4498},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4465) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4493
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4493) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4493) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4498) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4493) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4493) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4493) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 45
() -> take([z, y, nil]) -> 48
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 60
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 59
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(b, nil))  ;  _xq -> cons(b, cons(a, nil))  ;  n -> s(s(z))  ;  x -> b  ;  xs -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 45, which took 0.268144 s (model generation: 0.267563,  model checking: 0.000581):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4498, q_gen_4510},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4510
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<s, nil, nil>(q_gen_4510) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<s, b, b>(q_gen_4510) -> q_gen_4460
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, a, a>(q_gen_4510) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 48
() -> take([z, y, nil]) -> 48
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 60
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 59
}
Sat witness: Found: (() -> take([s(u), nil, nil]), {
u -> s(s(s(z)))
})

-------------------------------------------
Step 46, which took 0.601228 s (model generation: 0.595600,  model checking: 0.005628):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4474, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4490, q_gen_4498, q_gen_4499},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4465) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, a, a>(q_gen_4457) -> q_gen_4474
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4490) -> q_gen_4478
<s, b, b>(q_gen_4465) -> q_gen_4499
}

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]) -> 49
() -> take([z, y, nil]) -> 49
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 60
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 62
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(b, nil)  ;  u -> s(z)  ;  x2 -> a  ;  x3 -> cons(b, nil)
})

-------------------------------------------
Step 47, which took 0.597674 s (model generation: 0.581453,  model checking: 0.016221):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4501) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 50
() -> take([z, y, nil]) -> 50
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 63
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 62
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(b, cons(a, cons(a, cons(a, nil)))))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(b, cons(a, cons(a, cons(a, nil))))
})

-------------------------------------------
Step 48, which took 0.335083 s (model generation: 0.331039,  model checking: 0.004044):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4498},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4465) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4491, q_gen_4498) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 51
() -> take([z, y, nil]) -> 51
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 63
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 65
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(a, nil)  ;  u -> s(s(s(z)))  ;  x2 -> b  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 49, which took 0.705193 s (model generation: 0.688021,  model checking: 0.017172):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4501) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 52
() -> take([z, y, nil]) -> 52
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 66
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 65
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(a, cons(a, cons(b, nil)))  ;  _xq -> cons(a, nil)  ;  n -> s(z)  ;  x -> a  ;  xs -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 50, which took 0.738684 s (model generation: 0.734301,  model checking: 0.004383):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<s>(q_gen_4465) -> q_gen_4457
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4501) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 53
() -> take([z, y, nil]) -> 53
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 66
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 68
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(b, nil)  ;  u -> s(s(z))  ;  x2 -> a  ;  x3 -> cons(b, nil)
})

-------------------------------------------
Step 51, which took 0.848065 s (model generation: 0.781336,  model checking: 0.066729):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4501) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 54
() -> take([z, y, nil]) -> 54
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 69
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 68
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  _xq -> cons(b, cons(b, cons(b, cons(a, nil))))  ;  n -> s(s(s(z)))  ;  x -> b  ;  xs -> cons(b, cons(b, cons(b, cons(a, cons(b, nil)))))
})

-------------------------------------------
Step 52, which took 1.020043 s (model generation: 1.010460,  model checking: 0.009583):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4498},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4491, q_gen_4498) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 55
() -> take([z, y, nil]) -> 55
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 69
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 71
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(a, cons(b, cons(a, nil)))  ;  u -> s(s(s(z)))  ;  x2 -> a  ;  x3 -> cons(a, cons(b, cons(a, cons(a, nil))))
})

-------------------------------------------
Step 53, which took 1.083663 s (model generation: 1.027797,  model checking: 0.055866):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4498, q_gen_4510},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4510
<s>(q_gen_4510) -> q_gen_4510
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<s, nil, nil>(q_gen_4510) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, a, a>(q_gen_4510) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4510) -> q_gen_4483
}

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]) -> 56
() -> take([z, y, nil]) -> 56
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 72
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 71
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(a, cons(b, cons(a, cons(a, nil))))  ;  _xq -> cons(b, nil)  ;  n -> s(z)  ;  x -> a  ;  xs -> cons(b, cons(a, cons(a, nil)))
})

-------------------------------------------
Step 54, which took 1.224565 s (model generation: 1.216385,  model checking: 0.008180):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4493, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4477
<cons, cons>(q_gen_4491, q_gen_4501) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4493) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4493) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4493) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4501) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4493) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4493) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 57
() -> take([z, y, nil]) -> 57
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 72
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 74
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(a, nil)  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 55, which took 1.134290 s (model generation: 1.110844,  model checking: 0.023446):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4474, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4490, q_gen_4491, q_gen_4499, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4501) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4501
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4465) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, a, a>(q_gen_4457) -> q_gen_4474
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4501) -> q_gen_4478
<s, b, b>(q_gen_4465) -> q_gen_4499
}

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]) -> 58
() -> take([z, y, nil]) -> 58
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 75
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 74
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(b, cons(a, nil)))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(b, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 56, which took 1.657993 s (model generation: 1.638545,  model checking: 0.019448):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4498, q_gen_4499},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4491, q_gen_4498) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4490) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4499
}

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]) -> 59
() -> take([z, y, nil]) -> 59
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 75
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 77
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(b, cons(a, cons(b, nil)))  ;  u -> s(s(s(z)))  ;  x2 -> a  ;  x3 -> cons(b, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 57, which took 1.203066 s (model generation: 1.179728,  model checking: 0.023338):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4474, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4490, q_gen_4491, q_gen_4498, q_gen_4499},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4491, q_gen_4498) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4474, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4465) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, a, a>(q_gen_4457) -> q_gen_4474
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4474, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4490) -> q_gen_4478
<s, b, b>(q_gen_4465) -> q_gen_4499
}

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]) -> 60
() -> take([z, y, nil]) -> 60
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 78
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 77
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 58, which took 2.038139 s (model generation: 2.007992,  model checking: 0.030147):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4498, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4491, q_gen_4498) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4501
<cons, cons>(q_gen_4491, q_gen_4501) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4501) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 61
() -> take([z, y, nil]) -> 61
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 78
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 80
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(a, cons(b, nil))  ;  u -> s(s(z))  ;  x2 -> a  ;  x3 -> cons(a, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 59, which took 1.787829 s (model generation: 1.756846,  model checking: 0.030983):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4469, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4498, q_gen_4510},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4469
<cons>(q_gen_4463, q_gen_4469) -> q_gen_4469
<s>(q_gen_4465) -> q_gen_4510
<s>(q_gen_4510) -> q_gen_4510
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4498
<cons, nil>(q_gen_4463, q_gen_4469) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<s, nil, nil>(q_gen_4510) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4469) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, a, a>(q_gen_4510) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4510) -> q_gen_4483
}

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]) -> 62
() -> take([z, y, nil]) -> 62
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 81
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 80
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(a, cons(a, nil))  ;  _xq -> cons(a, cons(b, nil))  ;  n -> s(s(s(s(z))))  ;  x -> a  ;  xs -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 60, which took 2.429884 s (model generation: 2.424476,  model checking: 0.005408):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4469, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4498, q_gen_4510},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4469) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4510) -> q_gen_4465
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4469
<s>(q_gen_4465) -> q_gen_4510
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4498
<cons, nil>(q_gen_4463, q_gen_4469) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<s, nil, nil>(q_gen_4510) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4469) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, a, a>(q_gen_4510) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4510) -> q_gen_4483
}

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]) -> 63
() -> take([z, y, nil]) -> 63
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 81
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 83
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(a, cons(b, nil))  ;  u -> s(s(s(z)))  ;  x2 -> a  ;  x3 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 61, which took 2.943548 s (model generation: 2.906035,  model checking: 0.037513):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4470, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4479, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4491, q_gen_4493, q_gen_4498},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<cons>(q_gen_4470, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<a>() -> q_gen_4470
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4477
<cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4479
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4479
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4479) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4493) -> q_gen_4493
<cons, cons>(q_gen_4491, q_gen_4493) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4479) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4498) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4479) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4493) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4479) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4493) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4479) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4493) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 64
() -> take([z, y, nil]) -> 64
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 84
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 83
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(a, nil))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 62, which took 2.270434 s (model generation: 2.247316,  model checking: 0.023118):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4470, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4479, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4491, q_gen_4493, q_gen_4496},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<cons>(q_gen_4470, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<a>() -> q_gen_4470
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4477
<cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4479
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4479) -> q_gen_4493
<cons, cons>(q_gen_4491, q_gen_4493) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4496
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4496
<cons, cons>(q_gen_4482, q_gen_4493) -> q_gen_4496
<cons, cons>(q_gen_4482, q_gen_4496) -> q_gen_4496
<cons, cons>(q_gen_4491, q_gen_4479) -> q_gen_4496
<cons, cons>(q_gen_4491, q_gen_4496) -> q_gen_4496
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4479) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4493) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4496) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4493) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4496) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4479) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4496) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4493) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 65
() -> take([z, y, nil]) -> 65
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 84
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 86
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(b, nil)  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 63, which took 2.304628 s (model generation: 2.270953,  model checking: 0.033675):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4470, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4479, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4491, q_gen_4493, q_gen_4496},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<cons>(q_gen_4470, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<a>() -> q_gen_4470
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4477
<cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4479
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4496) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4479) -> q_gen_4481
<a, a>() -> q_gen_4482
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4479) -> q_gen_4493
<cons, cons>(q_gen_4491, q_gen_4493) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4496
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4496
<cons, cons>(q_gen_4482, q_gen_4493) -> q_gen_4496
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4496
<cons, cons>(q_gen_4491, q_gen_4496) -> q_gen_4496
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4479) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4493) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4496) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4493) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4496) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4479) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4496) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4493) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 66
() -> take([z, y, nil]) -> 66
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 87
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 86
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(b, cons(b, nil)))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(b, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 64, which took 3.034053 s (model generation: 3.008106,  model checking: 0.025947):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4470, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4479, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4496},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<cons>(q_gen_4470, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<a>() -> q_gen_4470
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4479
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4496) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4479) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4479) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4496
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4496
<cons, cons>(q_gen_4491, q_gen_4496) -> q_gen_4496
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4479) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4496) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4470, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4496) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4479) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4496) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 67
() -> take([z, y, nil]) -> 67
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 87
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 89
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(a, nil)  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 65, which took 2.707836 s (model generation: 2.680348,  model checking: 0.027488):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4498, q_gen_4499, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<cons, cons>(q_gen_4491, q_gen_4498) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4501) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4501) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4459) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4501) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4499
}

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]) -> 68
() -> take([z, y, nil]) -> 68
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 90
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 89
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(b, cons(b, cons(a, cons(a, nil)))))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(b, cons(b, cons(a, cons(a, nil))))
})

-------------------------------------------
Step 66, which took 3.660164 s (model generation: 3.653804,  model checking: 0.006360):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4493, q_gen_4498, q_gen_4499},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4493) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4493) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4498) -> q_gen_4498
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4493) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4493) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4493) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4459) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4493) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4499
}

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]) -> 69
() -> take([z, y, nil]) -> 69
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 90
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 92
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> nil  ;  u -> s(s(z))  ;  x2 -> b  ;  x3 -> nil
})

-------------------------------------------
Step 67, which took 3.543369 s (model generation: 3.514638,  model checking: 0.028731):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4469, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4501, q_gen_4512},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4469) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4469
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4482, q_gen_4512) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<cons, cons>(q_gen_4491, q_gen_4501) -> q_gen_4501
<cons, cons>(q_gen_4491, q_gen_4512) -> q_gen_4512
<cons, nil>(q_gen_4463, q_gen_4469) -> q_gen_4512
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4512) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4501) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4469) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4512) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4512) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 70
() -> take([z, y, nil]) -> 70
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 93
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 92
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(a, nil))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(a, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 68, which took 2.378443 s (model generation: 2.369320,  model checking: 0.009123):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4469, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4501, q_gen_4503},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4469
<cons>(q_gen_4463, q_gen_4469) -> q_gen_4469
<cons, cons>(q_gen_4491, q_gen_4501) -> q_gen_4459
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4501
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4503
<cons, cons>(q_gen_4482, q_gen_4503) -> q_gen_4503
<cons, cons>(q_gen_4491, q_gen_4503) -> q_gen_4503
<cons, nil>(q_gen_4463, q_gen_4469) -> q_gen_4503
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4501) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4469) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4503) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4503) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4503) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4483
}

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]) -> 71
() -> take([z, y, nil]) -> 71
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 93
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 95
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> nil  ;  u -> z  ;  x2 -> b  ;  x3 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 69, which took 5.605672 s (model generation: 5.559563,  model checking: 0.046109):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4498, q_gen_4499, q_gen_4503},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4503
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4503
<cons, cons>(q_gen_4491, q_gen_4498) -> q_gen_4503
<cons, cons>(q_gen_4491, q_gen_4503) -> q_gen_4503
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4503) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4503) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4503) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4503) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4499
}

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]) -> 72
() -> take([z, y, nil]) -> 72
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 96
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 95
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(a, cons(b, cons(b, cons(b, nil))))  ;  _xq -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  n -> s(s(s(z)))  ;  x -> a  ;  xs -> cons(b, cons(b, cons(b, cons(b, nil))))
})

-------------------------------------------
Step 70, which took 5.221398 s (model generation: 5.213132,  model checking: 0.008266):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4493, q_gen_4499, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4491, q_gen_4501) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4493) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4493) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4493
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4493) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4501) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4481) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4493) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4493) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4493) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4501) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4499
}

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]) -> 73
() -> take([z, y, nil]) -> 73
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 96
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 98
}
Sat witness: Found: ((take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]), {
_rq -> cons(a, cons(b, cons(b, nil)))  ;  u -> s(s(s(z)))  ;  x2 -> b  ;  x3 -> cons(a, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 71, which took 3.065901 s (model generation: 3.029272,  model checking: 0.036629):

Model:
|_
{
take -> 
{{{
Q={q_gen_4455, q_gen_4457, q_gen_4459, q_gen_4460, q_gen_4462, q_gen_4463, q_gen_4465, q_gen_4472, q_gen_4477, q_gen_4478, q_gen_4481, q_gen_4482, q_gen_4483, q_gen_4490, q_gen_4491, q_gen_4498, q_gen_4499, q_gen_4501},
Q_f={q_gen_4455},
Delta=
{
<z>() -> q_gen_4457
<cons>(q_gen_4463, q_gen_4462) -> q_gen_4462
<nil>() -> q_gen_4462
<a>() -> q_gen_4463
<b>() -> q_gen_4463
<s>(q_gen_4457) -> q_gen_4465
<s>(q_gen_4465) -> q_gen_4465
<nil, nil>() -> q_gen_4459
<cons, cons>(q_gen_4491, q_gen_4501) -> q_gen_4477
<cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4477
<cons, cons>(q_gen_4482, q_gen_4459) -> q_gen_4481
<cons, cons>(q_gen_4482, q_gen_4490) -> q_gen_4481
<cons, cons>(q_gen_4491, q_gen_4459) -> q_gen_4481
<a, a>() -> q_gen_4482
<cons, cons>(q_gen_4482, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4498) -> q_gen_4490
<cons, cons>(q_gen_4482, q_gen_4501) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4477) -> q_gen_4490
<cons, cons>(q_gen_4491, q_gen_4498) -> q_gen_4490
<b, b>() -> q_gen_4491
<cons, cons>(q_gen_4491, q_gen_4481) -> q_gen_4498
<cons, cons>(q_gen_4491, q_gen_4490) -> q_gen_4498
<cons, cons>(q_gen_4482, q_gen_4481) -> q_gen_4501
<s, cons, cons>(q_gen_4460, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4460, q_gen_4477) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4472, q_gen_4490) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4483, q_gen_4501) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4459) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4481) -> q_gen_4455
<s, cons, cons>(q_gen_4499, q_gen_4498) -> q_gen_4455
<s, nil, nil>(q_gen_4457) -> q_gen_4455
<s, nil, nil>(q_gen_4465) -> q_gen_4455
<z, cons, nil>(q_gen_4463, q_gen_4462) -> q_gen_4455
<z, nil, nil>() -> q_gen_4455
<z, a, a>() -> q_gen_4460
<z, b, b>() -> q_gen_4460
<s, a, a>(q_gen_4457) -> q_gen_4472
<s, b, b>(q_gen_4457) -> q_gen_4472
<s, cons, cons>(q_gen_4460, q_gen_4481) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4460, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4472, q_gen_4501) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4477) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4483, q_gen_4498) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4490) -> q_gen_4478
<s, cons, cons>(q_gen_4499, q_gen_4501) -> q_gen_4478
<s, a, a>(q_gen_4465) -> q_gen_4483
<s, b, b>(q_gen_4465) -> q_gen_4499
}

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]) -> 74
() -> take([z, y, nil]) -> 74
(take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]) -> 99
(take([u, x3, _rq])) -> take([s(u), cons(x2, x3), cons(x2, _rq)]) -> 98
}
Sat witness: Found: ((take([n, xs, _xq]) /\ take([s(n), cons(x, xs), _wq])) -> eq_eltlist([_wq, cons(x, _xq)]), {
_wq -> cons(b, cons(b, cons(a, cons(a, nil))))  ;  _xq -> nil  ;  n -> z  ;  x -> b  ;  xs -> cons(b, cons(a, cons(a, nil)))
})

Total time: 64.700635
Reason for stopping: DontKnow. Stopped because: timeout