Solving ../../benchmarks/true/prefix_append.smt2...

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


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, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)])}
(append([_or, _pr, _qr]) /\ append([_or, _pr, _rr])) -> eq_eltlist([_qr, _rr])
)
}

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


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0  ;  () -> prefix([nil, y]) -> 0  ;  (append([l1, l2, _sr])) -> prefix([l1, _sr]) -> 0  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 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 30.000066 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5141, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5149, q_gen_5150, q_gen_5151, q_gen_5152, q_gen_5159, q_gen_5160, q_gen_5161, q_gen_5162, q_gen_5163, q_gen_5164, q_gen_5165, q_gen_5166, q_gen_5169, q_gen_5170, q_gen_5171, q_gen_5172, q_gen_5173, q_gen_5176, q_gen_5177, q_gen_5178, q_gen_5182, q_gen_5183, q_gen_5184, q_gen_5185, q_gen_5186, q_gen_5189, q_gen_5190, q_gen_5191, q_gen_5192, q_gen_5193, q_gen_5194, q_gen_5195, q_gen_5196, q_gen_5197, q_gen_5198, q_gen_5199, q_gen_5200, q_gen_5201, q_gen_5202, q_gen_5203, q_gen_5204, q_gen_5205, q_gen_5206, q_gen_5207, q_gen_5208, q_gen_5209, q_gen_5210, q_gen_5211, q_gen_5212, q_gen_5213, q_gen_5214, q_gen_5215, q_gen_5216, q_gen_5217, q_gen_5218, q_gen_5219, q_gen_5220, q_gen_5221, q_gen_5222, q_gen_5223, q_gen_5224, q_gen_5225, q_gen_5226, q_gen_5227, q_gen_5228, q_gen_5229, q_gen_5230},
Q_f={},
Delta=
{
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<b>() -> q_gen_5172
<cons>(q_gen_5172, q_gen_5163) -> q_gen_5185
<cons>(q_gen_5164, q_gen_5163) -> q_gen_5226
<nil, nil>() -> q_gen_5142
<nil, b>() -> q_gen_5143
<b, nil>() -> q_gen_5144
<b, b>() -> q_gen_5145
<nil, a>() -> q_gen_5150
<a, nil>() -> q_gen_5151
<a, a>() -> q_gen_5152
<cons, cons>(q_gen_5152, q_gen_5151, q_gen_5150, q_gen_5142) -> q_gen_5161
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5162
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5165
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5170
<cons, b>(q_gen_5172, q_gen_5163) -> q_gen_5171
<b, cons>(q_gen_5172, q_gen_5163) -> q_gen_5173
<cons, a>(q_gen_5172, q_gen_5163) -> q_gen_5177
<a, cons>(q_gen_5172, q_gen_5163) -> q_gen_5178
<cons, cons>(q_gen_5145, q_gen_5173, q_gen_5171, q_gen_5170) -> q_gen_5183
<cons, b>(q_gen_5172, q_gen_5185) -> q_gen_5184
<b, cons>(q_gen_5172, q_gen_5185) -> q_gen_5186
<nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5201
<a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5222
<a, b>() -> q_gen_5223
<nil, nil, nil>() -> q_gen_5136
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5141
<nil, cons, cons>(q_gen_5152, q_gen_5151, q_gen_5150, q_gen_5142) -> q_gen_5149
<cons, nil, cons>(q_gen_5152, q_gen_5151, q_gen_5150, q_gen_5142) -> q_gen_5159
<cons, nil, cons>(q_gen_5145, q_gen_5165, q_gen_5162, q_gen_5161) -> q_gen_5160
<nil, cons, cons>(q_gen_5145, q_gen_5165, q_gen_5162, q_gen_5161) -> q_gen_5166
<nil, cons, cons>(q_gen_5145, q_gen_5173, q_gen_5171, q_gen_5170) -> q_gen_5169
<cons, nil, cons>(q_gen_5152, q_gen_5178, q_gen_5177, q_gen_5170) -> q_gen_5176
<nil, cons, cons>(q_gen_5145, q_gen_5186, q_gen_5184, q_gen_5183) -> q_gen_5182
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5189
<cons, cons, cons>(q_gen_5198, q_gen_5197, q_gen_5196, q_gen_5195, q_gen_5194, q_gen_5193, q_gen_5192, q_gen_5191) -> q_gen_5190
<nil, nil, cons>(q_gen_5172, q_gen_5163) -> q_gen_5191
<nil, nil, b>() -> q_gen_5192
<nil, b, cons>(q_gen_5172, q_gen_5163) -> q_gen_5193
<nil, b, b>() -> q_gen_5194
<b, nil, cons>(q_gen_5172, q_gen_5163) -> q_gen_5195
<b, nil, b>() -> q_gen_5196
<b, b, cons>(q_gen_5172, q_gen_5163) -> q_gen_5197
<b, b, b>() -> q_gen_5198
<nil, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5199
<cons, nil, cons>(q_gen_5145, q_gen_5165, q_gen_5143, q_gen_5201) -> q_gen_5200
<cons, cons, cons>(q_gen_5207, q_gen_5206, q_gen_5196, q_gen_5205, q_gen_5204, q_gen_5203, q_gen_5192, q_gen_5199) -> q_gen_5202
<nil, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5203
<nil, a, b>() -> q_gen_5204
<b, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5205
<b, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5206
<b, a, b>() -> q_gen_5207
<cons, cons, cons>(q_gen_5214, q_gen_5213, q_gen_5212, q_gen_5211, q_gen_5210, q_gen_5193, q_gen_5209, q_gen_5191) -> q_gen_5208
<nil, nil, a>() -> q_gen_5209
<nil, b, a>() -> q_gen_5210
<a, nil, cons>(q_gen_5172, q_gen_5163) -> q_gen_5211
<a, nil, a>() -> q_gen_5212
<a, b, cons>(q_gen_5172, q_gen_5163) -> q_gen_5213
<a, b, a>() -> q_gen_5214
<cons, cons, cons>(q_gen_5219, q_gen_5218, q_gen_5212, q_gen_5217, q_gen_5216, q_gen_5203, q_gen_5209, q_gen_5199) -> q_gen_5215
<nil, a, a>() -> q_gen_5216
<a, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5217
<a, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5218
<a, a, a>() -> q_gen_5219
<cons, cons, cons>(q_gen_5198, q_gen_5229, q_gen_5228, q_gen_5227, q_gen_5194, q_gen_5225, q_gen_5224, q_gen_5221) -> q_gen_5220
<nil, cons, cons>(q_gen_5223, q_gen_5222, q_gen_5143, q_gen_5201) -> q_gen_5221
<nil, cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5224
<nil, b, cons>(q_gen_5172, q_gen_5226) -> q_gen_5225
<b, cons, cons>(q_gen_5223, q_gen_5222, q_gen_5143, q_gen_5201) -> q_gen_5227
<b, cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5228
<b, b, cons>(q_gen_5172, q_gen_5226) -> q_gen_5229
<cons, nil, cons>(q_gen_5223, q_gen_5151, q_gen_5143, q_gen_5142) -> q_gen_5230
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5137, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5146, q_gen_5147, q_gen_5148, q_gen_5153, q_gen_5154, q_gen_5155, q_gen_5156, q_gen_5157, q_gen_5158, q_gen_5167, q_gen_5168, q_gen_5174, q_gen_5175, q_gen_5179, q_gen_5180, q_gen_5181, q_gen_5187, q_gen_5188, q_gen_5231, q_gen_5232},
Q_f={},
Delta=
{
<nil>() -> q_gen_5147
<b>() -> q_gen_5148
<a>() -> q_gen_5154
<cons>(q_gen_5154, q_gen_5147) -> q_gen_5168
<nil, nil>() -> q_gen_5135
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5137
<nil, b>() -> q_gen_5138
<b, nil>() -> q_gen_5139
<b, b>() -> q_gen_5140
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5146
<nil, cons>(q_gen_5154, q_gen_5147) -> q_gen_5153
<cons, cons>(q_gen_5158, q_gen_5157, q_gen_5156, q_gen_5135) -> q_gen_5155
<nil, a>() -> q_gen_5156
<a, nil>() -> q_gen_5157
<a, a>() -> q_gen_5158
<nil, cons>(q_gen_5148, q_gen_5168) -> q_gen_5167
<cons, cons>(q_gen_5140, q_gen_5175, q_gen_5138, q_gen_5153) -> q_gen_5174
<b, cons>(q_gen_5154, q_gen_5147) -> q_gen_5175
<cons, cons>(q_gen_5158, q_gen_5181, q_gen_5180, q_gen_5137) -> q_gen_5179
<cons, a>(q_gen_5148, q_gen_5147) -> q_gen_5180
<a, cons>(q_gen_5148, q_gen_5147) -> q_gen_5181
<cons, cons>(q_gen_5140, q_gen_5175, q_gen_5188, q_gen_5155) -> q_gen_5187
<cons, b>(q_gen_5154, q_gen_5147) -> q_gen_5188
<cons, cons>(q_gen_5232, q_gen_5157, q_gen_5138, q_gen_5135) -> q_gen_5231
<a, b>() -> q_gen_5232
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.012741 s (model generation: 0.009842,  model checking: 0.002899):

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

}

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

}

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

}
--
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, _sr])) -> prefix([l1, _sr]) -> 1  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 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: Yes: (() -> prefix([nil, y]), {
y -> nil
})

