Solving ../../benchmarks/true/length_reverse_eq.smt2...

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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)])}
(append([_ge, _he, _ie]) /\ append([_ge, _he, _je])) -> eq_eltlist([_ie, _je])
)
(reverse, F:
{() -> reverse([nil, nil])
(append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le])}
(reverse([_me, _ne]) /\ reverse([_me, _oe])) -> eq_eltlist([_ne, _oe])
)
(length, F:
{() -> length([nil, z])
(length([ll, _pe])) -> length([cons(x, ll), s(_pe)])}
(length([_qe, _re]) /\ length([_qe, _se])) -> eq_nat([_re, _se])
)
}

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


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

Clause system for inference is:

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


Solving took 30.004329 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3404, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3409, q_gen_3410, q_gen_3411, q_gen_3412, q_gen_3413, q_gen_3420, q_gen_3421, q_gen_3422, q_gen_3423, q_gen_3424, q_gen_3425, q_gen_3426, q_gen_3431, q_gen_3432, q_gen_3433, q_gen_3434, q_gen_3435, q_gen_3439, q_gen_3440, q_gen_3441, q_gen_3442, q_gen_3443, q_gen_3444, q_gen_3445, q_gen_3446, q_gen_3449, q_gen_3450, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457, q_gen_3467, q_gen_3468, q_gen_3469, q_gen_3470, q_gen_3476, q_gen_3477, q_gen_3478, q_gen_3479, q_gen_3480, q_gen_3481, q_gen_3482, q_gen_3483, q_gen_3489, q_gen_3490, q_gen_3491, q_gen_3492, q_gen_3493, q_gen_3494, q_gen_3495, q_gen_3496, q_gen_3497, q_gen_3498, q_gen_3499, q_gen_3500, q_gen_3501, q_gen_3502, q_gen_3503, q_gen_3504, q_gen_3505, q_gen_3506, q_gen_3508, q_gen_3509, q_gen_3510, q_gen_3511, q_gen_3512, q_gen_3513, q_gen_3514, q_gen_3518, q_gen_3519, q_gen_3520, q_gen_3521, q_gen_3522, q_gen_3523, q_gen_3524, q_gen_3525, q_gen_3526, q_gen_3527, q_gen_3528, q_gen_3529, q_gen_3533, q_gen_3534, q_gen_3535, q_gen_3536, q_gen_3537, q_gen_3538, q_gen_3539, q_gen_3540, q_gen_3541, q_gen_3542, q_gen_3543, q_gen_3544, q_gen_3545, q_gen_3546},
Q_f={},
Delta=
{
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3434
<cons>(q_gen_3434, q_gen_3424) -> q_gen_3445
<cons>(q_gen_3425, q_gen_3445) -> q_gen_3524
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3540
<nil, nil>() -> q_gen_3405
<nil, b>() -> q_gen_3406
<b, nil>() -> q_gen_3407
<b, b>() -> q_gen_3408
<nil, a>() -> q_gen_3410
<a, nil>() -> q_gen_3411
<a, a>() -> q_gen_3412
<cons, cons>(q_gen_3412, q_gen_3411, q_gen_3410, q_gen_3405) -> q_gen_3422
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3423
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3426
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3432
<cons, b>(q_gen_3434, q_gen_3424) -> q_gen_3433
<b, cons>(q_gen_3434, q_gen_3424) -> q_gen_3435
<cons, a>(q_gen_3434, q_gen_3424) -> q_gen_3440
<a, cons>(q_gen_3434, q_gen_3424) -> q_gen_3441
<cons, cons>(q_gen_3408, q_gen_3435, q_gen_3433, q_gen_3432) -> q_gen_3443
<cons, b>(q_gen_3434, q_gen_3445) -> q_gen_3444
<b, cons>(q_gen_3434, q_gen_3445) -> q_gen_3446
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3469
<nil, cons>(q_gen_3434, q_gen_3445) -> q_gen_3483
<nil, cons>(q_gen_3434, q_gen_3424) -> q_gen_3497
<cons, cons>(q_gen_3408, q_gen_3435, q_gen_3406, q_gen_3497) -> q_gen_3500
<a, cons>(q_gen_3434, q_gen_3445) -> q_gen_3501
<cons, a>(q_gen_3434, q_gen_3445) -> q_gen_3509
<cons, cons>(q_gen_3412, q_gen_3522, q_gen_3521, q_gen_3520) -> q_gen_3519
<cons, cons>(q_gen_3412, q_gen_3441, q_gen_3440, q_gen_3432) -> q_gen_3520
<cons, a>(q_gen_3425, q_gen_3445) -> q_gen_3521
<a, cons>(q_gen_3425, q_gen_3445) -> q_gen_3522
<cons, b>(q_gen_3425, q_gen_3524) -> q_gen_3523
<b, cons>(q_gen_3425, q_gen_3524) -> q_gen_3525
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3536
<a, b>() -> q_gen_3537
<nil, nil, nil>() -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3404
<nil, cons, cons>(q_gen_3412, q_gen_3411, q_gen_3410, q_gen_3405) -> q_gen_3409
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3413
<cons, nil, cons>(q_gen_3412, q_gen_3411, q_gen_3410, q_gen_3405) -> q_gen_3420
<cons, nil, cons>(q_gen_3408, q_gen_3426, q_gen_3423, q_gen_3422) -> q_gen_3421
<nil, cons, cons>(q_gen_3408, q_gen_3435, q_gen_3433, q_gen_3432) -> q_gen_3431
<cons, nil, cons>(q_gen_3412, q_gen_3441, q_gen_3440, q_gen_3432) -> q_gen_3439
<nil, cons, cons>(q_gen_3408, q_gen_3446, q_gen_3444, q_gen_3443) -> q_gen_3442
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3450) -> q_gen_3449
<nil, nil, cons>(q_gen_3434, q_gen_3424) -> q_gen_3450
<nil, nil, b>() -> q_gen_3451
<nil, b, cons>(q_gen_3434, q_gen_3424) -> q_gen_3452
<nil, b, b>() -> q_gen_3453
<b, nil, cons>(q_gen_3434, q_gen_3424) -> q_gen_3454
<b, nil, b>() -> q_gen_3455
<b, b, cons>(q_gen_3434, q_gen_3424) -> q_gen_3456
<b, b, b>() -> q_gen_3457
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3467
<cons, nil, cons>(q_gen_3408, q_gen_3426, q_gen_3406, q_gen_3469) -> q_gen_3468
<nil, cons, cons>(q_gen_3408, q_gen_3426, q_gen_3406, q_gen_3469) -> q_gen_3470
<cons, cons, cons>(q_gen_3481, q_gen_3480, q_gen_3455, q_gen_3479, q_gen_3478, q_gen_3477, q_gen_3451, q_gen_3467) -> q_gen_3476
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3477
<nil, a, b>() -> q_gen_3478
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3479
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3480
<b, a, b>() -> q_gen_3481
<nil, cons, cons>(q_gen_3408, q_gen_3446, q_gen_3406, q_gen_3483) -> q_gen_3482
<cons, cons, cons>(q_gen_3495, q_gen_3494, q_gen_3493, q_gen_3492, q_gen_3491, q_gen_3452, q_gen_3490, q_gen_3450) -> q_gen_3489
<nil, nil, a>() -> q_gen_3490
<nil, b, a>() -> q_gen_3491
<a, nil, cons>(q_gen_3434, q_gen_3424) -> q_gen_3492
<a, nil, a>() -> q_gen_3493
<a, b, cons>(q_gen_3434, q_gen_3424) -> q_gen_3494
<a, b, a>() -> q_gen_3495
<nil, cons, cons>(q_gen_3408, q_gen_3435, q_gen_3406, q_gen_3497) -> q_gen_3496
<cons, nil, cons>(q_gen_3408, q_gen_3435, q_gen_3406, q_gen_3497) -> q_gen_3498
<cons, nil, cons>(q_gen_3412, q_gen_3501, q_gen_3440, q_gen_3500) -> q_gen_3499
<cons, cons, cons>(q_gen_3457, q_gen_3506, q_gen_3455, q_gen_3505, q_gen_3453, q_gen_3504, q_gen_3451, q_gen_3503) -> q_gen_3502
<nil, nil, cons>(q_gen_3434, q_gen_3445) -> q_gen_3503
<nil, b, cons>(q_gen_3434, q_gen_3445) -> q_gen_3504
<b, nil, cons>(q_gen_3434, q_gen_3445) -> q_gen_3505
<b, b, cons>(q_gen_3434, q_gen_3445) -> q_gen_3506
<nil, cons, cons>(q_gen_3412, q_gen_3501, q_gen_3509, q_gen_3443) -> q_gen_3508
<cons, nil, cons>(q_gen_3408, q_gen_3446, q_gen_3406, q_gen_3483) -> q_gen_3510
<cons, cons, cons>(q_gen_3495, q_gen_3514, q_gen_3493, q_gen_3513, q_gen_3491, q_gen_3512, q_gen_3490, q_gen_3467) -> q_gen_3511
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3512
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3513
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3514
<nil, cons, cons>(q_gen_3408, q_gen_3525, q_gen_3523, q_gen_3519) -> q_gen_3518
<cons, cons, cons>(q_gen_3529, q_gen_3528, q_gen_3493, q_gen_3513, q_gen_3527, q_gen_3477, q_gen_3490, q_gen_3467) -> q_gen_3526
<nil, a, a>() -> q_gen_3527
<a, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3528
<a, a, a>() -> q_gen_3529
<nil, cons, cons>(q_gen_3408, q_gen_3426, q_gen_3423, q_gen_3422) -> q_gen_3533
<cons, cons, cons>(q_gen_3457, q_gen_3543, q_gen_3542, q_gen_3541, q_gen_3453, q_gen_3539, q_gen_3538, q_gen_3535) -> q_gen_3534
<nil, cons, cons>(q_gen_3537, q_gen_3536, q_gen_3406, q_gen_3469) -> q_gen_3535
<nil, cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3538
<nil, b, cons>(q_gen_3434, q_gen_3540) -> q_gen_3539
<b, cons, cons>(q_gen_3537, q_gen_3536, q_gen_3406, q_gen_3469) -> q_gen_3541
<b, cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3542
<b, b, cons>(q_gen_3434, q_gen_3540) -> q_gen_3543
<cons, cons, cons>(q_gen_3529, q_gen_3546, q_gen_3493, q_gen_3492, q_gen_3527, q_gen_3545, q_gen_3490, q_gen_3450) -> q_gen_3544
<nil, a, cons>(q_gen_3434, q_gen_3424) -> q_gen_3545
<a, a, cons>(q_gen_3434, q_gen_3424) -> q_gen_3546
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3402, q_gen_3403, q_gen_3418, q_gen_3419, q_gen_3436, q_gen_3437, q_gen_3438, q_gen_3447, q_gen_3448, q_gen_3463, q_gen_3464, q_gen_3465, q_gen_3466},
Q_f={},
Delta=
{
<z>() -> q_gen_3438
<s>(q_gen_3438) -> q_gen_3466
<nil, z>() -> q_gen_3400
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3402
<b, z>() -> q_gen_3403
<cons, s>(q_gen_3419, q_gen_3400) -> q_gen_3418
<a, z>() -> q_gen_3419
<cons, s>(q_gen_3437, q_gen_3418) -> q_gen_3436
<b, s>(q_gen_3438) -> q_gen_3437
<cons, s>(q_gen_3448, q_gen_3402) -> q_gen_3447
<a, s>(q_gen_3438) -> q_gen_3448
<cons, s>(q_gen_3437, q_gen_3402) -> q_gen_3463
<cons, s>(q_gen_3465, q_gen_3463) -> q_gen_3464
<b, s>(q_gen_3466) -> q_gen_3465
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3414, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3427, q_gen_3428, q_gen_3429, q_gen_3430, q_gen_3458, q_gen_3459, q_gen_3460, q_gen_3461, q_gen_3462, q_gen_3471, q_gen_3472, q_gen_3473, q_gen_3474, q_gen_3475, q_gen_3484, q_gen_3485, q_gen_3486, q_gen_3487, q_gen_3488, q_gen_3507, q_gen_3515, q_gen_3516, q_gen_3517, q_gen_3530, q_gen_3531, q_gen_3532, q_gen_3547, q_gen_3548, q_gen_3549, q_gen_3550},
Q_f={},
Delta=
{
<nil>() -> q_gen_3460
<b>() -> q_gen_3461
<a>() -> q_gen_3473
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3486
<nil, nil>() -> q_gen_3399
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3414
<nil, b>() -> q_gen_3415
<b, nil>() -> q_gen_3416
<b, b>() -> q_gen_3417
<cons, cons>(q_gen_3430, q_gen_3429, q_gen_3428, q_gen_3399) -> q_gen_3427
<nil, a>() -> q_gen_3428
<a, nil>() -> q_gen_3429
<a, a>() -> q_gen_3430
<cons, cons>(q_gen_3417, q_gen_3462, q_gen_3459, q_gen_3414) -> q_gen_3458
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3459
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3462
<cons, cons>(q_gen_3417, q_gen_3474, q_gen_3415, q_gen_3472) -> q_gen_3471
<nil, cons>(q_gen_3473, q_gen_3460) -> q_gen_3472
<b, cons>(q_gen_3473, q_gen_3460) -> q_gen_3474
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3475
<cons, cons>(q_gen_3417, q_gen_3487, q_gen_3415, q_gen_3485) -> q_gen_3484
<nil, cons>(q_gen_3461, q_gen_3486) -> q_gen_3485
<b, cons>(q_gen_3461, q_gen_3486) -> q_gen_3487
<cons, cons>(q_gen_3417, q_gen_3462, q_gen_3415, q_gen_3475) -> q_gen_3488
<cons, cons>(q_gen_3417, q_gen_3487, q_gen_3459, q_gen_3488) -> q_gen_3507
<cons, cons>(q_gen_3517, q_gen_3474, q_gen_3516, q_gen_3427) -> q_gen_3515
<cons, a>(q_gen_3473, q_gen_3460) -> q_gen_3516
<b, a>() -> q_gen_3517
<cons, cons>(q_gen_3517, q_gen_3462, q_gen_3516, q_gen_3531) -> q_gen_3530
<cons, cons>(q_gen_3532, q_gen_3429, q_gen_3415, q_gen_3399) -> q_gen_3531
<a, b>() -> q_gen_3532
<cons, cons>(q_gen_3517, q_gen_3416, q_gen_3428, q_gen_3399) -> q_gen_3547
<cons, cons>(q_gen_3430, q_gen_3550, q_gen_3549, q_gen_3414) -> q_gen_3548
<cons, a>(q_gen_3461, q_gen_3460) -> q_gen_3549
<a, cons>(q_gen_3461, q_gen_3460) -> q_gen_3550
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.011102 s (model generation: 0.009864,  model checking: 0.001238):

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> reverse([nil, nil]) -> 3  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 1  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 1  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 1  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 1
}
Sat witness: Yes: (() -> reverse([nil, nil]), {

})

