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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)])}
(append([_ji, _ki, _li]) /\ append([_ji, _ki, _mi])) -> eq_eltlist([_li, _mi])
)
(reverse, F:
{() -> reverse([nil, nil])
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi])}
(reverse([_pi, _qi]) /\ reverse([_pi, _ri])) -> eq_eltlist([_qi, _ri])
)
(not_null, P:
{() -> not_null([cons(x, ll)])
(not_null([nil])) -> BOT}
)
}

properties:
{(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> not_null([cons(x, ll)]) -> 0
() -> reverse([nil, nil]) -> 0
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 0
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 0
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 0
(not_null([nil])) -> BOT -> 0
}


Solving took 0.465114 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<cons>(q_gen_2157, q_gen_2156) -> q_gen_2156
<nil>() -> q_gen_2156
<a>() -> q_gen_2157
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<a, b>() -> q_gen_2145
<b, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<a, a, a>() -> q_gen_2158
<a, b, a>() -> q_gen_2158
<b, a, b>() -> q_gen_2158
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153, q_gen_2167, q_gen_2168, q_gen_2169},
Q_f={q_gen_2138},
Delta=
{
<cons>(q_gen_2169, q_gen_2168) -> q_gen_2168
<nil>() -> q_gen_2168
<a>() -> q_gen_2169
<b>() -> q_gen_2169
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<cons, cons>(q_gen_2153, q_gen_2167) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<a, b>() -> q_gen_2153
<b, a>() -> q_gen_2153
<b, b>() -> q_gen_2153
<cons, nil>(q_gen_2169, q_gen_2168) -> q_gen_2167
<nil, cons>(q_gen_2169, q_gen_2168) -> q_gen_2167
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007467 s (model generation: 0.007245,  model checking: 0.000222):

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> not_null([cons(x, ll)]) -> 0
() -> reverse([nil, nil]) -> 3
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 1
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 1
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 1
(not_null([nil])) -> BOT -> 1
}
Sat witness: Found: (() -> reverse([nil, nil]), {

})

