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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(prefix, P:
{() -> prefix([nil, y])
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)])
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys])
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT
(prefix([cons(z, zs), nil])) -> BOT}
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)])}
(append([_ue, _ve, _we]) /\ append([_ue, _ve, _xe])) -> eq_eltlist([_we, _xe])
)
}

properties:
{(append([l1, l2, _ye])) -> prefix([l1, _ye])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> prefix([nil, y]) -> 0
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 0
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 0
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 0
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 0
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 0
(prefix([cons(z, zs), nil])) -> BOT -> 0
}


Solving took 29.387989 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250, q_gen_1273, q_gen_1274, q_gen_1291},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<a, b>() -> q_gen_1273
<b, a>() -> q_gen_1273
<cons, cons>(q_gen_1235, q_gen_1291) -> q_gen_1291
<cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1291
<cons, cons>(q_gen_1273, q_gen_1291) -> q_gen_1291
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1291) -> q_gen_1230
<nil, cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1273, q_gen_1291) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
<cons, cons, cons>(q_gen_1250, q_gen_1274) -> q_gen_1274
<cons, nil, cons>(q_gen_1235, q_gen_1291) -> q_gen_1274
<cons, nil, cons>(q_gen_1273, q_gen_1234) -> q_gen_1274
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1275, q_gen_1276},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1232, q_gen_1275) -> q_gen_1275
<cons, cons>(q_gen_1276, q_gen_1229) -> q_gen_1275
<cons, cons>(q_gen_1276, q_gen_1275) -> q_gen_1275
<a, b>() -> q_gen_1276
<b, a>() -> q_gen_1276
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007718 s (model generation: 0.007391,  model checking: 0.000327):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> prefix([nil, y]) -> 3
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 1
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 1
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 1
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 1
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 1
(prefix([cons(z, zs), nil])) -> BOT -> 1
}
Sat witness: Found: (() -> prefix([nil, y]), {
y -> nil
})

-------------------------------------------
Step 1, which took 0.007429 s (model generation: 0.007290,  model checking: 0.000139):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229},
Q_f={q_gen_1229},
Delta=
{
<nil, nil>() -> q_gen_1229
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> prefix([nil, y]) -> 3
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 1
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 1
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 1
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 1
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 1
(prefix([cons(z, zs), nil])) -> BOT -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.008797 s (model generation: 0.007892,  model checking: 0.000905):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229},
Q_f={q_gen_1229},
Delta=
{
<nil, nil>() -> q_gen_1229
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> prefix([nil, y]) -> 3
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 1
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 1
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 2
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 2
(prefix([cons(z, zs), nil])) -> BOT -> 2
}
Sat witness: Found: ((prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]), {
y2 -> b  ;  ys -> nil  ;  zs -> nil
})

-------------------------------------------
Step 3, which took 0.008494 s (model generation: 0.008325,  model checking: 0.000169):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232},
Q_f={q_gen_1229},
Delta=
{
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<b, b>() -> q_gen_1232
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> prefix([nil, y]) -> 3
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 1
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 4
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 2
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 2
(prefix([cons(z, zs), nil])) -> BOT -> 2
}
Sat witness: Found: ((append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]), {
_te -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.008887 s (model generation: 0.007544,  model checking: 0.001343):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235},
Q_f={q_gen_1230},
Delta=
{
<nil, nil>() -> q_gen_1234
<b, b>() -> q_gen_1235
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232},
Q_f={q_gen_1229},
Delta=
{
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<b, b>() -> q_gen_1232
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> prefix([nil, y]) -> 6
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 2
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 4
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 3
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 3
(prefix([cons(z, zs), nil])) -> BOT -> 3
}
Sat witness: Found: (() -> prefix([nil, y]), {
y -> cons(b, nil)
})