-------------------------------------------
Step 1, which took 0.011105 s (model generation: 0.009981,  model checking: 0.001124):

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> length([nil, z]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 1  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 1  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 1  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 1
}
Sat witness: Yes: (() -> length([nil, z]), {

})

-------------------------------------------
Step 2, which took 0.011635 s (model generation: 0.010691,  model checking: 0.000944):

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

}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 1  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 1  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 1  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 1
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 3, which took 0.010963 s (model generation: 0.010716,  model checking: 0.000247):

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 1  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 1  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 1  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 4
}
Sat witness: Yes: ((length([ll, _pe])) -> length([cons(x, ll), s(_pe)]), {
_pe -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 4, which took 0.013410 s (model generation: 0.010771,  model checking: 0.002639):

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> reverse([nil, nil]) -> 3  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 1  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 4  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 2  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 4
}
Sat witness: Yes: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.015367 s (model generation: 0.011014,  model checking: 0.004353):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408},
Q_f={q_gen_3401},
Delta=
{
<nil, nil>() -> q_gen_3405
<nil, b>() -> q_gen_3406
<b, nil>() -> q_gen_3407
<b, b>() -> q_gen_3408
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> length([nil, z]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 2  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 4  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 3  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 4
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 6, which took 0.012155 s (model generation: 0.011717,  model checking: 0.000438):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408},
Q_f={q_gen_3401},
Delta=
{
<nil, nil>() -> q_gen_3405
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, nil>() -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> length([nil, z]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 5  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 4  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 3  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 4
}
Sat witness: Yes: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> nil  ;  _le -> cons(b, nil)  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.013939 s (model generation: 0.013460,  model checking: 0.000479):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408},
Q_f={q_gen_3401},
Delta=
{
<nil, nil>() -> q_gen_3405
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, nil>() -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417},
Q_f={q_gen_3399},
Delta=
{
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<nil, b>() -> q_gen_3415
<b, nil>() -> q_gen_3416
<b, b>() -> q_gen_3417
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> length([nil, z]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 5  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 4  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 4  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 7
}
Sat witness: Yes: ((length([ll, _pe])) -> length([cons(x, ll), s(_pe)]), {
_pe -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 8, which took 0.023767 s (model generation: 0.013161,  model checking: 0.010606):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408},
Q_f={q_gen_3401},
Delta=
{
<nil, nil>() -> q_gen_3405
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, nil>() -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417},
Q_f={q_gen_3399},
Delta=
{
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<nil, b>() -> q_gen_3415
<b, nil>() -> q_gen_3416
<b, b>() -> q_gen_3417
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> length([nil, z]) -> 4  ;  () -> reverse([nil, nil]) -> 4  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 5  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 7  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 5  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 7
}
Sat witness: Yes: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 9, which took 0.016099 s (model generation: 0.014365,  model checking: 0.001734):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425},
Q_f={q_gen_3401},
Delta=
{
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417},
Q_f={q_gen_3399},
Delta=
{
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<nil, b>() -> q_gen_3415
<b, nil>() -> q_gen_3416
<b, b>() -> q_gen_3417
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> length([nil, z]) -> 5  ;  () -> reverse([nil, nil]) -> 5  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 8  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 7  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 6  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 7
}
Sat witness: Yes: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> nil  ;  _le -> cons(a, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.035758 s (model generation: 0.014747,  model checking: 0.021011):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425},
Q_f={q_gen_3401},
Delta=
{
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417},
Q_f={q_gen_3399},
Delta=
{
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> length([nil, z]) -> 6  ;  () -> reverse([nil, nil]) -> 6  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 8  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 7  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 7  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 7
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 11, which took 0.005867 s (model generation: 0.005497,  model checking: 0.000370):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425},
Q_f={q_gen_3401},
Delta=
{
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417},
Q_f={q_gen_3399},
Delta=
{
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> length([nil, z]) -> 7  ;  () -> reverse([nil, nil]) -> 7  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 8  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 7  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 7  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 10
}
Sat witness: Yes: ((length([ll, _pe])) -> length([cons(x, ll), s(_pe)]), {
_pe -> s(z)  ;  ll -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 12, which took 0.021158 s (model generation: 0.010460,  model checking: 0.010698):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425},
Q_f={q_gen_3401},
Delta=
{
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417},
Q_f={q_gen_3399},
Delta=
{
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> length([nil, z]) -> 7  ;  () -> reverse([nil, nil]) -> 7  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 8  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 10  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 8  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 10
}
Sat witness: Yes: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, nil)  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 13, which took 0.022834 s (model generation: 0.009065,  model checking: 0.013769):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425},
Q_f={q_gen_3401},
Delta=
{
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417},
Q_f={q_gen_3399},
Delta=
{
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> length([nil, z]) -> 8  ;  () -> reverse([nil, nil]) -> 8  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 9  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 10  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 9  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 10
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 14, which took 0.008080 s (model generation: 0.006849,  model checking: 0.001231):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417},
Q_f={q_gen_3399},
Delta=
{
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> length([nil, z]) -> 9  ;  () -> reverse([nil, nil]) -> 9  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 10  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 10  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 10  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 13
}
Sat witness: Yes: ((length([ll, _pe])) -> length([cons(x, ll), s(_pe)]), {
_pe -> s(z)  ;  ll -> cons(b, nil)  ;  x -> a
})

-------------------------------------------
Step 15, which took 0.017896 s (model generation: 0.009853,  model checking: 0.008043):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417},
Q_f={q_gen_3399},
Delta=
{
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> length([nil, z]) -> 10  ;  () -> reverse([nil, nil]) -> 10  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 10  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 13  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 11  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 13
}
Sat witness: Yes: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 0.014940 s (model generation: 0.011593,  model checking: 0.003347):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, b>() -> q_gen_3451
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, b>() -> q_gen_3453
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, b>() -> q_gen_3455
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417},
Q_f={q_gen_3399},
Delta=
{
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> length([nil, z]) -> 10  ;  () -> reverse([nil, nil]) -> 10  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 13  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 13  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 11  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 13
}
Sat witness: Yes: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(b, nil)  ;  _le -> cons(b, cons(b, nil))  ;  h1 -> b  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 17, which took 0.025786 s (model generation: 0.019602,  model checking: 0.006184):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, b>() -> q_gen_3451
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, b>() -> q_gen_3453
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, b>() -> q_gen_3455
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461},
Q_f={q_gen_3399},
Delta=
{
<nil>() -> q_gen_3460
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> length([nil, z]) -> 11  ;  () -> reverse([nil, nil]) -> 11  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 13  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 13  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 12  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 16
}
Sat witness: Yes: ((length([ll, _pe])) -> length([cons(x, ll), s(_pe)]), {
_pe -> s(s(z))  ;  ll -> cons(b, cons(b, nil))  ;  x -> b
})

