Solving ../../benchmarks/false/prefix_append.smt2...

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, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)])}
(append([_jka, _kka, _lka]) /\ append([_jka, _kka, _mka])) -> eq_eltlist([_lka, _mka])
)
}

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


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> prefix([nil, y]) -> 0
(append([l1, l2, _nka])) -> prefix([l2, _nka]) -> 0
(append([t1, l2, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]) -> 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 0.378617 seconds.
Disproved
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010413 s (model generation: 0.009793,  model checking: 0.000620):

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, _nka])) -> prefix([l2, _nka]) -> 1
(append([t1, l2, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]) -> 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.010275 s (model generation: 0.009988,  model checking: 0.000287):

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

}

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

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, _nka])) -> prefix([l2, _nka]) -> 1
(append([t1, l2, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]) -> 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.010522 s (model generation: 0.010192,  model checking: 0.000330):

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

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

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, _nka])) -> prefix([l2, _nka]) -> 1
(append([t1, l2, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]) -> 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.013596 s (model generation: 0.013231,  model checking: 0.000365):

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

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

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, _nka])) -> prefix([l2, _nka]) -> 1
(append([t1, l2, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]) -> 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, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]), {
_ika -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.010925 s (model generation: 0.010693,  model checking: 0.000232):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6747, q_gen_6748},
Q_f={q_gen_6743},
Delta=
{
<nil, nil>() -> q_gen_6747
<b, b>() -> q_gen_6748
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, nil, nil>() -> q_gen_6743
}

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

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, _nka])) -> prefix([l2, _nka]) -> 4
(append([t1, l2, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]) -> 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([l1, l2, _nka])) -> prefix([l2, _nka]), {
_nka -> cons(b, nil)  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 5, which took 0.016309 s (model generation: 0.011190,  model checking: 0.005119):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6747, q_gen_6748},
Q_f={q_gen_6743},
Delta=
{
<nil, nil>() -> q_gen_6747
<b, b>() -> q_gen_6748
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, nil, nil>() -> q_gen_6743
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_6742, q_gen_6745, q_gen_6750, q_gen_6751},
Q_f={q_gen_6742},
Delta=
{
<nil>() -> q_gen_6750
<b>() -> q_gen_6751
<cons, cons>(q_gen_6745, q_gen_6742) -> q_gen_6742
<nil, cons>(q_gen_6751, q_gen_6750) -> q_gen_6742
<nil, nil>() -> q_gen_6742
<b, b>() -> q_gen_6745
}

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, _nka])) -> prefix([l2, _nka]) -> 4
(append([t1, l2, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]) -> 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(a, cons(a, nil))
})

-------------------------------------------
Step 6, which took 0.014407 s (model generation: 0.011744,  model checking: 0.002663):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6747, q_gen_6748},
Q_f={q_gen_6743},
Delta=
{
<nil, nil>() -> q_gen_6747
<b, b>() -> q_gen_6748
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, nil, nil>() -> q_gen_6743
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_6742, q_gen_6745, q_gen_6750, q_gen_6751},
Q_f={q_gen_6742},
Delta=
{
<cons>(q_gen_6751, q_gen_6750) -> q_gen_6750
<nil>() -> q_gen_6750
<a>() -> q_gen_6751
<b>() -> q_gen_6751
<cons, cons>(q_gen_6745, q_gen_6742) -> q_gen_6742
<nil, cons>(q_gen_6751, q_gen_6750) -> q_gen_6742
<nil, nil>() -> q_gen_6742
<b, b>() -> q_gen_6745
}

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, _nka])) -> prefix([l2, _nka]) -> 4
(append([t1, l2, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]) -> 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 7, which took 0.014748 s (model generation: 0.012187,  model checking: 0.002561):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6747, q_gen_6748},
Q_f={q_gen_6743},
Delta=
{
<cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6747
<nil, nil>() -> q_gen_6747
<a, a>() -> q_gen_6748
<b, b>() -> q_gen_6748
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, nil, nil>() -> q_gen_6743
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_6742, q_gen_6745, q_gen_6750, q_gen_6751},
Q_f={q_gen_6742},
Delta=
{
<cons>(q_gen_6751, q_gen_6750) -> q_gen_6750
<nil>() -> q_gen_6750
<a>() -> q_gen_6751
<b>() -> q_gen_6751
<cons, cons>(q_gen_6745, q_gen_6742) -> q_gen_6742
<nil, cons>(q_gen_6751, q_gen_6750) -> q_gen_6742
<nil, nil>() -> q_gen_6742
<b, b>() -> q_gen_6745
}

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

