Solving ../../benchmarks/true/member_equal_nat.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(memberl, P:
{() -> memberl([h1, cons(h1, t1)])
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)])
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1])
(memberl([e, nil])) -> BOT}
)
}

properties:
{(memberl([i, l2])) -> memberl([i, l2])}


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

Clause system for inference is:

{
() -> memberl([h1, cons(h1, t1)]) -> 0  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 0  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 0  ;  (memberl([e, nil])) -> BOT -> 0  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 0
}


Solving took 30.000589 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
memberl -> 
{{{
Q={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_f={},
Delta=
{
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4472
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4475
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<cons>(q_gen_4468, q_gen_4475) -> q_gen_4497
<s>(q_gen_4468) -> q_gen_4505
<cons>(q_gen_4468, q_gen_4509) -> q_gen_4508
<cons>(q_gen_4505, q_gen_4461) -> q_gen_4509
<cons>(q_gen_4462, q_gen_4477) -> q_gen_4513
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4521
<cons>(q_gen_4505, q_gen_4458) -> q_gen_4528
<cons>(q_gen_4459, q_gen_4528) -> q_gen_4530
<cons>(q_gen_4468, q_gen_4477) -> q_gen_4533
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4536
<cons>(q_gen_4462, q_gen_4513) -> q_gen_4539
<cons>(q_gen_4505, q_gen_4477) -> q_gen_4544
<cons>(q_gen_4462, q_gen_4521) -> q_gen_4546
<cons>(q_gen_4468, q_gen_4472) -> q_gen_4548
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4464
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4465
<z, s>(q_gen_4459) -> q_gen_4466
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4467
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4469
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4470
<z, cons>(q_gen_4462, q_gen_4472) -> q_gen_4471
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4473
<z, cons>(q_gen_4462, q_gen_4475) -> q_gen_4474
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4476
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4478
<z, z>() -> q_gen_4479
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4480
<s, nil>(q_gen_4459) -> q_gen_4481
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4482
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4483
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4484
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4485
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4486
<s, cons>(q_gen_4488, q_gen_4463) -> q_gen_4487
<z, s>(q_gen_4462) -> q_gen_4488
<s, cons>(q_gen_4488, q_gen_4469) -> q_gen_4489
<s, cons>(q_gen_4488, q_gen_4464) -> q_gen_4490
<s, cons>(q_gen_4492, q_gen_4481) -> q_gen_4491
<s, s>(q_gen_4466) -> q_gen_4492
<s, cons>(q_gen_4479, q_gen_4494) -> q_gen_4493
<z, cons>(q_gen_4468, q_gen_4475) -> q_gen_4494
<s, cons>(q_gen_4479, q_gen_4496) -> q_gen_4495
<z, cons>(q_gen_4459, q_gen_4497) -> q_gen_4496
<s, cons>(q_gen_4488, q_gen_4457) -> q_gen_4498
<s, cons>(q_gen_4492, q_gen_4486) -> q_gen_4499
<s, cons>(q_gen_4479, q_gen_4501) -> q_gen_4500
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4501
<s, cons>(q_gen_4479, q_gen_4467) -> q_gen_4502
<s, cons>(q_gen_4492, q_gen_4480) -> q_gen_4503
<z, cons>(q_gen_4505, q_gen_4472) -> q_gen_4504
<s, cons>(q_gen_4488, q_gen_4507) -> q_gen_4506
<z, cons>(q_gen_4468, q_gen_4508) -> q_gen_4507
<s, cons>(q_gen_4488, q_gen_4511) -> q_gen_4510
<z, cons>(q_gen_4468, q_gen_4509) -> q_gen_4511
<z, cons>(q_gen_4459, q_gen_4513) -> q_gen_4512
<s, cons>(q_gen_4488, q_gen_4460) -> q_gen_4514
<s, cons>(q_gen_4479, q_gen_4516) -> q_gen_4515
<z, cons>(q_gen_4468, q_gen_4472) -> q_gen_4516
<s, cons>(q_gen_4479, q_gen_4511) -> q_gen_4517
<s, cons>(q_gen_4488, q_gen_4519) -> q_gen_4518
<z, cons>(q_gen_4505, q_gen_4461) -> q_gen_4519
<z, cons>(q_gen_4459, q_gen_4521) -> q_gen_4520
<s, cons>(q_gen_4479, q_gen_4469) -> q_gen_4522
<s, cons>(q_gen_4479, q_gen_4520) -> q_gen_4523
<z, cons>(q_gen_4462, q_gen_4521) -> q_gen_4524
<s, cons>(q_gen_4492, q_gen_4526) -> q_gen_4525
<s, cons>(q_gen_4466, q_gen_4467) -> q_gen_4526
<z, cons>(q_gen_4459, q_gen_4528) -> q_gen_4527
<z, cons>(q_gen_4462, q_gen_4530) -> q_gen_4529
<z, cons>(q_gen_4468, q_gen_4521) -> q_gen_4531
<z, cons>(q_gen_4459, q_gen_4533) -> q_gen_4532
<s, cons>(q_gen_4488, q_gen_4535) -> q_gen_4534
<z, cons>(q_gen_4468, q_gen_4536) -> q_gen_4535
<s, cons>(q_gen_4488, q_gen_4467) -> q_gen_4537
<z, cons>(q_gen_4459, q_gen_4539) -> q_gen_4538
<s, cons>(q_gen_4488, q_gen_4541) -> q_gen_4540
<z, cons>(q_gen_4505, q_gen_4477) -> q_gen_4541
<s, cons>(q_gen_4479, q_gen_4543) -> q_gen_4542
<z, cons>(q_gen_4468, q_gen_4544) -> q_gen_4543
<z, cons>(q_gen_4462, q_gen_4546) -> q_gen_4545
<z, cons>(q_gen_4459, q_gen_4548) -> q_gen_4547
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.003644 s (model generation: 0.003460,  model checking: 0.000184):

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

}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 3  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 1  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 1  ;  (memberl([e, nil])) -> BOT -> 1  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 1
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> nil
})

-------------------------------------------
Step 1, which took 0.005626 s (model generation: 0.004290,  model checking: 0.001336):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459},
Q_f={q_gen_4457},
Delta=
{
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 3  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 4  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 2  ;  (memberl([e, nil])) -> BOT -> 2  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 2
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 2, which took 0.005161 s (model generation: 0.004906,  model checking: 0.000255):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459},
Q_f={q_gen_4457},
Delta=
{
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<s>(q_gen_4459) -> q_gen_4459
<z>() -> q_gen_4459
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 3  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 4  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 5  ;  (memberl([e, nil])) -> BOT -> 3  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 3
}
Sat witness: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> nil
})

