Solving ../../benchmarks/true/timbuk_delete.smt2...

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


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 1.533952 seconds.
Proved
Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079, q_gen_6087, q_gen_6111},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6063
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6063
<cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6063) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6087
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6087
<cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6087
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6087
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<cons>(q_gen_6061, q_gen_6084) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004728 s (model generation: 0.003817,  model checking: 0.000911):

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

}

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

}

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

}
--
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: Yes: (() -> mem([h, cons(h, t)]), {
h -> b  ;  t -> nil
})

-------------------------------------------
Step 1, which took 0.003710 s (model generation: 0.003597,  model checking: 0.000113):

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

}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
}

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

}
--
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: Yes: (() -> delete([x, nil, nil]), {
x -> b
})

-------------------------------------------
Step 2, which took 0.004498 s (model generation: 0.003424,  model checking: 0.001074):

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

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
}

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

}
--
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: Yes: ((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.003669 s (model generation: 0.003547,  model checking: 0.000122):

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

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057},
Q_f={q_gen_6055},
Delta=
{
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6056
<nil>() -> q_gen_6056
<a>() -> q_gen_6057
<b>() -> q_gen_6057
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
}

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

}
--
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: Yes: ((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.003711 s (model generation: 0.003677,  model checking: 0.000034):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066},
Q_f={q_gen_6058},
Delta=
{
<nil, nil>() -> q_gen_6063
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057},
Q_f={q_gen_6055},
Delta=
{
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6056
<nil>() -> q_gen_6056
<a>() -> q_gen_6057
<b>() -> q_gen_6057
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
}

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

}
--
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: Yes: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(a, nil)  ;  i -> b  ;  l -> cons(a, nil)
})

-------------------------------------------
Step 5, which took 0.006707 s (model generation: 0.004327,  model checking: 0.002380):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066},
Q_f={q_gen_6058},
Delta=
{
<nil, nil>() -> q_gen_6063
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<a>() -> q_gen_6061
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
}

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

}
--
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: Yes: ((delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]), {
_hu -> nil  ;  h -> b  ;  t -> nil
})

-------------------------------------------
Step 6, which took 0.007511 s (model generation: 0.007056,  model checking: 0.000455):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070},
Q_f={q_gen_6058},
Delta=
{
<nil>() -> q_gen_6069
<b>() -> q_gen_6070
<nil, nil>() -> q_gen_6063
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<a>() -> q_gen_6061
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
}

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

}
--
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: Yes: (() -> mem([h, cons(h, t)]), {
h -> a  ;  t -> nil
})

-------------------------------------------
Step 7, which took 0.010153 s (model generation: 0.009127,  model checking: 0.001026):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070},
Q_f={q_gen_6058},
Delta=
{
<nil>() -> q_gen_6069
<b>() -> q_gen_6070
<nil, nil>() -> q_gen_6063
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<a>() -> q_gen_6061
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
}

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

}
--
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: Yes: (() -> delete([x, nil, nil]), {
x -> a
})

-------------------------------------------
Step 8, which took 0.014213 s (model generation: 0.012347,  model checking: 0.001866):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070},
Q_f={q_gen_6058},
Delta=
{
<nil>() -> q_gen_6069
<b>() -> q_gen_6070
<nil, nil>() -> q_gen_6063
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<a>() -> q_gen_6061
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
}

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

}
--
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: Yes: ((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.011473 s (model generation: 0.008964,  model checking: 0.002509):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070},
Q_f={q_gen_6058},
Delta=
{
<nil>() -> q_gen_6069
<b>() -> q_gen_6070
<nil, nil>() -> q_gen_6063
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
}

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

}
--
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: Yes: ((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.005470 s (model generation: 0.005408,  model checking: 0.000062):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070},
Q_f={q_gen_6058},
Delta=
{
<nil>() -> q_gen_6069
<b>() -> q_gen_6070
<nil, nil>() -> q_gen_6063
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
}

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

}
--
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: Yes: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(b, nil)  ;  i -> b  ;  l -> cons(b, nil)
})

