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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)])}
(append([_sda, _tda, _uda]) /\ append([_sda, _tda, _vda])) -> eq_eltlist([_uda, _vda])
)
(reverse, F:
{() -> reverse([nil, nil])
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda])}
(reverse([_yda, _aea]) /\ reverse([_yda, _zda])) -> eq_eltlist([_zda, _aea])
)
(leq, P:
{() -> leq([z, s(nn2)])
() -> leq([z, z])
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)])
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2])
(leq([s(nn1), z])) -> BOT}
)
(length, F:
{() -> length([nil, z])
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)])}
(length([_cea, _dea]) /\ length([_cea, _eea])) -> eq_nat([_dea, _eea])
)
}

properties:
{(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]), (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 0
() -> reverse([nil, nil]) -> 0
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 0
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 0
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 0
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 0
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 0
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0
(leq([s(nn1), z])) -> BOT -> 0
}


Solving took 8.625602 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5878, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888, q_gen_5922, q_gen_5929},
Q_f={q_gen_5861, q_gen_5878},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons>(q_gen_5881, q_gen_5922) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<a, b>() -> q_gen_5867
<b, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5929
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5929
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5929) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5878) -> q_gen_5878
<cons, cons, cons>(q_gen_5882, q_gen_5888) -> q_gen_5878
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5878
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5878
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.011534 s (model generation: 0.010783,  model checking: 0.000751):

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

}

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 0
() -> reverse([nil, nil]) -> 3
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 1
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 1
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 1
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> reverse([nil, nil]), {

})

-------------------------------------------
Step 1, which took 0.010924 s (model generation: 0.010829,  model checking: 0.000095):

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

}

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 1
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 1
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 1
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([z, z]), {

})

-------------------------------------------
Step 2, which took 0.011041 s (model generation: 0.010886,  model checking: 0.000155):

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

}

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

}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857},
Q_f={q_gen_5857},
Delta=
{
<z, z>() -> q_gen_5857
}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 1
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 1
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 1
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 3, which took 0.011018 s (model generation: 0.010897,  model checking: 0.000121):

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

}

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

}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<z>() -> q_gen_5859
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 1
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 1
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 1
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> length([nil, z]), {

})