-------------------------------------------
Step 3, which took 0.008554 s (model generation: 0.008364,  model checking: 0.000190):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459},
Q_f={q_gen_4457},
Delta=
{
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<s>(q_gen_4459) -> q_gen_4459
<z>() -> q_gen_4459
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, nil>() -> q_gen_4457
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 3  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 4  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 5  ;  (memberl([e, nil])) -> BOT -> 6  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 4
}
Sat witness: Yes: ((memberl([e, nil])) -> BOT, {
e -> z
})

-------------------------------------------
Step 4, which took 0.014036 s (model generation: 0.013353,  model checking: 0.000683):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4461, q_gen_4462, q_gen_4463},
Q_f={q_gen_4457},
Delta=
{
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4463
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 6  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 4  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 5  ;  (memberl([e, nil])) -> BOT -> 6  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 4
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(z)  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.018836 s (model generation: 0.012654,  model checking: 0.006182):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4461, q_gen_4462, q_gen_4463, q_gen_4466},
Q_f={q_gen_4457},
Delta=
{
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4463
<z, s>(q_gen_4459) -> q_gen_4466
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 6  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 7  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 5  ;  (memberl([e, nil])) -> BOT -> 6  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 5
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(s(z))  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 6, which took 0.015880 s (model generation: 0.012941,  model checking: 0.002939):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4461, q_gen_4462, q_gen_4463, q_gen_4466},
Q_f={q_gen_4457},
Delta=
{
<nil>() -> q_gen_4458
<s>(q_gen_4462) -> q_gen_4459
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4463
<z, s>(q_gen_4459) -> q_gen_4466
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 6  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 7  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 8  ;  (memberl([e, nil])) -> BOT -> 6  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 6
}
Sat witness: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(s(z))  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.017012 s (model generation: 0.013515,  model checking: 0.003497):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4461, q_gen_4462, q_gen_4463, q_gen_4466},
Q_f={q_gen_4457},
Delta=
{
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4463
<z, s>(q_gen_4459) -> q_gen_4466
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 9  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 7  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 8  ;  (memberl([e, nil])) -> BOT -> 7  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 7
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 8, which took 0.018175 s (model generation: 0.014071,  model checking: 0.004104):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4461, q_gen_4462, q_gen_4463, q_gen_4466},
Q_f={q_gen_4457},
Delta=
{
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4463
<z, s>(q_gen_4459) -> q_gen_4466
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 9  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 10  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 8  ;  (memberl([e, nil])) -> BOT -> 8  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 8
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(s(z), cons(z, nil))
})

