Solving ../../benchmarks/true/sort_reverse.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(leq, P:
{() -> leq([a, y])
() -> leq([b, b])
(leq([b, a])) -> BOT}
)
(insert, F:
{() -> insert([x, nil, cons(x, nil)])
(insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)])
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))])}
(insert([_lt, _mt, _nt]) /\ insert([_lt, _mt, _ot])) -> eq_eltlist([_nt, _ot])
)
(sort, F:
{() -> sort([nil, nil])
(insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt])}
(sort([_rt, _st]) /\ sort([_rt, _tt])) -> eq_eltlist([_st, _tt])
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)])}
(append([_vt, _wt, _xt]) /\ append([_vt, _wt, _yt])) -> eq_eltlist([_xt, _yt])
)
(reverse, F:
{() -> reverse([nil, nil])
(append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au])}
(reverse([_bu, _cu]) /\ reverse([_bu, _du])) -> eq_eltlist([_cu, _du])
)
}

properties:
{(reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu])}


over-approximation: {append, insert, reverse, sort}
under-approximation: {leq}

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0  ;  () -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> reverse([nil, nil]) -> 0  ;  () -> sort([nil, nil]) -> 0  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 0  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 0  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 0  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 0  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 0  ;  (leq([b, a])) -> BOT -> 0  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 0
}


