Solving ../../benchmarks/true/isaplanner_prop26.smt2...

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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(elem, P:
{() -> elem([h1, cons(h1, t1)])
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)])
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1])
(elem([e, nil])) -> BOT}
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)])}
(append([_t, _u, _v]) /\ append([_t, _u, _w])) -> eq_eltlist([_v, _w])
)
}

properties:
{(append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0  ;  () -> elem([h1, cons(h1, t1)]) -> 0  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 0  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 0  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 0  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 0  ;  (elem([e, nil])) -> BOT -> 0
}


Solving took 38.780964 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1630, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1638, q_gen_1639, q_gen_1640, q_gen_1641, q_gen_1644, q_gen_1645, q_gen_1646, q_gen_1647, q_gen_1648, q_gen_1649, q_gen_1650, q_gen_1652, q_gen_1653, q_gen_1654, q_gen_1655, q_gen_1656, q_gen_1659, q_gen_1660, q_gen_1661, q_gen_1664, q_gen_1665, q_gen_1666, q_gen_1667, q_gen_1668, q_gen_1669, q_gen_1670, q_gen_1671, q_gen_1672, q_gen_1675, q_gen_1676, q_gen_1677, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684, q_gen_1685, q_gen_1686, q_gen_1687, q_gen_1688, q_gen_1689, q_gen_1695, q_gen_1696, q_gen_1697, q_gen_1698, q_gen_1699, q_gen_1700, q_gen_1701, q_gen_1706, q_gen_1707, q_gen_1708, q_gen_1709, q_gen_1710, q_gen_1711, q_gen_1712, q_gen_1713, q_gen_1714, q_gen_1720, q_gen_1721, q_gen_1722, q_gen_1723, q_gen_1724, q_gen_1725, q_gen_1726, q_gen_1727, q_gen_1728, q_gen_1729, q_gen_1730, q_gen_1736, q_gen_1737, q_gen_1738, q_gen_1739, q_gen_1740, q_gen_1741, q_gen_1742, q_gen_1743, q_gen_1744, q_gen_1745, q_gen_1750, q_gen_1751, q_gen_1752, q_gen_1753, q_gen_1754, q_gen_1755, q_gen_1756, q_gen_1757, q_gen_1758, q_gen_1759, q_gen_1760, q_gen_1762, q_gen_1763, q_gen_1764, q_gen_1767, q_gen_1768, q_gen_1769, q_gen_1770, q_gen_1771, q_gen_1772},
Q_f={},
Delta=
{
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1655
<cons>(q_gen_1655, q_gen_1648) -> q_gen_1668
<cons>(q_gen_1655, q_gen_1668) -> q_gen_1671
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1700
<cons>(q_gen_1649, q_gen_1668) -> q_gen_1729
<nil, nil>() -> q_gen_1631
<nil, b>() -> q_gen_1632
<b, nil>() -> q_gen_1633
<b, b>() -> q_gen_1634
<nil, a>() -> q_gen_1639
<a, nil>() -> q_gen_1640
<a, a>() -> q_gen_1641
<cons, cons>(q_gen_1641, q_gen_1640, q_gen_1639, q_gen_1631) -> q_gen_1646
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1647
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1650
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1653
<cons, b>(q_gen_1655, q_gen_1648) -> q_gen_1654
<b, cons>(q_gen_1655, q_gen_1648) -> q_gen_1656
<cons, a>(q_gen_1655, q_gen_1648) -> q_gen_1660
<a, cons>(q_gen_1655, q_gen_1648) -> q_gen_1661
<cons, cons>(q_gen_1634, q_gen_1669, q_gen_1667, q_gen_1666) -> q_gen_1665
<cons, cons>(q_gen_1634, q_gen_1656, q_gen_1654, q_gen_1653) -> q_gen_1666
<cons, b>(q_gen_1655, q_gen_1668) -> q_gen_1667
<b, cons>(q_gen_1655, q_gen_1668) -> q_gen_1669
<cons, b>(q_gen_1655, q_gen_1671) -> q_gen_1670
<b, cons>(q_gen_1655, q_gen_1671) -> q_gen_1672
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1697
<nil, cons>(q_gen_1655, q_gen_1700) -> q_gen_1699
<b, cons>(q_gen_1655, q_gen_1700) -> q_gen_1701
<nil, cons>(q_gen_1649, q_gen_1700) -> q_gen_1713
<b, cons>(q_gen_1649, q_gen_1700) -> q_gen_1714
<nil, cons>(q_gen_1655, q_gen_1729) -> q_gen_1728
<b, cons>(q_gen_1655, q_gen_1729) -> q_gen_1730
<cons, cons>(q_gen_1634, q_gen_1744, q_gen_1632, q_gen_1743) -> q_gen_1742
<nil, cons>(q_gen_1649, q_gen_1668) -> q_gen_1743
<b, cons>(q_gen_1649, q_gen_1668) -> q_gen_1744
<a, cons>(q_gen_1655, q_gen_1729) -> q_gen_1745
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1753
<a, b>() -> q_gen_1754
<cons, cons>(q_gen_1634, q_gen_1650, q_gen_1632, q_gen_1697) -> q_gen_1763
<a, cons>(q_gen_1655, q_gen_1700) -> q_gen_1764
<nil, cons>(q_gen_1655, q_gen_1648) -> q_gen_1769
<nil, nil, nil>() -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1630
<nil, cons, cons>(q_gen_1641, q_gen_1640, q_gen_1639, q_gen_1631) -> q_gen_1638
<cons, nil, cons>(q_gen_1641, q_gen_1640, q_gen_1639, q_gen_1631) -> q_gen_1644
<cons, nil, cons>(q_gen_1634, q_gen_1650, q_gen_1647, q_gen_1646) -> q_gen_1645
<nil, cons, cons>(q_gen_1634, q_gen_1656, q_gen_1654, q_gen_1653) -> q_gen_1652
<cons, nil, cons>(q_gen_1641, q_gen_1661, q_gen_1660, q_gen_1653) -> q_gen_1659
<nil, cons, cons>(q_gen_1634, q_gen_1672, q_gen_1670, q_gen_1665) -> q_gen_1664
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1675
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1677) -> q_gen_1676
<nil, nil, cons>(q_gen_1655, q_gen_1648) -> q_gen_1677
<nil, nil, b>() -> q_gen_1678
<nil, b, cons>(q_gen_1655, q_gen_1648) -> q_gen_1679
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1655, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, b, cons>(q_gen_1655, q_gen_1648) -> q_gen_1683
<b, b, b>() -> q_gen_1684
<cons, cons, cons>(q_gen_1684, q_gen_1689, q_gen_1682, q_gen_1688, q_gen_1680, q_gen_1687, q_gen_1678, q_gen_1686) -> q_gen_1685
<nil, nil, cons>(q_gen_1655, q_gen_1668) -> q_gen_1686
<nil, b, cons>(q_gen_1655, q_gen_1668) -> q_gen_1687
<b, nil, cons>(q_gen_1655, q_gen_1668) -> q_gen_1688
<b, b, cons>(q_gen_1655, q_gen_1668) -> q_gen_1689
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1695
<cons, nil, cons>(q_gen_1634, q_gen_1650, q_gen_1632, q_gen_1697) -> q_gen_1696
<cons, nil, cons>(q_gen_1634, q_gen_1701, q_gen_1632, q_gen_1699) -> q_gen_1698
<cons, cons, cons>(q_gen_1711, q_gen_1710, q_gen_1682, q_gen_1709, q_gen_1708, q_gen_1707, q_gen_1678, q_gen_1695) -> q_gen_1706
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1707
<nil, a, b>() -> q_gen_1708
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1709
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1710
<b, a, b>() -> q_gen_1711
<cons, nil, cons>(q_gen_1634, q_gen_1714, q_gen_1632, q_gen_1713) -> q_gen_1712
<cons, cons, cons>(q_gen_1726, q_gen_1725, q_gen_1724, q_gen_1723, q_gen_1722, q_gen_1679, q_gen_1721, q_gen_1677) -> q_gen_1720
<nil, nil, a>() -> q_gen_1721
<nil, b, a>() -> q_gen_1722
<a, nil, cons>(q_gen_1655, q_gen_1648) -> q_gen_1723
<a, nil, a>() -> q_gen_1724
<a, b, cons>(q_gen_1655, q_gen_1648) -> q_gen_1725
<a, b, a>() -> q_gen_1726
<cons, nil, cons>(q_gen_1634, q_gen_1730, q_gen_1632, q_gen_1728) -> q_gen_1727
<cons, cons, cons>(q_gen_1740, q_gen_1739, q_gen_1724, q_gen_1738, q_gen_1737, q_gen_1707, q_gen_1721, q_gen_1695) -> q_gen_1736
<nil, a, a>() -> q_gen_1737
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1738
<a, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1739
<a, a, a>() -> q_gen_1740
<cons, nil, cons>(q_gen_1641, q_gen_1745, q_gen_1660, q_gen_1742) -> q_gen_1741
<nil, cons, cons>(q_gen_1634, q_gen_1650, q_gen_1647, q_gen_1646) -> q_gen_1750
<cons, cons, cons>(q_gen_1684, q_gen_1759, q_gen_1758, q_gen_1757, q_gen_1680, q_gen_1756, q_gen_1755, q_gen_1752) -> q_gen_1751
<nil, cons, cons>(q_gen_1754, q_gen_1753, q_gen_1632, q_gen_1697) -> q_gen_1752
<nil, cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1755
<nil, b, cons>(q_gen_1655, q_gen_1700) -> q_gen_1756
<b, cons, cons>(q_gen_1754, q_gen_1753, q_gen_1632, q_gen_1697) -> q_gen_1757
<b, cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1758
<b, b, cons>(q_gen_1655, q_gen_1700) -> q_gen_1759
<cons, nil, cons>(q_gen_1754, q_gen_1640, q_gen_1632, q_gen_1631) -> q_gen_1760
<cons, nil, cons>(q_gen_1641, q_gen_1764, q_gen_1660, q_gen_1763) -> q_gen_1762
<cons, cons, cons>(q_gen_1684, q_gen_1689, q_gen_1772, q_gen_1771, q_gen_1680, q_gen_1687, q_gen_1770, q_gen_1768) -> q_gen_1767
<nil, cons, cons>(q_gen_1634, q_gen_1656, q_gen_1632, q_gen_1769) -> q_gen_1768
<nil, cons, b>(q_gen_1655, q_gen_1648) -> q_gen_1770
<b, cons, cons>(q_gen_1634, q_gen_1656, q_gen_1632, q_gen_1769) -> q_gen_1771
<b, cons, b>(q_gen_1655, q_gen_1648) -> q_gen_1772
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1627, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1636, q_gen_1637, q_gen_1642, q_gen_1643, q_gen_1651, q_gen_1657, q_gen_1658, q_gen_1662, q_gen_1663, q_gen_1673, q_gen_1674, q_gen_1690, q_gen_1691, q_gen_1692, q_gen_1693, q_gen_1694, q_gen_1702, q_gen_1703, q_gen_1704, q_gen_1705, q_gen_1715, q_gen_1716, q_gen_1717, q_gen_1718, q_gen_1719, q_gen_1731, q_gen_1732, q_gen_1733, q_gen_1734, q_gen_1735, q_gen_1746, q_gen_1747, q_gen_1748, q_gen_1749, q_gen_1761, q_gen_1765, q_gen_1766},
Q_f={},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1691
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1703
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1716
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1732
<cons>(q_gen_1629, q_gen_1643) -> q_gen_1748
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1627
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1636
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1637
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1642
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1651
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1657
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1662
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1663
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1673
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1674
<b, cons>(q_gen_1625, q_gen_1691) -> q_gen_1690
<a, nil>() -> q_gen_1692
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1693
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1694
<b, cons>(q_gen_1625, q_gen_1703) -> q_gen_1702
<a, cons>(q_gen_1629, q_gen_1691) -> q_gen_1704
<b, cons>(q_gen_1629, q_gen_1691) -> q_gen_1705
<b, cons>(q_gen_1625, q_gen_1716) -> q_gen_1715
<b, cons>(q_gen_1629, q_gen_1716) -> q_gen_1717
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1718
<a, cons>(q_gen_1625, q_gen_1703) -> q_gen_1719
<b, cons>(q_gen_1625, q_gen_1732) -> q_gen_1731
<a, cons>(q_gen_1625, q_gen_1691) -> q_gen_1733
<a, cons>(q_gen_1629, q_gen_1643) -> q_gen_1734
<a, cons>(q_gen_1625, q_gen_1716) -> q_gen_1735
<b, cons>(q_gen_1629, q_gen_1732) -> q_gen_1746
<b, cons>(q_gen_1625, q_gen_1748) -> q_gen_1747
<b, cons>(q_gen_1629, q_gen_1748) -> q_gen_1749
<a, cons>(q_gen_1625, q_gen_1732) -> q_gen_1761
<b, cons>(q_gen_1629, q_gen_1703) -> q_gen_1765
<a, cons>(q_gen_1625, q_gen_1748) -> q_gen_1766
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.011473 s (model generation: 0.010058,  model checking: 0.001415):

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> elem([h1, cons(h1, t1)]) -> 3  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 1  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 1  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 1  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 1  ;  (elem([e, nil])) -> BOT -> 1
}
Sat witness: Yes: (() -> elem([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 1, which took 0.011260 s (model generation: 0.010373,  model checking: 0.000887):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> elem([h1, cons(h1, t1)]) -> 3  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 1  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 1  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 1  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 1  ;  (elem([e, nil])) -> BOT -> 1
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.011478 s (model generation: 0.010522,  model checking: 0.000956):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> elem([h1, cons(h1, t1)]) -> 3  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 1  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 1  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 4  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 2  ;  (elem([e, nil])) -> BOT -> 2
}
Sat witness: Yes: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 3, which took 0.012607 s (model generation: 0.011356,  model checking: 0.001251):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1624
<nil>() -> q_gen_1624
<a>() -> q_gen_1625
<b>() -> q_gen_1625
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> elem([h1, cons(h1, t1)]) -> 3  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 1  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 4  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 4  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 2  ;  (elem([e, nil])) -> BOT -> 2
}
Sat witness: Yes: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.012603 s (model generation: 0.012277,  model checking: 0.000326):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634},
Q_f={q_gen_1626},
Delta=
{
<nil, nil>() -> q_gen_1631
<nil, b>() -> q_gen_1632
<b, nil>() -> q_gen_1633
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1624
<nil>() -> q_gen_1624
<a>() -> q_gen_1625
<b>() -> q_gen_1625
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> elem([h1, cons(h1, t1)]) -> 3  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 2  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 4  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 4  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 5  ;  (elem([e, nil])) -> BOT -> 3
}
Sat witness: Yes: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> b  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.013158 s (model generation: 0.013005,  model checking: 0.000153):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634},
Q_f={q_gen_1626},
Delta=
{
<nil, nil>() -> q_gen_1631
<nil, b>() -> q_gen_1632
<b, nil>() -> q_gen_1633
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1624
<nil>() -> q_gen_1624
<a>() -> q_gen_1625
<b>() -> q_gen_1625
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, nil>() -> q_gen_1623
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> elem([h1, cons(h1, t1)]) -> 3  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 3  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 4  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 4  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 5  ;  (elem([e, nil])) -> BOT -> 6
}
Sat witness: Yes: ((elem([e, nil])) -> BOT, {
e -> b
})