-------------------------------------------
Step 5, which took 0.011311 s (model generation: 0.009332,  model checking: 0.001979):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235},
Q_f={q_gen_1230},
Delta=
{
<nil, nil>() -> q_gen_1234
<b, b>() -> q_gen_1235
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238},
Q_f={q_gen_1229},
Delta=
{
<nil>() -> q_gen_1237
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<b, b>() -> q_gen_1232
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> prefix([nil, y]) -> 6
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 3
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 4
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 4
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 4
(prefix([cons(z, zs), nil])) -> BOT -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 6, which took 0.008970 s (model generation: 0.008671,  model checking: 0.000299):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235},
Q_f={q_gen_1230},
Delta=
{
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238},
Q_f={q_gen_1229},
Delta=
{
<nil>() -> q_gen_1237
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<b, b>() -> q_gen_1232
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> prefix([nil, y]) -> 6
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 6
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 4
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 4
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 4
(prefix([cons(z, zs), nil])) -> BOT -> 4
}
Sat witness: Found: ((append([l1, l2, _ye])) -> prefix([l1, _ye]), {
_ye -> cons(a, nil)  ;  l1 -> cons(a, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 7, which took 0.011389 s (model generation: 0.008878,  model checking: 0.002511):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235},
Q_f={q_gen_1230},
Delta=
{
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238},
Q_f={q_gen_1229},
Delta=
{
<nil>() -> q_gen_1237
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> prefix([nil, y]) -> 6
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 6
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 7
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 5
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 5
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 5
(prefix([cons(z, zs), nil])) -> BOT -> 5
}
Sat witness: Found: ((append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]), {
_te -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 8, which took 0.013876 s (model generation: 0.011492,  model checking: 0.002384):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250},
Q_f={q_gen_1230},
Delta=
{
<nil>() -> q_gen_1248
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<b, b, b>() -> q_gen_1250
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238},
Q_f={q_gen_1229},
Delta=
{
<nil>() -> q_gen_1237
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> prefix([nil, y]) -> 6
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 9
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 7
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 6
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 6
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 6
(prefix([cons(z, zs), nil])) -> BOT -> 6
}
Sat witness: Found: ((append([l1, l2, _ye])) -> prefix([l1, _ye]), {
_ye -> cons(a, cons(a, nil))  ;  l1 -> nil  ;  l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 9, which took 0.013824 s (model generation: 0.011439,  model checking: 0.002385):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250},
Q_f={q_gen_1230},
Delta=
{
<nil>() -> q_gen_1248
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<b, b, b>() -> q_gen_1250
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> prefix([nil, y]) -> 7
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 9
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 10
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 7
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 7
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 7
(prefix([cons(z, zs), nil])) -> BOT -> 7
}
Sat witness: Found: ((append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]), {
_te -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.015358 s (model generation: 0.012286,  model checking: 0.003072):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250},
Q_f={q_gen_1230},
Delta=
{
<nil>() -> q_gen_1248
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<b, b, b>() -> q_gen_1250
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> prefix([nil, y]) -> 8
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 10
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 13
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 8
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 8
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 8
(prefix([cons(z, zs), nil])) -> BOT -> 8
}
Sat witness: Found: ((append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]), {
_te -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.015450 s (model generation: 0.012068,  model checking: 0.003382):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250},
Q_f={q_gen_1230},
Delta=
{
<nil>() -> q_gen_1248
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, b, a>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> prefix([nil, y]) -> 9
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 11
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 16
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 9
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 9
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 9
(prefix([cons(z, zs), nil])) -> BOT -> 9
}
Sat witness: Found: ((append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]), {
_te -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 0.020703 s (model generation: 0.017067,  model checking: 0.003636):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250},
Q_f={q_gen_1230},
Delta=
{
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> prefix([nil, y]) -> 10
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 12
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 19
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 10
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 10
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 10
(prefix([cons(z, zs), nil])) -> BOT -> 10
}
Sat witness: Found: ((append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]), {
_te -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.021824 s (model generation: 0.018010,  model checking: 0.003814):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250},
Q_f={q_gen_1230},
Delta=
{
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> prefix([nil, y]) -> 11
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 13
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 22
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 11
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 11
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 11
(prefix([cons(z, zs), nil])) -> BOT -> 11
}
Sat witness: Found: ((append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]), {
_te -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.025324 s (model generation: 0.019934,  model checking: 0.005390):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
() -> prefix([nil, y]) -> 12
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 14
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 25
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 12
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 12
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 12
(prefix([cons(z, zs), nil])) -> BOT -> 12
}
Sat witness: Found: ((append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]), {
_te -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.026127 s (model generation: 0.023968,  model checking: 0.002159):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> prefix([nil, y]) -> 13
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 17
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 25
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 13
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 13
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 13
(prefix([cons(z, zs), nil])) -> BOT -> 13
}
Sat witness: Found: ((append([l1, l2, _ye])) -> prefix([l1, _ye]), {
_ye -> cons(a, nil)  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 16, which took 0.031295 s (model generation: 0.031178,  model checking: 0.000117):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> prefix([nil, y]) -> 13
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 17
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 25
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 13
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 13
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 16
(prefix([cons(z, zs), nil])) -> BOT -> 14
}
Sat witness: Found: ((prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT, {
y2 -> a  ;  ys -> nil  ;  z -> b  ;  zs -> nil
})

-------------------------------------------
Step 17, which took 0.077980 s (model generation: 0.050194,  model checking: 0.027786):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1247, q_gen_1248, q_gen_1249, q_gen_1250, q_gen_1273},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<b, a>() -> q_gen_1273
<cons, cons, cons>(q_gen_1250, q_gen_1247) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<cons, nil, cons>(q_gen_1273, q_gen_1234) -> q_gen_1247
<nil, cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1247
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1247
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1275, q_gen_1276},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1276, q_gen_1229) -> q_gen_1275
<b, a>() -> q_gen_1276
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> prefix([nil, y]) -> 14
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 20
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 25
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 14
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 14
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 17
(prefix([cons(z, zs), nil])) -> BOT -> 15
}
Sat witness: Found: ((append([l1, l2, _ye])) -> prefix([l1, _ye]), {
_ye -> cons(b, cons(a, nil))  ;  l1 -> cons(b, cons(b, nil))  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 18, which took 0.035632 s (model generation: 0.035400,  model checking: 0.000232):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250, q_gen_1273, q_gen_1274},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<b, a>() -> q_gen_1273
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, cons, cons>(q_gen_1250, q_gen_1274) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
<cons, nil, cons>(q_gen_1273, q_gen_1234) -> q_gen_1274
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1275, q_gen_1276},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<cons, cons>(q_gen_1232, q_gen_1275) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1276, q_gen_1229) -> q_gen_1275
<b, a>() -> q_gen_1276
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> prefix([nil, y]) -> 14
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 20
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 25
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 14
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 17
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 17
(prefix([cons(z, zs), nil])) -> BOT -> 15
}
Sat witness: Found: ((prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]), {
y2 -> b  ;  ys -> cons(a, nil)  ;  zs -> cons(b, nil)
})

