Solving ../../benchmarks/true/length_reverse_natlist.smt2... Inference procedure has parameters: Ice fuel: 200 Timeout: 30s Convolution: complete Learning problem is: env: { nat -> {s, z} ; natlist -> {cons, nil} } definition: { (append, F: {() -> append([nil, l2, l2]) (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)])} (append([_mea, _nea, _oea]) /\ append([_mea, _nea, _pea])) -> eq_natlist([_oea, _pea]) ) (reverse, F: {() -> reverse([nil, nil]) (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea])} (reverse([_sea, _tea]) /\ reverse([_sea, _uea])) -> eq_natlist([_tea, _uea]) ) (leq, P: {() -> leq([z, s(nn2)]) () -> leq([z, z]) (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) (leq([s(nn1), z])) -> BOT} ) (length, F: {() -> length([nil, z]) (length([ll, _vea])) -> length([cons(x, ll), s(_vea)])} (length([_wea, _xea]) /\ length([_wea, _yea])) -> eq_nat([_xea, _yea]) ) } properties: {(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa])} over-approximation: {append, length, reverse} under-approximation: {leq} Clause system for inference is: { () -> append([nil, l2, l2]) -> 0 ; () -> length([nil, z]) -> 0 ; () -> leq([z, s(nn2)]) -> 0 ; () -> leq([z, z]) -> 0 ; () -> reverse([nil, nil]) -> 0 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 0 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 0 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 0 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 0 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0 ; (leq([s(nn1), z])) -> BOT -> 0 } Solving took 30.000092 seconds. DontKnow. Stopped because: timeout Working model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3731, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3738, q_gen_3739, q_gen_3740, q_gen_3741, q_gen_3742, q_gen_3743, q_gen_3751, q_gen_3752, q_gen_3753, q_gen_3754, q_gen_3755, q_gen_3761, q_gen_3762, q_gen_3763, q_gen_3764, q_gen_3765, q_gen_3769, q_gen_3770, q_gen_3771, q_gen_3772, q_gen_3778, q_gen_3779, q_gen_3780, q_gen_3781, q_gen_3782, q_gen_3785, q_gen_3786, q_gen_3787, q_gen_3788, q_gen_3789, q_gen_3790, q_gen_3795, q_gen_3796, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803, q_gen_3804, q_gen_3807, q_gen_3808, q_gen_3809, q_gen_3814, q_gen_3815, q_gen_3816, q_gen_3817, q_gen_3818, q_gen_3819, q_gen_3820, q_gen_3821, q_gen_3822, q_gen_3823, q_gen_3824, q_gen_3825, q_gen_3826, q_gen_3831, q_gen_3832, q_gen_3833, q_gen_3834, q_gen_3835, q_gen_3836, q_gen_3837, q_gen_3840, q_gen_3841, q_gen_3842, q_gen_3843, q_gen_3844, 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_gen_3859, q_gen_3860, q_gen_3861, q_gen_3862, q_gen_3863, q_gen_3864, q_gen_3865, q_gen_3866, q_gen_3867, q_gen_3868, q_gen_3869, q_gen_3870, q_gen_3871, q_gen_3872, q_gen_3873, q_gen_3874, q_gen_3875, q_gen_3876, q_gen_3877, q_gen_3878, q_gen_3879, q_gen_3880, q_gen_3881, q_gen_3882, q_gen_3883, q_gen_3884, q_gen_3885, q_gen_3886, q_gen_3887, q_gen_3888, q_gen_3889, q_gen_3890, q_gen_3891, q_gen_3901, q_gen_3902, q_gen_3904, q_gen_3905, q_gen_3906, q_gen_3907, q_gen_3908}, Q_f={}, Delta= { () -> q_gen_3740 (q_gen_3740) -> q_gen_3753 () -> q_gen_3764 (q_gen_3740, q_gen_3764) -> q_gen_3781 () -> q_gen_3732 () -> q_gen_3733 () -> q_gen_3734 () -> q_gen_3735 (q_gen_3740) -> q_gen_3739 (q_gen_3740) -> q_gen_3741 (q_gen_3735) -> q_gen_3742 (q_gen_3753) -> q_gen_3752 (q_gen_3753) -> q_gen_3754 (q_gen_3742) -> q_gen_3755 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3762 (q_gen_3740, q_gen_3764) -> q_gen_3763 (q_gen_3740, q_gen_3764) -> q_gen_3765 (q_gen_3735, q_gen_3733) -> q_gen_3770 (q_gen_3735, q_gen_3734) -> q_gen_3771 (q_gen_3735, q_gen_3765, q_gen_3763, q_gen_3762) -> q_gen_3779 (q_gen_3740, q_gen_3781) -> q_gen_3780 (q_gen_3740, q_gen_3781) -> q_gen_3782 (q_gen_3787, q_gen_3739) -> q_gen_3786 (q_gen_3740) -> q_gen_3787 (q_gen_3789, q_gen_3741) -> q_gen_3788 (q_gen_3740) -> q_gen_3789 (q_gen_3740, q_gen_3764) -> q_gen_3808 (q_gen_3740, q_gen_3781) -> q_gen_3826 (q_gen_3753) -> q_gen_3854 (q_gen_3789) -> q_gen_3874 () -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3731 (q_gen_3742, q_gen_3741, q_gen_3739, q_gen_3732) -> q_gen_3738 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3743 (q_gen_3755, q_gen_3754, q_gen_3752, q_gen_3732) -> q_gen_3751 (q_gen_3735, q_gen_3765, q_gen_3763, q_gen_3762) -> q_gen_3761 (q_gen_3742, q_gen_3771, q_gen_3770, q_gen_3762) -> q_gen_3769 (q_gen_3755, q_gen_3754, q_gen_3752, q_gen_3732) -> q_gen_3772 (q_gen_3735, q_gen_3782, q_gen_3780, q_gen_3779) -> q_gen_3778 (q_gen_3755, q_gen_3788, q_gen_3786, q_gen_3762) -> q_gen_3785 (q_gen_3787, q_gen_3734, q_gen_3739, q_gen_3732) -> q_gen_3790 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3796) -> q_gen_3795 (q_gen_3740, q_gen_3764) -> q_gen_3796 () -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3798 () -> q_gen_3799 (q_gen_3740, q_gen_3764) -> q_gen_3800 () -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3803 (q_gen_3789, q_gen_3741, q_gen_3733, q_gen_3732) -> q_gen_3804 (q_gen_3735, q_gen_3765, q_gen_3733, q_gen_3808) -> q_gen_3807 (q_gen_3735, q_gen_3765, q_gen_3733, q_gen_3808) -> q_gen_3809 (q_gen_3823, q_gen_3820, q_gen_3819, q_gen_3818, q_gen_3817, q_gen_3816, q_gen_3815, q_gen_3796) -> q_gen_3814 (q_gen_3753) -> q_gen_3815 (q_gen_3735, q_gen_3734) -> q_gen_3816 (q_gen_3787) -> q_gen_3817 (q_gen_3789, q_gen_3741) -> q_gen_3818 (q_gen_3742) -> q_gen_3819 (q_gen_3822, q_gen_3821) -> q_gen_3820 (q_gen_3740) -> q_gen_3821 (q_gen_3740) -> q_gen_3822 (q_gen_3824) -> q_gen_3823 (q_gen_3735) -> q_gen_3824 (q_gen_3735, q_gen_3782, q_gen_3733, q_gen_3826) -> q_gen_3825 (q_gen_3824, q_gen_3836, q_gen_3835, q_gen_3834, q_gen_3833, q_gen_3798, q_gen_3832, q_gen_3796) -> q_gen_3831 (q_gen_3740) -> q_gen_3832 (q_gen_3740) -> q_gen_3833 (q_gen_3735, q_gen_3734) -> q_gen_3834 (q_gen_3735) -> q_gen_3835 (q_gen_3735, q_gen_3734) -> q_gen_3836 (q_gen_3789, q_gen_3771, q_gen_3733, q_gen_3808) -> q_gen_3837 (q_gen_3844, q_gen_3842, q_gen_3835, q_gen_3834, q_gen_3841, q_gen_3816, q_gen_3832, q_gen_3796) -> q_gen_3840 (q_gen_3735) -> q_gen_3841 (q_gen_3803, q_gen_3843) -> q_gen_3842 () -> q_gen_3843 (q_gen_3803) -> q_gen_3844 (q_gen_3850, q_gen_3849, q_gen_3801, q_gen_3800, q_gen_3848, q_gen_3816, q_gen_3797, q_gen_3796) -> q_gen_3847 (q_gen_3740) -> q_gen_3848 (q_gen_3735, q_gen_3734) -> q_gen_3849 (q_gen_3740) -> q_gen_3850 (q_gen_3854, q_gen_3754, q_gen_3733, q_gen_3732) -> q_gen_3853 (q_gen_3860, q_gen_3858, q_gen_3835, q_gen_3834, q_gen_3857, q_gen_3856, q_gen_3832, q_gen_3796) -> q_gen_3855 (q_gen_3789, q_gen_3741) -> q_gen_3856 (q_gen_3789) -> q_gen_3857 (q_gen_3850, q_gen_3859) -> q_gen_3858 (q_gen_3740) -> q_gen_3859 (q_gen_3850) -> q_gen_3860 (q_gen_3866, q_gen_3863, q_gen_3819, q_gen_3818, q_gen_3862, q_gen_3856, q_gen_3815, q_gen_3796) -> q_gen_3861 (q_gen_3742) -> q_gen_3862 (q_gen_3865, q_gen_3864) -> q_gen_3863 (q_gen_3735) -> q_gen_3864 (q_gen_3735) -> q_gen_3865 (q_gen_3844) -> q_gen_3866 (q_gen_3844, q_gen_3871, q_gen_3835, q_gen_3870, q_gen_3841, q_gen_3869, q_gen_3832, q_gen_3868) -> q_gen_3867 (q_gen_3753, q_gen_3764) -> q_gen_3868 (q_gen_3787, q_gen_3734) -> q_gen_3869 (q_gen_3787, q_gen_3734) -> q_gen_3870 (q_gen_3872, q_gen_3843) -> q_gen_3871 (q_gen_3740) -> q_gen_3872 (q_gen_3874, q_gen_3754, q_gen_3739, q_gen_3732) -> q_gen_3873 (q_gen_3860, q_gen_3877, q_gen_3835, q_gen_3870, q_gen_3857, q_gen_3876, q_gen_3832, q_gen_3868) -> q_gen_3875 (q_gen_3742, q_gen_3741) -> q_gen_3876 (q_gen_3878, q_gen_3859) -> q_gen_3877 (q_gen_3735) -> q_gen_3878 (q_gen_3803, q_gen_3884, q_gen_3883, q_gen_3882, q_gen_3799, q_gen_3881, q_gen_3880, q_gen_3809) -> q_gen_3879 (q_gen_3740, q_gen_3764) -> q_gen_3880 (q_gen_3740, q_gen_3781) -> q_gen_3881 (q_gen_3735, q_gen_3765, q_gen_3733, q_gen_3808) -> q_gen_3882 (q_gen_3740, q_gen_3764) -> q_gen_3883 (q_gen_3740, q_gen_3781) -> q_gen_3884 (q_gen_3803, q_gen_3884, q_gen_3801, q_gen_3889, q_gen_3888, q_gen_3887, q_gen_3886, q_gen_3807) -> q_gen_3885 (q_gen_3740, q_gen_3764) -> q_gen_3886 (q_gen_3735, q_gen_3765, q_gen_3733, q_gen_3808) -> q_gen_3887 (q_gen_3740, q_gen_3764) -> q_gen_3888 (q_gen_3740, q_gen_3781) -> q_gen_3889 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3888, q_gen_3891, q_gen_3886, q_gen_3731) -> q_gen_3890 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3891 (q_gen_3803, q_gen_3884, q_gen_3801, q_gen_3889, q_gen_3799, q_gen_3881, q_gen_3797, q_gen_3902) -> q_gen_3901 (q_gen_3740, q_gen_3781) -> q_gen_3902 (q_gen_3824, q_gen_3908, q_gen_3835, q_gen_3907, q_gen_3906, q_gen_3887, q_gen_3905, q_gen_3807) -> q_gen_3904 (q_gen_3735, q_gen_3733) -> q_gen_3905 (q_gen_3735, q_gen_3733) -> q_gen_3906 (q_gen_3735, q_gen_3765) -> q_gen_3907 (q_gen_3735, q_gen_3765) -> q_gen_3908 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3729, q_gen_3730, q_gen_3748, q_gen_3749, q_gen_3750, q_gen_3766, q_gen_3767, q_gen_3768, q_gen_3783, q_gen_3784, q_gen_3793, q_gen_3794, q_gen_3898, q_gen_3899}, Q_f={}, Delta= { () -> q_gen_3750 (q_gen_3750) -> q_gen_3768 () -> q_gen_3726 (q_gen_3730, q_gen_3726) -> q_gen_3729 () -> q_gen_3730 (q_gen_3749, q_gen_3726) -> q_gen_3748 (q_gen_3750) -> q_gen_3749 (q_gen_3767, q_gen_3726) -> q_gen_3766 (q_gen_3768) -> q_gen_3767 (q_gen_3784, q_gen_3729) -> q_gen_3783 (q_gen_3730) -> q_gen_3784 (q_gen_3794, q_gen_3729) -> q_gen_3793 (q_gen_3750) -> q_gen_3794 (q_gen_3899, q_gen_3793) -> q_gen_3898 (q_gen_3768) -> q_gen_3899 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3724, q_gen_3725, q_gen_3728, q_gen_3736, q_gen_3737, q_gen_3896, q_gen_3897, q_gen_3900}, Q_f={}, Delta= { () -> q_gen_3725 (q_gen_3725) -> q_gen_3737 () -> q_gen_3723 (q_gen_3725) -> q_gen_3724 (q_gen_3723) -> q_gen_3728 (q_gen_3737) -> q_gen_3736 (q_gen_3725) -> q_gen_3896 (q_gen_3896) -> q_gen_3897 (q_gen_3897) -> q_gen_3900 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3744, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3756, q_gen_3757, q_gen_3758, q_gen_3759, q_gen_3760, q_gen_3773, q_gen_3774, q_gen_3775, q_gen_3776, q_gen_3777, q_gen_3791, q_gen_3792, q_gen_3805, q_gen_3806, q_gen_3810, q_gen_3811, q_gen_3812, q_gen_3813, q_gen_3827, q_gen_3828, q_gen_3829, q_gen_3830, q_gen_3838, q_gen_3839, q_gen_3845, q_gen_3846, q_gen_3851, q_gen_3852, q_gen_3892, q_gen_3893, q_gen_3894, q_gen_3895, q_gen_3903}, Q_f={}, Delta= { () -> q_gen_3758 (q_gen_3758) -> q_gen_3775 () -> q_gen_3812 (q_gen_3758, q_gen_3812) -> q_gen_3829 () -> q_gen_3722 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3744 () -> q_gen_3745 () -> q_gen_3746 () -> q_gen_3747 (q_gen_3760, q_gen_3759, q_gen_3757, q_gen_3722) -> q_gen_3756 (q_gen_3758) -> q_gen_3757 (q_gen_3758) -> q_gen_3759 (q_gen_3747) -> q_gen_3760 (q_gen_3777, q_gen_3776, q_gen_3774, q_gen_3722) -> q_gen_3773 (q_gen_3775) -> q_gen_3774 (q_gen_3775) -> q_gen_3776 (q_gen_3760) -> q_gen_3777 (q_gen_3792, q_gen_3746, q_gen_3757, q_gen_3722) -> q_gen_3791 (q_gen_3758) -> q_gen_3792 (q_gen_3806, q_gen_3759, q_gen_3745, q_gen_3722) -> q_gen_3805 (q_gen_3758) -> q_gen_3806 (q_gen_3747, q_gen_3813, q_gen_3745, q_gen_3811) -> q_gen_3810 (q_gen_3758, q_gen_3812) -> q_gen_3811 (q_gen_3758, q_gen_3812) -> q_gen_3813 (q_gen_3747, q_gen_3830, q_gen_3745, q_gen_3828) -> q_gen_3827 (q_gen_3758, q_gen_3829) -> q_gen_3828 (q_gen_3758, q_gen_3829) -> q_gen_3830 (q_gen_3806, q_gen_3839, q_gen_3745, q_gen_3811) -> q_gen_3838 (q_gen_3747, q_gen_3746) -> q_gen_3839 (q_gen_3747, q_gen_3813, q_gen_3846, q_gen_3744) -> q_gen_3845 (q_gen_3758, q_gen_3812) -> q_gen_3846 (q_gen_3792, q_gen_3813, q_gen_3852, q_gen_3744) -> q_gen_3851 (q_gen_3747, q_gen_3745) -> q_gen_3852 (q_gen_3747, q_gen_3813, q_gen_3895, q_gen_3893) -> q_gen_3892 (q_gen_3747, q_gen_3746, q_gen_3846, q_gen_3894) -> q_gen_3893 (q_gen_3758, q_gen_3812) -> q_gen_3894 (q_gen_3758, q_gen_3829) -> q_gen_3895 (q_gen_3747, q_gen_3830, q_gen_3846, q_gen_3810) -> q_gen_3903 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.004683 s (model generation: 0.003971, model checking: 0.000712): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; length -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 ; () -> length([nil, z]) -> 0 ; () -> leq([z, s(nn2)]) -> 0 ; () -> leq([z, z]) -> 0 ; () -> reverse([nil, nil]) -> 3 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 1 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 1 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 1 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 ; (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Yes: (() -> reverse([nil, nil]), { }) ------------------------------------------- Step 1, which took 0.003566 s (model generation: 0.003539, model checking: 0.000027): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; length -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722}, Q_f={q_gen_3722}, Delta= { () -> q_gen_3722 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 ; () -> length([nil, z]) -> 0 ; () -> leq([z, s(nn2)]) -> 0 ; () -> leq([z, z]) -> 3 ; () -> reverse([nil, nil]) -> 3 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 1 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 1 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 1 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 ; (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Yes: (() -> leq([z, z]), { }) ------------------------------------------- Step 2, which took 0.003415 s (model generation: 0.003372, model checking: 0.000043): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; length -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723}, Q_f={q_gen_3723}, Delta= { () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722}, Q_f={q_gen_3722}, Delta= { () -> q_gen_3722 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 ; () -> length([nil, z]) -> 0 ; () -> leq([z, s(nn2)]) -> 3 ; () -> leq([z, z]) -> 3 ; () -> reverse([nil, nil]) -> 3 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 1 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 1 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 1 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 ; (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Yes: (() -> leq([z, s(nn2)]), { nn2 -> z }) ------------------------------------------- Step 3, which took 0.003446 s (model generation: 0.003388, model checking: 0.000058): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; length -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { () -> q_gen_3725 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722}, Q_f={q_gen_3722}, Delta= { () -> q_gen_3722 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 ; () -> length([nil, z]) -> 3 ; () -> leq([z, s(nn2)]) -> 3 ; () -> leq([z, z]) -> 3 ; () -> reverse([nil, nil]) -> 3 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 1 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 1 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 1 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 ; (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Yes: (() -> length([nil, z]), { }) ------------------------------------------- Step 4, which took 0.004494 s (model generation: 0.003424, model checking: 0.001070): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726}, Q_f={q_gen_3726}, Delta= { () -> q_gen_3726 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { () -> q_gen_3725 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722}, Q_f={q_gen_3722}, Delta= { () -> q_gen_3722 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 ; () -> length([nil, z]) -> 3 ; () -> leq([z, s(nn2)]) -> 3 ; () -> leq([z, z]) -> 3 ; () -> reverse([nil, nil]) -> 3 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 1 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 1 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 1 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 ; (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Yes: (() -> append([nil, l2, l2]), { l2 -> nil }) ------------------------------------------- Step 5, which took 0.004884 s (model generation: 0.004774, model checking: 0.000110): Model: |_ { append -> {{{ Q={q_gen_3727}, Q_f={q_gen_3727}, Delta= { () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726}, Q_f={q_gen_3726}, Delta= { () -> q_gen_3726 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { () -> q_gen_3725 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722}, Q_f={q_gen_3722}, Delta= { () -> q_gen_3722 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 ; () -> length([nil, z]) -> 3 ; () -> leq([z, s(nn2)]) -> 3 ; () -> leq([z, z]) -> 3 ; () -> reverse([nil, nil]) -> 3 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 1 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 1 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 1 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2 ; (leq([s(nn1), z])) -> BOT -> 2 } Sat witness: Yes: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), { nn1 -> z ; nn2 -> z }) ------------------------------------------- Step 6, which took 0.006350 s (model generation: 0.006175, model checking: 0.000175): Model: |_ { append -> {{{ Q={q_gen_3727}, Q_f={q_gen_3727}, Delta= { () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726}, Q_f={q_gen_3726}, Delta= { () -> q_gen_3726 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722}, Q_f={q_gen_3722}, Delta= { () -> q_gen_3722 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 ; () -> length([nil, z]) -> 3 ; () -> leq([z, s(nn2)]) -> 3 ; () -> leq([z, z]) -> 3 ; () -> reverse([nil, nil]) -> 3 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 1 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 1 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 4 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2 ; (leq([s(nn1), z])) -> BOT -> 2 } Sat witness: Yes: ((length([ll, _vea])) -> length([cons(x, ll), s(_vea)]), { _vea -> z ; ll -> nil ; x -> z }) ------------------------------------------- Step 7, which took 0.010495 s (model generation: 0.009544, model checking: 0.000951): Model: |_ { append -> {{{ Q={q_gen_3727}, Q_f={q_gen_3727}, Delta= { () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730}, Q_f={q_gen_3726}, Delta= { (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722}, Q_f={q_gen_3722}, Delta= { () -> q_gen_3722 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 ; () -> length([nil, z]) -> 3 ; () -> leq([z, s(nn2)]) -> 3 ; () -> leq([z, z]) -> 3 ; () -> reverse([nil, nil]) -> 3 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 4 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 2 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 4 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2 ; (leq([s(nn1), z])) -> BOT -> 2 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> nil ; h1 -> z ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 8, which took 0.009139 s (model generation: 0.007795, model checking: 0.001344): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735}, Q_f={q_gen_3727}, Delta= { () -> q_gen_3732 () -> q_gen_3733 () -> q_gen_3734 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730}, Q_f={q_gen_3726}, Delta= { (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722}, Q_f={q_gen_3722}, Delta= { () -> q_gen_3722 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 ; () -> length([nil, z]) -> 3 ; () -> leq([z, s(nn2)]) -> 6 ; () -> leq([z, z]) -> 4 ; () -> reverse([nil, nil]) -> 4 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 2 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 4 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 3 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 4 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3 ; (leq([s(nn1), z])) -> BOT -> 3 } Sat witness: Yes: (() -> leq([z, s(nn2)]), { nn2 -> s(z) }) ------------------------------------------- Step 9, which took 0.032196 s (model generation: 0.011043, model checking: 0.021153): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735}, Q_f={q_gen_3727}, Delta= { () -> q_gen_3732 () -> q_gen_3733 () -> q_gen_3734 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730}, Q_f={q_gen_3726}, Delta= { (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722}, Q_f={q_gen_3722}, Delta= { () -> q_gen_3722 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 ; () -> length([nil, z]) -> 4 ; () -> leq([z, s(nn2)]) -> 6 ; () -> leq([z, z]) -> 4 ; () -> reverse([nil, nil]) -> 4 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 3 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 4 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 4 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 4 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4 ; (leq([s(nn1), z])) -> BOT -> 4 } Sat witness: Yes: (() -> append([nil, l2, l2]), { l2 -> cons(s(z), nil) }) ------------------------------------------- Step 10, which took 0.004389 s (model generation: 0.004242, model checking: 0.000147): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740}, Q_f={q_gen_3727}, Delta= { () -> q_gen_3740 () -> q_gen_3732 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3740) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730}, Q_f={q_gen_3726}, Delta= { (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722}, Q_f={q_gen_3722}, Delta= { () -> q_gen_3722 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 ; () -> length([nil, z]) -> 4 ; () -> leq([z, s(nn2)]) -> 6 ; () -> leq([z, z]) -> 4 ; () -> reverse([nil, nil]) -> 4 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 6 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 4 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 4 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 4 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4 ; (leq([s(nn1), z])) -> BOT -> 4 } Sat witness: Yes: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), { _qea -> nil ; _rea -> cons(z, nil) ; h1 -> z ; t1 -> nil }) ------------------------------------------- Step 11, which took 0.005075 s (model generation: 0.004476, model checking: 0.000599): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740}, Q_f={q_gen_3727}, Delta= { () -> q_gen_3740 () -> q_gen_3732 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3740) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730}, Q_f={q_gen_3726}, Delta= { (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747}, Q_f={q_gen_3722}, Delta= { (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 () -> q_gen_3745 () -> q_gen_3746 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 ; () -> length([nil, z]) -> 4 ; () -> leq([z, s(nn2)]) -> 6 ; () -> leq([z, z]) -> 4 ; () -> reverse([nil, nil]) -> 4 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 6 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 4 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 4 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 7 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5 ; (leq([s(nn1), z])) -> BOT -> 5 } Sat witness: Yes: ((length([ll, _vea])) -> length([cons(x, ll), s(_vea)]), { _vea -> z ; ll -> nil ; x -> s(z) }) ------------------------------------------- Step 12, which took 0.009457 s (model generation: 0.006231, model checking: 0.003226): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740}, Q_f={q_gen_3727}, Delta= { () -> q_gen_3740 () -> q_gen_3732 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3740) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747}, Q_f={q_gen_3722}, Delta= { (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 () -> q_gen_3745 () -> q_gen_3746 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 ; () -> length([nil, z]) -> 4 ; () -> leq([z, s(nn2)]) -> 6 ; () -> leq([z, z]) -> 4 ; () -> reverse([nil, nil]) -> 4 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 6 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 7 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 5 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 7 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5 ; (leq([s(nn1), z])) -> BOT -> 5 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> nil ; h1 -> s(s(z)) ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 13, which took 0.012239 s (model generation: 0.009678, model checking: 0.002561): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 () -> q_gen_3732 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3740) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747}, Q_f={q_gen_3722}, Delta= { (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 () -> q_gen_3745 () -> q_gen_3746 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 ; () -> length([nil, z]) -> 5 ; () -> leq([z, s(nn2)]) -> 6 ; () -> leq([z, z]) -> 5 ; () -> reverse([nil, nil]) -> 5 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 9 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 7 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 6 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 7 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 6 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6 ; (leq([s(nn1), z])) -> BOT -> 6 } Sat witness: Yes: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), { _qea -> nil ; _rea -> cons(s(z), nil) ; h1 -> s(z) ; t1 -> nil }) ------------------------------------------- Step 14, which took 0.041928 s (model generation: 0.011858, model checking: 0.030070): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 () -> q_gen_3732 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3740) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758}, Q_f={q_gen_3722}, Delta= { () -> q_gen_3758 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 9 ; () -> length([nil, z]) -> 6 ; () -> leq([z, s(nn2)]) -> 7 ; () -> leq([z, z]) -> 6 ; () -> reverse([nil, nil]) -> 6 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 9 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 7 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 7 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 7 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7 ; (leq([s(nn1), z])) -> BOT -> 7 } Sat witness: Yes: (() -> append([nil, l2, l2]), { l2 -> cons(z, cons(z, nil)) }) ------------------------------------------- Step 15, which took 0.006183 s (model generation: 0.005617, model checking: 0.000566): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758}, Q_f={q_gen_3722}, Delta= { () -> q_gen_3758 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 9 ; () -> length([nil, z]) -> 7 ; () -> leq([z, s(nn2)]) -> 7 ; () -> leq([z, z]) -> 7 ; () -> reverse([nil, nil]) -> 7 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 9 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 7 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 7 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 10 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8 ; (leq([s(nn1), z])) -> BOT -> 8 } Sat witness: Yes: ((length([ll, _vea])) -> length([cons(x, ll), s(_vea)]), { _vea -> z ; ll -> nil ; x -> s(s(z)) }) ------------------------------------------- Step 16, which took 0.009558 s (model generation: 0.005736, model checking: 0.003822): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758}, Q_f={q_gen_3722}, Delta= { () -> q_gen_3758 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 9 ; () -> length([nil, z]) -> 7 ; () -> leq([z, s(nn2)]) -> 7 ; () -> leq([z, z]) -> 7 ; () -> reverse([nil, nil]) -> 7 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 9 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 10 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 8 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 10 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8 ; (leq([s(nn1), z])) -> BOT -> 8 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(z, nil) ; h1 -> s(z) ; l2 -> nil ; t1 -> cons(z, nil) }) ------------------------------------------- Step 17, which took 0.007395 s (model generation: 0.006078, model checking: 0.001317): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758}, Q_f={q_gen_3722}, Delta= { () -> q_gen_3758 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 9 ; () -> length([nil, z]) -> 8 ; () -> leq([z, s(nn2)]) -> 8 ; () -> leq([z, z]) -> 8 ; () -> reverse([nil, nil]) -> 8 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 12 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 10 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 9 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 10 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9 ; (leq([s(nn1), z])) -> BOT -> 9 } Sat witness: Yes: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), { _qea -> nil ; _rea -> cons(s(s(z)), nil) ; h1 -> s(s(z)) ; t1 -> nil }) ------------------------------------------- Step 18, which took 0.052308 s (model generation: 0.008257, model checking: 0.044051): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 12 ; () -> length([nil, z]) -> 9 ; () -> leq([z, s(nn2)]) -> 9 ; () -> leq([z, z]) -> 9 ; () -> reverse([nil, nil]) -> 9 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 12 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 10 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 10 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 10 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10 ; (leq([s(nn1), z])) -> BOT -> 10 } Sat witness: Yes: (() -> append([nil, l2, l2]), { l2 -> cons(z, cons(z, cons(z, nil))) }) ------------------------------------------- Step 19, which took 0.008679 s (model generation: 0.008199, model checking: 0.000480): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 12 ; () -> length([nil, z]) -> 10 ; () -> leq([z, s(nn2)]) -> 10 ; () -> leq([z, z]) -> 10 ; () -> reverse([nil, nil]) -> 10 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 12 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 10 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 10 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 13 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11 ; (leq([s(nn1), z])) -> BOT -> 11 } Sat witness: Yes: ((length([ll, _vea])) -> length([cons(x, ll), s(_vea)]), { _vea -> s(z) ; ll -> cons(z, nil) ; x -> s(z) }) ------------------------------------------- Step 20, which took 0.012152 s (model generation: 0.008029, model checking: 0.004123): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 12 ; () -> length([nil, z]) -> 10 ; () -> leq([z, s(nn2)]) -> 10 ; () -> leq([z, z]) -> 10 ; () -> reverse([nil, nil]) -> 10 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 12 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 13 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 11 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 13 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11 ; (leq([s(nn1), z])) -> BOT -> 11 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(z, nil) ; h1 -> s(s(z)) ; l2 -> nil ; t1 -> cons(z, nil) }) ------------------------------------------- Step 21, which took 0.009649 s (model generation: 0.008676, model checking: 0.000973): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 12 ; () -> length([nil, z]) -> 11 ; () -> leq([z, s(nn2)]) -> 11 ; () -> leq([z, z]) -> 11 ; () -> reverse([nil, nil]) -> 11 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 15 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 13 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 12 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 13 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 12 ; (leq([s(nn1), z])) -> BOT -> 12 } Sat witness: Yes: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), { _qea -> nil ; _rea -> cons(s(z), nil) ; h1 -> z ; t1 -> nil }) ------------------------------------------- Step 22, which took 0.018219 s (model generation: 0.015678, model checking: 0.002541): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 13 ; () -> length([nil, z]) -> 12 ; () -> leq([z, s(nn2)]) -> 12 ; () -> leq([z, z]) -> 12 ; () -> reverse([nil, nil]) -> 12 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 15 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 13 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 13 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 16 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13 ; (leq([s(nn1), z])) -> BOT -> 13 } Sat witness: Yes: ((length([ll, _vea])) -> length([cons(x, ll), s(_vea)]), { _vea -> s(z) ; ll -> cons(z, nil) ; x -> z }) ------------------------------------------- Step 23, which took 0.020609 s (model generation: 0.015280, model checking: 0.005329): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 13 ; () -> length([nil, z]) -> 13 ; () -> leq([z, s(nn2)]) -> 13 ; () -> leq([z, z]) -> 13 ; () -> reverse([nil, nil]) -> 13 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 15 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 16 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 14 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 16 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14 ; (leq([s(nn1), z])) -> BOT -> 14 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(z, nil) ; h1 -> z ; l2 -> cons(z, nil) ; t1 -> nil }) ------------------------------------------- Step 24, which took 0.022385 s (model generation: 0.015992, model checking: 0.006393): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 () -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3798 () -> q_gen_3799 (q_gen_3740, q_gen_3764) -> q_gen_3800 () -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 14 ; () -> length([nil, z]) -> 14 ; () -> leq([z, s(nn2)]) -> 14 ; () -> leq([z, z]) -> 14 ; () -> reverse([nil, nil]) -> 14 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 18 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 16 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 15 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 16 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 15 ; (leq([s(nn1), z])) -> BOT -> 15 } Sat witness: Yes: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), { _qea -> nil ; _rea -> cons(z, nil) ; h1 -> s(z) ; t1 -> nil }) ------------------------------------------- Step 25, which took 0.053865 s (model generation: 0.021082, model checking: 0.032783): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 () -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3798 () -> q_gen_3799 (q_gen_3740, q_gen_3764) -> q_gen_3800 () -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 15 ; () -> length([nil, z]) -> 15 ; () -> leq([z, s(nn2)]) -> 15 ; () -> leq([z, z]) -> 15 ; () -> reverse([nil, nil]) -> 15 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 18 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 19 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 16 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 17 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 16 ; (leq([s(nn1), z])) -> BOT -> 16 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(z, nil) ; h1 -> z ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 26, which took 0.015820 s (model generation: 0.012454, model checking: 0.003366): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 () -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3798 () -> q_gen_3799 (q_gen_3740, q_gen_3764) -> q_gen_3800 () -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 16 ; () -> length([nil, z]) -> 16 ; () -> leq([z, s(nn2)]) -> 16 ; () -> leq([z, z]) -> 16 ; () -> reverse([nil, nil]) -> 16 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 21 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 19 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 17 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 18 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17 ; (leq([s(nn1), z])) -> BOT -> 17 } Sat witness: Yes: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), { _qea -> nil ; _rea -> cons(z, cons(z, nil)) ; h1 -> z ; t1 -> nil }) ------------------------------------------- Step 27, which took 0.552367 s (model generation: 0.016527, model checking: 0.535840): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 () -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3798 () -> q_gen_3799 (q_gen_3740, q_gen_3764) -> q_gen_3800 () -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 17 ; () -> length([nil, z]) -> 17 ; () -> leq([z, s(nn2)]) -> 17 ; () -> leq([z, z]) -> 17 ; () -> reverse([nil, nil]) -> 17 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 21 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 22 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 18 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 19 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 18 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 18 ; (leq([s(nn1), z])) -> BOT -> 18 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(z, nil) ; h1 -> s(s(z)) ; l2 -> cons(s(z), nil) ; t1 -> nil }) ------------------------------------------- Step 28, which took 0.019633 s (model generation: 0.015844, model checking: 0.003789): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3735) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 18 ; () -> length([nil, z]) -> 18 ; () -> leq([z, s(nn2)]) -> 18 ; () -> leq([z, z]) -> 18 ; () -> reverse([nil, nil]) -> 18 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 24 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 22 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 19 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 20 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 19 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19 ; (leq([s(nn1), z])) -> BOT -> 19 } Sat witness: Yes: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), { _qea -> nil ; _rea -> cons(z, cons(z, cons(z, nil))) ; h1 -> z ; t1 -> nil }) ------------------------------------------- Step 29, which took 0.181374 s (model generation: 0.016953, model checking: 0.164421): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3735) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 19 ; () -> length([nil, z]) -> 19 ; () -> leq([z, s(nn2)]) -> 19 ; () -> leq([z, z]) -> 19 ; () -> reverse([nil, nil]) -> 19 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 24 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 25 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 20 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 21 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 20 ; (leq([s(nn1), z])) -> BOT -> 20 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(z, nil) ; h1 -> s(z) ; l2 -> cons(z, nil) ; t1 -> nil }) ------------------------------------------- Step 30, which took 0.023054 s (model generation: 0.019052, model checking: 0.004002): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 20 ; () -> length([nil, z]) -> 20 ; () -> leq([z, s(nn2)]) -> 20 ; () -> leq([z, z]) -> 20 ; () -> reverse([nil, nil]) -> 20 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 27 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 25 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 21 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 22 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 21 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21 ; (leq([s(nn1), z])) -> BOT -> 21 } Sat witness: Yes: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), { _qea -> nil ; _rea -> cons(z, cons(z, nil)) ; h1 -> s(z) ; t1 -> nil }) ------------------------------------------- Step 31, which took 0.186360 s (model generation: 0.020179, model checking: 0.166181): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 21 ; () -> length([nil, z]) -> 21 ; () -> leq([z, s(nn2)]) -> 21 ; () -> leq([z, z]) -> 21 ; () -> reverse([nil, nil]) -> 21 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 27 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 28 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 22 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 23 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 22 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22 ; (leq([s(nn1), z])) -> BOT -> 22 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(z, nil) ; h1 -> s(z) ; l2 -> cons(s(z), nil) ; t1 -> nil }) ------------------------------------------- Step 32, which took 0.027356 s (model generation: 0.020685, model checking: 0.006671): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 22 ; () -> length([nil, z]) -> 22 ; () -> leq([z, s(nn2)]) -> 22 ; () -> leq([z, z]) -> 22 ; () -> reverse([nil, nil]) -> 22 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 30 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 28 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 23 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 24 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 23 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23 ; (leq([s(nn1), z])) -> BOT -> 23 } Sat witness: Yes: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), { _qea -> cons(z, nil) ; _rea -> cons(z, cons(z, nil)) ; h1 -> z ; t1 -> cons(z, nil) }) ------------------------------------------- Step 33, which took 0.218237 s (model generation: 0.024022, model checking: 0.194215): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 23 ; () -> length([nil, z]) -> 23 ; () -> leq([z, s(nn2)]) -> 23 ; () -> leq([z, z]) -> 23 ; () -> reverse([nil, nil]) -> 23 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 30 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 31 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 24 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 25 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 24 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 24 ; (leq([s(nn1), z])) -> BOT -> 24 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(z, nil) ; h1 -> z ; l2 -> cons(s(z), nil) ; t1 -> nil }) ------------------------------------------- Step 34, which took 0.031021 s (model generation: 0.023383, model checking: 0.007638): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 24 ; () -> length([nil, z]) -> 24 ; () -> leq([z, s(nn2)]) -> 24 ; () -> leq([z, z]) -> 24 ; () -> reverse([nil, nil]) -> 24 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 33 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 31 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 25 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 26 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 25 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 25 ; (leq([s(nn1), z])) -> BOT -> 25 } Sat witness: Yes: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), { _qea -> cons(s(z), nil) ; _rea -> cons(s(z), cons(z, nil)) ; h1 -> z ; t1 -> cons(z, nil) }) ------------------------------------------- Step 35, which took 0.180204 s (model generation: 0.023988, model checking: 0.156216): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 25 ; () -> length([nil, z]) -> 25 ; () -> leq([z, s(nn2)]) -> 25 ; () -> leq([z, z]) -> 25 ; () -> reverse([nil, nil]) -> 25 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 33 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 34 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 26 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 27 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 26 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 26 ; (leq([s(nn1), z])) -> BOT -> 26 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(z, nil) ; h1 -> s(z) ; l2 -> cons(s(s(z)), nil) ; t1 -> nil }) ------------------------------------------- Step 36, which took 0.400421 s (model generation: 0.035360, model checking: 0.365061): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 26 ; () -> length([nil, z]) -> 26 ; () -> leq([z, s(nn2)]) -> 26 ; () -> leq([z, z]) -> 26 ; () -> reverse([nil, nil]) -> 26 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 34 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 37 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 27 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 28 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 27 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 27 ; (leq([s(nn1), z])) -> BOT -> 27 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(z, nil) ; h1 -> s(s(z)) ; l2 -> cons(s(s(z)), nil) ; t1 -> nil }) ------------------------------------------- Step 37, which took 0.544164 s (model generation: 0.030824, model checking: 0.513340): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 27 ; () -> length([nil, z]) -> 27 ; () -> leq([z, s(nn2)]) -> 27 ; () -> leq([z, z]) -> 27 ; () -> reverse([nil, nil]) -> 27 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 35 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 40 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 28 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 29 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 28 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 28 ; (leq([s(nn1), z])) -> BOT -> 28 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(s(z), nil) ; h1 -> s(z) ; l2 -> cons(s(z), nil) ; t1 -> nil }) ------------------------------------------- Step 38, which took 0.560905 s (model generation: 0.034553, model checking: 0.526352): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 28 ; () -> length([nil, z]) -> 28 ; () -> leq([z, s(nn2)]) -> 28 ; () -> leq([z, z]) -> 28 ; () -> reverse([nil, nil]) -> 28 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 36 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 43 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 29 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 30 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 29 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 29 ; (leq([s(nn1), z])) -> BOT -> 29 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(s(z), nil) ; h1 -> s(z) ; l2 -> cons(s(s(z)), nil) ; t1 -> nil }) ------------------------------------------- Step 39, which took 0.814265 s (model generation: 0.056895, model checking: 0.757370): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 29 ; () -> length([nil, z]) -> 29 ; () -> leq([z, s(nn2)]) -> 29 ; () -> leq([z, z]) -> 29 ; () -> reverse([nil, nil]) -> 29 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 37 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 46 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 30 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 31 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 30 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 30 ; (leq([s(nn1), z])) -> BOT -> 30 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(z, cons(z, nil)) ; h1 -> z ; l2 -> cons(z, cons(z, nil)) ; t1 -> nil }) ------------------------------------------- Step 40, which took 1.705466 s (model generation: 0.067573, model checking: 1.637893): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 30 ; () -> length([nil, z]) -> 30 ; () -> leq([z, s(nn2)]) -> 30 ; () -> leq([z, z]) -> 30 ; () -> reverse([nil, nil]) -> 30 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 38 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 49 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 31 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 32 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 31 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 31 ; (leq([s(nn1), z])) -> BOT -> 31 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(z, cons(z, nil)) ; h1 -> z ; l2 -> cons(z, nil) ; t1 -> cons(z, nil) }) ------------------------------------------- Step 41, which took 0.081261 s (model generation: 0.075276, model checking: 0.005985): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3798 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3799 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 31 ; () -> length([nil, z]) -> 31 ; () -> leq([z, s(nn2)]) -> 31 ; () -> leq([z, z]) -> 31 ; () -> reverse([nil, nil]) -> 31 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 41 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 49 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 32 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 33 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 32 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 32 ; (leq([s(nn1), z])) -> BOT -> 32 } Sat witness: Yes: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), { _qea -> cons(z, cons(z, nil)) ; _rea -> cons(z, cons(z, nil)) ; h1 -> z ; t1 -> cons(z, cons(z, nil)) }) ------------------------------------------- Step 42, which took 0.091089 s (model generation: 0.088712, model checking: 0.002377): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3798 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3799 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 32 ; () -> length([nil, z]) -> 32 ; () -> leq([z, s(nn2)]) -> 32 ; () -> leq([z, z]) -> 32 ; () -> reverse([nil, nil]) -> 32 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 41 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 49 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 35 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 33 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 33 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 33 ; (leq([s(nn1), z])) -> BOT -> 33 } Sat witness: Yes: ((length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]), { _afa -> nil ; _bfa -> z ; _zea -> s(z) ; l1 -> cons(z, nil) }) ------------------------------------------- Step 43, which took 0.091415 s (model generation: 0.089232, model checking: 0.002183): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3798 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3799 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 33 ; () -> length([nil, z]) -> 33 ; () -> leq([z, s(nn2)]) -> 33 ; () -> leq([z, z]) -> 33 ; () -> reverse([nil, nil]) -> 33 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 41 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 49 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 35 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 33 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 33 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 33 ; (leq([s(nn1), z])) -> BOT -> 36 } Sat witness: Yes: ((leq([s(nn1), z])) -> BOT, { nn1 -> z }) ------------------------------------------- Step 44, which took 0.180745 s (model generation: 0.177534, model checking: 0.003211): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3798 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3799 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725, q_gen_3896}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 (q_gen_3725) -> q_gen_3896 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3811, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3811) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 (q_gen_3758, q_gen_3812) -> q_gen_3811 (q_gen_3758, q_gen_3812) -> q_gen_3811 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 34 ; () -> length([nil, z]) -> 34 ; () -> leq([z, s(nn2)]) -> 34 ; () -> leq([z, z]) -> 34 ; () -> reverse([nil, nil]) -> 34 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 41 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 49 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 38 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 34 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 34 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 34 ; (leq([s(nn1), z])) -> BOT -> 36 } Sat witness: Yes: ((length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]), { _afa -> cons(z, nil) ; _bfa -> s(z) ; _zea -> s(s(z)) ; l1 -> cons(z, cons(z, nil)) }) ------------------------------------------- Step 45, which took 0.231557 s (model generation: 0.231471, model checking: 0.000086): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3798 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3799 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725, q_gen_3896}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3896) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 (q_gen_3725) -> q_gen_3896 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3811, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3811) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 (q_gen_3758, q_gen_3812) -> q_gen_3811 (q_gen_3758, q_gen_3812) -> q_gen_3811 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 34 ; () -> length([nil, z]) -> 34 ; () -> leq([z, s(nn2)]) -> 34 ; () -> leq([z, z]) -> 34 ; () -> reverse([nil, nil]) -> 34 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 41 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 49 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 38 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 34 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 34 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 37 ; (leq([s(nn1), z])) -> BOT -> 36 } Sat witness: Yes: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), { nn1 -> s(z) ; nn2 -> z }) ------------------------------------------- Step 46, which took 0.274605 s (model generation: 0.271598, model checking: 0.003007): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3798 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3799 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725, q_gen_3896}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 (q_gen_3896) -> q_gen_3896 (q_gen_3725) -> q_gen_3896 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3811, q_gen_3812, q_gen_3813}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3747, q_gen_3813, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3747, q_gen_3813, q_gen_3745, q_gen_3811) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3758) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3811) -> q_gen_3811 (q_gen_3758, q_gen_3812) -> q_gen_3811 (q_gen_3758, q_gen_3812) -> q_gen_3811 (q_gen_3747, q_gen_3746) -> q_gen_3813 (q_gen_3758, q_gen_3812) -> q_gen_3813 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 35 ; () -> length([nil, z]) -> 35 ; () -> leq([z, s(nn2)]) -> 35 ; () -> leq([z, z]) -> 35 ; () -> reverse([nil, nil]) -> 35 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 41 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 49 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 41 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 35 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 35 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 38 ; (leq([s(nn1), z])) -> BOT -> 37 } Sat witness: Yes: ((length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]), { _afa -> cons(z, cons(z, nil)) ; _bfa -> s(s(z)) ; _zea -> s(s(s(z))) ; l1 -> cons(z, cons(z, cons(z, nil))) }) ------------------------------------------- Step 47, which took 0.344418 s (model generation: 0.339627, model checking: 0.004791): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3796, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803, q_gen_3808}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3740, q_gen_3764) -> q_gen_3808 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3796) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3796 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3808) -> q_gen_3796 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3808) -> q_gen_3796 (q_gen_3740, q_gen_3764) -> q_gen_3796 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3798 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3808) -> q_gen_3798 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3799 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3808) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725, q_gen_3896}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 (q_gen_3896) -> q_gen_3896 (q_gen_3725) -> q_gen_3896 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3810, q_gen_3812}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3810) -> q_gen_3810 (q_gen_3758, q_gen_3812) -> q_gen_3810 (q_gen_3758, q_gen_3812) -> q_gen_3810 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 36 ; () -> length([nil, z]) -> 36 ; () -> leq([z, s(nn2)]) -> 36 ; () -> leq([z, z]) -> 36 ; () -> reverse([nil, nil]) -> 36 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 44 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 49 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 42 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 36 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 36 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 39 ; (leq([s(nn1), z])) -> BOT -> 38 } Sat witness: Yes: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), { _qea -> cons(z, nil) ; _rea -> cons(z, cons(z, cons(z, nil))) ; h1 -> z ; t1 -> cons(z, nil) }) ------------------------------------------- Step 48, which took 18.997771 s (model generation: 0.679572, model checking: 18.318199): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3796, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803, q_gen_3808}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3740, q_gen_3764) -> q_gen_3808 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3796) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 () -> q_gen_3727 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3796 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3808) -> q_gen_3796 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3808) -> q_gen_3796 (q_gen_3740, q_gen_3764) -> q_gen_3796 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3798 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3808) -> q_gen_3798 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3799 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3808) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725, q_gen_3896}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 (q_gen_3896) -> q_gen_3896 (q_gen_3725) -> q_gen_3896 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3812, q_gen_3892}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3758, q_gen_3812) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3892) -> q_gen_3892 (q_gen_3758, q_gen_3812) -> q_gen_3892 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 37 ; () -> length([nil, z]) -> 37 ; () -> leq([z, s(nn2)]) -> 37 ; () -> leq([z, z]) -> 37 ; () -> reverse([nil, nil]) -> 37 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 45 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 52 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 43 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 37 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 37 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 40 ; (leq([s(nn1), z])) -> BOT -> 39 } Sat witness: Yes: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), { _lea -> cons(z, cons(z, nil)) ; h1 -> s(z) ; l2 -> cons(z, nil) ; t1 -> cons(z, nil) }) ------------------------------------------- Step 49, which took 0.628397 s (model generation: 0.625722, model checking: 0.002675): Model: |_ { append -> {{{ Q={q_gen_3727, q_gen_3732, q_gen_3733, q_gen_3734, q_gen_3735, q_gen_3740, q_gen_3764, q_gen_3797, q_gen_3798, q_gen_3799, q_gen_3800, q_gen_3801, q_gen_3802, q_gen_3803}, Q_f={q_gen_3727}, Delta= { (q_gen_3740) -> q_gen_3740 () -> q_gen_3740 (q_gen_3740, q_gen_3764) -> q_gen_3764 () -> q_gen_3764 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3732 (q_gen_3740, q_gen_3764) -> q_gen_3732 () -> q_gen_3732 (q_gen_3735, q_gen_3733) -> q_gen_3733 (q_gen_3740, q_gen_3764) -> q_gen_3733 (q_gen_3740) -> q_gen_3733 () -> q_gen_3733 (q_gen_3735, q_gen_3734) -> q_gen_3734 (q_gen_3740) -> q_gen_3734 (q_gen_3740, q_gen_3764) -> q_gen_3734 () -> q_gen_3734 (q_gen_3735) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 (q_gen_3740) -> q_gen_3735 () -> q_gen_3735 (q_gen_3803, q_gen_3802, q_gen_3801, q_gen_3800, q_gen_3799, q_gen_3798, q_gen_3797, q_gen_3727) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3727 (q_gen_3740, q_gen_3764) -> q_gen_3727 () -> q_gen_3727 (q_gen_3735, q_gen_3733) -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740, q_gen_3764) -> q_gen_3797 (q_gen_3740) -> q_gen_3797 () -> q_gen_3797 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3798 (q_gen_3735, q_gen_3734) -> q_gen_3798 (q_gen_3740, q_gen_3764) -> q_gen_3798 (q_gen_3735, q_gen_3733) -> q_gen_3799 (q_gen_3740, q_gen_3764) -> q_gen_3799 (q_gen_3735) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 (q_gen_3740) -> q_gen_3799 () -> q_gen_3799 (q_gen_3735, q_gen_3734) -> q_gen_3800 (q_gen_3735, q_gen_3734, q_gen_3733, q_gen_3732) -> q_gen_3800 (q_gen_3740, q_gen_3764) -> q_gen_3800 (q_gen_3735) -> q_gen_3801 (q_gen_3740, q_gen_3764) -> q_gen_3801 () -> q_gen_3801 (q_gen_3803, q_gen_3802) -> q_gen_3802 (q_gen_3735) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3735, q_gen_3734) -> q_gen_3802 (q_gen_3740) -> q_gen_3802 (q_gen_3740, q_gen_3764) -> q_gen_3802 () -> q_gen_3802 (q_gen_3803) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3735) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 (q_gen_3740) -> q_gen_3803 () -> q_gen_3803 } Datatype: Convolution form: complete }}} ; length -> {{{ Q={q_gen_3726, q_gen_3730, q_gen_3750}, Q_f={q_gen_3726}, Delta= { (q_gen_3750) -> q_gen_3750 () -> q_gen_3750 (q_gen_3730, q_gen_3726) -> q_gen_3726 () -> q_gen_3726 (q_gen_3730) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 (q_gen_3750) -> q_gen_3730 () -> q_gen_3730 } Datatype: Convolution form: complete }}} ; leq -> {{{ Q={q_gen_3723, q_gen_3725, q_gen_3896, q_gen_3897}, Q_f={q_gen_3723}, Delta= { (q_gen_3725) -> q_gen_3725 () -> q_gen_3725 (q_gen_3723) -> q_gen_3723 (q_gen_3897) -> q_gen_3723 (q_gen_3725) -> q_gen_3723 () -> q_gen_3723 (q_gen_3725) -> q_gen_3896 (q_gen_3896) -> q_gen_3897 } Datatype: Convolution form: complete }}} ; reverse -> {{{ Q={q_gen_3722, q_gen_3745, q_gen_3746, q_gen_3747, q_gen_3758, q_gen_3811, q_gen_3812, q_gen_3894}, Q_f={q_gen_3722}, Delta= { (q_gen_3758) -> q_gen_3758 () -> q_gen_3758 (q_gen_3758, q_gen_3812) -> q_gen_3812 () -> q_gen_3812 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3722) -> q_gen_3722 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3811) -> q_gen_3722 () -> q_gen_3722 (q_gen_3747, q_gen_3745) -> q_gen_3745 (q_gen_3758, q_gen_3812) -> q_gen_3745 (q_gen_3758) -> q_gen_3745 () -> q_gen_3745 (q_gen_3747, q_gen_3746) -> q_gen_3746 (q_gen_3758) -> q_gen_3746 (q_gen_3758, q_gen_3812) -> q_gen_3746 () -> q_gen_3746 (q_gen_3747) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 (q_gen_3758) -> q_gen_3747 () -> q_gen_3747 (q_gen_3747, q_gen_3746, q_gen_3745, q_gen_3894) -> q_gen_3811 (q_gen_3758, q_gen_3812) -> q_gen_3811 (q_gen_3758, q_gen_3812) -> q_gen_3894 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 38 ; () -> length([nil, z]) -> 38 ; () -> leq([z, s(nn2)]) -> 38 ; () -> leq([z, z]) -> 38 ; () -> reverse([nil, nil]) -> 38 ; (append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 45 ; (append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 52 ; (length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 43 ; (length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 38 ; (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 38 ; (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 43 ; (leq([s(nn1), z])) -> BOT -> 40 } Sat witness: Yes: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), { nn1 -> s(s(z)) ; nn2 -> s(z) }) Total time: 30.000092 Reason for stopping: DontKnow. Stopped because: timeout