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, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)])}
(append([_kaa, _laa, _maa]) /\ append([_kaa, _laa, _naa])) -> eq_eltlist([_maa, _naa])
)
}

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


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> elem([h1, cons(h1, t1)]) -> 0
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 0
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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 25.181352 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5343, q_gen_5344, q_gen_5362},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<a, b>() -> q_gen_5343
<b, a>() -> q_gen_5343
<cons, cons>(q_gen_5269, q_gen_5362) -> q_gen_5362
<cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5362
<cons, cons>(q_gen_5343, q_gen_5362) -> q_gen_5362
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5362) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5362) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, cons, cons>(q_gen_5283, q_gen_5344) -> q_gen_5344
<cons, nil, cons>(q_gen_5269, q_gen_5362) -> q_gen_5344
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5344
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005935 s (model generation: 0.005154,  model checking: 0.000781):

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 1
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.005152 s (model generation: 0.004755,  model checking: 0.000397):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 1
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.005399 s (model generation: 0.004616,  model checking: 0.000783):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 1
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.004247 s (model generation: 0.004138,  model checking: 0.000109):

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

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

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 1
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.004632 s (model generation: 0.004501,  model checking: 0.000131):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269},
Q_f={q_gen_5263},
Delta=
{
<nil, nil>() -> q_gen_5268
<b, b>() -> q_gen_5269
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
}

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

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 2
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.006329 s (model generation: 0.006254,  model checking: 0.000075):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269},
Q_f={q_gen_5263},
Delta=
{
<nil, nil>() -> q_gen_5268
<b, b>() -> q_gen_5269
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
}

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

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 3
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.009369 s (model generation: 0.007920,  model checking: 0.001449):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269},
Q_f={q_gen_5263},
Delta=
{
<nil, nil>() -> q_gen_5268
<b, b>() -> q_gen_5269
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<a>() -> q_gen_5266
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 4
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.009623 s (model generation: 0.009430,  model checking: 0.000193):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269},
Q_f={q_gen_5263},
Delta=
{
<nil, nil>() -> q_gen_5268
<b, b>() -> q_gen_5269
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<a>() -> q_gen_5266
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 4
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.007283 s (model generation: 0.005615,  model checking: 0.001668):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269},
Q_f={q_gen_5263},
Delta=
{
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<a>() -> q_gen_5266
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 4
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.016750 s (model generation: 0.014411,  model checking: 0.002339):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269},
Q_f={q_gen_5263},
Delta=
{
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 4
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.019935 s (model generation: 0.015330,  model checking: 0.004605):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 7
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]), {
_oaa -> cons(b, cons(b, nil))  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 11, which took 0.019360 s (model generation: 0.016615,  model checking: 0.002745):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 7
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.020074 s (model generation: 0.015919,  model checking: 0.004155):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 7
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.018227 s (model generation: 0.017689,  model checking: 0.000538):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 7
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.020698 s (model generation: 0.019377,  model checking: 0.001321):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270},
Q_f={q_gen_5260},
Delta=
{
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5261
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 7
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.027878 s (model generation: 0.020777,  model checking: 0.007101):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270},
Q_f={q_gen_5260},
Delta=
{
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5261
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 10
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]), {
_oaa -> cons(b, cons(b, nil))  ;  i -> a  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 16, which took 0.026214 s (model generation: 0.024102,  model checking: 0.002112):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270},
Q_f={q_gen_5260},
Delta=
{
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5261
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 10
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.026843 s (model generation: 0.024603,  model checking: 0.002240):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270},
Q_f={q_gen_5260},
Delta=
{
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5261
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 10
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.025865 s (model generation: 0.025112,  model checking: 0.000753):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270},
Q_f={q_gen_5260},
Delta=
{
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5261
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, nil>() -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 10
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.027659 s (model generation: 0.025072,  model checking: 0.002587):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 10
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, cons(b, nil)))
})

-------------------------------------------
Step 20, which took 0.029919 s (model generation: 0.026695,  model checking: 0.003224):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 10
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 0.038426 s (model generation: 0.029449,  model checking: 0.008977):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, b, a>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 13
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]), {
_oaa -> cons(a, cons(b, cons(b, nil)))  ;  i -> a  ;  l1 -> cons(a, cons(b, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 22, which took 0.032110 s (model generation: 0.030273,  model checking: 0.001837):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, b, a>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 13
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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 -> b  ;  t1 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 23, which took 0.035950 s (model generation: 0.031991,  model checking: 0.003959):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, b, a>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 13
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, cons(b, nil))
})

