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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _hb])) -> append([cons(h1, t1), l2, cons(h1, _hb)])}
(append([_ib, _jb, _kb]) /\ append([_ib, _jb, _lb])) -> eq_eltlist([_kb, _lb])
)
(reverse, F:
{() -> reverse([nil, nil])
(append([_mb, cons(h1, nil), _nb]) /\ reverse([t1, _mb])) -> reverse([cons(h1, t1), _nb])}
(reverse([_ob, _pb]) /\ reverse([_ob, _qb])) -> eq_eltlist([_pb, _qb])
)
(not_null, P:
{() -> not_null([cons(x, ll)])
(not_null([nil])) -> BOT}
)
}

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


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([_mb, cons(h1, nil), _nb]) /\ reverse([t1, _mb])) -> reverse([cons(h1, t1), _nb]) -> 0
(append([t1, l2, _hb])) -> append([cons(h1, t1), l2, cons(h1, _hb)]) -> 0
(not_null([l1]) /\ reverse([l1, _rb])) -> not_null([_rb]) -> 0
(not_null([nil])) -> BOT -> 0
}


Solving took 0.333148 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<cons>(q_gen_407, q_gen_406) -> q_gen_406
<nil>() -> q_gen_406
<a>() -> q_gen_407
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, cons>(q_gen_407, q_gen_406) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<a, b>() -> q_gen_395
<b, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<a, a, a>() -> q_gen_408
<a, b, a>() -> q_gen_408
<b, a, b>() -> q_gen_408
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403, q_gen_417, q_gen_418, q_gen_419},
Q_f={q_gen_388},
Delta=
{
<cons>(q_gen_419, q_gen_418) -> q_gen_418
<nil>() -> q_gen_418
<a>() -> q_gen_419
<b>() -> q_gen_419
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<cons, cons>(q_gen_403, q_gen_417) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<a, b>() -> q_gen_403
<b, a>() -> q_gen_403
<b, b>() -> q_gen_403
<cons, nil>(q_gen_419, q_gen_418) -> q_gen_417
<nil, cons>(q_gen_419, q_gen_418) -> q_gen_417
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006799 s (model generation: 0.006192,  model checking: 0.000607):

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

}

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

}

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

}

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

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

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

})

-------------------------------------------
Step 1, which took 0.006419 s (model generation: 0.006290,  model checking: 0.000129):

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

}

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

}

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

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

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

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

-------------------------------------------
Step 2, which took 0.006456 s (model generation: 0.006323,  model checking: 0.000133):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<nil>() -> q_gen_389
<b>() -> q_gen_391
}

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

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

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

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

-------------------------------------------
Step 3, which took 0.006241 s (model generation: 0.006200,  model checking: 0.000041):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<nil>() -> q_gen_389
<b>() -> q_gen_391
}

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

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

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

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

})

-------------------------------------------
Step 4, which took 0.005774 s (model generation: 0.005017,  model checking: 0.000757):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<b>() -> q_gen_391
}

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

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

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

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

-------------------------------------------
Step 5, which took 0.006985 s (model generation: 0.006175,  model checking: 0.000810):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395},
Q_f={q_gen_392},
Delta=
{
<nil, nil>() -> q_gen_394
<b, b>() -> q_gen_395
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<b>() -> q_gen_391
}

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

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

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

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

-------------------------------------------
Step 6, which took 0.007286 s (model generation: 0.006322,  model checking: 0.000964):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395},
Q_f={q_gen_392},
Delta=
{
<nil, nil>() -> q_gen_394
<b, b>() -> q_gen_395
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

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

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

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

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

-------------------------------------------
Step 7, which took 0.006394 s (model generation: 0.005993,  model checking: 0.000401):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395},
Q_f={q_gen_392},
Delta=
{
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

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

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

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

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

-------------------------------------------
Step 8, which took 0.008724 s (model generation: 0.006747,  model checking: 0.001977):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395},
Q_f={q_gen_392},
Delta=
{
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403},
Q_f={q_gen_388},
Delta=
{
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<nil, nil>() -> q_gen_388
<b, b>() -> q_gen_403
}

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

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

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

