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, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)])}
(append([_ge, _he, _ie]) /\ append([_ge, _he, _je])) -> eq_eltlist([_ie, _je])
)
(reverse, F:
{() -> reverse([nil, nil])
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le])}
(reverse([_me, _ne]) /\ reverse([_me, _oe])) -> eq_eltlist([_ne, _oe])
)
(length, F:
{() -> length([nil, z])
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)])}
(length([_qe, _re]) /\ length([_qe, _se])) -> eq_nat([_re, _se])
)
}

properties:
{(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> reverse([nil, nil]) -> 0
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 0
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 0
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 0
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 0
}


Solving took 6.801908 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_878, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888, q_gen_920, q_gen_932},
Q_f={q_gen_864, q_gen_878},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons>(q_gen_881, q_gen_920) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<a, b>() -> q_gen_869
<b, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons>(q_gen_869, q_gen_932) -> q_gen_932
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_932
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_932) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_878) -> q_gen_878
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_878
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_878
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_878
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_932) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.003819 s (model generation: 0.003538,  model checking: 0.000281):

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

}

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

}

Datatype: <eltlist, 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
() -> reverse([nil, nil]) -> 3
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 1
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 1
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 1
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 1
}
Sat witness: Found: (() -> reverse([nil, nil]), {

})

-------------------------------------------
Step 1, which took 0.005912 s (model generation: 0.005850,  model checking: 0.000062):

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

}

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

}

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

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
() -> reverse([nil, nil]) -> 3
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 1
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 1
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 1
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 1
}
Sat witness: Found: (() -> length([nil, z]), {

})

-------------------------------------------
Step 2, which took 0.010861 s (model generation: 0.008276,  model checking: 0.002585):

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

}

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

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

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
() -> reverse([nil, nil]) -> 3
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 1
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 1
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 1
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 3, which took 0.010625 s (model generation: 0.010434,  model checking: 0.000191):

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

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

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

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
() -> reverse([nil, nil]) -> 3
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 1
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 1
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 1
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 4
}
Sat witness: Found: ((length([ll, _pe])) -> length([cons(x, ll), s(_pe)]), {
_pe -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 4, which took 0.011234 s (model generation: 0.010722,  model checking: 0.000512):

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

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

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

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
() -> reverse([nil, nil]) -> 3
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 1
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 4
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 2
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 4
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.014040 s (model generation: 0.010850,  model checking: 0.003190):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869},
Q_f={q_gen_864},
Delta=
{
<nil, nil>() -> q_gen_868
<b, b>() -> q_gen_869
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
}

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

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

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
() -> reverse([nil, nil]) -> 4
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 2
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 4
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 3
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 6, which took 0.011681 s (model generation: 0.011425,  model checking: 0.000256):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869},
Q_f={q_gen_864},
Delta=
{
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
}

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

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

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
() -> reverse([nil, nil]) -> 4
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 5
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 4
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 3
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 4
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> nil  ;  _le -> cons(b, nil)  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.012314 s (model generation: 0.011872,  model checking: 0.000442):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869},
Q_f={q_gen_864},
Delta=
{
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
}

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

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

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
() -> reverse([nil, nil]) -> 4
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 5
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 4
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 4
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 7
}
Sat witness: Found: ((length([ll, _pe])) -> length([cons(x, ll), s(_pe)]), {
_pe -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 8, which took 0.016672 s (model generation: 0.013991,  model checking: 0.002681):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869},
Q_f={q_gen_864},
Delta=
{
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
}

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

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

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
() -> reverse([nil, nil]) -> 4
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 5
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 7
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 5
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 7
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 9, which took 0.013998 s (model generation: 0.013171,  model checking: 0.000827):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<b, b, b>() -> q_gen_882
}

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

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

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
() -> reverse([nil, nil]) -> 5
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 8
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 7
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 6
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 7
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> nil  ;  _le -> cons(a, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.017842 s (model generation: 0.014965,  model checking: 0.002877):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<b, b, b>() -> q_gen_882
}

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

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

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
() -> reverse([nil, nil]) -> 6
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 8
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 10
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 7
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 8
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.017429 s (model generation: 0.014939,  model checking: 0.002490):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<b, b, b>() -> q_gen_882
}

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

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

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
() -> reverse([nil, nil]) -> 7
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 11
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 10
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 8
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 9
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> nil  ;  _le -> cons(b, cons(b, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 0.017081 s (model generation: 0.016570,  model checking: 0.000511):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<b, b>() -> q_gen_875
}

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
() -> reverse([nil, nil]) -> 8
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 11
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 10
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 11
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 9
}
Sat witness: Found: ((length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]), {
_te -> z  ;  _ue -> cons(b, nil)  ;  _ve -> s(z)  ;  l1 -> nil
})