Solving took 30.049949 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5925, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5933, q_gen_5934, q_gen_5935, q_gen_5936, q_gen_5949, q_gen_5950, q_gen_5951, q_gen_5952, q_gen_5953, q_gen_5954, q_gen_5955, q_gen_5956, q_gen_5961, q_gen_5962, q_gen_5963, q_gen_5964, q_gen_5965, q_gen_5976, q_gen_5977, q_gen_5978, q_gen_5983, q_gen_5984, q_gen_5985, q_gen_5986, q_gen_5987, q_gen_6002, q_gen_6003, q_gen_6004, q_gen_6005, q_gen_6006, q_gen_6007, q_gen_6008, q_gen_6009, q_gen_6010, q_gen_6020, q_gen_6021, q_gen_6022, q_gen_6023, q_gen_6042, q_gen_6043, q_gen_6044, q_gen_6045, q_gen_6046, q_gen_6047, q_gen_6048, q_gen_6049},
Q_f={},
Delta=
{
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5964
<cons>(q_gen_5964, q_gen_5953) -> q_gen_5986
<nil, nil>() -> q_gen_5926
<nil, b>() -> q_gen_5927
<b, nil>() -> q_gen_5928
<b, b>() -> q_gen_5929
<nil, a>() -> q_gen_5934
<a, nil>() -> q_gen_5935
<a, a>() -> q_gen_5936
<cons, cons>(q_gen_5936, q_gen_5935, q_gen_5934, q_gen_5926) -> q_gen_5951
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5952
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5955
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5962
<cons, b>(q_gen_5964, q_gen_5953) -> q_gen_5963
<b, cons>(q_gen_5964, q_gen_5953) -> q_gen_5965
<cons, a>(q_gen_5964, q_gen_5953) -> q_gen_5977
<a, cons>(q_gen_5964, q_gen_5953) -> q_gen_5978
<cons, cons>(q_gen_5929, q_gen_5965, q_gen_5963, q_gen_5962) -> q_gen_5984
<cons, b>(q_gen_5964, q_gen_5986) -> q_gen_5985
<b, cons>(q_gen_5964, q_gen_5986) -> q_gen_5987
<nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6022
<nil, cons>(q_gen_5964, q_gen_5986) -> q_gen_6049
<nil, nil, nil>() -> q_gen_5911
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5925
<nil, cons, cons>(q_gen_5936, q_gen_5935, q_gen_5934, q_gen_5926) -> q_gen_5933
<cons, nil, cons>(q_gen_5936, q_gen_5935, q_gen_5934, q_gen_5926) -> q_gen_5949
<cons, nil, cons>(q_gen_5929, q_gen_5955, q_gen_5952, q_gen_5951) -> q_gen_5950
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5956
<nil, cons, cons>(q_gen_5929, q_gen_5965, q_gen_5963, q_gen_5962) -> q_gen_5961
<cons, nil, cons>(q_gen_5936, q_gen_5978, q_gen_5977, q_gen_5962) -> q_gen_5976
<nil, cons, cons>(q_gen_5929, q_gen_5987, q_gen_5985, q_gen_5984) -> q_gen_5983
<cons, cons, cons>(q_gen_6010, q_gen_6009, q_gen_6008, q_gen_6007, q_gen_6006, q_gen_6005, q_gen_6004, q_gen_6003) -> q_gen_6002
<nil, nil, cons>(q_gen_5964, q_gen_5953) -> q_gen_6003
<nil, nil, b>() -> q_gen_6004
<nil, b, cons>(q_gen_5964, q_gen_5953) -> q_gen_6005
<nil, b, b>() -> q_gen_6006
<b, nil, cons>(q_gen_5964, q_gen_5953) -> q_gen_6007
<b, nil, b>() -> q_gen_6008
<b, b, cons>(q_gen_5964, q_gen_5953) -> q_gen_6009
<b, b, b>() -> q_gen_6010
<nil, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6020
<cons, nil, cons>(q_gen_5929, q_gen_5955, q_gen_5927, q_gen_6022) -> q_gen_6021
<nil, cons, cons>(q_gen_5929, q_gen_5955, q_gen_5927, q_gen_6022) -> q_gen_6023
<cons, cons, cons>(q_gen_6047, q_gen_6046, q_gen_6008, q_gen_6045, q_gen_6044, q_gen_6043, q_gen_6004, q_gen_6020) -> q_gen_6042
<nil, a, cons>(q_gen_5954, q_gen_5953) -> q_gen_6043
<nil, a, b>() -> q_gen_6044
<b, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6045
<b, a, cons>(q_gen_5954, q_gen_5953) -> q_gen_6046
<b, a, b>() -> q_gen_6047
<nil, cons, cons>(q_gen_5929, q_gen_5987, q_gen_5927, q_gen_6049) -> q_gen_6048
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5912, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916, q_gen_5922, q_gen_5923, q_gen_5924, q_gen_5931, q_gen_5932, q_gen_5937, q_gen_5938, q_gen_5939, q_gen_5944, q_gen_5945, q_gen_5946, q_gen_5947, q_gen_5948, q_gen_5966, q_gen_5967, q_gen_5968, q_gen_5969, q_gen_5988, q_gen_5989, q_gen_5990, q_gen_5991, q_gen_5992, q_gen_5993, q_gen_5994, q_gen_5995, q_gen_5996, q_gen_6019, q_gen_6029, q_gen_6030, q_gen_6031, q_gen_6032, q_gen_6033, q_gen_6034, q_gen_6035, q_gen_6036, q_gen_6037, q_gen_6038, q_gen_6039, q_gen_6040, q_gen_6041},
Q_f={},
Delta=
{
<nil>() -> q_gen_5909
<b>() -> q_gen_5910
<a>() -> q_gen_5932
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5948
<cons>(q_gen_5932, q_gen_5909) -> q_gen_5995
<cons>(q_gen_5910, q_gen_5948) -> q_gen_6034
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<nil, a>() -> q_gen_5914
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, a>() -> q_gen_5916
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5923
<a, a>() -> q_gen_5924
<nil, b>() -> q_gen_5938
<b, b>() -> q_gen_5939
<cons, cons>(q_gen_5939, q_gen_5915, q_gen_5938, q_gen_5913) -> q_gen_5945
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5946
<a, cons>(q_gen_5910, q_gen_5948) -> q_gen_5947
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5967
<b, cons>(q_gen_5910, q_gen_5948) -> q_gen_5968
<cons, cons>(q_gen_5992, q_gen_5991, q_gen_5938, q_gen_5990) -> q_gen_5989
<nil, cons>(q_gen_5932, q_gen_5909) -> q_gen_5990
<a, cons>(q_gen_5932, q_gen_5909) -> q_gen_5991
<a, b>() -> q_gen_5992
<cons, b>(q_gen_5932, q_gen_5909) -> q_gen_5993
<b, cons>(q_gen_5910, q_gen_5995) -> q_gen_5994
<cons, cons>(q_gen_5939, q_gen_5968, q_gen_5967, q_gen_5945) -> q_gen_6031
<cons, b>(q_gen_5910, q_gen_5948) -> q_gen_6032
<b, cons>(q_gen_5910, q_gen_6034) -> q_gen_6033
<cons, cons>(q_gen_5992, q_gen_5923, q_gen_5938, q_gen_5913) -> q_gen_6036
<cons, a>(q_gen_5932, q_gen_5909) -> q_gen_6037
<cons, cons>(q_gen_5916, q_gen_5968, q_gen_6037, q_gen_6036) -> q_gen_6039
<cons, a>(q_gen_5910, q_gen_5995) -> q_gen_6040
<a, cons>(q_gen_5932, q_gen_6034) -> q_gen_6041
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5912
<b, cons, cons>(q_gen_5924, q_gen_5923, q_gen_5914, q_gen_5913) -> q_gen_5922
<a, nil, cons>(q_gen_5932, q_gen_5909) -> q_gen_5931
<b, cons, cons>(q_gen_5939, q_gen_5915, q_gen_5938, q_gen_5913) -> q_gen_5937
<b, cons, cons>(q_gen_5924, q_gen_5947, q_gen_5946, q_gen_5945) -> q_gen_5944
<b, cons, cons>(q_gen_5939, q_gen_5968, q_gen_5967, q_gen_5945) -> q_gen_5966
<b, nil, cons>(q_gen_5932, q_gen_5948) -> q_gen_5969
<b, cons, cons>(q_gen_5939, q_gen_5994, q_gen_5993, q_gen_5989) -> q_gen_5988
<a, nil, cons>(q_gen_5910, q_gen_5995) -> q_gen_5996
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_6019
<a, nil, cons>(q_gen_5932, q_gen_5948) -> q_gen_6029
<b, cons, cons>(q_gen_5939, q_gen_6033, q_gen_6032, q_gen_6031) -> q_gen_6030
<b, cons, cons>(q_gen_5916, q_gen_5968, q_gen_6037, q_gen_6036) -> q_gen_6035
<b, cons, cons>(q_gen_5924, q_gen_6041, q_gen_6040, q_gen_6039) -> q_gen_6038
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5907, q_gen_5921, q_gen_5930},
Q_f={},
Delta=
{
<b, b>() -> q_gen_5906
<a, b>() -> q_gen_5907
<b, a>() -> q_gen_5921
<a, a>() -> q_gen_5930
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5957, q_gen_5958, q_gen_5959, q_gen_5960, q_gen_5979, q_gen_5980, q_gen_5981, q_gen_5982, q_gen_6011, q_gen_6012, q_gen_6013, q_gen_6014, q_gen_6015, q_gen_6024, q_gen_6025, q_gen_6026, q_gen_6027, q_gen_6028, q_gen_6050, q_gen_6051, q_gen_6052, q_gen_6053},
Q_f={},
Delta=
{
<nil>() -> q_gen_6013
<b>() -> q_gen_6014
<a>() -> q_gen_6026
<cons>(q_gen_6014, q_gen_6013) -> q_gen_6052
<nil, nil>() -> q_gen_5905
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5957
<nil, b>() -> q_gen_5958
<b, nil>() -> q_gen_5959
<b, b>() -> q_gen_5960
<cons, cons>(q_gen_5982, q_gen_5981, q_gen_5980, q_gen_5905) -> q_gen_5979
<nil, a>() -> q_gen_5980
<a, nil>() -> q_gen_5981
<a, a>() -> q_gen_5982
<cons, cons>(q_gen_5960, q_gen_6015, q_gen_6012, q_gen_5957) -> q_gen_6011
<cons, b>(q_gen_6014, q_gen_6013) -> q_gen_6012
<b, cons>(q_gen_6014, q_gen_6013) -> q_gen_6015
<cons, cons>(q_gen_5960, q_gen_6027, q_gen_5958, q_gen_6025) -> q_gen_6024
<nil, cons>(q_gen_6026, q_gen_6013) -> q_gen_6025
<b, cons>(q_gen_6026, q_gen_6013) -> q_gen_6027
<nil, cons>(q_gen_6014, q_gen_6013) -> q_gen_6028
<cons, cons>(q_gen_5960, q_gen_6053, q_gen_5958, q_gen_6051) -> q_gen_6050
<nil, cons>(q_gen_6014, q_gen_6052) -> q_gen_6051
<b, cons>(q_gen_6014, q_gen_6052) -> q_gen_6053
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5917, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5940, q_gen_5941, q_gen_5942, q_gen_5943, q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5973, q_gen_5974, q_gen_5975, q_gen_5997, q_gen_5998, q_gen_5999, q_gen_6000, q_gen_6001, q_gen_6016, q_gen_6017, q_gen_6018, q_gen_6054},
Q_f={},
Delta=
{
<nil>() -> q_gen_5972
<b>() -> q_gen_5973
<a>() -> q_gen_5999
<nil, nil>() -> q_gen_5904
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5917
<nil, b>() -> q_gen_5918
<b, nil>() -> q_gen_5919
<b, b>() -> q_gen_5920
<cons, cons>(q_gen_5943, q_gen_5942, q_gen_5941, q_gen_5904) -> q_gen_5940
<nil, a>() -> q_gen_5941
<a, nil>() -> q_gen_5942
<a, a>() -> q_gen_5943
<cons, cons>(q_gen_5975, q_gen_5974, q_gen_5941, q_gen_5971) -> q_gen_5970
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5971
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5974
<b, a>() -> q_gen_5975
<cons, cons>(q_gen_6001, q_gen_6000, q_gen_5918, q_gen_5998) -> q_gen_5997
<nil, cons>(q_gen_5999, q_gen_5972) -> q_gen_5998
<a, cons>(q_gen_5999, q_gen_5972) -> q_gen_6000
<a, b>() -> q_gen_6001
<cons, cons>(q_gen_5943, q_gen_6017, q_gen_5941, q_gen_5971) -> q_gen_6016
<a, cons>(q_gen_5973, q_gen_5972) -> q_gen_6017
<cons, cons>(q_gen_6001, q_gen_5942, q_gen_5918, q_gen_5904) -> q_gen_6018
<cons, cons>(q_gen_5975, q_gen_5919, q_gen_5941, q_gen_5904) -> q_gen_6054
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004545 s (model generation: 0.003939,  model checking: 0.000606):

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

}

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

}

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> reverse([nil, nil]) -> 0  ;  () -> sort([nil, nil]) -> 3  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 1
}
Sat witness: Yes: (() -> sort([nil, nil]), {

})