-------------------------------------------
Step 9, which took 0.008464 s (model generation: 0.007377,  model checking: 0.001087):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<nil>() -> q_gen_406
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403},
Q_f={q_gen_388},
Delta=
{
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<nil, nil>() -> q_gen_388
<b, b>() -> q_gen_403
}

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

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

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

-------------------------------------------
Step 10, which took 0.007968 s (model generation: 0.007047,  model checking: 0.000921):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<nil>() -> q_gen_406
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403},
Q_f={q_gen_388},
Delta=
{
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<b, b>() -> q_gen_403
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> not_null([cons(x, ll)]) -> 9
() -> reverse([nil, nil]) -> 6
(append([_mb, cons(h1, nil), _nb]) /\ reverse([t1, _mb])) -> reverse([cons(h1, t1), _nb]) -> 9
(append([t1, l2, _hb])) -> append([cons(h1, t1), l2, cons(h1, _hb)]) -> 7
(not_null([l1]) /\ reverse([l1, _rb])) -> not_null([_rb]) -> 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.007616 s (model generation: 0.005854,  model checking: 0.001762):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<nil>() -> q_gen_406
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403},
Q_f={q_gen_388},
Delta=
{
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<b, b>() -> q_gen_403
}

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

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

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

-------------------------------------------
Step 12, which took 0.008265 s (model generation: 0.007538,  model checking: 0.000727):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<nil>() -> q_gen_406
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, cons>(q_gen_407, q_gen_406) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403},
Q_f={q_gen_388},
Delta=
{
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<b, b>() -> q_gen_403
}

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

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

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

-------------------------------------------
Step 13, which took 0.010659 s (model generation: 0.008053,  model checking: 0.002606):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<nil>() -> q_gen_406
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, cons>(q_gen_407, q_gen_406) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403, q_gen_418, q_gen_419},
Q_f={q_gen_388},
Delta=
{
<nil>() -> q_gen_418
<b>() -> q_gen_419
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_419, q_gen_418) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<b, b>() -> q_gen_403
}

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

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

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

-------------------------------------------
Step 14, which took 0.009472 s (model generation: 0.008460,  model checking: 0.001012):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<nil>() -> q_gen_406
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, cons>(q_gen_407, q_gen_406) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<a, b, a>() -> q_gen_408
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403, q_gen_418, q_gen_419},
Q_f={q_gen_388},
Delta=
{
<nil>() -> q_gen_418
<b>() -> q_gen_419
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_419, q_gen_418) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<b, b>() -> q_gen_403
}

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

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

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

-------------------------------------------
Step 15, which took 0.010042 s (model generation: 0.009244,  model checking: 0.000798):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<nil>() -> q_gen_406
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, cons>(q_gen_407, q_gen_406) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<a, b, a>() -> q_gen_408
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403, q_gen_418, q_gen_419},
Q_f={q_gen_388},
Delta=
{
<nil>() -> q_gen_418
<b>() -> q_gen_419
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<cons, nil>(q_gen_419, q_gen_418) -> q_gen_388
<nil, cons>(q_gen_419, q_gen_418) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<b, b>() -> q_gen_403
}

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

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

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

-------------------------------------------
Step 16, which took 0.011023 s (model generation: 0.008571,  model checking: 0.002452):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<nil>() -> q_gen_406
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, cons>(q_gen_407, q_gen_406) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<a, b, a>() -> q_gen_408
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403, q_gen_417, q_gen_418, q_gen_419},
Q_f={q_gen_388},
Delta=
{
<nil>() -> q_gen_418
<b>() -> q_gen_419
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<cons, cons>(q_gen_403, q_gen_417) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<b, b>() -> q_gen_403
<cons, nil>(q_gen_419, q_gen_418) -> q_gen_417
<nil, cons>(q_gen_419, q_gen_418) -> q_gen_417
}

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

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

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

-------------------------------------------
Step 17, which took 0.012295 s (model generation: 0.010943,  model checking: 0.001352):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<nil>() -> q_gen_406
<a>() -> q_gen_407
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, cons>(q_gen_407, q_gen_406) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<a, b, a>() -> q_gen_408
<b, a, b>() -> q_gen_408
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403, q_gen_418, q_gen_419, q_gen_424},
Q_f={q_gen_388},
Delta=
{
<nil>() -> q_gen_418
<b>() -> q_gen_419
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<cons, cons>(q_gen_403, q_gen_424) -> q_gen_388
<nil, cons>(q_gen_419, q_gen_418) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<b, b>() -> q_gen_403
<cons, nil>(q_gen_419, q_gen_418) -> q_gen_424
}

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

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

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

