Solving ../../benchmarks/true/length_reverse_leq_leq.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, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)])} (append([_sda, _tda, _uda]) /\ append([_sda, _tda, _vda])) -> eq_eltlist([_uda, _vda]) ) (reverse, F: {() -> reverse([nil, nil]) (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda])} (reverse([_yda, _aea]) /\ reverse([_yda, _zda])) -> eq_eltlist([_zda, _aea]) ) (leq, P: {() -> leq([z, s(nn2)]) () -> leq([z, z]) (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) (leq([s(nn1), z])) -> BOT} ) (length, F: {() -> length([nil, z]) (length([ll, _bea])) -> length([cons(x, ll), s(_bea)])} (length([_cea, _dea]) /\ length([_cea, _eea])) -> eq_nat([_dea, _eea]) ) } properties: {(length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]), (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea])} over-approximation: {append, length, reverse} under-approximation: {leq} Clause system for inference is: { () -> append([nil, l2, l2]) -> 0 ; () -> length([nil, z]) -> 0 ; () -> leq([z, s(nn2)]) -> 0 ; () -> leq([z, z]) -> 0 ; () -> reverse([nil, nil]) -> 0 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 0 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 0 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 0 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 0 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 0 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0 ; (leq([s(nn1), z])) -> BOT -> 0 } Solving took 30.000246 seconds. DontKnow. Stopped because: timeout Working model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3560, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3567, q_gen_3568, q_gen_3569, q_gen_3570, q_gen_3571, q_gen_3578, q_gen_3579, q_gen_3580, q_gen_3581, q_gen_3582, q_gen_3583, q_gen_3584, q_gen_3589, q_gen_3590, q_gen_3591, q_gen_3592, q_gen_3593, q_gen_3597, q_gen_3598, q_gen_3599, q_gen_3600, q_gen_3601, q_gen_3602, q_gen_3603, q_gen_3604, q_gen_3607, q_gen_3608, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3625, q_gen_3626, q_gen_3627, q_gen_3628, q_gen_3635, q_gen_3636, q_gen_3637, q_gen_3638, q_gen_3639, q_gen_3640, q_gen_3641, q_gen_3642, q_gen_3643, q_gen_3650, q_gen_3651, q_gen_3652, q_gen_3653, q_gen_3654, q_gen_3655, q_gen_3656, q_gen_3657, q_gen_3658, q_gen_3659, q_gen_3660, q_gen_3661, q_gen_3663, q_gen_3664, q_gen_3665, q_gen_3666, q_gen_3667, q_gen_3668, q_gen_3669, q_gen_3670, q_gen_3671, q_gen_3672, q_gen_3673, q_gen_3674, q_gen_3675, q_gen_3676, q_gen_3677, q_gen_3678, q_gen_3682, q_gen_3683, q_gen_3684, q_gen_3685, q_gen_3686, q_gen_3694, q_gen_3699, q_gen_3700, q_gen_3701, q_gen_3702, q_gen_3703, q_gen_3704, q_gen_3705, q_gen_3706, q_gen_3707, q_gen_3708, q_gen_3711, q_gen_3712, q_gen_3713, q_gen_3714, q_gen_3715, q_gen_3716, q_gen_3717, q_gen_3718, q_gen_3719, q_gen_3720, q_gen_3721}, Q_f={}, Delta= { () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3592 (q_gen_3592, q_gen_3582) -> q_gen_3603 (q_gen_3583, q_gen_3603) -> q_gen_3668 (q_gen_3592, q_gen_3603) -> q_gen_3675 (q_gen_3583, q_gen_3582) -> q_gen_3718 () -> q_gen_3561 () -> q_gen_3562 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3568 () -> q_gen_3569 () -> q_gen_3570 (q_gen_3570, q_gen_3569, q_gen_3568, q_gen_3561) -> q_gen_3580 (q_gen_3583, q_gen_3582) -> q_gen_3581 (q_gen_3583, q_gen_3582) -> q_gen_3584 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3590 (q_gen_3592, q_gen_3582) -> q_gen_3591 (q_gen_3592, q_gen_3582) -> q_gen_3593 (q_gen_3592, q_gen_3582) -> q_gen_3598 (q_gen_3592, q_gen_3582) -> q_gen_3599 (q_gen_3570, q_gen_3599, q_gen_3598, q_gen_3590) -> q_gen_3601 (q_gen_3583, q_gen_3603) -> q_gen_3602 (q_gen_3583, q_gen_3603) -> q_gen_3604 (q_gen_3583, q_gen_3582) -> q_gen_3627 (q_gen_3592, q_gen_3603) -> q_gen_3642 (q_gen_3592, q_gen_3603) -> q_gen_3643 (q_gen_3570, q_gen_3666, q_gen_3665, q_gen_3601) -> q_gen_3664 (q_gen_3583, q_gen_3603) -> q_gen_3665 (q_gen_3583, q_gen_3603) -> q_gen_3666 (q_gen_3583, q_gen_3668) -> q_gen_3667 (q_gen_3583, q_gen_3668) -> q_gen_3669 (q_gen_3592, q_gen_3603) -> q_gen_3671 (q_gen_3570, q_gen_3671, q_gen_3568, q_gen_3642) -> q_gen_3673 (q_gen_3583, q_gen_3675) -> q_gen_3674 (q_gen_3592, q_gen_3582) -> q_gen_3701 (q_gen_3583, q_gen_3582) -> q_gen_3712 (q_gen_3583, q_gen_3582) -> q_gen_3713 () -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3560 (q_gen_3570, q_gen_3569, q_gen_3568, q_gen_3561) -> q_gen_3567 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3571 (q_gen_3570, q_gen_3569, q_gen_3568, q_gen_3561) -> q_gen_3578 (q_gen_3564, q_gen_3584, q_gen_3581, q_gen_3580) -> q_gen_3579 (q_gen_3564, q_gen_3593, q_gen_3591, q_gen_3590) -> q_gen_3589 (q_gen_3570, q_gen_3599, q_gen_3598, q_gen_3590) -> q_gen_3597 (q_gen_3564, q_gen_3604, q_gen_3602, q_gen_3601) -> q_gen_3600 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3608) -> q_gen_3607 (q_gen_3592, q_gen_3582) -> q_gen_3608 () -> q_gen_3609 (q_gen_3592, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 (q_gen_3592, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 (q_gen_3592, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 (q_gen_3583, q_gen_3582) -> q_gen_3625 (q_gen_3564, q_gen_3584, q_gen_3562, q_gen_3627) -> q_gen_3626 (q_gen_3564, q_gen_3584, q_gen_3562, q_gen_3627) -> q_gen_3628 (q_gen_3640, q_gen_3639, q_gen_3613, q_gen_3638, q_gen_3637, q_gen_3636, q_gen_3609, q_gen_3625) -> q_gen_3635 (q_gen_3583, q_gen_3582) -> q_gen_3636 () -> q_gen_3637 (q_gen_3583, q_gen_3582) -> q_gen_3638 (q_gen_3583, q_gen_3582) -> q_gen_3639 () -> q_gen_3640 (q_gen_3564, q_gen_3643, q_gen_3562, q_gen_3642) -> q_gen_3641 (q_gen_3656, q_gen_3655, q_gen_3654, q_gen_3653, q_gen_3652, q_gen_3610, q_gen_3651, q_gen_3608) -> q_gen_3650 () -> q_gen_3651 () -> q_gen_3652 (q_gen_3592, q_gen_3582) -> q_gen_3653 () -> q_gen_3654 (q_gen_3592, q_gen_3582) -> q_gen_3655 () -> q_gen_3656 (q_gen_3615, q_gen_3661, q_gen_3613, q_gen_3660, q_gen_3611, q_gen_3659, q_gen_3609, q_gen_3658) -> q_gen_3657 (q_gen_3592, q_gen_3603) -> q_gen_3658 (q_gen_3592, q_gen_3603) -> q_gen_3659 (q_gen_3592, q_gen_3603) -> q_gen_3660 (q_gen_3592, q_gen_3603) -> q_gen_3661 (q_gen_3564, q_gen_3669, q_gen_3667, q_gen_3664) -> q_gen_3663 (q_gen_3570, q_gen_3671, q_gen_3568, q_gen_3642) -> q_gen_3670 (q_gen_3564, q_gen_3674, q_gen_3581, q_gen_3673) -> q_gen_3672 (q_gen_3615, q_gen_3678, q_gen_3613, q_gen_3638, q_gen_3611, q_gen_3677, q_gen_3609, q_gen_3625) -> q_gen_3676 (q_gen_3583, q_gen_3582) -> q_gen_3677 (q_gen_3583, q_gen_3582) -> q_gen_3678 (q_gen_3686, q_gen_3685, q_gen_3654, q_gen_3684, q_gen_3683, q_gen_3636, q_gen_3651, q_gen_3625) -> q_gen_3682 () -> q_gen_3683 (q_gen_3583, q_gen_3582) -> q_gen_3684 (q_gen_3583, q_gen_3582) -> q_gen_3685 () -> q_gen_3686 (q_gen_3564, q_gen_3643, q_gen_3562, q_gen_3642) -> q_gen_3694 (q_gen_3656, q_gen_3705, q_gen_3704, q_gen_3703, q_gen_3652, q_gen_3659, q_gen_3702, q_gen_3700) -> q_gen_3699 (q_gen_3564, q_gen_3593, q_gen_3562, q_gen_3701) -> q_gen_3700 (q_gen_3592, q_gen_3582) -> q_gen_3702 (q_gen_3564, q_gen_3593, q_gen_3562, q_gen_3701) -> q_gen_3703 (q_gen_3592, q_gen_3582) -> q_gen_3704 (q_gen_3592, q_gen_3603) -> q_gen_3705 (q_gen_3686, q_gen_3708, q_gen_3654, q_gen_3653, q_gen_3683, q_gen_3707, q_gen_3651, q_gen_3608) -> q_gen_3706 (q_gen_3592, q_gen_3582) -> q_gen_3707 (q_gen_3592, q_gen_3582) -> q_gen_3708 (q_gen_3570, q_gen_3713, q_gen_3712, q_gen_3580) -> q_gen_3711 (q_gen_3640, q_gen_3721, q_gen_3720, q_gen_3719, q_gen_3637, q_gen_3717, q_gen_3716, q_gen_3715) -> q_gen_3714 (q_gen_3570, q_gen_3713, q_gen_3568, q_gen_3627) -> q_gen_3715 (q_gen_3583, q_gen_3582) -> q_gen_3716 (q_gen_3583, q_gen_3718) -> q_gen_3717 (q_gen_3570, q_gen_3713, q_gen_3568, q_gen_3627) -> q_gen_3719 (q_gen_3583, q_gen_3582) -> q_gen_3720 (q_gen_3583, q_gen_3718) -> q_gen_3721 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3558, q_gen_3559, q_gen_3576, q_gen_3577, q_gen_3594, q_gen_3595, q_gen_3596, q_gen_3605, q_gen_3606, q_gen_3621, q_gen_3622, q_gen_3623, q_gen_3624, q_gen_3689}, Q_f={}, Delta= { () -> q_gen_3596 (q_gen_3596) -> q_gen_3624 () -> q_gen_3555 (q_gen_3559, q_gen_3555) -> q_gen_3558 () -> q_gen_3559 (q_gen_3577, q_gen_3555) -> q_gen_3576 () -> q_gen_3577 (q_gen_3595, q_gen_3576) -> q_gen_3594 (q_gen_3596) -> q_gen_3595 (q_gen_3606, q_gen_3558) -> q_gen_3605 (q_gen_3596) -> q_gen_3606 (q_gen_3595, q_gen_3558) -> q_gen_3621 (q_gen_3623, q_gen_3621) -> q_gen_3622 (q_gen_3624) -> q_gen_3623 (q_gen_3623, q_gen_3605) -> q_gen_3689 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3553, q_gen_3554, q_gen_3557, q_gen_3565, q_gen_3566, q_gen_3634, q_gen_3649, q_gen_3693}, Q_f={}, Delta= { () -> q_gen_3554 (q_gen_3554) -> q_gen_3566 () -> q_gen_3552 (q_gen_3554) -> q_gen_3553 (q_gen_3552) -> q_gen_3557 (q_gen_3566) -> q_gen_3565 (q_gen_3554) -> q_gen_3634 (q_gen_3634) -> q_gen_3649 (q_gen_3649) -> q_gen_3693 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3572, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3585, q_gen_3586, q_gen_3587, q_gen_3588, q_gen_3616, q_gen_3617, q_gen_3618, q_gen_3619, q_gen_3620, q_gen_3629, q_gen_3630, q_gen_3631, q_gen_3632, q_gen_3633, q_gen_3644, q_gen_3645, q_gen_3646, q_gen_3647, q_gen_3648, q_gen_3662, q_gen_3679, q_gen_3680, q_gen_3681, q_gen_3687, q_gen_3688, q_gen_3690, q_gen_3691, q_gen_3692, q_gen_3695, q_gen_3696, q_gen_3697, q_gen_3698, q_gen_3709, q_gen_3710}, Q_f={}, Delta= { () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3631 (q_gen_3619, q_gen_3618) -> q_gen_3646 () -> q_gen_3551 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3572 () -> q_gen_3573 () -> q_gen_3574 () -> q_gen_3575 (q_gen_3588, q_gen_3587, q_gen_3586, q_gen_3551) -> q_gen_3585 () -> q_gen_3586 () -> q_gen_3587 () -> q_gen_3588 (q_gen_3575, q_gen_3620, q_gen_3617, q_gen_3572) -> q_gen_3616 (q_gen_3619, q_gen_3618) -> q_gen_3617 (q_gen_3619, q_gen_3618) -> q_gen_3620 (q_gen_3575, q_gen_3632, q_gen_3573, q_gen_3630) -> q_gen_3629 (q_gen_3631, q_gen_3618) -> q_gen_3630 (q_gen_3631, q_gen_3618) -> q_gen_3632 (q_gen_3619, q_gen_3618) -> q_gen_3633 (q_gen_3575, q_gen_3647, q_gen_3573, q_gen_3645) -> q_gen_3644 (q_gen_3619, q_gen_3646) -> q_gen_3645 (q_gen_3619, q_gen_3646) -> q_gen_3647 (q_gen_3575, q_gen_3620, q_gen_3573, q_gen_3633) -> q_gen_3648 (q_gen_3575, q_gen_3647, q_gen_3617, q_gen_3648) -> q_gen_3662 (q_gen_3575, q_gen_3632, q_gen_3617, q_gen_3680) -> q_gen_3679 (q_gen_3681, q_gen_3574, q_gen_3586, q_gen_3551) -> q_gen_3680 () -> q_gen_3681 (q_gen_3681, q_gen_3620, q_gen_3688, q_gen_3572) -> q_gen_3687 (q_gen_3619, q_gen_3618) -> q_gen_3688 (q_gen_3575, q_gen_3692, q_gen_3617, q_gen_3691) -> q_gen_3690 (q_gen_3681, q_gen_3620, q_gen_3586, q_gen_3633) -> q_gen_3691 (q_gen_3631, q_gen_3646) -> q_gen_3692 (q_gen_3681, q_gen_3620, q_gen_3698, q_gen_3696) -> q_gen_3695 (q_gen_3697, q_gen_3587, q_gen_3573, q_gen_3551) -> q_gen_3696 () -> q_gen_3697 (q_gen_3631, q_gen_3618) -> q_gen_3698 (q_gen_3588, q_gen_3710, q_gen_3688, q_gen_3572) -> q_gen_3709 (q_gen_3619, q_gen_3618) -> q_gen_3710 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.004360 s (model generation: 0.003907, model checking: 0.000453): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; length -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={}, Q_f={}, Delta= { } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 0 ; () -> leq([z, z]) -> 0 ; () -> reverse([nil, nil]) -> 3 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 1 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 1 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 1 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 1 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 ; (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Yes: (() -> reverse([nil, nil]), { }) ------------------------------------------- Step 1, which took 0.003586 s (model generation: 0.003559, model checking: 0.000027): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; length -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3551 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 0 ; () -> leq([z, z]) -> 3 ; () -> reverse([nil, nil]) -> 3 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 1 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 1 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 1 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 1 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 ; (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Yes: (() -> leq([z, z]), { }) ------------------------------------------- Step 2, which took 0.003469 s (model generation: 0.003426, model checking: 0.000043): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; length -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552}, Q_f={q_gen_3552}, Delta= { () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3551 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 3 ; () -> leq([z, z]) -> 3 ; () -> reverse([nil, nil]) -> 3 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 1 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 1 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 1 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 1 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 ; (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Yes: (() -> leq([z, s(nn2)]), { nn2 -> z }) ------------------------------------------- Step 3, which took 0.003416 s (model generation: 0.003374, model checking: 0.000042): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; length -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { () -> q_gen_3554 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3551 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 3 ; () -> leq([z, z]) -> 3 ; () -> reverse([nil, nil]) -> 3 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 1 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 1 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 1 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 1 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 ; (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Yes: (() -> length([nil, z]), { }) ------------------------------------------- Step 4, which took 0.004078 s (model generation: 0.003573, model checking: 0.000505): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555}, Q_f={q_gen_3555}, Delta= { () -> q_gen_3555 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { () -> q_gen_3554 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3551 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 3 ; () -> leq([z, z]) -> 3 ; () -> reverse([nil, nil]) -> 3 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 1 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 1 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 1 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 1 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 ; (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Yes: (() -> append([nil, l2, l2]), { l2 -> nil }) ------------------------------------------- Step 5, which took 0.004675 s (model generation: 0.004563, model checking: 0.000112): Model: |_ { append -> {{{ Q={q_gen_3556}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555}, Q_f={q_gen_3555}, Delta= { () -> q_gen_3555 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { () -> q_gen_3554 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3551 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 3 ; () -> leq([z, z]) -> 3 ; () -> reverse([nil, nil]) -> 3 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 1 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 1 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 1 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 1 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2 ; (leq([s(nn1), z])) -> BOT -> 2 } Sat witness: Yes: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), { nn1 -> z ; nn2 -> z }) ------------------------------------------- Step 6, which took 0.007117 s (model generation: 0.006919, model checking: 0.000198): Model: |_ { append -> {{{ Q={q_gen_3556}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555}, Q_f={q_gen_3555}, Delta= { () -> q_gen_3555 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3551 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 3 ; () -> leq([z, z]) -> 3 ; () -> reverse([nil, nil]) -> 3 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 1 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 1 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 1 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 4 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2 ; (leq([s(nn1), z])) -> BOT -> 2 } Sat witness: Yes: ((length([ll, _bea])) -> length([cons(x, ll), s(_bea)]), { _bea -> z ; ll -> nil ; x -> b }) ------------------------------------------- Step 7, which took 0.011329 s (model generation: 0.010121, model checking: 0.001208): Model: |_ { append -> {{{ Q={q_gen_3556}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559}, Q_f={q_gen_3555}, Delta= { (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3551 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 3 ; () -> leq([z, z]) -> 3 ; () -> reverse([nil, nil]) -> 3 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 1 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 4 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 2 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 2 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 4 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2 ; (leq([s(nn1), z])) -> BOT -> 2 } Sat witness: Yes: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), { _rda -> nil ; h1 -> b ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 8, which took 0.010026 s (model generation: 0.009686, model checking: 0.000340): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3561 () -> q_gen_3562 () -> q_gen_3563 () -> q_gen_3564 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559}, Q_f={q_gen_3555}, Delta= { (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3551 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 6 ; () -> leq([z, z]) -> 4 ; () -> reverse([nil, nil]) -> 4 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 2 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 4 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 3 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 3 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 4 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3 ; (leq([s(nn1), z])) -> BOT -> 3 } Sat witness: Yes: (() -> leq([z, s(nn2)]), { nn2 -> s(z) }) ------------------------------------------- Step 9, which took 0.010554 s (model generation: 0.009298, model checking: 0.001256): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3561 () -> q_gen_3562 () -> q_gen_3563 () -> q_gen_3564 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559}, Q_f={q_gen_3555}, Delta= { (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3551 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 6 ; () -> leq([z, z]) -> 4 ; () -> reverse([nil, nil]) -> 4 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 3 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 4 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 4 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 4 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 4 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4 ; (leq([s(nn1), z])) -> BOT -> 4 } Sat witness: Yes: (() -> append([nil, l2, l2]), { l2 -> cons(a, nil) }) ------------------------------------------- Step 10, which took 0.012240 s (model generation: 0.011763, model checking: 0.000477): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3561 () -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559}, Q_f={q_gen_3555}, Delta= { (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3551 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 6 ; () -> leq([z, z]) -> 4 ; () -> reverse([nil, nil]) -> 4 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 6 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 4 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 4 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 4 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 4 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4 ; (leq([s(nn1), z])) -> BOT -> 4 } Sat witness: Yes: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), { _wda -> nil ; _xda -> cons(b, nil) ; h1 -> b ; t1 -> nil }) ------------------------------------------- Step 11, which took 0.015149 s (model generation: 0.013344, model checking: 0.001805): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3561 () -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559}, Q_f={q_gen_3555}, Delta= { (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575}, Q_f={q_gen_3551}, Delta= { (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 () -> q_gen_3573 () -> q_gen_3574 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 6 ; () -> leq([z, z]) -> 4 ; () -> reverse([nil, nil]) -> 4 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 6 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 4 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 4 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 4 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 7 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5 ; (leq([s(nn1), z])) -> BOT -> 5 } Sat witness: Yes: ((length([ll, _bea])) -> length([cons(x, ll), s(_bea)]), { _bea -> z ; ll -> nil ; x -> a }) ------------------------------------------- Step 12, which took 0.019702 s (model generation: 0.011566, model checking: 0.008136): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3561 () -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559}, Q_f={q_gen_3555}, Delta= { (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 () -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575}, Q_f={q_gen_3551}, Delta= { (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 () -> q_gen_3573 () -> q_gen_3574 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 6 ; () -> leq([z, z]) -> 4 ; () -> reverse([nil, nil]) -> 4 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 6 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 7 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 5 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 5 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 7 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5 ; (leq([s(nn1), z])) -> BOT -> 5 } Sat witness: Yes: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), { _rda -> cons(a, nil) ; h1 -> b ; l2 -> nil ; t1 -> cons(a, nil) }) ------------------------------------------- Step 13, which took 0.018374 s (model generation: 0.015436, model checking: 0.002938): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3582 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559}, Q_f={q_gen_3555}, Delta= { (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 () -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575}, Q_f={q_gen_3551}, Delta= { (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 () -> q_gen_3573 () -> q_gen_3574 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 6 ; () -> leq([z, z]) -> 5 ; () -> reverse([nil, nil]) -> 5 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 9 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 7 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 6 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 6 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 7 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 6 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6 ; (leq([s(nn1), z])) -> BOT -> 6 } Sat witness: Yes: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), { _wda -> nil ; _xda -> cons(a, nil) ; h1 -> a ; t1 -> nil }) ------------------------------------------- Step 14, which took 0.038643 s (model generation: 0.016044, model checking: 0.022599): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3582 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559}, Q_f={q_gen_3555}, Delta= { (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 () -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575}, Q_f={q_gen_3551}, Delta= { (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 7 ; () -> leq([z, z]) -> 6 ; () -> reverse([nil, nil]) -> 6 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 9 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 7 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 7 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 7 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 7 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7 ; (leq([s(nn1), z])) -> BOT -> 7 } Sat witness: Yes: (() -> append([nil, l2, l2]), { l2 -> cons(b, cons(b, nil)) }) ------------------------------------------- Step 15, which took 0.006181 s (model generation: 0.005655, model checking: 0.000526): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559}, Q_f={q_gen_3555}, Delta= { (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 () -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575}, Q_f={q_gen_3551}, Delta= { (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 7 ; () -> leq([z, z]) -> 7 ; () -> reverse([nil, nil]) -> 7 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 9 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 7 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 7 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 7 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 10 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8 ; (leq([s(nn1), z])) -> BOT -> 8 } Sat witness: Yes: ((length([ll, _bea])) -> length([cons(x, ll), s(_bea)]), { _bea -> s(z) ; ll -> cons(a, nil) ; x -> b }) ------------------------------------------- Step 16, which took 0.016935 s (model generation: 0.007698, model checking: 0.009237): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575}, Q_f={q_gen_3551}, Delta= { (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 7 ; () -> leq([z, z]) -> 7 ; () -> reverse([nil, nil]) -> 7 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 9 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 10 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 8 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 8 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 10 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8 ; (leq([s(nn1), z])) -> BOT -> 8 } Sat witness: Yes: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), { _rda -> cons(b, nil) ; h1 -> a ; l2 -> nil ; t1 -> cons(b, nil) }) ------------------------------------------- Step 17, which took 0.018333 s (model generation: 0.007136, model checking: 0.011197): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575}, Q_f={q_gen_3551}, Delta= { (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 8 ; () -> leq([z, z]) -> 8 ; () -> reverse([nil, nil]) -> 8 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 10 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 10 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 9 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 9 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 10 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9 ; (leq([s(nn1), z])) -> BOT -> 9 } Sat witness: Yes: (() -> append([nil, l2, l2]), { l2 -> cons(b, cons(a, cons(b, nil))) }) ------------------------------------------- Step 18, which took 0.007561 s (model generation: 0.006844, model checking: 0.000717): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575}, Q_f={q_gen_3551}, Delta= { (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 9 ; () -> leq([z, z]) -> 9 ; () -> reverse([nil, nil]) -> 9 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 10 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 10 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 10 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 10 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 13 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10 ; (leq([s(nn1), z])) -> BOT -> 10 } Sat witness: Yes: ((length([ll, _bea])) -> length([cons(x, ll), s(_bea)]), { _bea -> s(z) ; ll -> cons(b, nil) ; x -> a }) ------------------------------------------- Step 19, which took 0.017909 s (model generation: 0.009752, model checking: 0.008157): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575}, Q_f={q_gen_3551}, Delta= { (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 10 ; () -> leq([z, z]) -> 10 ; () -> reverse([nil, nil]) -> 10 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 10 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 13 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 11 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 11 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 13 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11 ; (leq([s(nn1), z])) -> BOT -> 11 } Sat witness: Yes: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), { _rda -> cons(b, nil) ; h1 -> b ; l2 -> cons(b, nil) ; t1 -> nil }) ------------------------------------------- Step 20, which took 0.011372 s (model generation: 0.009881, model checking: 0.001491): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575}, Q_f={q_gen_3551}, Delta= { (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 10 ; () -> leq([z, z]) -> 10 ; () -> reverse([nil, nil]) -> 10 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 13 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 13 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 11 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 11 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 13 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11 ; (leq([s(nn1), z])) -> BOT -> 11 } Sat witness: Yes: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), { _wda -> cons(b, nil) ; _xda -> cons(b, cons(b, nil)) ; h1 -> b ; t1 -> cons(b, nil) }) ------------------------------------------- Step 21, which took 0.025711 s (model generation: 0.018582, model checking: 0.007129): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3618 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 11 ; () -> leq([z, z]) -> 11 ; () -> reverse([nil, nil]) -> 11 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 13 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 13 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 12 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 12 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 16 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 12 ; (leq([s(nn1), z])) -> BOT -> 12 } Sat witness: Yes: ((length([ll, _bea])) -> length([cons(x, ll), s(_bea)]), { _bea -> s(s(z)) ; ll -> cons(b, cons(b, nil)) ; x -> b }) ------------------------------------------- Step 22, which took 0.108289 s (model generation: 0.024555, model checking: 0.083734): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3618 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 12 ; () -> leq([z, z]) -> 12 ; () -> reverse([nil, nil]) -> 12 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 13 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 16 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 13 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 13 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 16 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13 ; (leq([s(nn1), z])) -> BOT -> 13 } Sat witness: Yes: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), { _rda -> cons(a, nil) ; h1 -> b ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 23, which took 0.012974 s (model generation: 0.010722, model checking: 0.002252): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3618 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 13 ; () -> leq([z, z]) -> 13 ; () -> reverse([nil, nil]) -> 13 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 16 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 16 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 14 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 14 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 16 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14 ; (leq([s(nn1), z])) -> BOT -> 14 } Sat witness: Yes: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), { _wda -> nil ; _xda -> cons(b, cons(a, nil)) ; h1 -> b ; t1 -> nil }) ------------------------------------------- Step 24, which took 0.014047 s (model generation: 0.010741, model checking: 0.003306): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 14 ; () -> leq([z, z]) -> 14 ; () -> reverse([nil, nil]) -> 14 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 16 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 16 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 14 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 17 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 16 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 15 ; (leq([s(nn1), z])) -> BOT -> 15 } Sat witness: Yes: ((length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]), { _iea -> cons(b, nil) ; _jea -> s(z) ; _kea -> z ; l1 -> nil }) ------------------------------------------- Step 25, which took 0.019793 s (model generation: 0.015008, model checking: 0.004785): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 15 ; () -> leq([z, z]) -> 15 ; () -> reverse([nil, nil]) -> 15 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 16 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 16 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 15 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 17 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 16 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 15 ; (leq([s(nn1), z])) -> BOT -> 18 } Sat witness: Yes: ((leq([s(nn1), z])) -> BOT, { nn1 -> z }) ------------------------------------------- Step 26, which took 0.093111 s (model generation: 0.022473, model checking: 0.070638): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3630}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3630) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3619, q_gen_3618) -> q_gen_3630 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 16 ; () -> leq([z, z]) -> 16 ; () -> reverse([nil, nil]) -> 16 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 16 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 19 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 16 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 17 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 17 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 16 ; (leq([s(nn1), z])) -> BOT -> 18 } Sat witness: Yes: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), { _rda -> cons(a, nil) ; h1 -> b ; l2 -> cons(a, nil) ; t1 -> nil }) ------------------------------------------- Step 27, which took 0.017707 s (model generation: 0.014247, model checking: 0.003460): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3630}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3630) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3619, q_gen_3618) -> q_gen_3630 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 16 ; () -> leq([z, z]) -> 16 ; () -> reverse([nil, nil]) -> 16 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 19 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 19 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 17 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 17 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 17 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17 ; (leq([s(nn1), z])) -> BOT -> 18 } Sat witness: Yes: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), { _wda -> nil ; _xda -> cons(b, cons(b, cons(b, nil))) ; h1 -> b ; t1 -> nil }) ------------------------------------------- Step 28, which took 0.017060 s (model generation: 0.014150, model checking: 0.002910): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3630}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3630) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3619, q_gen_3618) -> q_gen_3630 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 17 ; () -> leq([z, z]) -> 17 ; () -> reverse([nil, nil]) -> 17 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 19 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 19 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 17 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 20 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 18 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 18 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 18 ; (leq([s(nn1), z])) -> BOT -> 18 } Sat witness: Yes: ((length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]), { _iea -> cons(b, cons(b, nil)) ; _jea -> s(s(z)) ; _kea -> s(z) ; l1 -> cons(b, nil) }) ------------------------------------------- Step 29, which took 0.018291 s (model generation: 0.015661, model checking: 0.002630): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3634) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3630}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3630) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3619, q_gen_3618) -> q_gen_3630 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 18 ; () -> leq([z, z]) -> 18 ; () -> reverse([nil, nil]) -> 18 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 19 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 19 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 18 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 20 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 18 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 18 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21 ; (leq([s(nn1), z])) -> BOT -> 19 } Sat witness: Yes: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), { nn1 -> s(z) ; nn2 -> z }) ------------------------------------------- Step 30, which took 0.325598 s (model generation: 0.016668, model checking: 0.308930): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3608, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3627}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3583, q_gen_3582) -> q_gen_3627 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3608) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3608 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3608 (q_gen_3583, q_gen_3582) -> q_gen_3608 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3629}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3629) -> q_gen_3629 (q_gen_3619, q_gen_3618) -> q_gen_3629 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 19 ; () -> leq([z, z]) -> 19 ; () -> reverse([nil, nil]) -> 19 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 19 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 22 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 19 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 20 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 19 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 19 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21 ; (leq([s(nn1), z])) -> BOT -> 20 } Sat witness: Yes: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), { _rda -> cons(b, nil) ; h1 -> a ; l2 -> cons(b, nil) ; t1 -> nil }) ------------------------------------------- Step 31, which took 0.020744 s (model generation: 0.020184, model checking: 0.000560): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3627, q_gen_3628}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3583, q_gen_3582) -> q_gen_3627 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3628 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3629}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3629) -> q_gen_3629 (q_gen_3619, q_gen_3618) -> q_gen_3629 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 19 ; () -> leq([z, z]) -> 19 ; () -> reverse([nil, nil]) -> 19 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 22 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 22 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 20 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 20 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 20 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21 ; (leq([s(nn1), z])) -> BOT -> 20 } Sat witness: Yes: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), { _wda -> cons(b, nil) ; _xda -> cons(b, cons(b, cons(b, nil))) ; h1 -> b ; t1 -> cons(b, nil) }) ------------------------------------------- Step 32, which took 0.023591 s (model generation: 0.020846, model checking: 0.002745): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3620, q_gen_3631, q_gen_3633, q_gen_3646}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3631 (q_gen_3619, q_gen_3618) -> q_gen_3646 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3633) -> q_gen_3551 (q_gen_3575, q_gen_3620, q_gen_3573, q_gen_3551) -> q_gen_3551 (q_gen_3619, q_gen_3646) -> q_gen_3551 (q_gen_3631, q_gen_3618) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3646) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3619, q_gen_3618) -> q_gen_3620 (q_gen_3631, q_gen_3618) -> q_gen_3620 (q_gen_3575, q_gen_3620, q_gen_3573, q_gen_3633) -> q_gen_3633 (q_gen_3619, q_gen_3618) -> q_gen_3633 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 20 ; () -> leq([z, z]) -> 20 ; () -> reverse([nil, nil]) -> 20 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 22 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 22 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 20 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 23 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 21 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 21 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21 ; (leq([s(nn1), z])) -> BOT -> 21 } Sat witness: Yes: ((length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]), { _iea -> cons(a, nil) ; _jea -> s(z) ; _kea -> z ; l1 -> nil }) ------------------------------------------- Step 33, which took 0.028937 s (model generation: 0.025449, model checking: 0.003488): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3558, q_gen_3559, q_gen_3577, q_gen_3596, q_gen_3621}, Q_f={q_gen_3555, q_gen_3558}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3558) -> q_gen_3555 (q_gen_3577, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3559, q_gen_3555) -> q_gen_3558 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 () -> q_gen_3577 (q_gen_3596) -> q_gen_3577 (q_gen_3577, q_gen_3558) -> q_gen_3621 (q_gen_3577, q_gen_3621) -> q_gen_3621 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3630}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3630) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3619, q_gen_3618) -> q_gen_3630 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 21 ; () -> leq([z, z]) -> 21 ; () -> reverse([nil, nil]) -> 21 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 22 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 22 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 21 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 23 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 24 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 22 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22 ; (leq([s(nn1), z])) -> BOT -> 22 } Sat witness: Yes: ((length([ll, _bea])) -> length([cons(x, ll), s(_bea)]), { _bea -> s(z) ; ll -> cons(b, nil) ; x -> b }) ------------------------------------------- Step 34, which took 0.221836 s (model generation: 0.022916, model checking: 0.198920): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3603, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3627, q_gen_3628}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3583, q_gen_3582) -> q_gen_3603 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3583, q_gen_3582) -> q_gen_3627 (q_gen_3583, q_gen_3603) -> q_gen_3627 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3603) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3603) -> q_gen_3612 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3603) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3628) -> q_gen_3628 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3628 (q_gen_3583, q_gen_3603) -> q_gen_3628 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3629}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3629) -> q_gen_3629 (q_gen_3619, q_gen_3618) -> q_gen_3629 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 22 ; () -> leq([z, z]) -> 22 ; () -> reverse([nil, nil]) -> 22 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 22 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 22 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 22 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 23 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 24 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 22 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22 ; (leq([s(nn1), z])) -> BOT -> 22 } Sat witness: Yes: (() -> append([nil, l2, l2]), { l2 -> cons(b, cons(a, cons(a, cons(b, nil)))) }) ------------------------------------------- Step 35, which took 0.105003 s (model generation: 0.025210, model checking: 0.079793): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3603, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3627, q_gen_3628}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3583, q_gen_3582) -> q_gen_3603 (q_gen_3583, q_gen_3603) -> q_gen_3603 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3583, q_gen_3582) -> q_gen_3627 (q_gen_3583, q_gen_3603) -> q_gen_3627 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3603) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3603) -> q_gen_3612 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3603) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3628) -> q_gen_3628 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3628 (q_gen_3583, q_gen_3603) -> q_gen_3628 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3629}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3629) -> q_gen_3629 (q_gen_3619, q_gen_3618) -> q_gen_3629 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 22 ; () -> leq([z, z]) -> 22 ; () -> reverse([nil, nil]) -> 22 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 22 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 25 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 23 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 23 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 24 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 23 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23 ; (leq([s(nn1), z])) -> BOT -> 23 } Sat witness: Yes: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), { _rda -> cons(a, cons(b, cons(b, nil))) ; h1 -> b ; l2 -> nil ; t1 -> cons(a, nil) }) ------------------------------------------- Step 36, which took 0.045303 s (model generation: 0.028875, model checking: 0.016428): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3627, q_gen_3628}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3583, q_gen_3582) -> q_gen_3627 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3628 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3586, q_gen_3618, q_gen_3619, q_gen_3629}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 (q_gen_3575, q_gen_3574, q_gen_3586, q_gen_3551) -> q_gen_3551 (q_gen_3575, q_gen_3574, q_gen_3586, q_gen_3629) -> q_gen_3551 () -> q_gen_3551 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3619, q_gen_3618) -> q_gen_3586 () -> q_gen_3586 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3629) -> q_gen_3629 (q_gen_3619, q_gen_3618) -> q_gen_3629 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 22 ; () -> leq([z, z]) -> 22 ; () -> reverse([nil, nil]) -> 22 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 25 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 25 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 23 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 23 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 24 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 23 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23 ; (leq([s(nn1), z])) -> BOT -> 23 } Sat witness: Yes: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), { _wda -> cons(b, nil) ; _xda -> cons(b, cons(a, nil)) ; h1 -> b ; t1 -> cons(b, nil) }) ------------------------------------------- Step 37, which took 0.039152 s (model generation: 0.035167, model checking: 0.003985): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3568, q_gen_3571, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3564, q_gen_3563, q_gen_3568, q_gen_3561) -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3583, q_gen_3582) -> q_gen_3568 () -> q_gen_3568 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3568, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3568, q_gen_3561) -> q_gen_3571 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3571 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3572, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3588, q_gen_3618, q_gen_3619}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3588, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3572 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3572) -> q_gen_3572 (q_gen_3619, q_gen_3618) -> q_gen_3572 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3588 () -> q_gen_3588 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 23 ; () -> leq([z, z]) -> 23 ; () -> reverse([nil, nil]) -> 23 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 25 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 25 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 24 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 24 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 25 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 24 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 24 ; (leq([s(nn1), z])) -> BOT -> 24 } Sat witness: Yes: (() -> append([nil, l2, l2]), { l2 -> cons(b, nil) }) ------------------------------------------- Step 38, which took 0.031236 s (model generation: 0.030368, model checking: 0.000868): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3582) -> q_gen_3556 () -> q_gen_3556 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3630, q_gen_3631, q_gen_3633, q_gen_3646}, Q_f={q_gen_3551}, Delta= { () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3631 (q_gen_3619, q_gen_3618) -> q_gen_3646 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3630) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 (q_gen_3619, q_gen_3646) -> q_gen_3574 (q_gen_3631, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3633) -> q_gen_3630 (q_gen_3619, q_gen_3646) -> q_gen_3630 (q_gen_3631, q_gen_3618) -> q_gen_3630 (q_gen_3619, q_gen_3618) -> q_gen_3633 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 24 ; () -> leq([z, z]) -> 24 ; () -> reverse([nil, nil]) -> 24 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 25 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 25 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 24 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 27 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 25 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 25 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 25 ; (leq([s(nn1), z])) -> BOT -> 25 } Sat witness: Yes: ((length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]), { _iea -> cons(b, cons(a, nil)) ; _jea -> s(s(z)) ; _kea -> s(z) ; l1 -> cons(b, nil) }) ------------------------------------------- Step 39, which took 0.191896 s (model generation: 0.026906, model checking: 0.164990): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3608, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3627}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3583, q_gen_3582) -> q_gen_3627 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3608) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3608 (q_gen_3583, q_gen_3582) -> q_gen_3608 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3629, q_gen_3630}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3629) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3630) -> q_gen_3629 (q_gen_3619, q_gen_3618) -> q_gen_3630 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 25 ; () -> leq([z, z]) -> 25 ; () -> reverse([nil, nil]) -> 25 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 25 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 28 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 25 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 27 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 26 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 26 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 26 ; (leq([s(nn1), z])) -> BOT -> 26 } Sat witness: Yes: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), { _rda -> cons(a, nil) ; h1 -> a ; l2 -> cons(a, nil) ; t1 -> nil }) ------------------------------------------- Step 40, which took 0.036409 s (model generation: 0.033139, model checking: 0.003270): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3603, q_gen_3608, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3627}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3583, q_gen_3582) -> q_gen_3603 (q_gen_3583, q_gen_3603) -> q_gen_3603 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3583, q_gen_3582) -> q_gen_3627 (q_gen_3583, q_gen_3603) -> q_gen_3627 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3608) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3603) -> q_gen_3556 () -> q_gen_3556 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3608 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3608 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3608 (q_gen_3583, q_gen_3582) -> q_gen_3608 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3603) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3603) -> q_gen_3612 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3603) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3629}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3629) -> q_gen_3629 (q_gen_3619, q_gen_3618) -> q_gen_3629 } Datatype: 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 ; () -> leq([z, s(nn2)]) -> 25 ; () -> leq([z, z]) -> 25 ; () -> reverse([nil, nil]) -> 25 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 28 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 28 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 26 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 27 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 26 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 26 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 26 ; (leq([s(nn1), z])) -> BOT -> 26 } Sat witness: Yes: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), { _wda -> cons(a, nil) ; _xda -> cons(a, cons(b, nil)) ; h1 -> b ; t1 -> cons(b, nil) }) ------------------------------------------- Step 41, which took 0.035417 s (model generation: 0.034220, model checking: 0.001197): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3608, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3627}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3582) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3583, q_gen_3582) -> q_gen_3627 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3608) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 () -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3608 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3608 (q_gen_3583, q_gen_3582) -> q_gen_3608 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3617, q_gen_3618, q_gen_3619, q_gen_3629}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 (q_gen_3575, q_gen_3574, q_gen_3617, q_gen_3551) -> q_gen_3551 (q_gen_3575, q_gen_3574, q_gen_3617, q_gen_3629) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3619, q_gen_3618) -> q_gen_3617 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3629) -> q_gen_3629 (q_gen_3619, q_gen_3618) -> q_gen_3629 } Datatype: 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]) -> 26 ; () -> leq([z, s(nn2)]) -> 26 ; () -> leq([z, z]) -> 26 ; () -> reverse([nil, nil]) -> 26 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 28 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 28 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 27 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 30 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 27 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 27 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 27 ; (leq([s(nn1), z])) -> BOT -> 27 } Sat witness: Yes: ((length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]), { _iea -> cons(b, cons(a, cons(b, nil))) ; _jea -> s(s(s(z))) ; _kea -> s(s(z)) ; l1 -> cons(b, cons(b, nil)) }) ------------------------------------------- Step 42, which took 0.048070 s (model generation: 0.039728, model checking: 0.008342): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3603, q_gen_3608, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3627}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3583, q_gen_3582) -> q_gen_3603 (q_gen_3583, q_gen_3603) -> q_gen_3603 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3583, q_gen_3582) -> q_gen_3627 (q_gen_3583, q_gen_3603) -> q_gen_3627 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3608) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3603) -> q_gen_3556 () -> q_gen_3556 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3608 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3608 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3608 (q_gen_3583, q_gen_3582) -> q_gen_3608 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3603) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3603) -> q_gen_3612 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3603) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3629}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3629) -> q_gen_3629 (q_gen_3619, q_gen_3618) -> q_gen_3629 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 28 ; () -> length([nil, z]) -> 27 ; () -> leq([z, s(nn2)]) -> 27 ; () -> leq([z, z]) -> 27 ; () -> reverse([nil, nil]) -> 27 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 28 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 31 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 28 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 30 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 28 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 28 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 28 ; (leq([s(nn1), z])) -> BOT -> 28 } Sat witness: Yes: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), { _rda -> cons(b, cons(b, nil)) ; h1 -> b ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 43, which took 0.043291 s (model generation: 0.036137, model checking: 0.007154): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3603, q_gen_3608, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3627}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3583, q_gen_3582) -> q_gen_3603 (q_gen_3583, q_gen_3603) -> q_gen_3603 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3583, q_gen_3582) -> q_gen_3627 (q_gen_3583, q_gen_3603) -> q_gen_3627 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3608) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3603) -> q_gen_3556 () -> q_gen_3556 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3608 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3608 (q_gen_3583, q_gen_3582) -> q_gen_3608 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3603) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3603) -> q_gen_3612 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3603) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3629}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3629) -> q_gen_3629 (q_gen_3619, q_gen_3618) -> q_gen_3629 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 28 ; () -> length([nil, z]) -> 28 ; () -> leq([z, s(nn2)]) -> 28 ; () -> leq([z, z]) -> 28 ; () -> reverse([nil, nil]) -> 28 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 31 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 31 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 29 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 30 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 29 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 29 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 29 ; (leq([s(nn1), z])) -> BOT -> 29 } Sat witness: Yes: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), { _wda -> cons(a, nil) ; _xda -> cons(a, cons(b, nil)) ; h1 -> b ; t1 -> cons(a, nil) }) ------------------------------------------- Step 44, which took 13.536654 s (model generation: 0.039496, model checking: 13.497158): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3603, q_gen_3608, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3627}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3583, q_gen_3582) -> q_gen_3603 (q_gen_3583, q_gen_3603) -> q_gen_3603 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3583, q_gen_3582) -> q_gen_3627 (q_gen_3583, q_gen_3603) -> q_gen_3627 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3608) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3603) -> q_gen_3556 () -> q_gen_3556 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3608 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3608 (q_gen_3583, q_gen_3582) -> q_gen_3608 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3603) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3603) -> q_gen_3612 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3603) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3629}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3629) -> q_gen_3629 (q_gen_3619, q_gen_3618) -> q_gen_3629 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 29 ; () -> length([nil, z]) -> 29 ; () -> leq([z, s(nn2)]) -> 29 ; () -> leq([z, z]) -> 29 ; () -> reverse([nil, nil]) -> 29 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 31 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 34 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 30 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 31 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 30 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 30 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 30 ; (leq([s(nn1), z])) -> BOT -> 30 } Sat witness: Yes: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), { _rda -> cons(b, cons(b, nil)) ; h1 -> a ; l2 -> cons(b, cons(b, nil)) ; t1 -> nil }) ------------------------------------------- Step 45, which took 0.057841 s (model generation: 0.047199, model checking: 0.010642): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3603, q_gen_3608, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3627}, Q_f={q_gen_3556}, Delta= { () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3583, q_gen_3582) -> q_gen_3603 (q_gen_3583, q_gen_3603) -> q_gen_3603 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3583, q_gen_3582) -> q_gen_3627 (q_gen_3583, q_gen_3603) -> q_gen_3627 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3608) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3603) -> q_gen_3556 () -> q_gen_3556 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3608 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3608 (q_gen_3583, q_gen_3582) -> q_gen_3608 (q_gen_3583, q_gen_3582) -> q_gen_3609 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3603) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3603) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3613 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3603) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3603) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3629}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3629) -> q_gen_3629 (q_gen_3619, q_gen_3618) -> q_gen_3629 } Datatype: 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]) -> 30 ; () -> leq([z, s(nn2)]) -> 30 ; () -> leq([z, z]) -> 30 ; () -> reverse([nil, nil]) -> 30 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 34 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 34 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 31 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 32 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 31 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 31 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 31 ; (leq([s(nn1), z])) -> BOT -> 31 } Sat witness: Yes: ((append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]), { _wda -> cons(a, nil) ; _xda -> cons(a, cons(b, nil)) ; h1 -> a ; t1 -> cons(b, nil) }) ------------------------------------------- Step 46, which took 3.459638 s (model generation: 0.067399, model checking: 3.392239): Model: |_ { append -> {{{ Q={q_gen_3556, q_gen_3561, q_gen_3562, q_gen_3563, q_gen_3564, q_gen_3582, q_gen_3583, q_gen_3603, q_gen_3608, q_gen_3609, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3627}, Q_f={q_gen_3556}, Delta= { (q_gen_3583, q_gen_3603) -> q_gen_3582 () -> q_gen_3582 () -> q_gen_3583 () -> q_gen_3583 (q_gen_3583, q_gen_3582) -> q_gen_3603 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3561 () -> q_gen_3561 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3562 (q_gen_3583, q_gen_3603) -> q_gen_3562 () -> q_gen_3562 () -> q_gen_3562 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 (q_gen_3583, q_gen_3582) -> q_gen_3563 (q_gen_3583, q_gen_3603) -> q_gen_3563 () -> q_gen_3563 () -> q_gen_3564 () -> q_gen_3564 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3627 (q_gen_3583, q_gen_3582) -> q_gen_3627 (q_gen_3583, q_gen_3603) -> q_gen_3627 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3608) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3556 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3561) -> q_gen_3556 (q_gen_3583, q_gen_3603) -> q_gen_3556 () -> q_gen_3556 (q_gen_3615, q_gen_3614, q_gen_3613, q_gen_3612, q_gen_3611, q_gen_3610, q_gen_3609, q_gen_3556) -> q_gen_3608 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3608 (q_gen_3583, q_gen_3582) -> q_gen_3608 (q_gen_3583, q_gen_3582) -> q_gen_3609 () -> q_gen_3609 () -> q_gen_3609 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3582) -> q_gen_3610 (q_gen_3583, q_gen_3603) -> q_gen_3610 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 () -> q_gen_3611 (q_gen_3564, q_gen_3563, q_gen_3562, q_gen_3627) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3612 (q_gen_3583, q_gen_3603) -> q_gen_3612 (q_gen_3583, q_gen_3582) -> q_gen_3613 () -> q_gen_3613 () -> q_gen_3613 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3603) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3582) -> q_gen_3614 (q_gen_3583, q_gen_3603) -> q_gen_3614 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 () -> q_gen_3615 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3555, q_gen_3559, q_gen_3596}, Q_f={q_gen_3555}, Delta= { (q_gen_3596) -> q_gen_3596 () -> q_gen_3596 (q_gen_3559, q_gen_3555) -> q_gen_3555 () -> q_gen_3555 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 (q_gen_3596) -> q_gen_3559 () -> q_gen_3559 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3552, q_gen_3554, q_gen_3634}, Q_f={q_gen_3552}, Delta= { (q_gen_3554) -> q_gen_3554 () -> q_gen_3554 (q_gen_3552) -> q_gen_3552 (q_gen_3554) -> q_gen_3552 () -> q_gen_3552 (q_gen_3634) -> q_gen_3634 (q_gen_3554) -> q_gen_3634 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3551, q_gen_3573, q_gen_3574, q_gen_3575, q_gen_3618, q_gen_3619, q_gen_3629}, Q_f={q_gen_3551}, Delta= { (q_gen_3619, q_gen_3618) -> q_gen_3618 () -> q_gen_3618 () -> q_gen_3619 () -> q_gen_3619 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3551) -> q_gen_3551 () -> q_gen_3551 (q_gen_3619, q_gen_3618) -> q_gen_3573 (q_gen_3619, q_gen_3618) -> q_gen_3573 () -> q_gen_3573 () -> q_gen_3573 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 (q_gen_3619, q_gen_3618) -> q_gen_3574 () -> q_gen_3574 () -> q_gen_3575 () -> q_gen_3575 () -> q_gen_3575 () -> q_gen_3575 (q_gen_3575, q_gen_3574, q_gen_3573, q_gen_3629) -> q_gen_3629 (q_gen_3619, q_gen_3618) -> q_gen_3629 } Datatype: 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]) -> 31 ; () -> leq([z, s(nn2)]) -> 31 ; () -> leq([z, z]) -> 31 ; () -> reverse([nil, nil]) -> 31 ; (append([_wda, cons(h1, nil), _xda]) /\ reverse([t1, _wda])) -> reverse([cons(h1, t1), _xda]) -> 34 ; (append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]) -> 37 ; (length([_gea, _hea]) /\ length([l1, _fea]) /\ reverse([l1, _gea])) -> leq([_fea, _hea]) -> 32 ; (length([_iea, _jea]) /\ length([l1, _kea]) /\ reverse([l1, _iea])) -> leq([_jea, _kea]) -> 33 ; (length([ll, _bea])) -> length([cons(x, ll), s(_bea)]) -> 32 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 32 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 32 ; (leq([s(nn1), z])) -> BOT -> 32 } Sat witness: Yes: ((append([t1, l2, _rda])) -> append([cons(h1, t1), l2, cons(h1, _rda)]), { _rda -> cons(a, cons(a, nil)) ; h1 -> b ; l2 -> cons(a, cons(a, nil)) ; t1 -> nil }) Total time: 30.000246 Reason for stopping: DontKnow. Stopped because: timeout