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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(elem, P:
{() -> elem([h1, cons(h1, t1)])
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)])
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1])
(elem([e, nil])) -> BOT}
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)])}
(append([_t, _u, _v]) /\ append([_t, _u, _w])) -> eq_eltlist([_v, _w])
)
}

properties:
{(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> elem([h1, cons(h1, t1)]) -> 0
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 0
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 0
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 0
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 0
(elem([e, nil])) -> BOT -> 0
}


Solving took 24.695097 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125, q_gen_183, q_gen_184, q_gen_191},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<a, b>() -> q_gen_183
<b, a>() -> q_gen_183
<cons, cons>(q_gen_111, q_gen_191) -> q_gen_191
<cons, cons>(q_gen_183, q_gen_110) -> q_gen_191
<cons, cons>(q_gen_183, q_gen_191) -> q_gen_191
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_191) -> q_gen_105
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_183, q_gen_191) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
<cons, cons, cons>(q_gen_125, q_gen_184) -> q_gen_184
<cons, nil, cons>(q_gen_111, q_gen_191) -> q_gen_184
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_184
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.011183 s (model generation: 0.010145,  model checking: 0.001038):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
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:
{
() -> append([nil, l2, l2]) -> 0
() -> elem([h1, cons(h1, t1)]) -> 3
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 1
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 1
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 1
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 1
(elem([e, nil])) -> BOT -> 1
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 1, which took 0.010415 s (model generation: 0.010134,  model checking: 0.000281):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
}

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

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

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

-------------------------------------------
Step 2, which took 0.011002 s (model generation: 0.010371,  model checking: 0.000631):

