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


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, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)])}
(append([_pg, _qg, _rg]) /\ append([_pg, _qg, _sg])) -> eq_eltlist([_rg, _sg])
)
}

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


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> elem([h1, cons(h1, t1)]) -> 0
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 0
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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 34.956504 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1700, q_gen_1702, q_gen_1724},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<a, b>() -> q_gen_1700
<b, a>() -> q_gen_1700
<cons, cons>(q_gen_1629, q_gen_1724) -> q_gen_1724
<cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1724
<cons, cons>(q_gen_1700, q_gen_1724) -> q_gen_1724
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1724) -> q_gen_1623
<nil, cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1700, q_gen_1724) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
<cons, cons, cons>(q_gen_1643, q_gen_1702) -> q_gen_1702
<cons, nil, cons>(q_gen_1629, q_gen_1724) -> q_gen_1702
<cons, nil, cons>(q_gen_1700, q_gen_1628) -> q_gen_1702
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007781 s (model generation: 0.007454,  model checking: 0.000327):

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

}

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

}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 1
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 1, which took 0.007020 s (model generation: 0.006890,  model checking: 0.000130):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 1
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.007842 s (model generation: 0.007552,  model checking: 0.000290):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 1
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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: Found: ((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.008821 s (model generation: 0.008499,  model checking: 0.000322):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622},
Q_f={q_gen_1620},
Delta=
{
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1621
<nil>() -> q_gen_1621
<a>() -> q_gen_1622
<b>() -> q_gen_1622
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 1
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.008656 s (model generation: 0.008513,  model checking: 0.000143):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629},
Q_f={q_gen_1623},
Delta=
{
<nil, nil>() -> q_gen_1628
<b, b>() -> q_gen_1629
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622},
Q_f={q_gen_1620},
Delta=
{
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1621
<nil>() -> q_gen_1621
<a>() -> q_gen_1622
<b>() -> q_gen_1622
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 2
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> b  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.013676 s (model generation: 0.013571,  model checking: 0.000105):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629},
Q_f={q_gen_1623},
Delta=
{
<nil, nil>() -> q_gen_1628
<b, b>() -> q_gen_1629
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622},
Q_f={q_gen_1620},
Delta=
{
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1621
<nil>() -> q_gen_1621
<a>() -> q_gen_1622
<b>() -> q_gen_1622
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, nil>() -> q_gen_1620
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 3
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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: Found: ((elem([e, nil])) -> BOT, {
e -> b
})

-------------------------------------------
Step 6, which took 0.037674 s (model generation: 0.010802,  model checking: 0.026872):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629},
Q_f={q_gen_1623},
Delta=
{
<nil, nil>() -> q_gen_1628
<b, b>() -> q_gen_1629
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<a>() -> q_gen_1626
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 4
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.009323 s (model generation: 0.009088,  model checking: 0.000235):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629},
Q_f={q_gen_1623},
Delta=
{
<nil, nil>() -> q_gen_1628
<b, b>() -> q_gen_1629
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<a>() -> q_gen_1626
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 4
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 8, which took 0.013671 s (model generation: 0.013032,  model checking: 0.000639):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629},
Q_f={q_gen_1623},
Delta=
{
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<a>() -> q_gen_1626
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 4
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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: Found: ((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.011243 s (model generation: 0.010256,  model checking: 0.000987):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629},
Q_f={q_gen_1623},
Delta=
{
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 4
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.012787 s (model generation: 0.010955,  model checking: 0.001832):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 7
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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: Found: ((append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]), {
_tg -> cons(b, cons(b, nil))  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 11, which took 0.017926 s (model generation: 0.016625,  model checking: 0.001301):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 7
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 12, which took 0.013897 s (model generation: 0.012255,  model checking: 0.001642):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> elem([h1, cons(h1, t1)]) -> 9
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 7
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 7
(elem([e, nil])) -> BOT -> 8
}
Sat witness: Found: ((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.012760 s (model generation: 0.012525,  model checking: 0.000235):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> elem([h1, cons(h1, t1)]) -> 9
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 7
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 10
(elem([e, nil])) -> BOT -> 8
}
Sat witness: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 14, which took 0.085500 s (model generation: 0.084922,  model checking: 0.000578):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630},
Q_f={q_gen_1620},
Delta=
{
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1621
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> elem([h1, cons(h1, t1)]) -> 9
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 7
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 10
(elem([e, nil])) -> BOT -> 8
}
Sat witness: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.023057 s (model generation: 0.019761,  model checking: 0.003296):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630},
Q_f={q_gen_1620},
Delta=
{
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1621
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> elem([h1, cons(h1, t1)]) -> 9
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 10
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 10
(elem([e, nil])) -> BOT -> 8
}
Sat witness: Found: ((append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]), {
_tg -> cons(b, cons(b, nil))  ;  i -> a  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 16, which took 0.015731 s (model generation: 0.015167,  model checking: 0.000564):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630},
Q_f={q_gen_1620},
Delta=
{
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1621
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> elem([h1, cons(h1, t1)]) -> 12
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 10
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 10
(elem([e, nil])) -> BOT -> 9
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 17, which took 0.017390 s (model generation: 0.016456,  model checking: 0.000934):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630},
Q_f={q_gen_1620},
Delta=
{
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1621
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 10
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 13
(elem([e, nil])) -> BOT -> 10
}
Sat witness: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> a  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 18, which took 0.018278 s (model generation: 0.017674,  model checking: 0.000604):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630},
Q_f={q_gen_1620},
Delta=
{
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1621
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, nil>() -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> elem([h1, cons(h1, t1)]) -> 12
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 10
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 13
(elem([e, nil])) -> BOT -> 13
}
Sat witness: Found: ((elem([e, nil])) -> BOT, {
e -> a
})

-------------------------------------------
Step 19, which took 0.019124 s (model generation: 0.017907,  model checking: 0.001217):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> elem([h1, cons(h1, t1)]) -> 12
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 10
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 13
(elem([e, nil])) -> BOT -> 13
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 20, which took 0.021017 s (model generation: 0.019799,  model checking: 0.001218):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> elem([h1, cons(h1, t1)]) -> 12
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 10
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 13
(elem([e, nil])) -> BOT -> 13
}
Sat witness: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 0.021688 s (model generation: 0.019536,  model checking: 0.002152):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, b, a>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> elem([h1, cons(h1, t1)]) -> 12
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 13
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 13
(elem([e, nil])) -> BOT -> 13
}
Sat witness: Found: ((append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]), {
_tg -> cons(b, cons(a, nil))  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 22, which took 0.021365 s (model generation: 0.020808,  model checking: 0.000557):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, b, a>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> elem([h1, cons(h1, t1)]) -> 15
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 13
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 13
(elem([e, nil])) -> BOT -> 13
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 23, which took 0.026226 s (model generation: 0.025261,  model checking: 0.000965):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, b, a>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 13
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 16
(elem([e, nil])) -> BOT -> 14
}
Sat witness: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 24, which took 0.030259 s (model generation: 0.027315,  model checking: 0.002944):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, b, a>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 13
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 16
(elem([e, nil])) -> BOT -> 14
}
Sat witness: Found: ((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 25, which took 0.025439 s (model generation: 0.023874,  model checking: 0.001565):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, b, a>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 13
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 16
(elem([e, nil])) -> BOT -> 14
}
Sat witness: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 26, which took 0.028766 s (model generation: 0.025060,  model checking: 0.003706):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 16
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 16
(elem([e, nil])) -> BOT -> 14
}
Sat witness: Found: ((append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]), {
_tg -> cons(b, cons(a, cons(a, cons(b, nil))))  ;  i -> a  ;  l1 -> cons(b, cons(a, nil))  ;  l2 -> cons(b, cons(b, cons(a, cons(b, nil))))
})