-------------------------------------------
Step 18, which took 0.011970 s (model generation: 0.010750,  model checking: 0.001220):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<nil>() -> q_gen_406
<a>() -> q_gen_407
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, cons>(q_gen_407, q_gen_406) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<a, b, a>() -> q_gen_408
<b, a, b>() -> q_gen_408
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403, q_gen_417, q_gen_418, q_gen_419},
Q_f={q_gen_388},
Delta=
{
<nil>() -> q_gen_418
<b>() -> q_gen_419
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<cons, cons>(q_gen_403, q_gen_417) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<a, b>() -> q_gen_403
<b, b>() -> q_gen_403
<cons, nil>(q_gen_419, q_gen_418) -> q_gen_417
<nil, cons>(q_gen_419, q_gen_418) -> q_gen_417
}

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

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

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

-------------------------------------------
Step 19, which took 0.013179 s (model generation: 0.011197,  model checking: 0.001982):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<nil>() -> q_gen_406
<a>() -> q_gen_407
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, cons>(q_gen_407, q_gen_406) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<a, a, a>() -> q_gen_408
<a, b, a>() -> q_gen_408
<b, a, b>() -> q_gen_408
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403, q_gen_418, q_gen_419, q_gen_424},
Q_f={q_gen_388},
Delta=
{
<nil>() -> q_gen_418
<b>() -> q_gen_419
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<cons, cons>(q_gen_403, q_gen_424) -> q_gen_388
<nil, cons>(q_gen_419, q_gen_418) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<a, b>() -> q_gen_403
<b, b>() -> q_gen_403
<cons, nil>(q_gen_419, q_gen_418) -> q_gen_424
}

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

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

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

-------------------------------------------
Step 20, which took 0.014419 s (model generation: 0.011952,  model checking: 0.002467):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<nil>() -> q_gen_406
<a>() -> q_gen_407
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, cons>(q_gen_407, q_gen_406) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<a, a, a>() -> q_gen_408
<a, b, a>() -> q_gen_408
<b, a, b>() -> q_gen_408
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403, q_gen_417, q_gen_418, q_gen_419},
Q_f={q_gen_388},
Delta=
{
<nil>() -> q_gen_418
<a>() -> q_gen_419
<b>() -> q_gen_419
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<cons, cons>(q_gen_403, q_gen_417) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<a, b>() -> q_gen_403
<b, b>() -> q_gen_403
<cons, nil>(q_gen_419, q_gen_418) -> q_gen_417
<nil, cons>(q_gen_419, q_gen_418) -> q_gen_417
}

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

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

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

-------------------------------------------
Step 21, which took 0.014560 s (model generation: 0.013585,  model checking: 0.000975):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<cons>(q_gen_407, q_gen_406) -> q_gen_406
<nil>() -> q_gen_406
<a>() -> q_gen_407
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, cons>(q_gen_407, q_gen_406) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<a, a, a>() -> q_gen_408
<a, b, a>() -> q_gen_408
<b, a, b>() -> q_gen_408
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403, q_gen_417, q_gen_418, q_gen_419},
Q_f={q_gen_388},
Delta=
{
<nil>() -> q_gen_418
<a>() -> q_gen_419
<b>() -> q_gen_419
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<cons, cons>(q_gen_403, q_gen_417) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<a, b>() -> q_gen_403
<b, b>() -> q_gen_403
<cons, nil>(q_gen_419, q_gen_418) -> q_gen_417
<nil, cons>(q_gen_419, q_gen_418) -> q_gen_417
}

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

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

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

