Solving ../../benchmarks/true/reverse_not_null.smt2...

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


Learning problem is:

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

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


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0  ;  () -> not_null([cons(x, ll)]) -> 0  ;  () -> reverse([nil, nil]) -> 0  ;  (append([_mb, cons(h1, nil), _nb]) /\ reverse([t1, _mb])) -> reverse([cons(h1, t1), _nb]) -> 0  ;  (append([t1, l2, _hb])) -> append([cons(h1, t1), l2, cons(h1, _hb)]) -> 0  ;  (not_null([l1]) /\ reverse([l1, _rb])) -> not_null([_rb]) -> 0  ;  (not_null([nil])) -> BOT -> 0
}


Solving took 30.003937 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5436, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5443, q_gen_5444, q_gen_5445, q_gen_5446, q_gen_5447, q_gen_5452, q_gen_5453, q_gen_5454, q_gen_5455, q_gen_5456, q_gen_5457, q_gen_5458, q_gen_5464, q_gen_5465, q_gen_5466, q_gen_5467, q_gen_5468, q_gen_5469, q_gen_5470, q_gen_5471, q_gen_5472, q_gen_5473, q_gen_5474, q_gen_5475, q_gen_5476, q_gen_5477, q_gen_5478, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485, q_gen_5491, q_gen_5492, q_gen_5493, q_gen_5494, q_gen_5499, q_gen_5500, q_gen_5501, q_gen_5502, q_gen_5503, q_gen_5504, q_gen_5505, q_gen_5506, q_gen_5511, q_gen_5512, q_gen_5513, q_gen_5514, q_gen_5515, q_gen_5516, q_gen_5517, q_gen_5518, q_gen_5519, q_gen_5523, q_gen_5524, q_gen_5525, q_gen_5526, q_gen_5527, q_gen_5530, q_gen_5531, q_gen_5532, q_gen_5533, q_gen_5534, q_gen_5535, q_gen_5536, q_gen_5537, q_gen_5538, q_gen_5539, q_gen_5540, q_gen_5541, q_gen_5544, q_gen_5545, q_gen_5546, q_gen_5547, q_gen_5548, q_gen_5549, q_gen_5550, q_gen_5551, q_gen_5552, q_gen_5556, q_gen_5557, q_gen_5558, q_gen_5559, q_gen_5560, q_gen_5561, q_gen_5562, q_gen_5563, q_gen_5564, q_gen_5570, q_gen_5571, q_gen_5572, q_gen_5573, q_gen_5574, q_gen_5575, q_gen_5576, q_gen_5577, q_gen_5578, q_gen_5579, q_gen_5580, q_gen_5581, q_gen_5582, q_gen_5583, q_gen_5584, q_gen_5585, q_gen_5586, q_gen_5587, q_gen_5588, q_gen_5589, q_gen_5590, q_gen_5591},
Q_f={},
Delta=
{
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5467
<cons>(q_gen_5467, q_gen_5456) -> q_gen_5475
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5537
<nil, nil>() -> q_gen_5437
<nil, b>() -> q_gen_5438
<b, nil>() -> q_gen_5439
<b, b>() -> q_gen_5440
<nil, a>() -> q_gen_5444
<a, nil>() -> q_gen_5445
<a, a>() -> q_gen_5446
<cons, cons>(q_gen_5446, q_gen_5445, q_gen_5444, q_gen_5437) -> q_gen_5454
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5455
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5458
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5465
<cons, b>(q_gen_5467, q_gen_5456) -> q_gen_5466
<b, cons>(q_gen_5467, q_gen_5456) -> q_gen_5468
<cons, a>(q_gen_5467, q_gen_5456) -> q_gen_5470
<a, cons>(q_gen_5467, q_gen_5456) -> q_gen_5471
<cons, cons>(q_gen_5440, q_gen_5468, q_gen_5466, q_gen_5465) -> q_gen_5473
<cons, b>(q_gen_5467, q_gen_5475) -> q_gen_5474
<b, cons>(q_gen_5467, q_gen_5475) -> q_gen_5476
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5493
<nil, cons>(q_gen_5467, q_gen_5475) -> q_gen_5506
<nil, cons>(q_gen_5467, q_gen_5456) -> q_gen_5519
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5533
<a, b>() -> q_gen_5534
<b, a>() -> q_gen_5547
<nil, nil, nil>() -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5436
<nil, cons, cons>(q_gen_5446, q_gen_5445, q_gen_5444, q_gen_5437) -> q_gen_5443
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5447
<cons, nil, cons>(q_gen_5446, q_gen_5445, q_gen_5444, q_gen_5437) -> q_gen_5452
<cons, nil, cons>(q_gen_5440, q_gen_5458, q_gen_5455, q_gen_5454) -> q_gen_5453
<nil, cons, cons>(q_gen_5440, q_gen_5468, q_gen_5466, q_gen_5465) -> q_gen_5464
<cons, nil, cons>(q_gen_5446, q_gen_5471, q_gen_5470, q_gen_5465) -> q_gen_5469
<nil, cons, cons>(q_gen_5440, q_gen_5476, q_gen_5474, q_gen_5473) -> q_gen_5472
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5478) -> q_gen_5477
<nil, nil, cons>(q_gen_5467, q_gen_5456) -> q_gen_5478
<nil, nil, b>() -> q_gen_5479
<nil, b, cons>(q_gen_5467, q_gen_5456) -> q_gen_5480
<nil, b, b>() -> q_gen_5481
<b, nil, cons>(q_gen_5467, q_gen_5456) -> q_gen_5482
<b, nil, b>() -> q_gen_5483
<b, b, cons>(q_gen_5467, q_gen_5456) -> q_gen_5484
<b, b, b>() -> q_gen_5485
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5491
<cons, nil, cons>(q_gen_5440, q_gen_5458, q_gen_5438, q_gen_5493) -> q_gen_5492
<nil, cons, cons>(q_gen_5440, q_gen_5458, q_gen_5438, q_gen_5493) -> q_gen_5494
<cons, cons, cons>(q_gen_5504, q_gen_5503, q_gen_5483, q_gen_5502, q_gen_5501, q_gen_5500, q_gen_5479, q_gen_5491) -> q_gen_5499
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5500
<nil, a, b>() -> q_gen_5501
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5502
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5503
<b, a, b>() -> q_gen_5504
<nil, cons, cons>(q_gen_5440, q_gen_5476, q_gen_5438, q_gen_5506) -> q_gen_5505
<cons, cons, cons>(q_gen_5517, q_gen_5516, q_gen_5515, q_gen_5514, q_gen_5513, q_gen_5480, q_gen_5512, q_gen_5478) -> q_gen_5511
<nil, nil, a>() -> q_gen_5512
<nil, b, a>() -> q_gen_5513
<a, nil, cons>(q_gen_5467, q_gen_5456) -> q_gen_5514
<a, nil, a>() -> q_gen_5515
<a, b, cons>(q_gen_5467, q_gen_5456) -> q_gen_5516
<a, b, a>() -> q_gen_5517
<nil, cons, cons>(q_gen_5446, q_gen_5471, q_gen_5444, q_gen_5519) -> q_gen_5518
<cons, cons, cons>(q_gen_5527, q_gen_5526, q_gen_5515, q_gen_5525, q_gen_5524, q_gen_5500, q_gen_5512, q_gen_5491) -> q_gen_5523
<nil, a, a>() -> q_gen_5524
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5525
<a, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5526
<a, a, a>() -> q_gen_5527
<nil, cons, cons>(q_gen_5440, q_gen_5458, q_gen_5455, q_gen_5454) -> q_gen_5530
<cons, cons, cons>(q_gen_5485, q_gen_5540, q_gen_5539, q_gen_5538, q_gen_5481, q_gen_5536, q_gen_5535, q_gen_5532) -> q_gen_5531
<nil, cons, cons>(q_gen_5534, q_gen_5533, q_gen_5438, q_gen_5493) -> q_gen_5532
<nil, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5535
<nil, b, cons>(q_gen_5467, q_gen_5537) -> q_gen_5536
<b, cons, cons>(q_gen_5534, q_gen_5533, q_gen_5438, q_gen_5493) -> q_gen_5538
<b, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5539
<b, b, cons>(q_gen_5467, q_gen_5537) -> q_gen_5540
<nil, cons, cons>(q_gen_5534, q_gen_5445, q_gen_5438, q_gen_5437) -> q_gen_5541
<nil, cons, cons>(q_gen_5446, q_gen_5471, q_gen_5470, q_gen_5465) -> q_gen_5544
<cons, cons, cons>(q_gen_5527, q_gen_5552, q_gen_5551, q_gen_5550, q_gen_5524, q_gen_5549, q_gen_5548, q_gen_5546) -> q_gen_5545
<nil, cons, cons>(q_gen_5547, q_gen_5468, q_gen_5444, q_gen_5519) -> q_gen_5546
<nil, cons, a>(q_gen_5467, q_gen_5456) -> q_gen_5548
<nil, a, cons>(q_gen_5457, q_gen_5475) -> q_gen_5549
<a, cons, cons>(q_gen_5547, q_gen_5468, q_gen_5444, q_gen_5519) -> q_gen_5550
<a, cons, a>(q_gen_5467, q_gen_5456) -> q_gen_5551
<a, a, cons>(q_gen_5457, q_gen_5475) -> q_gen_5552
<cons, cons, cons>(q_gen_5485, q_gen_5562, q_gen_5483, q_gen_5561, q_gen_5560, q_gen_5559, q_gen_5558, q_gen_5557) -> q_gen_5556
<cons, nil, cons>(q_gen_5440, q_gen_5468, q_gen_5438, q_gen_5519) -> q_gen_5557
<cons, nil, b>(q_gen_5467, q_gen_5456) -> q_gen_5558
<cons, b, cons>(q_gen_5440, q_gen_5468, q_gen_5438, q_gen_5519) -> q_gen_5559
<cons, b, b>(q_gen_5467, q_gen_5456) -> q_gen_5560
<b, nil, cons>(q_gen_5467, q_gen_5475) -> q_gen_5561
<b, b, cons>(q_gen_5467, q_gen_5475) -> q_gen_5562
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5560, q_gen_5564, q_gen_5558, q_gen_5436) -> q_gen_5563
<cons, b, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5564
<cons, cons, cons>(q_gen_5504, q_gen_5572, q_gen_5483, q_gen_5482, q_gen_5501, q_gen_5571, q_gen_5479, q_gen_5478) -> q_gen_5570
<nil, a, cons>(q_gen_5467, q_gen_5456) -> q_gen_5571
<b, a, cons>(q_gen_5467, q_gen_5456) -> q_gen_5572
<cons, cons, cons>(q_gen_5504, q_gen_5576, q_gen_5483, q_gen_5561, q_gen_5575, q_gen_5574, q_gen_5558, q_gen_5557) -> q_gen_5573
<cons, a, cons>(q_gen_5440, q_gen_5468, q_gen_5438, q_gen_5519) -> q_gen_5574
<cons, a, b>(q_gen_5467, q_gen_5456) -> q_gen_5575
<b, a, cons>(q_gen_5467, q_gen_5475) -> q_gen_5576
<cons, cons, cons>(q_gen_5517, q_gen_5581, q_gen_5515, q_gen_5580, q_gen_5579, q_gen_5559, q_gen_5578, q_gen_5557) -> q_gen_5577
<cons, nil, a>(q_gen_5467, q_gen_5456) -> q_gen_5578
<cons, b, a>(q_gen_5467, q_gen_5456) -> q_gen_5579
<a, nil, cons>(q_gen_5467, q_gen_5475) -> q_gen_5580
<a, b, cons>(q_gen_5467, q_gen_5475) -> q_gen_5581
<cons, cons, cons>(q_gen_5527, q_gen_5584, q_gen_5515, q_gen_5580, q_gen_5583, q_gen_5574, q_gen_5578, q_gen_5557) -> q_gen_5582
<cons, a, a>(q_gen_5467, q_gen_5456) -> q_gen_5583
<a, a, cons>(q_gen_5467, q_gen_5475) -> q_gen_5584
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5588, q_gen_5587, q_gen_5481, q_gen_5480, q_gen_5586, q_gen_5447) -> q_gen_5585
<nil, cons, b>(q_gen_5467, q_gen_5456) -> q_gen_5586
<b, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5587
<b, cons, b>(q_gen_5467, q_gen_5456) -> q_gen_5588
<cons, cons, cons>(q_gen_5517, q_gen_5581, q_gen_5551, q_gen_5591, q_gen_5579, q_gen_5559, q_gen_5590, q_gen_5477) -> q_gen_5589
<cons, cons, a>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5590
<a, cons, cons>(q_gen_5440, q_gen_5468, q_gen_5438, q_gen_5519) -> q_gen_5591
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434, q_gen_5441, q_gen_5442, q_gen_5463},
Q_f={},
Delta=
{
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<b>() -> q_gen_5434
<cons>(q_gen_5442, q_gen_5433) -> q_gen_5441
<a>() -> q_gen_5442
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5463
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5448, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5459, q_gen_5460, q_gen_5461, q_gen_5462, q_gen_5486, q_gen_5487, q_gen_5488, q_gen_5489, q_gen_5490, q_gen_5495, q_gen_5496, q_gen_5497, q_gen_5498, q_gen_5507, q_gen_5508, q_gen_5509, q_gen_5510, q_gen_5520, q_gen_5521, q_gen_5522, q_gen_5528, q_gen_5529, q_gen_5542, q_gen_5543, q_gen_5553, q_gen_5554, q_gen_5555, q_gen_5565, q_gen_5566, q_gen_5567, q_gen_5568, q_gen_5569},
Q_f={},
Delta=
{
<nil>() -> q_gen_5488
<b>() -> q_gen_5489
<a>() -> q_gen_5497
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5509
<nil, nil>() -> q_gen_5431
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5448
<nil, b>() -> q_gen_5449
<b, nil>() -> q_gen_5450
<b, b>() -> q_gen_5451
<cons, cons>(q_gen_5462, q_gen_5461, q_gen_5460, q_gen_5431) -> q_gen_5459
<nil, a>() -> q_gen_5460
<a, nil>() -> q_gen_5461
<a, a>() -> q_gen_5462
<cons, cons>(q_gen_5451, q_gen_5490, q_gen_5487, q_gen_5448) -> q_gen_5486
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5487
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5490
<cons, cons>(q_gen_5451, q_gen_5498, q_gen_5449, q_gen_5496) -> q_gen_5495
<nil, cons>(q_gen_5497, q_gen_5488) -> q_gen_5496
<b, cons>(q_gen_5497, q_gen_5488) -> q_gen_5498
<cons, cons>(q_gen_5451, q_gen_5510, q_gen_5449, q_gen_5508) -> q_gen_5507
<nil, cons>(q_gen_5489, q_gen_5509) -> q_gen_5508
<b, cons>(q_gen_5489, q_gen_5509) -> q_gen_5510
<cons, cons>(q_gen_5462, q_gen_5522, q_gen_5460, q_gen_5521) -> q_gen_5520
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5521
<a, cons>(q_gen_5489, q_gen_5488) -> q_gen_5522
<cons, cons>(q_gen_5529, q_gen_5490, q_gen_5460, q_gen_5521) -> q_gen_5528
<b, a>() -> q_gen_5529
<cons, cons>(q_gen_5543, q_gen_5461, q_gen_5449, q_gen_5431) -> q_gen_5542
<a, b>() -> q_gen_5543
<cons, cons>(q_gen_5529, q_gen_5450, q_gen_5460, q_gen_5431) -> q_gen_5553
<cons, cons>(q_gen_5529, q_gen_5490, q_gen_5555, q_gen_5448) -> q_gen_5554
<cons, a>(q_gen_5489, q_gen_5488) -> q_gen_5555
<cons, cons>(q_gen_5543, q_gen_5522, q_gen_5487, q_gen_5448) -> q_gen_5565
<cons, cons>(q_gen_5451, q_gen_5490, q_gen_5569, q_gen_5567) -> q_gen_5566
<cons, cons>(q_gen_5543, q_gen_5461, q_gen_5487, q_gen_5568) -> q_gen_5567
<cons, nil>(q_gen_5489, q_gen_5488) -> q_gen_5568
<cons, b>(q_gen_5497, q_gen_5509) -> q_gen_5569
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004461 s (model generation: 0.003806,  model checking: 0.000655):

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

}

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

}

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

}

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

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

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

})