-------------------------------------------
Step 9, which took 0.024404 s (model generation: 0.015183,  model checking: 0.009221):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4461, q_gen_4462, q_gen_4463, q_gen_4466},
Q_f={q_gen_4457},
Delta=
{
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4463
<z, s>(q_gen_4459) -> q_gen_4466
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 12  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 10  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 9  ;  (memberl([e, nil])) -> BOT -> 9  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 9
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(z)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 10, which took 0.026096 s (model generation: 0.014581,  model checking: 0.011515):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4461, q_gen_4462, q_gen_4463, q_gen_4466},
Q_f={q_gen_4457},
Delta=
{
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4463
<z, s>(q_gen_4459) -> q_gen_4466
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 12  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 13  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 10  ;  (memberl([e, nil])) -> BOT -> 10  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 10
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(z, cons(z, nil))
})

-------------------------------------------
Step 11, which took 0.029527 s (model generation: 0.016510,  model checking: 0.013017):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4461, q_gen_4462, q_gen_4463, q_gen_4466},
Q_f={q_gen_4457},
Delta=
{
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4463
<z, s>(q_gen_4459) -> q_gen_4466
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 15  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 13  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 11  ;  (memberl([e, nil])) -> BOT -> 11  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 11
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 12, which took 0.029566 s (model generation: 0.018203,  model checking: 0.011363):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4461, q_gen_4462, q_gen_4463, q_gen_4466},
Q_f={q_gen_4457},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4463
<z, s>(q_gen_4459) -> q_gen_4466
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 15  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 16  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 12  ;  (memberl([e, nil])) -> BOT -> 12  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 12
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(s(z), cons(z, nil))
})

-------------------------------------------
Step 13, which took 0.022235 s (model generation: 0.017540,  model checking: 0.004695):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4461, q_gen_4462, q_gen_4463, q_gen_4466},
Q_f={q_gen_4457},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4463
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4466
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 15  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 16  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 15  ;  (memberl([e, nil])) -> BOT -> 13  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 13
}
Sat witness: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.024465 s (model generation: 0.022016,  model checking: 0.002449):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4461, q_gen_4462, q_gen_4463, q_gen_4466},
Q_f={q_gen_4457},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, nil>(q_gen_4459) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4463
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4466
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 15  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 16  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 15  ;  (memberl([e, nil])) -> BOT -> 16  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 14
}
Sat witness: Yes: ((memberl([e, nil])) -> BOT, {
e -> s(z)
})

-------------------------------------------
Step 15, which took 0.026008 s (model generation: 0.021313,  model checking: 0.004695):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4461, q_gen_4462, q_gen_4463, q_gen_4466, q_gen_4479},
Q_f={q_gen_4457},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4463
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 15  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 16  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 18  ;  (memberl([e, nil])) -> BOT -> 16  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 15
}
Sat witness: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 16, which took 0.026975 s (model generation: 0.022496,  model checking: 0.004479):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4460, q_gen_4461, q_gen_4462, q_gen_4463, q_gen_4466, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4463
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 18  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 16  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 18  ;  (memberl([e, nil])) -> BOT -> 16  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 16
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(z)  ;  t1 -> cons(s(z), cons(z, nil))
})

