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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(delete, F:
{() -> delete([x, nil, nil])
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu])
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)])}
(delete([_ju, _ku, _lu]) /\ delete([_ju, _ku, _mu])) -> eq_eltlist([_lu, _mu])
)
(mem, P:
{() -> mem([h, cons(h, t)])
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)])
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t])
(mem([e, nil])) -> BOT}
)
}

properties:
{(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT}


over-approximation: {delete, mem}
under-approximation: {}

Clause system for inference is:

{
() -> delete([x, nil, nil]) -> 0
() -> mem([h, cons(h, t)]) -> 0
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 0
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 0
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 0
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 0
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 0
(mem([e, nil])) -> BOT -> 0
}


Solving took 2.158214 seconds.
Proved
Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895, q_gen_3907},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3895
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3907
<cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3907
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<a, cons, cons>(q_gen_3878, q_gen_3907) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3884) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005233 s (model generation: 0.004874,  model checking: 0.000359):

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

}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 0
() -> mem([h, cons(h, t)]) -> 3
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 1
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 1
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 1
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 1
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 1
(mem([e, nil])) -> BOT -> 1
}
Sat witness: Found: (() -> mem([h, cons(h, t)]), {
h -> b  ;  t -> nil
})

-------------------------------------------
Step 1, which took 0.004463 s (model generation: 0.004177,  model checking: 0.000286):

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

}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 3
() -> mem([h, cons(h, t)]) -> 3
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 1
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 1
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 1
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 1
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 1
(mem([e, nil])) -> BOT -> 1
}
Sat witness: Found: (() -> delete([x, nil, nil]), {
x -> b
})

-------------------------------------------
Step 2, which took 0.005336 s (model generation: 0.004661,  model checking: 0.000675):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862},
Q_f={q_gen_3862},
Delta=
{
<b, nil, nil>() -> q_gen_3862
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 3
() -> mem([h, cons(h, t)]) -> 3
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 1
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 1
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 1
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 4
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 2
(mem([e, nil])) -> BOT -> 2
}
Sat witness: Found: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> b  ;  h -> a  ;  t -> cons(b, nil)
})

-------------------------------------------
Step 3, which took 0.005055 s (model generation: 0.004777,  model checking: 0.000278):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862},
Q_f={q_gen_3862},
Delta=
{
<b, nil, nil>() -> q_gen_3862
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861},
Q_f={q_gen_3859},
Delta=
{
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3860
<nil>() -> q_gen_3860
<a>() -> q_gen_3861
<b>() -> q_gen_3861
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 3
() -> mem([h, cons(h, t)]) -> 3
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 1
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 1
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 4
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 4
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 2
(mem([e, nil])) -> BOT -> 2
}
Sat witness: Found: ((delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]), {
_iu -> nil  ;  h -> a  ;  t -> nil  ;  x -> b
})

-------------------------------------------
Step 4, which took 0.005458 s (model generation: 0.005417,  model checking: 0.000041):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868},
Q_f={q_gen_3862},
Delta=
{
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861},
Q_f={q_gen_3859},
Delta=
{
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3860
<nil>() -> q_gen_3860
<a>() -> q_gen_3861
<b>() -> q_gen_3861
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 3
() -> mem([h, cons(h, t)]) -> 3
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 1
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 4
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 4
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 4
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 2
(mem([e, nil])) -> BOT -> 2
}
Sat witness: Found: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(a, nil)  ;  i -> b  ;  l -> cons(a, nil)
})

-------------------------------------------
Step 5, which took 0.006502 s (model generation: 0.006228,  model checking: 0.000274):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868},
Q_f={q_gen_3862},
Delta=
{
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<a>() -> q_gen_3865
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 3
() -> mem([h, cons(h, t)]) -> 3
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 4
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 4
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 4
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 4
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 2
(mem([e, nil])) -> BOT -> 2
}
Sat witness: Found: ((delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]), {
_hu -> nil  ;  h -> b  ;  t -> nil
})

-------------------------------------------
Step 6, which took 0.010290 s (model generation: 0.008838,  model checking: 0.001452):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872},
Q_f={q_gen_3862},
Delta=
{
<nil>() -> q_gen_3871
<b>() -> q_gen_3872
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<a>() -> q_gen_3865
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 3
() -> mem([h, cons(h, t)]) -> 6
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 4
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 4
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 4
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 4
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 3
(mem([e, nil])) -> BOT -> 3
}
Sat witness: Found: (() -> mem([h, cons(h, t)]), {
h -> a  ;  t -> nil
})