-------------------------------------------
Step 11, which took 0.007317 s (model generation: 0.005490,  model checking: 0.001827):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<nil>() -> q_gen_6069
<b>() -> q_gen_6070
<nil, nil>() -> q_gen_6063
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
}

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

}
--
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: Yes: ((delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]), {
_hu -> nil  ;  h -> a  ;  t -> nil
})

-------------------------------------------
Step 12, which took 0.015481 s (model generation: 0.012243,  model checking: 0.003238):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<nil, nil>() -> q_gen_6063
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
}

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

}
--
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: Yes: (() -> mem([h, cons(h, t)]), {
h -> b  ;  t -> cons(b, nil)
})

-------------------------------------------
Step 13, which took 0.021854 s (model generation: 0.016377,  model checking: 0.005477):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<nil, nil>() -> q_gen_6063
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
}

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

}
--
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: Yes: ((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.011444 s (model generation: 0.011316,  model checking: 0.000128):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6078, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<nil, nil>() -> q_gen_6063
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6078
<a, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
}

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

}
--
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: Yes: ((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.025954 s (model generation: 0.013830,  model checking: 0.012124):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6078, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<nil, nil>() -> q_gen_6063
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6078
<a, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067},
Q_f={q_gen_6055},
Delta=
{
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6056
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
}

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

}
--
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: Yes: ((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.017693 s (model generation: 0.017416,  model checking: 0.000277):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067},
Q_f={q_gen_6055},
Delta=
{
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6056
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
}

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

}
--
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: Yes: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(b, nil)  ;  i -> a  ;  l -> cons(b, nil)
})

-------------------------------------------
Step 17, which took 0.020668 s (model generation: 0.018437,  model checking: 0.002231):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6078, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6078
<a, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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: Yes: ((delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]), {
_hu -> nil  ;  h -> b  ;  t -> cons(b, nil)
})

-------------------------------------------
Step 18, which took 0.007166 s (model generation: 0.006592,  model checking: 0.000574):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6078, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6078
<a, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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: Yes: (() -> mem([h, cons(h, t)]), {
h -> a  ;  t -> cons(b, nil)
})

-------------------------------------------
Step 19, which took 0.008876 s (model generation: 0.006339,  model checking: 0.002537):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6078, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6078
<a, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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: Yes: ((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.012063 s (model generation: 0.006937,  model checking: 0.005126):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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: Yes: ((delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]), {
_iu -> nil  ;  h -> a  ;  t -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 21, which took 0.009140 s (model generation: 0.007457,  model checking: 0.001683):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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 -> 11  ;  (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: Yes: ((delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]), {
_hu -> cons(b, nil)  ;  h -> a  ;  t -> cons(b, nil)
})

-------------------------------------------
Step 22, which took 0.008925 s (model generation: 0.008321,  model checking: 0.000604):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, b>() -> q_gen_6066
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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)]) -> 12  ;  (delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 13  ;  (delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 11  ;  (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]) -> 14  ;  (mem([e, nil])) -> BOT -> 12
}
Sat witness: Yes: ((mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]), {
e -> a  ;  h -> b  ;  t -> cons(b, nil)
})

-------------------------------------------
Step 23, which took 0.008716 s (model generation: 0.008605,  model checking: 0.000111):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6077, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, b>() -> q_gen_6066
<b, nil>() -> q_gen_6077
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6084
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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)]) -> 12  ;  (delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 13  ;  (delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 14  ;  (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]) -> 14  ;  (mem([e, nil])) -> BOT -> 12
}
Sat witness: Yes: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(b, nil)  ;  i -> b  ;  l -> cons(a, nil)
})