-------------------------------------------
Step 1, which took 0.007904 s (model generation: 0.007840,  model checking: 0.000064):

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

}

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

}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138},
Q_f={q_gen_2138},
Delta=
{
<nil, nil>() -> q_gen_2138
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> not_null([cons(x, ll)]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 1
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 1
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 1
(not_null([nil])) -> BOT -> 1
}
Sat witness: Found: (() -> not_null([cons(x, ll)]), {
ll -> nil  ;  x -> b
})

-------------------------------------------
Step 2, which took 0.009247 s (model generation: 0.008948,  model checking: 0.000299):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<nil>() -> q_gen_2139
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138},
Q_f={q_gen_2138},
Delta=
{
<nil, nil>() -> q_gen_2138
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> not_null([cons(x, ll)]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 1
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 1
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 1
(not_null([nil])) -> BOT -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 3, which took 0.007699 s (model generation: 0.007682,  model checking: 0.000017):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<nil>() -> q_gen_2139
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138},
Q_f={q_gen_2138},
Delta=
{
<nil, nil>() -> q_gen_2138
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> not_null([cons(x, ll)]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 1
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 1
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 1
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((not_null([nil])) -> BOT, {

})

-------------------------------------------
Step 4, which took 0.007934 s (model generation: 0.007661,  model checking: 0.000273):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138},
Q_f={q_gen_2138},
Delta=
{
<nil, nil>() -> q_gen_2138
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> not_null([cons(x, ll)]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 1
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 4
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 2
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]), {
_ii -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.009329 s (model generation: 0.009080,  model checking: 0.000249):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145},
Q_f={q_gen_2142},
Delta=
{
<nil, nil>() -> q_gen_2144
<b, b>() -> q_gen_2145
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138},
Q_f={q_gen_2138},
Delta=
{
<nil, nil>() -> q_gen_2138
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> not_null([cons(x, ll)]) -> 6
() -> reverse([nil, nil]) -> 4
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 2
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 4
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 3
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: (() -> not_null([cons(x, ll)]), {
ll -> nil  ;  x -> a
})

-------------------------------------------
Step 6, which took 0.008754 s (model generation: 0.008455,  model checking: 0.000299):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145},
Q_f={q_gen_2142},
Delta=
{
<nil, nil>() -> q_gen_2144
<b, b>() -> q_gen_2145
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138},
Q_f={q_gen_2138},
Delta=
{
<nil, nil>() -> q_gen_2138
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> not_null([cons(x, ll)]) -> 6
() -> reverse([nil, nil]) -> 4
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 3
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 4
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 4
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 7, which took 0.009308 s (model generation: 0.009144,  model checking: 0.000164):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145},
Q_f={q_gen_2142},
Delta=
{
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138},
Q_f={q_gen_2138},
Delta=
{
<nil, nil>() -> q_gen_2138
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> not_null([cons(x, ll)]) -> 6
() -> reverse([nil, nil]) -> 4
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 6
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 4
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 4
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]), {
_ni -> nil  ;  _oi -> cons(b, nil)  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 8, which took 0.010095 s (model generation: 0.008952,  model checking: 0.001143):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145},
Q_f={q_gen_2142},
Delta=
{
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153},
Q_f={q_gen_2138},
Delta=
{
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<b, b>() -> q_gen_2153
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> not_null([cons(x, ll)]) -> 6
() -> reverse([nil, nil]) -> 4
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 6
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 7
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 5
(not_null([nil])) -> BOT -> 5
}
Sat witness: Found: ((append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]), {
_ii -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 9, which took 0.011514 s (model generation: 0.011144,  model checking: 0.000370):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<nil>() -> q_gen_2156
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153},
Q_f={q_gen_2138},
Delta=
{
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<b, b>() -> q_gen_2153
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> not_null([cons(x, ll)]) -> 6
() -> reverse([nil, nil]) -> 5
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 9
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 7
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 6
(not_null([nil])) -> BOT -> 6
}
Sat witness: Found: ((append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]), {
_ni -> nil  ;  _oi -> cons(a, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.010597 s (model generation: 0.010299,  model checking: 0.000298):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<nil>() -> q_gen_2156
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153},
Q_f={q_gen_2138},
Delta=
{
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<b, b>() -> q_gen_2153
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> not_null([cons(x, ll)]) -> 9
() -> reverse([nil, nil]) -> 6
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 9
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 7
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 7
(not_null([nil])) -> BOT -> 7
}
Sat witness: Found: (() -> not_null([cons(x, ll)]), {
ll -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 11, which took 0.011768 s (model generation: 0.010656,  model checking: 0.001112):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<nil>() -> q_gen_2156
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153},
Q_f={q_gen_2138},
Delta=
{
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<b, b>() -> q_gen_2153
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> not_null([cons(x, ll)]) -> 9
() -> reverse([nil, nil]) -> 7
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 9
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 10
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 8
(not_null([nil])) -> BOT -> 8
}
Sat witness: Found: ((append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]), {
_ii -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 0.013570 s (model generation: 0.012887,  model checking: 0.000683):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<nil>() -> q_gen_2156
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153},
Q_f={q_gen_2138},
Delta=
{
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<b, b>() -> q_gen_2153
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> not_null([cons(x, ll)]) -> 9
() -> reverse([nil, nil]) -> 8
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 12
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 10
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 9
(not_null([nil])) -> BOT -> 9
}
Sat witness: Found: ((append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]), {
_ni -> nil  ;  _oi -> cons(b, cons(b, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.014064 s (model generation: 0.012633,  model checking: 0.001431):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<nil>() -> q_gen_2156
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153, q_gen_2168, q_gen_2169},
Q_f={q_gen_2138},
Delta=
{
<nil>() -> q_gen_2168
<b>() -> q_gen_2169
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<nil, cons>(q_gen_2169, q_gen_2168) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<b, b>() -> q_gen_2153
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> not_null([cons(x, ll)]) -> 10
() -> reverse([nil, nil]) -> 9
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 12
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 13
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 10
(not_null([nil])) -> BOT -> 10
}
Sat witness: Found: ((append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]), {
_ii -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.014801 s (model generation: 0.013644,  model checking: 0.001157):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<nil>() -> q_gen_2156
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<a, b, a>() -> q_gen_2158
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153, q_gen_2168, q_gen_2169},
Q_f={q_gen_2138},
Delta=
{
<nil>() -> q_gen_2168
<b>() -> q_gen_2169
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<nil, cons>(q_gen_2169, q_gen_2168) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<b, b>() -> q_gen_2153
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> not_null([cons(x, ll)]) -> 11
() -> reverse([nil, nil]) -> 10
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 15
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 13
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 11
(not_null([nil])) -> BOT -> 11
}
Sat witness: Found: ((append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]), {
_ni -> cons(b, nil)  ;  _oi -> cons(b, nil)  ;  h1 -> b  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 15, which took 0.015883 s (model generation: 0.015432,  model checking: 0.000451):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<nil>() -> q_gen_2156
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<a, b, a>() -> q_gen_2158
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153, q_gen_2168, q_gen_2169},
Q_f={q_gen_2138},
Delta=
{
<nil>() -> q_gen_2168
<b>() -> q_gen_2169
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<cons, nil>(q_gen_2169, q_gen_2168) -> q_gen_2138
<nil, cons>(q_gen_2169, q_gen_2168) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<b, b>() -> q_gen_2153
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> not_null([cons(x, ll)]) -> 11
() -> reverse([nil, nil]) -> 11
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 15
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 13
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 14
(not_null([nil])) -> BOT -> 12
}
Sat witness: Found: ((not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]), {
_si -> nil  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 16, which took 0.016514 s (model generation: 0.014878,  model checking: 0.001636):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<nil>() -> q_gen_2156
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<a, b, a>() -> q_gen_2158
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153, q_gen_2167, q_gen_2168, q_gen_2169},
Q_f={q_gen_2138},
Delta=
{
<nil>() -> q_gen_2168
<b>() -> q_gen_2169
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<cons, cons>(q_gen_2153, q_gen_2167) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<b, b>() -> q_gen_2153
<cons, nil>(q_gen_2169, q_gen_2168) -> q_gen_2167
<nil, cons>(q_gen_2169, q_gen_2168) -> q_gen_2167
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
() -> not_null([cons(x, ll)]) -> 12
() -> reverse([nil, nil]) -> 12
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 15
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 16
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 14
(not_null([nil])) -> BOT -> 13
}
Sat witness: Found: ((append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]), {
_ii -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 17, which took 0.017601 s (model generation: 0.016445,  model checking: 0.001156):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<nil>() -> q_gen_2156
<a>() -> q_gen_2157
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<a, b, a>() -> q_gen_2158
<b, a, b>() -> q_gen_2158
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153, q_gen_2168, q_gen_2169, q_gen_2174},
Q_f={q_gen_2138},
Delta=
{
<nil>() -> q_gen_2168
<b>() -> q_gen_2169
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<cons, cons>(q_gen_2153, q_gen_2174) -> q_gen_2138
<nil, cons>(q_gen_2169, q_gen_2168) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<b, b>() -> q_gen_2153
<cons, nil>(q_gen_2169, q_gen_2168) -> q_gen_2174
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> not_null([cons(x, ll)]) -> 13
() -> reverse([nil, nil]) -> 13
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 18
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 16
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 15
(not_null([nil])) -> BOT -> 14
}
Sat witness: Found: ((append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]), {
_ni -> cons(b, nil)  ;  _oi -> cons(b, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 18, which took 0.020405 s (model generation: 0.018926,  model checking: 0.001479):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<nil>() -> q_gen_2156
<a>() -> q_gen_2157
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<a, b, a>() -> q_gen_2158
<b, a, b>() -> q_gen_2158
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153, q_gen_2167, q_gen_2168, q_gen_2169},
Q_f={q_gen_2138},
Delta=
{
<nil>() -> q_gen_2168
<b>() -> q_gen_2169
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<cons, cons>(q_gen_2153, q_gen_2167) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<a, b>() -> q_gen_2153
<b, b>() -> q_gen_2153
<cons, nil>(q_gen_2169, q_gen_2168) -> q_gen_2167
<nil, cons>(q_gen_2169, q_gen_2168) -> q_gen_2167
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> not_null([cons(x, ll)]) -> 14
() -> reverse([nil, nil]) -> 14
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 18
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 19
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 16
(not_null([nil])) -> BOT -> 15
}
Sat witness: Found: ((append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]), {
_ii -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.020523 s (model generation: 0.019449,  model checking: 0.001074):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<nil>() -> q_gen_2156
<a>() -> q_gen_2157
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<a, a, a>() -> q_gen_2158
<a, b, a>() -> q_gen_2158
<b, a, b>() -> q_gen_2158
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153, q_gen_2168, q_gen_2169, q_gen_2174},
Q_f={q_gen_2138},
Delta=
{
<nil>() -> q_gen_2168
<b>() -> q_gen_2169
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<cons, cons>(q_gen_2153, q_gen_2174) -> q_gen_2138
<nil, cons>(q_gen_2169, q_gen_2168) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<a, b>() -> q_gen_2153
<b, b>() -> q_gen_2153
<cons, nil>(q_gen_2169, q_gen_2168) -> q_gen_2174
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> not_null([cons(x, ll)]) -> 15
() -> reverse([nil, nil]) -> 15
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 21
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 19
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 17
(not_null([nil])) -> BOT -> 16
}
Sat witness: Found: ((append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]), {
_ni -> nil  ;  _oi -> cons(b, cons(a, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 20, which took 0.024042 s (model generation: 0.022207,  model checking: 0.001835):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<nil>() -> q_gen_2156
<a>() -> q_gen_2157
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<a, a, a>() -> q_gen_2158
<a, b, a>() -> q_gen_2158
<b, a, b>() -> q_gen_2158
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153, q_gen_2167, q_gen_2168, q_gen_2169},
Q_f={q_gen_2138},
Delta=
{
<nil>() -> q_gen_2168
<a>() -> q_gen_2169
<b>() -> q_gen_2169
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<cons, cons>(q_gen_2153, q_gen_2167) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<a, b>() -> q_gen_2153
<b, b>() -> q_gen_2153
<cons, nil>(q_gen_2169, q_gen_2168) -> q_gen_2167
<nil, cons>(q_gen_2169, q_gen_2168) -> q_gen_2167
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> not_null([cons(x, ll)]) -> 16
() -> reverse([nil, nil]) -> 16
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 21
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 22
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 18
(not_null([nil])) -> BOT -> 17
}
Sat witness: Found: ((append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]), {
_ii -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 0.032192 s (model generation: 0.031284,  model checking: 0.000908):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<cons>(q_gen_2157, q_gen_2156) -> q_gen_2156
<nil>() -> q_gen_2156
<a>() -> q_gen_2157
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<a, a, a>() -> q_gen_2158
<a, b, a>() -> q_gen_2158
<b, a, b>() -> q_gen_2158
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153, q_gen_2167, q_gen_2168, q_gen_2169},
Q_f={q_gen_2138},
Delta=
{
<nil>() -> q_gen_2168
<a>() -> q_gen_2169
<b>() -> q_gen_2169
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<cons, cons>(q_gen_2153, q_gen_2167) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<a, b>() -> q_gen_2153
<b, b>() -> q_gen_2153
<cons, nil>(q_gen_2169, q_gen_2168) -> q_gen_2167
<nil, cons>(q_gen_2169, q_gen_2168) -> q_gen_2167
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17
() -> not_null([cons(x, ll)]) -> 17
() -> reverse([nil, nil]) -> 17
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 24
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 22
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 19
(not_null([nil])) -> BOT -> 18
}
Sat witness: Found: ((append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]), {
_ni -> nil  ;  _oi -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 22, which took 0.033359 s (model generation: 0.028812,  model checking: 0.004547):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<cons>(q_gen_2157, q_gen_2156) -> q_gen_2156
<nil>() -> q_gen_2156
<a>() -> q_gen_2157
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<a, a, a>() -> q_gen_2158
<a, b, a>() -> q_gen_2158
<b, a, b>() -> q_gen_2158
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153, q_gen_2167, q_gen_2168, q_gen_2169},
Q_f={q_gen_2138},
Delta=
{
<cons>(q_gen_2169, q_gen_2168) -> q_gen_2168
<nil>() -> q_gen_2168
<a>() -> q_gen_2169
<b>() -> q_gen_2169
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<cons, cons>(q_gen_2153, q_gen_2167) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<a, b>() -> q_gen_2153
<b, b>() -> q_gen_2153
<cons, nil>(q_gen_2169, q_gen_2168) -> q_gen_2167
<nil, cons>(q_gen_2169, q_gen_2168) -> q_gen_2167
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18
() -> not_null([cons(x, ll)]) -> 18
() -> reverse([nil, nil]) -> 18
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 24
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 25
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 20
(not_null([nil])) -> BOT -> 19
}
Sat witness: Found: ((append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]), {
_ii -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 0.034912 s (model generation: 0.034046,  model checking: 0.000866):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<cons>(q_gen_2157, q_gen_2156) -> q_gen_2156
<nil>() -> q_gen_2156
<a>() -> q_gen_2157
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<a, a, a>() -> q_gen_2158
<a, b, a>() -> q_gen_2158
<b, a, b>() -> q_gen_2158
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153, q_gen_2167, q_gen_2168, q_gen_2169},
Q_f={q_gen_2138},
Delta=
{
<cons>(q_gen_2169, q_gen_2168) -> q_gen_2168
<nil>() -> q_gen_2168
<a>() -> q_gen_2169
<b>() -> q_gen_2169
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<cons, cons>(q_gen_2153, q_gen_2167) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<a, b>() -> q_gen_2153
<b, b>() -> q_gen_2153
<cons, nil>(q_gen_2169, q_gen_2168) -> q_gen_2167
<nil, cons>(q_gen_2169, q_gen_2168) -> q_gen_2167
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
() -> not_null([cons(x, ll)]) -> 19
() -> reverse([nil, nil]) -> 19
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 27
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 25
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 21
(not_null([nil])) -> BOT -> 20
}
Sat witness: Found: ((append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]), {
_ni -> nil  ;  _oi -> cons(a, nil)  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 24, which took 0.043618 s (model generation: 0.037948,  model checking: 0.005670):

Model:
|_
{
append -> 
{{{
Q={q_gen_2142, q_gen_2144, q_gen_2145, q_gen_2156, q_gen_2157, q_gen_2158},
Q_f={q_gen_2142},
Delta=
{
<cons>(q_gen_2157, q_gen_2156) -> q_gen_2156
<nil>() -> q_gen_2156
<a>() -> q_gen_2157
<b>() -> q_gen_2157
<cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2144
<nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2144
<nil, nil>() -> q_gen_2144
<a, a>() -> q_gen_2145
<b, a>() -> q_gen_2145
<b, b>() -> q_gen_2145
<cons, cons, cons>(q_gen_2158, q_gen_2142) -> q_gen_2142
<cons, nil, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, cons, cons>(q_gen_2145, q_gen_2144) -> q_gen_2142
<nil, nil, cons>(q_gen_2157, q_gen_2156) -> q_gen_2142
<nil, nil, nil>() -> q_gen_2142
<a, a, a>() -> q_gen_2158
<a, b, a>() -> q_gen_2158
<b, a, b>() -> q_gen_2158
<b, b, b>() -> q_gen_2158
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_2139, q_gen_2140, q_gen_2141},
Q_f={q_gen_2139},
Delta=
{
<cons>(q_gen_2141, q_gen_2139) -> q_gen_2139
<cons>(q_gen_2141, q_gen_2140) -> q_gen_2139
<nil>() -> q_gen_2140
<a>() -> q_gen_2141
<b>() -> q_gen_2141
}

Datatype: <eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_2138, q_gen_2153, q_gen_2167, q_gen_2168, q_gen_2169},
Q_f={q_gen_2138},
Delta=
{
<cons>(q_gen_2169, q_gen_2168) -> q_gen_2168
<nil>() -> q_gen_2168
<a>() -> q_gen_2169
<b>() -> q_gen_2169
<cons, cons>(q_gen_2153, q_gen_2138) -> q_gen_2138
<cons, cons>(q_gen_2153, q_gen_2167) -> q_gen_2138
<nil, nil>() -> q_gen_2138
<a, a>() -> q_gen_2153
<a, b>() -> q_gen_2153
<b, a>() -> q_gen_2153
<b, b>() -> q_gen_2153
<cons, nil>(q_gen_2169, q_gen_2168) -> q_gen_2167
<nil, cons>(q_gen_2169, q_gen_2168) -> q_gen_2167
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20
() -> not_null([cons(x, ll)]) -> 20
() -> reverse([nil, nil]) -> 20
(append([_ni, cons(h1, nil), _oi]) /\ reverse([t1, _ni])) -> reverse([cons(h1, t1), _oi]) -> 27
(append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]) -> 28
(not_null([l1]) /\ reverse([l1, _si])) -> not_null([_si]) -> 22
(not_null([nil])) -> BOT -> 21
}
Sat witness: Found: ((append([t1, l2, _ii])) -> append([cons(h1, t1), l2, cons(h1, _ii)]), {
_ii -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

Total time: 0.465114
Reason for stopping: Proved