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


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 20.910450 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450, q_gen_3473, q_gen_3474, q_gen_3491},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<a, b>() -> q_gen_3473
<b, a>() -> q_gen_3473
<cons, cons>(q_gen_3435, q_gen_3491) -> q_gen_3491
<cons, cons>(q_gen_3473, q_gen_3434) -> q_gen_3491
<cons, cons>(q_gen_3473, q_gen_3491) -> q_gen_3491
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3491) -> q_gen_3430
<nil, cons, cons>(q_gen_3473, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3473, q_gen_3491) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
<cons, cons, cons>(q_gen_3450, q_gen_3474) -> q_gen_3474
<cons, nil, cons>(q_gen_3435, q_gen_3491) -> q_gen_3474
<cons, nil, cons>(q_gen_3473, q_gen_3434) -> q_gen_3474
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438, q_gen_3475, q_gen_3476},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
<cons, cons>(q_gen_3432, q_gen_3475) -> q_gen_3475
<cons, cons>(q_gen_3476, q_gen_3429) -> q_gen_3475
<a, b>() -> q_gen_3476
<b, a>() -> q_gen_3476
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005399 s (model generation: 0.004758,  model checking: 0.000641):

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

}

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

}

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

}
--
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: Found: (() -> prefix([nil, y]), {
y -> nil
})

-------------------------------------------
Step 1, which took 0.005206 s (model generation: 0.004823,  model checking: 0.000383):

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

}

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

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

}
--
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: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.004998 s (model generation: 0.004863,  model checking: 0.000135):

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

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

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

}
--
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: Found: ((prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]), {
y2 -> b  ;  ys -> nil  ;  zs -> nil
})

-------------------------------------------
Step 3, which took 0.005710 s (model generation: 0.005556,  model checking: 0.000154):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432},
Q_f={q_gen_3429},
Delta=
{
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<b, b>() -> q_gen_3432
}

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

}
--
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: Found: ((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.007889 s (model generation: 0.005103,  model checking: 0.002786):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435},
Q_f={q_gen_3430},
Delta=
{
<nil, nil>() -> q_gen_3434
<b, b>() -> q_gen_3435
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432},
Q_f={q_gen_3429},
Delta=
{
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<b, b>() -> q_gen_3432
}

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

}
--
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: Found: (() -> prefix([nil, y]), {
y -> cons(b, nil)
})

-------------------------------------------
Step 5, which took 0.011669 s (model generation: 0.008288,  model checking: 0.003381):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435},
Q_f={q_gen_3430},
Delta=
{
<nil, nil>() -> q_gen_3434
<b, b>() -> q_gen_3435
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438},
Q_f={q_gen_3429},
Delta=
{
<nil>() -> q_gen_3437
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<b, b>() -> q_gen_3432
}

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

}
--
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: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 6, which took 0.011411 s (model generation: 0.010721,  model checking: 0.000690):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435},
Q_f={q_gen_3430},
Delta=
{
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438},
Q_f={q_gen_3429},
Delta=
{
<nil>() -> q_gen_3437
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<b, b>() -> q_gen_3432
}

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

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

-------------------------------------------
Step 7, which took 0.020721 s (model generation: 0.013004,  model checking: 0.007717):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435},
Q_f={q_gen_3430},
Delta=
{
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438},
Q_f={q_gen_3429},
Delta=
{
<nil>() -> q_gen_3437
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
}

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

}
--
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)]) -> 5
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 5
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 5
(prefix([cons(z, zs), nil])) -> BOT -> 5
}
Sat witness: Found: ((append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]), {
_nr -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 8, which took 0.020206 s (model generation: 0.014415,  model checking: 0.005791):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450},
Q_f={q_gen_3430},
Delta=
{
<nil>() -> q_gen_3448
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<b, b, b>() -> q_gen_3450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438},
Q_f={q_gen_3429},
Delta=
{
<nil>() -> q_gen_3437
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
}

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

}
--
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)]) -> 6
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 6
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 6
(prefix([cons(z, zs), nil])) -> BOT -> 6
}
Sat witness: Found: ((append([l1, l2, _sr])) -> prefix([l1, _sr]), {
_sr -> cons(a, cons(a, nil))  ;  l1 -> nil  ;  l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 9, which took 0.020501 s (model generation: 0.014925,  model checking: 0.005576):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450},
Q_f={q_gen_3430},
Delta=
{
<nil>() -> q_gen_3448
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<b, b, b>() -> q_gen_3450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
}

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

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

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

-------------------------------------------
Step 10, which took 0.023317 s (model generation: 0.015841,  model checking: 0.007476):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450},
Q_f={q_gen_3430},
Delta=
{
<nil>() -> q_gen_3448
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<b, b, b>() -> q_gen_3450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
}

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

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

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