-------------------------------------------
Step 1, which took 0.004004 s (model generation: 0.003927,  model checking: 0.000077):

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

}

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

}

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

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

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

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

-------------------------------------------
Step 2, which took 0.006425 s (model generation: 0.005576,  model checking: 0.000849):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<nil>() -> q_gen_5432
<b>() -> q_gen_5434
}

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

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

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

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

-------------------------------------------
Step 3, which took 0.005688 s (model generation: 0.005672,  model checking: 0.000016):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<nil>() -> q_gen_5432
<b>() -> q_gen_5434
}

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

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

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

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

})

-------------------------------------------
Step 4, which took 0.009036 s (model generation: 0.006988,  model checking: 0.002048):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<b>() -> q_gen_5434
}

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

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

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

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

-------------------------------------------
Step 5, which took 0.012394 s (model generation: 0.011705,  model checking: 0.000689):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440},
Q_f={q_gen_5435},
Delta=
{
<nil, nil>() -> q_gen_5437
<nil, b>() -> q_gen_5438
<b, nil>() -> q_gen_5439
<b, b>() -> q_gen_5440
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<b>() -> q_gen_5434
}

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

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

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

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

-------------------------------------------
Step 6, which took 0.011865 s (model generation: 0.010459,  model checking: 0.001406):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440},
Q_f={q_gen_5435},
Delta=
{
<nil, nil>() -> q_gen_5437
<nil, b>() -> q_gen_5438
<b, nil>() -> q_gen_5439
<b, b>() -> q_gen_5440
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

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

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

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

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

-------------------------------------------
Step 7, which took 0.011105 s (model generation: 0.010923,  model checking: 0.000182):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440},
Q_f={q_gen_5435},
Delta=
{
<nil, nil>() -> q_gen_5437
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, nil>() -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

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

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

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

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

-------------------------------------------
Step 8, which took 0.015007 s (model generation: 0.006885,  model checking: 0.008122):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440},
Q_f={q_gen_5435},
Delta=
{
<nil, nil>() -> q_gen_5437
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, nil>() -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451},
Q_f={q_gen_5431},
Delta=
{
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<nil, b>() -> q_gen_5449
<b, nil>() -> q_gen_5450
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 9, which took 0.008702 s (model generation: 0.008087,  model checking: 0.000615):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457},
Q_f={q_gen_5435},
Delta=
{
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451},
Q_f={q_gen_5431},
Delta=
{
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<nil, b>() -> q_gen_5449
<b, nil>() -> q_gen_5450
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 10, which took 0.009560 s (model generation: 0.009329,  model checking: 0.000231):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457},
Q_f={q_gen_5435},
Delta=
{
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451},
Q_f={q_gen_5431},
Delta=
{
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, nil>() -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 11, which took 0.030726 s (model generation: 0.008812,  model checking: 0.021914):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457},
Q_f={q_gen_5435},
Delta=
{
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451},
Q_f={q_gen_5431},
Delta=
{
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, nil>() -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 12, which took 0.010925 s (model generation: 0.005599,  model checking: 0.005326):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457},
Q_f={q_gen_5435},
Delta=
{
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451},
Q_f={q_gen_5431},
Delta=
{
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, nil>() -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 13, which took 0.015426 s (model generation: 0.005841,  model checking: 0.009585):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457},
Q_f={q_gen_5435},
Delta=
{
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451},
Q_f={q_gen_5431},
Delta=
{
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, nil>() -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 14, which took 0.010775 s (model generation: 0.006609,  model checking: 0.004166):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451},
Q_f={q_gen_5431},
Delta=
{
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, nil>() -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 15, which took 0.009340 s (model generation: 0.007365,  model checking: 0.001975):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<nil, nil, b>() -> q_gen_5479
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, b>() -> q_gen_5481
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, nil, b>() -> q_gen_5483
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451},
Q_f={q_gen_5431},
Delta=
{
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, nil>() -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 16, which took 0.042917 s (model generation: 0.009043,  model checking: 0.033874):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<nil, nil, b>() -> q_gen_5479
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, b>() -> q_gen_5481
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, nil, b>() -> q_gen_5483
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<nil>() -> q_gen_5488
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 17, which took 0.010788 s (model generation: 0.008834,  model checking: 0.001954):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<nil, nil, b>() -> q_gen_5479
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, b>() -> q_gen_5481
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, nil, b>() -> q_gen_5483
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<nil>() -> q_gen_5488
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 18, which took 0.082302 s (model generation: 0.009526,  model checking: 0.072776):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<nil, nil, b>() -> q_gen_5479
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, b>() -> q_gen_5481
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, nil, b>() -> q_gen_5483
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 19, which took 0.015202 s (model generation: 0.010751,  model checking: 0.004451):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<nil, nil, b>() -> q_gen_5479
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, a, b>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, nil, b>() -> q_gen_5483
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 20, which took 0.235840 s (model generation: 0.011640,  model checking: 0.224200):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<nil, nil, b>() -> q_gen_5479
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, a, b>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, nil, b>() -> q_gen_5483
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 21, which took 0.017817 s (model generation: 0.013282,  model checking: 0.004535):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<nil, nil, a>() -> q_gen_5479
<nil, nil, b>() -> q_gen_5479
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, a, b>() -> q_gen_5481
<nil, b, a>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<a, nil, a>() -> q_gen_5483
<b, nil, b>() -> q_gen_5483
<a, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, b, a>() -> q_gen_5485
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 22, which took 0.077797 s (model generation: 0.014437,  model checking: 0.063360):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<nil, nil, a>() -> q_gen_5479
<nil, nil, b>() -> q_gen_5479
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, a, b>() -> q_gen_5481
<nil, b, a>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<a, nil, a>() -> q_gen_5483
<b, nil, b>() -> q_gen_5483
<a, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, b, a>() -> q_gen_5485
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 23, which took 0.019277 s (model generation: 0.015765,  model checking: 0.003512):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<nil, nil, a>() -> q_gen_5479
<nil, nil, b>() -> q_gen_5479
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, a, a>() -> q_gen_5481
<nil, a, b>() -> q_gen_5481
<nil, b, a>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<a, nil, a>() -> q_gen_5483
<b, nil, b>() -> q_gen_5483
<a, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, a, a>() -> q_gen_5485
<a, b, a>() -> q_gen_5485
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 24, which took 2.034164 s (model generation: 0.019128,  model checking: 2.015036):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<nil, nil, a>() -> q_gen_5479
<nil, nil, b>() -> q_gen_5479
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, a, a>() -> q_gen_5481
<nil, a, b>() -> q_gen_5481
<nil, b, a>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<a, nil, a>() -> q_gen_5483
<b, nil, b>() -> q_gen_5483
<a, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, a, a>() -> q_gen_5485
<a, b, a>() -> q_gen_5485
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 25, which took 0.022924 s (model generation: 0.019794,  model checking: 0.003130):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<a, b>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<nil, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, nil, a>() -> q_gen_5479
<nil, nil, b>() -> q_gen_5479
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, a, a>() -> q_gen_5481
<nil, a, b>() -> q_gen_5481
<nil, b, a>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<a, nil, a>() -> q_gen_5483
<b, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5483
<b, nil, b>() -> q_gen_5483
<a, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, a, a>() -> q_gen_5485
<a, b, a>() -> q_gen_5485
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<b, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 26, which took 0.528003 s (model generation: 0.021308,  model checking: 0.506695):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<a, b>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<nil, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, nil, a>() -> q_gen_5479
<nil, nil, b>() -> q_gen_5479
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, a, a>() -> q_gen_5481
<nil, a, b>() -> q_gen_5481
<nil, b, a>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<a, nil, a>() -> q_gen_5483
<b, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5483
<b, nil, b>() -> q_gen_5483
<a, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, a, a>() -> q_gen_5485
<a, b, a>() -> q_gen_5485
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<a, b>() -> q_gen_5451
<b, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 27, which took 0.030937 s (model generation: 0.026662,  model checking: 0.004275):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<a, b>() -> q_gen_5440
<b, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<nil, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, nil, a>() -> q_gen_5479
<nil, nil, b>() -> q_gen_5479
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, a, a>() -> q_gen_5481
<nil, a, b>() -> q_gen_5481
<nil, b, a>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<a, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<a, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5483
<a, nil, a>() -> q_gen_5483
<b, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5483
<b, nil, b>() -> q_gen_5483
<a, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, a, a>() -> q_gen_5485
<a, b, a>() -> q_gen_5485
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<a, b>() -> q_gen_5451
<b, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 28, which took 3.415127 s (model generation: 0.140500,  model checking: 3.274627):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<a, b>() -> q_gen_5440
<b, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<nil, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, nil, a>() -> q_gen_5479
<nil, nil, b>() -> q_gen_5479
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, a, a>() -> q_gen_5481
<nil, a, b>() -> q_gen_5481
<nil, b, a>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<a, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<a, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5483
<a, nil, a>() -> q_gen_5483
<b, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5483
<b, nil, b>() -> q_gen_5483
<a, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, a, a>() -> q_gen_5485
<a, b, a>() -> q_gen_5485
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, a>(q_gen_5489, q_gen_5488) -> q_gen_5449
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<a, b>() -> q_gen_5451
<b, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 29, which took 0.072227 s (model generation: 0.066590,  model checking: 0.005637):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<a, b>() -> q_gen_5440
<b, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<cons, nil, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, nil, a>() -> q_gen_5479
<nil, nil, b>() -> q_gen_5479
<cons, b, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5480
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<cons, b, b>(q_gen_5457, q_gen_5456) -> q_gen_5481
<nil, a, a>() -> q_gen_5481
<nil, a, b>() -> q_gen_5481
<nil, b, a>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<a, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<a, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5483
<a, nil, a>() -> q_gen_5483
<b, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5483
<b, nil, b>() -> q_gen_5483
<a, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, a, a>() -> q_gen_5485
<a, b, a>() -> q_gen_5485
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, a>(q_gen_5489, q_gen_5488) -> q_gen_5449
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<a, b>() -> q_gen_5451
<b, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 30, which took 0.243389 s (model generation: 0.243160,  model checking: 0.000229):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<a, b>() -> q_gen_5440
<b, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<cons, nil, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, nil, a>() -> q_gen_5479
<nil, nil, b>() -> q_gen_5479
<cons, b, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5480
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<cons, b, b>(q_gen_5457, q_gen_5456) -> q_gen_5481
<nil, a, a>() -> q_gen_5481
<nil, a, b>() -> q_gen_5481
<nil, b, a>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<a, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<a, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5483
<a, nil, a>() -> q_gen_5483
<b, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5483
<b, nil, b>() -> q_gen_5483
<a, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, a, a>() -> q_gen_5485
<a, b, a>() -> q_gen_5485
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<cons, nil>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, a>(q_gen_5489, q_gen_5488) -> q_gen_5449
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<a, b>() -> q_gen_5451
<b, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
}

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

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

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

