Solving ../../benchmarks/true/append_length_commutative.smt2...

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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)])}
(append([_uy, _vy, _wy]) /\ append([_uy, _vy, _xy])) -> eq_eltlist([_wy, _xy])
)
(length, F:
{() -> length([nil, z])
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)])}
(length([_zy, _az]) /\ length([_zy, _bz])) -> eq_nat([_az, _bz])
)
}

properties:
{(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0  ;  () -> length([nil, z]) -> 0  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 0  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 0  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 0
}


Solving took 30.024995 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_144, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_149, q_gen_150, q_gen_151, q_gen_152, q_gen_155, q_gen_156, q_gen_157, q_gen_158, q_gen_159, q_gen_160, q_gen_161, q_gen_162, q_gen_163, q_gen_164, q_gen_165, q_gen_166, q_gen_170, q_gen_171, q_gen_172, q_gen_173, q_gen_174, q_gen_175, q_gen_176, q_gen_177, q_gen_180, q_gen_181, q_gen_182, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189, q_gen_194, q_gen_195, q_gen_196, q_gen_197, q_gen_198, q_gen_199, q_gen_200, q_gen_201, q_gen_202, q_gen_203, q_gen_204, q_gen_205, q_gen_206, q_gen_207, q_gen_208, q_gen_209, q_gen_210, q_gen_211, q_gen_212, q_gen_213, q_gen_214, q_gen_215, q_gen_216, q_gen_217, q_gen_218, q_gen_219, q_gen_220, q_gen_221, q_gen_222, q_gen_223, q_gen_224, q_gen_225, q_gen_226, q_gen_227, q_gen_228, q_gen_229, q_gen_232, q_gen_233, q_gen_234, q_gen_235, q_gen_236, q_gen_237, q_gen_238, q_gen_239, q_gen_240, q_gen_241, q_gen_242, q_gen_243, q_gen_244, q_gen_245, q_gen_246},
Q_f={},
Delta=
{
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_165
<cons>(q_gen_165, q_gen_159) -> q_gen_176
<cons>(q_gen_165, q_gen_176) -> q_gen_214
<nil, nil>() -> q_gen_145
<nil, b>() -> q_gen_146
<b, nil>() -> q_gen_147
<b, b>() -> q_gen_148
<nil, a>() -> q_gen_150
<a, nil>() -> q_gen_151
<a, a>() -> q_gen_152
<cons, cons>(q_gen_152, q_gen_151, q_gen_150, q_gen_145) -> q_gen_157
<cons, b>(q_gen_160, q_gen_159) -> q_gen_158
<b, cons>(q_gen_160, q_gen_159) -> q_gen_161
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_163
<cons, b>(q_gen_165, q_gen_159) -> q_gen_164
<b, cons>(q_gen_165, q_gen_159) -> q_gen_166
<cons, a>(q_gen_165, q_gen_159) -> q_gen_171
<a, cons>(q_gen_165, q_gen_159) -> q_gen_172
<cons, cons>(q_gen_148, q_gen_166, q_gen_164, q_gen_163) -> q_gen_174
<cons, b>(q_gen_165, q_gen_176) -> q_gen_175
<b, cons>(q_gen_165, q_gen_176) -> q_gen_177
<cons, a>(q_gen_165, q_gen_176) -> q_gen_207
<a, cons>(q_gen_165, q_gen_176) -> q_gen_208
<nil, cons>(q_gen_165, q_gen_176) -> q_gen_210
<cons, cons>(q_gen_152, q_gen_208, q_gen_207, q_gen_174) -> q_gen_212
<cons, b>(q_gen_160, q_gen_214) -> q_gen_213
<b, cons>(q_gen_160, q_gen_214) -> q_gen_215
<nil, cons>(q_gen_165, q_gen_159) -> q_gen_224
<cons, cons>(q_gen_148, q_gen_166, q_gen_146, q_gen_224) -> q_gen_234
<b, a>() -> q_gen_235
<nil, nil, nil>() -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_144
<nil, cons, cons>(q_gen_152, q_gen_151, q_gen_150, q_gen_145) -> q_gen_149
<cons, nil, cons>(q_gen_152, q_gen_151, q_gen_150, q_gen_145) -> q_gen_155
<cons, nil, cons>(q_gen_148, q_gen_161, q_gen_158, q_gen_157) -> q_gen_156
<nil, cons, cons>(q_gen_148, q_gen_166, q_gen_164, q_gen_163) -> q_gen_162
<cons, nil, cons>(q_gen_152, q_gen_172, q_gen_171, q_gen_163) -> q_gen_170
<nil, cons, cons>(q_gen_148, q_gen_177, q_gen_175, q_gen_174) -> q_gen_173
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_180
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_181
<nil, nil, cons>(q_gen_165, q_gen_159) -> q_gen_182
<nil, nil, b>() -> q_gen_183
<nil, b, cons>(q_gen_165, q_gen_159) -> q_gen_184
<nil, b, b>() -> q_gen_185
<b, nil, cons>(q_gen_165, q_gen_159) -> q_gen_186
<b, nil, b>() -> q_gen_187
<b, b, cons>(q_gen_165, q_gen_159) -> q_gen_188
<b, b, b>() -> q_gen_189
<cons, cons, cons>(q_gen_200, q_gen_199, q_gen_187, q_gen_198, q_gen_197, q_gen_196, q_gen_183, q_gen_195) -> q_gen_194
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_195
<nil, a, cons>(q_gen_160, q_gen_159) -> q_gen_196
<nil, a, b>() -> q_gen_197
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_198
<b, a, cons>(q_gen_160, q_gen_159) -> q_gen_199
<b, a, b>() -> q_gen_200
<cons, cons, cons>(q_gen_189, q_gen_205, q_gen_187, q_gen_204, q_gen_185, q_gen_203, q_gen_183, q_gen_202) -> q_gen_201
<nil, nil, cons>(q_gen_165, q_gen_176) -> q_gen_202
<nil, b, cons>(q_gen_165, q_gen_176) -> q_gen_203
<b, nil, cons>(q_gen_165, q_gen_176) -> q_gen_204
<b, b, cons>(q_gen_165, q_gen_176) -> q_gen_205
<nil, cons, cons>(q_gen_152, q_gen_208, q_gen_207, q_gen_174) -> q_gen_206
<cons, nil, cons>(q_gen_152, q_gen_208, q_gen_150, q_gen_210) -> q_gen_209
<nil, cons, cons>(q_gen_148, q_gen_215, q_gen_213, q_gen_212) -> q_gen_211
<cons, cons, cons>(q_gen_222, q_gen_221, q_gen_220, q_gen_219, q_gen_218, q_gen_184, q_gen_217, q_gen_182) -> q_gen_216
<nil, nil, a>() -> q_gen_217
<nil, b, a>() -> q_gen_218
<a, nil, cons>(q_gen_165, q_gen_159) -> q_gen_219
<a, nil, a>() -> q_gen_220
<a, b, cons>(q_gen_165, q_gen_159) -> q_gen_221
<a, b, a>() -> q_gen_222
<nil, cons, cons>(q_gen_148, q_gen_166, q_gen_146, q_gen_224) -> q_gen_223
<cons, cons, cons>(q_gen_229, q_gen_228, q_gen_220, q_gen_227, q_gen_226, q_gen_196, q_gen_217, q_gen_195) -> q_gen_225
<nil, a, a>() -> q_gen_226
<a, nil, cons>(q_gen_160, q_gen_159) -> q_gen_227
<a, a, cons>(q_gen_160, q_gen_159) -> q_gen_228
<a, a, a>() -> q_gen_229
<cons, cons, cons>(q_gen_200, q_gen_240, q_gen_239, q_gen_238, q_gen_197, q_gen_237, q_gen_236, q_gen_233) -> q_gen_232
<nil, cons, cons>(q_gen_235, q_gen_177, q_gen_171, q_gen_234) -> q_gen_233
<nil, cons, b>(q_gen_165, q_gen_176) -> q_gen_236
<nil, a, cons>(q_gen_160, q_gen_214) -> q_gen_237
<b, cons, cons>(q_gen_235, q_gen_177, q_gen_171, q_gen_234) -> q_gen_238
<b, cons, b>(q_gen_165, q_gen_176) -> q_gen_239
<b, a, cons>(q_gen_160, q_gen_214) -> q_gen_240
<cons, cons, cons>(q_gen_222, q_gen_243, q_gen_220, q_gen_227, q_gen_218, q_gen_242, q_gen_217, q_gen_195) -> q_gen_241
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_242
<a, b, cons>(q_gen_160, q_gen_159) -> q_gen_243
<cons, cons, cons>(q_gen_200, q_gen_246, q_gen_187, q_gen_204, q_gen_197, q_gen_245, q_gen_183, q_gen_202) -> q_gen_244
<nil, a, cons>(q_gen_165, q_gen_176) -> q_gen_245
<b, a, cons>(q_gen_165, q_gen_176) -> q_gen_246
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_142, q_gen_143, q_gen_153, q_gen_154, q_gen_167, q_gen_168, q_gen_169, q_gen_178, q_gen_179, q_gen_190, q_gen_191, q_gen_192, q_gen_193, q_gen_230, q_gen_231, q_gen_247},
Q_f={},
Delta=
{
<z>() -> q_gen_169
<s>(q_gen_169) -> q_gen_193
<nil, z>() -> q_gen_140
<cons, s>(q_gen_143, q_gen_140) -> q_gen_142
<b, z>() -> q_gen_143
<cons, s>(q_gen_154, q_gen_140) -> q_gen_153
<a, z>() -> q_gen_154
<cons, s>(q_gen_168, q_gen_153) -> q_gen_167
<b, s>(q_gen_169) -> q_gen_168
<cons, s>(q_gen_179, q_gen_142) -> q_gen_178
<a, s>(q_gen_169) -> q_gen_179
<cons, s>(q_gen_168, q_gen_142) -> q_gen_190
<cons, s>(q_gen_192, q_gen_190) -> q_gen_191
<b, s>(q_gen_193) -> q_gen_192
<cons, s>(q_gen_231, q_gen_190) -> q_gen_230
<a, s>(q_gen_193) -> q_gen_231
<cons, s>(q_gen_179, q_gen_153) -> q_gen_247
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004367 s (model generation: 0.004030,  model checking: 0.000337):

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> length([nil, z]) -> 3  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 1  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 1  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 1
}
Sat witness: Yes: (() -> length([nil, z]), {

})