-------------------------------------------
Step 17, which took 0.028616 s (model generation: 0.022833,  model checking: 0.005783):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4457, q_gen_4458, q_gen_4459, q_gen_4460, q_gen_4461, q_gen_4462, q_gen_4463, q_gen_4466, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4463
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 18  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 19  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 18  ;  (memberl([e, nil])) -> BOT -> 17  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 17
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 18, which took 0.030397 s (model generation: 0.023641,  model checking: 0.006756):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4464
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 18  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 19  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 21  ;  (memberl([e, nil])) -> BOT -> 18  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 18
}
Sat witness: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 19, which took 0.025321 s (model generation: 0.021570,  model checking: 0.003751):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4464
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 21  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 19  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 21  ;  (memberl([e, nil])) -> BOT -> 19  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 19
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(z)  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 20, which took 0.029840 s (model generation: 0.020662,  model checking: 0.009178):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4464
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 21  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 22  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 21  ;  (memberl([e, nil])) -> BOT -> 20  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 20
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> s(s(z))  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 21, which took 0.035262 s (model generation: 0.024419,  model checking: 0.010843):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, nil>() -> q_gen_4464
<z, s>(q_gen_4459) -> q_gen_4466
<z, s>(q_gen_4462) -> q_gen_4479
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 21  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 22  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 24  ;  (memberl([e, nil])) -> BOT -> 21  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 21
}
Sat witness: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(z)  ;  h1 -> s(s(z))  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 22, which took 0.027724 s (model generation: 0.022846,  model checking: 0.004878):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<s, nil>(q_gen_4459) -> q_gen_4464
<z, nil>() -> q_gen_4464
<z, s>(q_gen_4459) -> q_gen_4466
<z, s>(q_gen_4462) -> q_gen_4466
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 24  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 22  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 24  ;  (memberl([e, nil])) -> BOT -> 22  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 22
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(s(z))  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 0.030050 s (model generation: 0.025724,  model checking: 0.004326):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<z, nil>() -> q_gen_4464
<z, s>(q_gen_4459) -> q_gen_4466
<z, s>(q_gen_4462) -> q_gen_4466
<s, s>(q_gen_4466) -> q_gen_4479
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 24  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 25  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 24  ;  (memberl([e, nil])) -> BOT -> 23  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 23
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(z, cons(s(s(z)), cons(z, cons(z, nil))))
})

-------------------------------------------
Step 24, which took 0.034838 s (model generation: 0.027035,  model checking: 0.007803):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<z, nil>() -> q_gen_4464
<z, s>(q_gen_4459) -> q_gen_4466
<z, s>(q_gen_4462) -> q_gen_4466
<s, s>(q_gen_4466) -> q_gen_4479
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 24  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 25  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 27  ;  (memberl([e, nil])) -> BOT -> 24  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 24
}
Sat witness: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(z)  ;  h1 -> s(s(z))  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 25, which took 0.035676 s (model generation: 0.026168,  model checking: 0.009508):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4460
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<z, s>(q_gen_4459) -> q_gen_4466
<s, s>(q_gen_4466) -> q_gen_4479
<z, s>(q_gen_4462) -> q_gen_4479
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 27  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 25  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 27  ;  (memberl([e, nil])) -> BOT -> 25  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 25
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(s(z))  ;  t1 -> cons(s(z), cons(s(z), nil))
})

-------------------------------------------
Step 26, which took 0.068711 s (model generation: 0.020021,  model checking: 0.048690):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<z, s>(q_gen_4459) -> q_gen_4466
<s, s>(q_gen_4466) -> q_gen_4479
<z, s>(q_gen_4462) -> q_gen_4479
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 27  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 28  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 27  ;  (memberl([e, nil])) -> BOT -> 26  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 26
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(s(s(z)), cons(s(z), nil))
})

-------------------------------------------
Step 27, which took 0.073813 s (model generation: 0.021826,  model checking: 0.051987):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4479, q_gen_4488},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4462
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4464) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4457) -> q_gen_4464
<z, nil>() -> q_gen_4464
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
<s, s>(q_gen_4466) -> q_gen_4488
<z, s>(q_gen_4462) -> q_gen_4488
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 27  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 28  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 30  ;  (memberl([e, nil])) -> BOT -> 27  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 27
}
Sat witness: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(s(s(z)), cons(z, nil))
})

-------------------------------------------
Step 28, which took 0.062595 s (model generation: 0.023040,  model checking: 0.039555):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4477, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<z, s>(q_gen_4459) -> q_gen_4466
<s, s>(q_gen_4466) -> q_gen_4479
<z, s>(q_gen_4462) -> q_gen_4479
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 30  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 28  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 30  ;  (memberl([e, nil])) -> BOT -> 28  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 28
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(s(z))  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 29, which took 0.296180 s (model generation: 0.024443,  model checking: 0.271737):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4477, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, s>(q_gen_4462) -> q_gen_4479
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 30  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 31  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 30  ;  (memberl([e, nil])) -> BOT -> 29  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 29
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(s(s(z)))  ;  t1 -> cons(s(z), cons(z, nil))
})