-------------------------------------------
Step 31, which took 1.607333 s (model generation: 0.078254,  model checking: 1.529079):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<a, b>() -> q_gen_5440
<b, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<cons, nil, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, nil, a>() -> q_gen_5479
<nil, nil, b>() -> q_gen_5479
<cons, b, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5480
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<cons, b, b>(q_gen_5457, q_gen_5456) -> q_gen_5481
<nil, a, a>() -> q_gen_5481
<nil, a, b>() -> q_gen_5481
<nil, b, a>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<a, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<a, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5483
<a, nil, a>() -> q_gen_5483
<b, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5483
<b, nil, b>() -> q_gen_5483
<a, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, a, a>() -> q_gen_5485
<a, b, a>() -> q_gen_5485
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489, q_gen_5568},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5568) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, a>(q_gen_5489, q_gen_5488) -> q_gen_5449
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<a, b>() -> q_gen_5451
<b, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
<cons, nil>(q_gen_5489, q_gen_5488) -> q_gen_5568
}

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

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

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

-------------------------------------------
Step 32, which took 3.219798 s (model generation: 0.186310,  model checking: 3.033488):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<a, b>() -> q_gen_5440
<b, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<cons, nil, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, nil, a>() -> q_gen_5479
<nil, nil, b>() -> q_gen_5479
<cons, a, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5480
<cons, b, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5480
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<cons, a, b>(q_gen_5457, q_gen_5456) -> q_gen_5481
<cons, b, b>(q_gen_5457, q_gen_5456) -> q_gen_5481
<nil, a, a>() -> q_gen_5481
<nil, a, b>() -> q_gen_5481
<nil, b, a>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<a, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<a, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5483
<a, nil, a>() -> q_gen_5483
<b, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5483
<b, nil, b>() -> q_gen_5483
<a, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, a, a>() -> q_gen_5485
<a, b, a>() -> q_gen_5485
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489, q_gen_5568},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5568) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, a>(q_gen_5489, q_gen_5488) -> q_gen_5449
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<a, b>() -> q_gen_5451
<b, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
<cons, nil>(q_gen_5489, q_gen_5488) -> q_gen_5568
}

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

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

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