Model:
|_
{
append -> 
{{{
Q={q_gen_105},
Q_f={q_gen_105},
Delta=
{
<nil, nil, nil>() -> q_gen_105
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
}

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

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

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

-------------------------------------------
Step 3, which took 0.012624 s (model generation: 0.010860,  model checking: 0.001764):

Model:
|_
{
append -> 
{{{
Q={q_gen_105},
Q_f={q_gen_105},
Delta=
{
<nil, nil, nil>() -> q_gen_105
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_104, q_gen_103) -> q_gen_103
<nil>() -> q_gen_103
<a>() -> q_gen_104
<b>() -> q_gen_104
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
}

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

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

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

-------------------------------------------
Step 4, which took 0.011492 s (model generation: 0.011179,  model checking: 0.000313):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111},
Q_f={q_gen_105},
Delta=
{
<nil, nil>() -> q_gen_110
<b, b>() -> q_gen_111
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_104, q_gen_103) -> q_gen_103
<nil>() -> q_gen_103
<a>() -> q_gen_104
<b>() -> q_gen_104
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
}

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

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

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

-------------------------------------------
Step 5, which took 0.012322 s (model generation: 0.012143,  model checking: 0.000179):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111},
Q_f={q_gen_105},
Delta=
{
<nil, nil>() -> q_gen_110
<b, b>() -> q_gen_111
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_104, q_gen_103) -> q_gen_103
<nil>() -> q_gen_103
<a>() -> q_gen_104
<b>() -> q_gen_104
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, nil>() -> q_gen_102
}

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

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

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

-------------------------------------------
Step 6, which took 0.014078 s (model generation: 0.011733,  model checking: 0.002345):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111},
Q_f={q_gen_105},
Delta=
{
<nil, nil>() -> q_gen_110
<b, b>() -> q_gen_111
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<a>() -> q_gen_108
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 7, which took 0.012730 s (model generation: 0.012231,  model checking: 0.000499):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111},
Q_f={q_gen_105},
Delta=
{
<nil, nil>() -> q_gen_110
<b, b>() -> q_gen_111
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<a>() -> q_gen_108
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 8, which took 0.014360 s (model generation: 0.012424,  model checking: 0.001936):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111},
Q_f={q_gen_105},
Delta=
{
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<a>() -> q_gen_108
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 9, which took 0.015684 s (model generation: 0.013543,  model checking: 0.002141):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111},
Q_f={q_gen_105},
Delta=
{
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 10, which took 0.018125 s (model generation: 0.014678,  model checking: 0.003447):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 11, which took 0.017220 s (model generation: 0.015355,  model checking: 0.001865):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 12, which took 0.018894 s (model generation: 0.015695,  model checking: 0.003199):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 13, which took 0.017363 s (model generation: 0.016863,  model checking: 0.000500):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_108, q_gen_103) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<a, cons>(q_gen_104, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 14, which took 0.019078 s (model generation: 0.018020,  model checking: 0.001058):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_108, q_gen_103) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<a, cons>(q_gen_104, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 15, which took 0.023189 s (model generation: 0.018534,  model checking: 0.004655):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_108, q_gen_103) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<a, cons>(q_gen_104, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 16, which took 0.021396 s (model generation: 0.020430,  model checking: 0.000966):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_108, q_gen_103) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<a, cons>(q_gen_104, q_gen_103) -> q_gen_102
<a, cons>(q_gen_104, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 17, which took 0.023473 s (model generation: 0.022146,  model checking: 0.001327):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_108, q_gen_103) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<a, cons>(q_gen_104, q_gen_103) -> q_gen_102
<a, cons>(q_gen_104, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 18, which took 0.023637 s (model generation: 0.022992,  model checking: 0.000645):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_108, q_gen_103) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<a, cons>(q_gen_104, q_gen_103) -> q_gen_102
<a, cons>(q_gen_104, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, nil>() -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 19, which took 0.024507 s (model generation: 0.022813,  model checking: 0.001694):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 20, which took 0.025979 s (model generation: 0.023947,  model checking: 0.002032):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_107) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 21, which took 0.027750 s (model generation: 0.024453,  model checking: 0.003297):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, b, a>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_107) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 22, which took 0.029037 s (model generation: 0.027790,  model checking: 0.001247):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, b, a>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_107) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 23, which took 0.031001 s (model generation: 0.029348,  model checking: 0.001653):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, b, a>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_107) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 24, which took 0.034214 s (model generation: 0.028767,  model checking: 0.005447):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, b, a>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 25, which took 0.036475 s (model generation: 0.033947,  model checking: 0.002528):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, b, a>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_108, q_gen_129) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_104, q_gen_107) -> q_gen_129
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 26, which took 0.043331 s (model generation: 0.036596,  model checking: 0.006735):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_108, q_gen_129) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_104, q_gen_107) -> q_gen_129
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 27, which took 0.041066 s (model generation: 0.039943,  model checking: 0.001123):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_119) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 28, which took 0.044450 s (model generation: 0.041434,  model checking: 0.003016):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_119) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 29, which took 0.050699 s (model generation: 0.044030,  model checking: 0.006669):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_119) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 30, which took 0.049960 s (model generation: 0.048100,  model checking: 0.001860):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 31, which took 0.051973 s (model generation: 0.045182,  model checking: 0.006791):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_119) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_104, q_gen_119) -> q_gen_129
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 32, which took 0.060637 s (model generation: 0.058929,  model checking: 0.001708):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_119) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 33, which took 0.082503 s (model generation: 0.061448,  model checking: 0.021055):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_119) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 34, which took 0.048628 s (model generation: 0.044996,  model checking: 0.003632):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_104, q_gen_129) -> q_gen_107
<cons>(q_gen_108, q_gen_119) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 35, which took 0.065916 s (model generation: 0.061076,  model checking: 0.004840):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_104, q_gen_129) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 36, which took 0.143452 s (model generation: 0.075921,  model checking: 0.067531):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_108, q_gen_129) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_104, q_gen_129) -> q_gen_107
<cons>(q_gen_108, q_gen_119) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 37, which took 0.133776 s (model generation: 0.073475,  model checking: 0.060301):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_108, q_gen_129) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_104, q_gen_129) -> q_gen_107
<cons>(q_gen_108, q_gen_119) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 38, which took 0.140384 s (model generation: 0.074280,  model checking: 0.066104):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_108, q_gen_129) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_119) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 39, which took 0.082952 s (model generation: 0.080857,  model checking: 0.002095):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_119) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 40, which took 0.088776 s (model generation: 0.088537,  model checking: 0.000239):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_117, q_gen_120, q_gen_123, q_gen_124, q_gen_125},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<cons, cons>(q_gen_117, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<b, b>() -> q_gen_111
<a, a>() -> q_gen_117
<b, a>() -> q_gen_117
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, cons, cons>(q_gen_125, q_gen_120) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_117, q_gen_110) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<cons, nil, cons>(q_gen_117, q_gen_110) -> q_gen_120
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_120
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_120
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_104, q_gen_107) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 25
() -> elem([h1, cons(h1, t1)]) -> 24
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 25
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 25
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 25
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 23
(elem([e, nil])) -> BOT -> 23
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 41, which took 0.077923 s (model generation: 0.075591,  model checking: 0.002332):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_122, q_gen_123, q_gen_124, q_gen_125, q_gen_183},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<b, a>() -> q_gen_183
<cons, cons, cons>(q_gen_125, q_gen_122) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_122
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_122
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_122
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_122
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_119) -> q_gen_107
<cons>(q_gen_108, q_gen_129) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_104, q_gen_129) -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 42, which took 0.042766 s (model generation: 0.038437,  model checking: 0.004329):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_122, q_gen_123, q_gen_124, q_gen_125, q_gen_183},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<b, a>() -> q_gen_183
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, cons, cons>(q_gen_125, q_gen_122) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_122
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_122
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_108, q_gen_129) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<cons>(q_gen_108, q_gen_119) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 43, which took 0.096048 s (model generation: 0.092661,  model checking: 0.003387):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_122, q_gen_123, q_gen_124, q_gen_125, q_gen_183},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<b, a>() -> q_gen_183
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, cons, cons>(q_gen_125, q_gen_122) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_122
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_122
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_108, q_gen_129) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 44, which took 0.098079 s (model generation: 0.093129,  model checking: 0.004950):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125, q_gen_183, q_gen_184},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<cons, cons>(q_gen_183, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<b, a>() -> q_gen_183
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, cons, cons>(q_gen_125, q_gen_184) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_184
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_108, q_gen_129) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

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