-------------------------------------------
Step 4, which took 0.011045 s (model generation: 0.010621,  model checking: 0.000424):

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

}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<z>() -> q_gen_5859
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 1
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 1
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 1
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 5, which took 0.011023 s (model generation: 0.010776,  model checking: 0.000247):

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

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<z>() -> q_gen_5859
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 1
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 1
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 1
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 6, which took 0.011987 s (model generation: 0.010970,  model checking: 0.001017):

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

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 1
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 1
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 1
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((length([ll, _bea])) -> length([cons(x, ll), s(_bea)]), {
_bea -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 7, which took 0.012579 s (model generation: 0.012039,  model checking: 0.000540):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 4
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 2
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 2
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 8, which took 0.014507 s (model generation: 0.013426,  model checking: 0.001081):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867},
Q_f={q_gen_5861},
Delta=
{
<nil, nil>() -> q_gen_5866
<b, b>() -> q_gen_5867
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
() -> reverse([nil, nil]) -> 4
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 2
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 4
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 3
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 3
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3
(leq([s(nn1), z])) -> BOT -> 3
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 9, which took 0.014708 s (model generation: 0.013445,  model checking: 0.001263):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867},
Q_f={q_gen_5861},
Delta=
{
<nil, nil>() -> q_gen_5866
<b, b>() -> q_gen_5867
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
() -> reverse([nil, nil]) -> 4
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 3
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 4
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 4
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 4
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 10, which took 0.014170 s (model generation: 0.013880,  model checking: 0.000290):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867},
Q_f={q_gen_5861},
Delta=
{
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
() -> reverse([nil, nil]) -> 4
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 6
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 4
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 4
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 4
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
}
Sat witness: Found: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), {
_wda -> nil  ;  _xda -> cons(b, nil)  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.014525 s (model generation: 0.013830,  model checking: 0.000695):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867},
Q_f={q_gen_5861},
Delta=
{
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875},
Q_f={q_gen_5856},
Delta=
{
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<b, b>() -> q_gen_5875
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
() -> reverse([nil, nil]) -> 4
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 6
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 4
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 4
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 4
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5
(leq([s(nn1), z])) -> BOT -> 5
}
Sat witness: Found: ((length([ll, _bea])) -> length([cons(x, ll), s(_bea)]), {
_bea -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 12, which took 0.017401 s (model generation: 0.014673,  model checking: 0.002728):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867},
Q_f={q_gen_5861},
Delta=
{
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875},
Q_f={q_gen_5856},
Delta=
{
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<b, b>() -> q_gen_5875
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
() -> reverse([nil, nil]) -> 4
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 6
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 7
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 5
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 5
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5
(leq([s(nn1), z])) -> BOT -> 5
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.017908 s (model generation: 0.016422,  model checking: 0.001486):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875},
Q_f={q_gen_5856},
Delta=
{
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<b, b>() -> q_gen_5875
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 5
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 5
() -> reverse([nil, nil]) -> 5
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 9
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 7
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 6
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 6
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 6
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6
(leq([s(nn1), z])) -> BOT -> 6
}
Sat witness: Found: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), {
_wda -> nil  ;  _xda -> cons(a, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.020312 s (model generation: 0.017170,  model checking: 0.003142):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875},
Q_f={q_gen_5856},
Delta=
{
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> length([nil, z]) -> 6
() -> leq([z, s(nn2)]) -> 7
() -> leq([z, z]) -> 6
() -> reverse([nil, nil]) -> 6
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 9
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 10
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 7
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 7
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 8
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 7
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.019646 s (model generation: 0.017284,  model checking: 0.002362):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875},
Q_f={q_gen_5856},
Delta=
{
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> length([nil, z]) -> 7
() -> leq([z, s(nn2)]) -> 8
() -> leq([z, z]) -> 7
() -> reverse([nil, nil]) -> 7
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 12
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 10
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 8
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 8
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 9
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8
(leq([s(nn1), z])) -> BOT -> 8
}
Sat witness: Found: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), {
_wda -> nil  ;  _xda -> cons(b, cons(b, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 0.019746 s (model generation: 0.018829,  model checking: 0.000917):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> length([nil, z]) -> 8
() -> leq([z, s(nn2)]) -> 8
() -> leq([z, z]) -> 8
() -> reverse([nil, nil]) -> 8
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 12
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 10
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 8
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 11
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 9
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9
(leq([s(nn1), z])) -> BOT -> 9
}
Sat witness: Found: ((length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]), {
_iea -> cons(b, nil)  ;  _jea -> s(z)  ;  _kea -> z  ;  l1 -> nil
})

-------------------------------------------
Step 17, which took 0.019912 s (model generation: 0.018826,  model checking: 0.001086):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<s, z>(q_gen_5859) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> length([nil, z]) -> 9
() -> leq([z, s(nn2)]) -> 9
() -> leq([z, z]) -> 9
() -> reverse([nil, nil]) -> 9
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 12
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 10
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 9
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 11
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 9
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9
(leq([s(nn1), z])) -> BOT -> 12
}
Sat witness: Found: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 18, which took 0.023651 s (model generation: 0.018763,  model checking: 0.004888):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5890, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<cons, cons>(q_gen_5875, q_gen_5890) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5890
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> length([nil, z]) -> 10
() -> leq([z, s(nn2)]) -> 10
() -> leq([z, z]) -> 10
() -> reverse([nil, nil]) -> 10
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 12
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 13
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 10
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 11
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 10
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 12
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.024423 s (model generation: 0.021459,  model checking: 0.002964):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<a, b, a>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5890, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<cons, cons>(q_gen_5875, q_gen_5890) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5890
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> length([nil, z]) -> 11
() -> leq([z, s(nn2)]) -> 11
() -> leq([z, z]) -> 11
() -> reverse([nil, nil]) -> 11
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 12
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 13
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 11
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 14
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 11
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11
(leq([s(nn1), z])) -> BOT -> 12
}
Sat witness: Found: ((length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]), {
_iea -> cons(b, cons(b, nil))  ;  _jea -> s(s(z))  ;  _kea -> s(z)  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 20, which took 0.023008 s (model generation: 0.022795,  model checking: 0.000213):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<a, b, a>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5890, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<cons, cons>(q_gen_5875, q_gen_5890) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5890
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> length([nil, z]) -> 11
() -> leq([z, s(nn2)]) -> 11
() -> leq([z, z]) -> 11
() -> reverse([nil, nil]) -> 11
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 12
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 13
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 11
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 14
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 11
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14
(leq([s(nn1), z])) -> BOT -> 12
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> z
})

