Inference procedure has parameters: Ice fuel: 200 Timeout: 60s Convolution: right Learning problem is: env: { elt -> {a, b} ; eltlist -> {cons, nil} } definition: { (leq, P: {() -> leq([a, y]) () -> leq([b, b]) (leq([b, a])) -> BOT} ) (insert, F: {() -> insert([x, nil, cons(x, nil)]) (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))])} (insert([_lt, _mt, _nt]) /\ insert([_lt, _mt, _ot])) -> eq_eltlist([_nt, _ot]) ) (sort, F: {() -> sort([nil, nil]) (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt])} (sort([_rt, _st]) /\ sort([_rt, _tt])) -> eq_eltlist([_st, _tt]) ) (append, F: {() -> append([nil, l2, l2]) (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)])} (append([_vt, _wt, _xt]) /\ append([_vt, _wt, _yt])) -> eq_eltlist([_xt, _yt]) ) (reverse, F: {() -> reverse([nil, nil]) (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au])} (reverse([_bu, _cu]) /\ reverse([_bu, _du])) -> eq_eltlist([_cu, _du]) ) } properties: {(reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu])} over-approximation: {append, insert, reverse, sort} under-approximation: {leq} Clause system for inference is: { () -> append([nil, l2, l2]) -> 0 () -> insert([x, nil, cons(x, nil)]) -> 0 () -> leq([a, y]) -> 0 () -> leq([b, b]) -> 0 () -> reverse([nil, nil]) -> 0 () -> sort([nil, nil]) -> 0 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 0 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 0 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 0 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 0 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 0 (leq([b, a])) -> BOT -> 0 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 0 } Solving took 60.000388 seconds. DontKnow. Stopped because: timeout Working model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3748, q_gen_3749, q_gen_3750, q_gen_3754, q_gen_3755, q_gen_3756, q_gen_3766, q_gen_3767, q_gen_3768, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3779, q_gen_3780, q_gen_3781, q_gen_3786, q_gen_3787, q_gen_3788, q_gen_3793, q_gen_3797, q_gen_3798, q_gen_3808, q_gen_3809, q_gen_3810, q_gen_3811, q_gen_3812, q_gen_3813, q_gen_3819, q_gen_3820, q_gen_3821, q_gen_3827, q_gen_3828, q_gen_3829, q_gen_3830, q_gen_3831, q_gen_3835, q_gen_3836, q_gen_3837, q_gen_3838, q_gen_3845, q_gen_3846, q_gen_3847, q_gen_3848, q_gen_3849, q_gen_3850, q_gen_3853, q_gen_3854, q_gen_3855, q_gen_3856, q_gen_3857, q_gen_3858}, Q_f={}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3810 (q_gen_3770, q_gen_3769) -> q_gen_3849 () -> q_gen_3749 () -> q_gen_3750 (q_gen_3756, q_gen_3749) -> q_gen_3755 () -> q_gen_3756 (q_gen_3770, q_gen_3769) -> q_gen_3780 (q_gen_3810, q_gen_3769) -> q_gen_3813 (q_gen_3750, q_gen_3780) -> q_gen_3830 (q_gen_3750, q_gen_3749) -> q_gen_3854 () -> q_gen_3857 () -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3748 (q_gen_3756, q_gen_3755) -> q_gen_3754 (q_gen_3750, q_gen_3749) -> q_gen_3766 (q_gen_3771, q_gen_3768) -> q_gen_3767 (q_gen_3770, q_gen_3769) -> q_gen_3768 () -> q_gen_3771 (q_gen_3750, q_gen_3780) -> q_gen_3779 (q_gen_3756, q_gen_3749) -> q_gen_3781 (q_gen_3787, q_gen_3768) -> q_gen_3786 () -> q_gen_3787 (q_gen_3750, q_gen_3780) -> q_gen_3788 (q_gen_3750, q_gen_3755) -> q_gen_3793 (q_gen_3756, q_gen_3749) -> q_gen_3797 (q_gen_3771, q_gen_3739) -> q_gen_3798 (q_gen_3811, q_gen_3809) -> q_gen_3808 (q_gen_3810, q_gen_3769) -> q_gen_3809 () -> q_gen_3811 (q_gen_3750, q_gen_3813) -> q_gen_3812 (q_gen_3820, q_gen_3809) -> q_gen_3819 () -> q_gen_3820 (q_gen_3771, q_gen_3797) -> q_gen_3821 (q_gen_3811, q_gen_3779) -> q_gen_3827 (q_gen_3820, q_gen_3829) -> q_gen_3828 (q_gen_3750, q_gen_3830) -> q_gen_3829 (q_gen_3820, q_gen_3768) -> q_gen_3831 (q_gen_3771, q_gen_3809) -> q_gen_3835 (q_gen_3771, q_gen_3837) -> q_gen_3836 (q_gen_3750, q_gen_3813) -> q_gen_3837 (q_gen_3756, q_gen_3780) -> q_gen_3838 (q_gen_3820, q_gen_3788) -> q_gen_3845 (q_gen_3820, q_gen_3847) -> q_gen_3846 (q_gen_3787, q_gen_3848) -> q_gen_3847 (q_gen_3770, q_gen_3849) -> q_gen_3848 (q_gen_3771, q_gen_3848) -> q_gen_3850 (q_gen_3756, q_gen_3854) -> q_gen_3853 (q_gen_3820, q_gen_3856) -> q_gen_3855 (q_gen_3857, q_gen_3780) -> q_gen_3856 (q_gen_3857, q_gen_3749) -> q_gen_3858 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3740, q_gen_3741, q_gen_3742, q_gen_3746, q_gen_3747, q_gen_3752, q_gen_3753, q_gen_3757, q_gen_3758, q_gen_3759, q_gen_3762, q_gen_3763, q_gen_3764, q_gen_3765, q_gen_3774, q_gen_3775, q_gen_3776, q_gen_3784, q_gen_3794, q_gen_3801, q_gen_3802, q_gen_3803, q_gen_3806, q_gen_3807, q_gen_3818, q_gen_3826, q_gen_3841, q_gen_3842}, Q_f={}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3747 () -> q_gen_3758 (q_gen_3753, q_gen_3737) -> q_gen_3763 (q_gen_3747, q_gen_3763) -> q_gen_3765 (q_gen_3776, q_gen_3763) -> q_gen_3775 () -> q_gen_3776 (q_gen_3758, q_gen_3741) -> q_gen_3803 (q_gen_3742, q_gen_3741) -> q_gen_3807 (q_gen_3758, q_gen_3763) -> q_gen_3842 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3740 (q_gen_3747, q_gen_3741) -> q_gen_3746 (q_gen_3753, q_gen_3737) -> q_gen_3752 (q_gen_3758, q_gen_3741) -> q_gen_3757 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3747, q_gen_3763) -> q_gen_3762 (q_gen_3747, q_gen_3765) -> q_gen_3764 (q_gen_3742, q_gen_3775) -> q_gen_3774 (q_gen_3742, q_gen_3741) -> q_gen_3784 (q_gen_3753, q_gen_3737) -> q_gen_3794 (q_gen_3747, q_gen_3763) -> q_gen_3801 (q_gen_3742, q_gen_3803) -> q_gen_3802 (q_gen_3747, q_gen_3807) -> q_gen_3806 (q_gen_3758, q_gen_3741) -> q_gen_3818 (q_gen_3747, q_gen_3741) -> q_gen_3826 (q_gen_3747, q_gen_3842) -> q_gen_3841 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3735, q_gen_3745, q_gen_3751}, Q_f={}, Delta= { () -> q_gen_3734 () -> q_gen_3735 () -> q_gen_3745 () -> q_gen_3751 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3772, q_gen_3773, q_gen_3782, q_gen_3783, q_gen_3789, q_gen_3790, q_gen_3791, q_gen_3792, q_gen_3799, q_gen_3800, q_gen_3814, q_gen_3815, q_gen_3816, q_gen_3822, q_gen_3823, q_gen_3824, q_gen_3825, q_gen_3832, q_gen_3833, q_gen_3834, q_gen_3839, q_gen_3851, q_gen_3852}, Q_f={}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3816 () -> q_gen_3733 (q_gen_3773, q_gen_3733) -> q_gen_3772 () -> q_gen_3773 (q_gen_3783, q_gen_3733) -> q_gen_3782 () -> q_gen_3783 (q_gen_3773, q_gen_3790) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3773, q_gen_3800) -> q_gen_3799 (q_gen_3792, q_gen_3791) -> q_gen_3800 (q_gen_3773, q_gen_3815) -> q_gen_3814 (q_gen_3816, q_gen_3791) -> q_gen_3815 (q_gen_3773, q_gen_3823) -> q_gen_3822 (q_gen_3824, q_gen_3733) -> q_gen_3823 () -> q_gen_3824 (q_gen_3824, q_gen_3790) -> q_gen_3825 (q_gen_3783, q_gen_3833) -> q_gen_3832 (q_gen_3834, q_gen_3733) -> q_gen_3833 () -> q_gen_3834 (q_gen_3783, q_gen_3790) -> q_gen_3839 (q_gen_3773, q_gen_3852) -> q_gen_3851 (q_gen_3834, q_gen_3790) -> q_gen_3852 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761, q_gen_3777, q_gen_3778, q_gen_3785, q_gen_3795, q_gen_3796, q_gen_3804, q_gen_3805, q_gen_3817, q_gen_3840, q_gen_3843, q_gen_3844}, Q_f={}, Delta= { () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 (q_gen_3778, q_gen_3732) -> q_gen_3777 () -> q_gen_3778 (q_gen_3761, q_gen_3743) -> q_gen_3785 (q_gen_3796, q_gen_3732) -> q_gen_3795 () -> q_gen_3796 (q_gen_3744, q_gen_3805) -> q_gen_3804 (q_gen_3778, q_gen_3743) -> q_gen_3805 (q_gen_3796, q_gen_3743) -> q_gen_3817 (q_gen_3744, q_gen_3743) -> q_gen_3840 (q_gen_3778, q_gen_3844) -> q_gen_3843 (q_gen_3778, q_gen_3795) -> q_gen_3844 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.006878 s (model generation: 0.005148, model checking: 0.001730): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; insert -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; leq -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; sort -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 () -> insert([x, nil, cons(x, nil)]) -> 0 () -> leq([a, y]) -> 0 () -> leq([b, b]) -> 0 () -> reverse([nil, nil]) -> 0 () -> sort([nil, nil]) -> 3 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 1 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1 (leq([b, a])) -> BOT -> 1 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 1 } Sat witness: Found: (() -> sort([nil, nil]), { }) ------------------------------------------- Step 1, which took 0.008336 s (model generation: 0.008151, model checking: 0.000185): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; insert -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; leq -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732}, Q_f={q_gen_3732}, Delta= { () -> q_gen_3732 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 () -> insert([x, nil, cons(x, nil)]) -> 0 () -> leq([a, y]) -> 0 () -> leq([b, b]) -> 0 () -> reverse([nil, nil]) -> 3 () -> sort([nil, nil]) -> 3 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 1 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1 (leq([b, a])) -> BOT -> 1 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 1 } Sat witness: Found: (() -> reverse([nil, nil]), { }) ------------------------------------------- Step 2, which took 0.009965 s (model generation: 0.009900, model checking: 0.000065): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; insert -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; leq -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732}, Q_f={q_gen_3732}, Delta= { () -> q_gen_3732 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 () -> insert([x, nil, cons(x, nil)]) -> 0 () -> leq([a, y]) -> 0 () -> leq([b, b]) -> 3 () -> reverse([nil, nil]) -> 3 () -> sort([nil, nil]) -> 3 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 1 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1 (leq([b, a])) -> BOT -> 1 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 1 } Sat witness: Found: (() -> leq([b, b]), { }) ------------------------------------------- Step 3, which took 0.010298 s (model generation: 0.010226, model checking: 0.000072): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; insert -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732}, Q_f={q_gen_3732}, Delta= { () -> q_gen_3732 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 () -> insert([x, nil, cons(x, nil)]) -> 0 () -> leq([a, y]) -> 3 () -> leq([b, b]) -> 3 () -> reverse([nil, nil]) -> 3 () -> sort([nil, nil]) -> 3 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 1 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1 (leq([b, a])) -> BOT -> 1 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 1 } Sat witness: Found: (() -> leq([a, y]), { y -> b }) ------------------------------------------- Step 4, which took 0.011279 s (model generation: 0.011008, model checking: 0.000271): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; insert -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732}, Q_f={q_gen_3732}, Delta= { () -> q_gen_3732 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 () -> insert([x, nil, cons(x, nil)]) -> 3 () -> leq([a, y]) -> 3 () -> leq([b, b]) -> 3 () -> reverse([nil, nil]) -> 3 () -> sort([nil, nil]) -> 3 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 1 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1 (leq([b, a])) -> BOT -> 1 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 1 } Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), { x -> b }) ------------------------------------------- Step 5, which took 0.015578 s (model generation: 0.011496, model checking: 0.004082): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732}, Q_f={q_gen_3732}, Delta= { () -> q_gen_3732 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> insert([x, nil, cons(x, nil)]) -> 3 () -> leq([a, y]) -> 3 () -> leq([b, b]) -> 3 () -> reverse([nil, nil]) -> 3 () -> sort([nil, nil]) -> 3 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 1 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1 (leq([b, a])) -> BOT -> 1 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 1 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> nil }) ------------------------------------------- Step 6, which took 0.007200 s (model generation: 0.006760, model checking: 0.000440): Model: |_ { append -> {{{ Q={q_gen_3739}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3739 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732}, Q_f={q_gen_3732}, Delta= { () -> q_gen_3732 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> insert([x, nil, cons(x, nil)]) -> 3 () -> leq([a, y]) -> 3 () -> leq([b, b]) -> 3 () -> reverse([nil, nil]) -> 3 () -> sort([nil, nil]) -> 3 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 1 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4 (leq([b, a])) -> BOT -> 2 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 2 } Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), { x -> b ; y -> b ; z -> nil }) ------------------------------------------- Step 7, which took 0.005433 s (model generation: 0.005086, model checking: 0.000347): Model: |_ { append -> {{{ Q={q_gen_3739}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3739 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732}, Q_f={q_gen_3732}, Delta= { () -> q_gen_3732 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> insert([x, nil, cons(x, nil)]) -> 3 () -> leq([a, y]) -> 3 () -> leq([b, b]) -> 3 () -> reverse([nil, nil]) -> 3 () -> sort([nil, nil]) -> 3 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 1 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4 (leq([b, a])) -> BOT -> 2 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 2 } Sat witness: Found: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), { _pt -> nil ; _qt -> cons(b, nil) ; y -> b ; z -> nil }) ------------------------------------------- Step 8, which took 0.006130 s (model generation: 0.005891, model checking: 0.000239): Model: |_ { append -> {{{ Q={q_gen_3739}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3739 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> insert([x, nil, cons(x, nil)]) -> 3 () -> leq([a, y]) -> 3 () -> leq([b, b]) -> 3 () -> reverse([nil, nil]) -> 3 () -> sort([nil, nil]) -> 3 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 1 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4 (leq([b, a])) -> BOT -> 2 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 2 } Sat witness: Found: ((insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]), { _kt -> cons(b, nil) ; x -> b ; y -> a ; z -> nil }) ------------------------------------------- Step 9, which took 0.005995 s (model generation: 0.005517, model checking: 0.000478): Model: |_ { append -> {{{ Q={q_gen_3739}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3739 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> insert([x, nil, cons(x, nil)]) -> 3 () -> leq([a, y]) -> 3 () -> leq([b, b]) -> 3 () -> reverse([nil, nil]) -> 3 () -> sort([nil, nil]) -> 3 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 1 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4 (leq([b, a])) -> BOT -> 2 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 2 } Sat witness: Found: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), { _ut -> nil ; h1 -> b ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 10, which took 0.011141 s (model generation: 0.010817, model checking: 0.000324): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3749 () -> q_gen_3750 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> insert([x, nil, cons(x, nil)]) -> 3 () -> leq([a, y]) -> 3 () -> leq([b, b]) -> 3 () -> reverse([nil, nil]) -> 3 () -> sort([nil, nil]) -> 3 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 2 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4 (leq([b, a])) -> BOT -> 5 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 3 } Sat witness: Found: ((leq([b, a])) -> BOT, { }) ------------------------------------------- Step 11, which took 0.013999 s (model generation: 0.013303, model checking: 0.000696): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3749 () -> q_gen_3750 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> insert([x, nil, cons(x, nil)]) -> 3 () -> leq([a, y]) -> 6 () -> leq([b, b]) -> 4 () -> reverse([nil, nil]) -> 4 () -> sort([nil, nil]) -> 4 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 3 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4 (leq([b, a])) -> BOT -> 5 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 4 } Sat witness: Found: (() -> leq([a, y]), { y -> a }) ------------------------------------------- Step 12, which took 0.015512 s (model generation: 0.013459, model checking: 0.002053): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3749 () -> q_gen_3750 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> insert([x, nil, cons(x, nil)]) -> 6 () -> leq([a, y]) -> 6 () -> leq([b, b]) -> 4 () -> reverse([nil, nil]) -> 4 () -> sort([nil, nil]) -> 4 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 4 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4 (leq([b, a])) -> BOT -> 5 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 4 } Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), { x -> a }) ------------------------------------------- Step 13, which took 0.014299 s (model generation: 0.013737, model checking: 0.000562): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3749 () -> q_gen_3750 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> insert([x, nil, cons(x, nil)]) -> 6 () -> leq([a, y]) -> 6 () -> leq([b, b]) -> 4 () -> reverse([nil, nil]) -> 4 () -> sort([nil, nil]) -> 4 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 4 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4 (leq([b, a])) -> BOT -> 5 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 4 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 14, which took 0.015704 s (model generation: 0.014664, model checking: 0.001040): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750}, Q_f={q_gen_3739}, Delta= { (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> insert([x, nil, cons(x, nil)]) -> 6 () -> leq([a, y]) -> 6 () -> leq([b, b]) -> 4 () -> reverse([nil, nil]) -> 4 () -> sort([nil, nil]) -> 4 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 4 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 4 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7 (leq([b, a])) -> BOT -> 5 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 5 } Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), { x -> a ; y -> b ; z -> nil }) ------------------------------------------- Step 15, which took 0.016100 s (model generation: 0.014192, model checking: 0.001908): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750}, Q_f={q_gen_3739}, Delta= { (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> insert([x, nil, cons(x, nil)]) -> 6 () -> leq([a, y]) -> 6 () -> leq([b, b]) -> 4 () -> reverse([nil, nil]) -> 4 () -> sort([nil, nil]) -> 4 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 4 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 4 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 7 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7 (leq([b, a])) -> BOT -> 5 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 5 } Sat witness: Found: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), { _pt -> nil ; _qt -> cons(b, nil) ; y -> a ; z -> nil }) ------------------------------------------- Step 16, which took 0.016526 s (model generation: 0.014703, model checking: 0.001823): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750}, Q_f={q_gen_3739}, Delta= { (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> insert([x, nil, cons(x, nil)]) -> 6 () -> leq([a, y]) -> 6 () -> leq([b, b]) -> 4 () -> reverse([nil, nil]) -> 4 () -> sort([nil, nil]) -> 4 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 4 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 4 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 7 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 7 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7 (leq([b, a])) -> BOT -> 5 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 5 } Sat witness: Found: ((insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]), { _kt -> cons(a, cons(a, nil)) ; x -> b ; y -> a ; z -> cons(a, nil) }) ------------------------------------------- Step 17, which took 0.015146 s (model generation: 0.013757, model checking: 0.001389): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750}, Q_f={q_gen_3739}, Delta= { (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> insert([x, nil, cons(x, nil)]) -> 6 () -> leq([a, y]) -> 6 () -> leq([b, b]) -> 4 () -> reverse([nil, nil]) -> 4 () -> sort([nil, nil]) -> 4 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 4 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 7 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 7 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 7 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7 (leq([b, a])) -> BOT -> 5 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 5 } Sat witness: Found: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), { _ut -> cons(b, nil) ; h1 -> b ; l2 -> cons(b, nil) ; t1 -> nil }) ------------------------------------------- Step 18, which took 0.007597 s (model generation: 0.007461, model checking: 0.000136): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> insert([x, nil, cons(x, nil)]) -> 6 () -> leq([a, y]) -> 6 () -> leq([b, b]) -> 4 () -> reverse([nil, nil]) -> 4 () -> sort([nil, nil]) -> 4 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 7 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 7 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 7 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 7 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7 (leq([b, a])) -> BOT -> 5 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 5 } Sat witness: Found: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), { _au -> cons(b, nil) ; _zt -> nil ; h1 -> b ; t1 -> nil }) ------------------------------------------- Step 19, which took 0.009307 s (model generation: 0.007609, model checking: 0.001698): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773}, Q_f={q_gen_3733}, Delta= { (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 7 () -> insert([x, nil, cons(x, nil)]) -> 7 () -> leq([a, y]) -> 7 () -> leq([b, b]) -> 5 () -> reverse([nil, nil]) -> 5 () -> sort([nil, nil]) -> 5 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 7 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 7 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 7 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 7 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10 (leq([b, a])) -> BOT -> 6 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 6 } Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), { x -> b ; y -> b ; z -> cons(a, nil) }) ------------------------------------------- Step 20, which took 0.013526 s (model generation: 0.011388, model checking: 0.002138): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773}, Q_f={q_gen_3733}, Delta= { (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 7 () -> insert([x, nil, cons(x, nil)]) -> 7 () -> leq([a, y]) -> 7 () -> leq([b, b]) -> 6 () -> reverse([nil, nil]) -> 6 () -> sort([nil, nil]) -> 6 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 7 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 7 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 7 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 10 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10 (leq([b, a])) -> BOT -> 7 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 7 } Sat witness: Found: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), { _pt -> nil ; _qt -> cons(a, nil) ; y -> a ; z -> nil }) ------------------------------------------- Step 21, which took 0.024602 s (model generation: 0.021146, model checking: 0.003456): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773}, Q_f={q_gen_3733}, Delta= { (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 7 () -> insert([x, nil, cons(x, nil)]) -> 7 () -> leq([a, y]) -> 7 () -> leq([b, b]) -> 7 () -> reverse([nil, nil]) -> 7 () -> sort([nil, nil]) -> 7 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 7 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 10 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 8 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 10 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10 (leq([b, a])) -> BOT -> 8 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 8 } Sat witness: Found: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), { _ut -> cons(b, nil) ; h1 -> b ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 22, which took 0.021141 s (model generation: 0.020708, model checking: 0.000433): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773}, Q_f={q_gen_3733}, Delta= { (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 7 () -> insert([x, nil, cons(x, nil)]) -> 7 () -> leq([a, y]) -> 7 () -> leq([b, b]) -> 7 () -> reverse([nil, nil]) -> 7 () -> sort([nil, nil]) -> 7 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 10 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 10 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 8 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 10 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10 (leq([b, a])) -> BOT -> 8 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 8 } Sat witness: Found: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), { _au -> cons(a, nil) ; _zt -> nil ; h1 -> a ; t1 -> nil }) ------------------------------------------- Step 23, which took 0.024757 s (model generation: 0.022378, model checking: 0.002379): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773}, Q_f={q_gen_3733}, Delta= { (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 8 () -> insert([x, nil, cons(x, nil)]) -> 8 () -> leq([a, y]) -> 8 () -> leq([b, b]) -> 8 () -> reverse([nil, nil]) -> 8 () -> sort([nil, nil]) -> 8 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 10 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 10 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 8 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 10 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10 (leq([b, a])) -> BOT -> 8 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 11 } Sat witness: Found: ((reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]), { _eu -> cons(b, nil) ; _fu -> cons(a, nil) ; _gu -> cons(a, nil) ; l -> cons(a, nil) }) ------------------------------------------- Step 24, which took 0.023623 s (model generation: 0.022623, model checking: 0.001000): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3755, q_gen_3766, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3750, q_gen_3749) -> q_gen_3755 (q_gen_3770, q_gen_3769) -> q_gen_3755 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3755) -> q_gen_3739 (q_gen_3750, q_gen_3755) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3766 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3772, q_gen_3773}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3733 (q_gen_3773, q_gen_3733) -> q_gen_3772 () -> q_gen_3773 () -> q_gen_3773 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 11 () -> insert([x, nil, cons(x, nil)]) -> 9 () -> leq([a, y]) -> 9 () -> leq([b, b]) -> 9 () -> reverse([nil, nil]) -> 9 () -> sort([nil, nil]) -> 9 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 10 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 10 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 9 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 10 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10 (leq([b, a])) -> BOT -> 9 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 11 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(b, nil) }) ------------------------------------------- Step 25, which took 0.012528 s (model generation: 0.010215, model checking: 0.002313): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773}, Q_f={q_gen_3733}, Delta= { (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 11 () -> insert([x, nil, cons(x, nil)]) -> 10 () -> leq([a, y]) -> 10 () -> leq([b, b]) -> 10 () -> reverse([nil, nil]) -> 10 () -> sort([nil, nil]) -> 10 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 10 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 10 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 10 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 13 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11 (leq([b, a])) -> BOT -> 10 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 11 } Sat witness: Found: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), { _pt -> cons(b, nil) ; _qt -> cons(b, cons(b, nil)) ; y -> a ; z -> cons(b, nil) }) ------------------------------------------- Step 26, which took 0.021316 s (model generation: 0.019529, model checking: 0.001787): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773}, Q_f={q_gen_3733}, Delta= { (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 (q_gen_3761, q_gen_3743) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 11 () -> insert([x, nil, cons(x, nil)]) -> 10 () -> leq([a, y]) -> 10 () -> leq([b, b]) -> 10 () -> reverse([nil, nil]) -> 10 () -> sort([nil, nil]) -> 10 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 10 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 13 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 11 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 13 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11 (leq([b, a])) -> BOT -> 11 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 11 } Sat witness: Found: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), { _ut -> cons(b, nil) ; h1 -> a ; l2 -> cons(b, nil) ; t1 -> nil }) ------------------------------------------- Step 27, which took 0.014383 s (model generation: 0.013535, model checking: 0.000848): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773}, Q_f={q_gen_3733}, Delta= { (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 (q_gen_3761, q_gen_3743) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 11 () -> insert([x, nil, cons(x, nil)]) -> 10 () -> leq([a, y]) -> 10 () -> leq([b, b]) -> 10 () -> reverse([nil, nil]) -> 10 () -> sort([nil, nil]) -> 10 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 13 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 13 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 11 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 13 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11 (leq([b, a])) -> BOT -> 11 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 11 } Sat witness: Found: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), { _au -> cons(b, cons(b, nil)) ; _zt -> nil ; h1 -> b ; t1 -> nil }) ------------------------------------------- Step 28, which took 0.011648 s (model generation: 0.010683, model checking: 0.000965): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3747, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3747, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3747 () -> q_gen_3747 () -> q_gen_3747 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3759 (q_gen_3738, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3792, q_gen_3791) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 11 () -> insert([x, nil, cons(x, nil)]) -> 11 () -> leq([a, y]) -> 11 () -> leq([b, b]) -> 11 () -> reverse([nil, nil]) -> 11 () -> sort([nil, nil]) -> 11 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 13 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 13 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 11 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 13 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11 (leq([b, a])) -> BOT -> 11 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 14 } Sat witness: Found: ((reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]), { _eu -> nil ; _fu -> cons(b, nil) ; _gu -> cons(b, nil) ; l -> nil }) ------------------------------------------- Step 29, which took 0.013387 s (model generation: 0.012295, model checking: 0.001092): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3755, q_gen_3756, q_gen_3768, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3749 () -> q_gen_3750 (q_gen_3756, q_gen_3749) -> q_gen_3755 (q_gen_3770, q_gen_3769) -> q_gen_3755 () -> q_gen_3756 (q_gen_3771, q_gen_3768) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3756, q_gen_3755) -> q_gen_3739 () -> q_gen_3739 (q_gen_3750, q_gen_3755) -> q_gen_3768 (q_gen_3750, q_gen_3755) -> q_gen_3768 (q_gen_3756, q_gen_3749) -> q_gen_3768 (q_gen_3770, q_gen_3769) -> q_gen_3768 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3782, q_gen_3783, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 (q_gen_3773, q_gen_3782) -> q_gen_3782 (q_gen_3783, q_gen_3733) -> q_gen_3782 (q_gen_3792, q_gen_3791) -> q_gen_3782 () -> q_gen_3783 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 14 () -> insert([x, nil, cons(x, nil)]) -> 12 () -> leq([a, y]) -> 12 () -> leq([b, b]) -> 12 () -> reverse([nil, nil]) -> 12 () -> sort([nil, nil]) -> 12 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 13 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 13 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 12 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 13 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 12 (leq([b, a])) -> BOT -> 12 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 14 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(b, cons(a, nil)) }) ------------------------------------------- Step 30, which took 0.020178 s (model generation: 0.018770, model checking: 0.001408): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3755, q_gen_3756, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3781}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3749 () -> q_gen_3750 (q_gen_3756, q_gen_3749) -> q_gen_3755 (q_gen_3770, q_gen_3769) -> q_gen_3755 () -> q_gen_3756 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3755) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3755) -> q_gen_3739 (q_gen_3756, q_gen_3755) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 (q_gen_3756, q_gen_3749) -> q_gen_3781 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3782, q_gen_3783, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3782) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 (q_gen_3783, q_gen_3733) -> q_gen_3782 (q_gen_3792, q_gen_3791) -> q_gen_3782 () -> q_gen_3783 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 14 () -> insert([x, nil, cons(x, nil)]) -> 13 () -> leq([a, y]) -> 13 () -> leq([b, b]) -> 13 () -> reverse([nil, nil]) -> 13 () -> sort([nil, nil]) -> 13 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 13 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 13 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 13 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 16 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13 (leq([b, a])) -> BOT -> 13 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 14 } Sat witness: Found: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), { _pt -> nil ; _qt -> cons(a, nil) ; y -> b ; z -> nil }) ------------------------------------------- Step 31, which took 0.014513 s (model generation: 0.012795, model checking: 0.001718): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3755, q_gen_3756, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3781}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3749 () -> q_gen_3750 (q_gen_3756, q_gen_3749) -> q_gen_3755 (q_gen_3770, q_gen_3769) -> q_gen_3755 () -> q_gen_3756 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3755) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3755) -> q_gen_3739 (q_gen_3756, q_gen_3755) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 (q_gen_3756, q_gen_3749) -> q_gen_3781 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3782, q_gen_3783, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3782) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 (q_gen_3783, q_gen_3733) -> q_gen_3782 (q_gen_3792, q_gen_3791) -> q_gen_3782 () -> q_gen_3783 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 14 () -> insert([x, nil, cons(x, nil)]) -> 13 () -> leq([a, y]) -> 13 () -> leq([b, b]) -> 13 () -> reverse([nil, nil]) -> 13 () -> sort([nil, nil]) -> 13 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 13 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 16 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 14 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 16 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 14 (leq([b, a])) -> BOT -> 14 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 14 } Sat witness: Found: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), { _ut -> nil ; h1 -> a ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 32, which took 0.016188 s (model generation: 0.014171, model checking: 0.002017): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3755, q_gen_3756, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3781}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 (q_gen_3756, q_gen_3749) -> q_gen_3755 () -> q_gen_3756 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3756, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3755) -> q_gen_3739 (q_gen_3756, q_gen_3755) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 (q_gen_3756, q_gen_3749) -> q_gen_3781 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3782, q_gen_3783, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3782) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 (q_gen_3783, q_gen_3733) -> q_gen_3782 (q_gen_3792, q_gen_3791) -> q_gen_3782 () -> q_gen_3783 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 14 () -> insert([x, nil, cons(x, nil)]) -> 13 () -> leq([a, y]) -> 13 () -> leq([b, b]) -> 13 () -> reverse([nil, nil]) -> 13 () -> sort([nil, nil]) -> 13 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 16 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 16 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 14 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 16 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 14 (leq([b, a])) -> BOT -> 14 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 14 } Sat witness: Found: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), { _au -> cons(b, nil) ; _zt -> cons(b, nil) ; h1 -> b ; t1 -> cons(b, nil) }) ------------------------------------------- Step 33, which took 0.014836 s (model generation: 0.013860, model checking: 0.000976): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3755, q_gen_3756, q_gen_3768, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3749 () -> q_gen_3750 (q_gen_3756, q_gen_3749) -> q_gen_3755 (q_gen_3770, q_gen_3769) -> q_gen_3755 () -> q_gen_3756 (q_gen_3771, q_gen_3768) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3756, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3755) -> q_gen_3739 (q_gen_3756, q_gen_3755) -> q_gen_3739 () -> q_gen_3739 (q_gen_3771, q_gen_3739) -> q_gen_3768 (q_gen_3750, q_gen_3755) -> q_gen_3768 (q_gen_3756, q_gen_3749) -> q_gen_3768 (q_gen_3770, q_gen_3769) -> q_gen_3768 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3782, q_gen_3783, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3782) -> q_gen_3733 (q_gen_3792, q_gen_3791) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 (q_gen_3783, q_gen_3733) -> q_gen_3782 (q_gen_3792, q_gen_3791) -> q_gen_3782 () -> q_gen_3783 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 14 () -> insert([x, nil, cons(x, nil)]) -> 14 () -> leq([a, y]) -> 14 () -> leq([b, b]) -> 14 () -> reverse([nil, nil]) -> 14 () -> sort([nil, nil]) -> 14 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 16 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 16 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 14 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 16 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 14 (leq([b, a])) -> BOT -> 14 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 17 } Sat witness: Found: ((reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]), { _eu -> cons(b, nil) ; _fu -> nil ; _gu -> nil ; l -> cons(b, nil) }) ------------------------------------------- Step 34, which took 0.015715 s (model generation: 0.014175, model checking: 0.001540): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3755, q_gen_3756, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3781}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3749 () -> q_gen_3750 (q_gen_3756, q_gen_3749) -> q_gen_3755 (q_gen_3770, q_gen_3769) -> q_gen_3755 () -> q_gen_3756 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3755) -> q_gen_3739 (q_gen_3756, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3755) -> q_gen_3739 (q_gen_3756, q_gen_3755) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 (q_gen_3756, q_gen_3749) -> q_gen_3781 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3738 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3782, q_gen_3783, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3782) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 (q_gen_3783, q_gen_3733) -> q_gen_3782 (q_gen_3792, q_gen_3791) -> q_gen_3782 (q_gen_3792, q_gen_3791) -> q_gen_3782 () -> q_gen_3783 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 17 () -> insert([x, nil, cons(x, nil)]) -> 15 () -> leq([a, y]) -> 15 () -> leq([b, b]) -> 15 () -> reverse([nil, nil]) -> 15 () -> sort([nil, nil]) -> 15 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 16 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 16 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 15 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 16 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 15 (leq([b, a])) -> BOT -> 15 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 17 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(a, nil) }) ------------------------------------------- Step 35, which took 0.013395 s (model generation: 0.013116, model checking: 0.000279): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3758, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3758, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3759 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3790, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3790) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 17 () -> insert([x, nil, cons(x, nil)]) -> 15 () -> leq([a, y]) -> 15 () -> leq([b, b]) -> 15 () -> reverse([nil, nil]) -> 15 () -> sort([nil, nil]) -> 15 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 16 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 16 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 15 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 16 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18 (leq([b, a])) -> BOT -> 16 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 17 } Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), { x -> a ; y -> a ; z -> nil }) ------------------------------------------- Step 36, which took 0.019900 s (model generation: 0.013216, model checking: 0.006684): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3790, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3790) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 (q_gen_3761, q_gen_3743) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 17 () -> insert([x, nil, cons(x, nil)]) -> 16 () -> leq([a, y]) -> 16 () -> leq([b, b]) -> 16 () -> reverse([nil, nil]) -> 16 () -> sort([nil, nil]) -> 16 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 16 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 16 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 16 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 19 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18 (leq([b, a])) -> BOT -> 17 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 17 } Sat witness: Found: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), { _pt -> cons(b, cons(b, nil)) ; _qt -> cons(b, cons(a, cons(b, nil))) ; y -> b ; z -> cons(a, cons(b, nil)) }) ------------------------------------------- Step 37, which took 0.018262 s (model generation: 0.017297, model checking: 0.000965): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3747, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3747, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3747 () -> q_gen_3747 () -> q_gen_3747 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3759 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3790, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3790) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 17 () -> insert([x, nil, cons(x, nil)]) -> 16 () -> leq([a, y]) -> 16 () -> leq([b, b]) -> 16 () -> reverse([nil, nil]) -> 16 () -> sort([nil, nil]) -> 16 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 16 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 16 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 19 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 19 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18 (leq([b, a])) -> BOT -> 17 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 17 } Sat witness: Found: ((insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]), { _kt -> cons(b, cons(b, nil)) ; x -> b ; y -> a ; z -> cons(b, nil) }) ------------------------------------------- Step 38, which took 0.022375 s (model generation: 0.020660, model checking: 0.001715): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3747, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3747, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3747 () -> q_gen_3747 () -> q_gen_3747 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3759 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3790, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3790) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 17 () -> insert([x, nil, cons(x, nil)]) -> 16 () -> leq([a, y]) -> 16 () -> leq([b, b]) -> 16 () -> reverse([nil, nil]) -> 16 () -> sort([nil, nil]) -> 16 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 16 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 19 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 19 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 19 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18 (leq([b, a])) -> BOT -> 17 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 17 } Sat witness: Found: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), { _ut -> cons(a, nil) ; h1 -> b ; l2 -> cons(a, nil) ; t1 -> nil }) ------------------------------------------- Step 39, which took 0.020567 s (model generation: 0.019671, model checking: 0.000896): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3747, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3747, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3747 () -> q_gen_3747 () -> q_gen_3747 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3759 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3790, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3790) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 17 () -> insert([x, nil, cons(x, nil)]) -> 16 () -> leq([a, y]) -> 16 () -> leq([b, b]) -> 16 () -> reverse([nil, nil]) -> 16 () -> sort([nil, nil]) -> 16 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 19 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 19 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 19 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 19 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18 (leq([b, a])) -> BOT -> 17 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 17 } Sat witness: Found: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), { _au -> cons(b, cons(a, nil)) ; _zt -> nil ; h1 -> b ; t1 -> nil }) ------------------------------------------- Step 40, which took 0.021508 s (model generation: 0.020410, model checking: 0.001098): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3747, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3747, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3747 () -> q_gen_3747 () -> q_gen_3747 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3759 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3790, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3790) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 17 () -> insert([x, nil, cons(x, nil)]) -> 17 () -> leq([a, y]) -> 17 () -> leq([b, b]) -> 17 () -> reverse([nil, nil]) -> 17 () -> sort([nil, nil]) -> 17 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 19 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 19 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 19 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 19 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18 (leq([b, a])) -> BOT -> 17 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 20 } Sat witness: Found: ((reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]), { _eu -> cons(b, nil) ; _fu -> cons(b, cons(b, nil)) ; _gu -> cons(a, cons(b, nil)) ; l -> cons(b, nil) }) ------------------------------------------- Step 41, which took 0.025093 s (model generation: 0.022264, model checking: 0.002829): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3747, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3747, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3747 () -> q_gen_3747 () -> q_gen_3747 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3759 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3790, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3790) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 18 () -> insert([x, nil, cons(x, nil)]) -> 18 () -> leq([a, y]) -> 18 () -> leq([b, b]) -> 18 () -> reverse([nil, nil]) -> 18 () -> sort([nil, nil]) -> 18 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 19 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 19 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 19 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 22 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 19 (leq([b, a])) -> BOT -> 18 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 20 } Sat witness: Found: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), { _pt -> cons(b, nil) ; _qt -> cons(a, cons(b, nil)) ; y -> b ; z -> cons(b, nil) }) ------------------------------------------- Step 42, which took 0.030022 s (model generation: 0.022246, model checking: 0.007776): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3758, q_gen_3759, q_gen_3763}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3758, q_gen_3763) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3758 () -> q_gen_3758 (q_gen_3742, q_gen_3763) -> q_gen_3763 (q_gen_3758, q_gen_3741) -> q_gen_3763 (q_gen_3753, q_gen_3737) -> q_gen_3763 (q_gen_3742, q_gen_3763) -> q_gen_3736 (q_gen_3758, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3759 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3742, q_gen_3763) -> q_gen_3759 (q_gen_3758, q_gen_3741) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3790, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3790) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 19 () -> insert([x, nil, cons(x, nil)]) -> 19 () -> leq([a, y]) -> 19 () -> leq([b, b]) -> 19 () -> reverse([nil, nil]) -> 19 () -> sort([nil, nil]) -> 19 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 19 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 22 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 20 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 22 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 20 (leq([b, a])) -> BOT -> 19 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 20 } Sat witness: Found: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), { _ut -> cons(a, nil) ; h1 -> a ; l2 -> cons(a, nil) ; t1 -> nil }) ------------------------------------------- Step 43, which took 0.027468 s (model generation: 0.025237, model checking: 0.002231): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3758, q_gen_3759, q_gen_3763}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3742, q_gen_3763) -> q_gen_3741 (q_gen_3758, q_gen_3763) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3741) -> q_gen_3763 (q_gen_3753, q_gen_3737) -> q_gen_3763 (q_gen_3742, q_gen_3763) -> q_gen_3736 (q_gen_3758, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3759 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3742, q_gen_3763) -> q_gen_3759 (q_gen_3758, q_gen_3741) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3790, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3790) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 19 () -> insert([x, nil, cons(x, nil)]) -> 19 () -> leq([a, y]) -> 19 () -> leq([b, b]) -> 19 () -> reverse([nil, nil]) -> 19 () -> sort([nil, nil]) -> 19 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 22 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 22 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 20 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 22 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 20 (leq([b, a])) -> BOT -> 20 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 20 } Sat witness: Found: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), { _au -> cons(b, cons(a, nil)) ; _zt -> cons(b, cons(a, nil)) ; h1 -> b ; t1 -> cons(b, nil) }) ------------------------------------------- Step 44, which took 0.027213 s (model generation: 0.024830, model checking: 0.002383): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3747, q_gen_3753, q_gen_3758, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3747, q_gen_3741) -> q_gen_3741 (q_gen_3758, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3747 () -> q_gen_3758 () -> q_gen_3758 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3758, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3759 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3758, q_gen_3741) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3790, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3790) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 20 () -> insert([x, nil, cons(x, nil)]) -> 20 () -> leq([a, y]) -> 20 () -> leq([b, b]) -> 20 () -> reverse([nil, nil]) -> 20 () -> sort([nil, nil]) -> 20 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 22 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 22 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 20 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 22 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 20 (leq([b, a])) -> BOT -> 20 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 23 } Sat witness: Found: ((reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]), { _eu -> cons(b, nil) ; _fu -> cons(a, cons(b, nil)) ; _gu -> cons(a, cons(b, nil)) ; l -> cons(b, nil) }) ------------------------------------------- Step 45, which took 0.030495 s (model generation: 0.027646, model checking: 0.002849): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3758, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3758, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3758 () -> q_gen_3758 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3758, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3758, q_gen_3741) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3790, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3790) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 (q_gen_3744, q_gen_3760) -> q_gen_3743 (q_gen_3761, q_gen_3743) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3744, q_gen_3743) -> q_gen_3760 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 21 () -> insert([x, nil, cons(x, nil)]) -> 21 () -> leq([a, y]) -> 21 () -> leq([b, b]) -> 21 () -> reverse([nil, nil]) -> 21 () -> sort([nil, nil]) -> 21 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 22 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 22 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 21 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 25 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 21 (leq([b, a])) -> BOT -> 21 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 23 } Sat witness: Found: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), { _pt -> cons(a, nil) ; _qt -> cons(a, cons(b, nil)) ; y -> a ; z -> cons(b, nil) }) ------------------------------------------- Step 46, which took 0.036305 s (model generation: 0.028195, model checking: 0.008110): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3768, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3780}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3770, q_gen_3769) -> q_gen_3780 (q_gen_3771, q_gen_3768) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 (q_gen_3771, q_gen_3739) -> q_gen_3768 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3770, q_gen_3769) -> q_gen_3768 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3789, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3773, q_gen_3789) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { (q_gen_3744, q_gen_3760) -> q_gen_3732 () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 (q_gen_3761, q_gen_3743) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3744, q_gen_3743) -> q_gen_3760 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 22 () -> insert([x, nil, cons(x, nil)]) -> 22 () -> leq([a, y]) -> 22 () -> leq([b, b]) -> 22 () -> reverse([nil, nil]) -> 22 () -> sort([nil, nil]) -> 22 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 22 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 25 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 22 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 25 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 22 (leq([b, a])) -> BOT -> 22 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 23 } Sat witness: Found: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), { _ut -> cons(b, cons(b, cons(b, nil))) ; h1 -> a ; l2 -> cons(a, nil) ; t1 -> cons(b, cons(b, nil)) }) ------------------------------------------- Step 47, which took 0.029914 s (model generation: 0.027635, model checking: 0.002279): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3768, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3780}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3750, q_gen_3780) -> q_gen_3780 (q_gen_3770, q_gen_3769) -> q_gen_3780 (q_gen_3771, q_gen_3768) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 (q_gen_3771, q_gen_3739) -> q_gen_3768 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3770, q_gen_3769) -> q_gen_3768 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3789, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3773, q_gen_3789) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 (q_gen_3744, q_gen_3743) -> q_gen_3743 (q_gen_3761, q_gen_3743) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 22 () -> insert([x, nil, cons(x, nil)]) -> 22 () -> leq([a, y]) -> 22 () -> leq([b, b]) -> 22 () -> reverse([nil, nil]) -> 22 () -> sort([nil, nil]) -> 22 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 25 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 25 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 23 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 25 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 23 (leq([b, a])) -> BOT -> 23 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 23 } Sat witness: Found: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), { _au -> cons(a, cons(b, nil)) ; _zt -> cons(a, nil) ; h1 -> a ; t1 -> cons(a, nil) }) ------------------------------------------- Step 48, which took 0.028092 s (model generation: 0.026731, model checking: 0.001361): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3768, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3780}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3750, q_gen_3780) -> q_gen_3780 (q_gen_3770, q_gen_3769) -> q_gen_3780 (q_gen_3771, q_gen_3768) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3780) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 (q_gen_3771, q_gen_3739) -> q_gen_3768 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3770, q_gen_3769) -> q_gen_3768 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3747, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3747, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3747 () -> q_gen_3747 () -> q_gen_3747 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3759 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3789, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3773, q_gen_3789) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 23 () -> insert([x, nil, cons(x, nil)]) -> 23 () -> leq([a, y]) -> 23 () -> leq([b, b]) -> 23 () -> reverse([nil, nil]) -> 23 () -> sort([nil, nil]) -> 23 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 25 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 25 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 23 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 25 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 23 (leq([b, a])) -> BOT -> 23 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 26 } Sat witness: Found: ((reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]), { _eu -> cons(b, nil) ; _fu -> cons(b, nil) ; _gu -> cons(a, nil) ; l -> cons(b, nil) }) ------------------------------------------- Step 49, which took 0.066782 s (model generation: 0.064150, model checking: 0.002632): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3768, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3780}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3750, q_gen_3780) -> q_gen_3780 (q_gen_3770, q_gen_3769) -> q_gen_3780 (q_gen_3771, q_gen_3768) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3780) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 (q_gen_3771, q_gen_3739) -> q_gen_3768 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3770, q_gen_3769) -> q_gen_3768 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3789, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3773, q_gen_3789) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { (q_gen_3744, q_gen_3760) -> q_gen_3732 (q_gen_3761, q_gen_3743) -> q_gen_3732 () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3744, q_gen_3743) -> q_gen_3760 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 24 () -> insert([x, nil, cons(x, nil)]) -> 24 () -> leq([a, y]) -> 24 () -> leq([b, b]) -> 24 () -> reverse([nil, nil]) -> 24 () -> sort([nil, nil]) -> 24 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 25 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 25 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 24 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 28 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 24 (leq([b, a])) -> BOT -> 24 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 26 } Sat witness: Found: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), { _pt -> cons(b, nil) ; _qt -> cons(a, cons(b, nil)) ; y -> a ; z -> cons(b, nil) }) ------------------------------------------- Step 50, which took 0.049921 s (model generation: 0.047730, model checking: 0.002191): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3768, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3780}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3750, q_gen_3780) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3770, q_gen_3769) -> q_gen_3780 (q_gen_3771, q_gen_3768) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3780) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 (q_gen_3771, q_gen_3739) -> q_gen_3768 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3770, q_gen_3769) -> q_gen_3768 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3789, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3773, q_gen_3789) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { (q_gen_3744, q_gen_3743) -> q_gen_3732 () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 (q_gen_3761, q_gen_3743) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 25 () -> insert([x, nil, cons(x, nil)]) -> 25 () -> leq([a, y]) -> 25 () -> leq([b, b]) -> 25 () -> reverse([nil, nil]) -> 25 () -> sort([nil, nil]) -> 25 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 25 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 28 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 25 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 28 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 25 (leq([b, a])) -> BOT -> 25 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 26 } Sat witness: Found: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), { _ut -> cons(b, cons(a, nil)) ; h1 -> b ; l2 -> cons(b, nil) ; t1 -> cons(b, nil) }) ------------------------------------------- Step 51, which took 0.050130 s (model generation: 0.045150, model checking: 0.004980): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3747, q_gen_3753, q_gen_3758, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3747, q_gen_3741) -> q_gen_3741 (q_gen_3758, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3747 () -> q_gen_3758 () -> q_gen_3758 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3758, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3759 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3758, q_gen_3741) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3783, q_gen_3790, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3790) -> q_gen_3733 (q_gen_3783, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3783 () -> q_gen_3783 () -> q_gen_3783 (q_gen_3783, q_gen_3790) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 25 () -> insert([x, nil, cons(x, nil)]) -> 25 () -> leq([a, y]) -> 25 () -> leq([b, b]) -> 25 () -> reverse([nil, nil]) -> 25 () -> sort([nil, nil]) -> 25 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 28 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 28 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 26 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 28 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 26 (leq([b, a])) -> BOT -> 26 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 26 } Sat witness: Found: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), { _au -> cons(a, cons(b, nil)) ; _zt -> nil ; h1 -> a ; t1 -> nil }) ------------------------------------------- Step 52, which took 0.047567 s (model generation: 0.045912, model checking: 0.001655): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3747, q_gen_3753, q_gen_3758, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3747, q_gen_3741) -> q_gen_3741 (q_gen_3758, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3747 () -> q_gen_3758 () -> q_gen_3758 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3758, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3747, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3759 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3758, q_gen_3741) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3790, q_gen_3791, q_gen_3792, q_gen_3824}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3790) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3824, q_gen_3733) -> q_gen_3790 (q_gen_3824, q_gen_3790) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 () -> q_gen_3824 () -> q_gen_3824 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732}, Delta= { (q_gen_3744, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 26 () -> insert([x, nil, cons(x, nil)]) -> 26 () -> leq([a, y]) -> 26 () -> leq([b, b]) -> 26 () -> reverse([nil, nil]) -> 26 () -> sort([nil, nil]) -> 26 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 28 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 28 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 26 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 28 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 26 (leq([b, a])) -> BOT -> 26 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 29 } Sat witness: Found: ((reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]), { _eu -> cons(b, nil) ; _fu -> cons(b, cons(b, nil)) ; _gu -> cons(b, cons(b, nil)) ; l -> cons(b, nil) }) ------------------------------------------- Step 53, which took 0.058921 s (model generation: 0.048550, model checking: 0.010371): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3768, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3780}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3750, q_gen_3780) -> q_gen_3780 (q_gen_3770, q_gen_3769) -> q_gen_3780 (q_gen_3771, q_gen_3768) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 (q_gen_3771, q_gen_3739) -> q_gen_3768 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3770, q_gen_3769) -> q_gen_3768 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3789, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3773, q_gen_3789) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 (q_gen_3744, q_gen_3743) -> q_gen_3743 (q_gen_3761, q_gen_3743) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 27 () -> insert([x, nil, cons(x, nil)]) -> 27 () -> leq([a, y]) -> 27 () -> leq([b, b]) -> 27 () -> reverse([nil, nil]) -> 27 () -> sort([nil, nil]) -> 27 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 28 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 28 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 27 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 31 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 27 (leq([b, a])) -> BOT -> 27 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 29 } Sat witness: Found: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), { _pt -> cons(a, cons(b, nil)) ; _qt -> cons(a, cons(a, cons(a, nil))) ; y -> a ; z -> cons(a, cons(b, nil)) }) ------------------------------------------- Step 54, which took 0.064172 s (model generation: 0.050159, model checking: 0.014013): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3768, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3780}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3750, q_gen_3780) -> q_gen_3780 (q_gen_3770, q_gen_3769) -> q_gen_3780 (q_gen_3771, q_gen_3768) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 (q_gen_3771, q_gen_3739) -> q_gen_3768 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3770, q_gen_3769) -> q_gen_3768 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3789, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3773, q_gen_3789) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { (q_gen_3744, q_gen_3760) -> q_gen_3732 () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 (q_gen_3744, q_gen_3743) -> q_gen_3743 (q_gen_3761, q_gen_3743) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 28 () -> insert([x, nil, cons(x, nil)]) -> 28 () -> leq([a, y]) -> 28 () -> leq([b, b]) -> 28 () -> reverse([nil, nil]) -> 28 () -> sort([nil, nil]) -> 28 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 28 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 31 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 28 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 31 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 28 (leq([b, a])) -> BOT -> 28 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 29 } Sat witness: Found: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), { _ut -> cons(a, cons(b, cons(b, nil))) ; h1 -> a ; l2 -> cons(a, cons(b, nil)) ; t1 -> cons(a, nil) }) ------------------------------------------- Step 55, which took 0.063637 s (model generation: 0.062388, model checking: 0.001249): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3767, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3780, q_gen_3788}, Q_f={q_gen_3739, q_gen_3767}, Delta= { (q_gen_3770, q_gen_3769) -> q_gen_3769 () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3750, q_gen_3780) -> q_gen_3780 (q_gen_3770, q_gen_3769) -> q_gen_3780 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 (q_gen_3771, q_gen_3767) -> q_gen_3767 (q_gen_3750, q_gen_3780) -> q_gen_3767 (q_gen_3770, q_gen_3769) -> q_gen_3767 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 (q_gen_3771, q_gen_3739) -> q_gen_3788 (q_gen_3771, q_gen_3788) -> q_gen_3788 (q_gen_3750, q_gen_3780) -> q_gen_3788 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3789, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3773, q_gen_3789) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { (q_gen_3744, q_gen_3760) -> q_gen_3732 () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 (q_gen_3744, q_gen_3743) -> q_gen_3743 (q_gen_3761, q_gen_3743) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 28 () -> insert([x, nil, cons(x, nil)]) -> 28 () -> leq([a, y]) -> 28 () -> leq([b, b]) -> 28 () -> reverse([nil, nil]) -> 28 () -> sort([nil, nil]) -> 28 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 31 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 31 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 29 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 31 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 29 (leq([b, a])) -> BOT -> 29 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 29 } Sat witness: Found: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), { _au -> cons(b, cons(b, cons(b, nil))) ; _zt -> cons(b, nil) ; h1 -> b ; t1 -> cons(a, nil) }) ------------------------------------------- Step 56, which took 0.112301 s (model generation: 0.108875, model checking: 0.003426): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3768, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3780, q_gen_3849}, Q_f={q_gen_3739}, Delta= { () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3770, q_gen_3769) -> q_gen_3849 (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3750, q_gen_3780) -> q_gen_3780 (q_gen_3770, q_gen_3769) -> q_gen_3780 (q_gen_3771, q_gen_3768) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3849) -> q_gen_3739 () -> q_gen_3739 (q_gen_3771, q_gen_3739) -> q_gen_3768 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3770, q_gen_3769) -> q_gen_3768 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3789, q_gen_3791, q_gen_3792}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3773, q_gen_3789) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 (q_gen_3744, q_gen_3743) -> q_gen_3743 (q_gen_3744, q_gen_3760) -> q_gen_3743 (q_gen_3761, q_gen_3743) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 29 () -> insert([x, nil, cons(x, nil)]) -> 29 () -> leq([a, y]) -> 29 () -> leq([b, b]) -> 29 () -> reverse([nil, nil]) -> 29 () -> sort([nil, nil]) -> 29 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 31 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 31 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 29 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 31 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 29 (leq([b, a])) -> BOT -> 29 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 32 } Sat witness: Found: ((reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]), { _eu -> cons(b, nil) ; _fu -> cons(a, nil) ; _gu -> cons(a, nil) ; l -> cons(b, nil) }) ------------------------------------------- Step 57, which took 0.094779 s (model generation: 0.087508, model checking: 0.007271): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771}, Q_f={q_gen_3739}, Delta= { (q_gen_3770, q_gen_3769) -> q_gen_3769 () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3770, q_gen_3769) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3758, q_gen_3759, q_gen_3763}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3758, q_gen_3763) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3758 () -> q_gen_3758 (q_gen_3742, q_gen_3763) -> q_gen_3763 (q_gen_3758, q_gen_3741) -> q_gen_3763 (q_gen_3753, q_gen_3737) -> q_gen_3763 (q_gen_3742, q_gen_3763) -> q_gen_3736 (q_gen_3758, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3759 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3742, q_gen_3763) -> q_gen_3759 (q_gen_3758, q_gen_3741) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3790, q_gen_3791, q_gen_3792, q_gen_3824}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3790) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3824, q_gen_3733) -> q_gen_3790 (q_gen_3824, q_gen_3790) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 (q_gen_3792, q_gen_3791) -> q_gen_3790 () -> q_gen_3824 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761, q_gen_3778}, Q_f={q_gen_3732, q_gen_3743}, Delta= { () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 (q_gen_3778, q_gen_3732) -> q_gen_3743 (q_gen_3778, q_gen_3743) -> q_gen_3743 () -> q_gen_3744 (q_gen_3744, q_gen_3743) -> q_gen_3760 (q_gen_3761, q_gen_3732) -> q_gen_3760 (q_gen_3761, q_gen_3743) -> q_gen_3760 (q_gen_3778, q_gen_3760) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 () -> q_gen_3778 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 30 () -> insert([x, nil, cons(x, nil)]) -> 30 () -> leq([a, y]) -> 30 () -> leq([b, b]) -> 30 () -> reverse([nil, nil]) -> 30 () -> sort([nil, nil]) -> 30 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 31 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 31 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 30 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 34 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 30 (leq([b, a])) -> BOT -> 30 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 32 } Sat witness: Found: ((insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]), { _pt -> cons(b, nil) ; _qt -> cons(b, cons(b, nil)) ; y -> b ; z -> cons(b, nil) }) ------------------------------------------- Step 58, which took 0.111695 s (model generation: 0.099901, model checking: 0.011794): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3768, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3780}, Q_f={q_gen_3739}, Delta= { (q_gen_3770, q_gen_3769) -> q_gen_3769 () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3750, q_gen_3780) -> q_gen_3780 (q_gen_3770, q_gen_3769) -> q_gen_3780 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3771, q_gen_3768) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 () -> q_gen_3739 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3750, q_gen_3780) -> q_gen_3768 (q_gen_3770, q_gen_3769) -> q_gen_3768 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3789, q_gen_3791, q_gen_3792, q_gen_3800, q_gen_3824}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3800) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3773, q_gen_3789) -> q_gen_3789 (q_gen_3824, q_gen_3789) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 (q_gen_3824, q_gen_3733) -> q_gen_3800 (q_gen_3792, q_gen_3791) -> q_gen_3800 () -> q_gen_3824 () -> q_gen_3824 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { (q_gen_3744, q_gen_3743) -> q_gen_3732 (q_gen_3744, q_gen_3760) -> q_gen_3732 (q_gen_3761, q_gen_3743) -> q_gen_3732 () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 31 () -> insert([x, nil, cons(x, nil)]) -> 31 () -> leq([a, y]) -> 31 () -> leq([b, b]) -> 31 () -> reverse([nil, nil]) -> 31 () -> sort([nil, nil]) -> 31 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 31 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 34 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 31 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 34 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 31 (leq([b, a])) -> BOT -> 31 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 32 } Sat witness: Found: ((append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]), { _ut -> cons(a, cons(b, nil)) ; h1 -> a ; l2 -> cons(a, cons(b, nil)) ; t1 -> nil }) ------------------------------------------- Step 59, which took 0.116701 s (model generation: 0.115605, model checking: 0.001096): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3780, q_gen_3788}, Q_f={q_gen_3739}, Delta= { (q_gen_3770, q_gen_3769) -> q_gen_3769 () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3750, q_gen_3780) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3770, q_gen_3769) -> q_gen_3780 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3771, q_gen_3788) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3780) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 (q_gen_3750, q_gen_3780) -> q_gen_3788 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3789, q_gen_3791, q_gen_3792, q_gen_3800, q_gen_3824}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3800) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3773, q_gen_3789) -> q_gen_3789 (q_gen_3824, q_gen_3789) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 (q_gen_3824, q_gen_3733) -> q_gen_3800 (q_gen_3792, q_gen_3791) -> q_gen_3800 () -> q_gen_3824 () -> q_gen_3824 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { (q_gen_3744, q_gen_3743) -> q_gen_3732 (q_gen_3744, q_gen_3760) -> q_gen_3732 () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 (q_gen_3761, q_gen_3743) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 31 () -> insert([x, nil, cons(x, nil)]) -> 31 () -> leq([a, y]) -> 31 () -> leq([b, b]) -> 31 () -> reverse([nil, nil]) -> 31 () -> sort([nil, nil]) -> 31 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 34 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 34 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 32 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 34 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 32 (leq([b, a])) -> BOT -> 32 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 32 } Sat witness: Found: ((append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]), { _au -> cons(a, nil) ; _zt -> nil ; h1 -> b ; t1 -> nil }) ------------------------------------------- Step 60, which took 0.120092 s (model generation: 0.111486, model checking: 0.008606): Model: |_ { append -> {{{ Q={q_gen_3739, q_gen_3749, q_gen_3750, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3780, q_gen_3788, q_gen_3857}, Q_f={q_gen_3739}, Delta= { (q_gen_3770, q_gen_3769) -> q_gen_3769 () -> q_gen_3769 () -> q_gen_3770 () -> q_gen_3770 (q_gen_3750, q_gen_3749) -> q_gen_3749 (q_gen_3750, q_gen_3780) -> q_gen_3749 () -> q_gen_3749 () -> q_gen_3750 () -> q_gen_3750 (q_gen_3770, q_gen_3769) -> q_gen_3780 () -> q_gen_3857 (q_gen_3771, q_gen_3739) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3750, q_gen_3780) -> q_gen_3739 (q_gen_3750, q_gen_3749) -> q_gen_3739 (q_gen_3857, q_gen_3780) -> q_gen_3739 (q_gen_3770, q_gen_3769) -> q_gen_3739 () -> q_gen_3739 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 () -> q_gen_3771 (q_gen_3771, q_gen_3788) -> q_gen_3788 (q_gen_3750, q_gen_3780) -> q_gen_3788 (q_gen_3857, q_gen_3749) -> q_gen_3788 } Datatype: Convolution form: right }}} ; insert -> {{{ Q={q_gen_3736, q_gen_3737, q_gen_3738, q_gen_3741, q_gen_3742, q_gen_3753, q_gen_3759}, Q_f={q_gen_3736}, Delta= { () -> q_gen_3737 () -> q_gen_3738 () -> q_gen_3753 (q_gen_3742, q_gen_3741) -> q_gen_3741 (q_gen_3738, q_gen_3737) -> q_gen_3741 (q_gen_3753, q_gen_3737) -> q_gen_3741 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 () -> q_gen_3742 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3753, q_gen_3737) -> q_gen_3736 (q_gen_3742, q_gen_3741) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3736 (q_gen_3738, q_gen_3737) -> q_gen_3759 (q_gen_3753, q_gen_3737) -> q_gen_3759 } Datatype: Convolution form: right }}} ; leq -> {{{ Q={q_gen_3734, q_gen_3745}, Q_f={q_gen_3734}, Delta= { () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3734 () -> q_gen_3745 } Datatype: Convolution form: right }}} ; reverse -> {{{ Q={q_gen_3733, q_gen_3773, q_gen_3789, q_gen_3790, q_gen_3791, q_gen_3792, q_gen_3824}, Q_f={q_gen_3733}, Delta= { () -> q_gen_3791 () -> q_gen_3792 () -> q_gen_3792 (q_gen_3773, q_gen_3733) -> q_gen_3733 (q_gen_3773, q_gen_3789) -> q_gen_3733 () -> q_gen_3733 () -> q_gen_3773 () -> q_gen_3773 () -> q_gen_3773 (q_gen_3773, q_gen_3790) -> q_gen_3789 (q_gen_3824, q_gen_3733) -> q_gen_3789 (q_gen_3824, q_gen_3790) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3789 (q_gen_3792, q_gen_3791) -> q_gen_3790 () -> q_gen_3824 } Datatype: Convolution form: right }}} ; sort -> {{{ Q={q_gen_3732, q_gen_3743, q_gen_3744, q_gen_3760, q_gen_3761}, Q_f={q_gen_3732, q_gen_3743}, Delta= { (q_gen_3744, q_gen_3743) -> q_gen_3732 (q_gen_3744, q_gen_3760) -> q_gen_3732 (q_gen_3761, q_gen_3743) -> q_gen_3732 () -> q_gen_3732 (q_gen_3744, q_gen_3732) -> q_gen_3743 () -> q_gen_3744 () -> q_gen_3744 (q_gen_3761, q_gen_3732) -> q_gen_3760 () -> q_gen_3761 () -> q_gen_3761 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 32 () -> insert([x, nil, cons(x, nil)]) -> 32 () -> leq([a, y]) -> 32 () -> leq([b, b]) -> 32 () -> reverse([nil, nil]) -> 32 () -> sort([nil, nil]) -> 32 (append([_zt, cons(h1, nil), _au]) /\ reverse([t1, _zt])) -> reverse([cons(h1, t1), _au]) -> 34 (append([t1, l2, _ut])) -> append([cons(h1, t1), l2, cons(h1, _ut)]) -> 34 (insert([x, z, _kt]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _kt)]) -> 32 (insert([y, _pt, _qt]) /\ sort([z, _pt])) -> sort([cons(y, z), _qt]) -> 34 (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 32 (leq([b, a])) -> BOT -> 32 (reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]) -> 35 } Sat witness: Found: ((reverse([l, _fu]) /\ sort([_fu, _gu]) /\ sort([l, _eu])) -> eq_eltlist([_eu, _gu]), { _eu -> cons(a, nil) ; _fu -> cons(b, nil) ; _gu -> cons(b, nil) ; l -> cons(a, nil) }) Total time: 60.000388 Reason for stopping: DontKnow. Stopped because: timeout