-------------------------------------------
Step 1, which took 0.004522 s (model generation: 0.003543,  model checking: 0.000979):

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> length([nil, z]) -> 3  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 1  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 1  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 1
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.003438 s (model generation: 0.003368,  model checking: 0.000070):

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> length([nil, z]) -> 3  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 1  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 1  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 4
}
Sat witness: Yes: ((length([ll, _yy])) -> length([cons(x, ll), s(_yy)]), {
_yy -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 3, which took 0.004210 s (model generation: 0.003399,  model checking: 0.000811):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143},
Q_f={q_gen_140},
Delta=
{
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> length([nil, z]) -> 3  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 1  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 4  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 4
}
Sat witness: Yes: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.005169 s (model generation: 0.003641,  model checking: 0.001528):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148},
Q_f={q_gen_141},
Delta=
{
<nil, nil>() -> q_gen_145
<nil, b>() -> q_gen_146
<b, nil>() -> q_gen_147
<b, b>() -> q_gen_148
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143},
Q_f={q_gen_140},
Delta=
{
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> length([nil, z]) -> 4  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 2  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 4  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 4
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 5, which took 0.004844 s (model generation: 0.004264,  model checking: 0.000580):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148},
Q_f={q_gen_141},
Delta=
{
<nil, nil>() -> q_gen_145
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, nil>() -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143},
Q_f={q_gen_140},
Delta=
{
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> length([nil, z]) -> 4  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 3  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 4  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 7
}
Sat witness: Yes: ((length([ll, _yy])) -> length([cons(x, ll), s(_yy)]), {
_yy -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 6, which took 0.012961 s (model generation: 0.005615,  model checking: 0.007346):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148},
Q_f={q_gen_141},
Delta=
{
<nil, nil>() -> q_gen_145
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, nil>() -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143},
Q_f={q_gen_140},
Delta=
{
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, z>() -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> length([nil, z]) -> 4  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 4  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 7  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 7
}
Sat witness: Yes: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 7, which took 0.019120 s (model generation: 0.005158,  model checking: 0.013962):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160},
Q_f={q_gen_141},
Delta=
{
<nil>() -> q_gen_159
<a>() -> q_gen_160
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143},
Q_f={q_gen_140},
Delta=
{
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, z>() -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> length([nil, z]) -> 5  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 5  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 7  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 7
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 8, which took 0.005147 s (model generation: 0.004848,  model checking: 0.000299):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160},
Q_f={q_gen_141},
Delta=
{
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143},
Q_f={q_gen_140},
Delta=
{
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, z>() -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> length([nil, z]) -> 6  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 6  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 7  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 10
}
Sat witness: Yes: ((length([ll, _yy])) -> length([cons(x, ll), s(_yy)]), {
_yy -> s(z)  ;  ll -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 9, which took 0.011991 s (model generation: 0.005280,  model checking: 0.006711):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160},
Q_f={q_gen_141},
Delta=
{
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> length([nil, z]) -> 7  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 7  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 10  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 10
}
Sat witness: Yes: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, nil)  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 10, which took 0.014729 s (model generation: 0.005424,  model checking: 0.009305):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160},
Q_f={q_gen_141},
Delta=
{
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> length([nil, z]) -> 8  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 8  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 10  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 10
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 11, which took 0.006854 s (model generation: 0.005978,  model checking: 0.000876):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160},
Q_f={q_gen_141},
Delta=
{
<cons>(q_gen_160, q_gen_159) -> q_gen_159
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> length([nil, z]) -> 9  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 9  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 10  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 13
}
Sat witness: Yes: ((length([ll, _yy])) -> length([cons(x, ll), s(_yy)]), {
_yy -> s(z)  ;  ll -> cons(b, nil)  ;  x -> a
})