-------------------------------------------
Step 8, which took 0.015127 s (model generation: 0.012824,  model checking: 0.002303):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6747, q_gen_6748},
Q_f={q_gen_6743},
Delta=
{
<cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6747
<nil, nil>() -> q_gen_6747
<a, a>() -> q_gen_6748
<b, b>() -> q_gen_6748
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, nil, nil>() -> q_gen_6743
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_6742, q_gen_6745, q_gen_6750, q_gen_6751},
Q_f={q_gen_6742},
Delta=
{
<cons>(q_gen_6751, q_gen_6750) -> q_gen_6750
<nil>() -> q_gen_6750
<a>() -> q_gen_6751
<b>() -> q_gen_6751
<cons, cons>(q_gen_6745, q_gen_6742) -> q_gen_6742
<nil, cons>(q_gen_6751, q_gen_6750) -> q_gen_6742
<nil, nil>() -> q_gen_6742
<a, a>() -> q_gen_6745
<b, b>() -> q_gen_6745
}

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

-------------------------------------------
Step 9, which took 0.019860 s (model generation: 0.013662,  model checking: 0.006198):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6747, q_gen_6748, q_gen_6763, q_gen_6764, q_gen_6765},
Q_f={q_gen_6743},
Delta=
{
<nil>() -> q_gen_6763
<b>() -> q_gen_6764
<cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6747
<nil, nil>() -> q_gen_6747
<a, a>() -> q_gen_6748
<b, b>() -> q_gen_6748
<cons, cons, cons>(q_gen_6765, q_gen_6743) -> q_gen_6743
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6743
<nil, nil, nil>() -> q_gen_6743
<b, b, b>() -> q_gen_6765
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_6742, q_gen_6745, q_gen_6750, q_gen_6751},
Q_f={q_gen_6742},
Delta=
{
<cons>(q_gen_6751, q_gen_6750) -> q_gen_6750
<nil>() -> q_gen_6750
<a>() -> q_gen_6751
<b>() -> q_gen_6751
<cons, cons>(q_gen_6745, q_gen_6742) -> q_gen_6742
<nil, cons>(q_gen_6751, q_gen_6750) -> q_gen_6742
<nil, nil>() -> q_gen_6742
<a, a>() -> q_gen_6745
<b, b>() -> q_gen_6745
}

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, _nka])) -> prefix([l2, _nka]) -> 5
(append([t1, l2, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]) -> 10
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 8
(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([t1, l2, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]), {
_ika -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.021347 s (model generation: 0.015181,  model checking: 0.006166):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6747, q_gen_6748, q_gen_6763, q_gen_6764, q_gen_6765},
Q_f={q_gen_6743},
Delta=
{
<nil>() -> q_gen_6763
<b>() -> q_gen_6764
<cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6747
<nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6747
<nil, nil>() -> q_gen_6747
<a, a>() -> q_gen_6748
<b, b>() -> q_gen_6748
<cons, cons, cons>(q_gen_6765, q_gen_6743) -> q_gen_6743
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6743
<nil, nil, nil>() -> q_gen_6743
<b, b, b>() -> q_gen_6765
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_6742, q_gen_6745, q_gen_6750, q_gen_6751},
Q_f={q_gen_6742},
Delta=
{
<cons>(q_gen_6751, q_gen_6750) -> q_gen_6750
<nil>() -> q_gen_6750
<a>() -> q_gen_6751
<b>() -> q_gen_6751
<cons, cons>(q_gen_6745, q_gen_6742) -> q_gen_6742
<nil, cons>(q_gen_6751, q_gen_6750) -> q_gen_6742
<nil, nil>() -> q_gen_6742
<a, a>() -> q_gen_6745
<b, b>() -> q_gen_6745
}

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, _nka])) -> prefix([l2, _nka]) -> 6
(append([t1, l2, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]) -> 13
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 9
(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, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]), {
_ika -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.016130 s (model generation: 0.015491,  model checking: 0.000639):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6747, q_gen_6748, q_gen_6763, q_gen_6764, q_gen_6765},
Q_f={q_gen_6743},
Delta=
{
<nil>() -> q_gen_6763
<b>() -> q_gen_6764
<cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6747
<nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6747
<nil, nil>() -> q_gen_6747
<a, a>() -> q_gen_6748
<b, b>() -> q_gen_6748
<cons, cons, cons>(q_gen_6765, q_gen_6743) -> q_gen_6743
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6743
<nil, nil, nil>() -> q_gen_6743
<a, b, a>() -> q_gen_6765
<b, b, b>() -> q_gen_6765
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_6742, q_gen_6745, q_gen_6750, q_gen_6751},
Q_f={q_gen_6742},
Delta=
{
<cons>(q_gen_6751, q_gen_6750) -> q_gen_6750
<nil>() -> q_gen_6750
<a>() -> q_gen_6751
<b>() -> q_gen_6751
<cons, cons>(q_gen_6745, q_gen_6742) -> q_gen_6742
<nil, cons>(q_gen_6751, q_gen_6750) -> q_gen_6742
<nil, nil>() -> q_gen_6742
<a, a>() -> q_gen_6745
<b, b>() -> q_gen_6745
}

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