-------------------------------------------
Step 24, which took 0.013445 s (model generation: 0.012150,  model checking: 0.001295):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, b>() -> q_gen_6066
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6084
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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 -> 14  ;  (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]) -> 14  ;  (mem([e, nil])) -> BOT -> 13
}
Sat witness: Yes: (() -> mem([h, cons(h, t)]), {
h -> b  ;  t -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 25, which took 0.026793 s (model generation: 0.025467,  model checking: 0.001326):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, b>() -> q_gen_6066
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6084
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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 -> 14  ;  (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]) -> 14  ;  (mem([e, nil])) -> BOT -> 14
}
Sat witness: Yes: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> a  ;  h -> b  ;  t -> cons(a, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 26, which took 0.029011 s (model generation: 0.024145,  model checking: 0.004866):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, b>() -> q_gen_6066
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6084
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6084
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<cons>(q_gen_6061, q_gen_6084) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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 -> 14  ;  (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]) -> 14  ;  (mem([e, nil])) -> BOT -> 14
}
Sat witness: Yes: ((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 27, which took 0.025230 s (model generation: 0.022573,  model checking: 0.002657):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6063
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, b>() -> q_gen_6066
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6084) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6084
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6084
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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 -> 14  ;  (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]) -> 14  ;  (mem([e, nil])) -> BOT -> 14
}
Sat witness: Yes: ((delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]), {
_hu -> cons(a, nil)  ;  h -> b  ;  t -> cons(a, nil)
})

-------------------------------------------
Step 28, which took 0.022929 s (model generation: 0.020832,  model checking: 0.002097):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6063
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6084) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6084
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6084
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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)]) -> 15  ;  (delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 16  ;  (delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 14  ;  (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]) -> 17  ;  (mem([e, nil])) -> BOT -> 15
}
Sat witness: Yes: ((mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]), {
e -> a  ;  h -> b  ;  t -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 29, which took 0.023577 s (model generation: 0.022886,  model checking: 0.000691):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6063
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6056
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6084
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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)]) -> 15  ;  (delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 16  ;  (delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 17  ;  (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]) -> 17  ;  (mem([e, nil])) -> BOT -> 15
}
Sat witness: Yes: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(b, nil)  ;  i -> b  ;  l -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 30, which took 0.020593 s (model generation: 0.019580,  model checking: 0.001013):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6078, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, a>() -> q_gen_6066
<a, b>() -> q_gen_6078
<b, b>() -> q_gen_6078
<a, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6056
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6084
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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 -> 17  ;  (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]) -> 17  ;  (mem([e, nil])) -> BOT -> 16
}
Sat witness: Yes: (() -> mem([h, cons(h, t)]), {
h -> b  ;  t -> cons(a, nil)
})