-------------------------------------------
Step 19, which took 0.214034 s (model generation: 0.036345,  model checking: 0.177689):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250, q_gen_1273, q_gen_1274},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<b, a>() -> q_gen_1273
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
<cons, cons, cons>(q_gen_1250, q_gen_1274) -> q_gen_1274
<cons, nil, cons>(q_gen_1273, q_gen_1234) -> q_gen_1274
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1275, q_gen_1276},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1232, q_gen_1275) -> q_gen_1275
<cons, cons>(q_gen_1276, q_gen_1229) -> q_gen_1275
<b, a>() -> q_gen_1276
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> prefix([nil, y]) -> 15
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 21
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 28
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 15
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 18
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 18
(prefix([cons(z, zs), nil])) -> BOT -> 16
}
Sat witness: Found: ((append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]), {
_te -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 20, which took 0.038968 s (model generation: 0.033406,  model checking: 0.005562):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250, q_gen_1273, q_gen_1274},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<a, b>() -> q_gen_1235
<b, b>() -> q_gen_1235
<b, a>() -> q_gen_1273
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
<cons, cons, cons>(q_gen_1250, q_gen_1274) -> q_gen_1274
<cons, nil, cons>(q_gen_1273, q_gen_1234) -> q_gen_1274
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1275, q_gen_1276},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1232, q_gen_1275) -> q_gen_1275
<cons, cons>(q_gen_1276, q_gen_1229) -> q_gen_1275
<b, a>() -> q_gen_1276
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> prefix([nil, y]) -> 16
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 24
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 28
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 16
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 19
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 19
(prefix([cons(z, zs), nil])) -> BOT -> 17
}
Sat witness: Found: ((append([l1, l2, _ye])) -> prefix([l1, _ye]), {
_ye -> cons(b, nil)  ;  l1 -> cons(a, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 21, which took 0.034464 s (model generation: 0.034221,  model checking: 0.000243):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1241, q_gen_1242, q_gen_1248, q_gen_1249, q_gen_1250},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<cons, cons>(q_gen_1241, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<b, b>() -> q_gen_1235
<a, a>() -> q_gen_1241
<a, b>() -> q_gen_1241
<b, a>() -> q_gen_1241
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1241, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<cons, cons, cons>(q_gen_1250, q_gen_1242) -> q_gen_1242
<cons, nil, cons>(q_gen_1241, q_gen_1234) -> q_gen_1242
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1243, q_gen_1244},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, b>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1232, q_gen_1243) -> q_gen_1243
<cons, cons>(q_gen_1244, q_gen_1229) -> q_gen_1243
<a, a>() -> q_gen_1244
<b, a>() -> q_gen_1244
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> prefix([nil, y]) -> 16
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 24
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 28
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 19
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 19
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 19
(prefix([cons(z, zs), nil])) -> BOT -> 17
}
Sat witness: Found: ((prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]), {
y2 -> a  ;  ys -> nil  ;  zs -> nil
})