-------------------------------------------
Step 45, which took 0.123206 s (model generation: 0.097264,  model checking: 0.025942):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125, q_gen_182, q_gen_183},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<cons, cons>(q_gen_183, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<b, a>() -> q_gen_183
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, cons, cons>(q_gen_125, q_gen_182) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_182
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_182
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26
() -> elem([h1, cons(h1, t1)]) -> 26
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 28
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 31
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 29
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 27
(elem([e, nil])) -> BOT -> 27
}
Sat witness: Found: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 46, which took 0.116976 s (model generation: 0.109499,  model checking: 0.007477):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_117, q_gen_123, q_gen_124, q_gen_125, q_gen_153},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<cons, cons>(q_gen_117, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<b, b>() -> q_gen_111
<a, a>() -> q_gen_117
<a, b>() -> q_gen_117
<b, a>() -> q_gen_117
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, cons, cons>(q_gen_125, q_gen_153) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_117, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
<cons, nil, cons>(q_gen_117, q_gen_110) -> q_gen_153
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<cons>(q_gen_104, q_gen_107) -> q_gen_103
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_119) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27
() -> elem([h1, cons(h1, t1)]) -> 27
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 31
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 31
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 29
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 28
(elem([e, nil])) -> BOT -> 28
}
Sat witness: Found: ((append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]), {
_x -> cons(a, cons(b, cons(b, nil)))  ;  i -> b  ;  l1 -> cons(a, cons(b, nil))  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 47, which took 0.124109 s (model generation: 0.121110,  model checking: 0.002999):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_117, q_gen_123, q_gen_124, q_gen_125, q_gen_153},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<cons, cons>(q_gen_117, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<b, b>() -> q_gen_111
<a, a>() -> q_gen_117
<a, b>() -> q_gen_117
<b, a>() -> q_gen_117
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, cons, cons>(q_gen_125, q_gen_153) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_117, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
<cons, nil, cons>(q_gen_117, q_gen_110) -> q_gen_153
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 28
() -> elem([h1, cons(h1, t1)]) -> 28
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 31
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 34
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 30
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 29
(elem([e, nil])) -> BOT -> 29
}
Sat witness: Found: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> nil  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 48, which took 0.099603 s (model generation: 0.093759,  model checking: 0.005844):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125, q_gen_182, q_gen_183},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<cons, cons>(q_gen_183, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<a, b>() -> q_gen_111
<b, b>() -> q_gen_111
<b, a>() -> q_gen_183
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, cons, cons>(q_gen_125, q_gen_182) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_182
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_182
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 29
() -> elem([h1, cons(h1, t1)]) -> 29
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 34
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 34
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 31
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 30
(elem([e, nil])) -> BOT -> 30
}
Sat witness: Found: ((append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]), {
_x -> cons(b, nil)  ;  i -> a  ;  l1 -> cons(a, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 49, which took 1.426212 s (model generation: 0.111997,  model checking: 1.314215):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125, q_gen_183, q_gen_184},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<cons, cons>(q_gen_183, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<a, b>() -> q_gen_183
<b, a>() -> q_gen_183
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
<cons, cons, cons>(q_gen_125, q_gen_184) -> q_gen_184
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_184
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 30
() -> elem([h1, cons(h1, t1)]) -> 30
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 37
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 35
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 32
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 31
(elem([e, nil])) -> BOT -> 31
}
Sat witness: Found: ((append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]), {
_x -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  i -> a  ;  l1 -> cons(b, cons(a, cons(b, nil)))  ;  l2 -> nil
})