-------------------------------------------
Step 7, which took 0.013710 s (model generation: 0.011979,  model checking: 0.001731):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872},
Q_f={q_gen_3862},
Delta=
{
<nil>() -> q_gen_3871
<b>() -> q_gen_3872
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<a>() -> q_gen_3865
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 6
() -> mem([h, cons(h, t)]) -> 6
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 4
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 4
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 4
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 4
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 4
(mem([e, nil])) -> BOT -> 4
}
Sat witness: Found: (() -> delete([x, nil, nil]), {
x -> a
})

-------------------------------------------
Step 8, which took 0.014500 s (model generation: 0.012289,  model checking: 0.002211):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872},
Q_f={q_gen_3862},
Delta=
{
<nil>() -> q_gen_3871
<b>() -> q_gen_3872
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<a>() -> q_gen_3865
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 6
() -> mem([h, cons(h, t)]) -> 6
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 4
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 4
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 4
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 7
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 5
(mem([e, nil])) -> BOT -> 5
}
Sat witness: Found: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> b  ;  h -> a  ;  t -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 9, which took 0.014032 s (model generation: 0.013151,  model checking: 0.000881):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872},
Q_f={q_gen_3862},
Delta=
{
<nil>() -> q_gen_3871
<b>() -> q_gen_3872
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 6
() -> mem([h, cons(h, t)]) -> 6
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 4
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 4
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 7
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 7
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 5
(mem([e, nil])) -> BOT -> 5
}
Sat witness: Found: ((delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]), {
_iu -> nil  ;  h -> b  ;  t -> nil  ;  x -> a
})

-------------------------------------------
Step 10, which took 0.013799 s (model generation: 0.013653,  model checking: 0.000146):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872},
Q_f={q_gen_3862},
Delta=
{
<nil>() -> q_gen_3871
<b>() -> q_gen_3872
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, b>() -> q_gen_3868
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 6
() -> mem([h, cons(h, t)]) -> 6
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 4
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 7
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 7
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 7
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 5
(mem([e, nil])) -> BOT -> 5
}
Sat witness: Found: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(b, nil)  ;  i -> b  ;  l -> cons(b, nil)
})

-------------------------------------------
Step 11, which took 0.015556 s (model generation: 0.014482,  model checking: 0.001074):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<nil>() -> q_gen_3871
<b>() -> q_gen_3872
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 6
() -> mem([h, cons(h, t)]) -> 6
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 7
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 7
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 7
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 7
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 5
(mem([e, nil])) -> BOT -> 5
}
Sat witness: Found: ((delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]), {
_hu -> nil  ;  h -> a  ;  t -> nil
})

-------------------------------------------
Step 12, which took 0.017009 s (model generation: 0.014359,  model checking: 0.002650):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 6
() -> mem([h, cons(h, t)]) -> 9
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 7
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 7
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 7
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 7
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 6
(mem([e, nil])) -> BOT -> 6
}
Sat witness: Found: (() -> mem([h, cons(h, t)]), {
h -> b  ;  t -> cons(b, nil)
})

-------------------------------------------
Step 13, which took 0.018257 s (model generation: 0.015389,  model checking: 0.002868):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 7
() -> mem([h, cons(h, t)]) -> 9
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 7
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 7
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 7
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 10
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 7
(mem([e, nil])) -> BOT -> 7
}
Sat witness: Found: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> a  ;  h -> b  ;  t -> cons(a, nil)
})

-------------------------------------------
Step 14, which took 0.016582 s (model generation: 0.016176,  model checking: 0.000406):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 7
() -> mem([h, cons(h, t)]) -> 9
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 7
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 7
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 7
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 10
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 10
(mem([e, nil])) -> BOT -> 8
}
Sat witness: Found: ((mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]), {
e -> b  ;  h -> a  ;  t -> cons(a, nil)
})

-------------------------------------------
Step 15, which took 0.019018 s (model generation: 0.017192,  model checking: 0.001826):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869},
Q_f={q_gen_3859},
Delta=
{
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3860
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 7
() -> mem([h, cons(h, t)]) -> 9
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 7
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 7
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 10
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 10
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 10
(mem([e, nil])) -> BOT -> 8
}
Sat witness: Found: ((delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]), {
_iu -> nil  ;  h -> b  ;  t -> cons(a, nil)  ;  x -> a
})