-------------------------------------------
Step 21, which took 0.023665 s (model generation: 0.022140,  model checking: 0.001525):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5871, q_gen_5873, q_gen_5880, q_gen_5881, q_gen_5882},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5871
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5871) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5873) -> q_gen_5873
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5873
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5873
<a, b, a>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5874, q_gen_5875, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<b>() -> q_gen_5892
<nil, nil>() -> q_gen_5856
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5874
<cons, cons>(q_gen_5875, q_gen_5874) -> q_gen_5874
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5874
<a, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> length([nil, z]) -> 12
() -> leq([z, s(nn2)]) -> 12
() -> leq([z, z]) -> 12
() -> reverse([nil, nil]) -> 12
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 12
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 13
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 12
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 14
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 12
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14
(leq([s(nn1), z])) -> BOT -> 12
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 22, which took 0.023801 s (model generation: 0.021333,  model checking: 0.002468):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, b, a>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> length([nil, z]) -> 12
() -> leq([z, s(nn2)]) -> 12
() -> leq([z, z]) -> 12
() -> reverse([nil, nil]) -> 12
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 15
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 13
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 13
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 14
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14
(leq([s(nn1), z])) -> BOT -> 13
}
Sat witness: Found: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), {
_wda -> cons(a, nil)  ;  _xda -> cons(a, cons(b, nil))  ;  h1 -> b  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 23, which took 0.031133 s (model generation: 0.023133,  model checking: 0.008000):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, b, a>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> length([nil, z]) -> 13
() -> leq([z, s(nn2)]) -> 13
() -> leq([z, z]) -> 13
() -> reverse([nil, nil]) -> 13
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 15
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 16
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 14
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 14
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 14
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14
(leq([s(nn1), z])) -> BOT -> 14
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 24, which took 0.027923 s (model generation: 0.026874,  model checking: 0.001049):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<a, b, a>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5863, q_gen_5864, q_gen_5896},
Q_f={q_gen_5860, q_gen_5863},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<nil, z>() -> q_gen_5860
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5863
<cons, s>(q_gen_5864, q_gen_5863) -> q_gen_5896
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5890, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<cons, cons>(q_gen_5875, q_gen_5890) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5890
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> length([nil, z]) -> 14
() -> leq([z, s(nn2)]) -> 14
() -> leq([z, z]) -> 14
() -> reverse([nil, nil]) -> 14
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 15
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 16
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 14
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 14
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 17
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 15
(leq([s(nn1), z])) -> BOT -> 15
}
Sat witness: Found: ((length([ll, _bea])) -> length([cons(x, ll), s(_bea)]), {
_bea -> s(z)  ;  ll -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 25, which took 0.032771 s (model generation: 0.027073,  model checking: 0.005698):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, b, a>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> length([nil, z]) -> 15
() -> leq([z, s(nn2)]) -> 15
() -> leq([z, z]) -> 15
() -> reverse([nil, nil]) -> 15
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 18
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 16
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 15
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 15
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 17
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 16
(leq([s(nn1), z])) -> BOT -> 16
}
Sat witness: Found: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), {
_wda -> cons(b, nil)  ;  _xda -> cons(b, nil)  ;  h1 -> b  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 26, which took 0.031174 s (model generation: 0.030630,  model checking: 0.000544):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<a, b, a>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> length([nil, z]) -> 15
() -> leq([z, s(nn2)]) -> 15
() -> leq([z, z]) -> 15
() -> reverse([nil, nil]) -> 15
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 18
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 16
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 18
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 16
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 17
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 16
(leq([s(nn1), z])) -> BOT -> 16
}
Sat witness: Found: ((length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]), {
_fea -> s(z)  ;  _gea -> nil  ;  _hea -> z  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 27, which took 0.044390 s (model generation: 0.032793,  model checking: 0.011597):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, b, a>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> length([nil, z]) -> 16
() -> leq([z, s(nn2)]) -> 16
() -> leq([z, z]) -> 16
() -> reverse([nil, nil]) -> 16
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 18
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 19
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 18
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 17
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 17
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17
(leq([s(nn1), z])) -> BOT -> 17
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 28, which took 0.052275 s (model generation: 0.034891,  model checking: 0.017384):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17
() -> length([nil, z]) -> 17
() -> leq([z, s(nn2)]) -> 17
() -> leq([z, z]) -> 17
() -> reverse([nil, nil]) -> 17
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 19
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 22
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 19
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 18
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 18
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 18
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 18
(leq([s(nn1), z])) -> BOT -> 18
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 29, which took 0.110930 s (model generation: 0.039281,  model checking: 0.071649):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18
() -> length([nil, z]) -> 18
() -> leq([z, s(nn2)]) -> 18
() -> leq([z, z]) -> 18
() -> reverse([nil, nil]) -> 18
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 20
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 25
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 20
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 19
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 19
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 19
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19
(leq([s(nn1), z])) -> BOT -> 19
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(a, cons(b, cons(b, nil)))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 30, which took 0.047383 s (model generation: 0.037930,  model checking: 0.009453):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5865, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888},
Q_f={q_gen_5861, q_gen_5865},
Delta=
{
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5880
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5865) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5865
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5865
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5888
<cons, cons, cons>(q_gen_5882, q_gen_5888) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
() -> length([nil, z]) -> 19
() -> leq([z, s(nn2)]) -> 19
() -> leq([z, z]) -> 19
() -> reverse([nil, nil]) -> 19
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 23
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 25
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 21
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 20
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 20
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 20
(leq([s(nn1), z])) -> BOT -> 20
}
Sat witness: Found: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), {
_wda -> cons(a, nil)  ;  _xda -> cons(a, cons(b, cons(b, nil)))  ;  h1 -> b  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 31, which took 0.046217 s (model generation: 0.043072,  model checking: 0.003145):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882},
Q_f={q_gen_5861},
Delta=
{
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5880
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5863, q_gen_5864, q_gen_5877, q_gen_5896},
Q_f={q_gen_5860, q_gen_5863},
Delta=
{
<b>() -> q_gen_5864
<a>() -> q_gen_5877
<cons, s>(q_gen_5877, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5863
<cons, s>(q_gen_5864, q_gen_5863) -> q_gen_5896
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5890, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<cons, cons>(q_gen_5875, q_gen_5890) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5890
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5890
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20
() -> length([nil, z]) -> 20
() -> leq([z, s(nn2)]) -> 20
() -> leq([z, z]) -> 20
() -> reverse([nil, nil]) -> 20
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 23
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 25
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 21
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 20
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 23
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 21
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21
(leq([s(nn1), z])) -> BOT -> 21
}
Sat witness: Found: ((length([ll, _bea])) -> length([cons(x, ll), s(_bea)]), {
_bea -> s(z)  ;  ll -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 32, which took 0.031230 s (model generation: 0.030688,  model checking: 0.000542):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888},
Q_f={q_gen_5861},
Delta=
{
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5880
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<cons, cons, cons>(q_gen_5882, q_gen_5888) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5890, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5890) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5890
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20
() -> length([nil, z]) -> 20
() -> leq([z, s(nn2)]) -> 20
() -> leq([z, z]) -> 20
() -> reverse([nil, nil]) -> 20
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 23
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 25
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 21
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 23
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 23
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 21
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21
(leq([s(nn1), z])) -> BOT -> 21
}
Sat witness: Found: ((length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]), {
_iea -> cons(b, cons(b, cons(b, nil)))  ;  _jea -> s(s(s(z)))  ;  _kea -> s(s(z))  ;  l1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 33, which took 0.177251 s (model generation: 0.052174,  model checking: 0.125077):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5922},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 21
() -> length([nil, z]) -> 21
() -> leq([z, s(nn2)]) -> 21
() -> leq([z, z]) -> 21
() -> reverse([nil, nil]) -> 21
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 24
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 28
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 22
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 24
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 24
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 22
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22
(leq([s(nn1), z])) -> BOT -> 22
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 34, which took 0.021567 s (model generation: 0.019268,  model checking: 0.002299):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5922},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> length([nil, z]) -> 22
() -> leq([z, s(nn2)]) -> 22
() -> leq([z, z]) -> 22
() -> reverse([nil, nil]) -> 22
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 27
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 28
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 23
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 25
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 25
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 23
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23
(leq([s(nn1), z])) -> BOT -> 23
}
Sat witness: Found: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), {
_wda -> nil  ;  _xda -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 35, which took 0.074739 s (model generation: 0.071063,  model checking: 0.003676):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5922},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23
() -> length([nil, z]) -> 23
() -> leq([z, s(nn2)]) -> 23
() -> leq([z, z]) -> 23
() -> reverse([nil, nil]) -> 23
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 28
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 31
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 24
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 26
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 26
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 24
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 24
(leq([s(nn1), z])) -> BOT -> 24
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 36, which took 0.077518 s (model generation: 0.076098,  model checking: 0.001420):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887},
Q_f={q_gen_5861},
Delta=
{
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5880
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892, q_gen_5901, q_gen_5909},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<cons, cons>(q_gen_5875, q_gen_5909) -> q_gen_5856
<cons, cons>(q_gen_5901, q_gen_5856) -> q_gen_5856
<cons, cons>(q_gen_5901, q_gen_5889) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
<b, a>() -> q_gen_5901
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5909
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24
() -> length([nil, z]) -> 24
() -> leq([z, s(nn2)]) -> 24
() -> leq([z, z]) -> 24
() -> reverse([nil, nil]) -> 24
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 28
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 31
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 27
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 26
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 26
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 25
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 25
(leq([s(nn1), z])) -> BOT -> 25
}
Sat witness: Found: ((length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]), {
_fea -> s(s(z))  ;  _gea -> cons(b, nil)  ;  _hea -> s(z)  ;  l1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 37, which took 0.078824 s (model generation: 0.075225,  model checking: 0.003599):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5921, q_gen_5922},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<cons, cons, cons>(q_gen_5882, q_gen_5921) -> q_gen_5879
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5921
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 25
() -> length([nil, z]) -> 25
() -> leq([z, s(nn2)]) -> 25
() -> leq([z, z]) -> 25
() -> reverse([nil, nil]) -> 25
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 31
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 31
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 28
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 27
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 27
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 26
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 26
(leq([s(nn1), z])) -> BOT -> 26
}
Sat witness: Found: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), {
_wda -> cons(b, cons(b, nil))  ;  _xda -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> b  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 38, which took 0.084745 s (model generation: 0.083736,  model checking: 0.001009):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887},
Q_f={q_gen_5861},
Delta=
{
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5880
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5874, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892, q_gen_5900},
Q_f={q_gen_5856, q_gen_5874},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5900, q_gen_5874) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5874
<cons, cons>(q_gen_5900, q_gen_5889) -> q_gen_5874
<a, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5874) -> q_gen_5889
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, cons>(q_gen_5900, q_gen_5856) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
<a, b>() -> q_gen_5900
<b, a>() -> q_gen_5900
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26
() -> length([nil, z]) -> 26
() -> leq([z, s(nn2)]) -> 26
() -> leq([z, z]) -> 26
() -> reverse([nil, nil]) -> 26
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 31
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 31
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 28
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 30
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 28
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 27
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 27
(leq([s(nn1), z])) -> BOT -> 27
}
Sat witness: Found: ((length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]), {
_iea -> cons(a, cons(b, nil))  ;  _jea -> s(s(z))  ;  _kea -> s(z)  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 39, which took 0.106884 s (model generation: 0.105532,  model checking: 0.001352):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5917, q_gen_5922},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, cons, cons>(q_gen_5917, q_gen_5861) -> q_gen_5861
<cons, cons, cons>(q_gen_5917, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<a, a, a>() -> q_gen_5917
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27
() -> length([nil, z]) -> 27
() -> leq([z, s(nn2)]) -> 27
() -> leq([z, z]) -> 27
() -> reverse([nil, nil]) -> 27
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 31
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 34
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 29
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 31
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 29
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 28
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 28
(leq([s(nn1), z])) -> BOT -> 28
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 40, which took 0.105837 s (model generation: 0.105078,  model checking: 0.000759):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5922},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892, q_gen_5933},
Q_f={q_gen_5856},
Delta=
{
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5933
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, cons>(q_gen_5892, q_gen_5933) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 28
() -> length([nil, z]) -> 28
() -> leq([z, s(nn2)]) -> 28
() -> leq([z, z]) -> 28
() -> reverse([nil, nil]) -> 28
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 31
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 34
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 30
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 34
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 30
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 29
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 29
(leq([s(nn1), z])) -> BOT -> 29
}
Sat witness: Found: ((length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]), {
_iea -> cons(b, cons(b, nil))  ;  _jea -> s(s(z))  ;  _kea -> z  ;  l1 -> nil
})