-------------------------------------------
Step 31, which took 0.026702 s (model generation: 0.025432,  model checking: 0.001270):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6078, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, a>() -> q_gen_6066
<a, b>() -> q_gen_6078
<b, b>() -> q_gen_6078
<a, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6056
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6084
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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 -> 17  ;  (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 -> 17
}
Sat witness: Yes: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> b  ;  h -> a  ;  t -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 32, which took 0.018473 s (model generation: 0.014514,  model checking: 0.003959):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6063
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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 -> 17  ;  (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: Yes: ((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(b, nil)  ;  x -> b
})

-------------------------------------------
Step 33, which took 0.032650 s (model generation: 0.020153,  model checking: 0.012497):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6063
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6084
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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)]) -> 18  ;  (delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 17  ;  (delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 20  ;  (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: Yes: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(b, cons(a, nil))  ;  i -> a  ;  l -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 34, which took 0.028029 s (model generation: 0.018077,  model checking: 0.009952):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079, q_gen_6120},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6063
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6120
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6120) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6120) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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 -> 20  ;  (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]) -> 19  ;  (mem([e, nil])) -> BOT -> 19
}
Sat witness: Yes: (() -> mem([h, cons(h, t)]), {
h -> b  ;  t -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 35, which took 0.032339 s (model generation: 0.020780,  model checking: 0.011559):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079, q_gen_6120},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6063
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6120
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6120) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6120) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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 -> 20  ;  (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]) -> 20  ;  (mem([e, nil])) -> BOT -> 20
}
Sat witness: Yes: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> b  ;  h -> a  ;  t -> cons(b, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 36, which took 0.032572 s (model generation: 0.022506,  model checking: 0.010066):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6078, q_gen_6079, q_gen_6120},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, a>() -> q_gen_6066
<a, b>() -> q_gen_6078
<b, b>() -> q_gen_6078
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6120
<a, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6120) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6120) -> q_gen_6079
<b, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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 -> 20  ;  (delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 22  ;  (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]) -> 20  ;  (mem([e, nil])) -> BOT -> 20
}
Sat witness: Yes: ((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 37, which took 0.038127 s (model generation: 0.025634,  model checking: 0.012493):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6078, q_gen_6079, q_gen_6120},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<b, a>() -> q_gen_6066
<a, b>() -> q_gen_6078
<b, b>() -> q_gen_6078
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6120
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6120) -> q_gen_6120
<a, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6120) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6120) -> q_gen_6079
<b, cons, cons>(q_gen_6078, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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 -> 23  ;  (delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 22  ;  (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: Yes: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(a, cons(b, nil))  ;  i -> b  ;  l -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 38, which took 0.026921 s (model generation: 0.025692,  model checking: 0.001229):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079, q_gen_6081, q_gen_6122},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<cons>(q_gen_6081, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<b>() -> q_gen_6070
<a>() -> q_gen_6081
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6063
<cons, cons>(q_gen_6066, q_gen_6122, q_gen_6076, q_gen_6063) -> q_gen_6063
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<cons, nil>(q_gen_6081, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6081, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6076
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6076
<cons, b>(q_gen_6081, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<a, cons>(q_gen_6081, q_gen_6069) -> q_gen_6122
<b, cons>(q_gen_6081, q_gen_6069) -> q_gen_6122
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6081, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6122, q_gen_6076, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, cons, nil>(q_gen_6081, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6122, q_gen_6076, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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]) -> 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)]) -> 22  ;  (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: Yes: ((delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]), {
_hu -> cons(a, nil)  ;  h -> b  ;  t -> cons(b, nil)
})

-------------------------------------------
Step 39, which took 0.031133 s (model generation: 0.027727,  model checking: 0.003406):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6077, q_gen_6079, q_gen_6087, q_gen_6101},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6077
<b, nil>() -> q_gen_6077
<cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6087
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6087
<a, b>() -> q_gen_6101
<b, a>() -> q_gen_6101
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6087) -> q_gen_6058
<a, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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]) -> 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)]) -> 22  ;  (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: Yes: (() -> mem([h, cons(h, t)]), {
h -> a  ;  t -> cons(a, nil)
})

-------------------------------------------
Step 40, which took 0.034670 s (model generation: 0.029554,  model checking: 0.005116):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6077, q_gen_6079, q_gen_6087, q_gen_6101},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<b, nil>() -> q_gen_6077
<cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6087
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6087
<a, b>() -> q_gen_6101
<b, a>() -> q_gen_6101
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6087) -> q_gen_6058
<a, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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]) -> 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)]) -> 22  ;  (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: Yes: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> b  ;  h -> a  ;  t -> cons(a, cons(a, cons(b, cons(b, nil))))
})

-------------------------------------------
Step 41, which took 0.042759 s (model generation: 0.034283,  model checking: 0.008476):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6077, q_gen_6079, q_gen_6087, q_gen_6101},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<b, nil>() -> q_gen_6077
<cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6087
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6087
<a, b>() -> q_gen_6101
<b, a>() -> q_gen_6101
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6087) -> q_gen_6058
<a, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6074) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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]) -> 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)]) -> 25  ;  (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: Yes: ((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 42, which took 0.038671 s (model generation: 0.032511,  model checking: 0.006160):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6077, q_gen_6079, q_gen_6087, q_gen_6101},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<b, nil>() -> q_gen_6077
<cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6087
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6087
<a, b>() -> q_gen_6101
<b, a>() -> q_gen_6101
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6087) -> q_gen_6058
<a, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6074) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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 -> 26  ;  (delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 25  ;  (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: Yes: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(a, nil)  ;  i -> a  ;  l -> cons(a, nil)
})