-------------------------------------------
Step 18, which took 0.046412 s (model generation: 0.014784,  model checking: 0.031628):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, b>() -> q_gen_3451
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, b>() -> q_gen_3453
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, b>() -> q_gen_3455
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461},
Q_f={q_gen_3399},
Delta=
{
<nil>() -> q_gen_3460
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> length([nil, z]) -> 12  ;  () -> reverse([nil, nil]) -> 12  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 13  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 16  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 13  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 16
}
Sat witness: Yes: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.011412 s (model generation: 0.009473,  model checking: 0.001939):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, b>() -> q_gen_3451
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, b>() -> q_gen_3453
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, b>() -> q_gen_3455
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461},
Q_f={q_gen_3399},
Delta=
{
<nil>() -> q_gen_3460
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> length([nil, z]) -> 13  ;  () -> reverse([nil, nil]) -> 13  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 16  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 16  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 14  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 16
}
Sat witness: Yes: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> nil  ;  _le -> cons(b, cons(a, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 20, which took 0.014090 s (model generation: 0.010138,  model checking: 0.003952):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, b>() -> q_gen_3451
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, b>() -> q_gen_3453
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, b>() -> q_gen_3455
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461},
Q_f={q_gen_3399},
Delta=
{
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14  ;  () -> length([nil, z]) -> 14  ;  () -> reverse([nil, nil]) -> 14  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 16  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 16  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 17  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 16
}
Sat witness: Yes: ((length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]), {
_te -> z  ;  _ue -> cons(b, nil)  ;  _ve -> s(z)  ;  l1 -> nil
})