-------------------------------------------
Step 24, which took 0.038986 s (model generation: 0.035721,  model checking: 0.003265):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, b, a>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5261
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 13
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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(b, cons(b, nil))
})

-------------------------------------------
Step 25, which took 0.041113 s (model generation: 0.037261,  model checking: 0.003852):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, b, a>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 13
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 26, which took 0.045557 s (model generation: 0.040131,  model checking: 0.005426):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 16
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]), {
_oaa -> cons(b, cons(a, nil))  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 27, which took 0.045902 s (model generation: 0.044648,  model checking: 0.001254):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 16
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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(a, nil)
})

-------------------------------------------
Step 28, which took 0.051775 s (model generation: 0.048815,  model checking: 0.002960):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 16
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, nil)
})

-------------------------------------------
Step 29, which took 0.057560 s (model generation: 0.049813,  model checking: 0.007747):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 16
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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 -> b  ;  h1 -> a  ;  t1 -> cons(a, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 30, which took 0.053986 s (model generation: 0.051735,  model checking: 0.002251):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 16
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 31, which took 0.073712 s (model generation: 0.059594,  model checking: 0.014118):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 19
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]), {
_oaa -> cons(a, cons(b, cons(a, nil)))  ;  i -> a  ;  l1 -> cons(a, cons(b, nil))  ;  l2 -> cons(b, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 32, which took 0.064339 s (model generation: 0.062825,  model checking: 0.001514):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 19
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.042858 s (model generation: 0.036621,  model checking: 0.006237):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5261
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 19
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.043182 s (model generation: 0.039812,  model checking: 0.003370):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 19
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 35, which took 0.081244 s (model generation: 0.068687,  model checking: 0.012557):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 22
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]), {
_oaa -> cons(b, cons(a, cons(a, cons(b, nil))))  ;  i -> a  ;  l1 -> cons(b, cons(a, nil))  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 36, which took 0.056042 s (model generation: 0.052395,  model checking: 0.003647):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 22
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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 -> b  ;  t1 -> cons(b, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 37, which took 0.093199 s (model generation: 0.051436,  model checking: 0.041763):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5261
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 22
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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 -> b  ;  h1 -> a  ;  t1 -> cons(b, cons(a, cons(b, cons(b, nil))))
})