-------------------------------------------
Step 43, which took 0.046585 s (model generation: 0.036118,  model checking: 0.010467):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079, q_gen_6087, q_gen_6111},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6063) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6087
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6087
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6087) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6074) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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]) -> 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)]) -> 25  ;  (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: Yes: ((delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]), {
_hu -> cons(a, cons(a, cons(a, nil)))  ;  h -> b  ;  t -> cons(a, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 44, which took 0.040666 s (model generation: 0.035158,  model checking: 0.005508):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6077, q_gen_6079, q_gen_6101, q_gen_6110},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6110) -> q_gen_6063
<cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<b, nil>() -> q_gen_6077
<a, b>() -> q_gen_6101
<b, a>() -> q_gen_6101
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6110
<cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6110
<cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6110
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6110) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6110) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6110) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6074) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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]) -> 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)]) -> 25  ;  (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: Yes: (() -> mem([h, cons(h, t)]), {
h -> a  ;  t -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 45, which took 0.045204 s (model generation: 0.041024,  model checking: 0.004180):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079, q_gen_6087, q_gen_6111},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6063
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6087
<cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6063) -> q_gen_6087
<cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6087
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6087
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6074) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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]) -> 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)]) -> 25  ;  (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: Yes: ((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 46, which took 0.042564 s (model generation: 0.040685,  model checking: 0.001879):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6077, q_gen_6079, q_gen_6101, q_gen_6110},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6110) -> q_gen_6063
<cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<nil, b>() -> q_gen_6064
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, nil>() -> q_gen_6065
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<b, nil>() -> q_gen_6077
<a, b>() -> q_gen_6101
<b, a>() -> q_gen_6101
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6110
<cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6110
<cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6110
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6110) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6101, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6110) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6077, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6101, q_gen_6065, q_gen_6064, q_gen_6110) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6074) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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]) -> 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)]) -> 28  ;  (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: Yes: ((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 47, which took 0.050595 s (model generation: 0.045299,  model checking: 0.005296):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079, q_gen_6087, q_gen_6111},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6065
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6087
<cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6063) -> q_gen_6087
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6087
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6087) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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)]) -> 27  ;  (delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 26  ;  (delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 29  ;  (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)]) -> 28  ;  (mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 27  ;  (mem([e, nil])) -> BOT -> 27
}
Sat witness: Yes: ((delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT, {
_nu -> cons(b, cons(a, nil))  ;  i -> a  ;  l -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 48, which took 0.051024 s (model generation: 0.048212,  model checking: 0.002812):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079, q_gen_6087, q_gen_6111},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6063
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6087
<cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6063) -> q_gen_6087
<cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6087
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6087
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6074) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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)]) -> 27  ;  (delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 29  ;  (delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 29  ;  (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)]) -> 28  ;  (mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 27  ;  (mem([e, nil])) -> BOT -> 27
}
Sat witness: Yes: ((delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]), {
_hu -> cons(a, cons(a, nil))  ;  h -> b  ;  t -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 49, which took 0.058646 s (model generation: 0.055944,  model checking: 0.002702):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079, q_gen_6087, q_gen_6111},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6087
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6087
<cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6087
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6087
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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]) -> 29  ;  (delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 29  ;  (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)]) -> 28  ;  (mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 28  ;  (mem([e, nil])) -> BOT -> 28
}
Sat witness: Yes: (() -> mem([h, cons(h, t)]), {
h -> b  ;  t -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 50, which took 0.059968 s (model generation: 0.057020,  model checking: 0.002948):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079, q_gen_6087, q_gen_6111},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6087
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6087
<cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6087
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6087
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<cons>(q_gen_6061, q_gen_6084) -> q_gen_6056
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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)]) -> 30  ;  (delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 29  ;  (delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 29  ;  (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]) -> 29  ;  (mem([e, nil])) -> BOT -> 29
}
Sat witness: Yes: ((mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]), {
e -> a  ;  h -> b  ;  t -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 51, which took 0.071536 s (model generation: 0.064892,  model checking: 0.006644):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079, q_gen_6087, q_gen_6111},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6087
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6087
<cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6087
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6087
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6063) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<cons>(q_gen_6061, q_gen_6074) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<cons>(q_gen_6061, q_gen_6084) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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)]) -> 30  ;  (delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 29  ;  (delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 29  ;  (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)]) -> 31  ;  (mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 29  ;  (mem([e, nil])) -> BOT -> 29
}
Sat witness: Yes: ((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, cons(b, nil))  ;  x -> a
})