-------------------------------------------
Step 41, which took 0.107280 s (model generation: 0.103012,  model checking: 0.004268):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5922, q_gen_5929},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5929
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5929) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 29
() -> length([nil, z]) -> 29
() -> leq([z, s(nn2)]) -> 29
() -> leq([z, z]) -> 29
() -> reverse([nil, nil]) -> 29
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 32
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 37
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 31
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 35
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 31
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 30
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 30
(leq([s(nn1), z])) -> BOT -> 30
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, cons(b, nil)))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 42, which took 0.110360 s (model generation: 0.109114,  model checking: 0.001246):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5915, q_gen_5922},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, cons, cons>(q_gen_5915, q_gen_5861) -> q_gen_5861
<cons, cons, cons>(q_gen_5915, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, b, a>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<a, a, a>() -> q_gen_5915
<b, a, b>() -> q_gen_5915
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 30
() -> length([nil, z]) -> 30
() -> leq([z, s(nn2)]) -> 30
() -> leq([z, z]) -> 30
() -> reverse([nil, nil]) -> 30
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 35
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 37
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 32
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 35
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 32
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 31
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 31
(leq([s(nn1), z])) -> BOT -> 31
}
Sat witness: Found: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), {
_wda -> cons(b, nil)  ;  _xda -> cons(b, nil)  ;  h1 -> a  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 43, which took 0.137184 s (model generation: 0.136191,  model checking: 0.000993):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5865, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888},
Q_f={q_gen_5861, q_gen_5865},
Delta=
{
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5880
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5865) -> q_gen_5865
<cons, cons, cons>(q_gen_5882, q_gen_5888) -> q_gen_5865
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5865
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5865
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5865
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5874, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892, q_gen_5900},
Q_f={q_gen_5856, q_gen_5874},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5900, q_gen_5856) -> q_gen_5856
<cons, cons>(q_gen_5900, q_gen_5889) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5874
<a, a>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5874) -> q_gen_5889
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
<a, b>() -> q_gen_5900
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 31
() -> length([nil, z]) -> 31
() -> leq([z, s(nn2)]) -> 31
() -> leq([z, z]) -> 31
() -> reverse([nil, nil]) -> 31
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 35
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 37
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 35
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 35
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 33
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 32
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 32
(leq([s(nn1), z])) -> BOT -> 32
}
Sat witness: Found: ((length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]), {
_fea -> s(s(s(z)))  ;  _gea -> cons(b, cons(b, nil))  ;  _hea -> s(s(z))  ;  l1 -> cons(b, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 44, which took 0.180153 s (model generation: 0.178933,  model checking: 0.001220):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5886, q_gen_5887, q_gen_5895, q_gen_5922},
Q_f={q_gen_5861, q_gen_5886},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, cons, cons>(q_gen_5895, q_gen_5879) -> q_gen_5861
<cons, cons, cons>(q_gen_5895, q_gen_5886) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<cons, cons, cons>(q_gen_5882, q_gen_5886) -> q_gen_5879
<cons, cons, cons>(q_gen_5895, q_gen_5861) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5886
<a, a, a>() -> q_gen_5895
<a, b, a>() -> q_gen_5895
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 32
() -> length([nil, z]) -> 32
() -> leq([z, s(nn2)]) -> 32
() -> leq([z, z]) -> 32
() -> reverse([nil, nil]) -> 32
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 38
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 37
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 36
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 36
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 34
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 33
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 33
(leq([s(nn1), z])) -> BOT -> 33
}
Sat witness: Found: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), {
_wda -> cons(a, cons(b, nil))  ;  _xda -> cons(a, cons(b, cons(b, cons(b, nil))))  ;  h1 -> a  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 45, which took 0.188666 s (model generation: 0.187614,  model checking: 0.001052):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5871, q_gen_5872, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5883},
Q_f={q_gen_5861},
Delta=
{
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5880
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<nil, nil>() -> q_gen_5866
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5871) -> q_gen_5871
<cons, cons>(q_gen_5872, q_gen_5866) -> q_gen_5871
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5871
<a, a>() -> q_gen_5872
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5871) -> q_gen_5861
<cons, nil, cons>(q_gen_5872, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5872, q_gen_5871) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<cons, cons, cons>(q_gen_5882, q_gen_5883) -> q_gen_5883
<nil, cons, cons>(q_gen_5867, q_gen_5871) -> q_gen_5883
<nil, cons, cons>(q_gen_5872, q_gen_5866) -> q_gen_5883
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5874, q_gen_5875, q_gen_5884, q_gen_5885, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856, q_gen_5874},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<nil, nil>() -> q_gen_5856
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5874
<cons, cons>(q_gen_5885, q_gen_5884) -> q_gen_5874
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5874) -> q_gen_5884
<cons, cons>(q_gen_5875, q_gen_5884) -> q_gen_5884
<cons, cons>(q_gen_5885, q_gen_5856) -> q_gen_5884
<cons, cons>(q_gen_5885, q_gen_5874) -> q_gen_5884
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5884
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5884
<a, a>() -> q_gen_5885
<a, b>() -> q_gen_5885
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 35
() -> length([nil, z]) -> 33
() -> leq([z, s(nn2)]) -> 33
() -> leq([z, z]) -> 33
() -> reverse([nil, nil]) -> 33
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 38
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 37
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 36
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 36
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 34
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 33
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 33
(leq([s(nn1), z])) -> BOT -> 33
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 46, which took 0.161022 s (model generation: 0.159900,  model checking: 0.001122):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888},
Q_f={q_gen_5861},
Delta=
{
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5880
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5888) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5874, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892, q_gen_5899, q_gen_5900},
Q_f={q_gen_5856, q_gen_5874},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<nil, nil>() -> q_gen_5856
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5874
<cons, cons>(q_gen_5900, q_gen_5899) -> q_gen_5874
<a, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5874) -> q_gen_5889
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
<cons, cons>(q_gen_5875, q_gen_5899) -> q_gen_5899
<cons, cons>(q_gen_5900, q_gen_5856) -> q_gen_5899
<cons, cons>(q_gen_5900, q_gen_5889) -> q_gen_5899
<a, b>() -> q_gen_5900
<b, a>() -> q_gen_5900
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 36
() -> length([nil, z]) -> 34
() -> leq([z, s(nn2)]) -> 34
() -> leq([z, z]) -> 34
() -> reverse([nil, nil]) -> 34
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 38
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 37
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 36
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 39
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 35
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 34
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 34
(leq([s(nn1), z])) -> BOT -> 34
}
Sat witness: Found: ((length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]), {
_iea -> cons(a, cons(b, cons(b, nil)))  ;  _jea -> s(s(s(z)))  ;  _kea -> s(s(z))  ;  l1 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 47, which took 0.180497 s (model generation: 0.179616,  model checking: 0.000881):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5871, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5922, q_gen_5929},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5871
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5871
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5929
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5929) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5871) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<cons, nil, cons>(q_gen_5867, q_gen_5871) -> q_gen_5879
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 39
() -> length([nil, z]) -> 35
() -> leq([z, s(nn2)]) -> 35
() -> leq([z, z]) -> 35
() -> reverse([nil, nil]) -> 35
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 38
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 37
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 37
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 39
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 36
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 35
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 35
(leq([s(nn1), z])) -> BOT -> 35
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 48, which took 0.204564 s (model generation: 0.179941,  model checking: 0.024623):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5865, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888, q_gen_5922, q_gen_5929},
Q_f={q_gen_5861, q_gen_5865},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5929
<cons, nil, cons>(q_gen_5867, q_gen_5929) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5865) -> q_gen_5865
<cons, cons, cons>(q_gen_5882, q_gen_5888) -> q_gen_5865
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5865
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5865
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5865
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5865
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 39
() -> length([nil, z]) -> 36
() -> leq([z, s(nn2)]) -> 36
() -> leq([z, z]) -> 36
() -> reverse([nil, nil]) -> 36
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 38
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 40
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 38
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 39
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 37
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 36
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 36
(leq([s(nn1), z])) -> BOT -> 36
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(a, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 49, which took 0.156455 s (model generation: 0.155312,  model checking: 0.001143):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5865, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888, q_gen_5922, q_gen_5929},
Q_f={q_gen_5861, q_gen_5865},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5929
<cons, cons, cons>(q_gen_5882, q_gen_5865) -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5888) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5929) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5865
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5865
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5865
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 39
() -> length([nil, z]) -> 37
() -> leq([z, s(nn2)]) -> 37
() -> leq([z, z]) -> 37
() -> reverse([nil, nil]) -> 37
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 41
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 40
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 39
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 39
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 38
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 37
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 37
(leq([s(nn1), z])) -> BOT -> 37
}
Sat witness: Found: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), {
_wda -> cons(a, cons(b, nil))  ;  _xda -> cons(a, cons(b, nil))  ;  h1 -> a  ;  t1 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 50, which took 0.242865 s (model generation: 0.242756,  model checking: 0.000109):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888},
Q_f={q_gen_5861},
Delta=
{
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5880
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5888) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893, q_gen_5897},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<s, s>(q_gen_5897) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, z>(q_gen_5859) -> q_gen_5893
<s, s>(q_gen_5893) -> q_gen_5897
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5890, q_gen_5891, q_gen_5892, q_gen_5900},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5856
<cons, cons>(q_gen_5900, q_gen_5889) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5890) -> q_gen_5889
<cons, cons>(q_gen_5900, q_gen_5856) -> q_gen_5889
<cons, cons>(q_gen_5900, q_gen_5890) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5890
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5890
<a, b>() -> q_gen_5900
<b, a>() -> q_gen_5900
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 39
() -> length([nil, z]) -> 37
() -> leq([z, s(nn2)]) -> 37
() -> leq([z, z]) -> 37
() -> reverse([nil, nil]) -> 37
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 41
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 40
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 39
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 39
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 38
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 37
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 40
(leq([s(nn1), z])) -> BOT -> 38
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(s(z))  ;  nn2 -> s(z)
})