-------------------------------------------
Step 12, which took 0.012426 s (model generation: 0.006196,  model checking: 0.006230):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160},
Q_f={q_gen_141},
Delta=
{
<cons>(q_gen_160, q_gen_159) -> q_gen_159
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> length([nil, z]) -> 10  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 10  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 13  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 13
}
Sat witness: Yes: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.007588 s (model generation: 0.007332,  model checking: 0.000256):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189},
Q_f={q_gen_141},
Delta=
{
<cons>(q_gen_160, q_gen_159) -> q_gen_159
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_141) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<nil, nil, b>() -> q_gen_183
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, b>() -> q_gen_185
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, b>() -> q_gen_187
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, b>() -> q_gen_189
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> length([nil, z]) -> 10  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 13  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 13  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 13
}
Sat witness: Yes: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> nil  ;  _dz -> z  ;  _ez -> cons(b, nil)  ;  _fz -> s(z)  ;  l1 -> nil  ;  l2 -> nil
})

-------------------------------------------
Step 14, which took 0.015477 s (model generation: 0.009063,  model checking: 0.006414):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160, q_gen_182, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189},
Q_f={q_gen_141},
Delta=
{
<cons>(q_gen_160, q_gen_159) -> q_gen_159
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_182
<nil, nil, b>() -> q_gen_183
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, b>() -> q_gen_185
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, b>() -> q_gen_187
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, b>() -> q_gen_189
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> length([nil, z]) -> 11  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 13  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 13  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 16
}
Sat witness: Yes: ((length([ll, _yy])) -> length([cons(x, ll), s(_yy)]), {
_yy -> s(s(z))  ;  ll -> cons(b, cons(b, nil))  ;  x -> b
})

