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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(memberl, P:
{() -> memberl([h1, cons(h1, t1)])
(memberl([e, t1]) /\ not eq_elt([e, h1])) -> memberl([e, cons(h1, t1)])
(memberl([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> memberl([e, t1])
(memberl([e, nil])) -> BOT}
)
}

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


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

Clause system for inference is:

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


Solving took 0.640773 seconds.
Proved
Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5255, q_gen_5258},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5247, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5247, q_gen_5255) -> q_gen_5255
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5255) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<cons>(q_gen_5250, q_gen_5258) -> q_gen_5258
<a, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.040430 s (model generation: 0.040244,  model checking: 0.000186):

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

}

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

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

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

-------------------------------------------
Step 1, which took 0.010271 s (model generation: 0.009762,  model checking: 0.000509):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
}

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

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

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

-------------------------------------------
Step 2, which took 0.009859 s (model generation: 0.009677,  model checking: 0.000182):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247},
Q_f={q_gen_5245},
Delta=
{
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5246
<nil>() -> q_gen_5246
<a>() -> q_gen_5247
<b>() -> q_gen_5247
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
}

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

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

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

-------------------------------------------
Step 3, which took 0.009589 s (model generation: 0.009517,  model checking: 0.000072):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247},
Q_f={q_gen_5245},
Delta=
{
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5246
<nil>() -> q_gen_5246
<a>() -> q_gen_5247
<b>() -> q_gen_5247
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, nil>() -> q_gen_5245
}

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

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

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

-------------------------------------------
Step 4, which took 0.010283 s (model generation: 0.009913,  model checking: 0.000370):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<a>() -> q_gen_5250
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 5, which took 0.011439 s (model generation: 0.010575,  model checking: 0.000864):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<a>() -> q_gen_5250
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 6, which took 0.011994 s (model generation: 0.010496,  model checking: 0.001498):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 7, which took 0.014386 s (model generation: 0.012798,  model checking: 0.001588):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 8, which took 0.013111 s (model generation: 0.012131,  model checking: 0.000980):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251},
Q_f={q_gen_5245},
Delta=
{
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5246
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 9, which took 0.019901 s (model generation: 0.018994,  model checking: 0.000907):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 10, which took 0.016577 s (model generation: 0.015823,  model checking: 0.000754):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 11, which took 0.017363 s (model generation: 0.016660,  model checking: 0.000703):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251},
Q_f={q_gen_5245},
Delta=
{
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5246
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<a, nil>() -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 12, which took 0.015102 s (model generation: 0.013697,  model checking: 0.001405):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5258},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 12
(memberl([e, t1]) /\ not eq_elt([e, h1])) -> memberl([e, cons(h1, t1)]) -> 13
(memberl([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> memberl([e, t1]) -> 13
(memberl([e, nil])) -> BOT -> 13
(memberl([i, l2])) -> memberl([i, l2]) -> 11
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_elt([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 13, which took 0.017894 s (model generation: 0.016452,  model checking: 0.001442):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5258},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 15
(memberl([e, t1]) /\ not eq_elt([e, h1])) -> memberl([e, cons(h1, t1)]) -> 13
(memberl([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> memberl([e, t1]) -> 13
(memberl([e, nil])) -> BOT -> 13
(memberl([i, l2])) -> memberl([i, l2]) -> 12
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 14, which took 0.019704 s (model generation: 0.015976,  model checking: 0.003728):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5258},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5258
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 15, which took 0.019502 s (model generation: 0.017737,  model checking: 0.001765):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5258},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 16, which took 0.021579 s (model generation: 0.019468,  model checking: 0.002111):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5258, q_gen_5264},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5264
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5264) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5264) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 17, which took 0.024638 s (model generation: 0.020768,  model checking: 0.003870):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5258, q_gen_5264},
Q_f={q_gen_5245},
Delta=
{
<cons>(q_gen_5247, q_gen_5249) -> q_gen_5246
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5264
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5264) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5264) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 18, which took 0.033231 s (model generation: 0.024321,  model checking: 0.008910):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5255, q_gen_5258},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5247, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<a, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 19, which took 0.024423 s (model generation: 0.021514,  model checking: 0.002909):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5258, q_gen_5264},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<cons>(q_gen_5247, q_gen_5249) -> q_gen_5264
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5264
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5264) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5264) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5264) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 20, which took 0.027212 s (model generation: 0.024546,  model checking: 0.002666):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5258, q_gen_5264},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5247, q_gen_5249) -> q_gen_5249
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5264
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5264) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5264) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 21, which took 0.033043 s (model generation: 0.027507,  model checking: 0.005536):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5255, q_gen_5258},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5247, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<a, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

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