-------------------------------------------
Step 38, which took 0.100513 s (model generation: 0.093883,  model checking: 0.006630):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 22
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 39, which took 0.097237 s (model generation: 0.095695,  model checking: 0.001542):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 25
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]), {
_oaa -> cons(a, nil)  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 40, which took 0.058233 s (model generation: 0.057809,  model checking: 0.000424):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5275, q_gen_5278, q_gen_5281, q_gen_5282, q_gen_5283},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<cons, cons>(q_gen_5275, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<b, b>() -> q_gen_5269
<a, a>() -> q_gen_5275
<b, a>() -> q_gen_5275
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5275, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<cons, cons, cons>(q_gen_5283, q_gen_5278) -> q_gen_5278
<cons, nil, cons>(q_gen_5275, q_gen_5268) -> q_gen_5278
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5278
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5287, q_gen_5294},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5294) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5294
<cons>(q_gen_5262, q_gen_5294) -> q_gen_5294
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5294) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5294) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5294) -> q_gen_5270
<a, cons>(q_gen_5266, q_gen_5294) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 25
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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.096557 s (model generation: 0.093514,  model checking: 0.003043):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5275, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5301},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<cons, cons>(q_gen_5275, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<b, b>() -> q_gen_5269
<a, a>() -> q_gen_5275
<b, a>() -> q_gen_5275
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5275, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, cons, cons>(q_gen_5283, q_gen_5301) -> q_gen_5301
<cons, nil, cons>(q_gen_5275, q_gen_5268) -> q_gen_5301
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5270
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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)]) -> 27
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 25
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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]) -> 24
(elem([e, nil])) -> BOT -> 24
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 42, which took 0.086427 s (model generation: 0.085362,  model checking: 0.001065):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5275, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5301},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<cons, cons>(q_gen_5275, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<b, b>() -> q_gen_5269
<a, a>() -> q_gen_5275
<b, a>() -> q_gen_5275
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5275, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, cons, cons>(q_gen_5283, q_gen_5301) -> q_gen_5301
<cons, nil, cons>(q_gen_5275, q_gen_5268) -> q_gen_5301
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5287, q_gen_5294},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5294) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5294) -> q_gen_5287
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5294
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5294) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5294) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5294) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5294) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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)]) -> 27
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 25
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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]) -> 27
(elem([e, nil])) -> BOT -> 25
}
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 43, which took 0.072544 s (model generation: 0.070331,  model checking: 0.002213):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5275, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5301},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<cons, cons>(q_gen_5275, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<b, b>() -> q_gen_5269
<a, a>() -> q_gen_5275
<b, a>() -> q_gen_5275
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5275, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, cons, cons>(q_gen_5283, q_gen_5301) -> q_gen_5301
<cons, nil, cons>(q_gen_5275, q_gen_5268) -> q_gen_5301
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5287, q_gen_5294},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5294) -> q_gen_5265
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5294) -> q_gen_5287
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5294
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5294
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5294) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5294) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5294) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5294) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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)]) -> 27
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 25
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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]) -> 27
(elem([e, nil])) -> BOT -> 26
}
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 44, which took 0.088559 s (model generation: 0.088280,  model checking: 0.000279):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5275, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5301},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<cons, cons>(q_gen_5275, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<b, b>() -> q_gen_5269
<a, a>() -> q_gen_5275
<b, a>() -> q_gen_5275
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5275, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, cons, cons>(q_gen_5283, q_gen_5301) -> q_gen_5301
<cons, nil, cons>(q_gen_5275, q_gen_5268) -> q_gen_5301
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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)]) -> 27
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 25
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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]) -> 27
(elem([e, nil])) -> BOT -> 26
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> nil  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 45, which took 0.109055 s (model generation: 0.104310,  model checking: 0.004745):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5343, q_gen_5344},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<b, a>() -> q_gen_5343
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5344
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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)]) -> 27
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 28
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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]) -> 27
(elem([e, nil])) -> BOT -> 26
}
Sat witness: Found: ((append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]), {
_oaa -> cons(b, cons(a, cons(a, nil)))  ;  i -> a  ;  l1 -> cons(b, cons(a, nil))  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 46, which took 0.102680 s (model generation: 0.079734,  model checking: 0.022946):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5343, q_gen_5344},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<b, a>() -> q_gen_5343
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5344
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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)]) -> 28
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 28
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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 -> 27
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 47, which took 0.126526 s (model generation: 0.125137,  model checking: 0.001389):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5342, q_gen_5343},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<a, b>() -> q_gen_5343
<b, a>() -> q_gen_5343
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, cons, cons>(q_gen_5283, q_gen_5342) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5342
<nil, cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5342
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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)]) -> 28
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 28
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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]) -> 31
(elem([e, nil])) -> BOT -> 28
}
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 48, which took 0.130556 s (model generation: 0.110089,  model checking: 0.020467):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5343, q_gen_5344},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<a, b>() -> q_gen_5343
<b, a>() -> q_gen_5343
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5344
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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)]) -> 29
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 29
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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]) -> 32
(elem([e, nil])) -> BOT -> 29
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(b, cons(a, cons(a, cons(b, nil))))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, cons(a, cons(b, nil))))  ;  t1 -> nil
})