-------------------------------------------
Step 15, which took 0.120004 s (model generation: 0.012672,  model checking: 0.107332):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160, q_gen_182, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189},
Q_f={q_gen_141},
Delta=
{
<cons>(q_gen_160, q_gen_159) -> q_gen_159
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_182
<nil, nil, b>() -> q_gen_183
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, b>() -> q_gen_185
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, b>() -> q_gen_187
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, b>() -> q_gen_189
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<s>(q_gen_169) -> q_gen_169
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> length([nil, z]) -> 12  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 13  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 16  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 16
}
Sat witness: Yes: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 0.010254 s (model generation: 0.009471,  model checking: 0.000783):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160, q_gen_182, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189},
Q_f={q_gen_141},
Delta=
{
<cons>(q_gen_160, q_gen_159) -> q_gen_159
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_182
<nil, nil, b>() -> q_gen_183
<nil, a, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, a, b>() -> q_gen_185
<nil, b, b>() -> q_gen_185
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, b>() -> q_gen_187
<b, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, a, b>() -> q_gen_189
<b, b, b>() -> q_gen_189
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<s>(q_gen_169) -> q_gen_169
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> length([nil, z]) -> 13  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 16  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 16  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 16
}
Sat witness: Yes: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, cons(b, nil))  ;  _dz -> s(s(z))  ;  _ez -> cons(b, cons(b, cons(b, nil)))  ;  _fz -> s(s(s(z)))  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 17, which took 0.060730 s (model generation: 0.010572,  model checking: 0.050158):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160, q_gen_176, q_gen_182, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189},
Q_f={q_gen_141},
Delta=
{
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons>(q_gen_160, q_gen_159) -> q_gen_176
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_176) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, cons>(q_gen_160, q_gen_176) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, cons>(q_gen_160, q_gen_176) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_141) -> q_gen_182
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_182
<nil, nil, b>() -> q_gen_183
<nil, a, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_176) -> q_gen_184
<nil, a, b>() -> q_gen_185
<nil, b, b>() -> q_gen_185
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_176) -> q_gen_186
<b, nil, b>() -> q_gen_187
<b, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_176) -> q_gen_188
<b, a, b>() -> q_gen_189
<b, b, b>() -> q_gen_189
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<s>(q_gen_169) -> q_gen_169
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> length([nil, z]) -> 14  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 16  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 16  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 16
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 18, which took 0.056838 s (model generation: 0.012153,  model checking: 0.044685):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160, q_gen_176, q_gen_182, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189},
Q_f={q_gen_141},
Delta=
{
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons>(q_gen_160, q_gen_159) -> q_gen_176
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, a>(q_gen_160, q_gen_176) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_176) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, cons>(q_gen_160, q_gen_176) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, cons>(q_gen_160, q_gen_176) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, cons>(q_gen_160, q_gen_176) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_141) -> q_gen_182
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_182
<nil, nil, b>() -> q_gen_183
<nil, a, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_176) -> q_gen_184
<nil, a, b>() -> q_gen_185
<nil, b, b>() -> q_gen_185
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_176) -> q_gen_186
<b, nil, b>() -> q_gen_187
<b, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_176) -> q_gen_188
<b, a, b>() -> q_gen_189
<b, b, b>() -> q_gen_189
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<s>(q_gen_169) -> q_gen_169
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> length([nil, z]) -> 15  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 16  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 19  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 17
}
Sat witness: Yes: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.014227 s (model generation: 0.013816,  model checking: 0.000411):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160, q_gen_176, q_gen_182, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189},
Q_f={q_gen_141},
Delta=
{
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons>(q_gen_160, q_gen_159) -> q_gen_176
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, cons>(q_gen_160, q_gen_176) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, a>(q_gen_160, q_gen_176) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_176) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, cons>(q_gen_160, q_gen_176) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, cons>(q_gen_160, q_gen_176) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, cons>(q_gen_160, q_gen_176) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_141) -> q_gen_182
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_182
<nil, nil, b>() -> q_gen_183
<nil, a, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_176) -> q_gen_184
<nil, a, b>() -> q_gen_185
<nil, b, b>() -> q_gen_185
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_176) -> q_gen_186
<b, nil, b>() -> q_gen_187
<b, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_176) -> q_gen_188
<b, a, b>() -> q_gen_189
<b, b, b>() -> q_gen_189
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<s>(q_gen_169) -> q_gen_169
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> length([nil, z]) -> 16  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 19  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 19  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 17
}
Sat witness: Yes: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> nil  ;  _dz -> z  ;  _ez -> cons(b, cons(b, nil))  ;  _fz -> s(s(z))  ;  l1 -> nil  ;  l2 -> nil
})