-------------------------------------------
Step 1, which took 0.003733 s (model generation: 0.003617,  model checking: 0.000116):

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

}

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

}

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

}

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

}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904},
Q_f={q_gen_5904},
Delta=
{
<nil, nil>() -> q_gen_5904
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 1
}
Sat witness: Yes: (() -> reverse([nil, nil]), {

})

-------------------------------------------
Step 2, which took 0.003300 s (model generation: 0.003281,  model checking: 0.000019):

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

}

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

}

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

}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904},
Q_f={q_gen_5904},
Delta=
{
<nil, nil>() -> q_gen_5904
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 1
}
Sat witness: Yes: (() -> leq([b, b]), {

})

-------------------------------------------
Step 3, which took 0.003408 s (model generation: 0.003382,  model checking: 0.000026):

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

}

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

}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906},
Q_f={q_gen_5906},
Delta=
{
<b, b>() -> q_gen_5906
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904},
Q_f={q_gen_5904},
Delta=
{
<nil, nil>() -> q_gen_5904
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 1
}
Sat witness: Yes: (() -> leq([a, y]), {
y -> b
})

-------------------------------------------
Step 4, which took 0.003747 s (model generation: 0.003601,  model checking: 0.000146):

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

}

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

}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906},
Q_f={q_gen_5906},
Delta=
{
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904},
Q_f={q_gen_5904},
Delta=
{
<nil, nil>() -> q_gen_5904
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 1
}
Sat witness: Yes: (() -> insert([x, nil, cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 5, which took 0.005356 s (model generation: 0.004685,  model checking: 0.000671):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<b>() -> q_gen_5910
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906},
Q_f={q_gen_5906},
Delta=
{
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904},
Q_f={q_gen_5904},
Delta=
{
<nil, nil>() -> q_gen_5904
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 1
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 6, which took 0.008858 s (model generation: 0.007479,  model checking: 0.001379):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<b>() -> q_gen_5910
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906},
Q_f={q_gen_5906},
Delta=
{
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904},
Q_f={q_gen_5904},
Delta=
{
<nil, nil>() -> q_gen_5904
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 2
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> a  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 7, which took 0.006531 s (model generation: 0.006176,  model checking: 0.000355):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<b>() -> q_gen_5910
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<nil, a>() -> q_gen_5914
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, a>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906},
Q_f={q_gen_5906},
Delta=
{
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904},
Q_f={q_gen_5904},
Delta=
{
<nil, nil>() -> q_gen_5904
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 2
}
Sat witness: Yes: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), {
_pt -> nil  ;  _qt -> cons(b, nil)  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 8, which took 0.010047 s (model generation: 0.008326,  model checking: 0.001721):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<b>() -> q_gen_5910
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<nil, a>() -> q_gen_5914
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, a>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906},
Q_f={q_gen_5906},
Delta=
{
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920},
Q_f={q_gen_5904},
Delta=
{
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, b>() -> q_gen_5918
<b, nil>() -> q_gen_5919
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 2
}
Sat witness: Yes: ((insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]), {
_kt -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 9, which took 0.010511 s (model generation: 0.009386,  model checking: 0.001125):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<b>() -> q_gen_5910
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<nil, a>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906},
Q_f={q_gen_5906},
Delta=
{
<a, b>() -> q_gen_5906
<b, a>() -> q_gen_5906
<b, b>() -> q_gen_5906
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920},
Q_f={q_gen_5904},
Delta=
{
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, b>() -> q_gen_5918
<b, nil>() -> q_gen_5919
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 2
}
Sat witness: Yes: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), {
_ut -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.011722 s (model generation: 0.011536,  model checking: 0.000186):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929},
Q_f={q_gen_5911},
Delta=
{
<nil, nil>() -> q_gen_5926
<nil, b>() -> q_gen_5927
<b, nil>() -> q_gen_5928
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<b>() -> q_gen_5910
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<nil, a>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906},
Q_f={q_gen_5906},
Delta=
{
<a, b>() -> q_gen_5906
<b, a>() -> q_gen_5906
<b, b>() -> q_gen_5906
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920},
Q_f={q_gen_5904},
Delta=
{
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, b>() -> q_gen_5918
<b, nil>() -> q_gen_5919
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 2  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 3
}
Sat witness: Yes: ((leq([b, a])) -> BOT, {

})

-------------------------------------------
Step 11, which took 0.009415 s (model generation: 0.009050,  model checking: 0.000365):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929},
Q_f={q_gen_5911},
Delta=
{
<nil, nil>() -> q_gen_5926
<nil, b>() -> q_gen_5927
<b, nil>() -> q_gen_5928
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<b>() -> q_gen_5910
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<nil, a>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920},
Q_f={q_gen_5904},
Delta=
{
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, b>() -> q_gen_5918
<b, nil>() -> q_gen_5919
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 3  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 4
}
Sat witness: Yes: (() -> leq([a, y]), {
y -> a
})