-------------------------------------------
Step 16, which took 0.017843 s (model generation: 0.017609,  model checking: 0.000234):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869},
Q_f={q_gen_3859},
Delta=
{
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3860
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 7
() -> mem([h, cons(h, t)]) -> 9
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 7
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 10
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 10
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 10
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 10
(mem([e, nil])) -> BOT -> 8
}
Sat witness: Found: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(b, nil)  ;  i -> a  ;  l -> cons(b, nil)
})

-------------------------------------------
Step 17, which took 0.019317 s (model generation: 0.018272,  model checking: 0.001045):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 7
() -> mem([h, cons(h, t)]) -> 9
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 10
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 10
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 10
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 10
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 10
(mem([e, nil])) -> BOT -> 8
}
Sat witness: Found: ((delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]), {
_hu -> nil  ;  h -> b  ;  t -> cons(b, nil)
})

-------------------------------------------
Step 18, which took 0.020423 s (model generation: 0.019417,  model checking: 0.001006):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 8
() -> mem([h, cons(h, t)]) -> 12
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 10
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 10
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 10
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 10
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 10
(mem([e, nil])) -> BOT -> 9
}
Sat witness: Found: (() -> mem([h, cons(h, t)]), {
h -> a  ;  t -> cons(b, nil)
})

-------------------------------------------
Step 19, which took 0.026197 s (model generation: 0.019947,  model checking: 0.006250):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 9
() -> mem([h, cons(h, t)]) -> 12
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 10
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 10
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 10
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 13
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 11
(mem([e, nil])) -> BOT -> 10
}
Sat witness: Found: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> a  ;  h -> b  ;  t -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 20, which took 0.023595 s (model generation: 0.021165,  model checking: 0.002430):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 10
() -> mem([h, cons(h, t)]) -> 12
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 10
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 10
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 13
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 13
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 11
(mem([e, nil])) -> BOT -> 11
}
Sat witness: Found: ((delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]), {
_iu -> cons(b, nil)  ;  h -> b  ;  t -> cons(b, nil)  ;  x -> a
})

-------------------------------------------
Step 21, which took 0.022468 s (model generation: 0.022055,  model checking: 0.000413):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 10
() -> mem([h, cons(h, t)]) -> 12
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 10
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 13
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 13
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 13
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 11
(mem([e, nil])) -> BOT -> 11
}
Sat witness: Found: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(b, cons(b, nil))  ;  i -> a  ;  l -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 22, which took 0.023972 s (model generation: 0.022994,  model checking: 0.000978):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 10
() -> mem([h, cons(h, t)]) -> 12
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 13
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 13
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 13
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 13
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 11
(mem([e, nil])) -> BOT -> 11
}
Sat witness: Found: ((delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]), {
_hu -> cons(b, nil)  ;  h -> a  ;  t -> cons(b, nil)
})

-------------------------------------------
Step 23, which took 0.029411 s (model generation: 0.024526,  model checking: 0.004885):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<a, b>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 11
() -> mem([h, cons(h, t)]) -> 15
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 13
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 13
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 13
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 13
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 12
(mem([e, nil])) -> BOT -> 12
}
Sat witness: Found: (() -> mem([h, cons(h, t)]), {
h -> b  ;  t -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 24, which took 0.032907 s (model generation: 0.025631,  model checking: 0.007276):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 12
() -> mem([h, cons(h, t)]) -> 15
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 13
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 13
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 13
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 16
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 13
(mem([e, nil])) -> BOT -> 13
}
Sat witness: Found: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> a  ;  h -> b  ;  t -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 25, which took 0.034292 s (model generation: 0.027110,  model checking: 0.007182):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<a, b>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 13
() -> mem([h, cons(h, t)]) -> 15
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 13
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 13
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 13
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 16
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 16
(mem([e, nil])) -> BOT -> 14
}
Sat witness: Found: ((mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]), {
e -> b  ;  h -> a  ;  t -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 26, which took 0.034918 s (model generation: 0.031865,  model checking: 0.003053):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<a, b>() -> q_gen_3868
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 13
() -> mem([h, cons(h, t)]) -> 15
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 13
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 13
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 16
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 16
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 16
(mem([e, nil])) -> BOT -> 14
}
Sat witness: Found: ((delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]), {
_iu -> cons(a, nil)  ;  h -> b  ;  t -> cons(a, nil)  ;  x -> a
})