-------------------------------------------
Step 33, which took 3.256327 s (model generation: 0.185625,  model checking: 3.070702):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<a, b>() -> q_gen_5440
<b, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<cons, nil, a>(q_gen_5457, q_gen_5456) -> q_gen_5479
<cons, nil, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, nil, a>() -> q_gen_5479
<nil, nil, b>() -> q_gen_5479
<cons, a, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5480
<cons, b, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5480
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<cons, a, b>(q_gen_5457, q_gen_5456) -> q_gen_5481
<cons, b, a>(q_gen_5457, q_gen_5456) -> q_gen_5481
<cons, b, b>(q_gen_5457, q_gen_5456) -> q_gen_5481
<nil, a, a>() -> q_gen_5481
<nil, a, b>() -> q_gen_5481
<nil, b, a>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<a, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<a, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5483
<a, nil, a>() -> q_gen_5483
<b, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5483
<b, nil, b>() -> q_gen_5483
<a, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, a, a>() -> q_gen_5485
<a, b, a>() -> q_gen_5485
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489, q_gen_5568},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5568) -> q_gen_5431
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, a>(q_gen_5489, q_gen_5488) -> q_gen_5449
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<a, b>() -> q_gen_5451
<b, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
<cons, nil>(q_gen_5489, q_gen_5488) -> q_gen_5568
}

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

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

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