-------------------------------------------
Step 27, which took 0.031535 s (model generation: 0.030692,  model checking: 0.000843):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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)]) -> 18
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 16
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 16
(elem([e, nil])) -> BOT -> 15
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 28, which took 0.035823 s (model generation: 0.032450,  model checking: 0.003373):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 16
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 19
(elem([e, nil])) -> BOT -> 16
}
Sat witness: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(a, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 29, which took 0.036137 s (model generation: 0.033571,  model checking: 0.002566):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 16
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 19
(elem([e, nil])) -> BOT -> 17
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 30, which took 0.037073 s (model generation: 0.036082,  model checking: 0.000991):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 16
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 19
(elem([e, nil])) -> BOT -> 17
}
Sat witness: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 31, which took 0.044259 s (model generation: 0.038926,  model checking: 0.005333):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 19
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 19
(elem([e, nil])) -> BOT -> 17
}
Sat witness: Found: ((append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]), {
_tg -> cons(b, cons(b, cons(a, cons(b, nil))))  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, cons(b, cons(a, cons(b, nil))))
})

-------------------------------------------
Step 32, which took 0.045121 s (model generation: 0.044553,  model checking: 0.000568):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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)]) -> 21
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 19
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 19
(elem([e, nil])) -> BOT -> 18
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 33, which took 0.046529 s (model generation: 0.045393,  model checking: 0.001136):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1625
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 19
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 22
(elem([e, nil])) -> BOT -> 19
}
Sat witness: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 34, which took 0.049440 s (model generation: 0.047556,  model checking: 0.001884):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1621
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 19
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 22
(elem([e, nil])) -> BOT -> 20
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 35, which took 0.052268 s (model generation: 0.050726,  model checking: 0.001542):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 19
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 22
(elem([e, nil])) -> BOT -> 20
}
Sat witness: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 36, which took 0.066877 s (model generation: 0.055554,  model checking: 0.011323):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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)]) -> 22
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 20
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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 -> 21
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 37, which took 0.063931 s (model generation: 0.057935,  model checking: 0.005996):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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)]) -> 22
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 23
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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 -> 21
}
Sat witness: Found: ((append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]), {
_tg -> cons(b, cons(b, cons(a, cons(b, nil))))  ;  i -> a  ;  l1 -> cons(b, cons(b, cons(a, nil)))  ;  l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 38, which took 0.078715 s (model generation: 0.075077,  model checking: 0.003638):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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)]) -> 22
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 23
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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 -> 22
}
Sat witness: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 39, which took 0.084838 s (model generation: 0.083420,  model checking: 0.001418):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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)]) -> 23
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 23
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 26
(elem([e, nil])) -> BOT -> 23
}
Sat witness: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 40, which took 0.095740 s (model generation: 0.092999,  model checking: 0.002741):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1621
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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)]) -> 23
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 26
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 26
(elem([e, nil])) -> BOT -> 24
}
Sat witness: Found: ((append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]), {
_tg -> cons(a, cons(b, cons(b, nil)))  ;  i -> b  ;  l1 -> cons(b, cons(b, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 41, which took 0.098165 s (model generation: 0.091734,  model checking: 0.006431):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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)]) -> 24
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 26
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 28
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 26
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 26
(elem([e, nil])) -> BOT -> 25
}
Sat witness: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 42, which took 0.098359 s (model generation: 0.092270,  model checking: 0.006089):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<a, b>() -> q_gen_1629
<b, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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)]) -> 25
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 29
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 28
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 27
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 27
(elem([e, nil])) -> BOT -> 26
}
Sat witness: Found: ((append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]), {
_tg -> cons(a, cons(a, nil))  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 43, which took 0.105660 s (model generation: 0.105188,  model checking: 0.000472):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1634, q_gen_1638, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1634) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<a, b>() -> q_gen_1629
<b, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1634
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1634
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, cons, cons>(q_gen_1643, q_gen_1638) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1634) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1634) -> q_gen_1638
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1638
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1638
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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)]) -> 26
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 29
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 28
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 27
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 27
(elem([e, nil])) -> BOT -> 26
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 44, which took 0.134197 s (model generation: 0.104523,  model checking: 0.029674):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1640, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1650},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<a, b>() -> q_gen_1629
<b, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons>(q_gen_1629, q_gen_1650) -> q_gen_1650
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1650
<cons, cons, cons>(q_gen_1643, q_gen_1640) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1640
<cons, nil, cons>(q_gen_1629, q_gen_1650) -> q_gen_1640
<nil, cons, cons>(q_gen_1629, q_gen_1650) -> q_gen_1640
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1640
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1621
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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)]) -> 27
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 29
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 28
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 30
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 28
(elem([e, nil])) -> BOT -> 27
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 45, which took 0.114114 s (model generation: 0.101888,  model checking: 0.012226):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1635, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1696},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<cons, cons>(q_gen_1635, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, b>() -> q_gen_1629
<b, b>() -> q_gen_1629
<a, a>() -> q_gen_1635
<b, a>() -> q_gen_1635
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, cons, cons>(q_gen_1643, q_gen_1696) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1635, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
<cons, nil, cons>(q_gen_1635, q_gen_1628) -> q_gen_1696
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 29
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 31
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 30
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 29
(elem([e, nil])) -> BOT -> 28
}
Sat witness: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> nil  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 46, which took 0.129252 s (model generation: 0.109069,  model checking: 0.020183):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1699, q_gen_1700},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<a, b>() -> q_gen_1700
<b, a>() -> q_gen_1700
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, cons, cons>(q_gen_1643, q_gen_1699) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
<cons, nil, cons>(q_gen_1700, q_gen_1628) -> q_gen_1699
<nil, cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1699
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 32
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 31
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 30
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 30
(elem([e, nil])) -> BOT -> 29
}
Sat witness: Found: ((append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]), {
_tg -> cons(a, cons(b, cons(b, cons(b, cons(a, cons(b, nil))))))  ;  i -> b  ;  l1 -> cons(a, cons(b, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 47, which took 0.131930 s (model generation: 0.125937,  model checking: 0.005993):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1699, q_gen_1700},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<a, b>() -> q_gen_1700
<b, a>() -> q_gen_1700
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, cons, cons>(q_gen_1643, q_gen_1699) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
<cons, nil, cons>(q_gen_1700, q_gen_1628) -> q_gen_1699
<nil, cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1699
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

}
--
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, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 32
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 34
(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]) -> 31
(elem([e, nil])) -> BOT -> 30
}
Sat witness: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 48, which took 0.166116 s (model generation: 0.152726,  model checking: 0.013390):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1634, q_gen_1640, q_gen_1641, q_gen_1642, q_gen_1643},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<a, b>() -> q_gen_1629
<b, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1634
<cons, cons>(q_gen_1629, q_gen_1634) -> q_gen_1634
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1634
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, cons, cons>(q_gen_1643, q_gen_1640) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1634) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1634) -> q_gen_1640
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1640
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 31
() -> elem([h1, cons(h1, t1)]) -> 31
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 32
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 32
(elem([e, nil])) -> BOT -> 31
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(b, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 49, which took 0.166323 s (model generation: 0.160765,  model checking: 0.005558):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1640, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1650},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<a, b>() -> q_gen_1629
<b, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons>(q_gen_1629, q_gen_1650) -> q_gen_1650
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1650
<cons, cons, cons>(q_gen_1643, q_gen_1640) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1640
<cons, nil, cons>(q_gen_1629, q_gen_1650) -> q_gen_1640
<nil, cons, cons>(q_gen_1629, q_gen_1650) -> q_gen_1640
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1640
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 32
() -> elem([h1, cons(h1, t1)]) -> 32
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 35
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 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]) -> 33
(elem([e, nil])) -> BOT -> 32
}
Sat witness: Found: ((append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]), {
_tg -> cons(a, nil)  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 50, which took 1.833564 s (model generation: 0.209836,  model checking: 1.623728):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1700, q_gen_1702},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<a, b>() -> q_gen_1700
<b, a>() -> q_gen_1700
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
<cons, cons, cons>(q_gen_1643, q_gen_1702) -> q_gen_1702
<cons, nil, cons>(q_gen_1700, q_gen_1628) -> q_gen_1702
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 33
() -> elem([h1, cons(h1, t1)]) -> 33
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 38
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 35
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 35
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 34
(elem([e, nil])) -> BOT -> 33
}
Sat witness: Found: ((append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]), {
_tg -> cons(b, cons(b, nil))  ;  i -> a  ;  l1 -> cons(b, cons(a, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 51, which took 0.187571 s (model generation: 0.180986,  model checking: 0.006585):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1640, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1650, q_gen_1700},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons>(q_gen_1629, q_gen_1650) -> q_gen_1650
<cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1650
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1650
<a, b>() -> q_gen_1700
<b, a>() -> q_gen_1700
<cons, cons, cons>(q_gen_1643, q_gen_1640) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1640
<cons, nil, cons>(q_gen_1629, q_gen_1650) -> q_gen_1640
<cons, nil, cons>(q_gen_1700, q_gen_1628) -> q_gen_1640
<cons, nil, cons>(q_gen_1700, q_gen_1650) -> q_gen_1640
<nil, cons, cons>(q_gen_1629, q_gen_1650) -> q_gen_1640
<nil, cons, cons>(q_gen_1700, q_gen_1650) -> q_gen_1640
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1640
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 34
() -> elem([h1, cons(h1, t1)]) -> 34
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 38
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 35
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 38
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 35
(elem([e, nil])) -> BOT -> 34
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 52, which took 0.189534 s (model generation: 0.186723,  model checking: 0.002811):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1634, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1700, q_gen_1702},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1634
<cons, cons>(q_gen_1629, q_gen_1634) -> q_gen_1634
<cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1634
<a, b>() -> q_gen_1700
<b, a>() -> q_gen_1700
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1634) -> q_gen_1623
<nil, cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
<cons, cons, cons>(q_gen_1643, q_gen_1702) -> q_gen_1702
<cons, nil, cons>(q_gen_1629, q_gen_1634) -> q_gen_1702
<cons, nil, cons>(q_gen_1700, q_gen_1628) -> q_gen_1702
<cons, nil, cons>(q_gen_1700, q_gen_1634) -> q_gen_1702
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 35
() -> elem([h1, cons(h1, t1)]) -> 35
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 38
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 38
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 38
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 36
(elem([e, nil])) -> BOT -> 35
}
Sat witness: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 53, which took 0.263601 s (model generation: 0.256361,  model checking: 0.007240):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1699, q_gen_1700, q_gen_1724},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<a, b>() -> q_gen_1700
<b, a>() -> q_gen_1700
<cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1724
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, cons, cons>(q_gen_1643, q_gen_1699) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
<cons, nil, cons>(q_gen_1629, q_gen_1724) -> q_gen_1699
<cons, nil, cons>(q_gen_1700, q_gen_1628) -> q_gen_1699
<nil, cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1699
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 36
() -> elem([h1, cons(h1, t1)]) -> 36
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 38
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 41
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 39
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 37
(elem([e, nil])) -> BOT -> 36
}
Sat witness: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 54, which took 0.368129 s (model generation: 0.357482,  model checking: 0.010647):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1640, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1650, q_gen_1700},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<cons, cons>(q_gen_1629, q_gen_1650) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1650
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1650
<a, b>() -> q_gen_1700
<b, a>() -> q_gen_1700
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, cons, cons>(q_gen_1643, q_gen_1640) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1700, q_gen_1650) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1650) -> q_gen_1640
<cons, nil, cons>(q_gen_1700, q_gen_1628) -> q_gen_1640
<cons, nil, cons>(q_gen_1700, q_gen_1650) -> q_gen_1640
<nil, cons, cons>(q_gen_1629, q_gen_1650) -> q_gen_1640
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1640
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 37
() -> elem([h1, cons(h1, t1)]) -> 37
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 41
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 41
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 39
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 38
(elem([e, nil])) -> BOT -> 37
}
Sat witness: Found: ((append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]), {
_tg -> cons(a, cons(a, nil))  ;  i -> b  ;  l1 -> cons(a, cons(b, nil))  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 55, which took 0.395428 s (model generation: 0.377176,  model checking: 0.018252):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1700, q_gen_1702, q_gen_1724},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<a, b>() -> q_gen_1700
<b, a>() -> q_gen_1700
<cons, cons>(q_gen_1629, q_gen_1724) -> q_gen_1724
<cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1724
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
<cons, cons, cons>(q_gen_1643, q_gen_1702) -> q_gen_1702
<cons, nil, cons>(q_gen_1629, q_gen_1724) -> q_gen_1702
<cons, nil, cons>(q_gen_1700, q_gen_1628) -> q_gen_1702
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 38
() -> elem([h1, cons(h1, t1)]) -> 38
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 41
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 44
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 40
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 39
(elem([e, nil])) -> BOT -> 38
}
Sat witness: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> cons(b, cons(b, cons(a, cons(a, cons(b, nil)))))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, cons(a, cons(a, cons(b, nil)))))  ;  t1 -> nil
})