-------------------------------------------
Step 12, which took 0.017599 s (model generation: 0.016370,  model checking: 0.001229):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6747, q_gen_6748, q_gen_6763, q_gen_6764, q_gen_6765},
Q_f={q_gen_6743},
Delta=
{
<nil>() -> q_gen_6763
<b>() -> q_gen_6764
<cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6747
<nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6747
<nil, nil>() -> q_gen_6747
<a, a>() -> q_gen_6748
<b, b>() -> q_gen_6748
<cons, cons, cons>(q_gen_6765, q_gen_6743) -> q_gen_6743
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6743
<nil, nil, nil>() -> q_gen_6743
<a, b, a>() -> q_gen_6765
<b, b, b>() -> q_gen_6765
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_6742, q_gen_6745, q_gen_6750, q_gen_6751},
Q_f={q_gen_6742},
Delta=
{
<cons>(q_gen_6751, q_gen_6750) -> q_gen_6750
<nil>() -> q_gen_6750
<a>() -> q_gen_6751
<b>() -> q_gen_6751
<cons, cons>(q_gen_6745, q_gen_6742) -> q_gen_6742
<nil, cons>(q_gen_6751, q_gen_6750) -> q_gen_6742
<nil, nil>() -> q_gen_6742
<a, a>() -> q_gen_6745
<b, a>() -> q_gen_6745
<b, b>() -> q_gen_6745
}

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, _nka])) -> prefix([l2, _nka]) -> 9
(append([t1, l2, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]) -> 13
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 9
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 7
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 10
(prefix([cons(z, zs), nil])) -> BOT -> 8
}
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 13, which took 0.023629 s (model generation: 0.016441,  model checking: 0.007188):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6747, q_gen_6748, q_gen_6762, q_gen_6763, q_gen_6764, q_gen_6765},
Q_f={q_gen_6743},
Delta=
{
<nil>() -> q_gen_6763
<b>() -> q_gen_6764
<cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6747
<nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6747
<nil, nil>() -> q_gen_6747
<a, a>() -> q_gen_6748
<b, b>() -> q_gen_6748
<cons, cons, cons>(q_gen_6765, q_gen_6762) -> q_gen_6743
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, nil, nil>() -> q_gen_6743
<cons, cons, cons>(q_gen_6765, q_gen_6743) -> q_gen_6762
<nil, nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6762
<a, b, a>() -> q_gen_6765
<b, b, b>() -> q_gen_6765
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_6742, q_gen_6745, q_gen_6750, q_gen_6751, q_gen_6771, q_gen_6772},
Q_f={q_gen_6742},
Delta=
{
<cons>(q_gen_6751, q_gen_6750) -> q_gen_6750
<nil>() -> q_gen_6750
<a>() -> q_gen_6751
<b>() -> q_gen_6751
<cons, cons>(q_gen_6745, q_gen_6742) -> q_gen_6742
<nil, cons>(q_gen_6751, q_gen_6750) -> q_gen_6742
<nil, nil>() -> q_gen_6742
<a, a>() -> q_gen_6745
<b, b>() -> q_gen_6745
<cons, cons>(q_gen_6772, q_gen_6742) -> q_gen_6771
<b, a>() -> q_gen_6772
}

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, _nka])) -> prefix([l2, _nka]) -> 12
(append([t1, l2, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]) -> 13
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 10
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 8
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 10
(prefix([cons(z, zs), nil])) -> BOT -> 9
}
Sat witness: Found: ((append([l1, l2, _nka])) -> prefix([l2, _nka]), {
_nka -> cons(a, cons(b, nil))  ;  l1 -> cons(a, nil)  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 14, which took 0.024926 s (model generation: 0.017045,  model checking: 0.007881):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6747, q_gen_6748, q_gen_6762, q_gen_6763, q_gen_6764, q_gen_6765},
Q_f={q_gen_6743},
Delta=
{
<nil>() -> q_gen_6763
<b>() -> q_gen_6764
<cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6747
<nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6747
<nil, nil>() -> q_gen_6747
<a, a>() -> q_gen_6748
<b, b>() -> q_gen_6748
<cons, cons, cons>(q_gen_6765, q_gen_6762) -> q_gen_6743
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, nil, nil>() -> q_gen_6743
<cons, cons, cons>(q_gen_6765, q_gen_6743) -> q_gen_6762
<nil, nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6762
<a, b, a>() -> q_gen_6765
<b, b, b>() -> q_gen_6765
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_6742, q_gen_6744, q_gen_6745, q_gen_6750, q_gen_6751, q_gen_6771, q_gen_6772},
Q_f={q_gen_6742, q_gen_6744},
Delta=
{
<cons>(q_gen_6751, q_gen_6750) -> q_gen_6750
<nil>() -> q_gen_6750
<a>() -> q_gen_6751
<b>() -> q_gen_6751
<cons, cons>(q_gen_6772, q_gen_6744) -> q_gen_6742
<nil, nil>() -> q_gen_6742
<cons, cons>(q_gen_6745, q_gen_6742) -> q_gen_6744
<nil, cons>(q_gen_6751, q_gen_6750) -> q_gen_6744
<a, a>() -> q_gen_6745
<b, b>() -> q_gen_6745
<cons, cons>(q_gen_6772, q_gen_6742) -> q_gen_6771
<b, a>() -> q_gen_6772
}

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

-------------------------------------------
Step 15, which took 0.026956 s (model generation: 0.017621,  model checking: 0.009335):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6747, q_gen_6748, q_gen_6762, q_gen_6763, q_gen_6764, q_gen_6765},
Q_f={q_gen_6743},
Delta=
{
<nil>() -> q_gen_6763
<b>() -> q_gen_6764
<cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6747
<nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6747
<nil, nil>() -> q_gen_6747
<a, a>() -> q_gen_6748
<b, b>() -> q_gen_6748
<cons, cons, cons>(q_gen_6765, q_gen_6762) -> q_gen_6743
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, nil, nil>() -> q_gen_6743
<cons, cons, cons>(q_gen_6765, q_gen_6743) -> q_gen_6762
<nil, nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6762
<a, b, a>() -> q_gen_6765
<b, b, b>() -> q_gen_6765
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_6742, q_gen_6745, q_gen_6749, q_gen_6750, q_gen_6751, q_gen_6771, q_gen_6772},
Q_f={q_gen_6742, q_gen_6749},
Delta=
{
<cons>(q_gen_6751, q_gen_6750) -> q_gen_6750
<nil>() -> q_gen_6750
<a>() -> q_gen_6751
<b>() -> q_gen_6751
<cons, cons>(q_gen_6745, q_gen_6742) -> q_gen_6742
<cons, cons>(q_gen_6772, q_gen_6749) -> q_gen_6742
<nil, nil>() -> q_gen_6742
<a, a>() -> q_gen_6745
<b, b>() -> q_gen_6745
<nil, cons>(q_gen_6751, q_gen_6750) -> q_gen_6749
<cons, cons>(q_gen_6772, q_gen_6742) -> q_gen_6771
<b, a>() -> q_gen_6772
}

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

