Solving ../../benchmarks/true/timbuk_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}
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)])}
(append([_ef, _ff, _gf]) /\ append([_ef, _ff, _hf])) -> eq_eltlist([_gf, _hf])
)
(reverse, F:
{() -> reverse([nil, nil])
(append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf])}
(reverse([_kf, _lf]) /\ reverse([_kf, _mf])) -> eq_eltlist([_lf, _mf])
)
(sorted, P:
{() -> sorted([cons(x, nil)])
() -> sorted([nil])}
)
(invsorted, P:
{() -> invsorted([cons(x, nil)])
() -> invsorted([nil])}
)
}

properties:
{(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf])}


over-approximation: {append, leq, reverse, sorted}
under-approximation: {invsorted, leq}

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0  ;  () -> invsorted([cons(x, nil)]) -> 0  ;  () -> invsorted([nil]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> reverse([nil, nil]) -> 0  ;  () -> sorted([cons(x, nil)]) -> 0  ;  () -> sorted([nil]) -> 0  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 0  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 0  ;  (leq([b, a])) -> BOT -> 0  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 0
}


Solving took 30.005181 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6393, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6403, q_gen_6404, q_gen_6405, q_gen_6406, q_gen_6407, q_gen_6408, q_gen_6409, q_gen_6410, q_gen_6411, q_gen_6412, q_gen_6413, q_gen_6414, q_gen_6419, q_gen_6420, q_gen_6421, q_gen_6422, q_gen_6423, q_gen_6424, q_gen_6425, q_gen_6426, q_gen_6431, q_gen_6432, q_gen_6433, q_gen_6434, q_gen_6435, q_gen_6436, q_gen_6437, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444, q_gen_6450, q_gen_6451, q_gen_6452, q_gen_6453, q_gen_6458, q_gen_6459, q_gen_6460, q_gen_6461, q_gen_6462, q_gen_6463, q_gen_6464, q_gen_6465, q_gen_6470, q_gen_6471, q_gen_6472, q_gen_6473, q_gen_6474, q_gen_6475, q_gen_6476, q_gen_6477, q_gen_6478, q_gen_6482, q_gen_6483, q_gen_6484, q_gen_6485, q_gen_6486, q_gen_6489, q_gen_6490, q_gen_6491, q_gen_6492, q_gen_6493, q_gen_6494, q_gen_6495, q_gen_6496, q_gen_6497, q_gen_6498, q_gen_6499, q_gen_6500, q_gen_6503, q_gen_6504, q_gen_6505, q_gen_6506, q_gen_6507, q_gen_6508, q_gen_6509, q_gen_6510, q_gen_6511, q_gen_6512, q_gen_6513, q_gen_6514, q_gen_6518, q_gen_6519, q_gen_6520, q_gen_6521, q_gen_6522, q_gen_6523, q_gen_6524, q_gen_6525, q_gen_6526, q_gen_6532, q_gen_6533, q_gen_6534, q_gen_6535, q_gen_6536, q_gen_6537, q_gen_6538, q_gen_6539, q_gen_6540, q_gen_6541, q_gen_6542, q_gen_6543, q_gen_6544, q_gen_6545, q_gen_6546, q_gen_6547, q_gen_6548, q_gen_6549, q_gen_6550, q_gen_6551, q_gen_6552},
Q_f={},
Delta=
{
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6422
<cons>(q_gen_6422, q_gen_6411) -> q_gen_6434
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6496
<nil, nil>() -> q_gen_6394
<nil, b>() -> q_gen_6395
<b, nil>() -> q_gen_6396
<b, b>() -> q_gen_6397
<nil, a>() -> q_gen_6404
<a, nil>() -> q_gen_6405
<a, a>() -> q_gen_6406
<cons, cons>(q_gen_6406, q_gen_6405, q_gen_6404, q_gen_6394) -> q_gen_6409
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6410
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6413
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6420
<cons, b>(q_gen_6422, q_gen_6411) -> q_gen_6421
<b, cons>(q_gen_6422, q_gen_6411) -> q_gen_6423
<cons, a>(q_gen_6422, q_gen_6411) -> q_gen_6425
<a, cons>(q_gen_6422, q_gen_6411) -> q_gen_6426
<cons, cons>(q_gen_6397, q_gen_6423, q_gen_6421, q_gen_6420) -> q_gen_6432
<cons, b>(q_gen_6422, q_gen_6434) -> q_gen_6433
<b, cons>(q_gen_6422, q_gen_6434) -> q_gen_6435
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6452
<nil, cons>(q_gen_6422, q_gen_6434) -> q_gen_6465
<nil, cons>(q_gen_6422, q_gen_6411) -> q_gen_6478
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6492
<a, b>() -> q_gen_6493
<b, a>() -> q_gen_6506
<nil, nil, nil>() -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6393
<nil, cons, cons>(q_gen_6406, q_gen_6405, q_gen_6404, q_gen_6394) -> q_gen_6403
<cons, nil, cons>(q_gen_6406, q_gen_6405, q_gen_6404, q_gen_6394) -> q_gen_6407
<cons, nil, cons>(q_gen_6397, q_gen_6413, q_gen_6410, q_gen_6409) -> q_gen_6408
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6414
<nil, cons, cons>(q_gen_6397, q_gen_6423, q_gen_6421, q_gen_6420) -> q_gen_6419
<cons, nil, cons>(q_gen_6406, q_gen_6426, q_gen_6425, q_gen_6420) -> q_gen_6424
<nil, cons, cons>(q_gen_6397, q_gen_6435, q_gen_6433, q_gen_6432) -> q_gen_6431
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6437) -> q_gen_6436
<nil, nil, cons>(q_gen_6422, q_gen_6411) -> q_gen_6437
<nil, nil, b>() -> q_gen_6438
<nil, b, cons>(q_gen_6422, q_gen_6411) -> q_gen_6439
<nil, b, b>() -> q_gen_6440
<b, nil, cons>(q_gen_6422, q_gen_6411) -> q_gen_6441
<b, nil, b>() -> q_gen_6442
<b, b, cons>(q_gen_6422, q_gen_6411) -> q_gen_6443
<b, b, b>() -> q_gen_6444
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6450
<cons, nil, cons>(q_gen_6397, q_gen_6413, q_gen_6395, q_gen_6452) -> q_gen_6451
<nil, cons, cons>(q_gen_6397, q_gen_6413, q_gen_6395, q_gen_6452) -> q_gen_6453
<cons, cons, cons>(q_gen_6463, q_gen_6462, q_gen_6442, q_gen_6461, q_gen_6460, q_gen_6459, q_gen_6438, q_gen_6450) -> q_gen_6458
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6459
<nil, a, b>() -> q_gen_6460
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6461
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6462
<b, a, b>() -> q_gen_6463
<nil, cons, cons>(q_gen_6397, q_gen_6435, q_gen_6395, q_gen_6465) -> q_gen_6464
<cons, cons, cons>(q_gen_6476, q_gen_6475, q_gen_6474, q_gen_6473, q_gen_6472, q_gen_6439, q_gen_6471, q_gen_6437) -> q_gen_6470
<nil, nil, a>() -> q_gen_6471
<nil, b, a>() -> q_gen_6472
<a, nil, cons>(q_gen_6422, q_gen_6411) -> q_gen_6473
<a, nil, a>() -> q_gen_6474
<a, b, cons>(q_gen_6422, q_gen_6411) -> q_gen_6475
<a, b, a>() -> q_gen_6476
<nil, cons, cons>(q_gen_6406, q_gen_6426, q_gen_6404, q_gen_6478) -> q_gen_6477
<cons, cons, cons>(q_gen_6486, q_gen_6485, q_gen_6474, q_gen_6484, q_gen_6483, q_gen_6459, q_gen_6471, q_gen_6450) -> q_gen_6482
<nil, a, a>() -> q_gen_6483
<a, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6484
<a, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6485
<a, a, a>() -> q_gen_6486
<nil, cons, cons>(q_gen_6397, q_gen_6413, q_gen_6410, q_gen_6409) -> q_gen_6489
<cons, cons, cons>(q_gen_6444, q_gen_6499, q_gen_6498, q_gen_6497, q_gen_6440, q_gen_6495, q_gen_6494, q_gen_6491) -> q_gen_6490
<nil, cons, cons>(q_gen_6493, q_gen_6492, q_gen_6395, q_gen_6452) -> q_gen_6491
<nil, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6494
<nil, b, cons>(q_gen_6422, q_gen_6496) -> q_gen_6495
<b, cons, cons>(q_gen_6493, q_gen_6492, q_gen_6395, q_gen_6452) -> q_gen_6497
<b, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6498
<b, b, cons>(q_gen_6422, q_gen_6496) -> q_gen_6499
<nil, cons, cons>(q_gen_6493, q_gen_6405, q_gen_6395, q_gen_6394) -> q_gen_6500
<nil, cons, cons>(q_gen_6406, q_gen_6426, q_gen_6425, q_gen_6420) -> q_gen_6503
<cons, cons, cons>(q_gen_6486, q_gen_6511, q_gen_6510, q_gen_6509, q_gen_6483, q_gen_6508, q_gen_6507, q_gen_6505) -> q_gen_6504
<nil, cons, cons>(q_gen_6506, q_gen_6423, q_gen_6404, q_gen_6478) -> q_gen_6505
<nil, cons, a>(q_gen_6422, q_gen_6411) -> q_gen_6507
<nil, a, cons>(q_gen_6412, q_gen_6434) -> q_gen_6508
<a, cons, cons>(q_gen_6506, q_gen_6423, q_gen_6404, q_gen_6478) -> q_gen_6509
<a, cons, a>(q_gen_6422, q_gen_6411) -> q_gen_6510
<a, a, cons>(q_gen_6412, q_gen_6434) -> q_gen_6511
<cons, cons, cons>(q_gen_6486, q_gen_6514, q_gen_6474, q_gen_6473, q_gen_6483, q_gen_6513, q_gen_6471, q_gen_6437) -> q_gen_6512
<nil, a, cons>(q_gen_6422, q_gen_6411) -> q_gen_6513
<a, a, cons>(q_gen_6422, q_gen_6411) -> q_gen_6514
<cons, cons, cons>(q_gen_6444, q_gen_6524, q_gen_6442, q_gen_6523, q_gen_6522, q_gen_6521, q_gen_6520, q_gen_6519) -> q_gen_6518
<cons, nil, cons>(q_gen_6397, q_gen_6423, q_gen_6395, q_gen_6478) -> q_gen_6519
<cons, nil, b>(q_gen_6422, q_gen_6411) -> q_gen_6520
<cons, b, cons>(q_gen_6397, q_gen_6423, q_gen_6395, q_gen_6478) -> q_gen_6521
<cons, b, b>(q_gen_6422, q_gen_6411) -> q_gen_6522
<b, nil, cons>(q_gen_6422, q_gen_6434) -> q_gen_6523
<b, b, cons>(q_gen_6422, q_gen_6434) -> q_gen_6524
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6522, q_gen_6526, q_gen_6520, q_gen_6393) -> q_gen_6525
<cons, b, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6526
<cons, cons, cons>(q_gen_6463, q_gen_6533, q_gen_6442, q_gen_6441, q_gen_6460, q_gen_6513, q_gen_6438, q_gen_6437) -> q_gen_6532
<b, a, cons>(q_gen_6422, q_gen_6411) -> q_gen_6533
<cons, cons, cons>(q_gen_6463, q_gen_6537, q_gen_6442, q_gen_6523, q_gen_6536, q_gen_6535, q_gen_6520, q_gen_6519) -> q_gen_6534
<cons, a, cons>(q_gen_6397, q_gen_6423, q_gen_6395, q_gen_6478) -> q_gen_6535
<cons, a, b>(q_gen_6422, q_gen_6411) -> q_gen_6536
<b, a, cons>(q_gen_6422, q_gen_6434) -> q_gen_6537
<cons, cons, cons>(q_gen_6476, q_gen_6542, q_gen_6474, q_gen_6541, q_gen_6540, q_gen_6521, q_gen_6539, q_gen_6519) -> q_gen_6538
<cons, nil, a>(q_gen_6422, q_gen_6411) -> q_gen_6539
<cons, b, a>(q_gen_6422, q_gen_6411) -> q_gen_6540
<a, nil, cons>(q_gen_6422, q_gen_6434) -> q_gen_6541
<a, b, cons>(q_gen_6422, q_gen_6434) -> q_gen_6542
<cons, cons, cons>(q_gen_6486, q_gen_6545, q_gen_6474, q_gen_6541, q_gen_6544, q_gen_6535, q_gen_6539, q_gen_6519) -> q_gen_6543
<cons, a, a>(q_gen_6422, q_gen_6411) -> q_gen_6544
<a, a, cons>(q_gen_6422, q_gen_6434) -> q_gen_6545
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6549, q_gen_6548, q_gen_6440, q_gen_6439, q_gen_6547, q_gen_6414) -> q_gen_6546
<nil, cons, b>(q_gen_6422, q_gen_6411) -> q_gen_6547
<b, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6548
<b, cons, b>(q_gen_6422, q_gen_6411) -> q_gen_6549
<cons, cons, cons>(q_gen_6476, q_gen_6542, q_gen_6510, q_gen_6552, q_gen_6540, q_gen_6521, q_gen_6551, q_gen_6436) -> q_gen_6550
<cons, cons, a>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6551
<a, cons, cons>(q_gen_6397, q_gen_6423, q_gen_6395, q_gen_6478) -> q_gen_6552
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6390, q_gen_6391, q_gen_6401, q_gen_6402},
Q_f={},
Delta=
{
<nil>() -> q_gen_6389
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6390
<b>() -> q_gen_6391
<cons>(q_gen_6402, q_gen_6389) -> q_gen_6401
<a>() -> q_gen_6402
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6415, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6427, q_gen_6428, q_gen_6429, q_gen_6430, q_gen_6445, q_gen_6446, q_gen_6447, q_gen_6448, q_gen_6449, q_gen_6454, q_gen_6455, q_gen_6456, q_gen_6457, q_gen_6466, q_gen_6467, q_gen_6468, q_gen_6469, q_gen_6479, q_gen_6480, q_gen_6481, q_gen_6487, q_gen_6488, q_gen_6501, q_gen_6502, q_gen_6515, q_gen_6516, q_gen_6517, q_gen_6527, q_gen_6528, q_gen_6529, q_gen_6530, q_gen_6531},
Q_f={},
Delta=
{
<nil>() -> q_gen_6447
<b>() -> q_gen_6448
<a>() -> q_gen_6456
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6468
<nil, nil>() -> q_gen_6386
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6415
<nil, b>() -> q_gen_6416
<b, nil>() -> q_gen_6417
<b, b>() -> q_gen_6418
<cons, cons>(q_gen_6430, q_gen_6429, q_gen_6428, q_gen_6386) -> q_gen_6427
<nil, a>() -> q_gen_6428
<a, nil>() -> q_gen_6429
<a, a>() -> q_gen_6430
<cons, cons>(q_gen_6418, q_gen_6449, q_gen_6446, q_gen_6415) -> q_gen_6445
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6446
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6449
<cons, cons>(q_gen_6418, q_gen_6457, q_gen_6416, q_gen_6455) -> q_gen_6454
<nil, cons>(q_gen_6456, q_gen_6447) -> q_gen_6455
<b, cons>(q_gen_6456, q_gen_6447) -> q_gen_6457
<cons, cons>(q_gen_6418, q_gen_6469, q_gen_6416, q_gen_6467) -> q_gen_6466
<nil, cons>(q_gen_6448, q_gen_6468) -> q_gen_6467
<b, cons>(q_gen_6448, q_gen_6468) -> q_gen_6469
<cons, cons>(q_gen_6430, q_gen_6481, q_gen_6428, q_gen_6480) -> q_gen_6479
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6480
<a, cons>(q_gen_6448, q_gen_6447) -> q_gen_6481
<cons, cons>(q_gen_6488, q_gen_6449, q_gen_6428, q_gen_6480) -> q_gen_6487
<b, a>() -> q_gen_6488
<cons, cons>(q_gen_6502, q_gen_6429, q_gen_6416, q_gen_6386) -> q_gen_6501
<a, b>() -> q_gen_6502
<cons, cons>(q_gen_6488, q_gen_6417, q_gen_6428, q_gen_6386) -> q_gen_6515
<cons, cons>(q_gen_6430, q_gen_6481, q_gen_6517, q_gen_6415) -> q_gen_6516
<cons, a>(q_gen_6448, q_gen_6447) -> q_gen_6517
<cons, cons>(q_gen_6502, q_gen_6481, q_gen_6446, q_gen_6415) -> q_gen_6527
<cons, cons>(q_gen_6418, q_gen_6449, q_gen_6531, q_gen_6529) -> q_gen_6528
<cons, cons>(q_gen_6502, q_gen_6429, q_gen_6446, q_gen_6530) -> q_gen_6529
<cons, nil>(q_gen_6448, q_gen_6447) -> q_gen_6530
<cons, b>(q_gen_6456, q_gen_6468) -> q_gen_6531
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6384, q_gen_6385, q_gen_6398, q_gen_6399},
Q_f={},
Delta=
{
<nil>() -> q_gen_6383
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6384
<b>() -> q_gen_6385
<cons>(q_gen_6399, q_gen_6383) -> q_gen_6398
<a>() -> q_gen_6399
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004688 s (model generation: 0.003954,  model checking: 0.000734):

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

}

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

}