-------------------------------------------
Step 12, which took 0.010027 s (model generation: 0.009595,  model checking: 0.000432):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929},
Q_f={q_gen_5911},
Delta=
{
<nil, nil>() -> q_gen_5926
<nil, b>() -> q_gen_5927
<b, nil>() -> q_gen_5928
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<b>() -> q_gen_5910
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<nil, a>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920},
Q_f={q_gen_5904},
Delta=
{
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, b>() -> q_gen_5918
<b, nil>() -> q_gen_5919
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 4  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 4
}
Sat witness: Yes: (() -> insert([x, nil, cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 13, which took 0.011319 s (model generation: 0.007774,  model checking: 0.003545):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929},
Q_f={q_gen_5911},
Delta=
{
<nil, nil>() -> q_gen_5926
<nil, b>() -> q_gen_5927
<b, nil>() -> q_gen_5928
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<nil, a>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920},
Q_f={q_gen_5904},
Delta=
{
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, b>() -> q_gen_5918
<b, nil>() -> q_gen_5919
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 4  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 4
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 14, which took 0.017082 s (model generation: 0.011182,  model checking: 0.005900):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929},
Q_f={q_gen_5911},
Delta=
{
<nil, nil>() -> q_gen_5926
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, nil>() -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<nil, a>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920},
Q_f={q_gen_5904},
Delta=
{
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, b>() -> q_gen_5918
<b, nil>() -> q_gen_5919
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 4  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 5
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 15, which took 0.019407 s (model generation: 0.014704,  model checking: 0.004703):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929},
Q_f={q_gen_5911},
Delta=
{
<nil, nil>() -> q_gen_5926
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, nil>() -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920},
Q_f={q_gen_5904},
Delta=
{
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, b>() -> q_gen_5918
<b, nil>() -> q_gen_5919
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 4  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 5
}
Sat witness: Yes: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), {
_pt -> nil  ;  _qt -> cons(a, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 16, which took 0.015814 s (model generation: 0.010382,  model checking: 0.005432):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929},
Q_f={q_gen_5911},
Delta=
{
<nil, nil>() -> q_gen_5926
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, nil>() -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920},
Q_f={q_gen_5904},
Delta=
{
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, nil>() -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 4  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 7  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 5
}
Sat witness: Yes: ((insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]), {
_kt -> cons(b, cons(b, nil))  ;  x -> b  ;  y -> a  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 17, which took 0.020195 s (model generation: 0.011169,  model checking: 0.009026):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929},
Q_f={q_gen_5911},
Delta=
{
<nil, nil>() -> q_gen_5926
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, nil>() -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920},
Q_f={q_gen_5904},
Delta=
{
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, nil>() -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 4  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 7  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 7  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 5
}
Sat witness: Yes: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), {
_ut -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 18, which took 0.008229 s (model generation: 0.007760,  model checking: 0.000469):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954},
Q_f={q_gen_5911},
Delta=
{
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905},
Q_f={q_gen_5905},
Delta=
{
<nil, nil>() -> q_gen_5905
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920},
Q_f={q_gen_5904},
Delta=
{
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, nil>() -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 7  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 7  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 7  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 5
}
Sat witness: Yes: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), {
_au -> cons(b, nil)  ;  _zt -> nil  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.018053 s (model generation: 0.008144,  model checking: 0.009909):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954},
Q_f={q_gen_5911},
Delta=
{
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960},
Q_f={q_gen_5905},
Delta=
{
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<nil, b>() -> q_gen_5958
<b, nil>() -> q_gen_5959
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920},
Q_f={q_gen_5904},
Delta=
{
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, nil>() -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 5  ;  () -> reverse([nil, nil]) -> 5  ;  () -> sort([nil, nil]) -> 5  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 7  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 7  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 7  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 6  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 6
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 20, which took 0.008739 s (model generation: 0.006566,  model checking: 0.002173):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954},
Q_f={q_gen_5911},
Delta=
{
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960},
Q_f={q_gen_5905},
Delta=
{
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<nil, b>() -> q_gen_5958
<b, nil>() -> q_gen_5959
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920},
Q_f={q_gen_5904},
Delta=
{
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, nil>() -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 6  ;  () -> reverse([nil, nil]) -> 6  ;  () -> sort([nil, nil]) -> 6  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 7  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 7  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 7  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 7  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 7
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 21, which took 0.008783 s (model generation: 0.006996,  model checking: 0.001787):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954},
Q_f={q_gen_5911},
Delta=
{
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960},
Q_f={q_gen_5905},
Delta=
{
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<nil, b>() -> q_gen_5958
<b, nil>() -> q_gen_5959
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920},
Q_f={q_gen_5904},
Delta=
{
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, nil>() -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 7  ;  () -> reverse([nil, nil]) -> 7  ;  () -> sort([nil, nil]) -> 7  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 7  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 7  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 7  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 8  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 8
}
Sat witness: Yes: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), {
_pt -> nil  ;  _qt -> cons(a, cons(b, nil))  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 22, which took 0.020333 s (model generation: 0.007520,  model checking: 0.012813):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954},
Q_f={q_gen_5911},
Delta=
{
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960},
Q_f={q_gen_5905},
Delta=
{
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<nil, b>() -> q_gen_5958
<b, nil>() -> q_gen_5959
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 7  ;  () -> reverse([nil, nil]) -> 7  ;  () -> sort([nil, nil]) -> 7  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 7  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 10  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 8  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 8  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 8
}
Sat witness: Yes: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), {
_ut -> cons(b, nil)  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 23, which took 0.008507 s (model generation: 0.008111,  model checking: 0.000396):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954},
Q_f={q_gen_5911},
Delta=
{
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960},
Q_f={q_gen_5905},
Delta=
{
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<nil, b>() -> q_gen_5958
<b, nil>() -> q_gen_5959
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 7  ;  () -> reverse([nil, nil]) -> 7  ;  () -> sort([nil, nil]) -> 7  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 10  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 10  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 8  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 8  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 8
}
Sat witness: Yes: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), {
_au -> cons(a, nil)  ;  _zt -> nil  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 24, which took 0.008933 s (model generation: 0.008250,  model checking: 0.000683):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954},
Q_f={q_gen_5911},
Delta=
{
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960},
Q_f={q_gen_5905},
Delta=
{
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> insert([x, nil, cons(x, nil)]) -> 8  ;  () -> leq([a, y]) -> 8  ;  () -> leq([b, b]) -> 8  ;  () -> reverse([nil, nil]) -> 8  ;  () -> sort([nil, nil]) -> 8  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 10  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 10  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 8  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 8  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 11
}
Sat witness: Yes: ((reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]), {
_eu -> nil  ;  _fu -> nil  ;  _gu -> cons(b, nil)  ;  l -> nil
})