-------------------------------------------
Step 27, which took 0.033888 s (model generation: 0.033432,  model checking: 0.000456):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3867
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 13
() -> mem([h, cons(h, t)]) -> 15
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 13
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 16
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 16
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 16
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 16
(mem([e, nil])) -> BOT -> 14
}
Sat witness: Found: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(a, cons(b, nil))  ;  i -> b  ;  l -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 28, which took 0.036272 s (model generation: 0.034162,  model checking: 0.002110):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 13
() -> mem([h, cons(h, t)]) -> 15
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 16
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 16
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 16
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 16
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 16
(mem([e, nil])) -> BOT -> 14
}
Sat witness: Found: ((delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]), {
_hu -> cons(a, nil)  ;  h -> b  ;  t -> cons(a, nil)
})

-------------------------------------------
Step 29, which took 0.037088 s (model generation: 0.035966,  model checking: 0.001122):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 14
() -> mem([h, cons(h, t)]) -> 18
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 16
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 16
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 16
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 16
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 16
(mem([e, nil])) -> BOT -> 15
}
Sat witness: Found: (() -> mem([h, cons(h, t)]), {
h -> b  ;  t -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 30, which took 0.049066 s (model generation: 0.036826,  model checking: 0.012240):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 15
() -> mem([h, cons(h, t)]) -> 18
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 16
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 16
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 16
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 19
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 17
(mem([e, nil])) -> BOT -> 16
}
Sat witness: Found: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> b  ;  h -> a  ;  t -> cons(b, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 31, which took 0.043701 s (model generation: 0.040187,  model checking: 0.003514):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 16
() -> mem([h, cons(h, t)]) -> 18
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 16
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 16
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 19
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 19
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 17
(mem([e, nil])) -> BOT -> 17
}
Sat witness: Found: ((delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]), {
_iu -> cons(b, cons(b, nil))  ;  h -> b  ;  t -> cons(b, cons(b, nil))  ;  x -> a
})

-------------------------------------------
Step 32, which took 0.043112 s (model generation: 0.042180,  model checking: 0.000932):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3867
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 16
() -> mem([h, cons(h, t)]) -> 18
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 16
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 19
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 19
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 19
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 17
(mem([e, nil])) -> BOT -> 17
}
Sat witness: Found: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(a, cons(b, cons(b, nil)))  ;  i -> b  ;  l -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 33, which took 0.156828 s (model generation: 0.046514,  model checking: 0.110314):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3867
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3860
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 17
() -> mem([h, cons(h, t)]) -> 21
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 17
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 19
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 19
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 19
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 18
(mem([e, nil])) -> BOT -> 18
}
Sat witness: Found: (() -> mem([h, cons(h, t)]), {
h -> a  ;  t -> cons(a, nil)
})