-------------------------------------------
Step 22, which took 0.051408 s (model generation: 0.033666,  model checking: 0.017742):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250, q_gen_1273, q_gen_1274},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<a, b>() -> q_gen_1273
<b, a>() -> q_gen_1273
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
<cons, cons, cons>(q_gen_1250, q_gen_1274) -> q_gen_1274
<cons, nil, cons>(q_gen_1273, q_gen_1234) -> q_gen_1274
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1275, q_gen_1276},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1232, q_gen_1275) -> q_gen_1275
<cons, cons>(q_gen_1276, q_gen_1229) -> q_gen_1275
<a, b>() -> q_gen_1276
<b, a>() -> q_gen_1276
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17
() -> prefix([nil, y]) -> 17
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 25
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 31
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 20
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 20
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 20
(prefix([cons(z, zs), nil])) -> BOT -> 18
}
Sat witness: Found: ((append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]), {
_te -> cons(b, cons(b, cons(a, nil)))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, cons(a, nil)))  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 0.053085 s (model generation: 0.049903,  model checking: 0.003182):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250, q_gen_1273, q_gen_1274},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<a, b>() -> q_gen_1273
<b, a>() -> q_gen_1273
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
<cons, cons, cons>(q_gen_1250, q_gen_1274) -> q_gen_1274
<cons, nil, cons>(q_gen_1273, q_gen_1234) -> q_gen_1274
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1275, q_gen_1276},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1232, q_gen_1275) -> q_gen_1275
<cons, cons>(q_gen_1276, q_gen_1229) -> q_gen_1275
<a, b>() -> q_gen_1276
<b, a>() -> q_gen_1276
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18
() -> prefix([nil, y]) -> 18
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 28
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 31
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 21
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 21
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 21
(prefix([cons(z, zs), nil])) -> BOT -> 19
}
Sat witness: Found: ((append([l1, l2, _ye])) -> prefix([l1, _ye]), {
_ye -> cons(b, cons(a, nil))  ;  l1 -> cons(b, cons(b, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 24, which took 0.074981 s (model generation: 0.048224,  model checking: 0.026757):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250, q_gen_1273, q_gen_1274, q_gen_1291},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<a, b>() -> q_gen_1273
<b, a>() -> q_gen_1273
<cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1291
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1291) -> q_gen_1230
<nil, cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
<cons, cons, cons>(q_gen_1250, q_gen_1274) -> q_gen_1274
<cons, nil, cons>(q_gen_1235, q_gen_1291) -> q_gen_1274
<cons, nil, cons>(q_gen_1273, q_gen_1234) -> q_gen_1274
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1275, q_gen_1276},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1232, q_gen_1275) -> q_gen_1275
<cons, cons>(q_gen_1276, q_gen_1229) -> q_gen_1275
<a, b>() -> q_gen_1276
<b, a>() -> q_gen_1276
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
() -> prefix([nil, y]) -> 19
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 29
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 34
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 22
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 22
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 22
(prefix([cons(z, zs), nil])) -> BOT -> 20
}
Sat witness: Found: ((append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]), {
_te -> 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
})