-------------------------------------------
Step 1, which took 0.011640 s (model generation: 0.010114,  model checking: 0.001526):

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

}

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

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

}
--
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, _sr])) -> prefix([l1, _sr]) -> 1  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 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: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.011065 s (model generation: 0.010553,  model checking: 0.000512):

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

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

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

}
--
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, _sr])) -> prefix([l1, _sr]) -> 1  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 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: Yes: ((prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]), {
y2 -> b  ;  ys -> nil  ;  zs -> nil
})

-------------------------------------------
Step 3, which took 0.012995 s (model generation: 0.010900,  model checking: 0.002095):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140},
Q_f={q_gen_5135},
Delta=
{
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<nil, b>() -> q_gen_5138
<b, nil>() -> q_gen_5139
<b, b>() -> q_gen_5140
}

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

}
--
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, _sr])) -> prefix([l1, _sr]) -> 1  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 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: Yes: ((append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]), {
_nr -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.018142 s (model generation: 0.011236,  model checking: 0.006906):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145},
Q_f={q_gen_5136},
Delta=
{
<nil, nil>() -> q_gen_5142
<nil, b>() -> q_gen_5143
<b, nil>() -> q_gen_5144
<b, b>() -> q_gen_5145
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140},
Q_f={q_gen_5135},
Delta=
{
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<nil, b>() -> q_gen_5138
<b, nil>() -> q_gen_5139
<b, b>() -> q_gen_5140
}

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

}
--
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, _sr])) -> prefix([l1, _sr]) -> 2  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 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: Yes: (() -> prefix([nil, y]), {
y -> cons(b, nil)
})