-------------------------------------------
Step 21, which took 0.081450 s (model generation: 0.015370,  model checking: 0.066080):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, b>() -> q_gen_3451
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, b>() -> q_gen_3453
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, b>() -> q_gen_3455
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3472},
Q_f={q_gen_3399},
Delta=
{
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3472) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3472
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  () -> length([nil, z]) -> 15  ;  () -> reverse([nil, nil]) -> 15  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 16  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 19  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 17  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 17
}
Sat witness: Yes: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 22, which took 0.016526 s (model generation: 0.011244,  model checking: 0.005282):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, a, b>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, b>() -> q_gen_3455
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3472},
Q_f={q_gen_3399},
Delta=
{
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3472) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3472
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> length([nil, z]) -> 16  ;  () -> reverse([nil, nil]) -> 16  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 19  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 19  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 17  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 17
}
Sat witness: Yes: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> nil  ;  _le -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 0.015787 s (model generation: 0.012436,  model checking: 0.003351):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, a, b>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, b>() -> q_gen_3455
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3472},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3472) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3472
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17  ;  () -> length([nil, z]) -> 17  ;  () -> reverse([nil, nil]) -> 17  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 19  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 19  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 20  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 18
}
Sat witness: Yes: ((length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]), {
_te -> s(z)  ;  _ue -> cons(b, cons(b, nil))  ;  _ve -> s(s(z))  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 24, which took 0.324946 s (model generation: 0.015910,  model checking: 0.309036):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3450, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457, q_gen_3469},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3469
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3450) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3450
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3450
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3450
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, a, b>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, b>() -> q_gen_3455
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3471},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3471) -> q_gen_3471
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3471
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18  ;  () -> length([nil, z]) -> 18  ;  () -> reverse([nil, nil]) -> 18  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 19  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 22  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 20  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 19
}
Sat witness: Yes: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 25, which took 0.022047 s (model generation: 0.018253,  model checking: 0.003794):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, a>() -> q_gen_3451
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, a, b>() -> q_gen_3453
<nil, b, a>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<a, nil, a>() -> q_gen_3455
<b, nil, b>() -> q_gen_3455
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<a, b, a>() -> q_gen_3457
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3473, q_gen_3475, q_gen_3486},
Q_f={q_gen_3399},
Delta=
{
<nil>() -> q_gen_3460
<b>() -> q_gen_3461
<a>() -> q_gen_3473
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3486
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, cons>(q_gen_3461, q_gen_3486) -> q_gen_3399
<nil, cons>(q_gen_3473, q_gen_3460) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3486) -> q_gen_3416
<b, cons>(q_gen_3473, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3475) -> q_gen_3475
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3475
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19  ;  () -> length([nil, z]) -> 19  ;  () -> reverse([nil, nil]) -> 19  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 22  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 22  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 20  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 20
}
Sat witness: Yes: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> nil  ;  _le -> cons(b, cons(b, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 26, which took 0.062573 s (model generation: 0.018424,  model checking: 0.044149):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3450, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457, q_gen_3469},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3469
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3450) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3450
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3450
<nil, nil, a>() -> q_gen_3451
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, a, b>() -> q_gen_3453
<nil, b, a>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<a, nil, a>() -> q_gen_3455
<b, nil, b>() -> q_gen_3455
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<a, b, a>() -> q_gen_3457
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3471},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3471) -> q_gen_3471
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3471
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20  ;  () -> length([nil, z]) -> 20  ;  () -> reverse([nil, nil]) -> 20  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 22  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 25  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 21  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 21
}
Sat witness: Yes: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 27, which took 0.025091 s (model generation: 0.020319,  model checking: 0.004772):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457, q_gen_3469, q_gen_3470},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3469
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, a>() -> q_gen_3451
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, a, b>() -> q_gen_3453
<nil, b, a>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<a, nil, a>() -> q_gen_3455
<b, nil, b>() -> q_gen_3455
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<a, b, a>() -> q_gen_3457
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3470
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3471},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3471) -> q_gen_3471
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3471
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 21  ;  () -> length([nil, z]) -> 21  ;  () -> reverse([nil, nil]) -> 21  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 25  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 25  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 22  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 22
}
Sat witness: Yes: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(b, nil)  ;  _le -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 28, which took 0.029084 s (model generation: 0.025648,  model checking: 0.003436):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3410, q_gen_3413, q_gen_3424, q_gen_3425, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3410, q_gen_3405) -> q_gen_3405
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3410
<nil, a>() -> q_gen_3410
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3413) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3410, q_gen_3405) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3410, q_gen_3405) -> q_gen_3413
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3413
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3413
<nil, nil, a>() -> q_gen_3451
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, a, b>() -> q_gen_3453
<nil, b, a>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<a, nil, a>() -> q_gen_3455
<b, nil, b>() -> q_gen_3455
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<a, b, a>() -> q_gen_3457
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3414, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3428, q_gen_3460, q_gen_3461},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3428, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3414
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3414) -> q_gen_3414
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3428, q_gen_3414) -> q_gen_3414
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3414
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3428
<nil, a>() -> q_gen_3428
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24  ;  () -> length([nil, z]) -> 22  ;  () -> reverse([nil, nil]) -> 22  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 25  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 25  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 22  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 22
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 29, which took 0.212550 s (model generation: 0.023465,  model checking: 0.189085):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3445, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457, q_gen_3469, q_gen_3470},
Q_f={q_gen_3401},
Delta=
{
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3445
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3445) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3469
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3469
<nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3469
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, a>() -> q_gen_3451
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3452
<nil, a, b>() -> q_gen_3453
<nil, b, a>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3454
<a, nil, a>() -> q_gen_3455
<b, nil, b>() -> q_gen_3455
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3456
<a, b, a>() -> q_gen_3457
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3470) -> q_gen_3470
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3470
<nil, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3470
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3471},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3471) -> q_gen_3471
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3471
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27  ;  () -> length([nil, z]) -> 23  ;  () -> reverse([nil, nil]) -> 23  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 25  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 25  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 23  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 23
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 30, which took 0.025727 s (model generation: 0.025583,  model checking: 0.000144):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, a>() -> q_gen_3451
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, a, b>() -> q_gen_3453
<nil, b, a>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<a, nil, a>() -> q_gen_3455
<b, nil, b>() -> q_gen_3455
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<a, b, a>() -> q_gen_3457
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3402, q_gen_3403, q_gen_3419, q_gen_3438, q_gen_3463},
Q_f={q_gen_3400, q_gen_3402},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3402) -> q_gen_3400
<cons, s>(q_gen_3419, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3402
<a, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
<a, z>() -> q_gen_3419
<b, s>(q_gen_3438) -> q_gen_3419
<cons, s>(q_gen_3419, q_gen_3402) -> q_gen_3463
<cons, s>(q_gen_3419, q_gen_3463) -> q_gen_3463
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3472},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3472) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3472
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27  ;  () -> length([nil, z]) -> 23  ;  () -> reverse([nil, nil]) -> 23  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 25  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 25  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 23  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 26
}
Sat witness: Yes: ((length([ll, _pe])) -> length([cons(x, ll), s(_pe)]), {
_pe -> s(z)  ;  ll -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 31, which took 0.025780 s (model generation: 0.025486,  model checking: 0.000294):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457, q_gen_3469, q_gen_3470},
Q_f={q_gen_3401},
Delta=
{
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3424
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3469
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, a>() -> q_gen_3451
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, a, b>() -> q_gen_3453
<nil, b, a>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<a, nil, a>() -> q_gen_3455
<b, nil, b>() -> q_gen_3455
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<a, b, a>() -> q_gen_3457
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3470
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3428, q_gen_3460, q_gen_3461, q_gen_3471},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3428, q_gen_3399) -> q_gen_3399
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3428, q_gen_3471) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3428
<nil, a>() -> q_gen_3428
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3471) -> q_gen_3471
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3471
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27  ;  () -> length([nil, z]) -> 23  ;  () -> reverse([nil, nil]) -> 23  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 25  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 25  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 26  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 26
}
Sat witness: Yes: ((length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]), {
_te -> s(s(z))  ;  _ue -> cons(b, cons(b, cons(b, nil)))  ;  _ve -> s(s(s(z)))  ;  l1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 32, which took 0.028104 s (model generation: 0.023111,  model checking: 0.004993):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3445, q_gen_3450, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457, q_gen_3469},
Q_f={q_gen_3401},
Delta=
{
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3445
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, a>(q_gen_3425, q_gen_3445) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3445) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3469
<nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3469
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3450) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3450
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3450
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3450
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3450
<nil, nil, a>() -> q_gen_3451
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3452
<nil, a, b>() -> q_gen_3453
<nil, b, a>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3454
<a, nil, a>() -> q_gen_3455
<b, nil, b>() -> q_gen_3455
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3456
<a, b, a>() -> q_gen_3457
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3471},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3471) -> q_gen_3471
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3471
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27  ;  () -> length([nil, z]) -> 24  ;  () -> reverse([nil, nil]) -> 24  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 25  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 28  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 26  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 26
}
Sat witness: Yes: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 33, which took 0.030981 s (model generation: 0.025647,  model checking: 0.005334):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3445, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457, q_gen_3469, q_gen_3470},
Q_f={q_gen_3401},
Delta=
{
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3445
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, a>(q_gen_3425, q_gen_3445) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3445) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3469
<nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3469
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, a>() -> q_gen_3451
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3452
<nil, a, b>() -> q_gen_3453
<nil, b, a>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3454
<a, nil, a>() -> q_gen_3455
<b, nil, b>() -> q_gen_3455
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3456
<a, b, a>() -> q_gen_3457
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3470) -> q_gen_3470
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3470
<nil, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3470
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3471},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3471) -> q_gen_3471
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3471
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27  ;  () -> length([nil, z]) -> 25  ;  () -> reverse([nil, nil]) -> 25  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 28  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 28  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 26  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 26
}
Sat witness: Yes: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(a, nil)  ;  _le -> cons(a, cons(a, nil))  ;  h1 -> b  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 34, which took 0.162135 s (model generation: 0.024173,  model checking: 0.137962):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3445, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457, q_gen_3469, q_gen_3470},
Q_f={q_gen_3401},
Delta=
{
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3445
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, a>(q_gen_3425, q_gen_3445) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3445) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3469
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3469
<nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3469
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, a>() -> q_gen_3451
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3452
<nil, a, b>() -> q_gen_3453
<nil, b, a>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3454
<a, nil, a>() -> q_gen_3455
<b, nil, b>() -> q_gen_3455
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3456
<a, b, a>() -> q_gen_3457
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3470) -> q_gen_3470
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3470
<nil, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3470
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3471},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, a>(q_gen_3461, q_gen_3460) -> q_gen_3415
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3471) -> q_gen_3471
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3471
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 30  ;  () -> length([nil, z]) -> 26  ;  () -> reverse([nil, nil]) -> 26  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 28  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 28  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 27  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 27
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(a, cons(a, cons(b, nil))))
})