-------------------------------------------
Step 30, which took 0.128755 s (model generation: 0.027460,  model checking: 0.101295):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4477, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4468) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4477
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, s>(q_gen_4462) -> q_gen_4479
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 30  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 31  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 33  ;  (memberl([e, nil])) -> BOT -> 30  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 30
}
Sat witness: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(z)  ;  h1 -> s(s(z))  ;  t1 -> cons(s(s(z)), cons(s(s(z)), cons(s(s(s(z))), cons(z, nil))))
})

-------------------------------------------
Step 31, which took 0.281383 s (model generation: 0.034299,  model checking: 0.247084):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4477, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4458
<nil>() -> q_gen_4458
<s>(q_gen_4468) -> q_gen_4459
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, s>(q_gen_4462) -> q_gen_4479
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 33  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 31  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 33  ;  (memberl([e, nil])) -> BOT -> 31  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 31
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(s(z), cons(s(z), nil))
})

-------------------------------------------
Step 32, which took 0.091063 s (model generation: 0.037108,  model checking: 0.053955):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4479, q_gen_4488},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4458
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<s>(q_gen_4468) -> q_gen_4468
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4464) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4460
<s, cons>(q_gen_4488, q_gen_4460) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4463
<s, cons>(q_gen_4488, q_gen_4457) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, nil>(q_gen_4459) -> q_gen_4464
<z, nil>() -> q_gen_4464
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
<s, s>(q_gen_4466) -> q_gen_4488
<z, s>(q_gen_4462) -> q_gen_4488
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 33  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 34  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 33  ;  (memberl([e, nil])) -> BOT -> 32  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 32
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(s(s(z)), cons(s(z), cons(z, nil)))
})

-------------------------------------------
Step 33, which took 0.790077 s (model generation: 0.043365,  model checking: 0.746712):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4479, q_gen_4488},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4458
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<s>(q_gen_4468) -> q_gen_4468
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4464) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4460) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
<z, s>(q_gen_4462) -> q_gen_4488
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 33  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 34  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 36  ;  (memberl([e, nil])) -> BOT -> 33  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 33
}
Sat witness: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(s(s(z)), cons(s(s(s(z))), cons(z, nil)))
})

-------------------------------------------
Step 34, which took 0.728998 s (model generation: 0.052509,  model checking: 0.676489):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4479, q_gen_4488},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4468) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4464) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4463
<s, cons>(q_gen_4488, q_gen_4457) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4460) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
<z, s>(q_gen_4462) -> q_gen_4488
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 36  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 34  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 36  ;  (memberl([e, nil])) -> BOT -> 34  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 34
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 35, which took 1.015214 s (model generation: 0.053857,  model checking: 0.961357):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4479, q_gen_4488},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4468) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4464) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4460) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
<z, s>(q_gen_4462) -> q_gen_4488
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 36  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 37  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 36  ;  (memberl([e, nil])) -> BOT -> 35  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 35
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(z, cons(s(s(z)), nil))
})

-------------------------------------------
Step 36, which took 0.852570 s (model generation: 0.061508,  model checking: 0.791062):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4479, q_gen_4488},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<s>(q_gen_4468) -> q_gen_4468
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4464) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4460) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
<z, s>(q_gen_4462) -> q_gen_4488
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 36  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 37  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 39  ;  (memberl([e, nil])) -> BOT -> 36  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 36
}
Sat witness: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 37, which took 0.175943 s (model generation: 0.076356,  model checking: 0.099587):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4477, q_gen_4479, q_gen_4488},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<s>(q_gen_4468) -> q_gen_4459
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4477) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4477
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4463
<s, cons>(q_gen_4488, q_gen_4457) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4460) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4464) -> q_gen_4464
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<z, s>(q_gen_4459) -> q_gen_4466
<s, s>(q_gen_4466) -> q_gen_4479
<z, z>() -> q_gen_4479
<z, s>(q_gen_4462) -> q_gen_4488
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 39  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 37  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 39  ;  (memberl([e, nil])) -> BOT -> 37  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 37
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(s(z))  ;  t1 -> cons(s(z), cons(s(s(z)), cons(z, nil)))
})