-------------------------------------------
Step 5, which took 0.033000 s (model generation: 0.011390,  model checking: 0.021610):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145},
Q_f={q_gen_5136},
Delta=
{
<nil, nil>() -> q_gen_5142
<nil, b>() -> q_gen_5143
<b, nil>() -> q_gen_5144
<b, b>() -> q_gen_5145
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<nil>() -> q_gen_5147
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<nil, b>() -> q_gen_5138
<b, nil>() -> q_gen_5139
<b, b>() -> q_gen_5140
}

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

}
--
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, _sr])) -> prefix([l1, _sr]) -> 3  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 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: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 6, which took 0.004392 s (model generation: 0.003973,  model checking: 0.000419):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145},
Q_f={q_gen_5136},
Delta=
{
<nil, nil>() -> q_gen_5142
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, nil>() -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<nil>() -> q_gen_5147
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<nil, b>() -> q_gen_5138
<b, nil>() -> q_gen_5139
<b, b>() -> q_gen_5140
}

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

}
--
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, _sr])) -> prefix([l1, _sr]) -> 6  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 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: Yes: ((append([l1, l2, _sr])) -> prefix([l1, _sr]), {
_sr -> cons(a, nil)  ;  l1 -> nil  ;  l2 -> cons(a, nil)
})