-------------------------------------------
Step 34, which took 0.076777 s (model generation: 0.017778,  model checking: 0.058999):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3867
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 18
() -> mem([h, cons(h, t)]) -> 21
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 18
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 19
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 19
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 19
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 21
(mem([e, nil])) -> BOT -> 19
}
Sat witness: Found: ((mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]), {
e -> a  ;  h -> b  ;  t -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 35, which took 0.072630 s (model generation: 0.016991,  model checking: 0.055639):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3867
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3860
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 19
() -> mem([h, cons(h, t)]) -> 21
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 19
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 19
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 19
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 22
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 21
(mem([e, nil])) -> BOT -> 20
}
Sat witness: Found: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> b  ;  h -> a  ;  t -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 36, which took 0.019526 s (model generation: 0.017031,  model checking: 0.002495):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3895
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 19
() -> mem([h, cons(h, t)]) -> 21
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 19
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 22
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 20
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 22
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 21
(mem([e, nil])) -> BOT -> 20
}
Sat witness: Found: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(b, cons(a, nil))  ;  i -> a  ;  l -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 37, which took 0.025034 s (model generation: 0.019358,  model checking: 0.005676):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895, q_gen_3907},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3895
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3907
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<a, cons, cons>(q_gen_3878, q_gen_3907) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 20
() -> mem([h, cons(h, t)]) -> 21
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 20
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 22
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 23
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 22
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 21
(mem([e, nil])) -> BOT -> 21
}
Sat witness: Found: ((delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]), {
_iu -> cons(a, nil)  ;  h -> a  ;  t -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 38, which took 0.067685 s (model generation: 0.053353,  model checking: 0.014332):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895, q_gen_3907},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3895
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3907
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<a, cons, cons>(q_gen_3878, q_gen_3907) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 21
() -> mem([h, cons(h, t)]) -> 24
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 21
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 22
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 23
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 22
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 22
(mem([e, nil])) -> BOT -> 22
}
Sat witness: Found: (() -> mem([h, cons(h, t)]), {
h -> a  ;  t -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 39, which took 0.072876 s (model generation: 0.055813,  model checking: 0.017063):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895, q_gen_3907},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3895
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3907
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<a, cons, cons>(q_gen_3878, q_gen_3907) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 22
() -> mem([h, cons(h, t)]) -> 24
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 22
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 22
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 23
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 25
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 23
(mem([e, nil])) -> BOT -> 23
}
Sat witness: Found: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> a  ;  h -> b  ;  t -> cons(b, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 40, which took 0.082539 s (model generation: 0.060541,  model checking: 0.021998):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895, q_gen_3907},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3895
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3907
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<a, cons, cons>(q_gen_3878, q_gen_3907) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 23
() -> mem([h, cons(h, t)]) -> 24
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 23
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 23
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 26
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 25
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 24
(mem([e, nil])) -> BOT -> 24
}
Sat witness: Found: ((delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]), {
_iu -> cons(a, cons(a, nil))  ;  h -> a  ;  t -> cons(b, cons(b, nil))  ;  x -> b
})

-------------------------------------------
Step 41, which took 0.093018 s (model generation: 0.066056,  model checking: 0.026962):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895, q_gen_3907},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3895
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3907
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<a, cons, cons>(q_gen_3878, q_gen_3907) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 24
() -> mem([h, cons(h, t)]) -> 27
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 24
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 24
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 26
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 25
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 25
(mem([e, nil])) -> BOT -> 25
}
Sat witness: Found: (() -> mem([h, cons(h, t)]), {
h -> b  ;  t -> cons(a, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 42, which took 0.122529 s (model generation: 0.063957,  model checking: 0.058572):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895, q_gen_3907},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3895
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3907
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<a, cons, cons>(q_gen_3878, q_gen_3907) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3876) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 25
() -> mem([h, cons(h, t)]) -> 27
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 25
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 25
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 26
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 28
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 26
(mem([e, nil])) -> BOT -> 26
}
Sat witness: Found: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> a  ;  h -> b  ;  t -> cons(a, cons(b, cons(a, cons(b, nil))))
})

-------------------------------------------
Step 43, which took 0.093325 s (model generation: 0.071401,  model checking: 0.021924):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895, q_gen_3907},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3895
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3907
<cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3907
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<a, cons, cons>(q_gen_3878, q_gen_3907) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 26
() -> mem([h, cons(h, t)]) -> 30
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 26
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 26
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 27
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 28
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 27
(mem([e, nil])) -> BOT -> 27
}
Sat witness: Found: (() -> mem([h, cons(h, t)]), {
h -> b  ;  t -> cons(a, nil)
})

-------------------------------------------
Step 44, which took 0.120127 s (model generation: 0.077029,  model checking: 0.043098):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895, q_gen_3907},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3895
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3907
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<a, cons, cons>(q_gen_3878, q_gen_3907) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3876) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 27
() -> mem([h, cons(h, t)]) -> 30
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 27
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 27
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 28
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 31
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 28
(mem([e, nil])) -> BOT -> 28
}
Sat witness: Found: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> b  ;  h -> a  ;  t -> cons(a, cons(b, cons(a, cons(b, nil))))
})