-------------------------------------------
Step 38, which took 1.079042 s (model generation: 0.091933,  model checking: 0.987109):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4477, q_gen_4479, q_gen_4488},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4477) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<s>(q_gen_4468) -> q_gen_4468
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4477
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4460) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4464) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
<z, s>(q_gen_4462) -> q_gen_4488
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 39  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 40  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 39  ;  (memberl([e, nil])) -> BOT -> 38  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 38
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(z, cons(s(s(s(z))), nil))
})

-------------------------------------------
Step 39, which took 1.557848 s (model generation: 0.091504,  model checking: 1.466344):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4477, q_gen_4479, q_gen_4488},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4477) -> q_gen_4458
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4477) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<s>(q_gen_4468) -> q_gen_4468
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4477
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4463
<s, cons>(q_gen_4488, q_gen_4460) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4464) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
<z, s>(q_gen_4462) -> q_gen_4488
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 39  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 40  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 42  ;  (memberl([e, nil])) -> BOT -> 39  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 39
}
Sat witness: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(s(z))  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 40, which took 1.231919 s (model generation: 0.096252,  model checking: 1.135667):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4477, q_gen_4479, q_gen_4488},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4477) -> q_gen_4458
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4477) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4468) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4460
<s, cons>(q_gen_4488, q_gen_4457) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4460) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4464) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, z>() -> q_gen_4479
<z, s>(q_gen_4462) -> q_gen_4488
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 42  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 40  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 42  ;  (memberl([e, nil])) -> BOT -> 40  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 40
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(s(s(z)), cons(s(z), nil))
})

-------------------------------------------
Step 41, which took 0.340189 s (model generation: 0.099351,  model checking: 0.240838):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4477, q_gen_4479, q_gen_4488},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4477) -> q_gen_4458
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4458
<cons>(q_gen_4468, q_gen_4477) -> q_gen_4458
<nil>() -> q_gen_4458
<s>(q_gen_4468) -> q_gen_4459
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4477
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4488, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4463
<s, cons>(q_gen_4488, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4460) -> q_gen_4464
<s, cons>(q_gen_4488, q_gen_4464) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<z, s>(q_gen_4459) -> q_gen_4466
<s, s>(q_gen_4466) -> q_gen_4479
<z, z>() -> q_gen_4479
<z, s>(q_gen_4462) -> q_gen_4488
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 42  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 43  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 42  ;  (memberl([e, nil])) -> BOT -> 41  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 41
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> s(s(z))  ;  t1 -> cons(s(z), cons(z, nil))
})

-------------------------------------------
Step 42, which took 0.240689 s (model generation: 0.094716,  model checking: 0.145973):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4472, q_gen_4477, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4477) -> q_gen_4458
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4458
<cons>(q_gen_4468, q_gen_4477) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4477) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4468) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4472
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4472
<cons>(q_gen_4468, q_gen_4472) -> q_gen_4472
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4472) -> q_gen_4460
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4472) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<s, nil>(q_gen_4459) -> q_gen_4464
<z, cons>(q_gen_4459, q_gen_4472) -> q_gen_4464
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, s>(q_gen_4462) -> q_gen_4479
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 42  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 43  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 45  ;  (memberl([e, nil])) -> BOT -> 42  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 42
}
Sat witness: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(z)  ;  h1 -> s(s(z))  ;  t1 -> cons(s(s(z)), cons(s(s(z)), cons(z, nil)))
})

-------------------------------------------
Step 43, which took 0.389678 s (model generation: 0.108432,  model checking: 0.281246):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4472, q_gen_4477, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4477) -> q_gen_4461
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4468, q_gen_4477) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<s>(q_gen_4468) -> q_gen_4468
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4472
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4472
<cons>(q_gen_4468, q_gen_4472) -> q_gen_4472
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4472) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4468, q_gen_4472) -> q_gen_4460
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4459, q_gen_4472) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, s>(q_gen_4462) -> q_gen_4479
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 45  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 43  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 45  ;  (memberl([e, nil])) -> BOT -> 43  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 43
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(s(z), cons(s(z), cons(s(z), nil)))
})