Datatype: <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
}}}
  ;  sorted -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> invsorted([cons(x, nil)]) -> 0  ;  () -> invsorted([nil]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> reverse([nil, nil]) -> 0  ;  () -> sorted([cons(x, nil)]) -> 0  ;  () -> sorted([nil]) -> 3  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Yes: (() -> sorted([nil]), {

})

-------------------------------------------
Step 1, which took 0.003543 s (model generation: 0.003500,  model checking: 0.000043):

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

}

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

}

Datatype: <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
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383},
Q_f={q_gen_6383},
Delta=
{
<nil>() -> q_gen_6383
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> invsorted([cons(x, nil)]) -> 0  ;  () -> invsorted([nil]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> reverse([nil, nil]) -> 0  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Yes: (() -> sorted([cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 2, which took 0.003515 s (model generation: 0.003458,  model checking: 0.000057):

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

}

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

}

Datatype: <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
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> invsorted([cons(x, nil)]) -> 0  ;  () -> invsorted([nil]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Yes: (() -> reverse([nil, nil]), {

})

-------------------------------------------
Step 3, which took 0.003529 s (model generation: 0.003510,  model checking: 0.000019):

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

}

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

}

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

}

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

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> invsorted([cons(x, nil)]) -> 0  ;  () -> invsorted([nil]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Yes: (() -> leq([b, b]), {

})

-------------------------------------------
Step 4, which took 0.003595 s (model generation: 0.003569,  model checking: 0.000026):

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

}

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

}

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

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

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> invsorted([cons(x, nil)]) -> 0  ;  () -> invsorted([nil]) -> 0  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Yes: (() -> leq([a, y]), {
y -> b
})