-------------------------------------------
Step 11, which took 0.024977 s (model generation: 0.016657,  model checking: 0.008320):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450},
Q_f={q_gen_3430},
Delta=
{
<nil>() -> q_gen_3448
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, b, a>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
}

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

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

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

-------------------------------------------
Step 12, which took 0.024929 s (model generation: 0.018933,  model checking: 0.005996):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450},
Q_f={q_gen_3430},
Delta=
{
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
}

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

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

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

-------------------------------------------
Step 13, which took 0.011557 s (model generation: 0.008590,  model checking: 0.002967):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450},
Q_f={q_gen_3430},
Delta=
{
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
}

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

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

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

-------------------------------------------
Step 14, which took 0.014206 s (model generation: 0.009755,  model checking: 0.004451):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
}

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

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

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

-------------------------------------------
Step 15, which took 0.012360 s (model generation: 0.010795,  model checking: 0.001565):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
}

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

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

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

-------------------------------------------
Step 16, which took 0.012432 s (model generation: 0.012206,  model checking: 0.000226):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
}

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

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

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

-------------------------------------------
Step 17, which took 0.015245 s (model generation: 0.012122,  model checking: 0.003123):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3447, q_gen_3448, q_gen_3449, q_gen_3450, q_gen_3473},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<b, a>() -> q_gen_3473
<cons, cons, cons>(q_gen_3450, q_gen_3447) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<cons, nil, cons>(q_gen_3473, q_gen_3434) -> q_gen_3447
<nil, cons, cons>(q_gen_3473, q_gen_3434) -> q_gen_3447
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3447
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438, q_gen_3475, q_gen_3476},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
<cons, cons>(q_gen_3476, q_gen_3429) -> q_gen_3475
<b, a>() -> q_gen_3476
}

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

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

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

-------------------------------------------
Step 18, which took 0.014489 s (model generation: 0.013798,  model checking: 0.000691):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450, q_gen_3473, q_gen_3474},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<b, a>() -> q_gen_3473
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, cons, cons>(q_gen_3450, q_gen_3474) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3473, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
<cons, nil, cons>(q_gen_3473, q_gen_3434) -> q_gen_3474
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438, q_gen_3475, q_gen_3476},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<cons, cons>(q_gen_3432, q_gen_3475) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
<cons, cons>(q_gen_3476, q_gen_3429) -> q_gen_3475
<b, a>() -> q_gen_3476
}

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

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

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

-------------------------------------------
Step 19, which took 0.026641 s (model generation: 0.013600,  model checking: 0.013041):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450, q_gen_3473, q_gen_3474},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<b, a>() -> q_gen_3473
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3473, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
<cons, cons, cons>(q_gen_3450, q_gen_3474) -> q_gen_3474
<cons, nil, cons>(q_gen_3473, q_gen_3434) -> q_gen_3474
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438, q_gen_3475, q_gen_3476},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
<cons, cons>(q_gen_3432, q_gen_3475) -> q_gen_3475
<cons, cons>(q_gen_3476, q_gen_3429) -> q_gen_3475
<b, a>() -> q_gen_3476
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> prefix([nil, y]) -> 15
(append([l1, l2, _sr])) -> prefix([l1, _sr]) -> 21
(append([t1, l2, _nr])) -> append([cons(h1, t1), l2, cons(h1, _nr)]) -> 28
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 15
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 18
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 18
(prefix([cons(z, zs), nil])) -> BOT -> 16
}
Sat witness: Found: ((append([t1, l2, _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 20, which took 0.018611 s (model generation: 0.016193,  model checking: 0.002418):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450, q_gen_3473, q_gen_3474},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<a, b>() -> q_gen_3435
<b, b>() -> q_gen_3435
<b, a>() -> q_gen_3473
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3473, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
<cons, cons, cons>(q_gen_3450, q_gen_3474) -> q_gen_3474
<cons, nil, cons>(q_gen_3473, q_gen_3434) -> q_gen_3474
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438, q_gen_3475, q_gen_3476},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
<cons, cons>(q_gen_3432, q_gen_3475) -> q_gen_3475
<cons, cons>(q_gen_3476, q_gen_3429) -> q_gen_3475
<b, a>() -> q_gen_3476
}

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

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

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

-------------------------------------------
Step 21, which took 0.019220 s (model generation: 0.018036,  model checking: 0.001184):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450, q_gen_3473, q_gen_3474},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<a, b>() -> q_gen_3435
<b, b>() -> q_gen_3435
<b, a>() -> q_gen_3473
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3473, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
<cons, cons, cons>(q_gen_3450, q_gen_3474) -> q_gen_3474
<cons, nil, cons>(q_gen_3473, q_gen_3434) -> q_gen_3474
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438, q_gen_3475, q_gen_3476},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<a, b>() -> q_gen_3432
<b, b>() -> q_gen_3432
<cons, cons>(q_gen_3432, q_gen_3475) -> q_gen_3475
<cons, cons>(q_gen_3476, q_gen_3429) -> q_gen_3475
<b, a>() -> q_gen_3476
}

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

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