-------------------------------------------
Step 13, which took 0.020952 s (model generation: 0.016423,  model checking: 0.004529):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_890, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_875, q_gen_890) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<b, b>() -> q_gen_875
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_890
}

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
() -> reverse([nil, nil]) -> 9
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 11
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 13
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 11
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 10
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.019445 s (model generation: 0.018094,  model checking: 0.001351):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<a, b, a>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_890, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_875, q_gen_890) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<b, b>() -> q_gen_875
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_890
}

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
() -> reverse([nil, nil]) -> 10
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 11
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 13
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 14
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 11
}
Sat witness: Found: ((length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]), {
_te -> s(z)  ;  _ue -> cons(b, cons(b, nil))  ;  _ve -> s(s(z))  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 15, which took 0.019001 s (model generation: 0.018129,  model checking: 0.000872):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_871, q_gen_873, q_gen_880, q_gen_881, q_gen_882},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<b>() -> q_gen_881
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_871
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_871) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_873) -> q_gen_873
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_873
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_873
<a, b, a>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_874, q_gen_875, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<b>() -> q_gen_892
<nil, nil>() -> q_gen_862
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_874
<cons, cons>(q_gen_875, q_gen_874) -> q_gen_874
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_874
<a, a>() -> q_gen_875
<b, b>() -> q_gen_875
}

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]) -> 13
() -> length([nil, z]) -> 11
() -> reverse([nil, nil]) -> 11
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 11
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 13
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 14
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 11
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 16, which took 0.021806 s (model generation: 0.019150,  model checking: 0.002656):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_887},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_879) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_879
<a, b, a>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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]) -> 13
() -> length([nil, z]) -> 11
() -> reverse([nil, nil]) -> 11
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 14
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 13
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 14
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 12
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(a, nil)  ;  _le -> cons(a, cons(b, nil))  ;  h1 -> b  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 17, which took 0.027637 s (model generation: 0.020115,  model checking: 0.007522):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_887},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_879) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_879
<a, b, a>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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]) -> 13
() -> length([nil, z]) -> 12
() -> reverse([nil, nil]) -> 12
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 14
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 16
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 14
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 13
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 18, which took 0.023095 s (model generation: 0.022512,  model checking: 0.000583):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<a, b, a>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_890, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_875, q_gen_890) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_890
}

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]) -> 13
() -> length([nil, z]) -> 13
() -> reverse([nil, nil]) -> 13
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 14
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 16
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 14
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 16
}
Sat witness: Found: ((length([ll, _pe])) -> length([cons(x, ll), s(_pe)]), {
_pe -> s(z)  ;  ll -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 19, which took 0.029689 s (model generation: 0.024267,  model checking: 0.005422):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<a, b, a>() -> q_gen_882
<b, b, b>() -> q_gen_882
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 14
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 17
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 16
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 15
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 16
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(b, nil)  ;  _le -> cons(b, nil)  ;  h1 -> b  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 20, which took 0.028480 s (model generation: 0.026313,  model checking: 0.002167):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<a, b, a>() -> q_gen_882
<b, b, b>() -> q_gen_882
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 15
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 17
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 16
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 18
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 16
}
Sat witness: Found: ((length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]), {
_te -> s(z)  ;  _ue -> nil  ;  _ve -> z  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 21, which took 0.038460 s (model generation: 0.027630,  model checking: 0.010830):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_887},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_879) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_879
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_879
<a, b, a>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 16
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 17
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 19
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 18
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 17
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 22, which took 0.045074 s (model generation: 0.031163,  model checking: 0.013911):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_887},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_879) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_879
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_879
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 17
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 18
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 22
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 19
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 18
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 0.065822 s (model generation: 0.033533,  model checking: 0.032289):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_887},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_879) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_879
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_879
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 18
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 19
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 25
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 20
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 19
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(a, cons(b, cons(b, nil)))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 24, which took 0.048623 s (model generation: 0.045247,  model checking: 0.003376):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_867, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888},
Q_f={q_gen_864, q_gen_867},
Delta=
{
<cons>(q_gen_881, q_gen_880) -> q_gen_880
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_867) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_867
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_867
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_867
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 19
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 22
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 25
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 20
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 20
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(b, nil)  ;  _le -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> a  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 25, which took 0.051354 s (model generation: 0.049445,  model checking: 0.001909):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882},
Q_f={q_gen_864},
Delta=
{
<cons>(q_gen_881, q_gen_880) -> q_gen_880
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_863, q_gen_865, q_gen_866, q_gen_877, q_gen_895},
Q_f={q_gen_863, q_gen_865},
Delta=
{
<b>() -> q_gen_866
<a>() -> q_gen_877
<cons, s>(q_gen_877, q_gen_863) -> q_gen_863
<nil, z>() -> q_gen_863
<cons, s>(q_gen_866, q_gen_863) -> q_gen_865
<cons, s>(q_gen_866, q_gen_865) -> q_gen_895
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_890, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_875, q_gen_890) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_890
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_890
}

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
() -> reverse([nil, nil]) -> 20
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 22
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 25
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 20
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 23
}
Sat witness: Found: ((length([ll, _pe])) -> length([cons(x, ll), s(_pe)]), {
_pe -> s(z)  ;  ll -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 26, which took 0.046445 s (model generation: 0.046055,  model checking: 0.000390):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_887},
Q_f={q_gen_864},
Delta=
{
<cons>(q_gen_881, q_gen_880) -> q_gen_880
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_879) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_879
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_890, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_890) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_890
}

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
() -> reverse([nil, nil]) -> 20
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 22
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 25
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 23
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 23
}
Sat witness: Found: ((length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]), {
_te -> s(s(z))  ;  _ue -> cons(b, nil)  ;  _ve -> s(z)  ;  l1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 27, which took 0.055396 s (model generation: 0.050997,  model checking: 0.004399):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888},
Q_f={q_gen_864},
Delta=
{
<cons>(q_gen_881, q_gen_880) -> q_gen_880
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892, q_gen_898},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_898, q_gen_889) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, cons>(q_gen_898, q_gen_862) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
<a, b>() -> q_gen_898
<b, a>() -> q_gen_898
}

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
() -> reverse([nil, nil]) -> 21
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 25
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 25
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 23
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 23
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(a, cons(a, nil))  ;  _le -> cons(a, cons(a, nil))  ;  h1 -> a  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 28, which took 0.081811 s (model generation: 0.067036,  model checking: 0.014775):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_920},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_879) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_879
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_879
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 22
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 25
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 28
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 24
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 24
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 29, which took 0.067584 s (model generation: 0.064577,  model checking: 0.003007):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_920},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_879) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_879
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 23
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 28
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 28
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 25
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 25
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> nil  ;  _le -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 30, which took 0.091048 s (model generation: 0.089440,  model checking: 0.001608):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_920},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_879) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_879
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 24
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 28
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 31
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 26
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 26
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 31, which took 0.087914 s (model generation: 0.087192,  model checking: 0.000722):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_867, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888},
Q_f={q_gen_864, q_gen_867},
Delta=
{
<cons>(q_gen_881, q_gen_880) -> q_gen_880
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_867
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_867) -> q_gen_888
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892, q_gen_898},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_898, q_gen_889) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, cons>(q_gen_898, q_gen_862) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
<a, b>() -> q_gen_898
<b, a>() -> q_gen_898
}

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
() -> reverse([nil, nil]) -> 25
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 28
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 31
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 29
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 27
}
Sat witness: Found: ((length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]), {
_te -> s(z)  ;  _ue -> cons(a, cons(b, nil))  ;  _ve -> s(s(z))  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 32, which took 0.074829 s (model generation: 0.073265,  model checking: 0.001564):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_867, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888},
Q_f={q_gen_864, q_gen_867},
Delta=
{
<cons>(q_gen_881, q_gen_880) -> q_gen_880
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_867) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_867
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_867
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_867
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_890, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_890) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_890
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_890
}

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
() -> reverse([nil, nil]) -> 26
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 29
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 31
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 32
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 28
}
Sat witness: Found: ((length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]), {
_te -> s(s(z))  ;  _ue -> cons(b, cons(b, cons(b, nil)))  ;  _ve -> s(s(s(z)))  ;  l1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 33, which took 0.093219 s (model generation: 0.091864,  model checking: 0.001355):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_867, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888},
Q_f={q_gen_864, q_gen_867},
Delta=
{
<cons>(q_gen_881, q_gen_880) -> q_gen_880
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_867) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_867
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_867
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_867
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_867
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892, q_gen_898},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_898, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_898, q_gen_889) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
<a, b>() -> q_gen_898
}

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
() -> reverse([nil, nil]) -> 27
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 32
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 31
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 32
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 29
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(a, nil)  ;  _le -> cons(a, cons(b, cons(b, nil)))  ;  h1 -> b  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 34, which took 0.075724 s (model generation: 0.074305,  model checking: 0.001419):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_867, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888, q_gen_920},
Q_f={q_gen_864, q_gen_867},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_867) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_867
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_867
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_867
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_867
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 28
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 32
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 34
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 32
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 30
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(a, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 35, which took 0.102997 s (model generation: 0.101576,  model checking: 0.001421):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_867, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888, q_gen_920},
Q_f={q_gen_864, q_gen_867},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_887
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_867) -> q_gen_867
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_867
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_867
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_867
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_867
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 29
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 35
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 34
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 33
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 31
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(b, cons(b, nil))  ;  _le -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> a  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 36, which took 0.151252 s (model generation: 0.147175,  model checking: 0.004077):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_920, q_gen_932},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_932
<cons, cons, cons>(q_gen_882, q_gen_879) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_932) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_879
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_932) -> q_gen_879
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_879
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 30
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 35
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 37
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 34
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 32
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, cons(b, nil)))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 37, which took 0.150715 s (model generation: 0.149813,  model checking: 0.000902):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_915, q_gen_920},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_879) -> q_gen_864
<cons, cons, cons>(q_gen_915, q_gen_864) -> q_gen_864
<cons, cons, cons>(q_gen_915, q_gen_879) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_879
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<a, a, a>() -> q_gen_915
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 31
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 38
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 37
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 35
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 33
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(a, nil)  ;  _le -> cons(a, nil)  ;  h1 -> a  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 38, which took 0.134164 s (model generation: 0.133570,  model checking: 0.000594):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_920},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_879) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_879
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_879
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892, q_gen_936},
Q_f={q_gen_862},
Delta=
{
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons>(q_gen_892, q_gen_891) -> q_gen_936
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, cons>(q_gen_892, q_gen_936) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 32
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 38
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 37
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 38
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 34
}
Sat witness: Found: ((length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]), {
_te -> z  ;  _ue -> cons(b, cons(b, nil))  ;  _ve -> s(s(z))  ;  l1 -> nil
})