-------------------------------------------
Step 45, which took 0.097944 s (model generation: 0.078037,  model checking: 0.019907):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895, q_gen_3907},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3895
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3907
<cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3907
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<a, cons, cons>(q_gen_3878, q_gen_3907) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 28
() -> mem([h, cons(h, t)]) -> 33
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 28
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 28
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 29
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 31
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 29
(mem([e, nil])) -> BOT -> 29
}
Sat witness: Found: (() -> mem([h, cons(h, t)]), {
h -> b  ;  t -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 46, which took 0.070629 s (model generation: 0.069775,  model checking: 0.000854):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895, q_gen_3907},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3895
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3907
<cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3907
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<a, cons, cons>(q_gen_3878, q_gen_3907) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<cons>(q_gen_3865, q_gen_3884) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 28
() -> mem([h, cons(h, t)]) -> 33
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 28
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 31
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 29
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 31
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 29
(mem([e, nil])) -> BOT -> 29
}
Sat witness: Found: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(a, cons(a, cons(a, nil)))  ;  i -> b  ;  l -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 47, which took 0.102741 s (model generation: 0.076410,  model checking: 0.026331):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895, q_gen_3907},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3895
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3907
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<a, cons, cons>(q_gen_3878, q_gen_3907) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<cons>(q_gen_3865, q_gen_3884) -> q_gen_3860
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 29
() -> mem([h, cons(h, t)]) -> 33
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 29
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 31
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 30
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 34
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 30
(mem([e, nil])) -> BOT -> 30
}
Sat witness: Found: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> a  ;  h -> b  ;  t -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 48, which took 0.066129 s (model generation: 0.040983,  model checking: 0.025146):

Model:
|_
{
delete -> 
{{{
Q={q_gen_3862, q_gen_3867, q_gen_3868, q_gen_3871, q_gen_3872, q_gen_3878, q_gen_3879, q_gen_3895, q_gen_3907},
Q_f={q_gen_3862},
Delta=
{
<cons>(q_gen_3872, q_gen_3871) -> q_gen_3871
<nil>() -> q_gen_3871
<a>() -> q_gen_3872
<b>() -> q_gen_3872
<cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3867
<cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3867
<nil, nil>() -> q_gen_3867
<a, a>() -> q_gen_3868
<b, a>() -> q_gen_3868
<a, b>() -> q_gen_3878
<b, b>() -> q_gen_3878
<cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3895
<cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3895
<cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3907
<a, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3862
<a, cons, cons>(q_gen_3878, q_gen_3895) -> q_gen_3862
<a, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<a, nil, nil>() -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3862
<b, cons, cons>(q_gen_3868, q_gen_3907) -> q_gen_3862
<b, cons, nil>(q_gen_3872, q_gen_3871) -> q_gen_3862
<b, nil, nil>() -> q_gen_3862
<a, cons, cons>(q_gen_3868, q_gen_3867) -> q_gen_3879
<a, cons, cons>(q_gen_3878, q_gen_3907) -> q_gen_3879
<b, cons, cons>(q_gen_3868, q_gen_3895) -> q_gen_3879
<b, cons, cons>(q_gen_3878, q_gen_3867) -> q_gen_3879
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  mem -> 
{{{
Q={q_gen_3859, q_gen_3860, q_gen_3861, q_gen_3864, q_gen_3865, q_gen_3869, q_gen_3876, q_gen_3884},
Q_f={q_gen_3859},
Delta=
{
<nil>() -> q_gen_3860
<b>() -> q_gen_3861
<cons>(q_gen_3861, q_gen_3860) -> q_gen_3864
<cons>(q_gen_3861, q_gen_3864) -> q_gen_3864
<a>() -> q_gen_3865
<cons>(q_gen_3861, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3864) -> q_gen_3876
<cons>(q_gen_3865, q_gen_3876) -> q_gen_3876
<cons>(q_gen_3861, q_gen_3884) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3860) -> q_gen_3884
<cons>(q_gen_3865, q_gen_3884) -> q_gen_3884
<a, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3860) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3865, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3860) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3876) -> q_gen_3859
<b, cons>(q_gen_3861, q_gen_3884) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3864) -> q_gen_3859
<b, cons>(q_gen_3865, q_gen_3876) -> q_gen_3859
<a, cons>(q_gen_3861, q_gen_3860) -> q_gen_3869
<a, cons>(q_gen_3861, q_gen_3864) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3860) -> q_gen_3869
<b, cons>(q_gen_3865, q_gen_3884) -> q_gen_3869
}

Datatype: <elt, eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> delete([x, nil, nil]) -> 30
() -> mem([h, cons(h, t)]) -> 33
(delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 30
(delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 34
(delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 31
(mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 34
(mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 31
(mem([e, nil])) -> BOT -> 31
}
Sat witness: Found: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(b, cons(a, cons(a, nil)))  ;  i -> a  ;  l -> cons(b, cons(b, cons(b, nil)))
})

Total time: 2.158214
Reason for stopping: Proved