-------------------------------------------
Step 22, which took 0.018259 s (model generation: 0.018080,  model checking: 0.000179):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3441, q_gen_3442, q_gen_3448, q_gen_3449, q_gen_3450},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<cons, cons>(q_gen_3441, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<b, b>() -> q_gen_3435
<a, a>() -> q_gen_3441
<a, b>() -> q_gen_3441
<b, a>() -> q_gen_3441
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3441, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<cons, cons, cons>(q_gen_3450, q_gen_3442) -> q_gen_3442
<cons, nil, cons>(q_gen_3441, q_gen_3434) -> q_gen_3442
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3442
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438, q_gen_3443, q_gen_3444},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<b, b>() -> q_gen_3432
<cons, cons>(q_gen_3432, q_gen_3443) -> q_gen_3443
<cons, cons>(q_gen_3444, q_gen_3429) -> q_gen_3443
<a, a>() -> q_gen_3444
<a, b>() -> q_gen_3444
<b, a>() -> q_gen_3444
}

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

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

-------------------------------------------
Step 23, which took 0.016514 s (model generation: 0.016148,  model checking: 0.000366):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3441, q_gen_3442, q_gen_3448, q_gen_3449, q_gen_3450},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<cons, cons>(q_gen_3441, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<b, b>() -> q_gen_3435
<a, a>() -> q_gen_3441
<a, b>() -> q_gen_3441
<b, a>() -> q_gen_3441
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3441, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<cons, cons, cons>(q_gen_3450, q_gen_3442) -> q_gen_3442
<cons, nil, cons>(q_gen_3441, q_gen_3434) -> q_gen_3442
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3442
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438, q_gen_3475, q_gen_3476},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
<cons, cons>(q_gen_3432, q_gen_3475) -> q_gen_3475
<cons, cons>(q_gen_3476, q_gen_3429) -> q_gen_3475
<a, b>() -> q_gen_3476
<b, a>() -> q_gen_3476
}

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

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

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

-------------------------------------------
Step 24, which took 0.039698 s (model generation: 0.016449,  model checking: 0.023249):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450, q_gen_3473, q_gen_3474},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<a, b>() -> q_gen_3473
<b, a>() -> q_gen_3473
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3473, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
<cons, cons, cons>(q_gen_3450, q_gen_3474) -> q_gen_3474
<cons, nil, cons>(q_gen_3473, q_gen_3434) -> q_gen_3474
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438, q_gen_3475, q_gen_3476},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
<cons, cons>(q_gen_3432, q_gen_3475) -> q_gen_3475
<cons, cons>(q_gen_3476, q_gen_3429) -> q_gen_3475
<a, b>() -> q_gen_3476
<b, a>() -> q_gen_3476
}

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

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

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

-------------------------------------------
Step 25, which took 0.063030 s (model generation: 0.057711,  model checking: 0.005319):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450, q_gen_3473, q_gen_3474},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<cons, cons>(q_gen_3473, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<a, b>() -> q_gen_3473
<b, a>() -> q_gen_3473
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3473, q_gen_3434) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
<cons, cons, cons>(q_gen_3450, q_gen_3474) -> q_gen_3474
<cons, nil, cons>(q_gen_3473, q_gen_3434) -> q_gen_3474
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438, q_gen_3475, q_gen_3476},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
<cons, cons>(q_gen_3432, q_gen_3475) -> q_gen_3475
<cons, cons>(q_gen_3476, q_gen_3429) -> q_gen_3475
<a, b>() -> q_gen_3476
<b, a>() -> q_gen_3476
}

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

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

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