-------------------------------------------
Step 34, which took 1.730152 s (model generation: 0.200613,  model checking: 1.529539):

Model:
|_
{
append -> 
{{{
Q={q_gen_5435, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5456, q_gen_5457, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485},
Q_f={q_gen_5435},
Delta=
{
<cons>(q_gen_5457, q_gen_5456) -> q_gen_5456
<nil>() -> q_gen_5456
<a>() -> q_gen_5457
<b>() -> q_gen_5457
<cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5437
<nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5437
<nil, nil>() -> q_gen_5437
<cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5438
<cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5438
<nil, a>() -> q_gen_5438
<nil, b>() -> q_gen_5438
<a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<a, nil>() -> q_gen_5439
<b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5439
<b, nil>() -> q_gen_5439
<a, a>() -> q_gen_5440
<a, b>() -> q_gen_5440
<b, a>() -> q_gen_5440
<b, b>() -> q_gen_5440
<cons, cons, cons>(q_gen_5485, q_gen_5484, q_gen_5483, q_gen_5482, q_gen_5481, q_gen_5480, q_gen_5479, q_gen_5435) -> q_gen_5435
<cons, nil, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5435
<nil, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5435
<nil, nil, nil>() -> q_gen_5435
<cons, nil, a>(q_gen_5457, q_gen_5456) -> q_gen_5479
<cons, nil, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5479
<nil, nil, a>() -> q_gen_5479
<nil, nil, b>() -> q_gen_5479
<cons, a, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5480
<cons, b, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5480
<nil, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<nil, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5480
<cons, a, a>(q_gen_5457, q_gen_5456) -> q_gen_5481
<cons, a, b>(q_gen_5457, q_gen_5456) -> q_gen_5481
<cons, b, a>(q_gen_5457, q_gen_5456) -> q_gen_5481
<cons, b, b>(q_gen_5457, q_gen_5456) -> q_gen_5481
<nil, a, a>() -> q_gen_5481
<nil, a, b>() -> q_gen_5481
<nil, b, a>() -> q_gen_5481
<nil, b, b>() -> q_gen_5481
<a, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<a, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<b, cons, cons>(q_gen_5440, q_gen_5439, q_gen_5438, q_gen_5437) -> q_gen_5482
<b, nil, cons>(q_gen_5457, q_gen_5456) -> q_gen_5482
<a, cons, a>(q_gen_5457, q_gen_5456) -> q_gen_5483
<a, nil, a>() -> q_gen_5483
<b, cons, b>(q_gen_5457, q_gen_5456) -> q_gen_5483
<b, nil, b>() -> q_gen_5483
<a, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, a, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<b, b, cons>(q_gen_5457, q_gen_5456) -> q_gen_5484
<a, a, a>() -> q_gen_5485
<a, b, a>() -> q_gen_5485
<b, a, b>() -> q_gen_5485
<b, b, b>() -> q_gen_5485
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_5432, q_gen_5433, q_gen_5434},
Q_f={q_gen_5432},
Delta=
{
<cons>(q_gen_5434, q_gen_5432) -> q_gen_5432
<cons>(q_gen_5434, q_gen_5433) -> q_gen_5432
<nil>() -> q_gen_5433
<a>() -> q_gen_5434
<b>() -> q_gen_5434
}

Datatype: <eltlist>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_5431, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5488, q_gen_5489, q_gen_5496},
Q_f={q_gen_5431},
Delta=
{
<cons>(q_gen_5489, q_gen_5488) -> q_gen_5488
<nil>() -> q_gen_5488
<a>() -> q_gen_5489
<b>() -> q_gen_5489
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5431) -> q_gen_5431
<cons, cons>(q_gen_5451, q_gen_5450, q_gen_5449, q_gen_5496) -> q_gen_5431
<nil, nil>() -> q_gen_5431
<cons, a>(q_gen_5489, q_gen_5488) -> q_gen_5449
<cons, b>(q_gen_5489, q_gen_5488) -> q_gen_5449
<nil, a>() -> q_gen_5449
<nil, b>() -> q_gen_5449
<a, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<a, nil>() -> q_gen_5450
<b, cons>(q_gen_5489, q_gen_5488) -> q_gen_5450
<b, nil>() -> q_gen_5450
<a, a>() -> q_gen_5451
<a, b>() -> q_gen_5451
<b, a>() -> q_gen_5451
<b, b>() -> q_gen_5451
<cons, nil>(q_gen_5489, q_gen_5488) -> q_gen_5496
<nil, cons>(q_gen_5489, q_gen_5488) -> q_gen_5496
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 29  ;  () -> not_null([cons(x, ll)]) -> 29  ;  () -> reverse([nil, nil]) -> 29  ;  (append([_mb, cons(h1, nil), _nb]) /\ reverse([t1, _mb])) -> reverse([cons(h1, t1), _nb]) -> 37  ;  (append([t1, l2, _hb])) -> append([cons(h1, t1), l2, cons(h1, _hb)]) -> 46  ;  (not_null([l1]) /\ reverse([l1, _rb])) -> not_null([_rb]) -> 32  ;  (not_null([nil])) -> BOT -> 30
}
Sat witness: Yes: ((append([t1, l2, _hb])) -> append([cons(h1, t1), l2, cons(h1, _hb)]), {
_hb -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(b, nil)
})

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