-------------------------------------------
Step 20, which took 0.097309 s (model generation: 0.013797,  model checking: 0.083512):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160, q_gen_176, q_gen_182, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189, q_gen_204},
Q_f={q_gen_141},
Delta=
{
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons>(q_gen_160, q_gen_159) -> q_gen_176
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, cons>(q_gen_160, q_gen_176) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, a>(q_gen_160, q_gen_176) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_176) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, cons>(q_gen_160, q_gen_176) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, cons>(q_gen_160, q_gen_176) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_204, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_182
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_182
<nil, nil, cons>(q_gen_160, q_gen_176) -> q_gen_182
<nil, nil, b>() -> q_gen_183
<nil, a, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_176) -> q_gen_184
<nil, a, b>() -> q_gen_185
<nil, b, b>() -> q_gen_185
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, b>() -> q_gen_187
<b, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_176) -> q_gen_188
<b, a, b>() -> q_gen_189
<b, b, b>() -> q_gen_189
<b, nil, cons>(q_gen_160, q_gen_176) -> q_gen_204
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<s>(q_gen_169) -> q_gen_169
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19  ;  () -> length([nil, z]) -> 17  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 19  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 19  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 17
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(a, cons(b, cons(b, nil))))
})

-------------------------------------------
Step 21, which took 0.929771 s (model generation: 0.013927,  model checking: 0.915844):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160, q_gen_176, q_gen_182, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189, q_gen_205},
Q_f={q_gen_141},
Delta=
{
<cons>(q_gen_160, q_gen_176) -> q_gen_159
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons>(q_gen_160, q_gen_159) -> q_gen_176
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, cons>(q_gen_160, q_gen_176) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, a>(q_gen_160, q_gen_176) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_176) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, cons>(q_gen_160, q_gen_176) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, cons>(q_gen_160, q_gen_176) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<cons, cons, cons>(q_gen_189, q_gen_205, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_182
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_182
<nil, nil, cons>(q_gen_160, q_gen_176) -> q_gen_182
<nil, nil, b>() -> q_gen_183
<nil, a, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_176) -> q_gen_184
<nil, a, b>() -> q_gen_185
<nil, b, b>() -> q_gen_185
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_176) -> q_gen_186
<b, nil, b>() -> q_gen_187
<b, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, a, b>() -> q_gen_189
<b, b, b>() -> q_gen_189
<b, b, cons>(q_gen_160, q_gen_176) -> q_gen_205
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<s>(q_gen_169) -> q_gen_169
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19  ;  () -> length([nil, z]) -> 18  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 19  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 22  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 18
}
Sat witness: Yes: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 22, which took 0.016468 s (model generation: 0.015769,  model checking: 0.000699):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_151, q_gen_159, q_gen_160, q_gen_180, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189, q_gen_200},
Q_f={q_gen_141},
Delta=
{
<cons>(q_gen_160, q_gen_159) -> q_gen_159
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<cons, cons>(q_gen_148, q_gen_151, q_gen_146, q_gen_145) -> q_gen_145
<nil, cons>(q_gen_160, q_gen_159) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<a, cons>(q_gen_160, q_gen_159) -> q_gen_151
<a, nil>() -> q_gen_151
<b, cons>(q_gen_160, q_gen_159) -> q_gen_151
<cons, cons, cons>(q_gen_200, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_180) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_151, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_151, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_180) -> q_gen_180
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_180
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_180
<nil, nil, a>() -> q_gen_183
<nil, nil, b>() -> q_gen_183
<nil, a, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, a, b>() -> q_gen_185
<nil, b, a>() -> q_gen_185
<nil, b, b>() -> q_gen_185
<a, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<a, nil, a>() -> q_gen_187
<b, nil, b>() -> q_gen_187
<a, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<a, b, a>() -> q_gen_189
<b, b, b>() -> q_gen_189
<b, a, b>() -> q_gen_200
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<s>(q_gen_169) -> q_gen_169
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19  ;  () -> length([nil, z]) -> 19  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 22  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 22  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 19
}
Sat witness: Yes: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, cons(b, nil))  ;  _dz -> s(s(z))  ;  _ez -> cons(b, nil)  ;  _fz -> s(z)  ;  l1 -> nil  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 23, which took 0.021070 s (model generation: 0.017017,  model checking: 0.004053):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_150, q_gen_159, q_gen_160, q_gen_180, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189, q_gen_199},
Q_f={q_gen_141},
Delta=
{
<cons>(q_gen_160, q_gen_159) -> q_gen_159
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<cons, cons>(q_gen_148, q_gen_147, q_gen_150, q_gen_145) -> q_gen_145
<nil, cons>(q_gen_160, q_gen_159) -> q_gen_145
<nil, nil>() -> q_gen_145
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, a>(q_gen_160, q_gen_159) -> q_gen_150
<cons, b>(q_gen_160, q_gen_159) -> q_gen_150
<nil, a>() -> q_gen_150
<cons, cons, cons>(q_gen_189, q_gen_199, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_180) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_150, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_150, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_180) -> q_gen_180
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_180
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_180
<nil, nil, a>() -> q_gen_183
<nil, nil, b>() -> q_gen_183
<nil, a, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, a, b>() -> q_gen_185
<nil, b, a>() -> q_gen_185
<nil, b, b>() -> q_gen_185
<a, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<a, nil, a>() -> q_gen_187
<b, nil, b>() -> q_gen_187
<a, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<a, b, a>() -> q_gen_189
<b, a, b>() -> q_gen_189
<b, b, b>() -> q_gen_189
<b, a, cons>(q_gen_160, q_gen_159) -> q_gen_199
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<s>(q_gen_169) -> q_gen_169
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22  ;  () -> length([nil, z]) -> 20  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 22  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 22  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 20
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 24, which took 0.016097 s (model generation: 0.015880,  model checking: 0.000217):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160, q_gen_182, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189},
Q_f={q_gen_141},
Delta=
{
<cons>(q_gen_160, q_gen_159) -> q_gen_159
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, cons>(q_gen_160, q_gen_159) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_182
<nil, nil, a>() -> q_gen_183
<nil, nil, b>() -> q_gen_183
<nil, a, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, a, b>() -> q_gen_185
<nil, b, a>() -> q_gen_185
<nil, b, b>() -> q_gen_185
<a, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<a, nil, a>() -> q_gen_187
<b, nil, b>() -> q_gen_187
<a, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<a, b, a>() -> q_gen_189
<b, a, b>() -> q_gen_189
<b, b, b>() -> q_gen_189
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_142, q_gen_143, q_gen_154, q_gen_169, q_gen_190},
Q_f={q_gen_140, q_gen_142},
Delta=
{
<s>(q_gen_169) -> q_gen_169
<z>() -> q_gen_169
<cons, s>(q_gen_154, q_gen_140) -> q_gen_140
<cons, s>(q_gen_154, q_gen_142) -> q_gen_140
<nil, z>() -> q_gen_140
<cons, s>(q_gen_143, q_gen_140) -> q_gen_142
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
<a, s>(q_gen_169) -> q_gen_154
<a, z>() -> q_gen_154
<cons, s>(q_gen_143, q_gen_142) -> q_gen_190
<cons, s>(q_gen_143, q_gen_190) -> q_gen_190
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22  ;  () -> length([nil, z]) -> 20  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 22  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 22  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 23
}
Sat witness: Yes: ((length([ll, _yy])) -> length([cons(x, ll), s(_yy)]), {
_yy -> s(z)  ;  ll -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 25, which took 0.220133 s (model generation: 0.015462,  model checking: 0.204671):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160, q_gen_176, q_gen_182, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189, q_gen_201, q_gen_210},
Q_f={q_gen_141},
Delta=
{
<cons>(q_gen_160, q_gen_176) -> q_gen_159
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons>(q_gen_160, q_gen_159) -> q_gen_176
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, a>(q_gen_160, q_gen_176) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_176) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, cons>(q_gen_160, q_gen_176) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, cons>(q_gen_160, q_gen_176) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<nil, cons>(q_gen_160, q_gen_159) -> q_gen_210
<nil, cons>(q_gen_160, q_gen_176) -> q_gen_210
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_210) -> q_gen_182
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_182
<nil, nil, a>() -> q_gen_183
<nil, nil, b>() -> q_gen_183
<nil, a, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_176) -> q_gen_184
<nil, a, b>() -> q_gen_185
<nil, b, a>() -> q_gen_185
<nil, b, b>() -> q_gen_185
<a, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_176) -> q_gen_186
<a, nil, a>() -> q_gen_187
<b, nil, b>() -> q_gen_187
<a, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_176) -> q_gen_188
<a, b, a>() -> q_gen_189
<b, a, b>() -> q_gen_189
<b, b, b>() -> q_gen_189
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_201) -> q_gen_201
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_210) -> q_gen_201
<nil, nil, cons>(q_gen_160, q_gen_176) -> q_gen_201
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<s>(q_gen_169) -> q_gen_169
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22  ;  () -> length([nil, z]) -> 21  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 22  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 25  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 23
}
Sat witness: Yes: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 26, which took 0.022683 s (model generation: 0.019207,  model checking: 0.003476):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160, q_gen_176, q_gen_182, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189, q_gen_203, q_gen_224},
Q_f={q_gen_141},
Delta=
{
<cons>(q_gen_160, q_gen_176) -> q_gen_159
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons>(q_gen_160, q_gen_159) -> q_gen_176
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, cons>(q_gen_160, q_gen_176) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, a>(q_gen_160, q_gen_176) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_176) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, cons>(q_gen_160, q_gen_176) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, cons>(q_gen_160, q_gen_176) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<nil, cons>(q_gen_160, q_gen_159) -> q_gen_224
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_203, q_gen_183, q_gen_182) -> q_gen_182
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_224) -> q_gen_182
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_182
<nil, nil, cons>(q_gen_160, q_gen_176) -> q_gen_182
<nil, nil, a>() -> q_gen_183
<nil, nil, b>() -> q_gen_183
<nil, a, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, a, a>() -> q_gen_185
<nil, a, b>() -> q_gen_185
<nil, b, a>() -> q_gen_185
<nil, b, b>() -> q_gen_185
<a, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_176) -> q_gen_186
<a, nil, a>() -> q_gen_187
<b, nil, b>() -> q_gen_187
<a, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<a, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_176) -> q_gen_188
<a, a, a>() -> q_gen_189
<a, b, a>() -> q_gen_189
<b, a, b>() -> q_gen_189
<b, b, b>() -> q_gen_189
<nil, b, cons>(q_gen_160, q_gen_176) -> q_gen_203
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<s>(q_gen_169) -> q_gen_169
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22  ;  () -> length([nil, z]) -> 22  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 25  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 25  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 23
}
Sat witness: Yes: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(a, nil)  ;  _dz -> s(z)  ;  _ez -> cons(a, cons(b, cons(b, nil)))  ;  _fz -> s(s(s(z)))  ;  l1 -> nil  ;  l2 -> cons(a, nil)
})