-------------------------------------------
Step 25, which took 0.036893 s (model generation: 0.013941,  model checking: 0.022952):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954},
Q_f={q_gen_5911},
Delta=
{
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960},
Q_f={q_gen_5905},
Delta=
{
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5971, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5971
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> insert([x, nil, cons(x, nil)]) -> 9  ;  () -> leq([a, y]) -> 9  ;  () -> leq([b, b]) -> 9  ;  () -> reverse([nil, nil]) -> 9  ;  () -> sort([nil, nil]) -> 9  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 10  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 10  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 9  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 9  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 11
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 26, which took 0.018812 s (model generation: 0.008973,  model checking: 0.009839):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960},
Q_f={q_gen_5905},
Delta=
{
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5971, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5971
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> insert([x, nil, cons(x, nil)]) -> 10  ;  () -> leq([a, y]) -> 10  ;  () -> leq([b, b]) -> 10  ;  () -> reverse([nil, nil]) -> 10  ;  () -> sort([nil, nil]) -> 10  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 10  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 10  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 10  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 10  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 11
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 27, which took 0.013247 s (model generation: 0.009969,  model checking: 0.003278):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<a, b>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960},
Q_f={q_gen_5905},
Delta=
{
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5971, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5971
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> insert([x, nil, cons(x, nil)]) -> 10  ;  () -> leq([a, y]) -> 10  ;  () -> leq([b, b]) -> 10  ;  () -> reverse([nil, nil]) -> 10  ;  () -> sort([nil, nil]) -> 10  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 10  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 10  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 10  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 13  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 11  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 11
}
Sat witness: Yes: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), {
_pt -> nil  ;  _qt -> cons(b, cons(a, nil))  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 28, which took 0.023600 s (model generation: 0.012576,  model checking: 0.011024):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<a, b>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960},
Q_f={q_gen_5905},
Delta=
{
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5971, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<a>() -> q_gen_5973
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<a, b>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5971
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> insert([x, nil, cons(x, nil)]) -> 10  ;  () -> leq([a, y]) -> 10  ;  () -> leq([b, b]) -> 10  ;  () -> reverse([nil, nil]) -> 10  ;  () -> sort([nil, nil]) -> 10  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 10  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 13  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 11  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 13  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 11  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 11
}
Sat witness: Yes: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), {
_ut -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 29, which took 0.014444 s (model generation: 0.012541,  model checking: 0.001903):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954, q_gen_6004, q_gen_6005, q_gen_6006, q_gen_6007, q_gen_6008, q_gen_6009, q_gen_6010},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, cons, cons>(q_gen_6010, q_gen_6009, q_gen_6008, q_gen_6007, q_gen_6006, q_gen_6005, q_gen_6004, q_gen_5911) -> q_gen_5911
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
<nil, nil, b>() -> q_gen_6004
<nil, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6005
<nil, b, b>() -> q_gen_6006
<b, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6007
<b, nil, b>() -> q_gen_6008
<b, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6009
<b, b, b>() -> q_gen_6010
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<a, b>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960},
Q_f={q_gen_5905},
Delta=
{
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5971, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<a>() -> q_gen_5973
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<a, b>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5971
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> insert([x, nil, cons(x, nil)]) -> 10  ;  () -> leq([a, y]) -> 10  ;  () -> leq([b, b]) -> 10  ;  () -> reverse([nil, nil]) -> 10  ;  () -> sort([nil, nil]) -> 10  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 13  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 13  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 11  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 13  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 11  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 11
}
Sat witness: Yes: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), {
_au -> cons(b, cons(b, nil))  ;  _zt -> cons(b, nil)  ;  h1 -> b  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 30, which took 0.014956 s (model generation: 0.013842,  model checking: 0.001114):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954, q_gen_6004, q_gen_6005, q_gen_6006, q_gen_6007, q_gen_6008, q_gen_6009, q_gen_6010},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, cons, cons>(q_gen_6010, q_gen_6009, q_gen_6008, q_gen_6007, q_gen_6006, q_gen_6005, q_gen_6004, q_gen_5911) -> q_gen_5911
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
<nil, nil, b>() -> q_gen_6004
<nil, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6005
<nil, b, b>() -> q_gen_6006
<b, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6007
<b, nil, b>() -> q_gen_6008
<b, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6009
<b, b, b>() -> q_gen_6010
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<a, b>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960, q_gen_6013, q_gen_6014},
Q_f={q_gen_5905},
Delta=
{
<nil>() -> q_gen_6013
<b>() -> q_gen_6014
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<cons, b>(q_gen_6014, q_gen_6013) -> q_gen_5958
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, cons>(q_gen_6014, q_gen_6013) -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5971, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<a>() -> q_gen_5973
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<a, b>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5971
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> insert([x, nil, cons(x, nil)]) -> 11  ;  () -> leq([a, y]) -> 11  ;  () -> leq([b, b]) -> 11  ;  () -> reverse([nil, nil]) -> 11  ;  () -> sort([nil, nil]) -> 11  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 13  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 13  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 11  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 13  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 11  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 14
}
Sat witness: Yes: ((reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]), {
_eu -> cons(b, nil)  ;  _fu -> cons(a, nil)  ;  _gu -> cons(a, cons(b, nil))  ;  l -> cons(a, nil)
})

-------------------------------------------
Step 31, which took 0.023107 s (model generation: 0.012576,  model checking: 0.010531):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954, q_gen_6004, q_gen_6005, q_gen_6006, q_gen_6007, q_gen_6008, q_gen_6009, q_gen_6010},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, cons, cons>(q_gen_6010, q_gen_6009, q_gen_6008, q_gen_6007, q_gen_6006, q_gen_6005, q_gen_6004, q_gen_5911) -> q_gen_5911
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
<nil, nil, b>() -> q_gen_6004
<nil, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6005
<nil, b, b>() -> q_gen_6006
<b, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6007
<b, nil, b>() -> q_gen_6008
<b, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6009
<b, b, b>() -> q_gen_6010
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<a, b>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960, q_gen_6013, q_gen_6014},
Q_f={q_gen_5905},
Delta=
{
<nil>() -> q_gen_6013
<b>() -> q_gen_6014
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<cons, b>(q_gen_6014, q_gen_6013) -> q_gen_5958
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, cons>(q_gen_6014, q_gen_6013) -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5971, q_gen_5972, q_gen_5973, q_gen_5975},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<a>() -> q_gen_5973
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5904
<cons, cons>(q_gen_5975, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<cons, cons>(q_gen_5975, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5971
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5971
<a, b>() -> q_gen_5975
<b, a>() -> q_gen_5975
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> insert([x, nil, cons(x, nil)]) -> 12  ;  () -> leq([a, y]) -> 12  ;  () -> leq([b, b]) -> 12  ;  () -> reverse([nil, nil]) -> 12  ;  () -> sort([nil, nil]) -> 12  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 13  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 13  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 12  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 16  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 14  ;  (leq([b, a])) -> BOT -> 12  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 14
}
Sat witness: Yes: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), {
_pt -> nil  ;  _qt -> cons(b, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 32, which took 0.043974 s (model generation: 0.012707,  model checking: 0.031267):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954, q_gen_6004, q_gen_6005, q_gen_6006, q_gen_6007, q_gen_6008, q_gen_6009, q_gen_6010},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, cons, cons>(q_gen_6010, q_gen_6009, q_gen_6008, q_gen_6007, q_gen_6006, q_gen_6005, q_gen_6004, q_gen_5911) -> q_gen_5911
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
<nil, nil, b>() -> q_gen_6004
<nil, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6005
<nil, b, b>() -> q_gen_6006
<b, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6007
<b, nil, b>() -> q_gen_6008
<b, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6009
<b, b, b>() -> q_gen_6010
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<a, b>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960, q_gen_6013, q_gen_6014},
Q_f={q_gen_5905},
Delta=
{
<nil>() -> q_gen_6013
<b>() -> q_gen_6014
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<cons, b>(q_gen_6014, q_gen_6013) -> q_gen_5958
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, cons>(q_gen_6014, q_gen_6013) -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5943, q_gen_5971, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<a>() -> q_gen_5973
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5904
<cons, cons>(q_gen_5943, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, b>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<a, a>() -> q_gen_5943
<cons, cons>(q_gen_5943, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5971
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5971
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> insert([x, nil, cons(x, nil)]) -> 13  ;  () -> leq([a, y]) -> 13  ;  () -> leq([b, b]) -> 13  ;  () -> reverse([nil, nil]) -> 13  ;  () -> sort([nil, nil]) -> 13  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 13  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 16  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 13  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 16  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 14  ;  (leq([b, a])) -> BOT -> 13  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 14
}
Sat witness: Yes: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), {
_ut -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 33, which took 0.023197 s (model generation: 0.014973,  model checking: 0.008224):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954, q_gen_6004, q_gen_6005, q_gen_6006, q_gen_6007, q_gen_6008, q_gen_6009, q_gen_6010},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, cons, cons>(q_gen_6010, q_gen_6009, q_gen_6008, q_gen_6007, q_gen_6006, q_gen_6005, q_gen_6004, q_gen_5911) -> q_gen_5911
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
<nil, nil, b>() -> q_gen_6004
<nil, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6005
<nil, b, b>() -> q_gen_6006
<b, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6007
<b, nil, b>() -> q_gen_6008
<b, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6009
<b, b, b>() -> q_gen_6010
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<a, b>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960, q_gen_6013, q_gen_6014},
Q_f={q_gen_5905},
Delta=
{
<nil>() -> q_gen_6013
<b>() -> q_gen_6014
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<cons, b>(q_gen_6014, q_gen_6013) -> q_gen_5958
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, cons>(q_gen_6014, q_gen_6013) -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5943, q_gen_5971, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<a>() -> q_gen_5973
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5904
<cons, cons>(q_gen_5943, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, b>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<a, a>() -> q_gen_5943
<cons, cons>(q_gen_5943, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5971
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5971
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> insert([x, nil, cons(x, nil)]) -> 13  ;  () -> leq([a, y]) -> 13  ;  () -> leq([b, b]) -> 13  ;  () -> reverse([nil, nil]) -> 13  ;  () -> sort([nil, nil]) -> 13  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 16  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 16  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 14  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 16  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 14  ;  (leq([b, a])) -> BOT -> 14  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 14
}
Sat witness: Yes: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), {
_au -> cons(b, cons(a, nil))  ;  _zt -> nil  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 34, which took 0.018966 s (model generation: 0.015241,  model checking: 0.003725):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954, q_gen_6004, q_gen_6005, q_gen_6006, q_gen_6007, q_gen_6008, q_gen_6009, q_gen_6010},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, cons, cons>(q_gen_6010, q_gen_6009, q_gen_6008, q_gen_6007, q_gen_6006, q_gen_6005, q_gen_6004, q_gen_5911) -> q_gen_5911
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
<nil, nil, b>() -> q_gen_6004
<nil, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6005
<nil, b, b>() -> q_gen_6006
<b, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6007
<b, nil, b>() -> q_gen_6008
<b, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6009
<b, b, b>() -> q_gen_6010
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<a, b>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960, q_gen_6013, q_gen_6014},
Q_f={q_gen_5905},
Delta=
{
<nil>() -> q_gen_6013
<a>() -> q_gen_6014
<b>() -> q_gen_6014
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<nil, cons>(q_gen_6014, q_gen_6013) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<cons, b>(q_gen_6014, q_gen_6013) -> q_gen_5958
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, cons>(q_gen_6014, q_gen_6013) -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5971, q_gen_5972, q_gen_5973, q_gen_5975},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<a>() -> q_gen_5973
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<cons, cons>(q_gen_5975, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<cons, cons>(q_gen_5975, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5971
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5971
<a, b>() -> q_gen_5975
<b, a>() -> q_gen_5975
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14  ;  () -> insert([x, nil, cons(x, nil)]) -> 14  ;  () -> leq([a, y]) -> 14  ;  () -> leq([b, b]) -> 14  ;  () -> reverse([nil, nil]) -> 14  ;  () -> sort([nil, nil]) -> 14  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 16  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 16  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 14  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 16  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 14  ;  (leq([b, a])) -> BOT -> 14  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 17
}
Sat witness: Yes: ((reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]), {
_eu -> nil  ;  _fu -> cons(b, nil)  ;  _gu -> cons(b, nil)  ;  l -> nil
})

