Inference procedure has parameters: Ice fuel: 200 Timeout: 60s Convolution: right 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, _um])) -> drop([s(u), cons(x2, x3), _um])} (drop([_vm, _wm, _xm]) /\ drop([_vm, _wm, _ym])) -> eq_eltlist([_xm, _ym]) ) } properties: {(drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an])} over-approximation: {drop} under-approximation: {} Clause system for inference is: { () -> drop([s(u), nil, nil]) -> 0 () -> drop([z, l, l]) -> 0 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 0 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 0 } Solving took 65.278225 seconds. DontKnow. Stopped because: timeout Working model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2601, q_gen_2602, q_gen_2603, q_gen_2604, q_gen_2605, q_gen_2606, q_gen_2607, q_gen_2608, q_gen_2609, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2613, q_gen_2614, q_gen_2615, q_gen_2616, q_gen_2617, q_gen_2618, q_gen_2619, q_gen_2620, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2624, q_gen_2625, q_gen_2626, q_gen_2627, q_gen_2628, q_gen_2629, q_gen_2630, q_gen_2631, q_gen_2632, q_gen_2633, q_gen_2634, q_gen_2635, q_gen_2636, q_gen_2637, q_gen_2638, q_gen_2639, q_gen_2640, q_gen_2641, q_gen_2642, q_gen_2643, q_gen_2644, q_gen_2645, q_gen_2646, q_gen_2647, q_gen_2648, q_gen_2649, q_gen_2650, q_gen_2651, q_gen_2652, q_gen_2653, q_gen_2654, q_gen_2655, q_gen_2656, q_gen_2657, q_gen_2658, q_gen_2659, q_gen_2660, q_gen_2661, q_gen_2662, q_gen_2663, q_gen_2664, q_gen_2665, q_gen_2666, q_gen_2667, q_gen_2668, q_gen_2669, q_gen_2670, q_gen_2671, q_gen_2672, q_gen_2673, q_gen_2674, q_gen_2675, q_gen_2676, q_gen_2677, q_gen_2678, q_gen_2679, q_gen_2680, q_gen_2681, q_gen_2682, q_gen_2683, q_gen_2684, q_gen_2685, q_gen_2686, q_gen_2687, q_gen_2688, q_gen_2689, q_gen_2690, q_gen_2691, q_gen_2692, q_gen_2693, q_gen_2694, q_gen_2695, q_gen_2696, q_gen_2697, q_gen_2698, q_gen_2699, q_gen_2700, q_gen_2701, q_gen_2702, q_gen_2703, q_gen_2704, q_gen_2705, q_gen_2706, q_gen_2707, q_gen_2708, q_gen_2709, q_gen_2710, q_gen_2711, q_gen_2712, q_gen_2713, q_gen_2714, q_gen_2715, q_gen_2716, q_gen_2717, q_gen_2718, q_gen_2719, q_gen_2720, q_gen_2721, q_gen_2722, q_gen_2723, q_gen_2724, q_gen_2725, q_gen_2726, q_gen_2727, q_gen_2728, q_gen_2729, q_gen_2730, q_gen_2731, q_gen_2732, q_gen_2733, q_gen_2734, q_gen_2735, q_gen_2736, q_gen_2737, q_gen_2738, q_gen_2739, q_gen_2740, q_gen_2741, q_gen_2742, q_gen_2743, q_gen_2744, q_gen_2745, q_gen_2746}, Q_f={}, Delta= { () -> q_gen_2602 () -> q_gen_2605 (q_gen_2602) -> q_gen_2610 () -> q_gen_2612 () -> q_gen_2622 () -> q_gen_2604 () -> q_gen_2607 () -> q_gen_2608 (q_gen_2615, q_gen_2607) -> q_gen_2614 () -> q_gen_2615 (q_gen_2602) -> q_gen_2617 (q_gen_2612, q_gen_2604) -> q_gen_2619 (q_gen_2605, q_gen_2617) -> q_gen_2627 (q_gen_2605, q_gen_2622) -> q_gen_2630 (q_gen_2608, q_gen_2607) -> q_gen_2632 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2619) -> q_gen_2652 (q_gen_2605, q_gen_2604) -> q_gen_2657 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2605, q_gen_2682) -> q_gen_2684 (q_gen_2612, q_gen_2619) -> q_gen_2725 (q_gen_2605, q_gen_2630) -> q_gen_2743 (q_gen_2612, q_gen_2630) -> q_gen_2746 () -> q_gen_2600 (q_gen_2602) -> q_gen_2601 (q_gen_2605, q_gen_2604) -> q_gen_2603 (q_gen_2608, q_gen_2607) -> q_gen_2606 (q_gen_2610) -> q_gen_2609 (q_gen_2612, q_gen_2604) -> q_gen_2611 (q_gen_2615, q_gen_2614) -> q_gen_2613 (q_gen_2605, q_gen_2617) -> q_gen_2616 (q_gen_2605, q_gen_2619) -> q_gen_2618 (q_gen_2608, q_gen_2621) -> q_gen_2620 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2625) -> q_gen_2624 (q_gen_2615, q_gen_2600) -> q_gen_2625 (q_gen_2605, q_gen_2627) -> q_gen_2626 (q_gen_2608, q_gen_2601) -> q_gen_2628 (q_gen_2605, q_gen_2630) -> q_gen_2629 (q_gen_2608, q_gen_2632) -> q_gen_2631 (q_gen_2608, q_gen_2629) -> q_gen_2633 (q_gen_2608, q_gen_2635) -> q_gen_2634 (q_gen_2608, q_gen_2623) -> q_gen_2635 (q_gen_2608, q_gen_2637) -> q_gen_2636 (q_gen_2608, q_gen_2638) -> q_gen_2637 (q_gen_2608, q_gen_2603) -> q_gen_2638 (q_gen_2615, q_gen_2607) -> q_gen_2639 (q_gen_2642, q_gen_2641) -> q_gen_2640 (q_gen_2612, q_gen_2622) -> q_gen_2641 (q_gen_2608, q_gen_2644) -> q_gen_2643 (q_gen_2615, q_gen_2625) -> q_gen_2644 (q_gen_2612, q_gen_2619) -> q_gen_2645 (q_gen_2647, q_gen_2621) -> q_gen_2646 (q_gen_2642, q_gen_2621) -> q_gen_2648 (q_gen_2647, q_gen_2607) -> q_gen_2649 (q_gen_2608, q_gen_2641) -> q_gen_2650 (q_gen_2612, q_gen_2652) -> q_gen_2651 (q_gen_2642, q_gen_2611) -> q_gen_2653 (q_gen_2615, q_gen_2603) -> q_gen_2654 (q_gen_2615, q_gen_2656) -> q_gen_2655 (q_gen_2612, q_gen_2657) -> q_gen_2656 (q_gen_2647, q_gen_2659) -> q_gen_2658 (q_gen_2642, q_gen_2600) -> q_gen_2659 (q_gen_2608, q_gen_2654) -> q_gen_2660 (q_gen_2615, q_gen_2629) -> q_gen_2661 (q_gen_2615, q_gen_2663) -> q_gen_2662 (q_gen_2647, q_gen_2664) -> q_gen_2663 (q_gen_2642, q_gen_2607) -> q_gen_2664 (q_gen_2642, q_gen_2666) -> q_gen_2665 (q_gen_2647, q_gen_2667) -> q_gen_2666 (q_gen_2615, q_gen_2621) -> q_gen_2667 (q_gen_2608, q_gen_2669) -> q_gen_2668 (q_gen_2647, q_gen_2600) -> q_gen_2669 (q_gen_2615, q_gen_2638) -> q_gen_2670 (q_gen_2615, q_gen_2672) -> q_gen_2671 (q_gen_2647, q_gen_2673) -> q_gen_2672 (q_gen_2605, q_gen_2657) -> q_gen_2673 (q_gen_2642, q_gen_2625) -> q_gen_2674 (q_gen_2647, q_gen_2648) -> q_gen_2675 (q_gen_2608, q_gen_2661) -> q_gen_2676 (q_gen_2608, q_gen_2678) -> q_gen_2677 (q_gen_2642, q_gen_2669) -> q_gen_2678 (q_gen_2615, q_gen_2669) -> q_gen_2679 (q_gen_2615, q_gen_2681) -> q_gen_2680 (q_gen_2605, q_gen_2682) -> q_gen_2681 (q_gen_2605, q_gen_2684) -> q_gen_2683 (q_gen_2642, q_gen_2681) -> q_gen_2685 (q_gen_2615, q_gen_2683) -> q_gen_2686 (q_gen_2615, q_gen_2606) -> q_gen_2687 (q_gen_2642, q_gen_2646) -> q_gen_2688 (q_gen_2615, q_gen_2601) -> q_gen_2689 (q_gen_2642, q_gen_2691) -> q_gen_2690 (q_gen_2615, q_gen_2692) -> q_gen_2691 (q_gen_2647, q_gen_2623) -> q_gen_2692 (q_gen_2615, q_gen_2694) -> q_gen_2693 (q_gen_2642, q_gen_2695) -> q_gen_2694 (q_gen_2647, q_gen_2696) -> q_gen_2695 (q_gen_2647, q_gen_2603) -> q_gen_2696 (q_gen_2615, q_gen_2659) -> q_gen_2697 (q_gen_2647, q_gen_2649) -> q_gen_2698 (q_gen_2647, q_gen_2700) -> q_gen_2699 (q_gen_2647, q_gen_2641) -> q_gen_2700 (q_gen_2642, q_gen_2702) -> q_gen_2701 (q_gen_2615, q_gen_2623) -> q_gen_2702 (q_gen_2615, q_gen_2704) -> q_gen_2703 (q_gen_2642, q_gen_2696) -> q_gen_2704 (q_gen_2615, q_gen_2706) -> q_gen_2705 (q_gen_2647, q_gen_2625) -> q_gen_2706 (q_gen_2647, q_gen_2650) -> q_gen_2707 (q_gen_2647, q_gen_2709) -> q_gen_2708 (q_gen_2647, q_gen_2681) -> q_gen_2709 (q_gen_2615, q_gen_2611) -> q_gen_2710 (q_gen_2642, q_gen_2645) -> q_gen_2711 (q_gen_2615, q_gen_2649) -> q_gen_2712 (q_gen_2642, q_gen_2700) -> q_gen_2713 (q_gen_2642, q_gen_2661) -> q_gen_2714 (q_gen_2647, q_gen_2629) -> q_gen_2715 (q_gen_2615, q_gen_2717) -> q_gen_2716 (q_gen_2642, q_gen_2623) -> q_gen_2717 (q_gen_2642, q_gen_2670) -> q_gen_2718 (q_gen_2642, q_gen_2650) -> q_gen_2719 (q_gen_2615, q_gen_2664) -> q_gen_2720 (q_gen_2642, q_gen_2667) -> q_gen_2721 (q_gen_2608, q_gen_2723) -> q_gen_2722 (q_gen_2642, q_gen_2706) -> q_gen_2723 (q_gen_2605, q_gen_2725) -> q_gen_2724 (q_gen_2615, q_gen_2648) -> q_gen_2726 (q_gen_2647, q_gen_2668) -> q_gen_2727 (q_gen_2615, q_gen_2641) -> q_gen_2728 (q_gen_2642, q_gen_2730) -> q_gen_2729 (q_gen_2612, q_gen_2682) -> q_gen_2730 (q_gen_2647, q_gen_2732) -> q_gen_2731 (q_gen_2612, q_gen_2630) -> q_gen_2732 (q_gen_2608, q_gen_2664) -> q_gen_2733 (q_gen_2608, q_gen_2692) -> q_gen_2734 (q_gen_2608, q_gen_2736) -> q_gen_2735 (q_gen_2608, q_gen_2696) -> q_gen_2736 (q_gen_2608, q_gen_2732) -> q_gen_2737 (q_gen_2615, q_gen_2668) -> q_gen_2738 (q_gen_2642, q_gen_2740) -> q_gen_2739 (q_gen_2608, q_gen_2730) -> q_gen_2740 (q_gen_2608, q_gen_2742) -> q_gen_2741 (q_gen_2605, q_gen_2743) -> q_gen_2742 (q_gen_2608, q_gen_2745) -> q_gen_2744 (q_gen_2612, q_gen_2746) -> q_gen_2745 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.010339 s (model generation: 0.009697, model checking: 0.000642): Model: |_ { drop -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 1 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 1 } Sat witness: Found: (() -> drop([z, l, l]), { l -> nil }) ------------------------------------------- Step 1, which took 0.010269 s (model generation: 0.009969, model checking: 0.000300): Model: |_ { drop -> {{{ Q={q_gen_2600}, Q_f={q_gen_2600}, Delta= { () -> q_gen_2600 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 1 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 1 } Sat witness: Found: (() -> drop([s(u), nil, nil]), { u -> z }) ------------------------------------------- Step 2, which took 0.010818 s (model generation: 0.010350, model checking: 0.000468): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602}, Q_f={q_gen_2600}, Delta= { () -> q_gen_2602 (q_gen_2602) -> q_gen_2600 () -> q_gen_2600 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 1 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 4 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> nil ; u -> z ; x2 -> b ; x3 -> nil }) ------------------------------------------- Step 3, which took 0.011245 s (model generation: 0.010659, model checking: 0.000586): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605}, Q_f={q_gen_2600}, Delta= { () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2604 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 () -> q_gen_2600 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 2 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 4 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(b, nil) }) ------------------------------------------- Step 4, which took 0.011686 s (model generation: 0.010987, model checking: 0.000699): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608}, Q_f={q_gen_2600}, Delta= { () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2604 () -> q_gen_2607 () -> q_gen_2608 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 3 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 4 } Sat witness: Found: (() -> drop([s(u), nil, nil]), { u -> s(z) }) ------------------------------------------- Step 5, which took 0.012683 s (model generation: 0.011566, model checking: 0.001117): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2604 () -> q_gen_2607 () -> q_gen_2608 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 4 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 7 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> nil ; u -> z ; x2 -> a ; x3 -> nil }) ------------------------------------------- Step 6, which took 0.012871 s (model generation: 0.012023, model checking: 0.000848): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2604 () -> q_gen_2607 () -> q_gen_2608 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 5 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 7 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 7, which took 0.013999 s (model generation: 0.012714, model checking: 0.001285): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 6 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 10 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> nil ; u -> s(z) ; x2 -> b ; x3 -> nil }) ------------------------------------------- Step 8, which took 0.015273 s (model generation: 0.013305, model checking: 0.001968): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 7 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 13 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> nil ; u -> s(z) ; x2 -> b ; x3 -> cons(a, nil) }) ------------------------------------------- Step 9, which took 0.016062 s (model generation: 0.013984, model checking: 0.002078): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 8 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 16 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(b, nil) ; u -> z ; x2 -> b ; x3 -> cons(b, nil) }) ------------------------------------------- Step 10, which took 0.016626 s (model generation: 0.015813, model checking: 0.000813): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2622}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2608, q_gen_2600) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2605, q_gen_2622) -> q_gen_2600 () -> q_gen_2600 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 11 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 16 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(b, nil) ; l1 -> nil ; n -> z ; x -> b }) ------------------------------------------- Step 11, which took 0.018024 s (model generation: 0.016542, model checking: 0.001482): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2621, q_gen_2622}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2600) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 14 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 16 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(b, cons(a, nil)) ; l1 -> cons(a, nil) ; n -> s(z) ; x -> b }) ------------------------------------------- Step 12, which took 0.019830 s (model generation: 0.018052, model checking: 0.001778): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2601, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2622, q_gen_2623}, Q_f={q_gen_2600, q_gen_2601}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2608, q_gen_2601) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2601 (q_gen_2602) -> q_gen_2601 (q_gen_2608, q_gen_2607) -> q_gen_2601 (q_gen_2605, q_gen_2622) -> q_gen_2601 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 17 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 16 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> cons(b, nil) ; _zm -> nil ; l1 -> cons(b, nil) ; n -> s(s(z)) ; x -> b }) ------------------------------------------- Step 13, which took 0.024436 s (model generation: 0.021514, model checking: 0.002922): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2620, q_gen_2622, q_gen_2623}, Q_f={q_gen_2600, q_gen_2620}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2620) -> q_gen_2620 (q_gen_2605, q_gen_2622) -> q_gen_2620 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 17 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 19 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> nil ; u -> z ; x2 -> b ; x3 -> cons(b, nil) }) ------------------------------------------- Step 14, which took 0.024559 s (model generation: 0.022279, model checking: 0.002280): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2620, q_gen_2622, q_gen_2623}, Q_f={q_gen_2600, q_gen_2620}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 (q_gen_2605, q_gen_2622) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2620) -> q_gen_2620 (q_gen_2605, q_gen_2622) -> q_gen_2620 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 } Datatype: Convolution form: right }}} } -- 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]) -> 14 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 20 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 19 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(b, nil) ; l1 -> cons(b, nil) ; n -> z ; x -> b }) ------------------------------------------- Step 15, which took 0.025891 s (model generation: 0.024368, model checking: 0.001523): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2615, q_gen_2621, q_gen_2622}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 (q_gen_2605, q_gen_2622) -> q_gen_2604 () -> q_gen_2604 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2600) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2600) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 20 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 19 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(b, cons(b, nil)) }) ------------------------------------------- Step 16, which took 0.014187 s (model generation: 0.013015, model checking: 0.001172): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2621, q_gen_2622, q_gen_2623}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 (q_gen_2605, q_gen_2622) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2623) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 20 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 22 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(b, nil) ; u -> s(z) ; x2 -> b ; x3 -> cons(b, cons(b, nil)) }) ------------------------------------------- Step 17, which took 0.011104 s (model generation: 0.009583, model checking: 0.001521): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2630}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2600) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2600) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 23 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 22 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(a, nil) ; l1 -> nil ; n -> z ; x -> a }) ------------------------------------------- Step 18, which took 0.029461 s (model generation: 0.026206, model checking: 0.003255): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2603, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2621, q_gen_2622, q_gen_2623}, Q_f={q_gen_2600, q_gen_2603}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 (q_gen_2605, q_gen_2622) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2608, q_gen_2603) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2621) -> q_gen_2603 (q_gen_2605, q_gen_2604) -> q_gen_2603 (q_gen_2608, q_gen_2607) -> q_gen_2603 (q_gen_2608, q_gen_2623) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 23 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 25 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(b, cons(b, cons(b, nil))) ; u -> s(s(s(z))) ; x2 -> b ; x3 -> cons(b, cons(b, cons(b, nil))) }) ------------------------------------------- Step 19, which took 0.039585 s (model generation: 0.037340, model checking: 0.002245): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2603, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2621, q_gen_2622, q_gen_2623}, Q_f={q_gen_2600, q_gen_2603}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 (q_gen_2605, q_gen_2622) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2608, q_gen_2603) -> q_gen_2600 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2603 (q_gen_2608, q_gen_2607) -> q_gen_2603 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 26 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 25 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> cons(b, nil) ; _zm -> nil ; l1 -> cons(b, nil) ; n -> z ; x -> b }) ------------------------------------------- Step 20, which took 0.042112 s (model generation: 0.036933, model checking: 0.005179): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2605, q_gen_2622) -> q_gen_2630 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 26 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 28 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, nil) ; u -> z ; x2 -> b ; x3 -> cons(a, nil) }) ------------------------------------------- Step 21, which took 0.049303 s (model generation: 0.045360, model checking: 0.003943): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2605, q_gen_2622) -> q_gen_2630 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2623) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 29 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 28 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(b, cons(a, cons(a, nil))) ; l1 -> cons(a, cons(a, nil)) ; n -> s(s(z)) ; x -> b }) ------------------------------------------- Step 22, which took 0.059182 s (model generation: 0.053650, model checking: 0.005532): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2605, q_gen_2622) -> q_gen_2630 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 } Datatype: Convolution form: right }}} } -- 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]) -> 24 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 29 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 31 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(b, nil) ; u -> z ; x2 -> a ; x3 -> cons(b, nil) }) ------------------------------------------- Step 23, which took 0.064921 s (model generation: 0.060571, model checking: 0.004350): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2605, q_gen_2622) -> q_gen_2630 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 } Datatype: Convolution form: right }}} } -- 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]) -> 25 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 32 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 31 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> cons(a, nil) ; _zm -> cons(b, nil) ; l1 -> cons(b, cons(b, nil)) ; n -> s(z) ; x -> b }) ------------------------------------------- Step 24, which took 0.066867 s (model generation: 0.065197, model checking: 0.001670): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2614, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2624, q_gen_2630}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2605 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2608, q_gen_2607) -> q_gen_2614 (q_gen_2615, q_gen_2607) -> q_gen_2614 () -> q_gen_2615 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2608, q_gen_2614) -> q_gen_2600 (q_gen_2615, q_gen_2614) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2600) -> q_gen_2621 (q_gen_2615, q_gen_2621) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2615, q_gen_2607) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2624) -> q_gen_2624 (q_gen_2615, q_gen_2600) -> q_gen_2624 (q_gen_2615, q_gen_2624) -> q_gen_2624 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 32 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 31 } Sat witness: Found: (() -> drop([z, l, l]), { l -> cons(a, nil) }) ------------------------------------------- Step 25, which took 0.067816 s (model generation: 0.064669, model checking: 0.003147): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2624, q_gen_2630}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2615 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2624) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2600) -> q_gen_2621 (q_gen_2615, q_gen_2621) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2624) -> q_gen_2624 (q_gen_2615, q_gen_2600) -> q_gen_2624 (q_gen_2612, q_gen_2622) -> q_gen_2624 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 32 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 34 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(b, nil) ; u -> z ; x2 -> b ; x3 -> cons(a, nil) }) ------------------------------------------- Step 26, which took 0.079226 s (model generation: 0.076700, model checking: 0.002526): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2606, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2642}, Q_f={q_gen_2600, q_gen_2606}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 (q_gen_2608, q_gen_2606) -> q_gen_2600 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2642, q_gen_2606) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 () -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2606 (q_gen_2608, q_gen_2607) -> q_gen_2606 (q_gen_2612, q_gen_2622) -> q_gen_2606 (q_gen_2642, q_gen_2621) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 35 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 34 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> cons(a, nil) ; _zm -> nil ; l1 -> cons(b, cons(a, nil)) ; n -> s(s(z)) ; x -> a }) ------------------------------------------- Step 27, which took 0.085763 s (model generation: 0.083536, model checking: 0.002227): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2603, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2642}, Q_f={q_gen_2600, q_gen_2603}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2642, q_gen_2603) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2603) -> q_gen_2603 (q_gen_2605, q_gen_2604) -> q_gen_2603 (q_gen_2608, q_gen_2607) -> q_gen_2603 (q_gen_2612, q_gen_2622) -> q_gen_2603 (q_gen_2642, q_gen_2600) -> q_gen_2621 (q_gen_2642, q_gen_2621) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 } Datatype: Convolution form: right }}} } -- 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, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 35 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 37 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, nil) ; u -> s(s(z)) ; x2 -> a ; x3 -> cons(a, cons(b, nil)) }) ------------------------------------------- Step 28, which took 0.094326 s (model generation: 0.093102, model checking: 0.001224): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2625, q_gen_2627, q_gen_2640}, Q_f={q_gen_2600, q_gen_2640}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2615 () -> q_gen_2615 (q_gen_2605, q_gen_2604) -> q_gen_2627 (q_gen_2605, q_gen_2622) -> q_gen_2627 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2627) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2600) -> q_gen_2621 (q_gen_2608, q_gen_2625) -> q_gen_2621 (q_gen_2615, q_gen_2621) -> q_gen_2621 (q_gen_2605, q_gen_2627) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2615, q_gen_2600) -> q_gen_2625 (q_gen_2615, q_gen_2625) -> q_gen_2625 (q_gen_2608, q_gen_2640) -> q_gen_2640 (q_gen_2615, q_gen_2640) -> q_gen_2640 (q_gen_2612, q_gen_2622) -> q_gen_2640 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 27 () -> drop([z, l, l]) -> 32 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 38 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 37 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(a, nil) ; l1 -> cons(a, nil) ; n -> z ; x -> b }) ------------------------------------------- Step 29, which took 0.085635 s (model generation: 0.082560, model checking: 0.003075): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2629, q_gen_2630, q_gen_2642}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2608, q_gen_2629) -> q_gen_2600 (q_gen_2642, q_gen_2629) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2642, q_gen_2600) -> q_gen_2621 (q_gen_2642, q_gen_2621) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2605, q_gen_2630) -> q_gen_2629 (q_gen_2612, q_gen_2622) -> q_gen_2629 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 28 () -> drop([z, l, l]) -> 33 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 38 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 40 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(b, cons(a, nil)) ; u -> s(s(z)) ; x2 -> b ; x3 -> cons(a, cons(b, nil)) }) ------------------------------------------- Step 30, which took 0.095894 s (model generation: 0.092985, model checking: 0.002909): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2627, q_gen_2641, q_gen_2642}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2608 (q_gen_2605, q_gen_2604) -> q_gen_2627 (q_gen_2605, q_gen_2622) -> q_gen_2627 () -> q_gen_2642 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2642, q_gen_2621) -> q_gen_2621 (q_gen_2605, q_gen_2627) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2612, q_gen_2627) -> q_gen_2623 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 34 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 41 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 40 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> cons(b, nil) ; _zm -> cons(a, nil) ; l1 -> cons(b, cons(b, nil)) ; n -> s(z) ; x -> a }) ------------------------------------------- Step 31, which took 0.098088 s (model generation: 0.091624, model checking: 0.006464): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2615 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2600 (q_gen_2615, q_gen_2623) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2615, q_gen_2621) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 35 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 41 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 43 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, cons(b, cons(a, nil))) ; u -> s(s(z)) ; x2 -> b ; x3 -> cons(a, cons(a, cons(b, nil))) }) ------------------------------------------- Step 32, which took 0.142118 s (model generation: 0.140230, model checking: 0.001888): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2625, q_gen_2627}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2615 () -> q_gen_2615 (q_gen_2605, q_gen_2604) -> q_gen_2627 (q_gen_2605, q_gen_2622) -> q_gen_2627 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2608, q_gen_2623) -> q_gen_2600 (q_gen_2615, q_gen_2623) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2627) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2625) -> q_gen_2623 (q_gen_2612, q_gen_2622) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2625 (q_gen_2615, q_gen_2621) -> q_gen_2625 (q_gen_2615, q_gen_2625) -> q_gen_2625 (q_gen_2612, q_gen_2627) -> q_gen_2625 } Datatype: Convolution form: right }}} } -- 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]) -> 36 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 44 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 43 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(b, cons(b, nil)) ; l1 -> cons(a, nil) ; n -> s(z) ; x -> b }) ------------------------------------------- Step 33, which took 0.135879 s (model generation: 0.134111, model checking: 0.001768): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2625, q_gen_2627, q_gen_2647}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 () -> q_gen_2615 (q_gen_2605, q_gen_2604) -> q_gen_2627 (q_gen_2605, q_gen_2622) -> q_gen_2627 () -> q_gen_2647 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2625) -> q_gen_2600 (q_gen_2647, q_gen_2600) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2600) -> q_gen_2621 (q_gen_2608, q_gen_2625) -> q_gen_2621 (q_gen_2647, q_gen_2625) -> q_gen_2621 (q_gen_2605, q_gen_2627) -> q_gen_2621 (q_gen_2612, q_gen_2627) -> q_gen_2621 (q_gen_2647, q_gen_2607) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2615, q_gen_2600) -> q_gen_2625 (q_gen_2615, q_gen_2621) -> q_gen_2625 (q_gen_2612, q_gen_2622) -> q_gen_2625 } Datatype: Convolution form: right }}} } -- 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]) -> 37 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 44 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 46 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, nil) ; u -> z ; x2 -> b ; x3 -> cons(b, nil) }) ------------------------------------------- Step 34, which took 0.146317 s (model generation: 0.143359, model checking: 0.002958): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2625, q_gen_2627, q_gen_2642}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 () -> q_gen_2615 (q_gen_2605, q_gen_2604) -> q_gen_2627 (q_gen_2605, q_gen_2622) -> q_gen_2627 () -> q_gen_2642 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2608, q_gen_2623) -> q_gen_2600 (q_gen_2615, q_gen_2621) -> q_gen_2600 (q_gen_2642, q_gen_2623) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2625) -> q_gen_2621 (q_gen_2642, q_gen_2621) -> q_gen_2621 (q_gen_2642, q_gen_2625) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2605, q_gen_2627) -> q_gen_2623 (q_gen_2612, q_gen_2622) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2625 (q_gen_2615, q_gen_2625) -> q_gen_2625 (q_gen_2642, q_gen_2600) -> q_gen_2625 (q_gen_2612, q_gen_2627) -> q_gen_2625 (q_gen_2642, q_gen_2607) -> q_gen_2625 } Datatype: Convolution form: right }}} } -- 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]) -> 38 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 47 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 46 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(b, cons(b, nil)) ; l1 -> cons(b, nil) ; n -> s(z) ; x -> b }) ------------------------------------------- Step 35, which took 0.131459 s (model generation: 0.123824, model checking: 0.007635): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2627, q_gen_2642, q_gen_2647}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2604) -> q_gen_2627 (q_gen_2605, q_gen_2622) -> q_gen_2627 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2623) -> q_gen_2600 (q_gen_2642, q_gen_2623) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2623) -> q_gen_2621 (q_gen_2642, q_gen_2621) -> q_gen_2621 (q_gen_2605, q_gen_2627) -> q_gen_2621 (q_gen_2612, q_gen_2627) -> q_gen_2621 (q_gen_2647, q_gen_2607) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2612, q_gen_2622) -> q_gen_2623 } Datatype: Convolution form: right }}} } -- 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]) -> 39 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 47 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 49 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, cons(b, nil)) ; u -> s(s(s(z))) ; x2 -> a ; x3 -> cons(a, cons(b, cons(b, nil))) }) ------------------------------------------- Step 36, which took 0.134800 s (model generation: 0.132773, model checking: 0.002027): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2627, q_gen_2642, q_gen_2647}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2604) -> q_gen_2627 (q_gen_2605, q_gen_2622) -> q_gen_2627 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2642, q_gen_2623) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2623) -> q_gen_2621 (q_gen_2615, q_gen_2621) -> q_gen_2621 (q_gen_2642, q_gen_2621) -> q_gen_2621 (q_gen_2647, q_gen_2623) -> q_gen_2621 (q_gen_2605, q_gen_2627) -> q_gen_2621 (q_gen_2612, q_gen_2627) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2612, q_gen_2622) -> q_gen_2623 } Datatype: Convolution form: right }}} } -- 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]) -> 40 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 50 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 49 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(a, cons(a, nil)) ; l1 -> cons(a, nil) ; n -> s(z) ; x -> b }) ------------------------------------------- Step 37, which took 0.136229 s (model generation: 0.131707, model checking: 0.004522): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2627, q_gen_2641, q_gen_2642}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2604) -> q_gen_2627 (q_gen_2605, q_gen_2622) -> q_gen_2627 () -> q_gen_2642 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2642, q_gen_2621) -> q_gen_2621 (q_gen_2605, q_gen_2627) -> q_gen_2621 (q_gen_2612, q_gen_2627) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 41 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 50 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 52 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(b, cons(a, nil)) ; u -> s(s(z)) ; x2 -> b ; x3 -> cons(a, cons(b, cons(b, nil))) }) ------------------------------------------- Step 38, which took 0.149785 s (model generation: 0.146719, model checking: 0.003066): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2627, q_gen_2641, q_gen_2642}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2604) -> q_gen_2627 (q_gen_2605, q_gen_2622) -> q_gen_2627 () -> q_gen_2642 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2615, q_gen_2621) -> q_gen_2621 (q_gen_2642, q_gen_2623) -> q_gen_2621 (q_gen_2605, q_gen_2627) -> q_gen_2621 (q_gen_2612, q_gen_2627) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 42 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 53 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 52 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(b, cons(a, cons(b, nil))) ; l1 -> cons(b, cons(a, nil)) ; n -> s(s(z)) ; x -> b }) ------------------------------------------- Step 39, which took 0.158487 s (model generation: 0.153433, model checking: 0.005054): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2627, q_gen_2641, q_gen_2642}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2604) -> q_gen_2627 (q_gen_2605, q_gen_2622) -> q_gen_2627 () -> q_gen_2642 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2627) -> q_gen_2621 (q_gen_2612, q_gen_2627) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 43 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 53 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 55 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> nil ; u -> s(z) ; x2 -> b ; x3 -> cons(b, nil) }) ------------------------------------------- Step 40, which took 0.175602 s (model generation: 0.171677, model checking: 0.003925): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2600 (q_gen_2615, q_gen_2623) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 44 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 56 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 55 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(a, cons(b, nil)) ; l1 -> cons(a, nil) ; n -> s(z) ; x -> a }) ------------------------------------------- Step 41, which took 0.190301 s (model generation: 0.184859, model checking: 0.005442): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 45 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 56 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 58 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, nil) ; u -> s(z) ; x2 -> a ; x3 -> cons(b, cons(a, nil)) }) ------------------------------------------- Step 42, which took 0.220475 s (model generation: 0.219075, model checking: 0.001400): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2601, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642}, Q_f={q_gen_2600, q_gen_2601}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 (q_gen_2612, q_gen_2622) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2601) -> q_gen_2600 (q_gen_2642, q_gen_2600) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2601 (q_gen_2605, q_gen_2604) -> q_gen_2601 (q_gen_2612, q_gen_2604) -> q_gen_2601 (q_gen_2602) -> q_gen_2601 (q_gen_2608, q_gen_2607) -> q_gen_2601 (q_gen_2615, q_gen_2621) -> q_gen_2621 (q_gen_2642, q_gen_2601) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2601) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 46 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 59 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 58 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> cons(b, nil) ; _zm -> nil ; l1 -> cons(b, cons(a, nil)) ; n -> s(z) ; x -> b }) ------------------------------------------- Step 43, which took 0.213636 s (model generation: 0.209210, model checking: 0.004426): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2682) -> q_gen_2630 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 47 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 59 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 61 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, nil) ; u -> s(s(z)) ; x2 -> a ; x3 -> cons(b, cons(b, cons(a, nil))) }) ------------------------------------------- Step 44, which took 0.274996 s (model generation: 0.271242, model checking: 0.003754): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 48 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 62 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 61 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> cons(b, nil) ; _zm -> cons(a, nil) ; l1 -> cons(b, cons(a, nil)) ; n -> s(z) ; x -> a }) ------------------------------------------- Step 45, which took 0.282583 s (model generation: 0.280429, model checking: 0.002154): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2601, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647}, Q_f={q_gen_2600, q_gen_2601}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 (q_gen_2612, q_gen_2622) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2600) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2621) -> q_gen_2601 (q_gen_2615, q_gen_2601) -> q_gen_2601 (q_gen_2615, q_gen_2623) -> q_gen_2601 (q_gen_2605, q_gen_2604) -> q_gen_2601 (q_gen_2612, q_gen_2604) -> q_gen_2601 (q_gen_2602) -> q_gen_2601 (q_gen_2608, q_gen_2607) -> q_gen_2601 (q_gen_2608, q_gen_2601) -> q_gen_2621 (q_gen_2608, q_gen_2641) -> q_gen_2621 (q_gen_2642, q_gen_2601) -> q_gen_2621 (q_gen_2642, q_gen_2623) -> q_gen_2621 (q_gen_2647, q_gen_2623) -> q_gen_2621 (q_gen_2647, q_gen_2641) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2642, q_gen_2607) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2647, q_gen_2601) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 49 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 62 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 64 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, cons(b, nil)) ; u -> s(z) ; x2 -> b ; x3 -> cons(a, cons(b, nil)) }) ------------------------------------------- Step 46, which took 0.251301 s (model generation: 0.249700, model checking: 0.001601): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2601, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647}, Q_f={q_gen_2600, q_gen_2601}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 (q_gen_2612, q_gen_2622) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2615, q_gen_2601) -> q_gen_2601 (q_gen_2642, q_gen_2641) -> q_gen_2601 (q_gen_2647, q_gen_2621) -> q_gen_2601 (q_gen_2605, q_gen_2604) -> q_gen_2601 (q_gen_2612, q_gen_2604) -> q_gen_2601 (q_gen_2602) -> q_gen_2601 (q_gen_2615, q_gen_2641) -> q_gen_2621 (q_gen_2642, q_gen_2601) -> q_gen_2621 (q_gen_2642, q_gen_2623) -> q_gen_2621 (q_gen_2647, q_gen_2641) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2647, q_gen_2607) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2601) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2647, q_gen_2601) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2608, q_gen_2641) -> q_gen_2641 (q_gen_2615, q_gen_2623) -> q_gen_2641 (q_gen_2642, q_gen_2600) -> q_gen_2641 (q_gen_2647, q_gen_2600) -> q_gen_2641 (q_gen_2642, q_gen_2607) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 50 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 65 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 64 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(a, nil) ; l1 -> nil ; n -> s(z) ; x -> a }) ------------------------------------------- Step 47, which took 0.704499 s (model generation: 0.693629, model checking: 0.010870): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2600) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2621 (q_gen_2642, q_gen_2623) -> q_gen_2621 (q_gen_2647, q_gen_2623) -> q_gen_2621 (q_gen_2647, q_gen_2641) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2647, q_gen_2607) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2641 (q_gen_2615, q_gen_2623) -> q_gen_2641 (q_gen_2642, q_gen_2621) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2642, q_gen_2607) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 51 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 65 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 67 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, cons(a, cons(b, cons(b, nil)))) ; u -> s(s(s(s(z)))) ; x2 -> a ; x3 -> cons(b, cons(a, cons(a, cons(b, nil)))) }) ------------------------------------------- Step 48, which took 0.496976 s (model generation: 0.493837, model checking: 0.003139): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2621 (q_gen_2647, q_gen_2641) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2647, q_gen_2607) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2641 (q_gen_2642, q_gen_2600) -> q_gen_2641 (q_gen_2642, q_gen_2621) -> q_gen_2641 (q_gen_2647, q_gen_2623) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 52 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 68 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 67 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(a, cons(a, nil)) ; l1 -> cons(b, nil) ; n -> s(z) ; x -> a }) ------------------------------------------- Step 49, which took 0.602570 s (model generation: 0.593290, model checking: 0.009280): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2600) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2621 (q_gen_2642, q_gen_2623) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2647, q_gen_2607) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2647, q_gen_2641) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2641 (q_gen_2647, q_gen_2623) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2642, q_gen_2607) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 53 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 68 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 70 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(b, cons(b, nil)) ; u -> s(z) ; x2 -> a ; x3 -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 50, which took 0.794770 s (model generation: 0.790513, model checking: 0.004257): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2600) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2621 (q_gen_2642, q_gen_2623) -> q_gen_2621 (q_gen_2647, q_gen_2623) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2647, q_gen_2641) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 54 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 71 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 70 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(b, nil) ; l1 -> nil ; n -> z ; x -> a }) ------------------------------------------- Step 51, which took 0.679137 s (model generation: 0.670424, model checking: 0.008713): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2621 (q_gen_2647, q_gen_2623) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2642, q_gen_2607) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2641) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 55 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 71 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 73 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, cons(a, cons(b, nil))) ; u -> s(s(s(z))) ; x2 -> a ; x3 -> cons(b, cons(a, cons(b, nil))) }) ------------------------------------------- Step 52, which took 0.825796 s (model generation: 0.820737, model checking: 0.005059): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2642, q_gen_2607) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2641) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2641 (q_gen_2615, q_gen_2623) -> q_gen_2641 (q_gen_2642, q_gen_2621) -> q_gen_2641 (q_gen_2642, q_gen_2623) -> q_gen_2641 (q_gen_2647, q_gen_2623) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2647, q_gen_2607) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 56 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 74 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 73 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(a, cons(b, cons(a, nil))) ; l1 -> cons(a, cons(a, nil)) ; n -> s(s(z)) ; x -> a }) ------------------------------------------- Step 53, which took 0.765826 s (model generation: 0.757139, model checking: 0.008687): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2641 (q_gen_2615, q_gen_2623) -> q_gen_2641 (q_gen_2642, q_gen_2621) -> q_gen_2641 (q_gen_2642, q_gen_2623) -> q_gen_2641 (q_gen_2647, q_gen_2641) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2642, q_gen_2607) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 57 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 74 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 76 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(b, cons(b, nil)) ; u -> s(s(z)) ; x2 -> a ; x3 -> cons(a, cons(b, cons(a, nil))) }) ------------------------------------------- Step 54, which took 0.993276 s (model generation: 0.990127, model checking: 0.003149): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2603, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647}, Q_f={q_gen_2600, q_gen_2603}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 (q_gen_2612, q_gen_2622) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2615, q_gen_2603) -> q_gen_2603 (q_gen_2615, q_gen_2623) -> q_gen_2603 (q_gen_2647, q_gen_2603) -> q_gen_2603 (q_gen_2647, q_gen_2621) -> q_gen_2603 (q_gen_2605, q_gen_2604) -> q_gen_2603 (q_gen_2612, q_gen_2604) -> q_gen_2603 (q_gen_2642, q_gen_2603) -> q_gen_2621 (q_gen_2642, q_gen_2623) -> q_gen_2621 (q_gen_2647, q_gen_2623) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2603) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2608, q_gen_2641) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2641) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2641 (q_gen_2647, q_gen_2600) -> q_gen_2641 (q_gen_2647, q_gen_2641) -> q_gen_2641 (q_gen_2642, q_gen_2607) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 58 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 77 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 76 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(a, cons(a, nil)) ; l1 -> cons(a, nil) ; n -> s(z) ; x -> a }) ------------------------------------------- Step 55, which took 0.889939 s (model generation: 0.887038, model checking: 0.002901): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2603, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2625, q_gen_2630, q_gen_2642, q_gen_2647}, Q_f={q_gen_2600, q_gen_2603}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 (q_gen_2612, q_gen_2622) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2642, q_gen_2623) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2615, q_gen_2603) -> q_gen_2603 (q_gen_2605, q_gen_2604) -> q_gen_2603 (q_gen_2612, q_gen_2604) -> q_gen_2603 (q_gen_2608, q_gen_2625) -> q_gen_2621 (q_gen_2642, q_gen_2603) -> q_gen_2621 (q_gen_2647, q_gen_2603) -> q_gen_2621 (q_gen_2647, q_gen_2625) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2603) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2612, q_gen_2622) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2625 (q_gen_2615, q_gen_2623) -> q_gen_2625 (q_gen_2615, q_gen_2625) -> q_gen_2625 (q_gen_2642, q_gen_2625) -> q_gen_2625 (q_gen_2647, q_gen_2600) -> q_gen_2625 (q_gen_2647, q_gen_2623) -> q_gen_2625 (q_gen_2647, q_gen_2607) -> q_gen_2625 } Datatype: Convolution form: right }}} } -- 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]) -> 59 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 77 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 79 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, nil) ; u -> s(s(z)) ; x2 -> b ; x3 -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 56, which took 0.940699 s (model generation: 0.935071, model checking: 0.005628): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2615, q_gen_2621) -> q_gen_2621 (q_gen_2642, q_gen_2621) -> q_gen_2621 (q_gen_2647, q_gen_2623) -> q_gen_2621 (q_gen_2647, q_gen_2641) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2647, q_gen_2607) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2608, q_gen_2641) -> q_gen_2641 (q_gen_2615, q_gen_2623) -> q_gen_2641 (q_gen_2642, q_gen_2623) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 60 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 80 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 79 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(a, cons(a, cons(b, nil))) ; l1 -> cons(a, cons(b, nil)) ; n -> s(s(z)) ; x -> b }) ------------------------------------------- Step 57, which took 1.213654 s (model generation: 1.209485, model checking: 0.004169): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2624, q_gen_2630, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2624) -> q_gen_2600 (q_gen_2642, q_gen_2624) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2615, q_gen_2621) -> q_gen_2621 (q_gen_2647, q_gen_2624) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2624) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2624 (q_gen_2642, q_gen_2621) -> q_gen_2624 (q_gen_2605, q_gen_2682) -> q_gen_2624 (q_gen_2642, q_gen_2607) -> q_gen_2624 (q_gen_2647, q_gen_2607) -> q_gen_2624 (q_gen_2612, q_gen_2622) -> q_gen_2624 } Datatype: Convolution form: right }}} } -- 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]) -> 61 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 80 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 82 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, cons(b, nil)) ; u -> s(z) ; x2 -> b ; x3 -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 58, which took 1.194599 s (model generation: 1.187512, model checking: 0.007087): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2608, q_gen_2641) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2641) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2642, q_gen_2607) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 62 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 83 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 82 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> cons(b, nil) ; _zm -> cons(a, cons(a, nil)) ; l1 -> cons(a, cons(b, cons(b, nil))) ; n -> s(s(z)) ; x -> b }) ------------------------------------------- Step 59, which took 1.299401 s (model generation: 1.291017, model checking: 0.008384): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2608, q_gen_2641) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2641 (q_gen_2647, q_gen_2641) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 63 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 83 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 85 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, cons(a, cons(b, nil))) ; u -> s(s(s(z))) ; x2 -> b ; x3 -> cons(a, cons(b, cons(b, nil))) }) ------------------------------------------- Step 60, which took 1.939110 s (model generation: 1.932608, model checking: 0.006502): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2615, q_gen_2621) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2641) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2608, q_gen_2641) -> q_gen_2641 (q_gen_2642, q_gen_2621) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 64 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 86 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 85 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> cons(a, nil) ; _zm -> cons(a, cons(b, nil)) ; l1 -> cons(b, cons(a, nil)) ; n -> s(z) ; x -> b }) ------------------------------------------- Step 61, which took 1.921795 s (model generation: 1.919458, model checking: 0.002337): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2621 (q_gen_2615, q_gen_2621) -> q_gen_2621 (q_gen_2647, q_gen_2641) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2642, q_gen_2607) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 65 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 86 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 88 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, cons(a, nil)) ; u -> s(z) ; x2 -> b ; x3 -> cons(a, cons(b, nil)) }) ------------------------------------------- Step 62, which took 1.714263 s (model generation: 1.709782, model checking: 0.004481): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2615, q_gen_2621) -> q_gen_2621 (q_gen_2642, q_gen_2621) -> q_gen_2621 (q_gen_2647, q_gen_2623) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2642, q_gen_2607) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2608, q_gen_2641) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2641) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 66 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 89 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 88 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(b, cons(a, cons(b, cons(a, nil)))) ; l1 -> cons(b, cons(a, cons(a, nil))) ; n -> s(s(s(z))) ; x -> b }) ------------------------------------------- Step 63, which took 2.184626 s (model generation: 2.183075, model checking: 0.001551): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2615, q_gen_2621) -> q_gen_2621 (q_gen_2647, q_gen_2623) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2608, q_gen_2641) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2641) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 67 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 89 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 91 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, cons(a, nil)) ; u -> s(s(z)) ; x2 -> b ; x3 -> cons(a, cons(b, cons(b, nil))) }) ------------------------------------------- Step 64, which took 2.432786 s (model generation: 2.428915, model checking: 0.003871): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2623) -> q_gen_2621 (q_gen_2647, q_gen_2623) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2641) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2641) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 68 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 92 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 91 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(b, cons(b, cons(b, nil))) ; l1 -> cons(b, cons(a, nil)) ; n -> s(s(z)) ; x -> a }) ------------------------------------------- Step 65, which took 1.933802 s (model generation: 1.916735, model checking: 0.017067): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2621 (q_gen_2647, q_gen_2641) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2647, q_gen_2607) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 69 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 92 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 94 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, nil) ; u -> s(z) ; x2 -> b ; x3 -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 66, which took 2.984948 s (model generation: 2.979139, model checking: 0.005809): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2615, q_gen_2621) -> q_gen_2621 (q_gen_2642, q_gen_2621) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2608, q_gen_2641) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2641) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 70 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 95 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 94 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> cons(b, nil) ; _zm -> cons(b, cons(a, nil)) ; l1 -> cons(a, cons(b, nil)) ; n -> s(z) ; x -> a }) ------------------------------------------- Step 67, which took 1.852838 s (model generation: 1.841415, model checking: 0.011423): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2621 (q_gen_2647, q_gen_2641) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 71 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 95 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 97 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(b, nil) ; u -> s(z) ; x2 -> a ; x3 -> cons(a, cons(b, nil)) }) ------------------------------------------- Step 68, which took 2.611165 s (model generation: 2.605722, model checking: 0.005443): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2621 (q_gen_2647, q_gen_2641) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2612, q_gen_2630) -> q_gen_2621 (q_gen_2642, q_gen_2607) -> q_gen_2621 (q_gen_2647, q_gen_2607) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 67 () -> drop([z, l, l]) -> 72 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 98 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 97 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> cons(b, cons(a, nil)) ; _zm -> cons(b, nil) ; l1 -> cons(b, cons(b, nil)) ; n -> s(z) ; x -> a }) ------------------------------------------- Step 69, which took 2.159255 s (model generation: 2.141841, model checking: 0.017414): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2621 (q_gen_2647, q_gen_2623) -> q_gen_2621 (q_gen_2647, q_gen_2641) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2612, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 68 () -> drop([z, l, l]) -> 73 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 98 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 100 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(b, cons(b, cons(b, nil))) ; u -> s(s(s(z))) ; x2 -> b ; x3 -> cons(b, cons(a, cons(b, nil))) }) ------------------------------------------- Step 70, which took 2.905980 s (model generation: 2.899679, model checking: 0.006301): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2608, q_gen_2641) -> q_gen_2621 (q_gen_2647, q_gen_2641) -> q_gen_2621 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2612, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 74 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 101 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 100 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> cons(a, nil) ; _zm -> cons(b, cons(b, nil)) ; l1 -> cons(a, cons(b, cons(a, nil))) ; n -> s(s(z)) ; x -> a }) ------------------------------------------- Step 71, which took 3.216421 s (model generation: 3.211061, model checking: 0.005360): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2647, q_gen_2641) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2608, q_gen_2641) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2630) -> q_gen_2641 (q_gen_2612, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- 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]) -> 75 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 101 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 103 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(b, nil) ; u -> s(z) ; x2 -> b ; x3 -> cons(a, cons(b, nil)) }) ------------------------------------------- Step 72, which took 2.935039 s (model generation: 2.929078, model checking: 0.005961): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2624, q_gen_2630, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2624) -> q_gen_2600 (q_gen_2642, q_gen_2624) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2612, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2624) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2624 (q_gen_2647, q_gen_2624) -> q_gen_2624 (q_gen_2605, q_gen_2682) -> q_gen_2624 (q_gen_2612, q_gen_2682) -> q_gen_2624 (q_gen_2647, q_gen_2607) -> q_gen_2624 (q_gen_2612, q_gen_2622) -> q_gen_2624 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 71 () -> drop([z, l, l]) -> 76 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 104 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 103 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> nil ; _zm -> cons(a, cons(b, cons(b, nil))) ; l1 -> cons(b, cons(a, nil)) ; n -> s(s(z)) ; x -> a }) ------------------------------------------- Step 73, which took 3.005785 s (model generation: 2.997871, model checking: 0.007914): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2612, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2608, q_gen_2641) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2641) -> q_gen_2641 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 72 () -> drop([z, l, l]) -> 77 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 104 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 106 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(a, cons(b, nil)) ; u -> s(s(z)) ; x2 -> b ; x3 -> cons(b, cons(a, cons(a, nil))) }) ------------------------------------------- Step 74, which took 2.808838 s (model generation: 2.789846, model checking: 0.018992): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2612, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2608, q_gen_2641) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2641) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 73 () -> drop([z, l, l]) -> 78 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 105 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 109 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(b, nil) ; u -> s(s(z)) ; x2 -> b ; x3 -> cons(b, cons(b, cons(b, nil))) }) ------------------------------------------- Step 75, which took 5.307649 s (model generation: 5.285791, model checking: 0.021858): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2647, q_gen_2682}, Q_f={q_gen_2600}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2604) -> q_gen_2604 (q_gen_2612, q_gen_2604) -> q_gen_2604 (q_gen_2602) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2605, q_gen_2630) -> q_gen_2630 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2682) -> q_gen_2682 (q_gen_2612, q_gen_2622) -> q_gen_2682 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2615, q_gen_2641) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2621) -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2600 (q_gen_2612, q_gen_2604) -> q_gen_2600 (q_gen_2602) -> q_gen_2600 (q_gen_2608, q_gen_2607) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2630) -> q_gen_2621 (q_gen_2612, q_gen_2630) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2623) -> q_gen_2623 (q_gen_2608, q_gen_2641) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2623 (q_gen_2615, q_gen_2621) -> q_gen_2623 (q_gen_2615, q_gen_2623) -> q_gen_2623 (q_gen_2642, q_gen_2600) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2642, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2600) -> q_gen_2623 (q_gen_2647, q_gen_2623) -> q_gen_2623 (q_gen_2647, q_gen_2641) -> q_gen_2623 (q_gen_2642, q_gen_2607) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2605, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2682) -> q_gen_2641 (q_gen_2612, q_gen_2622) -> q_gen_2641 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 74 () -> drop([z, l, l]) -> 79 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 106 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 112 } Sat witness: Found: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), { _um -> cons(b, nil) ; u -> s(s(z)) ; x2 -> b ; x3 -> cons(a, cons(a, cons(b, nil))) }) ------------------------------------------- Step 76, which took 2.029084 s (model generation: 2.025359, model checking: 0.003725): Model: |_ { drop -> {{{ Q={q_gen_2600, q_gen_2601, q_gen_2602, q_gen_2604, q_gen_2605, q_gen_2607, q_gen_2608, q_gen_2612, q_gen_2615, q_gen_2617, q_gen_2621, q_gen_2622, q_gen_2623, q_gen_2625, q_gen_2629, q_gen_2630, q_gen_2641, q_gen_2642, q_gen_2643, q_gen_2644, q_gen_2645, q_gen_2646, q_gen_2647, q_gen_2650, q_gen_2657, q_gen_2659, q_gen_2660, q_gen_2661, q_gen_2662, q_gen_2663, q_gen_2664, q_gen_2666, q_gen_2667, q_gen_2668, q_gen_2669, q_gen_2671, q_gen_2672, q_gen_2673, q_gen_2675, q_gen_2676, q_gen_2677, q_gen_2683, q_gen_2684, q_gen_2685, q_gen_2686, q_gen_2688, q_gen_2690, q_gen_2691, q_gen_2693, q_gen_2694}, Q_f={q_gen_2600, q_gen_2601, q_gen_2646, q_gen_2673}, Delta= { (q_gen_2602) -> q_gen_2602 () -> q_gen_2602 () -> q_gen_2605 () -> q_gen_2612 () -> q_gen_2622 (q_gen_2605, q_gen_2617) -> q_gen_2604 () -> q_gen_2604 (q_gen_2608, q_gen_2607) -> q_gen_2607 (q_gen_2615, q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2608 () -> q_gen_2615 (q_gen_2612, q_gen_2604) -> q_gen_2617 (q_gen_2612, q_gen_2617) -> q_gen_2617 (q_gen_2602) -> q_gen_2617 (q_gen_2605, q_gen_2622) -> q_gen_2630 () -> q_gen_2642 () -> q_gen_2647 (q_gen_2605, q_gen_2604) -> q_gen_2657 (q_gen_2612, q_gen_2622) -> q_gen_2657 (q_gen_2605, q_gen_2630) -> q_gen_2684 (q_gen_2605, q_gen_2657) -> q_gen_2684 (q_gen_2612, q_gen_2630) -> q_gen_2684 (q_gen_2608, q_gen_2621) -> q_gen_2600 (q_gen_2608, q_gen_2629) -> q_gen_2600 (q_gen_2608, q_gen_2683) -> q_gen_2600 (q_gen_2608, q_gen_2690) -> q_gen_2600 (q_gen_2608, q_gen_2691) -> q_gen_2600 (q_gen_2615, q_gen_2673) -> q_gen_2600 (q_gen_2642, q_gen_2641) -> q_gen_2600 (q_gen_2647, q_gen_2691) -> q_gen_2600 (q_gen_2605, q_gen_2617) -> q_gen_2600 (q_gen_2615, q_gen_2607) -> q_gen_2600 () -> q_gen_2600 (q_gen_2605, q_gen_2604) -> q_gen_2601 (q_gen_2612, q_gen_2604) -> q_gen_2601 (q_gen_2602) -> q_gen_2601 (q_gen_2608, q_gen_2607) -> q_gen_2601 (q_gen_2608, q_gen_2623) -> q_gen_2621 (q_gen_2608, q_gen_2625) -> q_gen_2621 (q_gen_2615, q_gen_2659) -> q_gen_2621 (q_gen_2615, q_gen_2668) -> q_gen_2621 (q_gen_2615, q_gen_2669) -> q_gen_2621 (q_gen_2642, q_gen_2625) -> q_gen_2621 (q_gen_2647, q_gen_2650) -> q_gen_2621 (q_gen_2647, q_gen_2668) -> q_gen_2621 (q_gen_2647, q_gen_2672) -> q_gen_2621 (q_gen_2605, q_gen_2622) -> q_gen_2621 (q_gen_2608, q_gen_2600) -> q_gen_2623 (q_gen_2608, q_gen_2601) -> q_gen_2623 (q_gen_2608, q_gen_2693) -> q_gen_2623 (q_gen_2642, q_gen_2621) -> q_gen_2623 (q_gen_2647, q_gen_2607) -> q_gen_2623 (q_gen_2615, q_gen_2600) -> q_gen_2625 (q_gen_2605, q_gen_2630) -> q_gen_2629 (q_gen_2612, q_gen_2622) -> q_gen_2641 (q_gen_2608, q_gen_2644) -> q_gen_2643 (q_gen_2615, q_gen_2625) -> q_gen_2644 (q_gen_2612, q_gen_2617) -> q_gen_2645 (q_gen_2647, q_gen_2621) -> q_gen_2646 (q_gen_2608, q_gen_2641) -> q_gen_2650 (q_gen_2615, q_gen_2601) -> q_gen_2650 (q_gen_2615, q_gen_2650) -> q_gen_2650 (q_gen_2642, q_gen_2601) -> q_gen_2650 (q_gen_2647, q_gen_2659) -> q_gen_2650 (q_gen_2612, q_gen_2657) -> q_gen_2650 (q_gen_2642, q_gen_2600) -> q_gen_2659 (q_gen_2608, q_gen_2650) -> q_gen_2660 (q_gen_2615, q_gen_2629) -> q_gen_2661 (q_gen_2615, q_gen_2663) -> q_gen_2662 (q_gen_2647, q_gen_2664) -> q_gen_2663 (q_gen_2615, q_gen_2623) -> q_gen_2664 (q_gen_2642, q_gen_2666) -> q_gen_2664 (q_gen_2642, q_gen_2607) -> q_gen_2664 (q_gen_2647, q_gen_2667) -> q_gen_2666 (q_gen_2615, q_gen_2621) -> q_gen_2667 (q_gen_2608, q_gen_2669) -> q_gen_2668 (q_gen_2647, q_gen_2600) -> q_gen_2669 (q_gen_2615, q_gen_2672) -> q_gen_2671 (q_gen_2647, q_gen_2673) -> q_gen_2672 (q_gen_2605, q_gen_2657) -> q_gen_2673 (q_gen_2647, q_gen_2623) -> q_gen_2675 (q_gen_2608, q_gen_2661) -> q_gen_2676 (q_gen_2608, q_gen_2677) -> q_gen_2677 (q_gen_2642, q_gen_2650) -> q_gen_2677 (q_gen_2642, q_gen_2669) -> q_gen_2677 (q_gen_2605, q_gen_2684) -> q_gen_2683 (q_gen_2642, q_gen_2673) -> q_gen_2685 (q_gen_2615, q_gen_2683) -> q_gen_2686 (q_gen_2642, q_gen_2646) -> q_gen_2688 (q_gen_2642, q_gen_2691) -> q_gen_2690 (q_gen_2612, q_gen_2684) -> q_gen_2690 (q_gen_2615, q_gen_2675) -> q_gen_2691 (q_gen_2612, q_gen_2630) -> q_gen_2691 (q_gen_2615, q_gen_2694) -> q_gen_2693 (q_gen_2642, q_gen_2623) -> q_gen_2693 (q_gen_2647, q_gen_2601) -> q_gen_2693 (q_gen_2647, q_gen_2625) -> q_gen_2693 (q_gen_2608, q_gen_2664) -> q_gen_2694 (q_gen_2608, q_gen_2675) -> q_gen_2694 (q_gen_2608, q_gen_2694) -> q_gen_2694 (q_gen_2615, q_gen_2641) -> q_gen_2694 (q_gen_2615, q_gen_2664) -> q_gen_2694 (q_gen_2615, q_gen_2693) -> q_gen_2694 (q_gen_2642, q_gen_2645) -> q_gen_2694 (q_gen_2642, q_gen_2660) -> q_gen_2694 (q_gen_2642, q_gen_2661) -> q_gen_2694 (q_gen_2642, q_gen_2664) -> q_gen_2694 (q_gen_2642, q_gen_2667) -> q_gen_2694 (q_gen_2642, q_gen_2693) -> q_gen_2694 (q_gen_2642, q_gen_2694) -> q_gen_2694 (q_gen_2647, q_gen_2629) -> q_gen_2694 (q_gen_2647, q_gen_2641) -> q_gen_2694 (q_gen_2647, q_gen_2693) -> q_gen_2694 (q_gen_2647, q_gen_2694) -> q_gen_2694 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> drop([s(u), nil, nil]) -> 75 () -> drop([z, l, l]) -> 80 (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 109 (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 112 } Sat witness: Found: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), { _an -> cons(a, nil) ; _zm -> nil ; l1 -> cons(a, nil) ; n -> z ; x -> b }) Total time: 65.278225 Reason for stopping: DontKnow. Stopped because: timeout