-------------------------------------------
Step 5, which took 0.004552 s (model generation: 0.004514,  model checking: 0.000038):

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

}

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

}

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

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

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> invsorted([cons(x, nil)]) -> 0  ;  () -> invsorted([nil]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Yes: (() -> invsorted([nil]), {

})

-------------------------------------------
Step 6, which took 0.006702 s (model generation: 0.006662,  model checking: 0.000040):

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

}

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

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

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

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> invsorted([cons(x, nil)]) -> 3  ;  () -> invsorted([nil]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Yes: (() -> invsorted([cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 7, which took 0.010162 s (model generation: 0.005003,  model checking: 0.005159):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<b>() -> q_gen_6391
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> invsorted([cons(x, nil)]) -> 3  ;  () -> invsorted([nil]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 8, which took 0.005865 s (model generation: 0.004165,  model checking: 0.001700):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<b>() -> q_gen_6391
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> invsorted([cons(x, nil)]) -> 3  ;  () -> invsorted([nil]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4  ;  (leq([b, a])) -> BOT -> 2  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 2
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 9, which took 0.011264 s (model generation: 0.011133,  model checking: 0.000131):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397},
Q_f={q_gen_6392},
Delta=
{
<nil, nil>() -> q_gen_6394
<nil, b>() -> q_gen_6395
<b, nil>() -> q_gen_6396
<b, b>() -> q_gen_6397
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<b>() -> q_gen_6391
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> invsorted([cons(x, nil)]) -> 3  ;  () -> invsorted([nil]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 6  ;  () -> sorted([nil]) -> 4  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 2  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4  ;  (leq([b, a])) -> BOT -> 3  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 3
}
Sat witness: Yes: (() -> sorted([cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 10, which took 0.012472 s (model generation: 0.011998,  model checking: 0.000474):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397},
Q_f={q_gen_6392},
Delta=
{
<nil, nil>() -> q_gen_6394
<nil, b>() -> q_gen_6395
<b, nil>() -> q_gen_6396
<b, b>() -> q_gen_6397
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<b>() -> q_gen_6391
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> invsorted([cons(x, nil)]) -> 3  ;  () -> invsorted([nil]) -> 3  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  () -> sorted([cons(x, nil)]) -> 6  ;  () -> sorted([nil]) -> 4  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 3  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4  ;  (leq([b, a])) -> BOT -> 4  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 4
}
Sat witness: Yes: (() -> leq([a, y]), {
y -> a
})

-------------------------------------------
Step 11, which took 0.011489 s (model generation: 0.011379,  model checking: 0.000110):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397},
Q_f={q_gen_6392},
Delta=
{
<nil, nil>() -> q_gen_6394
<nil, b>() -> q_gen_6395
<b, nil>() -> q_gen_6396
<b, b>() -> q_gen_6397
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<b>() -> q_gen_6391
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> invsorted([cons(x, nil)]) -> 6  ;  () -> invsorted([nil]) -> 4  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  () -> sorted([cons(x, nil)]) -> 6  ;  () -> sorted([nil]) -> 4  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 4  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4  ;  (leq([b, a])) -> BOT -> 4  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 4
}
Sat witness: Yes: (() -> invsorted([cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 12, which took 0.015407 s (model generation: 0.012002,  model checking: 0.003405):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397},
Q_f={q_gen_6392},
Delta=
{
<nil, nil>() -> q_gen_6394
<nil, b>() -> q_gen_6395
<b, nil>() -> q_gen_6396
<b, b>() -> q_gen_6397
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> invsorted([cons(x, nil)]) -> 6  ;  () -> invsorted([nil]) -> 4  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  () -> sorted([cons(x, nil)]) -> 6  ;  () -> sorted([nil]) -> 4  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 4  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4  ;  (leq([b, a])) -> BOT -> 4  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 4
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 13, which took 0.025988 s (model generation: 0.012955,  model checking: 0.013033):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397},
Q_f={q_gen_6392},
Delta=
{
<nil, nil>() -> q_gen_6394
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, nil>() -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> invsorted([cons(x, nil)]) -> 6  ;  () -> invsorted([nil]) -> 4  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  () -> sorted([cons(x, nil)]) -> 6  ;  () -> sorted([nil]) -> 4  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 4  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 7  ;  (leq([b, a])) -> BOT -> 5  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 5
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 14, which took 0.012860 s (model generation: 0.012418,  model checking: 0.000442):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412},
Q_f={q_gen_6392},
Delta=
{
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> invsorted([cons(x, nil)]) -> 6  ;  () -> invsorted([nil]) -> 4  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  () -> sorted([cons(x, nil)]) -> 6  ;  () -> sorted([nil]) -> 4  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 7  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 7  ;  (leq([b, a])) -> BOT -> 5  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 5
}
Sat witness: Yes: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> nil  ;  _jf -> cons(b, nil)  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.041252 s (model generation: 0.016255,  model checking: 0.024997):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412},
Q_f={q_gen_6392},
Delta=
{
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418},
Q_f={q_gen_6386},
Delta=
{
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<nil, b>() -> q_gen_6416
<b, nil>() -> q_gen_6417
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> invsorted([cons(x, nil)]) -> 7  ;  () -> invsorted([nil]) -> 5  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 5  ;  () -> reverse([nil, nil]) -> 5  ;  () -> sorted([cons(x, nil)]) -> 7  ;  () -> sorted([nil]) -> 5  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 7  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 7  ;  (leq([b, a])) -> BOT -> 6  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 6
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 16, which took 0.011745 s (model generation: 0.005489,  model checking: 0.006256):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412},
Q_f={q_gen_6392},
Delta=
{
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418},
Q_f={q_gen_6386},
Delta=
{
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<nil, b>() -> q_gen_6416
<b, nil>() -> q_gen_6417
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> invsorted([cons(x, nil)]) -> 7  ;  () -> invsorted([nil]) -> 6  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 6  ;  () -> reverse([nil, nil]) -> 6  ;  () -> sorted([cons(x, nil)]) -> 7  ;  () -> sorted([nil]) -> 6  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 7  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 10  ;  (leq([b, a])) -> BOT -> 7  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 7
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, nil)  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 17, which took 0.006631 s (model generation: 0.006140,  model checking: 0.000491):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412},
Q_f={q_gen_6392},
Delta=
{
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418},
Q_f={q_gen_6386},
Delta=
{
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<nil, b>() -> q_gen_6416
<b, nil>() -> q_gen_6417
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> invsorted([cons(x, nil)]) -> 7  ;  () -> invsorted([nil]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 7  ;  () -> reverse([nil, nil]) -> 7  ;  () -> sorted([cons(x, nil)]) -> 7  ;  () -> sorted([nil]) -> 7  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 10  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 10  ;  (leq([b, a])) -> BOT -> 8  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 8
}
Sat witness: Yes: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> nil  ;  _jf -> cons(a, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 18, which took 0.018029 s (model generation: 0.006414,  model checking: 0.011615):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412},
Q_f={q_gen_6392},
Delta=
{
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418},
Q_f={q_gen_6386},
Delta=
{
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, nil>() -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> invsorted([cons(x, nil)]) -> 8  ;  () -> invsorted([nil]) -> 8  ;  () -> leq([a, y]) -> 8  ;  () -> leq([b, b]) -> 8  ;  () -> reverse([nil, nil]) -> 8  ;  () -> sorted([cons(x, nil)]) -> 8  ;  () -> sorted([nil]) -> 8  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 10  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 10  ;  (leq([b, a])) -> BOT -> 9  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 9
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 19, which took 0.012001 s (model generation: 0.006750,  model checking: 0.005251):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418},
Q_f={q_gen_6386},
Delta=
{
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, nil>() -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> invsorted([cons(x, nil)]) -> 9  ;  () -> invsorted([nil]) -> 9  ;  () -> leq([a, y]) -> 9  ;  () -> leq([b, b]) -> 9  ;  () -> reverse([nil, nil]) -> 9  ;  () -> sorted([cons(x, nil)]) -> 9  ;  () -> sorted([nil]) -> 9  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 10  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 13  ;  (leq([b, a])) -> BOT -> 10  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 10
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 20, which took 0.009849 s (model generation: 0.007489,  model checking: 0.002360):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<nil, nil, b>() -> q_gen_6438
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, b>() -> q_gen_6440
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, nil, b>() -> q_gen_6442
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418},
Q_f={q_gen_6386},
Delta=
{
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, nil>() -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> invsorted([cons(x, nil)]) -> 10  ;  () -> invsorted([nil]) -> 10  ;  () -> leq([a, y]) -> 10  ;  () -> leq([b, b]) -> 10  ;  () -> reverse([nil, nil]) -> 10  ;  () -> sorted([cons(x, nil)]) -> 10  ;  () -> sorted([nil]) -> 10  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 13  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 13  ;  (leq([b, a])) -> BOT -> 11  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 11
}
Sat witness: Yes: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> cons(b, nil)  ;  _jf -> cons(b, cons(b, nil))  ;  h1 -> b  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 21, which took 0.048398 s (model generation: 0.008991,  model checking: 0.039407):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<nil, nil, b>() -> q_gen_6438
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, b>() -> q_gen_6440
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, nil, b>() -> q_gen_6442
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<nil>() -> q_gen_6447
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> invsorted([cons(x, nil)]) -> 11  ;  () -> invsorted([nil]) -> 11  ;  () -> leq([a, y]) -> 11  ;  () -> leq([b, b]) -> 11  ;  () -> reverse([nil, nil]) -> 11  ;  () -> sorted([cons(x, nil)]) -> 11  ;  () -> sorted([nil]) -> 11  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 13  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 16  ;  (leq([b, a])) -> BOT -> 12  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 12
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 22, which took 0.011835 s (model generation: 0.009267,  model checking: 0.002568):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<nil, nil, b>() -> q_gen_6438
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, b>() -> q_gen_6440
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, nil, b>() -> q_gen_6442
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<nil>() -> q_gen_6447
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> invsorted([cons(x, nil)]) -> 12  ;  () -> invsorted([nil]) -> 12  ;  () -> leq([a, y]) -> 12  ;  () -> leq([b, b]) -> 12  ;  () -> reverse([nil, nil]) -> 12  ;  () -> sorted([cons(x, nil)]) -> 12  ;  () -> sorted([nil]) -> 12  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 16  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 16  ;  (leq([b, a])) -> BOT -> 13  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 13
}
Sat witness: Yes: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> nil  ;  _jf -> cons(b, cons(a, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 0.086763 s (model generation: 0.009503,  model checking: 0.077260):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<nil, nil, b>() -> q_gen_6438
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, b>() -> q_gen_6440
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, nil, b>() -> q_gen_6442
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14  ;  () -> invsorted([cons(x, nil)]) -> 13  ;  () -> invsorted([nil]) -> 13  ;  () -> leq([a, y]) -> 13  ;  () -> leq([b, b]) -> 13  ;  () -> reverse([nil, nil]) -> 13  ;  () -> sorted([cons(x, nil)]) -> 13  ;  () -> sorted([nil]) -> 13  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 16  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 19  ;  (leq([b, a])) -> BOT -> 14  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 14
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 24, which took 0.015829 s (model generation: 0.011034,  model checking: 0.004795):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<nil, nil, b>() -> q_gen_6438
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, a, b>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, nil, b>() -> q_gen_6442
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  () -> invsorted([cons(x, nil)]) -> 14  ;  () -> invsorted([nil]) -> 14  ;  () -> leq([a, y]) -> 14  ;  () -> leq([b, b]) -> 14  ;  () -> reverse([nil, nil]) -> 14  ;  () -> sorted([cons(x, nil)]) -> 14  ;  () -> sorted([nil]) -> 14  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 19  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 19  ;  (leq([b, a])) -> BOT -> 15  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 15
}
Sat witness: Yes: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> nil  ;  _jf -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 25, which took 0.220570 s (model generation: 0.011533,  model checking: 0.209037):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<nil, nil, b>() -> q_gen_6438
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, a, b>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, nil, b>() -> q_gen_6442
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6447
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> invsorted([cons(x, nil)]) -> 15  ;  () -> invsorted([nil]) -> 15  ;  () -> leq([a, y]) -> 15  ;  () -> leq([b, b]) -> 15  ;  () -> reverse([nil, nil]) -> 15  ;  () -> sorted([cons(x, nil)]) -> 15  ;  () -> sorted([nil]) -> 15  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 19  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 22  ;  (leq([b, a])) -> BOT -> 16  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 16
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 26, which took 0.017987 s (model generation: 0.013017,  model checking: 0.004970):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<nil, nil, a>() -> q_gen_6438
<nil, nil, b>() -> q_gen_6438
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, a, b>() -> q_gen_6440
<nil, b, a>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<a, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<a, nil, a>() -> q_gen_6442
<b, nil, b>() -> q_gen_6442
<a, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, b, a>() -> q_gen_6444
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6447
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17  ;  () -> invsorted([cons(x, nil)]) -> 16  ;  () -> invsorted([nil]) -> 16  ;  () -> leq([a, y]) -> 16  ;  () -> leq([b, b]) -> 16  ;  () -> reverse([nil, nil]) -> 16  ;  () -> sorted([cons(x, nil)]) -> 16  ;  () -> sorted([nil]) -> 16  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 22  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 22  ;  (leq([b, a])) -> BOT -> 17  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 17
}
Sat witness: Yes: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> nil  ;  _jf -> cons(a, cons(b, nil))  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 27, which took 0.078465 s (model generation: 0.014372,  model checking: 0.064093):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<nil, nil, a>() -> q_gen_6438
<nil, nil, b>() -> q_gen_6438
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, a, b>() -> q_gen_6440
<nil, b, a>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<a, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<a, nil, a>() -> q_gen_6442
<b, nil, b>() -> q_gen_6442
<a, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, b, a>() -> q_gen_6444
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6447
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18  ;  () -> invsorted([cons(x, nil)]) -> 17  ;  () -> invsorted([nil]) -> 17  ;  () -> leq([a, y]) -> 17  ;  () -> leq([b, b]) -> 17  ;  () -> reverse([nil, nil]) -> 17  ;  () -> sorted([cons(x, nil)]) -> 17  ;  () -> sorted([nil]) -> 17  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 22  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 25  ;  (leq([b, a])) -> BOT -> 18  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 18
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 28, which took 0.019483 s (model generation: 0.015530,  model checking: 0.003953):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<nil, nil, a>() -> q_gen_6438
<nil, nil, b>() -> q_gen_6438
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, a, a>() -> q_gen_6440
<nil, a, b>() -> q_gen_6440
<nil, b, a>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<a, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<a, nil, a>() -> q_gen_6442
<b, nil, b>() -> q_gen_6442
<a, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, a, a>() -> q_gen_6444
<a, b, a>() -> q_gen_6444
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6447
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19  ;  () -> invsorted([cons(x, nil)]) -> 18  ;  () -> invsorted([nil]) -> 18  ;  () -> leq([a, y]) -> 18  ;  () -> leq([b, b]) -> 18  ;  () -> reverse([nil, nil]) -> 18  ;  () -> sorted([cons(x, nil)]) -> 18  ;  () -> sorted([nil]) -> 18  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 25  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 25  ;  (leq([b, a])) -> BOT -> 19  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 19
}
Sat witness: Yes: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> cons(a, nil)  ;  _jf -> cons(a, cons(b, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 29, which took 1.263693 s (model generation: 0.018839,  model checking: 1.244854):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<nil, nil, a>() -> q_gen_6438
<nil, nil, b>() -> q_gen_6438
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, a, a>() -> q_gen_6440
<nil, a, b>() -> q_gen_6440
<nil, b, a>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<a, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<a, nil, a>() -> q_gen_6442
<b, nil, b>() -> q_gen_6442
<a, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, a, a>() -> q_gen_6444
<a, b, a>() -> q_gen_6444
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6447
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<b, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20  ;  () -> invsorted([cons(x, nil)]) -> 19  ;  () -> invsorted([nil]) -> 19  ;  () -> leq([a, y]) -> 19  ;  () -> leq([b, b]) -> 19  ;  () -> reverse([nil, nil]) -> 19  ;  () -> sorted([cons(x, nil)]) -> 19  ;  () -> sorted([nil]) -> 19  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 25  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 28  ;  (leq([b, a])) -> BOT -> 20  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 20
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 30, which took 0.022811 s (model generation: 0.019649,  model checking: 0.003162):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<a, b>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<nil, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, nil, a>() -> q_gen_6438
<nil, nil, b>() -> q_gen_6438
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, a, a>() -> q_gen_6440
<nil, a, b>() -> q_gen_6440
<nil, b, a>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<a, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<a, nil, a>() -> q_gen_6442
<b, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6442
<b, nil, b>() -> q_gen_6442
<a, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, a, a>() -> q_gen_6444
<a, b, a>() -> q_gen_6444
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6447
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<b, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 21  ;  () -> invsorted([cons(x, nil)]) -> 20  ;  () -> invsorted([nil]) -> 20  ;  () -> leq([a, y]) -> 20  ;  () -> leq([b, b]) -> 20  ;  () -> reverse([nil, nil]) -> 20  ;  () -> sorted([cons(x, nil)]) -> 20  ;  () -> sorted([nil]) -> 20  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 28  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 28  ;  (leq([b, a])) -> BOT -> 21  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 21
}
Sat witness: Yes: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> nil  ;  _jf -> cons(b, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 31, which took 0.523714 s (model generation: 0.021367,  model checking: 0.502347):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<a, b>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<nil, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, nil, a>() -> q_gen_6438
<nil, nil, b>() -> q_gen_6438
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, a, a>() -> q_gen_6440
<nil, a, b>() -> q_gen_6440
<nil, b, a>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<a, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<a, nil, a>() -> q_gen_6442
<b, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6442
<b, nil, b>() -> q_gen_6442
<a, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, a, a>() -> q_gen_6444
<a, b, a>() -> q_gen_6444
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6447
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<a, b>() -> q_gen_6418
<b, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22  ;  () -> invsorted([cons(x, nil)]) -> 21  ;  () -> invsorted([nil]) -> 21  ;  () -> leq([a, y]) -> 21  ;  () -> leq([b, b]) -> 21  ;  () -> reverse([nil, nil]) -> 21  ;  () -> sorted([cons(x, nil)]) -> 21  ;  () -> sorted([nil]) -> 21  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 28  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 31  ;  (leq([b, a])) -> BOT -> 22  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 22
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 32, which took 0.031133 s (model generation: 0.026601,  model checking: 0.004532):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<a, b>() -> q_gen_6397
<b, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<nil, cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, nil, a>() -> q_gen_6438
<nil, nil, b>() -> q_gen_6438
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, a, a>() -> q_gen_6440
<nil, a, b>() -> q_gen_6440
<nil, b, a>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<a, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<a, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<a, cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6442
<a, nil, a>() -> q_gen_6442
<b, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6442
<b, nil, b>() -> q_gen_6442
<a, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, a, a>() -> q_gen_6444
<a, b, a>() -> q_gen_6444
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6447
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<a, b>() -> q_gen_6418
<b, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23  ;  () -> invsorted([cons(x, nil)]) -> 22  ;  () -> invsorted([nil]) -> 22  ;  () -> leq([a, y]) -> 22  ;  () -> leq([b, b]) -> 22  ;  () -> reverse([nil, nil]) -> 22  ;  () -> sorted([cons(x, nil)]) -> 22  ;  () -> sorted([nil]) -> 22  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 31  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 31  ;  (leq([b, a])) -> BOT -> 23  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 23
}
Sat witness: Yes: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> cons(a, nil)  ;  _jf -> cons(a, cons(b, nil))  ;  h1 -> a  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 33, which took 3.213752 s (model generation: 0.046456,  model checking: 3.167296):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<a, b>() -> q_gen_6397
<b, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<nil, cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, nil, a>() -> q_gen_6438
<nil, nil, b>() -> q_gen_6438
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, a, a>() -> q_gen_6440
<nil, a, b>() -> q_gen_6440
<nil, b, a>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<a, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<a, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<a, cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6442
<a, nil, a>() -> q_gen_6442
<b, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6442
<b, nil, b>() -> q_gen_6442
<a, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, a, a>() -> q_gen_6444
<a, b, a>() -> q_gen_6444
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6447
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, a>(q_gen_6448, q_gen_6447) -> q_gen_6416
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<a, b>() -> q_gen_6418
<b, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24  ;  () -> invsorted([cons(x, nil)]) -> 23  ;  () -> invsorted([nil]) -> 23  ;  () -> leq([a, y]) -> 23  ;  () -> leq([b, b]) -> 23  ;  () -> reverse([nil, nil]) -> 23  ;  () -> sorted([cons(x, nil)]) -> 23  ;  () -> sorted([nil]) -> 23  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 31  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 34  ;  (leq([b, a])) -> BOT -> 24  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 24
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 34, which took 0.053076 s (model generation: 0.048253,  model checking: 0.004823):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<a, b>() -> q_gen_6397
<b, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<cons, nil, b>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, nil, a>() -> q_gen_6438
<nil, nil, b>() -> q_gen_6438
<cons, b, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6439
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<cons, b, b>(q_gen_6412, q_gen_6411) -> q_gen_6440
<nil, a, a>() -> q_gen_6440
<nil, a, b>() -> q_gen_6440
<nil, b, a>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<a, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<a, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<a, cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6442
<a, nil, a>() -> q_gen_6442
<b, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6442
<b, nil, b>() -> q_gen_6442
<a, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, a, a>() -> q_gen_6444
<a, b, a>() -> q_gen_6444
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6447
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, a>(q_gen_6448, q_gen_6447) -> q_gen_6416
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<a, b>() -> q_gen_6418
<b, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 25  ;  () -> invsorted([cons(x, nil)]) -> 24  ;  () -> invsorted([nil]) -> 24  ;  () -> leq([a, y]) -> 24  ;  () -> leq([b, b]) -> 24  ;  () -> reverse([nil, nil]) -> 24  ;  () -> sorted([cons(x, nil)]) -> 24  ;  () -> sorted([nil]) -> 24  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 34  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 34  ;  (leq([b, a])) -> BOT -> 25  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 25
}
Sat witness: Yes: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> cons(b, cons(b, nil))  ;  _jf -> cons(b, cons(b, nil))  ;  h1 -> b  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 35, which took 1.772496 s (model generation: 0.085052,  model checking: 1.687444):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<a, b>() -> q_gen_6397
<b, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<cons, nil, b>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, nil, a>() -> q_gen_6438
<nil, nil, b>() -> q_gen_6438
<cons, b, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6439
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<cons, b, b>(q_gen_6412, q_gen_6411) -> q_gen_6440
<nil, a, a>() -> q_gen_6440
<nil, a, b>() -> q_gen_6440
<nil, b, a>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<a, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<a, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<a, cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6442
<a, nil, a>() -> q_gen_6442
<b, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6442
<b, nil, b>() -> q_gen_6442
<a, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, a, a>() -> q_gen_6444
<a, b, a>() -> q_gen_6444
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6447
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<cons, nil>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, a>(q_gen_6448, q_gen_6447) -> q_gen_6416
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<a, b>() -> q_gen_6418
<b, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26  ;  () -> invsorted([cons(x, nil)]) -> 25  ;  () -> invsorted([nil]) -> 25  ;  () -> leq([a, y]) -> 25  ;  () -> leq([b, b]) -> 25  ;  () -> reverse([nil, nil]) -> 25  ;  () -> sorted([cons(x, nil)]) -> 25  ;  () -> sorted([nil]) -> 25  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 34  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 37  ;  (leq([b, a])) -> BOT -> 26  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 26
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 36, which took 3.218720 s (model generation: 0.147525,  model checking: 3.071195):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<a, b>() -> q_gen_6397
<b, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<cons, nil, b>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, nil, a>() -> q_gen_6438
<nil, nil, b>() -> q_gen_6438
<cons, a, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6439
<cons, b, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6439
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<cons, a, b>(q_gen_6412, q_gen_6411) -> q_gen_6440
<cons, b, b>(q_gen_6412, q_gen_6411) -> q_gen_6440
<nil, a, a>() -> q_gen_6440
<nil, a, b>() -> q_gen_6440
<nil, b, a>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<a, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<a, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<a, cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6442
<a, nil, a>() -> q_gen_6442
<b, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6442
<b, nil, b>() -> q_gen_6442
<a, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, a, a>() -> q_gen_6444
<a, b, a>() -> q_gen_6444
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6447
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<cons, nil>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, a>(q_gen_6448, q_gen_6447) -> q_gen_6416
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<a, b>() -> q_gen_6418
<b, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27  ;  () -> invsorted([cons(x, nil)]) -> 26  ;  () -> invsorted([nil]) -> 26  ;  () -> leq([a, y]) -> 26  ;  () -> leq([b, b]) -> 26  ;  () -> reverse([nil, nil]) -> 26  ;  () -> sorted([cons(x, nil)]) -> 26  ;  () -> sorted([nil]) -> 26  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 35  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 40  ;  (leq([b, a])) -> BOT -> 27  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 27
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 37, which took 3.144935 s (model generation: 0.127331,  model checking: 3.017604):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<a, b>() -> q_gen_6397
<b, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<cons, nil, a>(q_gen_6412, q_gen_6411) -> q_gen_6438
<cons, nil, b>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, nil, a>() -> q_gen_6438
<nil, nil, b>() -> q_gen_6438
<cons, a, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6439
<cons, b, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6439
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<cons, a, b>(q_gen_6412, q_gen_6411) -> q_gen_6440
<cons, b, a>(q_gen_6412, q_gen_6411) -> q_gen_6440
<cons, b, b>(q_gen_6412, q_gen_6411) -> q_gen_6440
<nil, a, a>() -> q_gen_6440
<nil, a, b>() -> q_gen_6440
<nil, b, a>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<a, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<a, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<a, cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6442
<a, nil, a>() -> q_gen_6442
<b, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6442
<b, nil, b>() -> q_gen_6442
<a, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, a, a>() -> q_gen_6444
<a, b, a>() -> q_gen_6444
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6447
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<cons, nil>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, a>(q_gen_6448, q_gen_6447) -> q_gen_6416
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<a, b>() -> q_gen_6418
<b, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 28  ;  () -> invsorted([cons(x, nil)]) -> 27  ;  () -> invsorted([nil]) -> 27  ;  () -> leq([a, y]) -> 27  ;  () -> leq([b, b]) -> 27  ;  () -> reverse([nil, nil]) -> 27  ;  () -> sorted([cons(x, nil)]) -> 27  ;  () -> sorted([nil]) -> 27  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 36  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 43  ;  (leq([b, a])) -> BOT -> 28  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 28
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 38, which took 1.744499 s (model generation: 0.249392,  model checking: 1.495107):

Model:
|_
{
append -> 
{{{
Q={q_gen_6392, q_gen_6394, q_gen_6395, q_gen_6396, q_gen_6397, q_gen_6411, q_gen_6412, q_gen_6438, q_gen_6439, q_gen_6440, q_gen_6441, q_gen_6442, q_gen_6443, q_gen_6444},
Q_f={q_gen_6392},
Delta=
{
<cons>(q_gen_6412, q_gen_6411) -> q_gen_6411
<nil>() -> q_gen_6411
<a>() -> q_gen_6412
<b>() -> q_gen_6412
<cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6394
<nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6394
<nil, nil>() -> q_gen_6394
<cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6395
<cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6395
<nil, a>() -> q_gen_6395
<nil, b>() -> q_gen_6395
<a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<a, nil>() -> q_gen_6396
<b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6396
<b, nil>() -> q_gen_6396
<a, a>() -> q_gen_6397
<a, b>() -> q_gen_6397
<b, a>() -> q_gen_6397
<b, b>() -> q_gen_6397
<cons, cons, cons>(q_gen_6444, q_gen_6443, q_gen_6442, q_gen_6441, q_gen_6440, q_gen_6439, q_gen_6438, q_gen_6392) -> q_gen_6392
<cons, nil, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6392
<nil, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6392
<nil, nil, nil>() -> q_gen_6392
<cons, nil, a>(q_gen_6412, q_gen_6411) -> q_gen_6438
<cons, nil, b>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6438
<nil, nil, a>() -> q_gen_6438
<nil, nil, b>() -> q_gen_6438
<cons, a, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6439
<cons, b, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6439
<nil, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<nil, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6439
<cons, a, a>(q_gen_6412, q_gen_6411) -> q_gen_6440
<cons, a, b>(q_gen_6412, q_gen_6411) -> q_gen_6440
<cons, b, a>(q_gen_6412, q_gen_6411) -> q_gen_6440
<cons, b, b>(q_gen_6412, q_gen_6411) -> q_gen_6440
<nil, a, a>() -> q_gen_6440
<nil, a, b>() -> q_gen_6440
<nil, b, a>() -> q_gen_6440
<nil, b, b>() -> q_gen_6440
<a, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<a, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<b, cons, cons>(q_gen_6397, q_gen_6396, q_gen_6395, q_gen_6394) -> q_gen_6441
<b, nil, cons>(q_gen_6412, q_gen_6411) -> q_gen_6441
<a, cons, a>(q_gen_6412, q_gen_6411) -> q_gen_6442
<a, nil, a>() -> q_gen_6442
<b, cons, b>(q_gen_6412, q_gen_6411) -> q_gen_6442
<b, nil, b>() -> q_gen_6442
<a, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, a, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<b, b, cons>(q_gen_6412, q_gen_6411) -> q_gen_6443
<a, a, a>() -> q_gen_6444
<a, b, a>() -> q_gen_6444
<b, a, b>() -> q_gen_6444
<b, b, b>() -> q_gen_6444
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  invsorted -> 
{{{
Q={q_gen_6389, q_gen_6391},
Q_f={q_gen_6389},
Delta=
{
<cons>(q_gen_6391, q_gen_6389) -> q_gen_6389
<nil>() -> q_gen_6389
<a>() -> q_gen_6391
<b>() -> q_gen_6391
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_6386, q_gen_6416, q_gen_6417, q_gen_6418, q_gen_6447, q_gen_6448},
Q_f={q_gen_6386},
Delta=
{
<cons>(q_gen_6448, q_gen_6447) -> q_gen_6447
<nil>() -> q_gen_6447
<a>() -> q_gen_6448
<b>() -> q_gen_6448
<cons, cons>(q_gen_6418, q_gen_6417, q_gen_6416, q_gen_6386) -> q_gen_6386
<cons, nil>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, cons>(q_gen_6448, q_gen_6447) -> q_gen_6386
<nil, nil>() -> q_gen_6386
<cons, a>(q_gen_6448, q_gen_6447) -> q_gen_6416
<cons, b>(q_gen_6448, q_gen_6447) -> q_gen_6416
<nil, a>() -> q_gen_6416
<nil, b>() -> q_gen_6416
<a, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<a, nil>() -> q_gen_6417
<b, cons>(q_gen_6448, q_gen_6447) -> q_gen_6417
<b, nil>() -> q_gen_6417
<a, a>() -> q_gen_6418
<a, b>() -> q_gen_6418
<b, a>() -> q_gen_6418
<b, b>() -> q_gen_6418
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6383, q_gen_6385},
Q_f={q_gen_6383},
Delta=
{
<cons>(q_gen_6385, q_gen_6383) -> q_gen_6383
<nil>() -> q_gen_6383
<a>() -> q_gen_6385
<b>() -> q_gen_6385
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 29  ;  () -> invsorted([cons(x, nil)]) -> 28  ;  () -> invsorted([nil]) -> 28  ;  () -> leq([a, y]) -> 28  ;  () -> leq([b, b]) -> 28  ;  () -> reverse([nil, nil]) -> 28  ;  () -> sorted([cons(x, nil)]) -> 28  ;  () -> sorted([nil]) -> 28  ;  (append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 37  ;  (append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 46  ;  (leq([b, a])) -> BOT -> 29  ;  (reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 29
}
Sat witness: Yes: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(b, nil)
})

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