-------------------------------------------
Step 49, which took 0.084255 s (model generation: 0.078143,  model checking: 0.006112):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5343, q_gen_5344},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<a, b>() -> q_gen_5343
<b, a>() -> q_gen_5343
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5344
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 32
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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]) -> 32
(elem([e, nil])) -> BOT -> 30
}
Sat witness: Found: ((append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]), {
_oaa -> cons(b, cons(b, cons(a, nil)))  ;  i -> a  ;  l1 -> cons(b, cons(a, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 50, which took 0.143063 s (model generation: 0.135134,  model checking: 0.007929):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5343, q_gen_5344},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<a, b>() -> q_gen_5343
<b, a>() -> q_gen_5343
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5344
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 35
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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]) -> 33
(elem([e, nil])) -> BOT -> 31
}
Sat witness: Found: ((append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]), {
_oaa -> cons(b, cons(b, nil))  ;  i -> a  ;  l1 -> cons(b, cons(a, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 51, which took 0.100836 s (model generation: 0.100339,  model checking: 0.000497):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5343, q_gen_5344, q_gen_5363},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<cons, cons>(q_gen_5269, q_gen_5363) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<a, b>() -> q_gen_5343
<b, a>() -> q_gen_5343
<cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5363
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, nil, cons>(q_gen_5269, q_gen_5363) -> q_gen_5344
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5344
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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)]) -> 33
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 35
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 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]) -> 33
(elem([e, nil])) -> BOT -> 31
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 52, which took 0.140892 s (model generation: 0.138791,  model checking: 0.002101):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5274, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5301, q_gen_5343},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5274) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5274
<cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5274
<a, b>() -> q_gen_5343
<b, a>() -> q_gen_5343
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, cons, cons>(q_gen_5283, q_gen_5301) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5274) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, nil, cons>(q_gen_5269, q_gen_5274) -> q_gen_5301
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5301
<nil, cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5301
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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)]) -> 33
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 35
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 34
(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]) -> 33
(elem([e, nil])) -> BOT -> 32
}
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 53, which took 0.126905 s (model generation: 0.123385,  model checking: 0.003520):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5274, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5301, q_gen_5343},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5274) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5274
<cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5274
<a, b>() -> q_gen_5343
<b, a>() -> q_gen_5343
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, cons, cons>(q_gen_5283, q_gen_5301) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5274) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, nil, cons>(q_gen_5269, q_gen_5274) -> q_gen_5301
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5301
<nil, cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5301
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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]) -> 32
() -> elem([h1, cons(h1, t1)]) -> 34
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 35
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 37
(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]) -> 34
(elem([e, nil])) -> BOT -> 33
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 54, which took 0.175770 s (model generation: 0.167230,  model checking: 0.008540):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5280, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5290, q_gen_5343},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<cons, cons>(q_gen_5269, q_gen_5290) -> q_gen_5290
<cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5290
<cons, cons>(q_gen_5343, q_gen_5290) -> q_gen_5290
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5290
<a, b>() -> q_gen_5343
<b, a>() -> q_gen_5343
<cons, cons, cons>(q_gen_5283, q_gen_5280) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5280
<cons, nil, cons>(q_gen_5269, q_gen_5290) -> q_gen_5280
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5280
<nil, cons, cons>(q_gen_5269, q_gen_5290) -> q_gen_5280
<nil, cons, cons>(q_gen_5343, q_gen_5290) -> q_gen_5280
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5280
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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]) -> 33
() -> elem([h1, cons(h1, t1)]) -> 35
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 38
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 37
(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]) -> 35
(elem([e, nil])) -> BOT -> 34
}
Sat witness: Found: ((append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]), {
_oaa -> cons(b, cons(b, nil))  ;  i -> a  ;  l1 -> cons(b, cons(a, nil))  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 55, which took 0.176002 s (model generation: 0.170082,  model checking: 0.005920):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5343, q_gen_5344, q_gen_5362},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<a, b>() -> q_gen_5343
<b, a>() -> q_gen_5343
<cons, cons>(q_gen_5269, q_gen_5362) -> q_gen_5362
<cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5362
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5362) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, cons, cons>(q_gen_5283, q_gen_5344) -> q_gen_5344
<cons, nil, cons>(q_gen_5269, q_gen_5362) -> q_gen_5344
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5344
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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)]) -> 36
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 38
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 37
(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]) -> 36
(elem([e, nil])) -> BOT -> 35
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 56, which took 0.299084 s (model generation: 0.265947,  model checking: 0.033137):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5343, q_gen_5344, q_gen_5362},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<a, b>() -> q_gen_5343
<b, a>() -> q_gen_5343
<cons, cons>(q_gen_5269, q_gen_5362) -> q_gen_5362
<cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5362
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5362) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, cons, cons>(q_gen_5283, q_gen_5344) -> q_gen_5344
<cons, nil, cons>(q_gen_5269, q_gen_5362) -> q_gen_5344
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5344
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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)]) -> 37
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 38
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 40
(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]) -> 37
(elem([e, nil])) -> BOT -> 36
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, cons(a, nil)))  ;  t1 -> nil
})