-------------------------------------------
Step 7, which took 0.007335 s (model generation: 0.004068,  model checking: 0.003267):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145},
Q_f={q_gen_5136},
Delta=
{
<nil, nil>() -> q_gen_5142
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, nil>() -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<nil, b>() -> q_gen_5138
<b, nil>() -> q_gen_5139
<b, b>() -> q_gen_5140
}

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

}
--
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, _sr])) -> prefix([l1, _sr]) -> 6  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 4  ;  (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 7  ;  (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: Yes: ((prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]), {
y2 -> a  ;  ys -> nil  ;  zs -> nil
})

-------------------------------------------
Step 8, which took 0.009121 s (model generation: 0.004890,  model checking: 0.004231):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145},
Q_f={q_gen_5136},
Delta=
{
<nil, nil>() -> q_gen_5142
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, nil>() -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, nil>() -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

}
--
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, _sr])) -> prefix([l1, _sr]) -> 6  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 7  ;  (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 7  ;  (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: Yes: ((append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]), {
_nr -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 9, which took 0.012570 s (model generation: 0.005770,  model checking: 0.006800):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164},
Q_f={q_gen_5136},
Delta=
{
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, nil>() -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

}
--
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, _sr])) -> prefix([l1, _sr]) -> 9  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 7  ;  (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 7  ;  (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: Yes: ((append([l1, l2, _sr])) -> prefix([l1, _sr]), {
_sr -> cons(b, cons(a, nil))  ;  l1 -> nil  ;  l2 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 10, which took 0.016582 s (model generation: 0.005270,  model checking: 0.011312):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164},
Q_f={q_gen_5136},
Delta=
{
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<cons>(q_gen_5148, q_gen_5147) -> q_gen_5147
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, nil>() -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> prefix([nil, y]) -> 7  ;  (append([l1, l2, _sr])) -> prefix([l1, _sr]) -> 9  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 7  ;  (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: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 11, which took 0.007981 s (model generation: 0.005684,  model checking: 0.002297):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164},
Q_f={q_gen_5136},
Delta=
{
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<b>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<cons>(q_gen_5148, q_gen_5147) -> q_gen_5147
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, nil>() -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> prefix([nil, y]) -> 7  ;  (append([l1, l2, _sr])) -> prefix([l1, _sr]) -> 9  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 7  ;  (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 10  ;  (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: Yes: ((prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]), {
y2 -> b  ;  ys -> cons(a, nil)  ;  zs -> nil
})

-------------------------------------------
Step 12, which took 0.011696 s (model generation: 0.005925,  model checking: 0.005771):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164},
Q_f={q_gen_5136},
Delta=
{
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<b>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<cons>(q_gen_5148, q_gen_5147) -> q_gen_5147
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, nil>() -> q_gen_5139
<b, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> prefix([nil, y]) -> 7  ;  (append([l1, l2, _sr])) -> prefix([l1, _sr]) -> 9  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 10  ;  (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 10  ;  (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: Yes: ((append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]), {
_nr -> cons(b, nil)  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 13, which took 0.010518 s (model generation: 0.006375,  model checking: 0.004143):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164},
Q_f={q_gen_5136},
Delta=
{
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<b>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, a>(q_gen_5164, q_gen_5163) -> q_gen_5143
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<cons>(q_gen_5148, q_gen_5147) -> q_gen_5147
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, nil>() -> q_gen_5139
<b, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> prefix([nil, y]) -> 8  ;  (append([l1, l2, _sr])) -> prefix([l1, _sr]) -> 12  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 10  ;  (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 10  ;  (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: Yes: ((append([l1, l2, _sr])) -> prefix([l1, _sr]), {
_sr -> cons(a, cons(b, nil))  ;  l1 -> cons(a, cons(b, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 14, which took 0.022227 s (model generation: 0.006740,  model checking: 0.015487):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164},
Q_f={q_gen_5136},
Delta=
{
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<b>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, a>(q_gen_5164, q_gen_5163) -> q_gen_5143
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<cons>(q_gen_5148, q_gen_5147) -> q_gen_5147
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<cons, a>(q_gen_5148, q_gen_5147) -> q_gen_5138
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<a, nil>() -> q_gen_5139
<b, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> prefix([nil, y]) -> 9  ;  (append([l1, l2, _sr])) -> prefix([l1, _sr]) -> 12  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 10  ;  (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: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 15, which took 0.014610 s (model generation: 0.007250,  model checking: 0.007360):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164},
Q_f={q_gen_5136},
Delta=
{
<cons>(q_gen_5164, q_gen_5163) -> q_gen_5163
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<b>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, a>(q_gen_5164, q_gen_5163) -> q_gen_5143
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<cons>(q_gen_5148, q_gen_5147) -> q_gen_5147
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<cons, a>(q_gen_5148, q_gen_5147) -> q_gen_5138
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<a, nil>() -> q_gen_5139
<b, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> prefix([nil, y]) -> 10  ;  (append([l1, l2, _sr])) -> prefix([l1, _sr]) -> 12  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 10  ;  (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 13  ;  (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: Yes: ((prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]), {
y2 -> b  ;  ys -> cons(a, nil)  ;  zs -> cons(a, nil)
})

-------------------------------------------
Step 16, which took 0.011096 s (model generation: 0.007612,  model checking: 0.003484):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164},
Q_f={q_gen_5136},
Delta=
{
<cons>(q_gen_5164, q_gen_5163) -> q_gen_5163
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<b>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, a>(q_gen_5164, q_gen_5163) -> q_gen_5143
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<cons>(q_gen_5148, q_gen_5147) -> q_gen_5147
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<cons, a>(q_gen_5148, q_gen_5147) -> q_gen_5138
<cons, b>(q_gen_5148, q_gen_5147) -> q_gen_5138
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<a, nil>() -> q_gen_5139
<b, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> prefix([nil, y]) -> 10  ;  (append([l1, l2, _sr])) -> prefix([l1, _sr]) -> 12  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 13  ;  (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 13  ;  (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: Yes: ((append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]), {
_nr -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 17, which took 0.053327 s (model generation: 0.008992,  model checking: 0.044335):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164, q_gen_5192, q_gen_5193, q_gen_5194, q_gen_5195, q_gen_5196, q_gen_5197, q_gen_5198},
Q_f={q_gen_5136},
Delta=
{
<cons>(q_gen_5164, q_gen_5163) -> q_gen_5163
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<b>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, a>(q_gen_5164, q_gen_5163) -> q_gen_5143
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, cons, cons>(q_gen_5198, q_gen_5197, q_gen_5196, q_gen_5195, q_gen_5194, q_gen_5193, q_gen_5192, q_gen_5136) -> q_gen_5136
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
<nil, nil, b>() -> q_gen_5192
<nil, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5193
<nil, b, b>() -> q_gen_5194
<b, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5195
<b, nil, b>() -> q_gen_5196
<b, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<b, b, b>() -> q_gen_5198
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<cons>(q_gen_5148, q_gen_5147) -> q_gen_5147
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<cons, a>(q_gen_5148, q_gen_5147) -> q_gen_5138
<cons, b>(q_gen_5148, q_gen_5147) -> q_gen_5138
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<a, nil>() -> q_gen_5139
<b, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> prefix([nil, y]) -> 11  ;  (append([l1, l2, _sr])) -> prefix([l1, _sr]) -> 13  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 16  ;  (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 14  ;  (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: Yes: ((append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]), {
_nr -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 18, which took 0.090991 s (model generation: 0.009997,  model checking: 0.080994):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164, q_gen_5192, q_gen_5193, q_gen_5194, q_gen_5195, q_gen_5196, q_gen_5197, q_gen_5198},
Q_f={q_gen_5136},
Delta=
{
<cons>(q_gen_5164, q_gen_5163) -> q_gen_5163
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<b>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, a>(q_gen_5164, q_gen_5163) -> q_gen_5143
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, cons, cons>(q_gen_5198, q_gen_5197, q_gen_5196, q_gen_5195, q_gen_5194, q_gen_5193, q_gen_5192, q_gen_5136) -> q_gen_5136
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
<nil, nil, b>() -> q_gen_5192
<nil, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5193
<nil, b, b>() -> q_gen_5194
<b, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5195
<b, nil, b>() -> q_gen_5196
<b, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<b, b, b>() -> q_gen_5198
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<cons>(q_gen_5148, q_gen_5147) -> q_gen_5147
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<cons, a>(q_gen_5148, q_gen_5147) -> q_gen_5138
<cons, b>(q_gen_5148, q_gen_5147) -> q_gen_5138
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<a, nil>() -> q_gen_5139
<b, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14  ;  () -> prefix([nil, y]) -> 12  ;  (append([l1, l2, _sr])) -> prefix([l1, _sr]) -> 14  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 19  ;  (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 15  ;  (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: Yes: ((append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]), {
_nr -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.222974 s (model generation: 0.011110,  model checking: 0.211864):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164, q_gen_5192, q_gen_5193, q_gen_5194, q_gen_5195, q_gen_5196, q_gen_5197, q_gen_5198},
Q_f={q_gen_5136},
Delta=
{
<cons>(q_gen_5164, q_gen_5163) -> q_gen_5163
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<b>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, a>(q_gen_5164, q_gen_5163) -> q_gen_5143
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, cons, cons>(q_gen_5198, q_gen_5197, q_gen_5196, q_gen_5195, q_gen_5194, q_gen_5193, q_gen_5192, q_gen_5136) -> q_gen_5136
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
<nil, nil, b>() -> q_gen_5192
<nil, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5193
<nil, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5193
<nil, a, b>() -> q_gen_5194
<nil, b, b>() -> q_gen_5194
<b, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5195
<b, nil, b>() -> q_gen_5196
<b, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<b, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<b, a, b>() -> q_gen_5198
<b, b, b>() -> q_gen_5198
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<cons>(q_gen_5148, q_gen_5147) -> q_gen_5147
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<cons, a>(q_gen_5148, q_gen_5147) -> q_gen_5138
<cons, b>(q_gen_5148, q_gen_5147) -> q_gen_5138
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<a, nil>() -> q_gen_5139
<b, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

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

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

-------------------------------------------
Step 20, which took 0.085097 s (model generation: 0.012238,  model checking: 0.072859):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164, q_gen_5192, q_gen_5193, q_gen_5194, q_gen_5195, q_gen_5196, q_gen_5197, q_gen_5198},
Q_f={q_gen_5136},
Delta=
{
<cons>(q_gen_5164, q_gen_5163) -> q_gen_5163
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<b>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, a>(q_gen_5164, q_gen_5163) -> q_gen_5143
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, cons, cons>(q_gen_5198, q_gen_5197, q_gen_5196, q_gen_5195, q_gen_5194, q_gen_5193, q_gen_5192, q_gen_5136) -> q_gen_5136
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
<nil, nil, a>() -> q_gen_5192
<nil, nil, b>() -> q_gen_5192
<nil, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5193
<nil, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5193
<nil, a, b>() -> q_gen_5194
<nil, b, a>() -> q_gen_5194
<nil, b, b>() -> q_gen_5194
<a, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5195
<b, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5195
<a, nil, a>() -> q_gen_5196
<b, nil, b>() -> q_gen_5196
<a, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<b, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<b, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<a, b, a>() -> q_gen_5198
<b, a, b>() -> q_gen_5198
<b, b, b>() -> q_gen_5198
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<cons>(q_gen_5148, q_gen_5147) -> q_gen_5147
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<cons, a>(q_gen_5148, q_gen_5147) -> q_gen_5138
<cons, b>(q_gen_5148, q_gen_5147) -> q_gen_5138
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<a, nil>() -> q_gen_5139
<b, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

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

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

-------------------------------------------
Step 21, which took 1.069162 s (model generation: 0.012449,  model checking: 1.056713):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164, q_gen_5192, q_gen_5193, q_gen_5194, q_gen_5195, q_gen_5196, q_gen_5197, q_gen_5198},
Q_f={q_gen_5136},
Delta=
{
<cons>(q_gen_5164, q_gen_5163) -> q_gen_5163
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<b>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, a>(q_gen_5164, q_gen_5163) -> q_gen_5143
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, cons, cons>(q_gen_5198, q_gen_5197, q_gen_5196, q_gen_5195, q_gen_5194, q_gen_5193, q_gen_5192, q_gen_5136) -> q_gen_5136
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
<nil, nil, a>() -> q_gen_5192
<nil, nil, b>() -> q_gen_5192
<nil, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5193
<nil, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5193
<nil, a, a>() -> q_gen_5194
<nil, a, b>() -> q_gen_5194
<nil, b, a>() -> q_gen_5194
<nil, b, b>() -> q_gen_5194
<a, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5195
<b, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5195
<a, nil, a>() -> q_gen_5196
<b, nil, b>() -> q_gen_5196
<a, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<a, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<b, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<b, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<a, a, a>() -> q_gen_5198
<a, b, a>() -> q_gen_5198
<b, a, b>() -> q_gen_5198
<b, b, b>() -> q_gen_5198
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<cons>(q_gen_5148, q_gen_5147) -> q_gen_5147
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<cons, a>(q_gen_5148, q_gen_5147) -> q_gen_5138
<cons, b>(q_gen_5148, q_gen_5147) -> q_gen_5138
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<a, nil>() -> q_gen_5139
<b, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

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

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

-------------------------------------------
Step 22, which took 0.026351 s (model generation: 0.014718,  model checking: 0.011633):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164, q_gen_5192, q_gen_5193, q_gen_5194, q_gen_5195, q_gen_5196, q_gen_5197, q_gen_5198},
Q_f={q_gen_5136},
Delta=
{
<cons>(q_gen_5164, q_gen_5163) -> q_gen_5163
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<b>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, a>(q_gen_5164, q_gen_5163) -> q_gen_5143
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<a, b>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, cons, cons>(q_gen_5198, q_gen_5197, q_gen_5196, q_gen_5195, q_gen_5194, q_gen_5193, q_gen_5192, q_gen_5136) -> q_gen_5136
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
<nil, cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5192
<nil, nil, a>() -> q_gen_5192
<nil, nil, b>() -> q_gen_5192
<nil, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5193
<nil, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5193
<nil, a, a>() -> q_gen_5194
<nil, a, b>() -> q_gen_5194
<nil, b, a>() -> q_gen_5194
<nil, b, b>() -> q_gen_5194
<a, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5195
<b, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5195
<b, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5195
<a, nil, a>() -> q_gen_5196
<b, cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5196
<b, nil, b>() -> q_gen_5196
<a, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<a, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<b, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<b, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<a, a, a>() -> q_gen_5198
<a, b, a>() -> q_gen_5198
<b, a, b>() -> q_gen_5198
<b, b, b>() -> q_gen_5198
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<cons>(q_gen_5148, q_gen_5147) -> q_gen_5147
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<cons, a>(q_gen_5148, q_gen_5147) -> q_gen_5138
<cons, b>(q_gen_5148, q_gen_5147) -> q_gen_5138
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<a, nil>() -> q_gen_5139
<b, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17  ;  () -> prefix([nil, y]) -> 16  ;  (append([l1, l2, _sr])) -> prefix([l1, _sr]) -> 20  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 28  ;  (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 18  ;  (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 -> 17
}
Sat witness: Yes: ((append([l1, l2, _sr])) -> prefix([l1, _sr]), {
_sr -> cons(b, nil)  ;  l1 -> cons(a, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 23, which took 0.015608 s (model generation: 0.015405,  model checking: 0.000203):

Model:
|_
{
append -> 
{{{
Q={q_gen_5136, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5163, q_gen_5164, q_gen_5192, q_gen_5193, q_gen_5194, q_gen_5195, q_gen_5196, q_gen_5197, q_gen_5198},
Q_f={q_gen_5136},
Delta=
{
<cons>(q_gen_5164, q_gen_5163) -> q_gen_5163
<nil>() -> q_gen_5163
<a>() -> q_gen_5164
<b>() -> q_gen_5164
<cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5142
<nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5142
<nil, nil>() -> q_gen_5142
<cons, a>(q_gen_5164, q_gen_5163) -> q_gen_5143
<cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5143
<nil, a>() -> q_gen_5143
<nil, b>() -> q_gen_5143
<a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<a, nil>() -> q_gen_5144
<b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5144
<b, nil>() -> q_gen_5144
<a, a>() -> q_gen_5145
<a, b>() -> q_gen_5145
<b, b>() -> q_gen_5145
<cons, cons, cons>(q_gen_5198, q_gen_5197, q_gen_5196, q_gen_5195, q_gen_5194, q_gen_5193, q_gen_5192, q_gen_5136) -> q_gen_5136
<cons, nil, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5136
<nil, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5136
<nil, nil, nil>() -> q_gen_5136
<nil, cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5192
<nil, nil, a>() -> q_gen_5192
<nil, nil, b>() -> q_gen_5192
<nil, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5193
<nil, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5193
<nil, a, a>() -> q_gen_5194
<nil, a, b>() -> q_gen_5194
<nil, b, a>() -> q_gen_5194
<nil, b, b>() -> q_gen_5194
<a, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5195
<b, cons, cons>(q_gen_5145, q_gen_5144, q_gen_5143, q_gen_5142) -> q_gen_5195
<b, nil, cons>(q_gen_5164, q_gen_5163) -> q_gen_5195
<a, nil, a>() -> q_gen_5196
<b, cons, b>(q_gen_5164, q_gen_5163) -> q_gen_5196
<b, nil, b>() -> q_gen_5196
<a, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<a, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<b, a, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<b, b, cons>(q_gen_5164, q_gen_5163) -> q_gen_5197
<a, a, a>() -> q_gen_5198
<a, b, a>() -> q_gen_5198
<b, a, b>() -> q_gen_5198
<b, b, b>() -> q_gen_5198
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  prefix -> 
{{{
Q={q_gen_5135, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5147, q_gen_5148},
Q_f={q_gen_5135},
Delta=
{
<cons>(q_gen_5148, q_gen_5147) -> q_gen_5147
<nil>() -> q_gen_5147
<a>() -> q_gen_5148
<b>() -> q_gen_5148
<cons, cons>(q_gen_5140, q_gen_5139, q_gen_5138, q_gen_5135) -> q_gen_5135
<nil, cons>(q_gen_5148, q_gen_5147) -> q_gen_5135
<nil, nil>() -> q_gen_5135
<cons, a>(q_gen_5148, q_gen_5147) -> q_gen_5138
<cons, b>(q_gen_5148, q_gen_5147) -> q_gen_5138
<nil, a>() -> q_gen_5138
<nil, b>() -> q_gen_5138
<a, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<a, nil>() -> q_gen_5139
<b, cons>(q_gen_5148, q_gen_5147) -> q_gen_5139
<b, nil>() -> q_gen_5139
<a, a>() -> q_gen_5140
<a, b>() -> q_gen_5140
<b, b>() -> q_gen_5140
}

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

}
--
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, _sr])) -> prefix([l1, _sr]) -> 20  ;  (append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 28  ;  (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 18  ;  (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 17  ;  (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 20  ;  (prefix([cons(z, zs), nil])) -> BOT -> 18
}
Sat witness: Yes: ((prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT, {
y2 -> b  ;  ys -> nil  ;  z -> a  ;  zs -> nil
})

Total time: 30.000066
Reason for stopping: DontKnow. Stopped because: timeout