-------------------------------------------
Step 27, which took 22.223764 s (model generation: 0.019573,  model checking: 22.204191):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160, q_gen_176, q_gen_182, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189, q_gen_203, q_gen_210},
Q_f={q_gen_141},
Delta=
{
<cons>(q_gen_160, q_gen_176) -> q_gen_159
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons>(q_gen_160, q_gen_159) -> q_gen_176
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, a>(q_gen_160, q_gen_176) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_176) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, cons>(q_gen_160, q_gen_176) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, cons>(q_gen_160, q_gen_176) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, b>() -> q_gen_148
<nil, cons>(q_gen_160, q_gen_159) -> q_gen_210
<nil, cons>(q_gen_160, q_gen_176) -> q_gen_210
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_203, q_gen_183, q_gen_182) -> q_gen_182
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_210) -> q_gen_182
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_210) -> q_gen_182
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_182
<nil, nil, cons>(q_gen_160, q_gen_176) -> q_gen_182
<nil, nil, a>() -> q_gen_183
<nil, nil, b>() -> q_gen_183
<nil, a, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, a, a>() -> q_gen_185
<nil, a, b>() -> q_gen_185
<nil, b, a>() -> q_gen_185
<nil, b, b>() -> q_gen_185
<a, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_176) -> q_gen_186
<a, nil, a>() -> q_gen_187
<b, nil, b>() -> q_gen_187
<a, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<a, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_176) -> q_gen_188
<a, a, a>() -> q_gen_189
<a, b, a>() -> q_gen_189
<b, a, b>() -> q_gen_189
<b, b, b>() -> q_gen_189
<nil, b, cons>(q_gen_160, q_gen_176) -> q_gen_203
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<s>(q_gen_169) -> q_gen_169
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23  ;  () -> length([nil, z]) -> 23  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 25  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 28  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 24
}
Sat witness: Yes: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(a, cons(b, cons(b, nil)))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, cons(b, nil)))  ;  t1 -> nil
})