-------------------------------------------
Step 16, which took 0.032276 s (model generation: 0.019211,  model checking: 0.013065):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6747, q_gen_6748, q_gen_6762, q_gen_6763, q_gen_6764, q_gen_6765},
Q_f={q_gen_6743},
Delta=
{
<nil>() -> q_gen_6763
<b>() -> q_gen_6764
<cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6747
<nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6747
<nil, nil>() -> q_gen_6747
<a, a>() -> q_gen_6748
<b, b>() -> q_gen_6748
<cons, cons, cons>(q_gen_6765, q_gen_6762) -> q_gen_6743
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, nil, nil>() -> q_gen_6743
<cons, cons, cons>(q_gen_6765, q_gen_6743) -> q_gen_6762
<nil, nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6762
<a, b, a>() -> q_gen_6765
<b, b, b>() -> q_gen_6765
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_6742, q_gen_6745, q_gen_6749, q_gen_6750, q_gen_6751, q_gen_6771, q_gen_6772},
Q_f={q_gen_6742, q_gen_6749},
Delta=
{
<cons>(q_gen_6751, q_gen_6750) -> q_gen_6750
<nil>() -> q_gen_6750
<a>() -> q_gen_6751
<b>() -> q_gen_6751
<cons, cons>(q_gen_6745, q_gen_6742) -> q_gen_6742
<cons, cons>(q_gen_6745, q_gen_6749) -> q_gen_6742
<nil, nil>() -> q_gen_6742
<a, a>() -> q_gen_6745
<b, b>() -> q_gen_6745
<cons, cons>(q_gen_6772, q_gen_6749) -> q_gen_6749
<nil, cons>(q_gen_6751, q_gen_6750) -> q_gen_6749
<cons, cons>(q_gen_6772, q_gen_6742) -> q_gen_6771
<b, a>() -> q_gen_6772
}

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, _nka])) -> prefix([l2, _nka]) -> 15
(append([t1, l2, _ika])) -> append([cons(h1, t1), l2, cons(h1, _ika)]) -> 13
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 13
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 11
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 13
(prefix([cons(z, zs), nil])) -> BOT -> 12
}
Sat witness: Found: ((append([l1, l2, _nka])) -> prefix([l2, _nka]), {
_nka -> cons(a, cons(b, nil))  ;  l1 -> cons(a, cons(b, nil))  ;  l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 17, which took 0.026986 s (model generation: 0.022698,  model checking: 0.004288):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6747, q_gen_6748, q_gen_6757, q_gen_6760, q_gen_6763, q_gen_6764, q_gen_6765},
Q_f={q_gen_6743},
Delta=
{
<nil>() -> q_gen_6763
<b>() -> q_gen_6764
<cons, cons>(q_gen_6757, q_gen_6747) -> q_gen_6747
<nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6747
<nil, nil>() -> q_gen_6747
<b, b>() -> q_gen_6748
<a, a>() -> q_gen_6757
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6743
<nil, cons, cons>(q_gen_6757, q_gen_6747) -> q_gen_6743
<nil, nil, nil>() -> q_gen_6743
<cons, cons, cons>(q_gen_6765, q_gen_6743) -> q_gen_6760
<cons, cons, cons>(q_gen_6765, q_gen_6760) -> q_gen_6760
<nil, cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6760
<nil, nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6760
<a, b, a>() -> q_gen_6765
<b, b, b>() -> q_gen_6765
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_6742, q_gen_6745, q_gen_6750, q_gen_6751, q_gen_6771, q_gen_6772},
Q_f={q_gen_6742},
Delta=
{
<cons>(q_gen_6751, q_gen_6750) -> q_gen_6750
<nil>() -> q_gen_6750
<a>() -> q_gen_6751
<b>() -> q_gen_6751
<cons, cons>(q_gen_6745, q_gen_6742) -> q_gen_6742
<nil, cons>(q_gen_6751, q_gen_6750) -> q_gen_6742
<nil, nil>() -> q_gen_6742
<a, a>() -> q_gen_6745
<b, b>() -> q_gen_6745
<cons, cons>(q_gen_6772, q_gen_6742) -> q_gen_6771
<b, a>() -> q_gen_6772
}

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

-------------------------------------------
Step 18, which took 0.032640 s (model generation: 0.021210,  model checking: 0.011430):

Model:
|_
{
append -> 
{{{
Q={q_gen_6743, q_gen_6746, q_gen_6747, q_gen_6748, q_gen_6763, q_gen_6764, q_gen_6765, q_gen_6770},
Q_f={q_gen_6743, q_gen_6746},
Delta=
{
<nil>() -> q_gen_6763
<b>() -> q_gen_6764
<cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6747
<nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6747
<nil, nil>() -> q_gen_6747
<a, a>() -> q_gen_6748
<b, b>() -> q_gen_6748
<nil, nil, nil>() -> q_gen_6743
<cons, cons, cons>(q_gen_6765, q_gen_6746) -> q_gen_6746
<cons, nil, cons>(q_gen_6748, q_gen_6747) -> q_gen_6746
<nil, cons, cons>(q_gen_6748, q_gen_6747) -> q_gen_6746
<nil, nil, cons>(q_gen_6764, q_gen_6763) -> q_gen_6746
<a, b, a>() -> q_gen_6765
<b, b, b>() -> q_gen_6765
<cons, cons, cons>(q_gen_6765, q_gen_6743) -> q_gen_6770
<cons, cons, cons>(q_gen_6765, q_gen_6770) -> q_gen_6770
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  prefix -> 
{{{
Q={q_gen_6742, q_gen_6745, q_gen_6749, q_gen_6750, q_gen_6751, q_gen_6771, q_gen_6772},
Q_f={q_gen_6742, q_gen_6749},
Delta=
{
<cons>(q_gen_6751, q_gen_6750) -> q_gen_6750
<nil>() -> q_gen_6750
<a>() -> q_gen_6751
<b>() -> q_gen_6751
<cons, cons>(q_gen_6745, q_gen_6742) -> q_gen_6742
<nil, nil>() -> q_gen_6742
<a, a>() -> q_gen_6745
<b, b>() -> q_gen_6745
<cons, cons>(q_gen_6745, q_gen_6749) -> q_gen_6749
<cons, cons>(q_gen_6772, q_gen_6749) -> q_gen_6749
<nil, cons>(q_gen_6751, q_gen_6750) -> q_gen_6749
<cons, cons>(q_gen_6772, q_gen_6742) -> q_gen_6771
<b, a>() -> q_gen_6772
}

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

Total time: 0.378617
Reason for stopping: Disproved