-------------------------------------------
Step 50, which took 0.111000 s (model generation: 0.108623,  model checking: 0.002377):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125, q_gen_182, q_gen_183},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<cons, cons>(q_gen_183, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<a, b>() -> q_gen_183
<b, a>() -> q_gen_183
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, cons, cons>(q_gen_125, q_gen_182) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_182
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_182
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129, q_gen_136},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_136) -> q_gen_119
<cons>(q_gen_104, q_gen_136) -> q_gen_129
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<cons>(q_gen_104, q_gen_107) -> q_gen_136
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_136) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_136) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<b, cons>(q_gen_108, q_gen_136) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, cons>(q_gen_104, q_gen_136) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 31
() -> elem([h1, cons(h1, t1)]) -> 31
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 37
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 35
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 32
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 34
(elem([e, nil])) -> BOT -> 32
}
Sat witness: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 51, which took 0.097752 s (model generation: 0.096882,  model checking: 0.000870):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_116, q_gen_123, q_gen_124, q_gen_125, q_gen_153, q_gen_183},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_183, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_116
<cons, cons>(q_gen_183, q_gen_116) -> q_gen_116
<a, b>() -> q_gen_183
<b, a>() -> q_gen_183
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, cons, cons>(q_gen_125, q_gen_153) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_116) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
<cons, nil, cons>(q_gen_111, q_gen_116) -> q_gen_153
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_153
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_153
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 34
() -> elem([h1, cons(h1, t1)]) -> 32
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 37
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 35
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 32
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 34
(elem([e, nil])) -> BOT -> 32
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 52, which took 0.120789 s (model generation: 0.116875,  model checking: 0.003914):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_116, q_gen_123, q_gen_124, q_gen_125, q_gen_153, q_gen_183},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_116) -> q_gen_110
<cons, cons>(q_gen_183, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_116
<cons, cons>(q_gen_183, q_gen_116) -> q_gen_116
<a, b>() -> q_gen_183
<b, a>() -> q_gen_183
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, cons, cons>(q_gen_125, q_gen_153) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_116) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
<cons, nil, cons>(q_gen_111, q_gen_116) -> q_gen_153
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_153
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_153
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 35
() -> elem([h1, cons(h1, t1)]) -> 33
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 37
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 38
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 33
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 35
(elem([e, nil])) -> BOT -> 33
}
Sat witness: Found: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 53, which took 0.123742 s (model generation: 0.121824,  model checking: 0.001918):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_122, q_gen_123, q_gen_124, q_gen_125, q_gen_132, q_gen_183},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons>(q_gen_111, q_gen_132) -> q_gen_132
<cons, cons>(q_gen_183, q_gen_110) -> q_gen_132
<cons, cons>(q_gen_183, q_gen_132) -> q_gen_132
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_132
<a, b>() -> q_gen_183
<b, a>() -> q_gen_183
<cons, cons, cons>(q_gen_125, q_gen_122) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_122
<cons, nil, cons>(q_gen_111, q_gen_132) -> q_gen_122
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_122
<nil, cons, cons>(q_gen_111, q_gen_132) -> q_gen_122
<nil, cons, cons>(q_gen_183, q_gen_132) -> q_gen_122
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_122
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_129
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_104, q_gen_129) -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 35
() -> elem([h1, cons(h1, t1)]) -> 36
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 37
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 38
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 34
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 35
(elem([e, nil])) -> BOT -> 34
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 54, which took 0.129107 s (model generation: 0.120345,  model checking: 0.008762):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_122, q_gen_123, q_gen_124, q_gen_125, q_gen_132, q_gen_183},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<cons, cons>(q_gen_111, q_gen_132) -> q_gen_132
<cons, cons>(q_gen_183, q_gen_110) -> q_gen_132
<cons, cons>(q_gen_183, q_gen_132) -> q_gen_132
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_132
<a, b>() -> q_gen_183
<b, a>() -> q_gen_183
<cons, cons, cons>(q_gen_125, q_gen_122) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_122
<cons, nil, cons>(q_gen_111, q_gen_132) -> q_gen_122
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_122
<nil, cons, cons>(q_gen_111, q_gen_132) -> q_gen_122
<nil, cons, cons>(q_gen_183, q_gen_132) -> q_gen_122
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_122
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 36
() -> elem([h1, cons(h1, t1)]) -> 37
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 40
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 38
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 35
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 36
(elem([e, nil])) -> BOT -> 35
}
Sat witness: Found: ((append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]), {
_x -> cons(b, cons(b, nil))  ;  i -> a  ;  l1 -> cons(b, cons(a, nil))  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 55, which took 0.136937 s (model generation: 0.118663,  model checking: 0.018274):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125, q_gen_183, q_gen_184, q_gen_191},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<a, b>() -> q_gen_183
<b, a>() -> q_gen_183
<cons, cons>(q_gen_183, q_gen_110) -> q_gen_191
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
<cons, cons, cons>(q_gen_125, q_gen_184) -> q_gen_184
<cons, nil, cons>(q_gen_111, q_gen_191) -> q_gen_184
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_184
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 37
() -> elem([h1, cons(h1, t1)]) -> 38
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 40
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 41
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 36
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 37
(elem([e, nil])) -> BOT -> 36
}
Sat witness: Found: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> cons(b, cons(a, cons(a, cons(a, cons(b, nil)))))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, cons(a, cons(a, cons(b, nil)))))  ;  t1 -> nil
})