-------------------------------------------
Step 6, which took 0.014272 s (model generation: 0.012473,  model checking: 0.001799):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634},
Q_f={q_gen_1626},
Delta=
{
<nil, nil>() -> q_gen_1631
<nil, b>() -> q_gen_1632
<b, nil>() -> q_gen_1633
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<a>() -> q_gen_1629
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> elem([h1, cons(h1, t1)]) -> 6  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 4  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 4  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 4  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 5  ;  (elem([e, nil])) -> BOT -> 6
}
Sat witness: Yes: (() -> elem([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.015933 s (model generation: 0.012523,  model checking: 0.003410):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634},
Q_f={q_gen_1626},
Delta=
{
<nil, nil>() -> q_gen_1631
<nil, b>() -> q_gen_1632
<b, nil>() -> q_gen_1633
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> elem([h1, cons(h1, t1)]) -> 6  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 4  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 4  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 4  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 5  ;  (elem([e, nil])) -> BOT -> 6
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 8, which took 0.014229 s (model generation: 0.013159,  model checking: 0.001070):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634},
Q_f={q_gen_1626},
Delta=
{
<nil, nil>() -> q_gen_1631
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, nil>() -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> elem([h1, cons(h1, t1)]) -> 6  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 4  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 4  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 7  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 5  ;  (elem([e, nil])) -> BOT -> 6
}
Sat witness: Yes: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 9, which took 0.024726 s (model generation: 0.013756,  model checking: 0.010970):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634},
Q_f={q_gen_1626},
Delta=
{
<nil, nil>() -> q_gen_1631
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, nil>() -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> elem([h1, cons(h1, t1)]) -> 6  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 4  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 7  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 7  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 5  ;  (elem([e, nil])) -> BOT -> 6
}
Sat witness: Yes: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 10, which took 0.018268 s (model generation: 0.014918,  model checking: 0.003350):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649},
Q_f={q_gen_1626},
Delta=
{
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> elem([h1, cons(h1, t1)]) -> 9  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 5  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 7  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 7  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 6  ;  (elem([e, nil])) -> BOT -> 7
}
Sat witness: Yes: (() -> elem([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 11, which took 0.038663 s (model generation: 0.015963,  model checking: 0.022700):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649},
Q_f={q_gen_1626},
Delta=
{
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> elem([h1, cons(h1, t1)]) -> 9  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 6  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 7  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 7  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 7  ;  (elem([e, nil])) -> BOT -> 7
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 12, which took 0.007215 s (model generation: 0.005612,  model checking: 0.001603):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649},
Q_f={q_gen_1626},
Delta=
{
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> elem([h1, cons(h1, t1)]) -> 9  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 7  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 7  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 10  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 8  ;  (elem([e, nil])) -> BOT -> 8
}
Sat witness: Yes: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 13, which took 0.012908 s (model generation: 0.006278,  model checking: 0.006630):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649},
Q_f={q_gen_1626},
Delta=
{
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> elem([h1, cons(h1, t1)]) -> 9  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 7  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 10  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 10  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 8  ;  (elem([e, nil])) -> BOT -> 8
}
Sat witness: Yes: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> cons(b, nil)  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 14, which took 0.008574 s (model generation: 0.006585,  model checking: 0.001989):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649},
Q_f={q_gen_1626},
Delta=
{
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> elem([h1, cons(h1, t1)]) -> 9  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 8  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 10  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 10  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 11  ;  (elem([e, nil])) -> BOT -> 9
}
Sat witness: Yes: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 15, which took 0.014545 s (model generation: 0.010449,  model checking: 0.004096):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649},
Q_f={q_gen_1626},
Delta=
{
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1624
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> elem([h1, cons(h1, t1)]) -> 12  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 9  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 10  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 10  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 11  ;  (elem([e, nil])) -> BOT -> 10
}
Sat witness: Yes: (() -> elem([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 16, which took 0.036742 s (model generation: 0.017250,  model checking: 0.019492):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649},
Q_f={q_gen_1626},
Delta=
{
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1624
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> elem([h1, cons(h1, t1)]) -> 12  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 10  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 10  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 10  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 11  ;  (elem([e, nil])) -> BOT -> 10
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, cons(b, nil))))
})