-------------------------------------------
Step 44, which took 0.369833 s (model generation: 0.119945,  model checking: 0.249888):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4472, q_gen_4477, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4462, q_gen_4477) -> q_gen_4458
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4458
<cons>(q_gen_4468, q_gen_4477) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<s>(q_gen_4468) -> q_gen_4468
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4472
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4472) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4460
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4468, q_gen_4472) -> q_gen_4460
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4464
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, s>(q_gen_4462) -> q_gen_4479
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 45  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 46  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 45  ;  (memberl([e, nil])) -> BOT -> 44  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 44
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(s(s(z)), cons(s(s(s(z))), cons(s(z), nil)))
})

-------------------------------------------
Step 45, which took 15.010661 s (model generation: 0.285680,  model checking: 14.724981):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4472, q_gen_4477, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4468, q_gen_4477) -> q_gen_4458
<nil>() -> q_gen_4458
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4477) -> q_gen_4461
<cons>(q_gen_4462, q_gen_4477) -> q_gen_4461
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4468) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4472
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4477
<cons>(q_gen_4468, q_gen_4472) -> q_gen_4477
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4472) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4472) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<z, cons>(q_gen_4468, q_gen_4472) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, s>(q_gen_4462) -> q_gen_4479
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 45  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 46  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 48  ;  (memberl([e, nil])) -> BOT -> 45  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 45
}
Sat witness: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(s(z), cons(s(s(z)), nil))
})

-------------------------------------------
Step 46, which took 1.204969 s (model generation: 0.173611,  model checking: 1.031358):

Model:
|_
{
memberl -> 
{{{
Q={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_4466, q_gen_4468, q_gen_4472, q_gen_4477, q_gen_4479},
Q_f={q_gen_4457, q_gen_4460},
Delta=
{
<cons>(q_gen_4459, q_gen_4477) -> q_gen_4458
<cons>(q_gen_4462, q_gen_4477) -> q_gen_4458
<cons>(q_gen_4468, q_gen_4461) -> q_gen_4458
<cons>(q_gen_4468, q_gen_4477) -> q_gen_4458
<nil>() -> q_gen_4458
<s>(q_gen_4468) -> q_gen_4459
<z>() -> q_gen_4459
<cons>(q_gen_4459, q_gen_4458) -> q_gen_4461
<cons>(q_gen_4459, q_gen_4461) -> q_gen_4461
<s>(q_gen_4459) -> q_gen_4462
<s>(q_gen_4462) -> q_gen_4468
<cons>(q_gen_4462, q_gen_4461) -> q_gen_4472
<cons>(q_gen_4462, q_gen_4458) -> q_gen_4477
<cons>(q_gen_4468, q_gen_4458) -> q_gen_4477
<s, cons>(q_gen_4466, q_gen_4457) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4463) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4460) -> q_gen_4457
<s, cons>(q_gen_4479, q_gen_4463) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4458) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4461) -> q_gen_4457
<z, cons>(q_gen_4459, q_gen_4477) -> q_gen_4457
<z, cons>(q_gen_4462, q_gen_4472) -> q_gen_4457
<z, cons>(q_gen_4468, q_gen_4461) -> q_gen_4457
<s, cons>(q_gen_4466, q_gen_4464) -> q_gen_4460
<z, cons>(q_gen_4459, q_gen_4472) -> q_gen_4460
<z, cons>(q_gen_4462, q_gen_4461) -> q_gen_4460
<s, cons>(q_gen_4479, q_gen_4457) -> q_gen_4463
<s, nil>(q_gen_4459) -> q_gen_4463
<z, cons>(q_gen_4462, q_gen_4458) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4472) -> q_gen_4463
<z, cons>(q_gen_4468, q_gen_4477) -> q_gen_4463
<s, cons>(q_gen_4479, q_gen_4464) -> q_gen_4464
<z, cons>(q_gen_4462, q_gen_4477) -> q_gen_4464
<z, cons>(q_gen_4468, q_gen_4458) -> q_gen_4464
<z, nil>() -> q_gen_4464
<s, s>(q_gen_4466) -> q_gen_4466
<z, s>(q_gen_4459) -> q_gen_4466
<z, s>(q_gen_4462) -> q_gen_4479
<z, z>() -> q_gen_4479
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 48  ;  (memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 46  ;  (memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 48  ;  (memberl([e, nil])) -> BOT -> 46  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 46
}
Sat witness: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(s(s(z)), cons(s(z), cons(z, nil)))
})

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