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


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.648161 seconds.
Proved
Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2458, q_gen_2461},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2450, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2450, q_gen_2458) -> q_gen_2458
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2458) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<cons>(q_gen_2453, q_gen_2461) -> q_gen_2461
<a, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010415 s (model generation: 0.010078,  model checking: 0.000337):

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

}

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

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

Teacher's answer:
New clause system:
{
() -> 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.010996 s (model generation: 0.010229,  model checking: 0.000767):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
}

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

}
--
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.012532 s (model generation: 0.010763,  model checking: 0.001769):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450},
Q_f={q_gen_2448},
Delta=
{
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2449
<nil>() -> q_gen_2449
<a>() -> q_gen_2450
<b>() -> q_gen_2450
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
}

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

}
--
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.011547 s (model generation: 0.011401,  model checking: 0.000146):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450},
Q_f={q_gen_2448},
Delta=
{
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2449
<nil>() -> q_gen_2449
<a>() -> q_gen_2450
<b>() -> q_gen_2450
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, nil>() -> q_gen_2448
}

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

}
--
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.011757 s (model generation: 0.011305,  model checking: 0.000452):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<a>() -> q_gen_2453
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.013774 s (model generation: 0.011612,  model checking: 0.002162):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<a>() -> q_gen_2453
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.015189 s (model generation: 0.012391,  model checking: 0.002798):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.016126 s (model generation: 0.012987,  model checking: 0.003139):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.016015 s (model generation: 0.014015,  model checking: 0.002000):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2448},
Delta=
{
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2449
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.016871 s (model generation: 0.015441,  model checking: 0.001430):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.017703 s (model generation: 0.016126,  model checking: 0.001577):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.018307 s (model generation: 0.017021,  model checking: 0.001286):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2448},
Delta=
{
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2449
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<a, nil>() -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.019520 s (model generation: 0.017089,  model checking: 0.002431):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2461},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.020696 s (model generation: 0.018444,  model checking: 0.002252):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2461},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.026406 s (model generation: 0.019990,  model checking: 0.006416):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2461},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2461
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.023612 s (model generation: 0.021031,  model checking: 0.002581):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2461},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.025402 s (model generation: 0.022274,  model checking: 0.003128):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2461, q_gen_2467},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2467
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2467) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2467) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.030228 s (model generation: 0.024247,  model checking: 0.005981):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2461, q_gen_2467},
Q_f={q_gen_2448},
Delta=
{
<cons>(q_gen_2450, q_gen_2452) -> q_gen_2449
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2467
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2467) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2467) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.035023 s (model generation: 0.025898,  model checking: 0.009125):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2458, q_gen_2461},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2450, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<a, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.031499 s (model generation: 0.027118,  model checking: 0.004381):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2461, q_gen_2467},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<cons>(q_gen_2450, q_gen_2452) -> q_gen_2467
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2467
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2467) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2467) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2467) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.033331 s (model generation: 0.028768,  model checking: 0.004563):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2461, q_gen_2467},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2450, q_gen_2452) -> q_gen_2452
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2467
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2467) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2467) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.040533 s (model generation: 0.031189,  model checking: 0.009344):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2458, q_gen_2461},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2450, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<a, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.046275 s (model generation: 0.032932,  model checking: 0.013343):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2458, q_gen_2461},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2450, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<a, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.041081 s (model generation: 0.035433,  model checking: 0.005648):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2458, q_gen_2461},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2450, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2461) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<a, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.038474 s (model generation: 0.036229,  model checking: 0.002245):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2458, q_gen_2461},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2450, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<cons>(q_gen_2453, q_gen_2461) -> q_gen_2461
<a, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.021984 s (model generation: 0.018861,  model checking: 0.003123):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2458, q_gen_2461},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2450, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<cons>(q_gen_2453, q_gen_2461) -> q_gen_2461
<a, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.020561 s (model generation: 0.016054,  model checking: 0.004507):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_2448, q_gen_2449, q_gen_2450, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2458, q_gen_2461},
Q_f={q_gen_2448},
Delta=
{
<nil>() -> q_gen_2449
<b>() -> q_gen_2450
<cons>(q_gen_2450, q_gen_2449) -> q_gen_2452
<cons>(q_gen_2450, q_gen_2452) -> q_gen_2452
<a>() -> q_gen_2453
<cons>(q_gen_2450, q_gen_2458) -> q_gen_2458
<cons>(q_gen_2450, q_gen_2461) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2452) -> q_gen_2458
<cons>(q_gen_2453, q_gen_2449) -> q_gen_2461
<cons>(q_gen_2453, q_gen_2461) -> q_gen_2461
<a, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2449) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2453, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2449) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2458) -> q_gen_2448
<b, cons>(q_gen_2450, q_gen_2461) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2452) -> q_gen_2448
<b, cons>(q_gen_2453, q_gen_2458) -> q_gen_2448
<a, cons>(q_gen_2450, q_gen_2449) -> q_gen_2454
<a, cons>(q_gen_2450, q_gen_2452) -> q_gen_2454
<a, nil>() -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2449) -> q_gen_2454
<b, cons>(q_gen_2453, q_gen_2461) -> q_gen_2454
<b, nil>() -> q_gen_2454
}

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

}
--
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.648161
Reason for stopping: Proved