-------------------------------------------
Step 52, which took 0.115699 s (model generation: 0.069892,  model checking: 0.045807):

Model:
|_
{
delete -> 
{{{
Q={q_gen_6058, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6069, q_gen_6070, q_gen_6076, q_gen_6079, q_gen_6087, q_gen_6111},
Q_f={q_gen_6058},
Delta=
{
<cons>(q_gen_6070, q_gen_6069) -> q_gen_6069
<nil>() -> q_gen_6069
<a>() -> q_gen_6070
<b>() -> q_gen_6070
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6063
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6063
<cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6063) -> q_gen_6063
<nil, nil>() -> q_gen_6063
<cons, b>(q_gen_6070, q_gen_6069) -> q_gen_6064
<nil, a>() -> q_gen_6064
<a, nil>() -> q_gen_6065
<b, nil>() -> q_gen_6065
<a, a>() -> q_gen_6066
<a, b>() -> q_gen_6066
<b, a>() -> q_gen_6066
<b, b>() -> q_gen_6066
<cons, a>(q_gen_6070, q_gen_6069) -> q_gen_6076
<nil, b>() -> q_gen_6076
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6087
<cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6087
<cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6087
<a, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<b, cons>(q_gen_6070, q_gen_6069) -> q_gen_6111
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6087) -> q_gen_6058
<a, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<a, nil, nil>() -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6087) -> q_gen_6058
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6063) -> q_gen_6058
<b, cons, nil>(q_gen_6070, q_gen_6069) -> q_gen_6058
<b, nil, nil>() -> q_gen_6058
<a, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6063) -> q_gen_6079
<a, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6064, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6064, q_gen_6087) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6065, q_gen_6076, q_gen_6063) -> q_gen_6079
<b, cons, cons>(q_gen_6066, q_gen_6111, q_gen_6076, q_gen_6087) -> q_gen_6079
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  mem -> 
{{{
Q={q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6060, q_gen_6061, q_gen_6067, q_gen_6074, q_gen_6084},
Q_f={q_gen_6055},
Delta=
{
<nil>() -> q_gen_6056
<b>() -> q_gen_6057
<cons>(q_gen_6057, q_gen_6056) -> q_gen_6060
<cons>(q_gen_6057, q_gen_6060) -> q_gen_6060
<a>() -> q_gen_6061
<cons>(q_gen_6057, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6057, q_gen_6084) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6060) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6074) -> q_gen_6074
<cons>(q_gen_6061, q_gen_6056) -> q_gen_6084
<cons>(q_gen_6061, q_gen_6084) -> q_gen_6084
<a, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6056) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6061, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6056) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6074) -> q_gen_6055
<b, cons>(q_gen_6057, q_gen_6084) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6060) -> q_gen_6055
<b, cons>(q_gen_6061, q_gen_6074) -> q_gen_6055
<a, cons>(q_gen_6057, q_gen_6056) -> q_gen_6067
<a, cons>(q_gen_6057, q_gen_6060) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6056) -> q_gen_6067
<b, cons>(q_gen_6061, q_gen_6084) -> q_gen_6067
}

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

}
--
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)]) -> 31  ;  (delete([h, t, _hu])) -> delete([h, cons(h, t), _hu]) -> 30  ;  (delete([i, l, _nu]) /\ mem([i, _nu])) -> BOT -> 30  ;  (delete([x, t, _iu]) /\ not eq_elt([x, h])) -> delete([x, cons(h, t), cons(h, _iu)]) -> 34  ;  (mem([e, t]) /\ not eq_elt([e, h])) -> mem([e, cons(h, t)]) -> 32  ;  (mem([e, cons(h, t)]) /\ not eq_elt([e, h])) -> mem([e, t]) -> 30  ;  (mem([e, nil])) -> BOT -> 30
}
Sat witness: Yes: ((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, cons(b, nil)))  ;  x -> a
})

Total time: 1.533952
Reason for stopping: Proved