-------------------------------------------
Step 39, which took 0.113565 s (model generation: 0.112676,  model checking: 0.000889):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_871, q_gen_872, q_gen_880, q_gen_881, q_gen_882, q_gen_883},
Q_f={q_gen_864},
Delta=
{
<cons>(q_gen_881, q_gen_880) -> q_gen_880
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<nil, nil>() -> q_gen_868
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_871) -> q_gen_871
<cons, cons>(q_gen_872, q_gen_868) -> q_gen_871
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_871
<a, a>() -> q_gen_872
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_871) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_872, q_gen_871) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_883) -> q_gen_883
<cons, nil, cons>(q_gen_872, q_gen_868) -> q_gen_883
<nil, cons, cons>(q_gen_869, q_gen_871) -> q_gen_883
<nil, cons, cons>(q_gen_872, q_gen_868) -> q_gen_883
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_874, q_gen_875, q_gen_884, q_gen_885, q_gen_891, q_gen_892},
Q_f={q_gen_862, q_gen_874},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<nil, nil>() -> q_gen_862
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_874
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_874) -> q_gen_884
<cons, cons>(q_gen_875, q_gen_884) -> q_gen_884
<cons, cons>(q_gen_885, q_gen_862) -> q_gen_884
<cons, cons>(q_gen_885, q_gen_884) -> q_gen_884
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_884
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_884
<a, a>() -> q_gen_885
<a, b>() -> q_gen_885
<b, a>() -> q_gen_885
}

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
() -> reverse([nil, nil]) -> 33
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 38
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 37
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 38
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 34
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 40, which took 0.153507 s (model generation: 0.139980,  model checking: 0.013527):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888},
Q_f={q_gen_864},
Delta=
{
<cons>(q_gen_881, q_gen_880) -> q_gen_880
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_885, q_gen_889, q_gen_890, q_gen_891, q_gen_892, q_gen_908},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<b>() -> q_gen_892
<a>() -> q_gen_908
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_885, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_885, q_gen_889) -> q_gen_862
<cons, nil>(q_gen_908, q_gen_891) -> q_gen_862
<nil, nil>() -> q_gen_862
<b, b>() -> q_gen_875
<a, a>() -> q_gen_885
<a, b>() -> q_gen_885
<b, a>() -> q_gen_885
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, cons>(q_gen_875, q_gen_890) -> q_gen_889
<cons, cons>(q_gen_885, q_gen_890) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_890
<nil, cons>(q_gen_908, q_gen_891) -> q_gen_890
}

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
() -> reverse([nil, nil]) -> 34
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 38
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 40
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 38
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 35
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(a, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 41, which took 0.178657 s (model generation: 0.167202,  model checking: 0.011455):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_870, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888, q_gen_920, q_gen_932},
Q_f={q_gen_864, q_gen_870},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<b, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_932
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_932) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_870) -> q_gen_870
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_870
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_870
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_870
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_870
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_932) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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]) -> 37
() -> length([nil, z]) -> 35
() -> reverse([nil, nil]) -> 35
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 39
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 43
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 39
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 36
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 42, which took 0.166658 s (model generation: 0.165691,  model checking: 0.000967):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_878, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888},
Q_f={q_gen_864, q_gen_878},
Delta=
{
<cons>(q_gen_881, q_gen_880) -> q_gen_880
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<a, b>() -> q_gen_869
<b, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_878) -> q_gen_878
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_878
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_878
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_878
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_885, q_gen_889, q_gen_890, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_885, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_885, q_gen_889) -> q_gen_862
<nil, nil>() -> q_gen_862
<b, b>() -> q_gen_875
<a, a>() -> q_gen_885
<a, b>() -> q_gen_885
<b, a>() -> q_gen_885
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, cons>(q_gen_875, q_gen_890) -> q_gen_889
<cons, cons>(q_gen_885, q_gen_890) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_890
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_890
}

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]) -> 38
() -> length([nil, z]) -> 36
() -> reverse([nil, nil]) -> 36
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 39
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 43
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 42
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 37
}
Sat witness: Found: ((length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]), {
_te -> s(s(z))  ;  _ue -> cons(a, cons(b, cons(b, nil)))  ;  _ve -> s(s(s(z)))  ;  l1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 43, which took 0.174267 s (model generation: 0.170162,  model checking: 0.004105):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_878, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888, q_gen_920},
Q_f={q_gen_864, q_gen_878},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<a, b>() -> q_gen_869
<b, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_887
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_878) -> q_gen_878
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_878
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_878
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_878
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_885, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_885, q_gen_862) -> q_gen_862
<cons, cons>(q_gen_885, q_gen_889) -> q_gen_862
<nil, nil>() -> q_gen_862
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<a, a>() -> q_gen_885
<a, b>() -> q_gen_885
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 37
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 42
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 43
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 42
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 38
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(a, cons(b, nil))  ;  _le -> cons(a, cons(b, cons(b, cons(b, nil))))  ;  h1 -> b  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 44, which took 0.164185 s (model generation: 0.162490,  model checking: 0.001695):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_870, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_894, q_gen_920},
Q_f={q_gen_864, q_gen_870},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<a, b>() -> q_gen_869
<b, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_887
<cons, cons, cons>(q_gen_882, q_gen_870) -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_879) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_894, q_gen_864) -> q_gen_870
<cons, cons, cons>(q_gen_894, q_gen_879) -> q_gen_870
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_870
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_870
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_870
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_879
<cons, cons, cons>(q_gen_894, q_gen_870) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_879
<a, a, a>() -> q_gen_882
<b, b, b>() -> q_gen_882
<a, b, a>() -> q_gen_894
<b, a, b>() -> q_gen_894
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 38
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 45
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 43
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 43
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 39
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(b, nil)  ;  _le -> cons(b, nil)  ;  h1 -> a  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 45, which took 0.228264 s (model generation: 0.224103,  model checking: 0.004161):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_867, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888, q_gen_920, q_gen_932},
Q_f={q_gen_864, q_gen_867},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<a, b>() -> q_gen_869
<b, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_932
<cons, cons, cons>(q_gen_882, q_gen_867) -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_932) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_867
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_867
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_867
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_932) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 39
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 45
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 46
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 44
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 40
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(a, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 46, which took 0.272323 s (model generation: 0.270206,  model checking: 0.002117):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_867, q_gen_868, q_gen_869, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888, q_gen_920, q_gen_932},
Q_f={q_gen_864, q_gen_867},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<a, b>() -> q_gen_869
<b, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_932
<cons, nil, cons>(q_gen_869, q_gen_932) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_867) -> q_gen_867
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_867
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_867
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_867
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_867
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_867
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_932) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 40
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 48
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 46
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 45
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 41
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(b, cons(b, nil))  ;  _le -> cons(b, cons(b, nil))  ;  h1 -> b  ;  t1 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 47, which took 0.363063 s (model generation: 0.339208,  model checking: 0.023855):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_878, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888, q_gen_920, q_gen_932},
Q_f={q_gen_864, q_gen_878},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<a, b>() -> q_gen_869
<b, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_932
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_932) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_878) -> q_gen_878
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_878
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_878
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_878
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_932) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 41
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 48
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 49
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 46
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 42
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 48, which took 0.527644 s (model generation: 0.524599,  model checking: 0.003045):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_878, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888, q_gen_920, q_gen_932},
Q_f={q_gen_864, q_gen_878},
Delta=
{
<cons>(q_gen_881, q_gen_920) -> q_gen_880
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<a, b>() -> q_gen_869
<b, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_932
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_932) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_878) -> q_gen_878
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_878
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_878
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_878
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_932) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 42
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 51
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 49
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 47
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 43
}
Sat witness: Found: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(b, nil)  ;  _le -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> b  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 49, which took 0.585582 s (model generation: 0.583029,  model checking: 0.002553):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_912, q_gen_920, q_gen_939},
Q_f={q_gen_864},
Delta=
{
<nil>() -> q_gen_880
<b>() -> q_gen_881
<a>() -> q_gen_912
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons>(q_gen_881, q_gen_920) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<a, b>() -> q_gen_869
<b, a>() -> q_gen_869
<b, b>() -> q_gen_869
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_887
<nil, cons>(q_gen_912, q_gen_880) -> q_gen_939
<cons, cons, cons>(q_gen_882, q_gen_879) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_864
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_879
<cons, nil, cons>(q_gen_869, q_gen_939) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_879
<nil, cons, cons>(q_gen_869, q_gen_939) -> q_gen_879
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_879
<nil, nil, cons>(q_gen_912, q_gen_880) -> q_gen_879
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 43
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 51
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 52
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 48
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 44
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 50, which took 0.665002 s (model generation: 0.640047,  model checking: 0.024955):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_870, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888, q_gen_920, q_gen_932},
Q_f={q_gen_864, q_gen_870},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons>(q_gen_881, q_gen_920) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<a, b>() -> q_gen_869
<b, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_932
<cons, cons, cons>(q_gen_882, q_gen_870) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_932) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_870
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_870
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_870
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_870
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_932) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 44
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 52
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 55
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 49
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 45
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, cons(b, cons(a, cons(b, cons(b, nil)))))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, cons(a, cons(b, nil))))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 51, which took 0.620538 s (model generation: 0.587198,  model checking: 0.033340):