-------------------------------------------
Step 51, which took 0.195133 s (model generation: 0.187266,  model checking: 0.007867):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5870, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888, q_gen_5922, q_gen_5929},
Q_f={q_gen_5861, q_gen_5870},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<b, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5929
<cons, cons, cons>(q_gen_5882, q_gen_5870) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5929) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5888) -> q_gen_5870
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5870
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5870
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5870
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 40
() -> length([nil, z]) -> 38
() -> leq([z, s(nn2)]) -> 38
() -> leq([z, z]) -> 38
() -> reverse([nil, nil]) -> 38
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 41
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 43
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 40
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 40
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 39
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 38
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 41
(leq([s(nn1), z])) -> BOT -> 39
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 52, which took 0.263541 s (model generation: 0.261392,  model checking: 0.002149):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5871, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5922, q_gen_5929},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<a, b>() -> q_gen_5867
<b, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5871
<cons, cons>(q_gen_5867, q_gen_5871) -> q_gen_5871
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5871
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5929
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5929) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5871) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<cons, nil, cons>(q_gen_5867, q_gen_5871) -> q_gen_5879
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 41
() -> length([nil, z]) -> 39
() -> leq([z, s(nn2)]) -> 39
() -> leq([z, z]) -> 39
() -> reverse([nil, nil]) -> 39
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 44
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 43
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 41
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 41
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 40
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 39
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 42
(leq([s(nn1), z])) -> BOT -> 40
}
Sat witness: Found: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), {
_wda -> cons(a, cons(b, cons(b, nil)))  ;  _xda -> cons(a, cons(b, cons(b, nil)))  ;  h1 -> b  ;  t1 -> cons(a, cons(a, cons(a, nil)))
})