-------------------------------------------
Step 25, which took 0.065623 s (model generation: 0.065181,  model checking: 0.000442):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1240, q_gen_1241, q_gen_1242, q_gen_1248, q_gen_1249, q_gen_1250},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<cons, cons>(q_gen_1235, q_gen_1240) -> q_gen_1234
<cons, cons>(q_gen_1241, q_gen_1240) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, b>() -> q_gen_1235
<b, b>() -> q_gen_1235
<cons, cons>(q_gen_1241, q_gen_1234) -> q_gen_1240
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1240
<a, a>() -> q_gen_1241
<b, a>() -> q_gen_1241
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1241, q_gen_1240) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1242
<cons, cons, cons>(q_gen_1250, q_gen_1242) -> q_gen_1242
<cons, nil, cons>(q_gen_1235, q_gen_1240) -> q_gen_1242
<cons, nil, cons>(q_gen_1241, q_gen_1234) -> q_gen_1242
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1242
<nil, cons, cons>(q_gen_1235, q_gen_1240) -> q_gen_1242
<nil, cons, cons>(q_gen_1241, q_gen_1234) -> q_gen_1242
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1242
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1275, q_gen_1276},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<a, b>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1232, q_gen_1275) -> q_gen_1275
<cons, cons>(q_gen_1276, q_gen_1229) -> q_gen_1275
<b, a>() -> q_gen_1276
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> prefix([nil, y]) -> 20
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 29
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 34
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 22
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 22
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 22
(prefix([cons(z, zs), nil])) -> BOT -> 20
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 26, which took 0.061810 s (model generation: 0.061644,  model checking: 0.000166):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250, q_gen_1273, q_gen_1274, q_gen_1291},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<cons, cons>(q_gen_1273, q_gen_1291) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<a, b>() -> q_gen_1273
<b, a>() -> q_gen_1273
<cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1291
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1291) -> q_gen_1230
<nil, cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
<cons, cons, cons>(q_gen_1250, q_gen_1274) -> q_gen_1274
<cons, nil, cons>(q_gen_1235, q_gen_1291) -> q_gen_1274
<cons, nil, cons>(q_gen_1273, q_gen_1234) -> q_gen_1274
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1275, q_gen_1276},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<a, b>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1232, q_gen_1275) -> q_gen_1275
<cons, cons>(q_gen_1276, q_gen_1229) -> q_gen_1275
<b, a>() -> q_gen_1276
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> prefix([nil, y]) -> 21
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 29
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 34
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 22
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 22
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 25
(prefix([cons(z, zs), nil])) -> BOT -> 21
}
Sat witness: Found: ((prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT, {
y2 -> b  ;  ys -> nil  ;  z -> a  ;  zs -> nil
})

-------------------------------------------
Step 27, which took 0.063453 s (model generation: 0.060262,  model checking: 0.003191):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250, q_gen_1273, q_gen_1274, q_gen_1291},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<cons, cons>(q_gen_1273, q_gen_1291) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<a, b>() -> q_gen_1273
<b, a>() -> q_gen_1273
<cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1291
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1291) -> q_gen_1230
<nil, cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
<cons, cons, cons>(q_gen_1250, q_gen_1274) -> q_gen_1274
<cons, nil, cons>(q_gen_1235, q_gen_1291) -> q_gen_1274
<cons, nil, cons>(q_gen_1273, q_gen_1234) -> q_gen_1274
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1275, q_gen_1276},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1232, q_gen_1275) -> q_gen_1275
<cons, cons>(q_gen_1276, q_gen_1229) -> q_gen_1275
<a, b>() -> q_gen_1276
<b, a>() -> q_gen_1276
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23
() -> prefix([nil, y]) -> 22
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 32
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 34
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 23
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 23
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 26
(prefix([cons(z, zs), nil])) -> BOT -> 22
}
Sat witness: Found: ((append([l1, l2, _ye])) -> prefix([l1, _ye]), {
_ye -> cons(b, cons(a, cons(a, nil)))  ;  l1 -> cons(b, cons(b, cons(b, nil)))  ;  l2 -> nil
})