Model:
|_
{
append -> 
{{{
Q={q_gen_864, q_gen_868, q_gen_869, q_gen_870, q_gen_880, q_gen_881, q_gen_882, q_gen_887, q_gen_888, q_gen_920, q_gen_932},
Q_f={q_gen_864, q_gen_870},
Delta=
{
<nil>() -> q_gen_880
<a>() -> q_gen_881
<b>() -> q_gen_881
<cons>(q_gen_881, q_gen_880) -> q_gen_920
<cons>(q_gen_881, q_gen_920) -> q_gen_920
<cons, cons>(q_gen_869, q_gen_868) -> q_gen_868
<nil, nil>() -> q_gen_868
<a, a>() -> q_gen_869
<a, b>() -> q_gen_869
<b, a>() -> q_gen_869
<b, b>() -> q_gen_869
<cons, cons>(q_gen_869, q_gen_887) -> q_gen_887
<nil, cons>(q_gen_881, q_gen_880) -> q_gen_887
<cons, cons>(q_gen_869, q_gen_932) -> q_gen_932
<nil, cons>(q_gen_881, q_gen_920) -> q_gen_932
<cons, cons, cons>(q_gen_882, q_gen_870) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_868) -> q_gen_864
<cons, nil, cons>(q_gen_869, q_gen_932) -> q_gen_864
<nil, nil, cons>(q_gen_881, q_gen_920) -> q_gen_864
<nil, nil, nil>() -> q_gen_864
<cons, cons, cons>(q_gen_882, q_gen_888) -> q_gen_870
<cons, nil, cons>(q_gen_869, q_gen_887) -> q_gen_870
<nil, cons, cons>(q_gen_869, q_gen_868) -> q_gen_870
<nil, nil, cons>(q_gen_881, q_gen_880) -> q_gen_870
<a, a, a>() -> q_gen_882
<a, b, a>() -> q_gen_882
<b, a, b>() -> q_gen_882
<b, b, b>() -> q_gen_882
<cons, cons, cons>(q_gen_882, q_gen_864) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_887) -> q_gen_888
<nil, cons, cons>(q_gen_869, q_gen_932) -> q_gen_888
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_862, q_gen_875, q_gen_889, q_gen_891, q_gen_892},
Q_f={q_gen_862},
Delta=
{
<cons>(q_gen_892, q_gen_891) -> q_gen_891
<nil>() -> q_gen_891
<a>() -> q_gen_892
<b>() -> q_gen_892
<cons, cons>(q_gen_875, q_gen_862) -> q_gen_862
<nil, nil>() -> q_gen_862
<a, a>() -> q_gen_875
<a, b>() -> q_gen_875
<b, a>() -> q_gen_875
<b, b>() -> q_gen_875
<cons, cons>(q_gen_875, q_gen_889) -> q_gen_889
<cons, nil>(q_gen_892, q_gen_891) -> q_gen_889
<nil, cons>(q_gen_892, q_gen_891) -> q_gen_889
}

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
() -> reverse([nil, nil]) -> 45
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 53
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 58
(length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 50
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 46
}
Sat witness: Found: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> cons(b, nil)
})

Total time: 6.801908
Reason for stopping: Proved