-------------------------------------------
Step 35, which took 0.027313 s (model generation: 0.015925,  model checking: 0.011388):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954, q_gen_6004, q_gen_6005, q_gen_6006, q_gen_6007, q_gen_6008, q_gen_6009, q_gen_6010},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, cons, cons>(q_gen_6010, q_gen_6009, q_gen_6008, q_gen_6007, q_gen_6006, q_gen_6005, q_gen_6004, q_gen_5911) -> q_gen_5911
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
<nil, nil, b>() -> q_gen_6004
<nil, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6005
<nil, b, b>() -> q_gen_6006
<b, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6007
<b, nil, b>() -> q_gen_6008
<b, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6009
<b, b, b>() -> q_gen_6010
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, a>() -> q_gen_5916
<a, b>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960, q_gen_6013, q_gen_6014, q_gen_6025},
Q_f={q_gen_5905},
Delta=
{
<nil>() -> q_gen_6013
<a>() -> q_gen_6014
<b>() -> q_gen_6014
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_6025) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<cons, b>(q_gen_6014, q_gen_6013) -> q_gen_5958
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, cons>(q_gen_6014, q_gen_6013) -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
<nil, cons>(q_gen_6014, q_gen_6013) -> q_gen_6025
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5943, q_gen_5971, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<a>() -> q_gen_5973
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5904
<cons, cons>(q_gen_5943, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, b>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<a, a>() -> q_gen_5943
<cons, cons>(q_gen_5943, q_gen_5919, q_gen_5918, q_gen_5971) -> q_gen_5971
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5971
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  () -> insert([x, nil, cons(x, nil)]) -> 15  ;  () -> leq([a, y]) -> 15  ;  () -> leq([b, b]) -> 15  ;  () -> reverse([nil, nil]) -> 15  ;  () -> sort([nil, nil]) -> 15  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 16  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 16  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 15  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 19  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 15  ;  (leq([b, a])) -> BOT -> 15  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 17
}
Sat witness: Yes: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), {
_pt -> nil  ;  _qt -> cons(a, cons(b, nil))  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 36, which took 0.098953 s (model generation: 0.018559,  model checking: 0.080394):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954, q_gen_6004, q_gen_6005, q_gen_6006, q_gen_6007, q_gen_6008, q_gen_6009, q_gen_6010},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, cons, cons>(q_gen_6010, q_gen_6009, q_gen_6008, q_gen_6007, q_gen_6006, q_gen_6005, q_gen_6004, q_gen_5911) -> q_gen_5911
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
<nil, nil, b>() -> q_gen_6004
<nil, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6005
<nil, b, b>() -> q_gen_6006
<b, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6007
<b, nil, b>() -> q_gen_6008
<b, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6009
<b, b, b>() -> q_gen_6010
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916, q_gen_5948, q_gen_5969},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5948
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, cons>(q_gen_5910, q_gen_5948) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5948) -> q_gen_5915
<a, a>() -> q_gen_5916
<a, b>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5948) -> q_gen_5969
<b, nil, cons>(q_gen_5910, q_gen_5948) -> q_gen_5969
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960, q_gen_6013, q_gen_6014, q_gen_6025},
Q_f={q_gen_5905},
Delta=
{
<nil>() -> q_gen_6013
<a>() -> q_gen_6014
<b>() -> q_gen_6014
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_6025) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<cons, b>(q_gen_6014, q_gen_6013) -> q_gen_5958
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, cons>(q_gen_6014, q_gen_6013) -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
<nil, cons>(q_gen_6014, q_gen_6013) -> q_gen_6025
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5970, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<a>() -> q_gen_5973
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<a, b>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5970) -> q_gen_5970
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5970
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  () -> insert([x, nil, cons(x, nil)]) -> 15  ;  () -> leq([a, y]) -> 15  ;  () -> leq([b, b]) -> 15  ;  () -> reverse([nil, nil]) -> 15  ;  () -> sort([nil, nil]) -> 15  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 16  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 16  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 15  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 19  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18  ;  (leq([b, a])) -> BOT -> 16  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 17
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 37, which took 1.520348 s (model generation: 0.018363,  model checking: 1.501985):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954, q_gen_6004, q_gen_6005, q_gen_6006, q_gen_6007, q_gen_6008, q_gen_6009, q_gen_6010},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, cons, cons>(q_gen_6010, q_gen_6009, q_gen_6008, q_gen_6007, q_gen_6006, q_gen_6005, q_gen_6004, q_gen_5911) -> q_gen_5911
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
<nil, nil, b>() -> q_gen_6004
<nil, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6005
<nil, b, b>() -> q_gen_6006
<b, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6007
<b, nil, b>() -> q_gen_6008
<b, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6009
<b, b, b>() -> q_gen_6010
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916, q_gen_5948, q_gen_5969},
Q_f={q_gen_5908},
Delta=
{
<cons>(q_gen_5910, q_gen_5948) -> q_gen_5909
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5948
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5948) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, cons>(q_gen_5910, q_gen_5948) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5948) -> q_gen_5915
<a, a>() -> q_gen_5916
<a, b>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5948) -> q_gen_5969
<b, nil, cons>(q_gen_5910, q_gen_5948) -> q_gen_5969
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960, q_gen_6013, q_gen_6014, q_gen_6025},
Q_f={q_gen_5905},
Delta=
{
<nil>() -> q_gen_6013
<a>() -> q_gen_6014
<b>() -> q_gen_6014
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_6025) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<cons, b>(q_gen_6014, q_gen_6013) -> q_gen_5958
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, cons>(q_gen_6014, q_gen_6013) -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
<nil, cons>(q_gen_6014, q_gen_6013) -> q_gen_6025
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5970, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<a>() -> q_gen_5973
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<a, b>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5970) -> q_gen_5970
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5970
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  () -> insert([x, nil, cons(x, nil)]) -> 15  ;  () -> leq([a, y]) -> 15  ;  () -> leq([b, b]) -> 15  ;  () -> reverse([nil, nil]) -> 15  ;  () -> sort([nil, nil]) -> 15  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 16  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 16  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 18  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 19  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18  ;  (leq([b, a])) -> BOT -> 16  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 17
}
Sat witness: Yes: ((insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]), {
_kt -> cons(a, cons(b, cons(b, nil)))  ;  x -> b  ;  y -> a  ;  z -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 38, which took 0.089046 s (model generation: 0.020565,  model checking: 0.068481):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954, q_gen_6004, q_gen_6005, q_gen_6006, q_gen_6007, q_gen_6008, q_gen_6009, q_gen_6010},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, cons, cons>(q_gen_6010, q_gen_6009, q_gen_6008, q_gen_6007, q_gen_6006, q_gen_6005, q_gen_6004, q_gen_5911) -> q_gen_5911
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
<nil, nil, b>() -> q_gen_6004
<nil, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6005
<nil, b, b>() -> q_gen_6006
<b, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6007
<b, nil, b>() -> q_gen_6008
<b, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6009
<b, b, b>() -> q_gen_6010
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916, q_gen_5948, q_gen_5969},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5948
<cons>(q_gen_5910, q_gen_5948) -> q_gen_5948
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, a>(q_gen_5910, q_gen_5948) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5948) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, cons>(q_gen_5910, q_gen_5948) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5948) -> q_gen_5915
<a, a>() -> q_gen_5916
<a, b>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5948) -> q_gen_5969
<b, nil, cons>(q_gen_5910, q_gen_5948) -> q_gen_5969
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960, q_gen_6013, q_gen_6014, q_gen_6025},
Q_f={q_gen_5905},
Delta=
{
<nil>() -> q_gen_6013
<a>() -> q_gen_6014
<b>() -> q_gen_6014
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_6025) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<cons, b>(q_gen_6014, q_gen_6013) -> q_gen_5958
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, cons>(q_gen_6014, q_gen_6013) -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
<nil, cons>(q_gen_6014, q_gen_6013) -> q_gen_6025
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5970, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<a>() -> q_gen_5973
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<a, b>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5970) -> q_gen_5970
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5970
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> insert([x, nil, cons(x, nil)]) -> 16  ;  () -> leq([a, y]) -> 16  ;  () -> leq([b, b]) -> 16  ;  () -> reverse([nil, nil]) -> 16  ;  () -> sort([nil, nil]) -> 16  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 16  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 19  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 18  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 19  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18  ;  (leq([b, a])) -> BOT -> 17  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 17
}
Sat witness: Yes: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), {
_ut -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 39, which took 0.025044 s (model generation: 0.021279,  model checking: 0.003765):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954, q_gen_6004, q_gen_6005, q_gen_6006, q_gen_6007, q_gen_6008, q_gen_6009, q_gen_6010},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, cons, cons>(q_gen_6010, q_gen_6009, q_gen_6008, q_gen_6007, q_gen_6006, q_gen_6005, q_gen_6004, q_gen_5911) -> q_gen_5911
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
<nil, nil, b>() -> q_gen_6004
<nil, a, cons>(q_gen_5954, q_gen_5953) -> q_gen_6005
<nil, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6005
<nil, a, b>() -> q_gen_6006
<nil, b, b>() -> q_gen_6006
<b, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6007
<b, nil, b>() -> q_gen_6008
<b, a, cons>(q_gen_5954, q_gen_5953) -> q_gen_6009
<b, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6009
<b, a, b>() -> q_gen_6010
<b, b, b>() -> q_gen_6010
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916, q_gen_5948, q_gen_5969},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5948
<cons>(q_gen_5910, q_gen_5948) -> q_gen_5948
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, a>(q_gen_5910, q_gen_5948) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5948) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, cons>(q_gen_5910, q_gen_5948) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5948) -> q_gen_5915
<a, a>() -> q_gen_5916
<a, b>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5948) -> q_gen_5969
<b, nil, cons>(q_gen_5910, q_gen_5948) -> q_gen_5969
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960, q_gen_6013, q_gen_6014, q_gen_6025},
Q_f={q_gen_5905},
Delta=
{
<nil>() -> q_gen_6013
<a>() -> q_gen_6014
<b>() -> q_gen_6014
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_6025) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<cons, b>(q_gen_6014, q_gen_6013) -> q_gen_5958
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, cons>(q_gen_6014, q_gen_6013) -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
<nil, cons>(q_gen_6014, q_gen_6013) -> q_gen_6025
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5970, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<a>() -> q_gen_5973
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<a, b>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5970) -> q_gen_5970
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5970
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> insert([x, nil, cons(x, nil)]) -> 16  ;  () -> leq([a, y]) -> 16  ;  () -> leq([b, b]) -> 16  ;  () -> reverse([nil, nil]) -> 16  ;  () -> sort([nil, nil]) -> 16  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 19  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 19  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 18  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 19  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18  ;  (leq([b, a])) -> BOT -> 17  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 17
}
Sat witness: Yes: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), {
_au -> cons(b, cons(b, cons(b, nil)))  ;  _zt -> nil  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 40, which took 0.028025 s (model generation: 0.024404,  model checking: 0.003621):

Model:
|_
{
append -> 
{{{
Q={q_gen_5911, q_gen_5926, q_gen_5927, q_gen_5928, q_gen_5929, q_gen_5953, q_gen_5954, q_gen_6004, q_gen_6005, q_gen_6006, q_gen_6007, q_gen_6008, q_gen_6009, q_gen_6010},
Q_f={q_gen_5911},
Delta=
{
<cons>(q_gen_5954, q_gen_5953) -> q_gen_5953
<nil>() -> q_gen_5953
<a>() -> q_gen_5954
<b>() -> q_gen_5954
<cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5926
<nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5926
<nil, nil>() -> q_gen_5926
<cons, a>(q_gen_5954, q_gen_5953) -> q_gen_5927
<cons, b>(q_gen_5954, q_gen_5953) -> q_gen_5927
<nil, a>() -> q_gen_5927
<nil, b>() -> q_gen_5927
<a, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<a, nil>() -> q_gen_5928
<b, cons>(q_gen_5954, q_gen_5953) -> q_gen_5928
<b, nil>() -> q_gen_5928
<a, a>() -> q_gen_5929
<b, b>() -> q_gen_5929
<cons, cons, cons>(q_gen_6010, q_gen_6009, q_gen_6008, q_gen_6007, q_gen_6006, q_gen_6005, q_gen_6004, q_gen_5911) -> q_gen_5911
<cons, nil, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, cons, cons>(q_gen_5929, q_gen_5928, q_gen_5927, q_gen_5926) -> q_gen_5911
<nil, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_5911
<nil, nil, nil>() -> q_gen_5911
<nil, nil, b>() -> q_gen_6004
<nil, a, cons>(q_gen_5954, q_gen_5953) -> q_gen_6005
<nil, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6005
<nil, a, b>() -> q_gen_6006
<nil, b, b>() -> q_gen_6006
<b, nil, cons>(q_gen_5954, q_gen_5953) -> q_gen_6007
<b, nil, b>() -> q_gen_6008
<b, a, cons>(q_gen_5954, q_gen_5953) -> q_gen_6009
<b, b, cons>(q_gen_5954, q_gen_5953) -> q_gen_6009
<b, a, b>() -> q_gen_6010
<b, b, b>() -> q_gen_6010
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5908, q_gen_5909, q_gen_5910, q_gen_5913, q_gen_5914, q_gen_5915, q_gen_5916, q_gen_5948, q_gen_5969},
Q_f={q_gen_5908},
Delta=
{
<nil>() -> q_gen_5909
<a>() -> q_gen_5910
<b>() -> q_gen_5910
<cons>(q_gen_5910, q_gen_5909) -> q_gen_5948
<cons>(q_gen_5910, q_gen_5948) -> q_gen_5948
<cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5913
<nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5913
<cons, a>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, a>(q_gen_5910, q_gen_5948) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5909) -> q_gen_5914
<cons, b>(q_gen_5910, q_gen_5948) -> q_gen_5914
<nil, a>() -> q_gen_5914
<nil, b>() -> q_gen_5914
<a, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<a, cons>(q_gen_5910, q_gen_5948) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5909) -> q_gen_5915
<b, cons>(q_gen_5910, q_gen_5948) -> q_gen_5915
<a, a>() -> q_gen_5916
<a, b>() -> q_gen_5916
<b, a>() -> q_gen_5916
<b, b>() -> q_gen_5916
<a, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<b, cons, cons>(q_gen_5916, q_gen_5915, q_gen_5914, q_gen_5913) -> q_gen_5908
<b, nil, cons>(q_gen_5910, q_gen_5909) -> q_gen_5908
<a, nil, cons>(q_gen_5910, q_gen_5948) -> q_gen_5969
<b, nil, cons>(q_gen_5910, q_gen_5948) -> q_gen_5969
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_5906, q_gen_5921},
Q_f={q_gen_5906},
Delta=
{
<a, a>() -> q_gen_5906
<a, b>() -> q_gen_5906
<b, b>() -> q_gen_5906
<b, a>() -> q_gen_5921
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5905, q_gen_5958, q_gen_5959, q_gen_5960, q_gen_6013, q_gen_6014, q_gen_6025},
Q_f={q_gen_5905},
Delta=
{
<cons>(q_gen_6014, q_gen_6013) -> q_gen_6013
<nil>() -> q_gen_6013
<a>() -> q_gen_6014
<b>() -> q_gen_6014
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_5905) -> q_gen_5905
<cons, cons>(q_gen_5960, q_gen_5959, q_gen_5958, q_gen_6025) -> q_gen_5905
<nil, nil>() -> q_gen_5905
<cons, b>(q_gen_6014, q_gen_6013) -> q_gen_5958
<nil, a>() -> q_gen_5958
<nil, b>() -> q_gen_5958
<a, nil>() -> q_gen_5959
<b, cons>(q_gen_6014, q_gen_6013) -> q_gen_5959
<b, nil>() -> q_gen_5959
<a, a>() -> q_gen_5960
<b, b>() -> q_gen_5960
<nil, cons>(q_gen_6014, q_gen_6013) -> q_gen_6025
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5904, q_gen_5918, q_gen_5919, q_gen_5920, q_gen_5970, q_gen_5972, q_gen_5973},
Q_f={q_gen_5904},
Delta=
{
<nil>() -> q_gen_5972
<a>() -> q_gen_5973
<b>() -> q_gen_5973
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5904) -> q_gen_5904
<nil, nil>() -> q_gen_5904
<nil, a>() -> q_gen_5918
<nil, b>() -> q_gen_5918
<a, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<a, nil>() -> q_gen_5919
<b, cons>(q_gen_5973, q_gen_5972) -> q_gen_5919
<b, nil>() -> q_gen_5919
<a, a>() -> q_gen_5920
<a, b>() -> q_gen_5920
<b, a>() -> q_gen_5920
<b, b>() -> q_gen_5920
<cons, cons>(q_gen_5920, q_gen_5919, q_gen_5918, q_gen_5970) -> q_gen_5970
<nil, cons>(q_gen_5973, q_gen_5972) -> q_gen_5970
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17  ;  () -> insert([x, nil, cons(x, nil)]) -> 17  ;  () -> leq([a, y]) -> 17  ;  () -> leq([b, b]) -> 17  ;  () -> reverse([nil, nil]) -> 17  ;  () -> sort([nil, nil]) -> 17  ;  (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 19  ;  (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 19  ;  (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 18  ;  (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 19  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18  ;  (leq([b, a])) -> BOT -> 17  ;  (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 20
}
Sat witness: Yes: ((reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]), {
_eu -> cons(b, nil)  ;  _fu -> cons(b, nil)  ;  _gu -> cons(a, nil)  ;  l -> cons(b, nil)
})

Total time: 30.049949
Reason for stopping: DontKnow. Stopped because: timeout