-------------------------------------------
Step 53, which took 0.259132 s (model generation: 0.243040,  model checking: 0.016092):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5878, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888, q_gen_5922, q_gen_5929},
Q_f={q_gen_5861, q_gen_5878},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<a, b>() -> q_gen_5867
<b, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5929
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5929) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5878) -> q_gen_5878
<cons, cons, cons>(q_gen_5882, q_gen_5888) -> q_gen_5878
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5878
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5878
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 42
() -> length([nil, z]) -> 40
() -> leq([z, s(nn2)]) -> 40
() -> leq([z, z]) -> 40
() -> reverse([nil, nil]) -> 40
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 44
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 46
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 42
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 42
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 41
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 40
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 43
(leq([s(nn1), z])) -> BOT -> 41
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 54, which took 0.391452 s (model generation: 0.375573,  model checking: 0.015879):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5870, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888, q_gen_5922, q_gen_5929},
Q_f={q_gen_5861, q_gen_5870},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons>(q_gen_5881, q_gen_5922) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<a, b>() -> q_gen_5867
<b, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5929
<cons, cons, cons>(q_gen_5882, q_gen_5870) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5929) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5888) -> q_gen_5870
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5870
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5870
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5870
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 43
() -> length([nil, z]) -> 41
() -> leq([z, s(nn2)]) -> 41
() -> leq([z, z]) -> 41
() -> reverse([nil, nil]) -> 41
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 45
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 49
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 43
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 43
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 42
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 41
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 44
(leq([s(nn1), z])) -> BOT -> 42
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(b, cons(a, cons(a, cons(b, cons(b, nil)))))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, cons(a, cons(b, nil))))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 55, which took 0.388977 s (model generation: 0.346037,  model checking: 0.042940):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5870, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888, q_gen_5922, q_gen_5929},
Q_f={q_gen_5861, q_gen_5870},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons>(q_gen_5881, q_gen_5922) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<a, b>() -> q_gen_5867
<b, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5929
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5929
<cons, cons, cons>(q_gen_5882, q_gen_5870) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5929) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5888) -> q_gen_5870
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5870
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5870
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5870
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 44
() -> length([nil, z]) -> 42
() -> leq([z, s(nn2)]) -> 42
() -> leq([z, z]) -> 42
() -> reverse([nil, nil]) -> 42
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 46
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 52
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 44
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 44
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 43
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 42
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 45
(leq([s(nn1), z])) -> BOT -> 43
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 56, which took 1.628608 s (model generation: 1.625567,  model checking: 0.003041):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5905, q_gen_5922, q_gen_5929},
Q_f={q_gen_5861},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons>(q_gen_5881, q_gen_5922) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<a, b>() -> q_gen_5867
<b, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5905
<cons, cons>(q_gen_5867, q_gen_5905) -> q_gen_5905
<cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5905
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5929
<cons, cons, cons>(q_gen_5882, q_gen_5879) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5929) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5905) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5879
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<cons, nil, cons>(q_gen_5867, q_gen_5905) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5879
<nil, cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5879
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5879
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 45
() -> length([nil, z]) -> 43
() -> leq([z, s(nn2)]) -> 43
() -> leq([z, z]) -> 43
() -> reverse([nil, nil]) -> 43
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 49
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 52
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 45
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 45
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 44
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 43
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 46
(leq([s(nn1), z])) -> BOT -> 44
}
Sat witness: Found: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), {
_wda -> cons(b, cons(a, cons(a, cons(b, nil))))  ;  _xda -> cons(b, cons(a, cons(a, cons(b, cons(b, cons(b, nil))))))  ;  h1 -> a  ;  t1 -> cons(b, cons(a, cons(a, cons(b, nil))))
})