-------------------------------------------
Step 17, which took 0.009754 s (model generation: 0.008746,  model checking: 0.001008):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1624
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> elem([h1, cons(h1, t1)]) -> 12  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 10  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 10  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 13  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 11  ;  (elem([e, nil])) -> BOT -> 11
}
Sat witness: Yes: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 18, which took 0.017039 s (model generation: 0.012685,  model checking: 0.004354):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1624
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> elem([h1, cons(h1, t1)]) -> 12  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 10  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 13  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 13  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 11  ;  (elem([e, nil])) -> BOT -> 11
}
Sat witness: Yes: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.029797 s (model generation: 0.022148,  model checking: 0.007649):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1624
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> elem([h1, cons(h1, t1)]) -> 12  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 13  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 13  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 13  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 11  ;  (elem([e, nil])) -> BOT -> 11
}
Sat witness: Yes: ((append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]), {
_x -> cons(b, cons(b, cons(b, nil)))  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 20, which took 0.025942 s (model generation: 0.025573,  model checking: 0.000369):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1624
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> elem([h1, cons(h1, t1)]) -> 12  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 13  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 13  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 13  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 14  ;  (elem([e, nil])) -> BOT -> 12
}
Sat witness: Yes: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> a  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 0.021250 s (model generation: 0.021232,  model checking: 0.000018):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1624
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, nil>() -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> elem([h1, cons(h1, t1)]) -> 12  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 13  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 13  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 13  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 14  ;  (elem([e, nil])) -> BOT -> 15
}
Sat witness: Yes: ((elem([e, nil])) -> BOT, {
e -> a
})

