Solving ../../benchmarks/true/member_equal_ab.smt2...

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


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.527913 seconds.
Proved
Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4424, q_gen_4427},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4416, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4416, q_gen_4424) -> q_gen_4424
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4424) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<cons>(q_gen_4419, q_gen_4427) -> q_gen_4427
<a, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.003990 s (model generation: 0.003844,  model checking: 0.000146):

Model:
|_
{
memberl -> 
{{{
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:
{
() -> 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: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 1, which took 0.004474 s (model generation: 0.003534,  model checking: 0.000940):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
}

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

}
--
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: Yes: ((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.003645 s (model generation: 0.003551,  model checking: 0.000094):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416},
Q_f={q_gen_4414},
Delta=
{
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4415
<nil>() -> q_gen_4415
<a>() -> q_gen_4416
<b>() -> q_gen_4416
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
}

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

}
--
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: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> memberl([e, t1]), {
e -> b  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 3, which took 0.003824 s (model generation: 0.003778,  model checking: 0.000046):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416},
Q_f={q_gen_4414},
Delta=
{
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4415
<nil>() -> q_gen_4415
<a>() -> q_gen_4416
<b>() -> q_gen_4416
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, nil>() -> q_gen_4414
}

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

}
--
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: Yes: ((memberl([e, nil])) -> BOT, {
e -> b
})

-------------------------------------------
Step 4, which took 0.004927 s (model generation: 0.003894,  model checking: 0.001033):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<a>() -> q_gen_4419
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.005931 s (model generation: 0.004612,  model checking: 0.001319):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<a>() -> q_gen_4419
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: ((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.010638 s (model generation: 0.007696,  model checking: 0.002942):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 7, which took 0.011356 s (model generation: 0.010021,  model checking: 0.001335):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: ((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.012017 s (model generation: 0.011324,  model checking: 0.000693):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420},
Q_f={q_gen_4414},
Delta=
{
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4415
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: ((memberl([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> memberl([e, t1]), {
e -> a  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 9, which took 0.012301 s (model generation: 0.011587,  model checking: 0.000714):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 10, which took 0.012922 s (model generation: 0.010202,  model checking: 0.002720):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: ((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.019215 s (model generation: 0.017212,  model checking: 0.002003):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420},
Q_f={q_gen_4414},
Delta=
{
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4415
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<a, nil>() -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: ((memberl([e, nil])) -> BOT, {
e -> a
})

-------------------------------------------
Step 12, which took 0.020371 s (model generation: 0.016853,  model checking: 0.003518):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4427},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: ((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.014478 s (model generation: 0.013400,  model checking: 0.001078):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4427},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 14, which took 0.024367 s (model generation: 0.017562,  model checking: 0.006805):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4427},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4427
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: ((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.020674 s (model generation: 0.018570,  model checking: 0.002104):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4427},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: ((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.013914 s (model generation: 0.012418,  model checking: 0.001496):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4427, q_gen_4433},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4433
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4433) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4433) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 17, which took 0.021505 s (model generation: 0.017938,  model checking: 0.003567):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4427, q_gen_4433},
Q_f={q_gen_4414},
Delta=
{
<cons>(q_gen_4416, q_gen_4418) -> q_gen_4415
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4433
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4433) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4433) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: ((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.028123 s (model generation: 0.020760,  model checking: 0.007363):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4424, q_gen_4427},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4416, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<a, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 19, which took 0.026287 s (model generation: 0.024067,  model checking: 0.002220):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4427, q_gen_4433},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<cons>(q_gen_4416, q_gen_4418) -> q_gen_4433
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4433
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4433) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4433) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4433) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: ((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.025578 s (model generation: 0.022556,  model checking: 0.003022):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4427, q_gen_4433},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4416, q_gen_4418) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4433
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4433) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4433) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: ((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.027735 s (model generation: 0.023234,  model checking: 0.004501):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4424, q_gen_4427},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4416, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<a, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 22, which took 0.031617 s (model generation: 0.024911,  model checking: 0.006706):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4424, q_gen_4427},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4416, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<a, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: ((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.020972 s (model generation: 0.018620,  model checking: 0.002352):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4424, q_gen_4427},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4416, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4427) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<a, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: ((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.025087 s (model generation: 0.022969,  model checking: 0.002118):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4424, q_gen_4427},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4416, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<cons>(q_gen_4419, q_gen_4427) -> q_gen_4427
<a, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 25, which took 0.019405 s (model generation: 0.015975,  model checking: 0.003430):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4424, q_gen_4427},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4416, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<cons>(q_gen_4419, q_gen_4427) -> q_gen_4427
<a, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: ((memberl([e, t1]) /\ not eq_elt([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(a, cons(a, cons(b, cons(b, nil))))
})

-------------------------------------------
Step 26, which took 0.051107 s (model generation: 0.021358,  model checking: 0.029749):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4424, q_gen_4427},
Q_f={q_gen_4414},
Delta=
{
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4416, q_gen_4418) -> q_gen_4418
<cons>(q_gen_4419, q_gen_4424) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<cons>(q_gen_4419, q_gen_4427) -> q_gen_4427
<a, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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: Yes: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(b, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 27, which took 0.026904 s (model generation: 0.018018,  model checking: 0.008886):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_4414, q_gen_4415, q_gen_4416, q_gen_4418, q_gen_4419, q_gen_4420, q_gen_4424, q_gen_4427},
Q_f={q_gen_4414},
Delta=
{
<cons>(q_gen_4416, q_gen_4424) -> q_gen_4415
<nil>() -> q_gen_4415
<b>() -> q_gen_4416
<cons>(q_gen_4416, q_gen_4415) -> q_gen_4418
<cons>(q_gen_4416, q_gen_4418) -> q_gen_4418
<a>() -> q_gen_4419
<cons>(q_gen_4416, q_gen_4427) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4418) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4424) -> q_gen_4424
<cons>(q_gen_4419, q_gen_4415) -> q_gen_4427
<cons>(q_gen_4419, q_gen_4427) -> q_gen_4427
<a, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4415) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4419, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4415) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4424) -> q_gen_4414
<b, cons>(q_gen_4416, q_gen_4427) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4418) -> q_gen_4414
<b, cons>(q_gen_4419, q_gen_4424) -> q_gen_4414
<a, cons>(q_gen_4416, q_gen_4415) -> q_gen_4420
<a, cons>(q_gen_4416, q_gen_4418) -> q_gen_4420
<a, nil>() -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4415) -> q_gen_4420
<b, cons>(q_gen_4419, q_gen_4427) -> q_gen_4420
<b, nil>() -> q_gen_4420
}

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

}
--
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)]) -> 31  ;  (memberl([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> memberl([e, t1]) -> 28  ;  (memberl([e, nil])) -> BOT -> 27  ;  (memberl([i, l2])) -> memberl([i, l2]) -> 26
}
Sat witness: Yes: ((memberl([e, t1]) /\ not eq_elt([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(b, cons(a, cons(b, cons(b, nil))))
})

Total time: 0.527913
Reason for stopping: Proved