-------------------------------------------
Step 56, which took 0.106798 s (model generation: 0.097881,  model checking: 0.008917):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125, q_gen_183, q_gen_184, q_gen_191},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<cons, cons>(q_gen_111, q_gen_191) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<a, b>() -> q_gen_183
<b, a>() -> q_gen_183
<cons, cons>(q_gen_183, q_gen_110) -> q_gen_191
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
<cons, cons, cons>(q_gen_125, q_gen_184) -> q_gen_184
<cons, nil, cons>(q_gen_111, q_gen_191) -> q_gen_184
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_184
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 38
() -> elem([h1, cons(h1, t1)]) -> 39
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 43
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 41
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 37
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 38
(elem([e, nil])) -> BOT -> 37
}
Sat witness: Found: ((append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]), {
_x -> cons(a, cons(a, cons(a, nil)))  ;  i -> b  ;  l1 -> cons(a, cons(a, cons(b, nil)))  ;  l2 -> nil
})

-------------------------------------------
Step 57, which took 0.193854 s (model generation: 0.169166,  model checking: 0.024688):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125, q_gen_183, q_gen_184, q_gen_191},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<a, b>() -> q_gen_183
<b, a>() -> q_gen_183
<cons, cons>(q_gen_111, q_gen_191) -> q_gen_191
<cons, cons>(q_gen_183, q_gen_110) -> q_gen_191
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_183, q_gen_191) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
<cons, cons, cons>(q_gen_125, q_gen_184) -> q_gen_184
<cons, nil, cons>(q_gen_111, q_gen_191) -> q_gen_184
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_184
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 39
() -> elem([h1, cons(h1, t1)]) -> 40
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 43
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 44
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 38
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 39
(elem([e, nil])) -> BOT -> 38
}
Sat witness: Found: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, cons(a, nil)))  ;  t1 -> nil
})

-------------------------------------------
Step 58, which took 0.183466 s (model generation: 0.147457,  model checking: 0.036009):