-------------------------------------------
Step 28, which took 0.078458 s (model generation: 0.065770,  model checking: 0.012688):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1240, q_gen_1241, q_gen_1242, q_gen_1248, q_gen_1249, q_gen_1250},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1241, q_gen_1240) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<b, b>() -> q_gen_1235
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1240
<cons, cons>(q_gen_1235, q_gen_1240) -> q_gen_1240
<cons, cons>(q_gen_1241, q_gen_1234) -> q_gen_1240
<a, a>() -> q_gen_1241
<a, b>() -> q_gen_1241
<b, a>() -> q_gen_1241
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1241, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1241, q_gen_1240) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<cons, cons, cons>(q_gen_1250, q_gen_1242) -> q_gen_1242
<cons, nil, cons>(q_gen_1235, q_gen_1240) -> q_gen_1242
<cons, nil, cons>(q_gen_1241, q_gen_1234) -> q_gen_1242
<nil, cons, cons>(q_gen_1235, q_gen_1240) -> q_gen_1242
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1275, q_gen_1276},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<cons, cons>(q_gen_1276, q_gen_1275) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1232, q_gen_1275) -> q_gen_1275
<cons, cons>(q_gen_1276, q_gen_1229) -> q_gen_1275
<a, b>() -> q_gen_1276
<b, a>() -> q_gen_1276
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26
() -> prefix([nil, y]) -> 23
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 32
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 34
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 24
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 24
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 26
(prefix([cons(z, zs), nil])) -> BOT -> 23
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 29, which took 0.078080 s (model generation: 0.069230,  model checking: 0.008850):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250, q_gen_1273, q_gen_1274, q_gen_1291},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<cons, cons>(q_gen_1273, q_gen_1291) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<a, b>() -> q_gen_1273
<b, a>() -> q_gen_1273
<cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1291
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1291) -> q_gen_1230
<nil, cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
<cons, cons, cons>(q_gen_1250, q_gen_1274) -> q_gen_1274
<cons, nil, cons>(q_gen_1235, q_gen_1291) -> q_gen_1274
<cons, nil, cons>(q_gen_1273, q_gen_1234) -> q_gen_1274
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1275, q_gen_1276},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<cons, cons>(q_gen_1276, q_gen_1275) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1232, q_gen_1275) -> q_gen_1275
<cons, cons>(q_gen_1276, q_gen_1229) -> q_gen_1275
<a, b>() -> q_gen_1276
<b, a>() -> q_gen_1276
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26
() -> prefix([nil, y]) -> 24
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 32
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 34
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 25
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 25
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 29
(prefix([cons(z, zs), nil])) -> BOT -> 24
}
Sat witness: Found: ((prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT, {
y2 -> b  ;  ys -> cons(a, nil)  ;  z -> a  ;  zs -> cons(b, nil)
})

-------------------------------------------
Step 30, which took 0.075475 s (model generation: 0.072720,  model checking: 0.002755):

Model:
|_
{
append -> 
{{{
Q={q_gen_1230, q_gen_1234, q_gen_1235, q_gen_1248, q_gen_1249, q_gen_1250, q_gen_1273, q_gen_1274, q_gen_1291},
Q_f={q_gen_1230},
Delta=
{
<cons>(q_gen_1249, q_gen_1248) -> q_gen_1248
<nil>() -> q_gen_1248
<a>() -> q_gen_1249
<b>() -> q_gen_1249
<cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1234
<cons, cons>(q_gen_1235, q_gen_1291) -> q_gen_1234
<nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1234
<nil, nil>() -> q_gen_1234
<a, a>() -> q_gen_1235
<b, b>() -> q_gen_1235
<a, b>() -> q_gen_1273
<b, a>() -> q_gen_1273
<cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1291
<cons, cons>(q_gen_1273, q_gen_1291) -> q_gen_1291
<cons, cons, cons>(q_gen_1250, q_gen_1230) -> q_gen_1230
<cons, nil, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1234) -> q_gen_1230
<nil, cons, cons>(q_gen_1235, q_gen_1291) -> q_gen_1230
<nil, cons, cons>(q_gen_1273, q_gen_1234) -> q_gen_1230
<nil, nil, cons>(q_gen_1249, q_gen_1248) -> q_gen_1230
<nil, nil, nil>() -> q_gen_1230
<a, a, a>() -> q_gen_1250
<a, b, a>() -> q_gen_1250
<b, a, b>() -> q_gen_1250
<b, b, b>() -> q_gen_1250
<cons, cons, cons>(q_gen_1250, q_gen_1274) -> q_gen_1274
<cons, nil, cons>(q_gen_1235, q_gen_1291) -> q_gen_1274
<cons, nil, cons>(q_gen_1273, q_gen_1234) -> q_gen_1274
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_1229, q_gen_1232, q_gen_1237, q_gen_1238, q_gen_1275, q_gen_1276},
Q_f={q_gen_1229},
Delta=
{
<cons>(q_gen_1238, q_gen_1237) -> q_gen_1237
<nil>() -> q_gen_1237
<a>() -> q_gen_1238
<b>() -> q_gen_1238
<cons, cons>(q_gen_1232, q_gen_1229) -> q_gen_1229
<nil, cons>(q_gen_1238, q_gen_1237) -> q_gen_1229
<nil, nil>() -> q_gen_1229
<a, a>() -> q_gen_1232
<b, b>() -> q_gen_1232
<cons, cons>(q_gen_1232, q_gen_1275) -> q_gen_1275
<cons, cons>(q_gen_1276, q_gen_1229) -> q_gen_1275
<cons, cons>(q_gen_1276, q_gen_1275) -> q_gen_1275
<a, b>() -> q_gen_1276
<b, a>() -> q_gen_1276
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27
() -> prefix([nil, y]) -> 25
(append([l1, l2, _ye])) -> prefix([l1, _ye]) -> 35
(append([t1, l2, _te])) -> append([cons(h1, t1), l2, cons(h1, _te)]) -> 34
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 26
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 26
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 30
(prefix([cons(z, zs), nil])) -> BOT -> 25
}
Sat witness: Found: ((append([l1, l2, _ye])) -> prefix([l1, _ye]), {
_ye -> cons(b, cons(b, cons(a, nil)))  ;  l1 -> cons(b, cons(b, cons(b, nil)))  ;  l2 -> nil
})

Total time: 29.387989
Reason for stopping: Proved