-------------------------------------------
Step 22, which took 0.022510 s (model generation: 0.017299,  model checking: 0.005211):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<cons>(q_gen_407, q_gen_406) -> q_gen_406
<nil>() -> q_gen_406
<a>() -> q_gen_407
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, cons>(q_gen_407, q_gen_406) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<a, a, a>() -> q_gen_408
<a, b, a>() -> q_gen_408
<b, a, b>() -> q_gen_408
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403, q_gen_417, q_gen_418, q_gen_419},
Q_f={q_gen_388},
Delta=
{
<cons>(q_gen_419, q_gen_418) -> q_gen_418
<nil>() -> q_gen_418
<a>() -> q_gen_419
<b>() -> q_gen_419
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<cons, cons>(q_gen_403, q_gen_417) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<a, b>() -> q_gen_403
<b, b>() -> q_gen_403
<cons, nil>(q_gen_419, q_gen_418) -> q_gen_417
<nil, cons>(q_gen_419, q_gen_418) -> q_gen_417
}

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

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

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

-------------------------------------------
Step 23, which took 0.020537 s (model generation: 0.019725,  model checking: 0.000812):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<cons>(q_gen_407, q_gen_406) -> q_gen_406
<nil>() -> q_gen_406
<a>() -> q_gen_407
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, cons>(q_gen_407, q_gen_406) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<a, a, a>() -> q_gen_408
<a, b, a>() -> q_gen_408
<b, a, b>() -> q_gen_408
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403, q_gen_417, q_gen_418, q_gen_419},
Q_f={q_gen_388},
Delta=
{
<cons>(q_gen_419, q_gen_418) -> q_gen_418
<nil>() -> q_gen_418
<a>() -> q_gen_419
<b>() -> q_gen_419
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<cons, cons>(q_gen_403, q_gen_417) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<a, b>() -> q_gen_403
<b, b>() -> q_gen_403
<cons, nil>(q_gen_419, q_gen_418) -> q_gen_417
<nil, cons>(q_gen_419, q_gen_418) -> q_gen_417
}

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

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

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

-------------------------------------------
Step 24, which took 0.026312 s (model generation: 0.020944,  model checking: 0.005368):

Model:
|_
{
append -> 
{{{
Q={q_gen_392, q_gen_394, q_gen_395, q_gen_406, q_gen_407, q_gen_408},
Q_f={q_gen_392},
Delta=
{
<cons>(q_gen_407, q_gen_406) -> q_gen_406
<nil>() -> q_gen_406
<a>() -> q_gen_407
<b>() -> q_gen_407
<cons, cons>(q_gen_395, q_gen_394) -> q_gen_394
<nil, cons>(q_gen_407, q_gen_406) -> q_gen_394
<nil, nil>() -> q_gen_394
<a, a>() -> q_gen_395
<b, a>() -> q_gen_395
<b, b>() -> q_gen_395
<cons, cons, cons>(q_gen_408, q_gen_392) -> q_gen_392
<cons, nil, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_392
<nil, nil, cons>(q_gen_407, q_gen_406) -> q_gen_392
<nil, nil, nil>() -> q_gen_392
<a, a, a>() -> q_gen_408
<a, b, a>() -> q_gen_408
<b, a, b>() -> q_gen_408
<b, b, b>() -> q_gen_408
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_389},
Delta=
{
<cons>(q_gen_391, q_gen_389) -> q_gen_389
<cons>(q_gen_391, q_gen_390) -> q_gen_389
<nil>() -> q_gen_390
<a>() -> q_gen_391
<b>() -> q_gen_391
}

Datatype: <eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_388, q_gen_403, q_gen_417, q_gen_418, q_gen_419},
Q_f={q_gen_388},
Delta=
{
<cons>(q_gen_419, q_gen_418) -> q_gen_418
<nil>() -> q_gen_418
<a>() -> q_gen_419
<b>() -> q_gen_419
<cons, cons>(q_gen_403, q_gen_388) -> q_gen_388
<cons, cons>(q_gen_403, q_gen_417) -> q_gen_388
<nil, nil>() -> q_gen_388
<a, a>() -> q_gen_403
<a, b>() -> q_gen_403
<b, a>() -> q_gen_403
<b, b>() -> q_gen_403
<cons, nil>(q_gen_419, q_gen_418) -> q_gen_417
<nil, cons>(q_gen_419, q_gen_418) -> q_gen_417
}

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

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

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

Total time: 0.333148
Reason for stopping: Proved