-------------------------------------------
Step 22, which took 0.033713 s (model generation: 0.025978,  model checking: 0.007735):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5255, q_gen_5258},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5247, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<a, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 24
(memberl([e, t1]) /\ not eq_elt([e, h1])) -> memberl([e, cons(h1, t1)]) -> 25
(memberl([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> memberl([e, t1]) -> 23
(memberl([e, nil])) -> BOT -> 22
(memberl([i, l2])) -> memberl([i, l2]) -> 21
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_elt([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 23, which took 0.032233 s (model generation: 0.029305,  model checking: 0.002928):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5255, q_gen_5258},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5247, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5258) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<a, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 24
(memberl([e, t1]) /\ not eq_elt([e, h1])) -> memberl([e, cons(h1, t1)]) -> 25
(memberl([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> memberl([e, t1]) -> 26
(memberl([e, nil])) -> BOT -> 23
(memberl([i, l2])) -> memberl([i, l2]) -> 22
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> memberl([e, t1]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 24, which took 0.032588 s (model generation: 0.030145,  model checking: 0.002443):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5255, q_gen_5258},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5247, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<cons>(q_gen_5250, q_gen_5258) -> q_gen_5258
<a, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 27
(memberl([e, t1]) /\ not eq_elt([e, h1])) -> memberl([e, cons(h1, t1)]) -> 25
(memberl([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> memberl([e, t1]) -> 26
(memberl([e, nil])) -> BOT -> 24
(memberl([i, l2])) -> memberl([i, l2]) -> 23
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 25, which took 0.036763 s (model generation: 0.031010,  model checking: 0.005753):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5255, q_gen_5258},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5247, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<cons>(q_gen_5250, q_gen_5258) -> q_gen_5258
<a, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 27
(memberl([e, t1]) /\ not eq_elt([e, h1])) -> memberl([e, cons(h1, t1)]) -> 28
(memberl([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> memberl([e, t1]) -> 26
(memberl([e, nil])) -> BOT -> 25
(memberl([i, l2])) -> memberl([i, l2]) -> 24
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_elt([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(b, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 26, which took 0.041672 s (model generation: 0.035050,  model checking: 0.006622):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5249, q_gen_5250, q_gen_5251, q_gen_5255, q_gen_5258},
Q_f={q_gen_5245},
Delta=
{
<nil>() -> q_gen_5246
<b>() -> q_gen_5247
<cons>(q_gen_5247, q_gen_5246) -> q_gen_5249
<cons>(q_gen_5247, q_gen_5249) -> q_gen_5249
<a>() -> q_gen_5250
<cons>(q_gen_5247, q_gen_5255) -> q_gen_5255
<cons>(q_gen_5247, q_gen_5258) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5249) -> q_gen_5255
<cons>(q_gen_5250, q_gen_5246) -> q_gen_5258
<cons>(q_gen_5250, q_gen_5258) -> q_gen_5258
<a, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5246) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5250, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5246) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5255) -> q_gen_5245
<b, cons>(q_gen_5247, q_gen_5258) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5249) -> q_gen_5245
<b, cons>(q_gen_5250, q_gen_5255) -> q_gen_5245
<a, cons>(q_gen_5247, q_gen_5246) -> q_gen_5251
<a, cons>(q_gen_5247, q_gen_5249) -> q_gen_5251
<a, nil>() -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5246) -> q_gen_5251
<b, cons>(q_gen_5250, q_gen_5258) -> q_gen_5251
<b, nil>() -> q_gen_5251
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 30
(memberl([e, t1]) /\ not eq_elt([e, h1])) -> memberl([e, cons(h1, t1)]) -> 28
(memberl([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> memberl([e, t1]) -> 27
(memberl([e, nil])) -> BOT -> 26
(memberl([i, l2])) -> memberl([i, l2]) -> 25
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(a, cons(a, cons(b, nil)))
})

Total time: 0.640773
Reason for stopping: Proved