Model:
|_
{
append -> 
{{{
Q={q_gen_105, q_gen_110, q_gen_111, q_gen_123, q_gen_124, q_gen_125, q_gen_183, q_gen_184, q_gen_191},
Q_f={q_gen_105},
Delta=
{
<cons>(q_gen_124, q_gen_123) -> q_gen_123
<nil>() -> q_gen_123
<a>() -> q_gen_124
<b>() -> q_gen_124
<cons, cons>(q_gen_111, q_gen_110) -> q_gen_110
<nil, cons>(q_gen_124, q_gen_123) -> q_gen_110
<nil, nil>() -> q_gen_110
<a, a>() -> q_gen_111
<b, b>() -> q_gen_111
<a, b>() -> q_gen_183
<b, a>() -> q_gen_183
<cons, cons>(q_gen_111, q_gen_191) -> q_gen_191
<cons, cons>(q_gen_183, q_gen_110) -> q_gen_191
<cons, cons, cons>(q_gen_125, q_gen_105) -> q_gen_105
<cons, nil, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_111, q_gen_191) -> q_gen_105
<nil, cons, cons>(q_gen_183, q_gen_110) -> q_gen_105
<nil, cons, cons>(q_gen_183, q_gen_191) -> q_gen_105
<nil, nil, cons>(q_gen_124, q_gen_123) -> q_gen_105
<nil, nil, nil>() -> q_gen_105
<a, a, a>() -> q_gen_125
<a, b, a>() -> q_gen_125
<b, a, b>() -> q_gen_125
<b, b, b>() -> q_gen_125
<cons, cons, cons>(q_gen_125, q_gen_184) -> q_gen_184
<cons, nil, cons>(q_gen_111, q_gen_191) -> q_gen_184
<cons, nil, cons>(q_gen_183, q_gen_110) -> q_gen_184
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_102, q_gen_103, q_gen_104, q_gen_107, q_gen_108, q_gen_112, q_gen_119, q_gen_129},
Q_f={q_gen_102},
Delta=
{
<nil>() -> q_gen_103
<b>() -> q_gen_104
<cons>(q_gen_104, q_gen_103) -> q_gen_107
<cons>(q_gen_104, q_gen_107) -> q_gen_107
<a>() -> q_gen_108
<cons>(q_gen_104, q_gen_119) -> q_gen_119
<cons>(q_gen_104, q_gen_129) -> q_gen_119
<cons>(q_gen_108, q_gen_107) -> q_gen_119
<cons>(q_gen_108, q_gen_119) -> q_gen_119
<cons>(q_gen_108, q_gen_103) -> q_gen_129
<cons>(q_gen_108, q_gen_129) -> q_gen_129
<a, cons>(q_gen_104, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_129) -> q_gen_102
<a, cons>(q_gen_108, q_gen_103) -> q_gen_102
<a, cons>(q_gen_108, q_gen_107) -> q_gen_102
<a, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_108, q_gen_129) -> q_gen_102
<b, cons>(q_gen_104, q_gen_103) -> q_gen_102
<b, cons>(q_gen_104, q_gen_107) -> q_gen_102
<b, cons>(q_gen_104, q_gen_119) -> q_gen_102
<b, cons>(q_gen_104, q_gen_129) -> q_gen_102
<b, cons>(q_gen_108, q_gen_107) -> q_gen_102
<b, cons>(q_gen_108, q_gen_119) -> q_gen_102
<a, cons>(q_gen_104, q_gen_103) -> q_gen_112
<a, cons>(q_gen_104, q_gen_107) -> q_gen_112
<a, nil>() -> q_gen_112
<b, cons>(q_gen_108, q_gen_103) -> q_gen_112
<b, cons>(q_gen_108, q_gen_129) -> q_gen_112
<b, nil>() -> q_gen_112
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 40
() -> elem([h1, cons(h1, t1)]) -> 41
(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 44
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 47
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 39
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 40
(elem([e, nil])) -> BOT -> 39
}
Sat witness: Found: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> cons(b, cons(a, cons(a, cons(b, cons(a, cons(b, nil))))))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, cons(a, cons(b, cons(a, cons(b, nil))))))  ;  t1 -> nil
})

Total time: 24.695097
Reason for stopping: Proved