-------------------------------------------
Step 56, which took 0.539759 s (model generation: 0.528370,  model checking: 0.011389):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1700, q_gen_1702, q_gen_1724},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<cons, cons>(q_gen_1629, q_gen_1724) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<a, b>() -> q_gen_1700
<b, a>() -> q_gen_1700
<cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1724
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1724) -> q_gen_1623
<nil, cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
<cons, cons, cons>(q_gen_1643, q_gen_1702) -> q_gen_1702
<cons, nil, cons>(q_gen_1629, q_gen_1724) -> q_gen_1702
<cons, nil, cons>(q_gen_1700, q_gen_1628) -> q_gen_1702
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 39
() -> elem([h1, cons(h1, t1)]) -> 39
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 44
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 44
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 41
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 40
(elem([e, nil])) -> BOT -> 39
}
Sat witness: Found: ((append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]), {
_tg -> cons(a, cons(a, cons(a, nil)))  ;  i -> b  ;  l1 -> cons(a, cons(a, cons(b, nil)))  ;  l2 -> nil
})

-------------------------------------------
Step 57, which took 0.455703 s (model generation: 0.423059,  model checking: 0.032644):

Model:
|_
{
append -> 
{{{
Q={q_gen_1623, q_gen_1628, q_gen_1629, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1700, q_gen_1702, q_gen_1724},
Q_f={q_gen_1623},
Delta=
{
<cons>(q_gen_1642, q_gen_1641) -> q_gen_1641
<nil>() -> q_gen_1641
<a>() -> q_gen_1642
<b>() -> q_gen_1642
<cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1628
<nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1628
<nil, nil>() -> q_gen_1628
<a, a>() -> q_gen_1629
<b, b>() -> q_gen_1629
<a, b>() -> q_gen_1700
<b, a>() -> q_gen_1700
<cons, cons>(q_gen_1629, q_gen_1724) -> q_gen_1724
<cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1724
<cons, cons>(q_gen_1700, q_gen_1724) -> q_gen_1724
<cons, cons, cons>(q_gen_1643, q_gen_1623) -> q_gen_1623
<cons, nil, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1628) -> q_gen_1623
<nil, cons, cons>(q_gen_1629, q_gen_1724) -> q_gen_1623
<nil, cons, cons>(q_gen_1700, q_gen_1628) -> q_gen_1623
<nil, nil, cons>(q_gen_1642, q_gen_1641) -> q_gen_1623
<nil, nil, nil>() -> q_gen_1623
<a, a, a>() -> q_gen_1643
<a, b, a>() -> q_gen_1643
<b, a, b>() -> q_gen_1643
<b, b, b>() -> q_gen_1643
<cons, cons, cons>(q_gen_1643, q_gen_1702) -> q_gen_1702
<cons, nil, cons>(q_gen_1629, q_gen_1724) -> q_gen_1702
<cons, nil, cons>(q_gen_1700, q_gen_1628) -> q_gen_1702
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1625, q_gen_1626, q_gen_1630, q_gen_1637, q_gen_1647},
Q_f={q_gen_1620},
Delta=
{
<nil>() -> q_gen_1621
<b>() -> q_gen_1622
<cons>(q_gen_1622, q_gen_1621) -> q_gen_1625
<cons>(q_gen_1622, q_gen_1625) -> q_gen_1625
<a>() -> q_gen_1626
<cons>(q_gen_1622, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1622, q_gen_1647) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1625) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1637) -> q_gen_1637
<cons>(q_gen_1626, q_gen_1621) -> q_gen_1647
<cons>(q_gen_1626, q_gen_1647) -> q_gen_1647
<a, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1621) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1626, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1621) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1637) -> q_gen_1620
<b, cons>(q_gen_1622, q_gen_1647) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1625) -> q_gen_1620
<b, cons>(q_gen_1626, q_gen_1637) -> q_gen_1620
<a, cons>(q_gen_1622, q_gen_1621) -> q_gen_1630
<a, cons>(q_gen_1622, q_gen_1625) -> q_gen_1630
<a, nil>() -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1621) -> q_gen_1630
<b, cons>(q_gen_1626, q_gen_1647) -> q_gen_1630
<b, nil>() -> q_gen_1630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 40
() -> elem([h1, cons(h1, t1)]) -> 40
(append([l1, l2, _tg]) /\ elem([i, l1])) -> elem([i, _tg]) -> 44
(append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]) -> 47
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 42
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 41
(elem([e, nil])) -> BOT -> 40
}
Sat witness: Found: ((append([t1, l2, _og])) -> append([cons(h1, t1), l2, cons(h1, _og)]), {
_og -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, cons(a, nil)))  ;  t1 -> nil
})

Total time: 34.956504
Reason for stopping: Proved