-------------------------------------------
Step 28, which took 0.052465 s (model generation: 0.022517,  model checking: 0.029948):

Model:
|_
{
append -> 
{{{
Q={q_gen_141, q_gen_145, q_gen_146, q_gen_147, q_gen_148, q_gen_159, q_gen_160, q_gen_176, q_gen_182, q_gen_183, q_gen_184, q_gen_185, q_gen_186, q_gen_187, q_gen_188, q_gen_189, q_gen_205, q_gen_210},
Q_f={q_gen_141},
Delta=
{
<nil>() -> q_gen_159
<a>() -> q_gen_160
<b>() -> q_gen_160
<cons>(q_gen_160, q_gen_159) -> q_gen_176
<cons>(q_gen_160, q_gen_176) -> q_gen_176
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_145
<nil, nil>() -> q_gen_145
<cons, a>(q_gen_160, q_gen_159) -> q_gen_146
<cons, a>(q_gen_160, q_gen_176) -> q_gen_146
<cons, b>(q_gen_160, q_gen_159) -> q_gen_146
<cons, b>(q_gen_160, q_gen_176) -> q_gen_146
<nil, a>() -> q_gen_146
<nil, b>() -> q_gen_146
<a, cons>(q_gen_160, q_gen_159) -> q_gen_147
<a, cons>(q_gen_160, q_gen_176) -> q_gen_147
<a, nil>() -> q_gen_147
<b, cons>(q_gen_160, q_gen_159) -> q_gen_147
<b, cons>(q_gen_160, q_gen_176) -> q_gen_147
<b, nil>() -> q_gen_147
<a, a>() -> q_gen_148
<b, a>() -> q_gen_148
<b, b>() -> q_gen_148
<cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_210) -> q_gen_210
<nil, cons>(q_gen_160, q_gen_159) -> q_gen_210
<nil, cons>(q_gen_160, q_gen_176) -> q_gen_210
<cons, cons, cons>(q_gen_189, q_gen_188, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_141
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_145) -> q_gen_141
<nil, nil, nil>() -> q_gen_141
<cons, cons, cons>(q_gen_189, q_gen_205, q_gen_187, q_gen_186, q_gen_185, q_gen_184, q_gen_183, q_gen_182) -> q_gen_182
<cons, nil, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_210) -> q_gen_182
<nil, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_210) -> q_gen_182
<nil, nil, cons>(q_gen_160, q_gen_159) -> q_gen_182
<nil, nil, cons>(q_gen_160, q_gen_176) -> q_gen_182
<nil, cons, b>(q_gen_160, q_gen_176) -> q_gen_183
<nil, nil, a>() -> q_gen_183
<nil, nil, b>() -> q_gen_183
<nil, a, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, a, cons>(q_gen_160, q_gen_176) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_159) -> q_gen_184
<nil, b, cons>(q_gen_160, q_gen_176) -> q_gen_184
<nil, a, a>() -> q_gen_185
<nil, a, b>() -> q_gen_185
<nil, b, a>() -> q_gen_185
<nil, b, b>() -> q_gen_185
<a, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, cons, cons>(q_gen_148, q_gen_147, q_gen_146, q_gen_210) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_159) -> q_gen_186
<b, nil, cons>(q_gen_160, q_gen_176) -> q_gen_186
<a, nil, a>() -> q_gen_187
<b, cons, b>(q_gen_160, q_gen_176) -> q_gen_187
<b, nil, b>() -> q_gen_187
<a, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<a, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, a, cons>(q_gen_160, q_gen_159) -> q_gen_188
<b, a, cons>(q_gen_160, q_gen_176) -> q_gen_188
<b, b, cons>(q_gen_160, q_gen_159) -> q_gen_188
<a, a, a>() -> q_gen_189
<a, b, a>() -> q_gen_189
<b, a, b>() -> q_gen_189
<b, b, b>() -> q_gen_189
<b, b, cons>(q_gen_160, q_gen_176) -> q_gen_205
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_140, q_gen_143, q_gen_169},
Q_f={q_gen_140},
Delta=
{
<s>(q_gen_169) -> q_gen_169
<z>() -> q_gen_169
<cons, s>(q_gen_143, q_gen_140) -> q_gen_140
<nil, z>() -> q_gen_140
<a, s>(q_gen_169) -> q_gen_143
<a, z>() -> q_gen_143
<b, s>(q_gen_169) -> q_gen_143
<b, z>() -> q_gen_143
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24  ;  () -> length([nil, z]) -> 24  ;  (append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 28  ;  (append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 28  ;  (length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 25
}
Sat witness: Yes: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(a, cons(a, nil))  ;  _dz -> s(s(z))  ;  _ez -> cons(b, cons(b, cons(b, nil)))  ;  _fz -> s(s(s(z)))  ;  l1 -> cons(a, nil)  ;  l2 -> cons(b, nil)
})

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