-------------------------------------------
Step 35, which took 0.195566 s (model generation: 0.029174,  model checking: 0.166392):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3445, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457, q_gen_3469, q_gen_3470},
Q_f={q_gen_3401},
Delta=
{
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3445
<cons>(q_gen_3425, q_gen_3445) -> q_gen_3445
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, a>(q_gen_3425, q_gen_3445) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3445) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3469
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3469
<nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3469
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, a>() -> q_gen_3451
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3452
<nil, a, b>() -> q_gen_3453
<nil, b, a>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3454
<a, nil, a>() -> q_gen_3455
<b, nil, b>() -> q_gen_3455
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3456
<a, b, a>() -> q_gen_3457
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3470) -> q_gen_3470
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3470
<nil, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3470
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3471},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, a>(q_gen_3461, q_gen_3460) -> q_gen_3415
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3471) -> q_gen_3471
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3471
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 30  ;  () -> length([nil, z]) -> 27  ;  () -> reverse([nil, nil]) -> 27  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 28  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 31  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 28  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 28
}
Sat witness: Yes: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 36, which took 0.035512 s (model generation: 0.029050,  model checking: 0.006462):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3445, q_gen_3450, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457, q_gen_3469},
Q_f={q_gen_3401},
Delta=
{
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3445
<cons>(q_gen_3425, q_gen_3445) -> q_gen_3445
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, a>(q_gen_3425, q_gen_3445) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3445) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3469
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3469
<nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3469
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3450) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3450
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3450
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3450
<nil, nil, a>() -> q_gen_3451
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3452
<nil, a, a>() -> q_gen_3453
<nil, a, b>() -> q_gen_3453
<nil, b, a>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3454
<a, nil, a>() -> q_gen_3455
<b, nil, b>() -> q_gen_3455
<a, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3456
<a, a, a>() -> q_gen_3457
<a, b, a>() -> q_gen_3457
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3471},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, a>(q_gen_3461, q_gen_3460) -> q_gen_3415
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<b, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3471) -> q_gen_3471
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3471
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 30  ;  () -> length([nil, z]) -> 28  ;  () -> reverse([nil, nil]) -> 28  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 31  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 31  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 29  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 29
}
Sat witness: Yes: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(a, nil)  ;  _le -> cons(a, cons(b, nil))  ;  h1 -> b  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 37, which took 17.244134 s (model generation: 0.032846,  model checking: 17.211288):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3445, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457, q_gen_3469, q_gen_3470},
Q_f={q_gen_3401},
Delta=
{
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3445
<cons>(q_gen_3425, q_gen_3445) -> q_gen_3445
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, a>(q_gen_3425, q_gen_3445) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3445) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3469
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3469
<nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3469
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<nil, nil, a>() -> q_gen_3451
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3452
<nil, a, a>() -> q_gen_3453
<nil, a, b>() -> q_gen_3453
<nil, b, a>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3454
<a, nil, a>() -> q_gen_3455
<b, nil, b>() -> q_gen_3455
<a, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3456
<a, a, a>() -> q_gen_3457
<a, b, a>() -> q_gen_3457
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3470) -> q_gen_3470
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3470
<nil, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3470
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3471},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, a>(q_gen_3461, q_gen_3460) -> q_gen_3415
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<a, b>() -> q_gen_3417
<b, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3471) -> q_gen_3471
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3471
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 31  ;  () -> length([nil, z]) -> 29  ;  () -> reverse([nil, nil]) -> 29  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 31  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 34  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 30  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 30
}
Sat witness: Yes: ((append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]), {
_fe -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 38, which took 0.057794 s (model generation: 0.052389,  model checking: 0.005405):

Model:
|_
{
append -> 
{{{
Q={q_gen_3401, q_gen_3405, q_gen_3406, q_gen_3407, q_gen_3408, q_gen_3424, q_gen_3425, q_gen_3445, q_gen_3450, q_gen_3451, q_gen_3452, q_gen_3453, q_gen_3454, q_gen_3455, q_gen_3456, q_gen_3457, q_gen_3469},
Q_f={q_gen_3401},
Delta=
{
<nil>() -> q_gen_3424
<a>() -> q_gen_3425
<b>() -> q_gen_3425
<cons>(q_gen_3425, q_gen_3424) -> q_gen_3445
<cons>(q_gen_3425, q_gen_3445) -> q_gen_3445
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3405
<nil, nil>() -> q_gen_3405
<cons, a>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, a>(q_gen_3425, q_gen_3445) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3406
<cons, b>(q_gen_3425, q_gen_3445) -> q_gen_3406
<nil, a>() -> q_gen_3406
<nil, b>() -> q_gen_3406
<a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<a, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<a, nil>() -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3407
<b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3407
<b, nil>() -> q_gen_3407
<a, a>() -> q_gen_3408
<a, b>() -> q_gen_3408
<b, b>() -> q_gen_3408
<cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3469
<nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3469
<nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3469
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3450) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<cons, nil, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3401
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3405) -> q_gen_3401
<nil, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3401
<nil, nil, nil>() -> q_gen_3401
<cons, cons, cons>(q_gen_3457, q_gen_3456, q_gen_3455, q_gen_3454, q_gen_3453, q_gen_3452, q_gen_3451, q_gen_3401) -> q_gen_3450
<nil, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3450
<nil, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3450
<nil, cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3451
<nil, nil, a>() -> q_gen_3451
<nil, nil, b>() -> q_gen_3451
<nil, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3452
<nil, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3452
<nil, a, a>() -> q_gen_3453
<nil, a, b>() -> q_gen_3453
<nil, b, a>() -> q_gen_3453
<nil, b, b>() -> q_gen_3453
<a, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, cons, cons>(q_gen_3408, q_gen_3407, q_gen_3406, q_gen_3469) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3424) -> q_gen_3454
<b, nil, cons>(q_gen_3425, q_gen_3445) -> q_gen_3454
<a, nil, a>() -> q_gen_3455
<b, cons, b>(q_gen_3425, q_gen_3424) -> q_gen_3455
<b, nil, b>() -> q_gen_3455
<a, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<a, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, a, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3424) -> q_gen_3456
<b, b, cons>(q_gen_3425, q_gen_3445) -> q_gen_3456
<a, a, a>() -> q_gen_3457
<a, b, a>() -> q_gen_3457
<b, a, b>() -> q_gen_3457
<b, b, b>() -> q_gen_3457
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3400, q_gen_3403, q_gen_3438},
Q_f={q_gen_3400},
Delta=
{
<s>(q_gen_3438) -> q_gen_3438
<z>() -> q_gen_3438
<cons, s>(q_gen_3403, q_gen_3400) -> q_gen_3400
<nil, z>() -> q_gen_3400
<a, s>(q_gen_3438) -> q_gen_3403
<a, z>() -> q_gen_3403
<b, s>(q_gen_3438) -> q_gen_3403
<b, z>() -> q_gen_3403
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  reverse -> 
{{{
Q={q_gen_3399, q_gen_3415, q_gen_3416, q_gen_3417, q_gen_3460, q_gen_3461, q_gen_3471},
Q_f={q_gen_3399},
Delta=
{
<cons>(q_gen_3461, q_gen_3460) -> q_gen_3460
<nil>() -> q_gen_3460
<a>() -> q_gen_3461
<b>() -> q_gen_3461
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3399) -> q_gen_3399
<nil, nil>() -> q_gen_3399
<cons, a>(q_gen_3461, q_gen_3460) -> q_gen_3415
<cons, b>(q_gen_3461, q_gen_3460) -> q_gen_3415
<nil, a>() -> q_gen_3415
<nil, b>() -> q_gen_3415
<a, nil>() -> q_gen_3416
<b, cons>(q_gen_3461, q_gen_3460) -> q_gen_3416
<b, nil>() -> q_gen_3416
<a, a>() -> q_gen_3417
<a, b>() -> q_gen_3417
<b, a>() -> q_gen_3417
<b, b>() -> q_gen_3417
<cons, cons>(q_gen_3417, q_gen_3416, q_gen_3415, q_gen_3471) -> q_gen_3471
<nil, cons>(q_gen_3461, q_gen_3460) -> q_gen_3471
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 31  ;  () -> length([nil, z]) -> 30  ;  () -> reverse([nil, nil]) -> 30  ;  (append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]) -> 34  ;  (append([t1, l2, _fe])) -> append([cons(h1, t1), l2, cons(h1, _fe)]) -> 34  ;  (length([_ue, _ve]) /\ length([l1, _te]) /\ reverse([l1, _ue])) -> eq_nat([_te, _ve]) -> 31  ;  (length([ll, _pe])) -> length([cons(x, ll), s(_pe)]) -> 31
}
Sat witness: Yes: ((append([_ke, cons(h1, nil), _le]) /\ reverse([t1, _ke])) -> reverse([cons(h1, t1), _le]), {
_ke -> cons(a, nil)  ;  _le -> cons(a, cons(b, nil))  ;  h1 -> a  ;  t1 -> cons(b, nil)
})

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