-------------------------------------------
Step 26, which took 0.119050 s (model generation: 0.063125,  model checking: 0.055925):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450, q_gen_3473, q_gen_3474, q_gen_3491},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<a, b>() -> q_gen_3473
<b, a>() -> q_gen_3473
<cons, cons>(q_gen_3473, q_gen_3434) -> q_gen_3491
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3473, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3473, q_gen_3491) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
<cons, cons, cons>(q_gen_3450, q_gen_3474) -> q_gen_3474
<cons, nil, cons>(q_gen_3435, q_gen_3491) -> q_gen_3474
<cons, nil, cons>(q_gen_3473, q_gen_3434) -> q_gen_3474
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438, q_gen_3475, q_gen_3476},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
<cons, cons>(q_gen_3432, q_gen_3475) -> q_gen_3475
<cons, cons>(q_gen_3476, q_gen_3429) -> q_gen_3475
<a, b>() -> q_gen_3476
<b, a>() -> q_gen_3476
}

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

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

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

-------------------------------------------
Step 27, which took 0.116134 s (model generation: 0.073721,  model checking: 0.042413):

Model:
|_
{
append -> 
{{{
Q={q_gen_3430, q_gen_3434, q_gen_3435, q_gen_3448, q_gen_3449, q_gen_3450, q_gen_3473, q_gen_3474, q_gen_3491},
Q_f={q_gen_3430},
Delta=
{
<cons>(q_gen_3449, q_gen_3448) -> q_gen_3448
<nil>() -> q_gen_3448
<a>() -> q_gen_3449
<b>() -> q_gen_3449
<cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3434
<nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3434
<nil, nil>() -> q_gen_3434
<a, a>() -> q_gen_3435
<b, b>() -> q_gen_3435
<a, b>() -> q_gen_3473
<b, a>() -> q_gen_3473
<cons, cons>(q_gen_3435, q_gen_3491) -> q_gen_3491
<cons, cons>(q_gen_3473, q_gen_3434) -> q_gen_3491
<cons, cons, cons>(q_gen_3450, q_gen_3430) -> q_gen_3430
<cons, nil, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3435, q_gen_3491) -> q_gen_3430
<nil, cons, cons>(q_gen_3473, q_gen_3434) -> q_gen_3430
<nil, cons, cons>(q_gen_3473, q_gen_3491) -> q_gen_3430
<nil, nil, cons>(q_gen_3449, q_gen_3448) -> q_gen_3430
<nil, nil, nil>() -> q_gen_3430
<a, a, a>() -> q_gen_3450
<a, b, a>() -> q_gen_3450
<b, a, b>() -> q_gen_3450
<b, b, b>() -> q_gen_3450
<cons, cons, cons>(q_gen_3450, q_gen_3474) -> q_gen_3474
<cons, nil, cons>(q_gen_3435, q_gen_3491) -> q_gen_3474
<cons, nil, cons>(q_gen_3473, q_gen_3434) -> q_gen_3474
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_3429, q_gen_3432, q_gen_3437, q_gen_3438, q_gen_3475, q_gen_3476},
Q_f={q_gen_3429},
Delta=
{
<cons>(q_gen_3438, q_gen_3437) -> q_gen_3437
<nil>() -> q_gen_3437
<a>() -> q_gen_3438
<b>() -> q_gen_3438
<cons, cons>(q_gen_3432, q_gen_3429) -> q_gen_3429
<nil, cons>(q_gen_3438, q_gen_3437) -> q_gen_3429
<nil, nil>() -> q_gen_3429
<a, a>() -> q_gen_3432
<b, b>() -> q_gen_3432
<cons, cons>(q_gen_3432, q_gen_3475) -> q_gen_3475
<cons, cons>(q_gen_3476, q_gen_3429) -> q_gen_3475
<a, b>() -> q_gen_3476
<b, a>() -> q_gen_3476
}

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

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

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

Total time: 20.910450
Reason for stopping: Proved