Inference procedure has parameters: Ice fuel: 200 Timeout: 60s Convolution: left Learning problem is: env: { elt -> {a, b} ; eltlist -> {cons, nil} ; nat -> {s, z} } definition: { (drop, F: {() -> drop([s(u), nil, nil]) () -> drop([z, l, l]) (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca])} (drop([_oca, _pca, _qca]) /\ drop([_oca, _pca, _rca])) -> eq_eltlist([_qca, _rca]) ) } properties: {(drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca])} over-approximation: {drop} under-approximation: {} Clause system for inference is: { () -> drop([s(u), nil, nil]) -> 0 () -> drop([z, l, l]) -> 0 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 0 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 0 } Solving took 912.478062 seconds. DontKnow. Stopped because: timeout Working model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7750, q_gen_7751, q_gen_7752, q_gen_7753, q_gen_7754, q_gen_7755, q_gen_7756, q_gen_7757, q_gen_7758, q_gen_7759, q_gen_7760, q_gen_7761, q_gen_7762, q_gen_7763, q_gen_7764, q_gen_7765, q_gen_7766, q_gen_7767, q_gen_7768, q_gen_7769, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7774, q_gen_7775, q_gen_7776, q_gen_7777, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7781, q_gen_7782, q_gen_7783, q_gen_7784, q_gen_7785, q_gen_7786, q_gen_7787, q_gen_7788, q_gen_7789, q_gen_7790, q_gen_7791, q_gen_7792, q_gen_7793, q_gen_7794, q_gen_7795, q_gen_7796, q_gen_7797, q_gen_7798, q_gen_7799, q_gen_7800, q_gen_7801, q_gen_7802, q_gen_7803, q_gen_7804, q_gen_7805, q_gen_7806, q_gen_7807, q_gen_7808, q_gen_7809, q_gen_7810, q_gen_7811, q_gen_7812, q_gen_7813, q_gen_7814, q_gen_7815, q_gen_7816, q_gen_7817, q_gen_7818, q_gen_7819, q_gen_7820, q_gen_7821, q_gen_7822, q_gen_7823, q_gen_7824, q_gen_7825, q_gen_7826, q_gen_7827, q_gen_7828, q_gen_7829, q_gen_7830, q_gen_7831, q_gen_7832, q_gen_7833, q_gen_7834, q_gen_7835, q_gen_7836, q_gen_7837, q_gen_7838, q_gen_7839, q_gen_7840, q_gen_7841, q_gen_7842, q_gen_7843, q_gen_7844, q_gen_7845, q_gen_7846, q_gen_7847, q_gen_7848, q_gen_7849, q_gen_7850, q_gen_7851, q_gen_7852, q_gen_7853, q_gen_7854, q_gen_7855, q_gen_7856, q_gen_7857, q_gen_7858, q_gen_7859, q_gen_7860, q_gen_7861, q_gen_7862, q_gen_7863, q_gen_7864, q_gen_7865, q_gen_7866, q_gen_7867, q_gen_7868, q_gen_7869, q_gen_7870, q_gen_7871, q_gen_7872, q_gen_7873, q_gen_7874, q_gen_7875, q_gen_7876, q_gen_7877}, Q_f={}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7759) -> q_gen_7805 (q_gen_7771, q_gen_7790) -> q_gen_7833 (q_gen_7771, q_gen_7833) -> q_gen_7851 (q_gen_7805) -> q_gen_7876 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7761 (q_gen_7764, q_gen_7756) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7768 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7757, q_gen_7775) -> q_gen_7795 (q_gen_7764, q_gen_7778) -> q_gen_7799 (q_gen_7759) -> q_gen_7809 (q_gen_7757, q_gen_7778) -> q_gen_7812 (q_gen_7757, q_gen_7789) -> q_gen_7814 (q_gen_7759) -> q_gen_7818 (q_gen_7757, q_gen_7763) -> q_gen_7821 (q_gen_7764, q_gen_7763) -> q_gen_7823 (q_gen_7779, q_gen_7833) -> q_gen_7832 (q_gen_7764, q_gen_7821) -> q_gen_7837 (q_gen_7764, q_gen_7799) -> q_gen_7842 (q_gen_7779, q_gen_7790) -> q_gen_7844 (q_gen_7757, q_gen_7795) -> q_gen_7846 (q_gen_7805) -> q_gen_7848 (q_gen_7771, q_gen_7851) -> q_gen_7850 (q_gen_7757, q_gen_7821) -> q_gen_7854 (q_gen_7771, q_gen_7833) -> q_gen_7857 (q_gen_7764, q_gen_7832) -> q_gen_7860 (q_gen_7805) -> q_gen_7869 (q_gen_7764, q_gen_7812) -> q_gen_7873 () -> q_gen_7749 (q_gen_7751) -> q_gen_7750 (q_gen_7754, q_gen_7753) -> q_gen_7752 (q_gen_7757, q_gen_7756) -> q_gen_7755 (q_gen_7759) -> q_gen_7758 (q_gen_7761, q_gen_7753) -> q_gen_7760 (q_gen_7764, q_gen_7763) -> q_gen_7762 (q_gen_7766, q_gen_7753) -> q_gen_7765 (q_gen_7768, q_gen_7753) -> q_gen_7767 (q_gen_7772, q_gen_7770) -> q_gen_7769 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7774 (q_gen_7764, q_gen_7756) -> q_gen_7776 (q_gen_7780, q_gen_7778) -> q_gen_7777 () -> q_gen_7780 (q_gen_7772, q_gen_7778) -> q_gen_7781 (q_gen_7780, q_gen_7756) -> q_gen_7782 (q_gen_7784, q_gen_7778) -> q_gen_7783 () -> q_gen_7784 (q_gen_7786, q_gen_7770) -> q_gen_7785 () -> q_gen_7786 (q_gen_7786, q_gen_7778) -> q_gen_7787 (q_gen_7791, q_gen_7789) -> q_gen_7788 (q_gen_7751) -> q_gen_7791 (q_gen_7754, q_gen_7790) -> q_gen_7792 (q_gen_7766, q_gen_7790) -> q_gen_7793 (q_gen_7757, q_gen_7795) -> q_gen_7794 (q_gen_7761, q_gen_7790) -> q_gen_7796 (q_gen_7784, q_gen_7763) -> q_gen_7797 (q_gen_7791, q_gen_7799) -> q_gen_7798 (q_gen_7791, q_gen_7770) -> q_gen_7800 (q_gen_7780, q_gen_7799) -> q_gen_7801 (q_gen_7803, q_gen_7789) -> q_gen_7802 (q_gen_7759) -> q_gen_7803 (q_gen_7805) -> q_gen_7804 (q_gen_7757, q_gen_7778) -> q_gen_7806 (q_gen_7786, q_gen_7789) -> q_gen_7807 (q_gen_7809, q_gen_7753) -> q_gen_7808 (q_gen_7791, q_gen_7756) -> q_gen_7810 (q_gen_7780, q_gen_7812) -> q_gen_7811 (q_gen_7791, q_gen_7814) -> q_gen_7813 (q_gen_7757, q_gen_7775) -> q_gen_7815 (q_gen_7803, q_gen_7770) -> q_gen_7816 (q_gen_7818, q_gen_7753) -> q_gen_7817 (q_gen_7803, q_gen_7812) -> q_gen_7819 (q_gen_7757, q_gen_7821) -> q_gen_7820 (q_gen_7757, q_gen_7823) -> q_gen_7822 (q_gen_7764, q_gen_7775) -> q_gen_7824 (q_gen_7818, q_gen_7790) -> q_gen_7825 (q_gen_7786, q_gen_7823) -> q_gen_7826 (q_gen_7764, q_gen_7778) -> q_gen_7827 (q_gen_7757, q_gen_7763) -> q_gen_7828 (q_gen_7809, q_gen_7790) -> q_gen_7829 (q_gen_7791, q_gen_7778) -> q_gen_7830 (q_gen_7834, q_gen_7832) -> q_gen_7831 (q_gen_7759) -> q_gen_7834 (q_gen_7754, q_gen_7833) -> q_gen_7835 (q_gen_7757, q_gen_7837) -> q_gen_7836 (q_gen_7834, q_gen_7778) -> q_gen_7838 (q_gen_7840, q_gen_7789) -> q_gen_7839 (q_gen_7805) -> q_gen_7840 (q_gen_7803, q_gen_7842) -> q_gen_7841 (q_gen_7791, q_gen_7844) -> q_gen_7843 (q_gen_7757, q_gen_7846) -> q_gen_7845 (q_gen_7848, q_gen_7833) -> q_gen_7847 (q_gen_7852, q_gen_7850) -> q_gen_7849 (q_gen_7805) -> q_gen_7852 (q_gen_7834, q_gen_7854) -> q_gen_7853 (q_gen_7757, q_gen_7789) -> q_gen_7855 (q_gen_7786, q_gen_7857) -> q_gen_7856 (q_gen_7764, q_gen_7821) -> q_gen_7858 (q_gen_7861, q_gen_7860) -> q_gen_7859 (q_gen_7751) -> q_gen_7861 (q_gen_7786, q_gen_7832) -> q_gen_7862 (q_gen_7784, q_gen_7844) -> q_gen_7863 (q_gen_7772, q_gen_7763) -> q_gen_7864 (q_gen_7861, q_gen_7789) -> q_gen_7865 (q_gen_7818, q_gen_7851) -> q_gen_7866 (q_gen_7818, q_gen_7833) -> q_gen_7867 (q_gen_7869, q_gen_7851) -> q_gen_7868 (q_gen_7852, q_gen_7778) -> q_gen_7870 (q_gen_7764, q_gen_7795) -> q_gen_7871 (q_gen_7803, q_gen_7873) -> q_gen_7872 (q_gen_7768, q_gen_7833) -> q_gen_7874 (q_gen_7876) -> q_gen_7875 (q_gen_7869, q_gen_7833) -> q_gen_7877 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.007922 s (model generation: 0.007417, model checking: 0.000505): Model: |_ { drop -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 0 () -> drop([z, l, l]) -> 3 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 1 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 1 } Sat witness: Found: (() -> drop([z, l, l]), { l -> nil }) ------------------------------------------- Step 1, which took 0.007534 s (model generation: 0.007357, model checking: 0.000177): Model: |_ { drop -> {{{ Q={q_gen_7749}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7749 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 3 () -> drop([z, l, l]) -> 3 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 1 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 1 } Sat witness: Found: (() -> drop([s(u), nil, nil]), { u -> z }) ------------------------------------------- Step 2, which took 0.007966 s (model generation: 0.007751, model checking: 0.000215): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 (q_gen_7751) -> q_gen_7749 () -> q_gen_7749 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 3 () -> drop([z, l, l]) -> 3 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 1 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 4 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> nil ; u -> z ; x2 -> b ; x3 -> nil }) ------------------------------------------- Step 3, which took 0.013508 s (model generation: 0.012041, model checking: 0.001467): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7754 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 () -> q_gen_7749 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 3 () -> drop([z, l, l]) -> 6 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 2 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 4 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(b, nil) }) ------------------------------------------- Step 4, which took 0.016480 s (model generation: 0.010091, model checking: 0.006389): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 6 () -> drop([z, l, l]) -> 6 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 3 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 4 } Sat witness: Found: (() -> drop([s(u), nil, nil]), { u -> s(z) }) ------------------------------------------- Step 5, which took 0.009172 s (model generation: 0.008148, model checking: 0.001024): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 6 () -> drop([z, l, l]) -> 6 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 4 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 7 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> nil ; u -> z ; x2 -> a ; x3 -> nil }) ------------------------------------------- Step 6, which took 0.009037 s (model generation: 0.008636, model checking: 0.000401): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 6 () -> drop([z, l, l]) -> 9 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 5 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 7 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 7, which took 0.015519 s (model generation: 0.013422, model checking: 0.002097): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 7 () -> drop([z, l, l]) -> 9 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 6 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 10 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> nil ; u -> s(z) ; x2 -> b ; x3 -> nil }) ------------------------------------------- Step 8, which took 0.013055 s (model generation: 0.011505, model checking: 0.001550): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 8 () -> drop([z, l, l]) -> 10 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 7 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 13 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> nil ; u -> s(z) ; x2 -> a ; x3 -> nil }) ------------------------------------------- Step 9, which took 0.012822 s (model generation: 0.011098, model checking: 0.001724): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7754 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 9 () -> drop([z, l, l]) -> 11 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 8 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 16 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> cons(b, nil) ; u -> z ; x2 -> b ; x3 -> cons(b, nil) }) ------------------------------------------- Step 10, which took 0.011572 s (model generation: 0.011164, model checking: 0.000408): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7771, q_gen_7772}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 (q_gen_7751) -> q_gen_7754 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 (q_gen_7771, q_gen_7753) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7772, q_gen_7756) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 9 () -> drop([z, l, l]) -> 11 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 11 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 16 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(b, nil) ; _tca -> nil ; l1 -> nil ; n -> z ; x -> b }) ------------------------------------------- Step 11, which took 0.020116 s (model generation: 0.017499, model checking: 0.002617): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7763, q_gen_7771, q_gen_7772, q_gen_7773}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 (q_gen_7751) -> q_gen_7754 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 10 () -> drop([z, l, l]) -> 11 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 14 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 16 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(b, cons(b, nil)) ; _tca -> cons(b, nil) ; l1 -> cons(b, nil) ; n -> z ; x -> b }) ------------------------------------------- Step 12, which took 0.015133 s (model generation: 0.012644, model checking: 0.002489): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 (q_gen_7751) -> q_gen_7754 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 11 () -> drop([z, l, l]) -> 12 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 15 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 19 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> cons(a, nil) ; u -> z ; x2 -> b ; x3 -> cons(a, nil) }) ------------------------------------------- Step 13, which took 0.015565 s (model generation: 0.013969, model checking: 0.001596): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7771 (q_gen_7751) -> q_gen_7754 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 12 () -> drop([z, l, l]) -> 13 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 18 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 19 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(b, nil) ; _tca -> cons(a, nil) ; l1 -> cons(a, nil) ; n -> z ; x -> b }) ------------------------------------------- Step 14, which took 0.015847 s (model generation: 0.014904, model checking: 0.000943): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7763, q_gen_7764, q_gen_7771, q_gen_7772, q_gen_7773}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7771 (q_gen_7751) -> q_gen_7754 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 () -> q_gen_7764 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7764, q_gen_7756) -> q_gen_7773 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 13 () -> drop([z, l, l]) -> 16 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 18 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 19 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(a, nil) }) ------------------------------------------- Step 15, which took 0.016354 s (model generation: 0.014384, model checking: 0.001970): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7779, q_gen_7780}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7751) -> q_gen_7754 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 (q_gen_7779, q_gen_7753) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7756) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 14 () -> drop([z, l, l]) -> 17 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 21 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 19 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(a, nil) ; _tca -> nil ; l1 -> nil ; n -> z ; x -> b }) ------------------------------------------- Step 16, which took 0.017758 s (model generation: 0.015748, model checking: 0.002010): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7751) -> q_gen_7754 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 15 () -> drop([z, l, l]) -> 18 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 21 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 22 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> cons(a, nil) ; u -> z ; x2 -> a ; x3 -> cons(a, nil) }) ------------------------------------------- Step 17, which took 0.021155 s (model generation: 0.016330, model checking: 0.004825): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7751) -> q_gen_7754 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 () -> q_gen_7780 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 16 () -> drop([z, l, l]) -> 19 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 22 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 25 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> cons(b, nil) ; u -> z ; x2 -> a ; x3 -> cons(b, nil) }) ------------------------------------------- Step 18, which took 0.023007 s (model generation: 0.017775, model checking: 0.005232): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7751) -> q_gen_7754 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 () -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 17 () -> drop([z, l, l]) -> 20 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 25 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 25 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(b, nil) ; _tca -> cons(a, nil) ; l1 -> cons(a, nil) ; n -> z ; x -> a }) ------------------------------------------- Step 19, which took 0.022307 s (model generation: 0.019310, model checking: 0.002997): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7751) -> q_gen_7754 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 () -> q_gen_7780 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 18 () -> drop([z, l, l]) -> 21 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 25 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 28 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> cons(a, nil) ; u -> s(z) ; x2 -> a ; x3 -> cons(b, cons(a, nil)) }) ------------------------------------------- Step 20, which took 0.023068 s (model generation: 0.020730, model checking: 0.002338): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 (q_gen_7779, q_gen_7753) -> q_gen_7753 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7751) -> q_gen_7754 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 (q_gen_7751) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 () -> q_gen_7780 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 19 () -> drop([z, l, l]) -> 22 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 28 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 28 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> nil ; _tca -> cons(a, nil) ; l1 -> cons(a, nil) ; n -> z ; x -> b }) ------------------------------------------- Step 21, which took 0.024989 s (model generation: 0.022887, model checking: 0.002102): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7751) -> q_gen_7754 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7790) -> q_gen_7770 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 (q_gen_7751) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 () -> q_gen_7780 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 20 () -> drop([z, l, l]) -> 23 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 28 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 31 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> nil ; u -> s(z) ; x2 -> b ; x3 -> cons(a, nil) }) ------------------------------------------- Step 22, which took 0.024046 s (model generation: 0.022739, model checking: 0.001307): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7761, q_gen_7763, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7779, q_gen_7780, q_gen_7790}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7751) -> q_gen_7761 (q_gen_7751) -> q_gen_7761 () -> q_gen_7761 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7779, q_gen_7753) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7790) -> q_gen_7770 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7761, q_gen_7753) -> q_gen_7749 (q_gen_7761, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 (q_gen_7751) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 () -> q_gen_7780 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 21 () -> drop([z, l, l]) -> 26 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 28 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 31 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(b, cons(b, cons(b, nil))) }) ------------------------------------------- Step 23, which took 0.028111 s (model generation: 0.024952, model checking: 0.003159): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7761, q_gen_7763, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7779, q_gen_7780, q_gen_7790}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 (q_gen_7757, q_gen_7763) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7751) -> q_gen_7761 (q_gen_7751) -> q_gen_7761 () -> q_gen_7761 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7779, q_gen_7753) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7790) -> q_gen_7770 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7761, q_gen_7753) -> q_gen_7749 (q_gen_7761, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 (q_gen_7751) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 () -> q_gen_7780 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 22 () -> drop([z, l, l]) -> 27 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 31 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 31 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> nil ; _tca -> cons(a, nil) ; l1 -> cons(a, nil) ; n -> z ; x -> a }) ------------------------------------------- Step 24, which took 0.028752 s (model generation: 0.025712, model checking: 0.003040): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7763, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7779, q_gen_7780, q_gen_7790}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7763) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7779, q_gen_7753) -> q_gen_7763 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7790) -> q_gen_7770 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 (q_gen_7751) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 () -> q_gen_7780 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 23 () -> drop([z, l, l]) -> 28 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 31 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 34 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> cons(a, cons(a, nil)) ; u -> s(z) ; x2 -> a ; x3 -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 25, which took 0.036569 s (model generation: 0.031913, model checking: 0.004656): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7763, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7779, q_gen_7780, q_gen_7790}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7757, q_gen_7763) -> q_gen_7763 (q_gen_7779, q_gen_7753) -> q_gen_7763 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7790) -> q_gen_7770 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7763) -> q_gen_7749 (q_gen_7780, q_gen_7770) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7751) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 24 () -> drop([z, l, l]) -> 29 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 34 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 34 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(a, nil) ; _tca -> nil ; l1 -> cons(b, nil) ; n -> s(z) ; x -> a }) ------------------------------------------- Step 26, which took 0.036602 s (model generation: 0.033601, model checking: 0.003001): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 (q_gen_7757, q_gen_7778) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7790) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7751) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 25 () -> drop([z, l, l]) -> 30 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 34 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 37 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> cons(a, cons(a, nil)) ; u -> z ; x2 -> b ; x3 -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 27, which took 0.039822 s (model generation: 0.035825, model checking: 0.003997): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7763, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7779, q_gen_7780, q_gen_7790}, Q_f={q_gen_7749}, Delta= { (q_gen_7751) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7757, q_gen_7763) -> q_gen_7763 (q_gen_7771, q_gen_7790) -> q_gen_7763 (q_gen_7779, q_gen_7753) -> q_gen_7763 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7751) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 26 () -> drop([z, l, l]) -> 31 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 37 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 37 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(a, nil) ; _tca -> nil ; l1 -> cons(b, cons(a, nil)) ; n -> s(s(z)) ; x -> a }) ------------------------------------------- Step 28, which took 0.038188 s (model generation: 0.037306, model checking: 0.000882): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7779, q_gen_7780, q_gen_7790}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7757, q_gen_7763) -> q_gen_7763 (q_gen_7771, q_gen_7790) -> q_gen_7763 (q_gen_7779, q_gen_7753) -> q_gen_7763 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7751) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 29 () -> drop([z, l, l]) -> 31 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 37 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 37 } Sat witness: Found: (() -> drop([s(u), nil, nil]), { u -> s(s(z)) }) ------------------------------------------- Step 29, which took 0.042740 s (model generation: 0.040163, model checking: 0.002577): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7779, q_gen_7780, q_gen_7790}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7757, q_gen_7763) -> q_gen_7763 (q_gen_7771, q_gen_7790) -> q_gen_7763 (q_gen_7779, q_gen_7753) -> q_gen_7763 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7751) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 30 () -> drop([z, l, l]) -> 32 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 37 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 40 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> cons(b, nil) ; u -> z ; x2 -> a ; x3 -> cons(b, cons(a, nil)) }) ------------------------------------------- Step 30, which took 0.049435 s (model generation: 0.045194, model checking: 0.004241): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7757, q_gen_7778) -> q_gen_7778 (q_gen_7771, q_gen_7790) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7751) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 31 () -> drop([z, l, l]) -> 33 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 40 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 40 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(a, cons(a, nil)) ; _tca -> cons(a, nil) ; l1 -> cons(a, cons(a, nil)) ; n -> s(z) ; x -> a }) ------------------------------------------- Step 31, which took 0.053320 s (model generation: 0.047282, model checking: 0.006038): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 (q_gen_7771, q_gen_7790) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7757, q_gen_7778) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7756) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 32 () -> drop([z, l, l]) -> 34 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 40 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 43 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> nil ; u -> s(s(z)) ; x2 -> a ; x3 -> nil }) ------------------------------------------- Step 32, which took 0.052353 s (model generation: 0.046992, model checking: 0.005361): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 (q_gen_7771, q_gen_7790) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7757, q_gen_7778) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7756) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 33 () -> drop([z, l, l]) -> 35 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 43 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 43 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(a, nil) ; _tca -> nil ; l1 -> nil ; n -> s(z) ; x -> a }) ------------------------------------------- Step 33, which took 0.054729 s (model generation: 0.050028, model checking: 0.004701): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7784, q_gen_7790}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7757, q_gen_7778) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7790) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7784, q_gen_7778) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7784, q_gen_7756) -> q_gen_7773 (q_gen_7784, q_gen_7770) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 () -> q_gen_7780 (q_gen_7751) -> q_gen_7784 () -> q_gen_7784 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 34 () -> drop([z, l, l]) -> 36 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 43 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 46 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> cons(a, cons(b, nil)) ; u -> s(z) ; x2 -> a ; x3 -> cons(b, cons(b, cons(a, nil))) }) ------------------------------------------- Step 34, which took 0.062634 s (model generation: 0.061123, model checking: 0.001511): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7775) -> q_gen_7756 (q_gen_7764, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7764, q_gen_7775) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7771, q_gen_7790) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7775) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7775) -> q_gen_7773 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 35 () -> drop([z, l, l]) -> 39 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 43 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 46 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(b, cons(b, nil)) }) ------------------------------------------- Step 35, which took 0.076157 s (model generation: 0.068454, model checking: 0.007703): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 (q_gen_7757, q_gen_7778) -> q_gen_7756 (q_gen_7764, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7764, q_gen_7778) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7790) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7778) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 36 () -> drop([z, l, l]) -> 40 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 46 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 46 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(a, nil) ; _tca -> nil ; l1 -> cons(b, nil) ; n -> s(s(z)) ; x -> a }) ------------------------------------------- Step 36, which took 0.074255 s (model generation: 0.065138, model checking: 0.009117): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7757, q_gen_7763) -> q_gen_7763 (q_gen_7771, q_gen_7790) -> q_gen_7763 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7757, q_gen_7778) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 37 () -> drop([z, l, l]) -> 41 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 46 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 49 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> nil ; u -> s(s(z)) ; x2 -> b ; x3 -> nil }) ------------------------------------------- Step 37, which took 0.075712 s (model generation: 0.069237, model checking: 0.006475): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7759) -> q_gen_7754 (q_gen_7759) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7757, q_gen_7778) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7757, q_gen_7789) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7772, q_gen_7789) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 38 () -> drop([z, l, l]) -> 42 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 49 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 49 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(a, cons(b, nil)) ; _tca -> nil ; l1 -> cons(b, cons(a, nil)) ; n -> s(s(z)) ; x -> a }) ------------------------------------------- Step 38, which took 0.082917 s (model generation: 0.081177, model checking: 0.001740): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7759) -> q_gen_7754 (q_gen_7759) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7789) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7757, q_gen_7775) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7757, q_gen_7789) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 39 () -> drop([z, l, l]) -> 45 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 49 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 49 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(b, cons(b, cons(a, nil))) }) ------------------------------------------- Step 39, which took 0.089148 s (model generation: 0.086939, model checking: 0.002209): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7759) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7757, q_gen_7763) -> q_gen_7789 (q_gen_7757, q_gen_7775) -> q_gen_7789 (q_gen_7757, q_gen_7789) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7757, q_gen_7789) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 40 () -> drop([z, l, l]) -> 48 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 49 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 49 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(b, cons(a, cons(a, nil))) }) ------------------------------------------- Step 40, which took 0.090976 s (model generation: 0.089592, model checking: 0.001384): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7759) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7757, q_gen_7775) -> q_gen_7763 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7764, q_gen_7763) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7757, q_gen_7763) -> q_gen_7789 (q_gen_7757, q_gen_7789) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7757, q_gen_7789) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 41 () -> drop([z, l, l]) -> 51 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 49 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 49 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(a, cons(b, nil)) }) ------------------------------------------- Step 41, which took 0.099221 s (model generation: 0.086093, model checking: 0.013128): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7759) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7764, q_gen_7763) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7757, q_gen_7763) -> q_gen_7789 (q_gen_7757, q_gen_7775) -> q_gen_7789 (q_gen_7757, q_gen_7789) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7757, q_gen_7789) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 (q_gen_7764, q_gen_7775) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 42 () -> drop([z, l, l]) -> 51 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 49 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 52 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> nil ; u -> s(s(z)) ; x2 -> b ; x3 -> cons(a, nil) }) ------------------------------------------- Step 42, which took 0.100405 s (model generation: 0.089269, model checking: 0.011136): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7759) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7764, q_gen_7763) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7757, q_gen_7763) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7757, q_gen_7775) -> q_gen_7789 (q_gen_7757, q_gen_7789) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7757, q_gen_7789) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 (q_gen_7764, q_gen_7775) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 43 () -> drop([z, l, l]) -> 51 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 52 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 52 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(b, cons(a, cons(a, nil))) ; _tca -> cons(a, nil) ; l1 -> cons(a, cons(a, nil)) ; n -> z ; x -> a }) ------------------------------------------- Step 43, which took 0.100229 s (model generation: 0.098874, model checking: 0.001355): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7789) -> q_gen_7756 (q_gen_7764, q_gen_7763) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7757, q_gen_7763) -> q_gen_7789 (q_gen_7757, q_gen_7775) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7757, q_gen_7789) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 (q_gen_7764, q_gen_7775) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 44 () -> drop([z, l, l]) -> 54 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 52 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 52 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(b, cons(a, nil)) }) ------------------------------------------- Step 44, which took 0.113414 s (model generation: 0.107927, model checking: 0.005487): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7784, q_gen_7790, q_gen_7803}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7759) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 (q_gen_7757, q_gen_7778) -> q_gen_7756 (q_gen_7764, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7764, q_gen_7778) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7790) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7784, q_gen_7778) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7784, q_gen_7756) -> q_gen_7773 (q_gen_7784, q_gen_7770) -> q_gen_7773 (q_gen_7803, q_gen_7756) -> q_gen_7773 (q_gen_7803, q_gen_7770) -> q_gen_7773 (q_gen_7803, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7764, q_gen_7778) -> q_gen_7773 () -> q_gen_7780 (q_gen_7751) -> q_gen_7784 () -> q_gen_7784 (q_gen_7759) -> q_gen_7803 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 45 () -> drop([z, l, l]) -> 54 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 52 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 55 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> nil ; u -> s(s(z)) ; x2 -> a ; x3 -> cons(a, nil) }) ------------------------------------------- Step 45, which took 0.113046 s (model generation: 0.106576, model checking: 0.006470): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7784, q_gen_7790, q_gen_7803}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 (q_gen_7757, q_gen_7778) -> q_gen_7756 (q_gen_7764, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7764, q_gen_7778) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7790) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7784, q_gen_7778) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7784, q_gen_7756) -> q_gen_7773 (q_gen_7784, q_gen_7770) -> q_gen_7773 (q_gen_7803, q_gen_7756) -> q_gen_7773 (q_gen_7803, q_gen_7770) -> q_gen_7773 (q_gen_7803, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7764, q_gen_7778) -> q_gen_7773 () -> q_gen_7780 (q_gen_7751) -> q_gen_7784 () -> q_gen_7784 (q_gen_7759) -> q_gen_7803 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 46 () -> drop([z, l, l]) -> 54 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 55 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 55 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(a, nil) ; _tca -> nil ; l1 -> cons(a, nil) ; n -> s(z) ; x -> a }) ------------------------------------------- Step 46, which took 0.126140 s (model generation: 0.111331, model checking: 0.014809): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7775) -> q_gen_7756 (q_gen_7764, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7757, q_gen_7789) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7775) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 47 () -> drop([z, l, l]) -> 55 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 55 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 58 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> cons(a, nil) ; u -> s(s(z)) ; x2 -> b ; x3 -> cons(a, cons(b, cons(a, nil))) }) ------------------------------------------- Step 47, which took 0.127835 s (model generation: 0.120764, model checking: 0.007071): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 (q_gen_7771, q_gen_7790) -> q_gen_7753 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7789) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7757, q_gen_7763) -> q_gen_7775 (q_gen_7764, q_gen_7763) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7757, q_gen_7775) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7757, q_gen_7789) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 (q_gen_7764, q_gen_7775) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 48 () -> drop([z, l, l]) -> 55 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 58 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 58 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> nil ; _tca -> cons(b, cons(a, nil)) ; l1 -> cons(b, cons(a, nil)) ; n -> z ; x -> b }) ------------------------------------------- Step 48, which took 0.126737 s (model generation: 0.124655, model checking: 0.002082): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7771, q_gen_7790) -> q_gen_7790 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7775) -> q_gen_7756 (q_gen_7764, q_gen_7763) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7779, q_gen_7790) -> q_gen_7775 (q_gen_7757, q_gen_7763) -> q_gen_7789 (q_gen_7757, q_gen_7789) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7757, q_gen_7789) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 (q_gen_7764, q_gen_7775) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 49 () -> drop([z, l, l]) -> 58 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 58 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 58 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(b, cons(a, cons(b, cons(a, nil)))) }) ------------------------------------------- Step 49, which took 0.141915 s (model generation: 0.131344, model checking: 0.010571): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7771, q_gen_7790) -> q_gen_7790 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7775) -> q_gen_7756 (q_gen_7764, q_gen_7763) -> q_gen_7756 (q_gen_7764, q_gen_7789) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7779, q_gen_7790) -> q_gen_7775 (q_gen_7757, q_gen_7763) -> q_gen_7789 (q_gen_7757, q_gen_7789) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7757, q_gen_7789) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 (q_gen_7764, q_gen_7775) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 50 () -> drop([z, l, l]) -> 58 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 58 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 61 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> cons(a, nil) ; u -> s(s(s(z))) ; x2 -> b ; x3 -> cons(b, cons(a, nil)) }) ------------------------------------------- Step 50, which took 0.190400 s (model generation: 0.167528, model checking: 0.022872): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7771, q_gen_7790) -> q_gen_7790 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7778) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7764, q_gen_7770) -> q_gen_7763 (q_gen_7771, q_gen_7790) -> q_gen_7763 (q_gen_7779, q_gen_7790) -> q_gen_7763 () -> q_gen_7764 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7763) -> q_gen_7770 (q_gen_7764, q_gen_7763) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7764, q_gen_7778) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7770) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7764, q_gen_7778) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 (q_gen_7751) -> q_gen_7791 (q_gen_7759) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 51 () -> drop([z, l, l]) -> 58 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 61 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 61 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(a, cons(a, cons(a, nil))) ; _tca -> cons(a, nil) ; l1 -> cons(a, cons(a, cons(a, nil))) ; n -> s(s(z)) ; x -> a }) ------------------------------------------- Step 51, which took 0.199245 s (model generation: 0.197755, model checking: 0.001490): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7771, q_gen_7790) -> q_gen_7790 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7778) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7764, q_gen_7763) -> q_gen_7763 (q_gen_7771, q_gen_7790) -> q_gen_7763 () -> q_gen_7764 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7763) -> q_gen_7770 (q_gen_7764, q_gen_7770) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7779, q_gen_7790) -> q_gen_7770 (q_gen_7764, q_gen_7778) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7770) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7764, q_gen_7778) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 (q_gen_7751) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 52 () -> drop([z, l, l]) -> 61 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 61 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 61 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(b, cons(b, cons(b, cons(b, nil)))) }) ------------------------------------------- Step 52, which took 0.225994 s (model generation: 0.216178, model checking: 0.009816): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7771, q_gen_7790) -> q_gen_7790 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7778) -> q_gen_7756 (q_gen_7764, q_gen_7763) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7757, q_gen_7770) -> q_gen_7763 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7790) -> q_gen_7763 () -> q_gen_7764 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7763) -> q_gen_7770 (q_gen_7764, q_gen_7770) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7764, q_gen_7778) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7779, q_gen_7790) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7770) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7764, q_gen_7778) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 53 () -> drop([z, l, l]) -> 61 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 61 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 64 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> nil ; u -> s(s(s(z))) ; x2 -> a ; x3 -> cons(b, cons(a, nil)) }) ------------------------------------------- Step 53, which took 0.242930 s (model generation: 0.233019, model checking: 0.009911): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7771, q_gen_7790) -> q_gen_7790 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7778) -> q_gen_7756 (q_gen_7764, q_gen_7763) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7790) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7763) -> q_gen_7770 (q_gen_7757, q_gen_7770) -> q_gen_7770 (q_gen_7764, q_gen_7770) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7779, q_gen_7790) -> q_gen_7770 (q_gen_7764, q_gen_7778) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7770) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7764, q_gen_7778) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 (q_gen_7751) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 54 () -> drop([z, l, l]) -> 61 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 64 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 64 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(a, nil) ; _tca -> cons(a, cons(b, cons(b, cons(a, nil)))) ; l1 -> cons(b, cons(b, cons(b, cons(a, nil)))) ; n -> s(s(s(z))) ; x -> a }) ------------------------------------------- Step 54, which took 0.242883 s (model generation: 0.234966, model checking: 0.007917): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790, q_gen_7791, q_gen_7803}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7771, q_gen_7790) -> q_gen_7790 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7779, q_gen_7790) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7757, q_gen_7763) -> q_gen_7763 (q_gen_7757, q_gen_7770) -> q_gen_7763 (q_gen_7771, q_gen_7790) -> q_gen_7763 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7778) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7763) -> q_gen_7749 (q_gen_7803, q_gen_7756) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7803, q_gen_7763) -> q_gen_7773 (q_gen_7803, q_gen_7770) -> q_gen_7773 (q_gen_7803, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 (q_gen_7759) -> q_gen_7803 (q_gen_7759) -> q_gen_7803 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 55 () -> drop([z, l, l]) -> 62 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 64 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 67 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> cons(b, nil) ; u -> z ; x2 -> a ; x3 -> cons(b, cons(b, cons(a, nil))) }) ------------------------------------------- Step 55, which took 0.277004 s (model generation: 0.275526, model checking: 0.001478): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7771, q_gen_7790) -> q_gen_7790 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7757, q_gen_7775) -> q_gen_7763 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 (q_gen_7779, q_gen_7790) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7757, q_gen_7789) -> q_gen_7775 (q_gen_7764, q_gen_7763) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7757, q_gen_7763) -> q_gen_7789 (q_gen_7764, q_gen_7789) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7757, q_gen_7789) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 (q_gen_7764, q_gen_7775) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 (q_gen_7751) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 56 () -> drop([z, l, l]) -> 65 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 64 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 67 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(a, cons(b, cons(a, nil))) }) ------------------------------------------- Step 56, which took 0.298153 s (model generation: 0.282343, model checking: 0.015810): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7771, q_gen_7790) -> q_gen_7790 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7763) -> q_gen_7756 (q_gen_7757, q_gen_7789) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7757, q_gen_7775) -> q_gen_7763 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 (q_gen_7779, q_gen_7790) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7764, q_gen_7763) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 (q_gen_7764, q_gen_7775) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7789) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 (q_gen_7751) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 57 () -> drop([z, l, l]) -> 65 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 67 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 67 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(a, cons(a, nil)) ; _tca -> cons(b, nil) ; l1 -> cons(a, cons(a, cons(b, cons(a, nil)))) ; n -> s(z) ; x -> b }) ------------------------------------------- Step 57, which took 0.348889 s (model generation: 0.340739, model checking: 0.008150): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7771, q_gen_7790) -> q_gen_7790 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7763) -> q_gen_7756 (q_gen_7757, q_gen_7775) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 (q_gen_7779, q_gen_7790) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7757, q_gen_7789) -> q_gen_7775 (q_gen_7764, q_gen_7763) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 (q_gen_7764, q_gen_7775) -> q_gen_7749 () -> q_gen_7749 (q_gen_7751) -> q_gen_7772 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7789) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 58 () -> drop([z, l, l]) -> 66 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 67 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 70 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> cons(a, nil) ; u -> z ; x2 -> a ; x3 -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 58, which took 0.449966 s (model generation: 0.433639, model checking: 0.016327): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7771, q_gen_7790) -> q_gen_7790 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7775) -> q_gen_7756 (q_gen_7764, q_gen_7763) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7753) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7757, q_gen_7763) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7779, q_gen_7790) -> q_gen_7775 (q_gen_7757, q_gen_7789) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7763) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 (q_gen_7764, q_gen_7775) -> q_gen_7749 () -> q_gen_7749 (q_gen_7751) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7789) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 59 () -> drop([z, l, l]) -> 67 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 70 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 70 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(a, nil) ; _tca -> cons(b, cons(a, nil)) ; l1 -> cons(b, cons(a, nil)) ; n -> s(z) ; x -> a }) ------------------------------------------- Step 59, which took 0.496660 s (model generation: 0.491956, model checking: 0.004704): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7771, q_gen_7790) -> q_gen_7790 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 (q_gen_7764, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7779, q_gen_7790) -> q_gen_7770 (q_gen_7764, q_gen_7778) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7757, q_gen_7778) -> q_gen_7789 (q_gen_7757, q_gen_7789) -> q_gen_7789 (q_gen_7764, q_gen_7770) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7772, q_gen_7789) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7757, q_gen_7789) -> q_gen_7773 (q_gen_7764, q_gen_7778) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 (q_gen_7751) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 60 () -> drop([z, l, l]) -> 68 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 70 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 73 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> cons(a, nil) ; u -> s(z) ; x2 -> b ; x3 -> cons(b, cons(a, nil)) }) ------------------------------------------- Step 60, which took 0.406965 s (model generation: 0.401066, model checking: 0.005899): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7771, q_gen_7790) -> q_gen_7790 (q_gen_7779, q_gen_7753) -> q_gen_7790 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 (q_gen_7764, q_gen_7756) -> q_gen_7756 (q_gen_7764, q_gen_7770) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7778) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7779, q_gen_7790) -> q_gen_7770 (q_gen_7764, q_gen_7778) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7757, q_gen_7789) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7772, q_gen_7789) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7757, q_gen_7789) -> q_gen_7773 (q_gen_7764, q_gen_7778) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 61 () -> drop([z, l, l]) -> 69 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 73 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 73 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> nil ; _tca -> cons(a, nil) ; l1 -> cons(b, cons(b, cons(a, nil))) ; n -> s(s(z)) ; x -> b }) ------------------------------------------- Step 61, which took 0.452816 s (model generation: 0.443029, model checking: 0.009787): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791, q_gen_7833, q_gen_7851}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7771, q_gen_7790) -> q_gen_7833 (q_gen_7771, q_gen_7833) -> q_gen_7851 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 (q_gen_7764, q_gen_7756) -> q_gen_7756 (q_gen_7764, q_gen_7770) -> q_gen_7756 (q_gen_7771, q_gen_7851) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7789) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7833) -> q_gen_7770 (q_gen_7779, q_gen_7790) -> q_gen_7770 (q_gen_7779, q_gen_7833) -> q_gen_7770 (q_gen_7764, q_gen_7778) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7757, q_gen_7778) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7766, q_gen_7833) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7772, q_gen_7789) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7754, q_gen_7833) -> q_gen_7773 (q_gen_7766, q_gen_7851) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7757, q_gen_7789) -> q_gen_7773 (q_gen_7764, q_gen_7778) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 62 () -> drop([z, l, l]) -> 70 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 73 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 76 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> nil ; u -> s(s(s(z))) ; x2 -> b ; x3 -> cons(b, cons(b, cons(a, nil))) }) ------------------------------------------- Step 62, which took 0.455129 s (model generation: 0.449350, model checking: 0.005779): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791, q_gen_7809, q_gen_7833}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7759) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7771, q_gen_7790) -> q_gen_7833 (q_gen_7771, q_gen_7833) -> q_gen_7833 (q_gen_7751) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 (q_gen_7757, q_gen_7778) -> q_gen_7756 (q_gen_7764, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7789) -> q_gen_7770 (q_gen_7764, q_gen_7789) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7779, q_gen_7790) -> q_gen_7770 (q_gen_7764, q_gen_7778) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7771, q_gen_7833) -> q_gen_7789 (q_gen_7779, q_gen_7833) -> q_gen_7789 (q_gen_7759) -> q_gen_7809 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7809, q_gen_7753) -> q_gen_7749 (q_gen_7809, q_gen_7790) -> q_gen_7749 (q_gen_7809, q_gen_7833) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7772, q_gen_7789) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7754, q_gen_7833) -> q_gen_7773 (q_gen_7766, q_gen_7833) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7757, q_gen_7789) -> q_gen_7773 (q_gen_7764, q_gen_7778) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 (q_gen_7751) -> q_gen_7791 (q_gen_7759) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 63 () -> drop([z, l, l]) -> 71 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 76 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 76 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(a, nil) ; _tca -> nil ; l1 -> cons(a, nil) ; n -> s(s(s(z))) ; x -> a }) ------------------------------------------- Step 63, which took 0.681845 s (model generation: 0.673357, model checking: 0.008488): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790, q_gen_7791, q_gen_7809, q_gen_7833}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7771, q_gen_7790) -> q_gen_7833 (q_gen_7771, q_gen_7833) -> q_gen_7833 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7770) -> q_gen_7756 (q_gen_7764, q_gen_7770) -> q_gen_7756 (q_gen_7779, q_gen_7790) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7757, q_gen_7778) -> q_gen_7763 (q_gen_7764, q_gen_7756) -> q_gen_7763 (q_gen_7771, q_gen_7790) -> q_gen_7763 (q_gen_7779, q_gen_7833) -> q_gen_7763 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7757, q_gen_7763) -> q_gen_7770 (q_gen_7764, q_gen_7763) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7833) -> q_gen_7770 (q_gen_7764, q_gen_7778) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7759) -> q_gen_7809 (q_gen_7759) -> q_gen_7809 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7766, q_gen_7833) -> q_gen_7749 (q_gen_7809, q_gen_7753) -> q_gen_7749 (q_gen_7809, q_gen_7790) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 (q_gen_7757, q_gen_7770) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7763) -> q_gen_7749 (q_gen_7764, q_gen_7770) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7754, q_gen_7833) -> q_gen_7773 (q_gen_7809, q_gen_7833) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7764, q_gen_7778) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 (q_gen_7751) -> q_gen_7791 (q_gen_7759) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 64 () -> drop([z, l, l]) -> 72 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 76 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 79 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> nil ; u -> s(s(z)) ; x2 -> b ; x3 -> cons(b, cons(a, nil)) }) ------------------------------------------- Step 64, which took 0.528107 s (model generation: 0.525780, model checking: 0.002327): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790, q_gen_7791, q_gen_7809, q_gen_7833, q_gen_7851}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7771, q_gen_7790) -> q_gen_7833 (q_gen_7771, q_gen_7833) -> q_gen_7851 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7764, q_gen_7756) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7764 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7757, q_gen_7775) -> q_gen_7770 (q_gen_7764, q_gen_7770) -> q_gen_7770 (q_gen_7764, q_gen_7775) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7833) -> q_gen_7770 (q_gen_7771, q_gen_7851) -> q_gen_7770 (q_gen_7779, q_gen_7790) -> q_gen_7770 (q_gen_7779, q_gen_7833) -> q_gen_7770 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7757, q_gen_7770) -> q_gen_7775 (q_gen_7757, q_gen_7778) -> q_gen_7775 (q_gen_7771, q_gen_7790) -> q_gen_7775 (q_gen_7764, q_gen_7778) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7759) -> q_gen_7809 (q_gen_7759) -> q_gen_7809 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7775) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7766, q_gen_7833) -> q_gen_7749 (q_gen_7766, q_gen_7851) -> q_gen_7749 (q_gen_7809, q_gen_7753) -> q_gen_7749 (q_gen_7809, q_gen_7790) -> q_gen_7749 (q_gen_7809, q_gen_7833) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7770) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7775) -> q_gen_7749 () -> q_gen_7749 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7780, q_gen_7775) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7754, q_gen_7833) -> q_gen_7773 (q_gen_7809, q_gen_7851) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7764, q_gen_7778) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 65 () -> drop([z, l, l]) -> 75 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 76 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 79 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(a, cons(b, cons(b, nil))) }) ------------------------------------------- Step 65, which took 0.541132 s (model generation: 0.531080, model checking: 0.010052): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7766, q_gen_7768, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7784, q_gen_7789, q_gen_7790, q_gen_7791, q_gen_7833, q_gen_7851}, Q_f={q_gen_7749}, Delta= { (q_gen_7759) -> q_gen_7751 () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7771, q_gen_7790) -> q_gen_7833 (q_gen_7771, q_gen_7833) -> q_gen_7851 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7756) -> q_gen_7756 (q_gen_7771, q_gen_7833) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7759) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7751) -> q_gen_7768 (q_gen_7759) -> q_gen_7768 (q_gen_7757, q_gen_7778) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7851) -> q_gen_7770 (q_gen_7779, q_gen_7790) -> q_gen_7770 (q_gen_7779, q_gen_7833) -> q_gen_7770 (q_gen_7757, q_gen_7770) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7757, q_gen_7789) -> q_gen_7789 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7784, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7766, q_gen_7851) -> q_gen_7749 (q_gen_7768, q_gen_7753) -> q_gen_7749 (q_gen_7768, q_gen_7790) -> q_gen_7749 (q_gen_7768, q_gen_7833) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 () -> q_gen_7749 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7772, q_gen_7789) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7784, q_gen_7756) -> q_gen_7773 (q_gen_7784, q_gen_7770) -> q_gen_7773 (q_gen_7784, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7754, q_gen_7833) -> q_gen_7773 (q_gen_7768, q_gen_7851) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7757, q_gen_7789) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 (q_gen_7759) -> q_gen_7784 () -> q_gen_7784 (q_gen_7751) -> q_gen_7791 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 66 () -> drop([z, l, l]) -> 76 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 79 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 79 } Sat witness: Found: ((drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]), { _sca -> cons(a, cons(a, cons(b, nil))) ; _tca -> nil ; l1 -> cons(a, cons(b, cons(a, nil))) ; n -> s(s(z)) ; x -> a }) ------------------------------------------- Step 66, which took 0.533701 s (model generation: 0.532135, model checking: 0.001566): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7764, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7775, q_gen_7779, q_gen_7780, q_gen_7789, q_gen_7790, q_gen_7791, q_gen_7805, q_gen_7833, q_gen_7851}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7759) -> q_gen_7805 (q_gen_7771, q_gen_7790) -> q_gen_7833 (q_gen_7771, q_gen_7833) -> q_gen_7851 (q_gen_7751) -> q_gen_7754 (q_gen_7805) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7789) -> q_gen_7756 (q_gen_7764, q_gen_7756) -> q_gen_7756 (q_gen_7764, q_gen_7770) -> q_gen_7756 (q_gen_7771, q_gen_7833) -> q_gen_7756 (q_gen_7771, q_gen_7851) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7764 (q_gen_7759) -> q_gen_7766 (q_gen_7805) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7757, q_gen_7770) -> q_gen_7770 (q_gen_7757, q_gen_7775) -> q_gen_7770 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7779, q_gen_7833) -> q_gen_7770 (q_gen_7757, q_gen_7756) -> q_gen_7775 (q_gen_7764, q_gen_7775) -> q_gen_7775 (q_gen_7779, q_gen_7753) -> q_gen_7775 (q_gen_7779, q_gen_7790) -> q_gen_7775 (q_gen_7771, q_gen_7790) -> q_gen_7789 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7772, q_gen_7789) -> q_gen_7749 (q_gen_7780, q_gen_7775) -> q_gen_7749 (q_gen_7791, q_gen_7789) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7754, q_gen_7851) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7766, q_gen_7833) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7805) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7770) -> q_gen_7749 (q_gen_7757, q_gen_7775) -> q_gen_7749 (q_gen_7764, q_gen_7756) -> q_gen_7749 (q_gen_7764, q_gen_7770) -> q_gen_7749 (q_gen_7764, q_gen_7775) -> q_gen_7749 () -> q_gen_7749 (q_gen_7805) -> q_gen_7772 (q_gen_7751) -> q_gen_7772 (q_gen_7759) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7775) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7770) -> q_gen_7773 (q_gen_7780, q_gen_7789) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7775) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7754, q_gen_7833) -> q_gen_7773 (q_gen_7766, q_gen_7851) -> q_gen_7773 (q_gen_7757, q_gen_7789) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 (q_gen_7805) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 69 () -> drop([z, l, l]) -> 76 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 79 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 79 } Sat witness: Found: (() -> drop([s(u), nil, nil]), { u -> s(s(s(z))) }) ------------------------------------------- Step 67, which took 0.565292 s (model generation: 0.550503, model checking: 0.014789): Model: |_ { drop -> {{{ Q={q_gen_7749, q_gen_7751, q_gen_7753, q_gen_7754, q_gen_7756, q_gen_7757, q_gen_7759, q_gen_7763, q_gen_7766, q_gen_7770, q_gen_7771, q_gen_7772, q_gen_7773, q_gen_7778, q_gen_7779, q_gen_7780, q_gen_7790, q_gen_7791, q_gen_7803, q_gen_7805, q_gen_7833, q_gen_7851}, Q_f={q_gen_7749}, Delta= { () -> q_gen_7751 () -> q_gen_7753 (q_gen_7751) -> q_gen_7759 (q_gen_7805) -> q_gen_7759 () -> q_gen_7771 () -> q_gen_7779 (q_gen_7779, q_gen_7753) -> q_gen_7790 (q_gen_7759) -> q_gen_7805 (q_gen_7771, q_gen_7790) -> q_gen_7833 (q_gen_7771, q_gen_7833) -> q_gen_7851 (q_gen_7805) -> q_gen_7754 () -> q_gen_7754 () -> q_gen_7754 (q_gen_7757, q_gen_7770) -> q_gen_7756 (q_gen_7771, q_gen_7851) -> q_gen_7756 (q_gen_7779, q_gen_7790) -> q_gen_7756 () -> q_gen_7756 () -> q_gen_7757 () -> q_gen_7757 (q_gen_7757, q_gen_7756) -> q_gen_7763 (q_gen_7757, q_gen_7763) -> q_gen_7763 (q_gen_7771, q_gen_7790) -> q_gen_7763 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7805) -> q_gen_7766 (q_gen_7751) -> q_gen_7766 (q_gen_7759) -> q_gen_7766 (q_gen_7771, q_gen_7753) -> q_gen_7770 (q_gen_7771, q_gen_7833) -> q_gen_7770 (q_gen_7779, q_gen_7833) -> q_gen_7770 (q_gen_7757, q_gen_7778) -> q_gen_7778 (q_gen_7779, q_gen_7753) -> q_gen_7778 (q_gen_7772, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7770) -> q_gen_7749 (q_gen_7780, q_gen_7778) -> q_gen_7749 (q_gen_7791, q_gen_7763) -> q_gen_7749 (q_gen_7754, q_gen_7753) -> q_gen_7749 (q_gen_7754, q_gen_7851) -> q_gen_7749 (q_gen_7766, q_gen_7753) -> q_gen_7749 (q_gen_7766, q_gen_7790) -> q_gen_7749 (q_gen_7766, q_gen_7833) -> q_gen_7749 (q_gen_7751) -> q_gen_7749 (q_gen_7759) -> q_gen_7749 (q_gen_7805) -> q_gen_7749 (q_gen_7757, q_gen_7756) -> q_gen_7749 (q_gen_7757, q_gen_7763) -> q_gen_7749 () -> q_gen_7749 (q_gen_7805) -> q_gen_7772 () -> q_gen_7772 () -> q_gen_7772 (q_gen_7772, q_gen_7756) -> q_gen_7773 (q_gen_7772, q_gen_7763) -> q_gen_7773 (q_gen_7772, q_gen_7778) -> q_gen_7773 (q_gen_7780, q_gen_7756) -> q_gen_7773 (q_gen_7780, q_gen_7763) -> q_gen_7773 (q_gen_7791, q_gen_7756) -> q_gen_7773 (q_gen_7791, q_gen_7770) -> q_gen_7773 (q_gen_7791, q_gen_7778) -> q_gen_7773 (q_gen_7803, q_gen_7763) -> q_gen_7773 (q_gen_7803, q_gen_7770) -> q_gen_7773 (q_gen_7803, q_gen_7778) -> q_gen_7773 (q_gen_7754, q_gen_7790) -> q_gen_7773 (q_gen_7754, q_gen_7833) -> q_gen_7773 (q_gen_7766, q_gen_7851) -> q_gen_7773 (q_gen_7757, q_gen_7778) -> q_gen_7773 (q_gen_7759) -> q_gen_7780 () -> q_gen_7780 () -> q_gen_7780 (q_gen_7751) -> q_gen_7791 (q_gen_7751) -> q_gen_7791 (q_gen_7805) -> q_gen_7791 (q_gen_7759) -> q_gen_7803 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 70 () -> drop([z, l, l]) -> 77 (drop([n, l1, _tca]) /\ drop([s(n), cons(x, l1), _sca])) -> eq_eltlist([_sca, _tca]) -> 79 (drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]) -> 82 } Sat witness: Found: ((drop([u, x3, _nca])) -> drop([s(u), cons(x2, x3), _nca]), { _nca -> nil ; u -> s(s(s(z))) ; x2 -> b ; x3 -> cons(b, cons(a, nil)) }) Total time: 912.478062 Reason for stopping: DontKnow. Stopped because: timeout