-------------------------------------------
Step 57, which took 0.219652 s (model generation: 0.211993,  model checking: 0.007659):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5343, q_gen_5344, q_gen_5363},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<cons, cons>(q_gen_5269, q_gen_5363) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<a, b>() -> q_gen_5343
<b, a>() -> q_gen_5343
<cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5363
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5363) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, cons, cons>(q_gen_5283, q_gen_5344) -> q_gen_5344
<cons, nil, cons>(q_gen_5269, q_gen_5363) -> q_gen_5344
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5344
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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)]) -> 38
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 41
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 40
(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]) -> 38
(elem([e, nil])) -> BOT -> 37
}
Sat witness: Found: ((append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]), {
_oaa -> cons(a, cons(a, cons(a, nil)))  ;  i -> b  ;  l1 -> cons(a, cons(a, cons(b, nil)))  ;  l2 -> nil
})

-------------------------------------------
Step 58, which took 0.206179 s (model generation: 0.169407,  model checking: 0.036772):

Model:
|_
{
append -> 
{{{
Q={q_gen_5263, q_gen_5268, q_gen_5269, q_gen_5281, q_gen_5282, q_gen_5283, q_gen_5343, q_gen_5344, q_gen_5362},
Q_f={q_gen_5263},
Delta=
{
<cons>(q_gen_5282, q_gen_5281) -> q_gen_5281
<nil>() -> q_gen_5281
<a>() -> q_gen_5282
<b>() -> q_gen_5282
<cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5268
<nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5268
<nil, nil>() -> q_gen_5268
<a, a>() -> q_gen_5269
<b, b>() -> q_gen_5269
<a, b>() -> q_gen_5343
<b, a>() -> q_gen_5343
<cons, cons>(q_gen_5269, q_gen_5362) -> q_gen_5362
<cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5362
<cons, cons, cons>(q_gen_5283, q_gen_5263) -> q_gen_5263
<cons, nil, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5269, q_gen_5362) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5268) -> q_gen_5263
<nil, cons, cons>(q_gen_5343, q_gen_5362) -> q_gen_5263
<nil, nil, cons>(q_gen_5282, q_gen_5281) -> q_gen_5263
<nil, nil, nil>() -> q_gen_5263
<a, a, a>() -> q_gen_5283
<a, b, a>() -> q_gen_5283
<b, a, b>() -> q_gen_5283
<b, b, b>() -> q_gen_5283
<cons, cons, cons>(q_gen_5283, q_gen_5344) -> q_gen_5344
<cons, nil, cons>(q_gen_5269, q_gen_5362) -> q_gen_5344
<cons, nil, cons>(q_gen_5343, q_gen_5268) -> q_gen_5344
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  elem -> 
{{{
Q={q_gen_5260, q_gen_5261, q_gen_5262, q_gen_5265, q_gen_5266, q_gen_5270, q_gen_5277, q_gen_5287},
Q_f={q_gen_5260},
Delta=
{
<nil>() -> q_gen_5261
<b>() -> q_gen_5262
<cons>(q_gen_5262, q_gen_5261) -> q_gen_5265
<cons>(q_gen_5262, q_gen_5265) -> q_gen_5265
<a>() -> q_gen_5266
<cons>(q_gen_5262, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5262, q_gen_5287) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5265) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5277) -> q_gen_5277
<cons>(q_gen_5266, q_gen_5261) -> q_gen_5287
<cons>(q_gen_5266, q_gen_5287) -> q_gen_5287
<a, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5261) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5266, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5261) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5277) -> q_gen_5260
<b, cons>(q_gen_5262, q_gen_5287) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5265) -> q_gen_5260
<b, cons>(q_gen_5266, q_gen_5277) -> q_gen_5260
<a, cons>(q_gen_5262, q_gen_5261) -> q_gen_5270
<a, cons>(q_gen_5262, q_gen_5265) -> q_gen_5270
<a, nil>() -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5261) -> q_gen_5270
<b, cons>(q_gen_5266, q_gen_5287) -> q_gen_5270
<b, nil>() -> q_gen_5270
}

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)]) -> 39
(append([l1, l2, _oaa]) /\ elem([i, l1])) -> elem([i, _oaa]) -> 41
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 43
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 40
(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, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(a, cons(b, cons(b, cons(a, cons(b, nil)))))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, cons(b, cons(a, cons(b, nil)))))  ;  t1 -> nil
})

Total time: 25.181352
Reason for stopping: Proved