-------------------------------------------
Step 22, which took 0.016186 s (model generation: 0.015919,  model checking: 0.000267):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> elem([h1, cons(h1, t1)]) -> 15  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 13  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 13  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 13  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 14  ;  (elem([e, nil])) -> BOT -> 15
}
Sat witness: Yes: (() -> elem([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 23, which took 0.017268 s (model generation: 0.013834,  model checking: 0.003434):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> elem([h1, cons(h1, t1)]) -> 15  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 13  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 13  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 16  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 14  ;  (elem([e, nil])) -> BOT -> 15
}
Sat witness: Yes: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 24, which took 0.046392 s (model generation: 0.017291,  model checking: 0.029101):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> elem([h1, cons(h1, t1)]) -> 15  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 13  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 16  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 16  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 14  ;  (elem([e, nil])) -> BOT -> 15
}
Sat witness: Yes: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 25, which took 0.015869 s (model generation: 0.013645,  model checking: 0.002224):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> elem([h1, cons(h1, t1)]) -> 15  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 16  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 16  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 16  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 14  ;  (elem([e, nil])) -> BOT -> 15
}
Sat witness: Yes: ((append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]), {
_x -> cons(b, cons(b, cons(a, nil)))  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 26, which took 0.018732 s (model generation: 0.016183,  model checking: 0.002549):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14  ;  () -> elem([h1, cons(h1, t1)]) -> 15  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 16  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 16  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 16  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 17  ;  (elem([e, nil])) -> BOT -> 15
}
Sat witness: Yes: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 27, which took 0.026132 s (model generation: 0.023510,  model checking: 0.002622):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  () -> elem([h1, cons(h1, t1)]) -> 18  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 16  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 16  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 16  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 17  ;  (elem([e, nil])) -> BOT -> 16
}
Sat witness: Yes: (() -> elem([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 28, which took 0.025961 s (model generation: 0.022787,  model checking: 0.003174):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> elem([h1, cons(h1, t1)]) -> 18  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 16  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 16  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 19  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 17  ;  (elem([e, nil])) -> BOT -> 17
}
Sat witness: Yes: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 29, which took 0.084354 s (model generation: 0.021120,  model checking: 0.063234):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> elem([h1, cons(h1, t1)]) -> 18  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 16  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 19  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 19  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 17  ;  (elem([e, nil])) -> BOT -> 17
}
Sat witness: Yes: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 30, which took 0.021208 s (model generation: 0.017399,  model checking: 0.003809):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, b>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> elem([h1, cons(h1, t1)]) -> 18  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 19  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 19  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 19  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 17  ;  (elem([e, nil])) -> BOT -> 17
}
Sat witness: Yes: ((append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]), {
_x -> cons(b, cons(a, cons(a, nil)))  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 31, which took 0.023208 s (model generation: 0.020099,  model checking: 0.003109):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, b>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17  ;  () -> elem([h1, cons(h1, t1)]) -> 18  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 19  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 19  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 19  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 20  ;  (elem([e, nil])) -> BOT -> 18
}
Sat witness: Yes: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 32, which took 0.024601 s (model generation: 0.022038,  model checking: 0.002563):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, b>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1624
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18  ;  () -> elem([h1, cons(h1, t1)]) -> 21  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 19  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 19  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 19  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 20  ;  (elem([e, nil])) -> BOT -> 19
}
Sat witness: Yes: (() -> elem([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 33, which took 0.027332 s (model generation: 0.024221,  model checking: 0.003111):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, b>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19  ;  () -> elem([h1, cons(h1, t1)]) -> 21  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 19  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 19  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 22  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 20  ;  (elem([e, nil])) -> BOT -> 20
}
Sat witness: Yes: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 34, which took 0.212707 s (model generation: 0.024993,  model checking: 0.187714):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, b>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, b>() -> q_gen_1682
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19  ;  () -> elem([h1, cons(h1, t1)]) -> 21  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 19  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 22  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 22  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 20  ;  (elem([e, nil])) -> BOT -> 20
}
Sat witness: Yes: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 35, which took 0.028159 s (model generation: 0.023345,  model checking: 0.004814):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19  ;  () -> elem([h1, cons(h1, t1)]) -> 21  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 22  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 22  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 22  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 20  ;  (elem([e, nil])) -> BOT -> 20
}
Sat witness: Yes: ((append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]), {
_x -> cons(b, cons(b, cons(a, cons(b, nil))))  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 36, which took 0.031061 s (model generation: 0.028065,  model checking: 0.002996):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20  ;  () -> elem([h1, cons(h1, t1)]) -> 21  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 22  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 22  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 22  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 23  ;  (elem([e, nil])) -> BOT -> 21
}
Sat witness: Yes: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 37, which took 0.033554 s (model generation: 0.031016,  model checking: 0.002538):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1624
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 21  ;  () -> elem([h1, cons(h1, t1)]) -> 24  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 22  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 22  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 22  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 23  ;  (elem([e, nil])) -> BOT -> 22
}
Sat witness: Yes: (() -> elem([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 38, which took 0.035201 s (model generation: 0.031712,  model checking: 0.003489):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1624
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22  ;  () -> elem([h1, cons(h1, t1)]) -> 24  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 22  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 22  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 25  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 23  ;  (elem([e, nil])) -> BOT -> 23
}
Sat witness: Yes: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 39, which took 0.084109 s (model generation: 0.032631,  model checking: 0.051478):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1624
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22  ;  () -> elem([h1, cons(h1, t1)]) -> 24  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 22  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 25  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 25  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 23  ;  (elem([e, nil])) -> BOT -> 23
}
Sat witness: Yes: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 40, which took 0.038323 s (model generation: 0.034669,  model checking: 0.003654):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, a>() -> q_gen_1680
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, a, a>() -> q_gen_1684
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1624
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22  ;  () -> elem([h1, cons(h1, t1)]) -> 24  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 25  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 25  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 25  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 23  ;  (elem([e, nil])) -> BOT -> 23
}
Sat witness: Yes: ((append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]), {
_x -> cons(a, cons(b, cons(a, cons(b, nil))))  ;  i -> b  ;  l1 -> cons(a, cons(b, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 41, which took 0.043637 s (model generation: 0.038776,  model checking: 0.004861):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, a>() -> q_gen_1680
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, a, a>() -> q_gen_1684
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1643
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23  ;  () -> elem([h1, cons(h1, t1)]) -> 27  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 25  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 25  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 25  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 24  ;  (elem([e, nil])) -> BOT -> 24
}
Sat witness: Yes: (() -> elem([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(a, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 42, which took 0.044968 s (model generation: 0.039352,  model checking: 0.005616):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, a>() -> q_gen_1680
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, a, a>() -> q_gen_1684
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1643
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1643) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24  ;  () -> elem([h1, cons(h1, t1)]) -> 27  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 25  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 25  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 28  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 25  ;  (elem([e, nil])) -> BOT -> 25
}
Sat witness: Yes: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(a, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 43, which took 1.840131 s (model generation: 0.043726,  model checking: 1.796405):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, a>() -> q_gen_1680
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, a, a>() -> q_gen_1684
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1643) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 25  ;  () -> elem([h1, cons(h1, t1)]) -> 27  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 25  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 28  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 28  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 26  ;  (elem([e, nil])) -> BOT -> 26
}
Sat witness: Yes: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 44, which took 0.047890 s (model generation: 0.046509,  model checking: 0.001381):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<a, b>() -> q_gen_1634
<b, b>() -> q_gen_1634
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<nil, cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1678
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, a>() -> q_gen_1680
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, a, a>() -> q_gen_1684
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1643) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 25  ;  () -> elem([h1, cons(h1, t1)]) -> 27  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 28  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 28  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 28  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 26  ;  (elem([e, nil])) -> BOT -> 26
}
Sat witness: Yes: ((append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]), {
_x -> cons(b, nil)  ;  i -> a  ;  l1 -> cons(a, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 45, which took 0.059061 s (model generation: 0.049465,  model checking: 0.009596):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1640, q_gen_1644, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<cons, cons>(q_gen_1634, q_gen_1640, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<a, b>() -> q_gen_1634
<b, b>() -> q_gen_1634
<a, nil>() -> q_gen_1640
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1644) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1640, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1640, q_gen_1632, q_gen_1631) -> q_gen_1644
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1644
<nil, cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1678
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, a>() -> q_gen_1680
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, a, a>() -> q_gen_1684
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1643) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26  ;  () -> elem([h1, cons(h1, t1)]) -> 28  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 28  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 28  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 31  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 27  ;  (elem([e, nil])) -> BOT -> 27
}
Sat witness: Yes: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 46, which took 0.060324 s (model generation: 0.050518,  model checking: 0.009806):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1640, q_gen_1644, q_gen_1648, q_gen_1649, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<cons, cons>(q_gen_1634, q_gen_1640, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<a, b>() -> q_gen_1634
<b, b>() -> q_gen_1634
<a, nil>() -> q_gen_1640
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1626) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1640, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1640, q_gen_1632, q_gen_1631) -> q_gen_1644
<nil, cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1678
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, a>() -> q_gen_1680
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, a, a>() -> q_gen_1684
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1643) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27  ;  () -> elem([h1, cons(h1, t1)]) -> 28  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 28  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 31  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 31  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 28  ;  (elem([e, nil])) -> BOT -> 28
}
Sat witness: Yes: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> nil  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 47, which took 0.061147 s (model generation: 0.049916,  model checking: 0.011231):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1677, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684, q_gen_1754},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<a, b>() -> q_gen_1754
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1677) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<cons, nil, cons>(q_gen_1754, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1677
<nil, cons, cons>(q_gen_1754, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1677
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1677
<nil, cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1678
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, a>() -> q_gen_1680
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, cons, cons>(q_gen_1754, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, a, a>() -> q_gen_1684
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1643) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 28  ;  () -> elem([h1, cons(h1, t1)]) -> 28  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 31  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 31  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 31  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 29  ;  (elem([e, nil])) -> BOT -> 29
}
Sat witness: Yes: ((append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]), {
_x -> cons(a, cons(b, cons(a, nil)))  ;  i -> b  ;  l1 -> cons(a, cons(b, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 48, which took 0.067142 s (model generation: 0.056648,  model checking: 0.010494):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1677, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684, q_gen_1754},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<a, b>() -> q_gen_1754
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1677) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<cons, nil, cons>(q_gen_1754, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1677
<nil, cons, cons>(q_gen_1754, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1677
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1677
<nil, cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1678
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, a>() -> q_gen_1680
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, cons, cons>(q_gen_1754, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, a, a>() -> q_gen_1684
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<cons>(q_gen_1629, q_gen_1643) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1643
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 29  ;  () -> elem([h1, cons(h1, t1)]) -> 29  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 31  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 31  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 34  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 30  ;  (elem([e, nil])) -> BOT -> 30
}
Sat witness: Yes: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(a, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 49, which took 6.321301 s (model generation: 0.056533,  model checking: 6.264768):

Model:
|_
{
append -> 
{{{
Q={q_gen_1626, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1648, q_gen_1649, q_gen_1677, q_gen_1678, q_gen_1679, q_gen_1680, q_gen_1681, q_gen_1682, q_gen_1683, q_gen_1684, q_gen_1754},
Q_f={q_gen_1626},
Delta=
{
<cons>(q_gen_1649, q_gen_1648) -> q_gen_1648
<nil>() -> q_gen_1648
<a>() -> q_gen_1649
<b>() -> q_gen_1649
<cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1631
<nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1631
<nil, nil>() -> q_gen_1631
<cons, a>(q_gen_1649, q_gen_1648) -> q_gen_1632
<cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1632
<nil, a>() -> q_gen_1632
<nil, b>() -> q_gen_1632
<a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<a, nil>() -> q_gen_1633
<b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1633
<b, nil>() -> q_gen_1633
<a, a>() -> q_gen_1634
<b, b>() -> q_gen_1634
<a, b>() -> q_gen_1754
<cons, cons, cons>(q_gen_1684, q_gen_1683, q_gen_1682, q_gen_1681, q_gen_1680, q_gen_1679, q_gen_1678, q_gen_1677) -> q_gen_1626
<cons, nil, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, cons, cons>(q_gen_1634, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1626
<nil, nil, nil>() -> q_gen_1626
<cons, nil, cons>(q_gen_1754, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1677
<nil, cons, cons>(q_gen_1754, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1677
<nil, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1677
<nil, cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1678
<nil, nil, a>() -> q_gen_1678
<nil, nil, b>() -> q_gen_1678
<nil, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1679
<nil, a, a>() -> q_gen_1680
<nil, a, b>() -> q_gen_1680
<nil, b, a>() -> q_gen_1680
<nil, b, b>() -> q_gen_1680
<a, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<b, cons, cons>(q_gen_1754, q_gen_1633, q_gen_1632, q_gen_1631) -> q_gen_1681
<b, nil, cons>(q_gen_1649, q_gen_1648) -> q_gen_1681
<a, nil, a>() -> q_gen_1682
<b, cons, b>(q_gen_1649, q_gen_1648) -> q_gen_1682
<b, nil, b>() -> q_gen_1682
<a, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, a, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<b, b, cons>(q_gen_1649, q_gen_1648) -> q_gen_1683
<a, a, a>() -> q_gen_1684
<a, b, a>() -> q_gen_1684
<b, a, b>() -> q_gen_1684
<b, b, b>() -> q_gen_1684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  elem -> 
{{{
Q={q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1643, q_gen_1658},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1624
<b>() -> q_gen_1625
<cons>(q_gen_1625, q_gen_1624) -> q_gen_1628
<cons>(q_gen_1625, q_gen_1628) -> q_gen_1628
<a>() -> q_gen_1629
<cons>(q_gen_1625, q_gen_1643) -> q_gen_1643
<cons>(q_gen_1625, q_gen_1658) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1628) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1643) -> q_gen_1643
<cons>(q_gen_1629, q_gen_1624) -> q_gen_1658
<cons>(q_gen_1629, q_gen_1658) -> q_gen_1658
<a, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1624) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1629, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1643) -> q_gen_1623
<b, cons>(q_gen_1625, q_gen_1658) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<b, cons>(q_gen_1629, q_gen_1643) -> q_gen_1623
<a, cons>(q_gen_1625, q_gen_1624) -> q_gen_1635
<a, cons>(q_gen_1625, q_gen_1628) -> q_gen_1635
<a, nil>() -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1624) -> q_gen_1635
<b, cons>(q_gen_1629, q_gen_1658) -> q_gen_1635
<b, nil>() -> q_gen_1635
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 30  ;  () -> elem([h1, cons(h1, t1)]) -> 30  ;  (append([l1, l2, _x]) /\ elem([i, l1])) -> elem([i, _x]) -> 31  ;  (append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]) -> 34  ;  (elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 34  ;  (elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 31  ;  (elem([e, nil])) -> BOT -> 31
}
Sat witness: Yes: ((append([t1, l2, _s])) -> append([cons(h1, t1), l2, cons(h1, _s)]), {
_s -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> nil
})

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