-------------------------------------------
Step 57, which took 0.933904 s (model generation: 0.932846,  model checking: 0.001058):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5878, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888, q_gen_5922, q_gen_5929},
Q_f={q_gen_5861, q_gen_5878},
Delta=
{
<cons>(q_gen_5881, q_gen_5922) -> q_gen_5880
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<a, b>() -> q_gen_5867
<b, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5929
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5929
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5929) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5878) -> q_gen_5878
<cons, cons, cons>(q_gen_5882, q_gen_5888) -> q_gen_5878
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5878
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5878
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 46
() -> length([nil, z]) -> 44
() -> leq([z, s(nn2)]) -> 44
() -> leq([z, z]) -> 44
() -> reverse([nil, nil]) -> 44
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 52
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 52
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 46
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 46
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 45
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 44
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 47
(leq([s(nn1), z])) -> BOT -> 45
}
Sat witness: Found: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), {
_wda -> cons(b, nil)  ;  _xda -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> b  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 58, which took 0.738826 s (model generation: 0.705864,  model checking: 0.032962):

Model:
|_
{
append -> 
{{{
Q={q_gen_5861, q_gen_5866, q_gen_5867, q_gen_5878, q_gen_5880, q_gen_5881, q_gen_5882, q_gen_5887, q_gen_5888, q_gen_5922, q_gen_5929},
Q_f={q_gen_5861, q_gen_5878},
Delta=
{
<nil>() -> q_gen_5880
<a>() -> q_gen_5881
<b>() -> q_gen_5881
<cons>(q_gen_5881, q_gen_5880) -> q_gen_5922
<cons>(q_gen_5881, q_gen_5922) -> q_gen_5922
<cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5866
<cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5866
<nil, nil>() -> q_gen_5866
<a, a>() -> q_gen_5867
<a, b>() -> q_gen_5867
<b, a>() -> q_gen_5867
<b, b>() -> q_gen_5867
<cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5887
<nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5929
<cons, nil, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<cons, nil, cons>(q_gen_5867, q_gen_5929) -> q_gen_5861
<nil, cons, cons>(q_gen_5867, q_gen_5866) -> q_gen_5861
<nil, nil, cons>(q_gen_5881, q_gen_5922) -> q_gen_5861
<nil, nil, nil>() -> q_gen_5861
<cons, cons, cons>(q_gen_5882, q_gen_5878) -> q_gen_5878
<cons, cons, cons>(q_gen_5882, q_gen_5888) -> q_gen_5878
<cons, nil, cons>(q_gen_5867, q_gen_5887) -> q_gen_5878
<nil, nil, cons>(q_gen_5881, q_gen_5880) -> q_gen_5878
<a, a, a>() -> q_gen_5882
<a, b, a>() -> q_gen_5882
<b, a, b>() -> q_gen_5882
<b, b, b>() -> q_gen_5882
<cons, cons, cons>(q_gen_5882, q_gen_5861) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5887) -> q_gen_5888
<nil, cons, cons>(q_gen_5867, q_gen_5929) -> q_gen_5888
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_5860, q_gen_5864},
Q_f={q_gen_5860},
Delta=
{
<a>() -> q_gen_5864
<b>() -> q_gen_5864
<cons, s>(q_gen_5864, q_gen_5860) -> q_gen_5860
<nil, z>() -> q_gen_5860
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5857, q_gen_5859, q_gen_5893},
Q_f={q_gen_5857},
Delta=
{
<s>(q_gen_5859) -> q_gen_5859
<z>() -> q_gen_5859
<s, s>(q_gen_5857) -> q_gen_5857
<z, s>(q_gen_5859) -> q_gen_5857
<z, z>() -> q_gen_5857
<s, s>(q_gen_5893) -> q_gen_5893
<s, z>(q_gen_5859) -> q_gen_5893
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_5856, q_gen_5875, q_gen_5889, q_gen_5891, q_gen_5892},
Q_f={q_gen_5856},
Delta=
{
<cons>(q_gen_5892, q_gen_5891) -> q_gen_5891
<nil>() -> q_gen_5891
<a>() -> q_gen_5892
<b>() -> q_gen_5892
<cons, cons>(q_gen_5875, q_gen_5856) -> q_gen_5856
<nil, nil>() -> q_gen_5856
<a, a>() -> q_gen_5875
<a, b>() -> q_gen_5875
<b, a>() -> q_gen_5875
<b, b>() -> q_gen_5875
<cons, cons>(q_gen_5875, q_gen_5889) -> q_gen_5889
<cons, nil>(q_gen_5892, q_gen_5891) -> q_gen_5889
<nil, cons>(q_gen_5892, q_gen_5891) -> q_gen_5889
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 47
() -> length([nil, z]) -> 45
() -> leq([z, s(nn2)]) -> 45
() -> leq([z, z]) -> 45
() -> reverse([nil, nil]) -> 45
(append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 52
(append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 55
(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 47
(length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 47
(length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 46
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 45
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 48
(leq([s(nn1), z])) -> BOT -> 46
}
Sat witness: Found: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), {
_rda -> cons(b, cons(a, cons(b, cons(b, cons(b, nil)))))  ;  h1 -> b  ;  l2 -> cons(a, cons(a, cons(b, nil)))  ;  t1 -> nil
})

Total time: 8.625602
Reason for stopping: Proved