Solving ../../benchmarks/true/isaplanner_prop54.smt2... Inference procedure has parameters: Ice fuel: 200 Timeout: 30s Convolution: complete Learning problem is: env: { nat -> {s, z} } definition: { (minus, F: {() -> minus([s(u), z, s(u)]) () -> minus([z, y, z]) (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec])} (minus([_fc, _gc, _hc]) /\ minus([_fc, _gc, _ic])) -> eq_nat([_hc, _ic]) ) (plus, F: {() -> plus([n, z, n]) (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)])} (plus([_kc, _lc, _mc]) /\ plus([_kc, _lc, _nc])) -> eq_nat([_mc, _nc]) ) } properties: {(minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m])} over-approximation: {minus, plus} under-approximation: {} Clause system for inference is: { () -> minus([s(u), z, s(u)]) -> 0 ; () -> minus([z, y, z]) -> 0 ; () -> plus([n, z, n]) -> 0 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 0 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 0 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 0 } Solving took 30.568983 seconds. DontKnow. Stopped because: timeout Working model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2604, q_gen_2606, q_gen_2607, q_gen_2608, q_gen_2609, q_gen_2613, q_gen_2614, q_gen_2618, q_gen_2619, q_gen_2623, q_gen_2624, q_gen_2625, q_gen_2630, q_gen_2631, q_gen_2632, q_gen_2635, q_gen_2636, q_gen_2640, q_gen_2641, q_gen_2642, q_gen_2643, q_gen_2644, q_gen_2646, q_gen_2647, q_gen_2652, q_gen_2657, q_gen_2658, q_gen_2659, q_gen_2663, q_gen_2664, q_gen_2665, q_gen_2666, q_gen_2667, q_gen_2668, q_gen_2672, q_gen_2674, 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_2690, q_gen_2693, q_gen_2694, q_gen_2695, q_gen_2696, q_gen_2697, q_gen_2698, q_gen_2703, q_gen_2704, q_gen_2705, q_gen_2708, q_gen_2709, q_gen_2710, q_gen_2711, q_gen_2712, q_gen_2713, q_gen_2715, q_gen_2716, q_gen_2717, q_gen_2718, q_gen_2719, q_gen_2720, q_gen_2730, q_gen_2735, q_gen_2736, q_gen_2744}, Q_f={}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2659 () -> q_gen_2601 (q_gen_2601) -> q_gen_2609 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2642 (q_gen_2607) -> q_gen_2647 (q_gen_2609) -> q_gen_2664 (q_gen_2624) -> q_gen_2666 (q_gen_2619) -> q_gen_2680 (q_gen_2659) -> q_gen_2696 (q_gen_2647) -> q_gen_2705 (q_gen_2680) -> q_gen_2709 (q_gen_2659) -> q_gen_2712 () -> q_gen_2599 (q_gen_2601) -> q_gen_2600 (q_gen_2601) -> q_gen_2604 (q_gen_2607) -> q_gen_2606 (q_gen_2609) -> q_gen_2608 (q_gen_2614) -> q_gen_2613 (q_gen_2607) -> q_gen_2614 (q_gen_2619) -> q_gen_2618 (q_gen_2624) -> q_gen_2623 (q_gen_2599) -> q_gen_2625 (q_gen_2624) -> q_gen_2630 (q_gen_2600) -> q_gen_2631 (q_gen_2604) -> q_gen_2632 (q_gen_2606) -> q_gen_2635 (q_gen_2623) -> q_gen_2636 (q_gen_2641) -> q_gen_2640 (q_gen_2642) -> q_gen_2641 (q_gen_2644) -> q_gen_2643 (q_gen_2630) -> q_gen_2644 (q_gen_2647) -> q_gen_2646 (q_gen_2613) -> q_gen_2652 (q_gen_2646) -> q_gen_2657 (q_gen_2659) -> q_gen_2658 (q_gen_2664) -> q_gen_2663 (q_gen_2666) -> q_gen_2665 (q_gen_2668) -> q_gen_2667 (q_gen_2619) -> q_gen_2668 (q_gen_2642) -> q_gen_2672 (q_gen_2609) -> q_gen_2674 (q_gen_2680) -> q_gen_2679 (q_gen_2682) -> q_gen_2681 (q_gen_2680) -> q_gen_2682 (q_gen_2684) -> q_gen_2683 (q_gen_2685) -> q_gen_2684 (q_gen_2659) -> q_gen_2685 (q_gen_2687) -> q_gen_2686 (q_gen_2647) -> q_gen_2687 (q_gen_2667) -> q_gen_2690 (q_gen_2666) -> q_gen_2693 (q_gen_2608) -> q_gen_2694 (q_gen_2696) -> q_gen_2695 (q_gen_2698) -> q_gen_2697 (q_gen_2631) -> q_gen_2698 (q_gen_2704) -> q_gen_2703 (q_gen_2705) -> q_gen_2704 (q_gen_2709) -> q_gen_2708 (q_gen_2711) -> q_gen_2710 (q_gen_2712) -> q_gen_2711 (q_gen_2709) -> q_gen_2713 (q_gen_2716) -> q_gen_2715 (q_gen_2705) -> q_gen_2716 (q_gen_2681) -> q_gen_2717 (q_gen_2635) -> q_gen_2718 (q_gen_2636) -> q_gen_2719 (q_gen_2652) -> q_gen_2720 (q_gen_2683) -> q_gen_2730 (q_gen_2736) -> q_gen_2735 (q_gen_2679) -> q_gen_2736 (q_gen_2664) -> q_gen_2744 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2605, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2616, q_gen_2617, q_gen_2620, q_gen_2621, q_gen_2622, q_gen_2626, q_gen_2627, q_gen_2628, q_gen_2629, q_gen_2633, q_gen_2634, q_gen_2637, q_gen_2638, q_gen_2639, q_gen_2645, q_gen_2648, q_gen_2649, q_gen_2650, q_gen_2651, q_gen_2653, q_gen_2654, q_gen_2655, q_gen_2656, q_gen_2660, q_gen_2661, q_gen_2662, q_gen_2669, q_gen_2670, q_gen_2671, q_gen_2673, q_gen_2675, q_gen_2676, q_gen_2677, q_gen_2678, q_gen_2688, q_gen_2689, q_gen_2691, q_gen_2692, q_gen_2699, q_gen_2700, q_gen_2701, q_gen_2702, q_gen_2706, q_gen_2707, q_gen_2714, 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_2731, q_gen_2732, q_gen_2733, q_gen_2734, q_gen_2737, q_gen_2738, q_gen_2739, q_gen_2740, q_gen_2741, q_gen_2742, q_gen_2743, q_gen_2745, q_gen_2746}, Q_f={}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2678 (q_gen_2678) -> q_gen_2734 () -> q_gen_2603 (q_gen_2603) -> q_gen_2617 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2649 (q_gen_2617) -> q_gen_2651 (q_gen_2622) -> q_gen_2671 (q_gen_2678) -> q_gen_2729 (q_gen_2671) -> q_gen_2739 (q_gen_2649) -> q_gen_2743 (q_gen_2651) -> q_gen_2746 () -> q_gen_2598 (q_gen_2603) -> q_gen_2602 (q_gen_2603) -> q_gen_2605 (q_gen_2611) -> q_gen_2610 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2617) -> q_gen_2616 (q_gen_2621) -> q_gen_2620 (q_gen_2622) -> q_gen_2621 (q_gen_2622) -> q_gen_2626 (q_gen_2628) -> q_gen_2627 (q_gen_2629) -> q_gen_2628 (q_gen_2617) -> q_gen_2633 (q_gen_2626) -> q_gen_2634 (q_gen_2615) -> q_gen_2637 (q_gen_2639) -> q_gen_2638 (q_gen_2602) -> q_gen_2639 (q_gen_2627) -> q_gen_2645 (q_gen_2649) -> q_gen_2648 (q_gen_2651) -> q_gen_2650 (q_gen_2654) -> q_gen_2653 (q_gen_2605) -> q_gen_2654 (q_gen_2656) -> q_gen_2655 (q_gen_2610) -> q_gen_2656 (q_gen_2633) -> q_gen_2660 (q_gen_2662) -> q_gen_2661 (q_gen_2651) -> q_gen_2662 (q_gen_2670) -> q_gen_2669 (q_gen_2671) -> q_gen_2670 (q_gen_2671) -> q_gen_2673 (q_gen_2649) -> q_gen_2675 (q_gen_2677) -> q_gen_2676 (q_gen_2678) -> q_gen_2677 (q_gen_2634) -> q_gen_2688 (q_gen_2645) -> q_gen_2689 (q_gen_2692) -> q_gen_2691 (q_gen_2675) -> q_gen_2692 (q_gen_2637) -> q_gen_2699 (q_gen_2638) -> q_gen_2700 (q_gen_2702) -> q_gen_2701 (q_gen_2676) -> q_gen_2702 (q_gen_2653) -> q_gen_2706 (q_gen_2655) -> q_gen_2707 (q_gen_2648) -> q_gen_2714 (q_gen_2722) -> q_gen_2721 (q_gen_2723) -> q_gen_2722 (q_gen_2616) -> q_gen_2723 (q_gen_2725) -> q_gen_2724 (q_gen_2688) -> q_gen_2725 (q_gen_2727) -> q_gen_2726 (q_gen_2714) -> q_gen_2727 (q_gen_2729) -> q_gen_2728 (q_gen_2729) -> q_gen_2731 (q_gen_2733) -> q_gen_2732 (q_gen_2734) -> q_gen_2733 (q_gen_2738) -> q_gen_2737 (q_gen_2739) -> q_gen_2738 (q_gen_2741) -> q_gen_2740 (q_gen_2742) -> q_gen_2741 (q_gen_2743) -> q_gen_2742 (q_gen_2746) -> q_gen_2745 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.004041 s (model generation: 0.003914, model checking: 0.000127): Model: |_ { minus -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 0 ; () -> minus([z, y, z]) -> 0 ; () -> plus([n, z, n]) -> 3 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 1 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 1 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 1 } Sat witness: Yes: (() -> plus([n, z, n]), { n -> z }) ------------------------------------------- Step 1, which took 0.004235 s (model generation: 0.003486, model checking: 0.000749): Model: |_ { minus -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2598 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 0 ; () -> minus([z, y, z]) -> 3 ; () -> plus([n, z, n]) -> 3 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 1 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 1 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 1 } Sat witness: Yes: (() -> minus([z, y, z]), { y -> z }) ------------------------------------------- Step 2, which took 0.003538 s (model generation: 0.003475, model checking: 0.000063): Model: |_ { minus -> {{{ Q={q_gen_2599}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2599 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2598 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 3 ; () -> minus([z, y, z]) -> 3 ; () -> plus([n, z, n]) -> 3 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 1 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 1 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 1 } Sat witness: Yes: (() -> minus([s(u), z, s(u)]), { u -> z }) ------------------------------------------- Step 3, which took 0.003572 s (model generation: 0.003511, model checking: 0.000061): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 () -> q_gen_2599 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2598 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 3 ; () -> minus([z, y, z]) -> 3 ; () -> plus([n, z, n]) -> 3 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 1 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 1 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 4 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> z ; mm -> z ; n -> z }) ------------------------------------------- Step 4, which took 0.003571 s (model generation: 0.003441, model checking: 0.000130): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 () -> q_gen_2599 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2603 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 3 ; () -> minus([z, y, z]) -> 3 ; () -> plus([n, z, n]) -> 3 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 1 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 4 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 4 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> z ; u -> z ; x2 -> z }) ------------------------------------------- Step 5, which took 0.004853 s (model generation: 0.004703, model checking: 0.000150): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 () -> q_gen_2599 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2603 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 3 ; () -> minus([z, y, z]) -> 3 ; () -> plus([n, z, n]) -> 6 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 2 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 4 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 4 } Sat witness: Yes: (() -> plus([n, z, n]), { n -> s(z) }) ------------------------------------------- Step 6, which took 0.011109 s (model generation: 0.007459, model checking: 0.003650): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 () -> q_gen_2599 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2603 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 3 ; () -> minus([z, y, z]) -> 6 ; () -> plus([n, z, n]) -> 6 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 3 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 4 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 4 } Sat witness: Yes: (() -> minus([z, y, z]), { y -> s(z) }) ------------------------------------------- Step 7, which took 0.009979 s (model generation: 0.009854, model checking: 0.000125): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2603 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 6 ; () -> minus([z, y, z]) -> 6 ; () -> plus([n, z, n]) -> 6 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 4 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 4 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 4 } Sat witness: Yes: (() -> minus([s(u), z, s(u)]), { u -> s(z) }) ------------------------------------------- Step 8, which took 0.009434 s (model generation: 0.009337, model checking: 0.000097): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2603 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 6 ; () -> minus([z, y, z]) -> 6 ; () -> plus([n, z, n]) -> 6 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 4 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 4 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 7 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(z) ; mm -> z ; n -> s(z) }) ------------------------------------------- Step 9, which took 0.008000 s (model generation: 0.007068, model checking: 0.000932): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2612}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 () -> q_gen_2603 (q_gen_2598) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2612) -> q_gen_2598 () -> q_gen_2598 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 6 ; () -> minus([z, y, z]) -> 6 ; () -> plus([n, z, n]) -> 6 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 4 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 7 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 7 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(z) ; u -> s(z) ; x2 -> z }) ------------------------------------------- Step 10, which took 0.008008 s (model generation: 0.007611, model checking: 0.000397): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2599) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2612}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 () -> q_gen_2603 (q_gen_2598) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2612) -> q_gen_2598 () -> q_gen_2598 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 6 ; () -> minus([z, y, z]) -> 6 ; () -> plus([n, z, n]) -> 6 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 7 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 7 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 7 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(z) ; _pc -> z ; m -> s(z) ; n -> s(z) }) ------------------------------------------- Step 11, which took 0.008933 s (model generation: 0.008846, model checking: 0.000087): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2599) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 () -> q_gen_2603 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2598) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 6 ; () -> minus([z, y, z]) -> 6 ; () -> plus([n, z, n]) -> 9 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 7 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 7 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 7 } Sat witness: Yes: (() -> plus([n, z, n]), { n -> s(s(z)) }) ------------------------------------------- Step 12, which took 0.009143 s (model generation: 0.008877, model checking: 0.000266): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2599) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2598) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 6 ; () -> minus([z, y, z]) -> 9 ; () -> plus([n, z, n]) -> 9 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 7 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 7 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 7 } Sat witness: Yes: (() -> minus([z, y, z]), { y -> s(s(z)) }) ------------------------------------------- Step 13, which took 0.012639 s (model generation: 0.011868, model checking: 0.000771): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607}, Q_f={q_gen_2599}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2599) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2598) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 7 ; () -> minus([z, y, z]) -> 9 ; () -> plus([n, z, n]) -> 9 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 7 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 7 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 10 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(z)) ; mm -> s(z) ; n -> s(z) }) ------------------------------------------- Step 14, which took 0.015695 s (model generation: 0.015263, model checking: 0.000432): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607}, Q_f={q_gen_2599}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2599) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2612, q_gen_2615}, Q_f={q_gen_2598, q_gen_2602}, Delta= { () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 (q_gen_2612) -> q_gen_2603 () -> q_gen_2603 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2612) -> q_gen_2602 (q_gen_2598) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 7 ; () -> minus([z, y, z]) -> 9 ; () -> plus([n, z, n]) -> 9 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 7 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 10 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 10 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> z ; u -> z ; x2 -> s(z) }) ------------------------------------------- Step 15, which took 0.018599 s (model generation: 0.016672, model checking: 0.001927): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607}, Q_f={q_gen_2599}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2599) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2612) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 7 ; () -> minus([z, y, z]) -> 9 ; () -> plus([n, z, n]) -> 9 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 10 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 10 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 10 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(z) ; _pc -> s(z) ; m -> z ; n -> s(z) }) ------------------------------------------- Step 16, which took 0.019145 s (model generation: 0.017380, model checking: 0.001765): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614}, Q_f={q_gen_2599}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2612, q_gen_2615}, Q_f={q_gen_2598, q_gen_2602}, Delta= { () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 (q_gen_2612) -> q_gen_2603 () -> q_gen_2603 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2612) -> q_gen_2602 (q_gen_2598) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 8 ; () -> minus([z, y, z]) -> 10 ; () -> plus([n, z, n]) -> 10 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 10 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 10 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 13 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(z)) ; mm -> z ; n -> s(z) }) ------------------------------------------- Step 17, which took 0.019847 s (model generation: 0.019468, model checking: 0.000379): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614}, Q_f={q_gen_2599}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2612, q_gen_2615}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 (q_gen_2612) -> q_gen_2603 () -> q_gen_2603 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2612) -> q_gen_2602 (q_gen_2598) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 9 ; () -> minus([z, y, z]) -> 10 ; () -> plus([n, z, n]) -> 10 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 10 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 13 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 13 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(z)) ; u -> s(z) ; x2 -> z }) ------------------------------------------- Step 18, which took 0.016340 s (model generation: 0.016070, model checking: 0.000270): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2625}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 () -> q_gen_2599 (q_gen_2600) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2607) -> q_gen_2600 (q_gen_2607) -> q_gen_2600 (q_gen_2599) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2612, q_gen_2615}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 (q_gen_2612) -> q_gen_2603 () -> q_gen_2603 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2612) -> q_gen_2602 (q_gen_2598) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 10 ; () -> minus([z, y, z]) -> 10 ; () -> plus([n, z, n]) -> 10 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 13 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 13 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 13 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(z)) ; _pc -> s(z) ; m -> z ; n -> s(s(z)) }) ------------------------------------------- Step 19, which took 0.016436 s (model generation: 0.015425, model checking: 0.001011): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2625}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 () -> q_gen_2599 (q_gen_2600) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2607) -> q_gen_2600 (q_gen_2607) -> q_gen_2600 (q_gen_2599) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2612, q_gen_2615}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 (q_gen_2612) -> q_gen_2603 () -> q_gen_2603 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2612) -> q_gen_2602 (q_gen_2598) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 11 ; () -> minus([z, y, z]) -> 11 ; () -> plus([n, z, n]) -> 11 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 13 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 13 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 16 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(z)) ; mm -> z ; n -> s(s(z)) }) ------------------------------------------- Step 20, which took 0.024150 s (model generation: 0.022971, model checking: 0.001179): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2625}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 () -> q_gen_2599 (q_gen_2600) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2607) -> q_gen_2600 (q_gen_2607) -> q_gen_2600 (q_gen_2599) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2612, q_gen_2615}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 (q_gen_2612) -> q_gen_2603 () -> q_gen_2603 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2612) -> q_gen_2602 (q_gen_2598) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 12 ; () -> minus([z, y, z]) -> 12 ; () -> plus([n, z, n]) -> 12 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 13 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 16 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 16 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(z) ; u -> s(z) ; x2 -> s(s(z)) }) ------------------------------------------- Step 21, which took 0.023806 s (model generation: 0.022962, model checking: 0.000844): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2614}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2600) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2614) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2599) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2612, q_gen_2615}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 (q_gen_2612) -> q_gen_2603 () -> q_gen_2603 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2612) -> q_gen_2602 (q_gen_2598) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 13 ; () -> minus([z, y, z]) -> 13 ; () -> plus([n, z, n]) -> 13 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 16 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 16 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 16 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(z) ; _pc -> s(z) ; m -> z ; n -> z }) ------------------------------------------- Step 22, which took 0.021456 s (model generation: 0.020451, model checking: 0.001005): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2614}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2600) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2614) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2599) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2611, q_gen_2612}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 (q_gen_2612) -> q_gen_2603 () -> q_gen_2603 (q_gen_2602) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2598) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 14 ; () -> minus([z, y, z]) -> 14 ; () -> plus([n, z, n]) -> 14 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 16 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 16 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 19 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(z)) ; mm -> s(s(z)) ; n -> s(s(z)) }) ------------------------------------------- Step 23, which took 0.020761 s (model generation: 0.019946, model checking: 0.000815): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2624}, Q_f={q_gen_2599}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2607) -> q_gen_2624 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2612) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 15 ; () -> minus([z, y, z]) -> 15 ; () -> plus([n, z, n]) -> 15 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 16 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 19 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 19 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(s(z)))) ; u -> s(s(z)) ; x2 -> s(z) }) ------------------------------------------- Step 24, which took 0.020309 s (model generation: 0.019789, model checking: 0.000520): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2625}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2600) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2607) -> q_gen_2600 (q_gen_2599) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2611, q_gen_2612}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 (q_gen_2612) -> q_gen_2603 () -> q_gen_2603 (q_gen_2611) -> q_gen_2598 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2598) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 16 ; () -> minus([z, y, z]) -> 16 ; () -> plus([n, z, n]) -> 16 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 19 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 19 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 19 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(z)) ; _pc -> s(z) ; m -> z ; n -> s(z) }) ------------------------------------------- Step 25, which took 0.019348 s (model generation: 0.018505, model checking: 0.000843): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2625}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2600) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2607) -> q_gen_2600 (q_gen_2599) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2612) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 17 ; () -> minus([z, y, z]) -> 17 ; () -> plus([n, z, n]) -> 17 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 19 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 19 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 22 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(z))) ; mm -> s(z) ; n -> s(s(z)) }) ------------------------------------------- Step 26, which took 0.024737 s (model generation: 0.023982, model checking: 0.000755): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2625}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2600) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2607) -> q_gen_2600 (q_gen_2599) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2612) -> q_gen_2622 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2611) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 18 ; () -> minus([z, y, z]) -> 18 ; () -> plus([n, z, n]) -> 18 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 19 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 22 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 22 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> z ; u -> s(z) ; x2 -> z }) ------------------------------------------- Step 27, which took 0.019172 s (model generation: 0.018884, model checking: 0.000288): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2625}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2600) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2607) -> q_gen_2600 (q_gen_2599) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2612) -> q_gen_2622 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2611) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 19 ; () -> minus([z, y, z]) -> 19 ; () -> plus([n, z, n]) -> 19 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 22 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 22 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 22 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(z) ; _pc -> z ; m -> s(z) ; n -> z }) ------------------------------------------- Step 28, which took 0.020663 s (model generation: 0.019566, model checking: 0.001097): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2614}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2600) -> q_gen_2600 (q_gen_2614) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2599) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2612) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2629) -> q_gen_2598 () -> q_gen_2598 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 20 ; () -> minus([z, y, z]) -> 20 ; () -> plus([n, z, n]) -> 20 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 22 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 22 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 25 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(z)) ; mm -> z ; n -> z }) ------------------------------------------- Step 29, which took 0.024634 s (model generation: 0.024522, model checking: 0.000112): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2614}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2600) -> q_gen_2600 (q_gen_2614) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2599) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2617}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 () -> q_gen_2603 (q_gen_2603) -> q_gen_2617 (q_gen_2612) -> q_gen_2617 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2611) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2617) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2598) -> q_gen_2611 (q_gen_2617) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 20 ; () -> minus([z, y, z]) -> 20 ; () -> plus([n, z, n]) -> 23 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 22 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 22 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 25 } Sat witness: Yes: (() -> plus([n, z, n]), { n -> s(s(s(z))) }) ------------------------------------------- Step 30, which took 0.021223 s (model generation: 0.020723, model checking: 0.000500): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2614}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2600) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2599) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2605, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598, q_gen_2605}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2612) -> q_gen_2622 (q_gen_2605) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2605 (q_gen_2603) -> q_gen_2605 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 21 ; () -> minus([z, y, z]) -> 21 ; () -> plus([n, z, n]) -> 23 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 22 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 25 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 25 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(z)) ; u -> s(s(z)) ; x2 -> s(z) }) ------------------------------------------- Step 31, which took 0.021313 s (model generation: 0.021000, model checking: 0.000313): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2614}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2600) -> q_gen_2600 (q_gen_2614) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2599) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2617}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 () -> q_gen_2603 (q_gen_2603) -> q_gen_2617 (q_gen_2617) -> q_gen_2617 (q_gen_2612) -> q_gen_2617 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2611) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2617) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2598) -> q_gen_2611 (q_gen_2617) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 22 ; () -> minus([z, y, z]) -> 22 ; () -> plus([n, z, n]) -> 23 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 25 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 25 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 25 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(z) ; _pc -> s(s(z)) ; m -> s(z) ; n -> z }) ------------------------------------------- Step 32, which took 0.022327 s (model generation: 0.021692, model checking: 0.000635): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2613, q_gen_2614, q_gen_2624}, Q_f={q_gen_2599, q_gen_2613}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2607) -> q_gen_2624 (q_gen_2613) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2614) -> q_gen_2613 (q_gen_2599) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2617}, Q_f={q_gen_2598, q_gen_2610}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 () -> q_gen_2603 (q_gen_2603) -> q_gen_2617 (q_gen_2617) -> q_gen_2617 (q_gen_2612) -> q_gen_2617 (q_gen_2610) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2610 (q_gen_2617) -> q_gen_2610 (q_gen_2598) -> q_gen_2611 (q_gen_2617) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 23 ; () -> minus([z, y, z]) -> 23 ; () -> plus([n, z, n]) -> 24 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 25 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 25 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 28 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(z))) ; mm -> s(s(z)) ; n -> s(s(s(z))) }) ------------------------------------------- Step 33, which took 0.023289 s (model generation: 0.022645, model checking: 0.000644): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2613, q_gen_2614, q_gen_2624}, Q_f={q_gen_2599, q_gen_2613}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 (q_gen_2607) -> q_gen_2601 () -> q_gen_2601 (q_gen_2607) -> q_gen_2624 (q_gen_2613) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2614) -> q_gen_2613 (q_gen_2599) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2605, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598, q_gen_2605}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2612) -> q_gen_2622 (q_gen_2605) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2605 (q_gen_2603) -> q_gen_2605 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 24 ; () -> minus([z, y, z]) -> 24 ; () -> plus([n, z, n]) -> 25 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 25 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 28 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 28 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(z) ; u -> s(s(z)) ; x2 -> s(z) }) ------------------------------------------- Step 34, which took 0.021297 s (model generation: 0.020788, model checking: 0.000509): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2606, q_gen_2607, q_gen_2614, q_gen_2624}, Q_f={q_gen_2599, q_gen_2606}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 () -> q_gen_2599 (q_gen_2606) -> q_gen_2606 (q_gen_2614) -> q_gen_2606 (q_gen_2624) -> q_gen_2606 (q_gen_2607) -> q_gen_2606 (q_gen_2599) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2605, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598, q_gen_2605}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2612) -> q_gen_2622 (q_gen_2605) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2605 (q_gen_2603) -> q_gen_2605 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 25 ; () -> minus([z, y, z]) -> 25 ; () -> plus([n, z, n]) -> 25 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 28 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 28 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 28 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(z)) ; _pc -> z ; m -> s(z) ; n -> s(z) }) ------------------------------------------- Step 35, which took 0.021482 s (model generation: 0.021010, model checking: 0.000472): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2642}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2642 (q_gen_2619) -> q_gen_2642 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2642) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2642) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2605, q_gen_2611, q_gen_2612, q_gen_2617}, Q_f={q_gen_2598, q_gen_2605}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 () -> q_gen_2603 (q_gen_2603) -> q_gen_2617 (q_gen_2617) -> q_gen_2617 (q_gen_2612) -> q_gen_2617 (q_gen_2605) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2605 (q_gen_2603) -> q_gen_2605 (q_gen_2617) -> q_gen_2605 (q_gen_2598) -> q_gen_2611 (q_gen_2617) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 25 ; () -> minus([z, y, z]) -> 28 ; () -> plus([n, z, n]) -> 26 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 28 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 28 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 28 } Sat witness: Yes: (() -> minus([z, y, z]), { y -> s(s(s(z))) }) ------------------------------------------- Step 36, which took 0.023837 s (model generation: 0.023197, model checking: 0.000640): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2624, q_gen_2625, q_gen_2647}, Q_f={q_gen_2599}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2625) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2599) -> q_gen_2625 (q_gen_2624) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2617}, Q_f={q_gen_2598, q_gen_2610}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2617) -> q_gen_2603 () -> q_gen_2603 (q_gen_2603) -> q_gen_2617 (q_gen_2612) -> q_gen_2617 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2617) -> q_gen_2610 (q_gen_2598) -> q_gen_2611 (q_gen_2617) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 26 ; () -> minus([z, y, z]) -> 28 ; () -> plus([n, z, n]) -> 27 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 28 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 28 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 31 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(z))) ; mm -> s(s(s(z))) ; n -> s(z) }) ------------------------------------------- Step 37, which took 0.026335 s (model generation: 0.026223, model checking: 0.000112): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2609, q_gen_2613, q_gen_2614, q_gen_2624}, Q_f={q_gen_2599, q_gen_2613}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 () -> q_gen_2601 (q_gen_2601) -> q_gen_2609 (q_gen_2607) -> q_gen_2609 (q_gen_2607) -> q_gen_2624 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2609) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2613) -> q_gen_2613 (q_gen_2614) -> q_gen_2613 (q_gen_2599) -> q_gen_2614 (q_gen_2609) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2605, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598, q_gen_2605}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2612) -> q_gen_2622 (q_gen_2605) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2605 (q_gen_2603) -> q_gen_2605 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 29 ; () -> minus([z, y, z]) -> 28 ; () -> plus([n, z, n]) -> 27 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 28 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 28 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 31 } Sat witness: Yes: (() -> minus([s(u), z, s(u)]), { u -> s(s(z)) }) ------------------------------------------- Step 38, which took 0.026326 s (model generation: 0.025964, model checking: 0.000362): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2606, q_gen_2607, q_gen_2614, q_gen_2624, q_gen_2647}, Q_f={q_gen_2599, q_gen_2606}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 () -> q_gen_2599 (q_gen_2606) -> q_gen_2606 (q_gen_2614) -> q_gen_2606 (q_gen_2624) -> q_gen_2606 (q_gen_2607) -> q_gen_2606 (q_gen_2599) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2605, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598, q_gen_2605}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2612) -> q_gen_2622 (q_gen_2605) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2605 (q_gen_2603) -> q_gen_2605 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 29 ; () -> minus([z, y, z]) -> 28 ; () -> plus([n, z, n]) -> 28 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 28 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 31 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 31 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> z ; u -> s(z) ; x2 -> s(s(z)) }) ------------------------------------------- Step 39, which took 0.026505 s (model generation: 0.026311, model checking: 0.000194): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2613, q_gen_2614, q_gen_2624, q_gen_2647}, Q_f={q_gen_2599, q_gen_2613}, Delta= { (q_gen_2607) -> q_gen_2607 () -> q_gen_2607 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 () -> q_gen_2599 (q_gen_2613) -> q_gen_2613 (q_gen_2614) -> q_gen_2613 (q_gen_2599) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2605, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598, q_gen_2605}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2612) -> q_gen_2622 (q_gen_2605) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2605 (q_gen_2603) -> q_gen_2605 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 29 ; () -> minus([z, y, z]) -> 28 ; () -> plus([n, z, n]) -> 28 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 31 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 31 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 31 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(z))) ; _pc -> s(z) ; m -> s(s(z)) ; n -> s(z) }) ------------------------------------------- Step 40, which took 0.026164 s (model generation: 0.025363, model checking: 0.000801): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2605, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598, q_gen_2605}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2612) -> q_gen_2622 (q_gen_2605) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2605 (q_gen_2603) -> q_gen_2605 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 30 ; () -> minus([z, y, z]) -> 29 ; () -> plus([n, z, n]) -> 29 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 31 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 31 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 34 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(z))) ; mm -> z ; n -> s(s(s(z))) }) ------------------------------------------- Step 41, which took 0.037394 s (model generation: 0.036842, model checking: 0.000552): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2642}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2642 (q_gen_2619) -> q_gen_2642 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2642) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2642) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2611) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 31 ; () -> minus([z, y, z]) -> 30 ; () -> plus([n, z, n]) -> 30 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 31 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 34 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 34 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> z ; u -> z ; x2 -> s(s(z)) }) ------------------------------------------- Step 42, which took 0.037010 s (model generation: 0.036593, model checking: 0.000417): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2609, q_gen_2614, q_gen_2619, q_gen_2624}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2601) -> q_gen_2609 (q_gen_2609) -> q_gen_2609 (q_gen_2607) -> q_gen_2609 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2609) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2609) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2617}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2617) -> q_gen_2603 () -> q_gen_2603 (q_gen_2603) -> q_gen_2617 (q_gen_2612) -> q_gen_2617 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2611) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2617) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2598) -> q_gen_2611 (q_gen_2617) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 31 ; () -> minus([z, y, z]) -> 31 ; () -> plus([n, z, n]) -> 31 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 34 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 34 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 34 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(z))) ; _pc -> s(z) ; m -> z ; n -> s(s(z)) }) ------------------------------------------- Step 43, which took 0.039362 s (model generation: 0.038309, model checking: 0.001053): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2609, q_gen_2614, q_gen_2619, q_gen_2624}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2601) -> q_gen_2609 (q_gen_2609) -> q_gen_2609 (q_gen_2607) -> q_gen_2609 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2609) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2609) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2611) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 32 ; () -> minus([z, y, z]) -> 32 ; () -> plus([n, z, n]) -> 32 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 34 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 37 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 35 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> z ; u -> s(z) ; x2 -> s(z) }) ------------------------------------------- Step 44, which took 0.038616 s (model generation: 0.038206, model checking: 0.000410): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2617}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 () -> q_gen_2603 (q_gen_2603) -> q_gen_2617 (q_gen_2617) -> q_gen_2617 (q_gen_2612) -> q_gen_2617 () -> q_gen_2598 (q_gen_2602) -> q_gen_2602 (q_gen_2611) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2617) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2598) -> q_gen_2611 (q_gen_2617) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 33 ; () -> minus([z, y, z]) -> 33 ; () -> plus([n, z, n]) -> 33 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 37 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 37 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 35 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(z)) ; _pc -> z ; m -> s(z) ; n -> s(s(z)) }) ------------------------------------------- Step 45, which took 0.039311 s (model generation: 0.038299, model checking: 0.001012): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 (q_gen_2629) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2629) -> q_gen_2598 () -> q_gen_2598 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 34 ; () -> minus([z, y, z]) -> 34 ; () -> plus([n, z, n]) -> 34 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 37 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 37 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 38 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(z))) ; mm -> z ; n -> s(z) }) ------------------------------------------- Step 46, which took 0.048391 s (model generation: 0.047590, model checking: 0.000801): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598}, Delta= { (q_gen_2629) -> q_gen_2612 () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 (q_gen_2629) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2629) -> q_gen_2598 () -> q_gen_2598 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 35 ; () -> minus([z, y, z]) -> 35 ; () -> plus([n, z, n]) -> 35 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 37 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 40 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 38 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> z ; u -> s(s(z)) ; x2 -> z }) ------------------------------------------- Step 47, which took 0.058975 s (model generation: 0.058204, model checking: 0.000771): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2617}, Q_f={q_gen_2598, q_gen_2610}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 () -> q_gen_2603 (q_gen_2603) -> q_gen_2617 (q_gen_2617) -> q_gen_2617 (q_gen_2612) -> q_gen_2617 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2617) -> q_gen_2610 (q_gen_2598) -> q_gen_2611 (q_gen_2617) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 36 ; () -> minus([z, y, z]) -> 36 ; () -> plus([n, z, n]) -> 36 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 40 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 40 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 38 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(z)) ; _pc -> z ; m -> s(z) ; n -> z }) ------------------------------------------- Step 48, which took 0.059275 s (model generation: 0.057989, model checking: 0.001286): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598}, Delta= { (q_gen_2629) -> q_gen_2612 () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 (q_gen_2629) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2629) -> q_gen_2598 () -> q_gen_2598 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 37 ; () -> minus([z, y, z]) -> 37 ; () -> plus([n, z, n]) -> 37 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 40 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 43 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 39 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(z)) ; u -> s(s(s(s(z)))) ; x2 -> s(z) }) ------------------------------------------- Step 49, which took 0.074189 s (model generation: 0.072944, model checking: 0.001245): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598}, Delta= { (q_gen_2629) -> q_gen_2612 () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 (q_gen_2629) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2629) -> q_gen_2598 () -> q_gen_2598 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 38 ; () -> minus([z, y, z]) -> 38 ; () -> plus([n, z, n]) -> 38 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 43 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 43 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 40 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(z)) ; _pc -> z ; m -> s(s(z)) ; n -> z }) ------------------------------------------- Step 50, which took 0.070643 s (model generation: 0.069263, model checking: 0.001380): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647, q_gen_2667}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2667) -> q_gen_2667 (q_gen_2619) -> q_gen_2667 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598}, Delta= { (q_gen_2629) -> q_gen_2612 () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 (q_gen_2629) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2629) -> q_gen_2598 () -> q_gen_2598 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 39 ; () -> minus([z, y, z]) -> 39 ; () -> plus([n, z, n]) -> 39 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 43 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 46 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 41 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(z)) ; u -> s(s(z)) ; x2 -> z }) ------------------------------------------- Step 51, which took 0.082248 s (model generation: 0.081148, model checking: 0.001100): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2624) -> q_gen_2601 () -> q_gen_2601 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2630) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2624) -> q_gen_2630 (q_gen_2619) -> q_gen_2630 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598}, Delta= { (q_gen_2629) -> q_gen_2612 () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 (q_gen_2629) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2629) -> q_gen_2598 () -> q_gen_2598 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 40 ; () -> minus([z, y, z]) -> 40 ; () -> plus([n, z, n]) -> 40 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 46 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 46 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 42 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(z)) ; _pc -> s(s(z)) ; m -> z ; n -> z }) ------------------------------------------- Step 52, which took 0.089743 s (model generation: 0.088841, model checking: 0.000902): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647, q_gen_2667}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2624) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2667) -> q_gen_2667 (q_gen_2619) -> q_gen_2667 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2605, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598, q_gen_2605}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2605) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2605 (q_gen_2603) -> q_gen_2605 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 41 ; () -> minus([z, y, z]) -> 41 ; () -> plus([n, z, n]) -> 41 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 46 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 46 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 45 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(s(z)))) ; mm -> s(s(z)) ; n -> s(s(s(z))) }) ------------------------------------------- Step 53, which took 0.136121 s (model generation: 0.135220, model checking: 0.000901): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2624) -> q_gen_2601 () -> q_gen_2601 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2630) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2624) -> q_gen_2630 (q_gen_2619) -> q_gen_2630 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2617}, Q_f={q_gen_2598, q_gen_2610}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 () -> q_gen_2603 (q_gen_2603) -> q_gen_2617 (q_gen_2617) -> q_gen_2617 (q_gen_2612) -> q_gen_2617 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2617) -> q_gen_2610 (q_gen_2598) -> q_gen_2611 (q_gen_2617) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 42 ; () -> minus([z, y, z]) -> 42 ; () -> plus([n, z, n]) -> 42 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 46 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 46 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 48 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(z) ; mm -> s(z) ; n -> z }) ------------------------------------------- Step 54, which took 0.089738 s (model generation: 0.089255, model checking: 0.000483): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2624) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2619) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2630) -> q_gen_2630 (q_gen_2624) -> q_gen_2630 (q_gen_2619) -> q_gen_2630 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598, q_gen_2610}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2622) -> q_gen_2610 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 43 ; () -> minus([z, y, z]) -> 43 ; () -> plus([n, z, n]) -> 43 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 46 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 49 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 48 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(z)) ; u -> s(s(s(z))) ; x2 -> s(z) }) ------------------------------------------- Step 55, which took 0.100651 s (model generation: 0.099823, model checking: 0.000828): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2630) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2624) -> q_gen_2630 (q_gen_2619) -> q_gen_2630 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2605, q_gen_2611, q_gen_2612, q_gen_2622}, Q_f={q_gen_2598, q_gen_2605}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2605) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2605 (q_gen_2603) -> q_gen_2605 (q_gen_2622) -> q_gen_2605 (q_gen_2598) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 44 ; () -> minus([z, y, z]) -> 44 ; () -> plus([n, z, n]) -> 44 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 49 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 49 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 48 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(z)) ; _pc -> z ; m -> s(s(z)) ; n -> s(s(z)) }) ------------------------------------------- Step 56, which took 0.094840 s (model generation: 0.094261, model checking: 0.000579): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2624) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2630) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2624) -> q_gen_2630 (q_gen_2619) -> q_gen_2630 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 45 ; () -> minus([z, y, z]) -> 45 ; () -> plus([n, z, n]) -> 45 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 49 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 49 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 51 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(s(z)))) ; mm -> s(z) ; n -> s(s(s(z))) }) ------------------------------------------- Step 57, which took 0.123430 s (model generation: 0.122680, model checking: 0.000750): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2624) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2619) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2630) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2624) -> q_gen_2630 (q_gen_2619) -> q_gen_2630 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622}, Q_f={q_gen_2598, q_gen_2610}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 46 ; () -> minus([z, y, z]) -> 46 ; () -> plus([n, z, n]) -> 46 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 49 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 52 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 51 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(z))) ; u -> s(s(z)) ; x2 -> z }) ------------------------------------------- Step 58, which took 0.112204 s (model generation: 0.111307, model checking: 0.000897): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2630) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2624) -> q_gen_2630 (q_gen_2619) -> q_gen_2630 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622}, Q_f={q_gen_2598, q_gen_2610}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2615) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 47 ; () -> minus([z, y, z]) -> 47 ; () -> plus([n, z, n]) -> 47 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 52 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 52 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 51 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(z))) ; _pc -> z ; m -> s(z) ; n -> s(z) }) ------------------------------------------- Step 59, which took 0.116087 s (model generation: 0.114594, model checking: 0.001493): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647, q_gen_2668}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622}, Q_f={q_gen_2598, q_gen_2610}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2615) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 48 ; () -> minus([z, y, z]) -> 48 ; () -> plus([n, z, n]) -> 48 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 52 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 55 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 52 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(s(z)))) ; u -> s(z) ; x2 -> z }) ------------------------------------------- Step 60, which took 0.122720 s (model generation: 0.121448, model checking: 0.001272): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2630) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2624) -> q_gen_2630 (q_gen_2619) -> q_gen_2630 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2605, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622}, Q_f={q_gen_2598, q_gen_2605}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2605) -> q_gen_2605 (q_gen_2611) -> q_gen_2605 (q_gen_2603) -> q_gen_2605 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2615) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 49 ; () -> minus([z, y, z]) -> 49 ; () -> plus([n, z, n]) -> 49 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 55 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 55 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 53 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(z)) ; _pc -> s(z) ; m -> s(s(z)) ; n -> s(z) }) ------------------------------------------- Step 61, which took 0.130458 s (model generation: 0.129443, model checking: 0.001015): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2630) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2624) -> q_gen_2630 (q_gen_2619) -> q_gen_2630 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622}, Q_f={q_gen_2598, q_gen_2610}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2615) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 50 ; () -> minus([z, y, z]) -> 50 ; () -> plus([n, z, n]) -> 50 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 55 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 58 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 54 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(s(z)))) ; u -> s(s(s(z))) ; x2 -> s(s(z)) }) ------------------------------------------- Step 62, which took 0.132982 s (model generation: 0.131855, model checking: 0.001127): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2625, q_gen_2647}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2625) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2599) -> q_gen_2625 (q_gen_2624) -> q_gen_2625 (q_gen_2619) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622}, Q_f={q_gen_2598, q_gen_2610}, Delta= { (q_gen_2612) -> q_gen_2612 () -> q_gen_2612 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2615) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 51 ; () -> minus([z, y, z]) -> 51 ; () -> plus([n, z, n]) -> 51 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 58 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 58 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 55 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(z))) ; _pc -> s(s(z)) ; m -> s(z) ; n -> s(z) }) ------------------------------------------- Step 63, which took 0.112338 s (model generation: 0.111489, model checking: 0.000849): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647, q_gen_2668}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2602}, Delta= { (q_gen_2629) -> q_gen_2612 () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 (q_gen_2629) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 () -> q_gen_2598 (q_gen_2611) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2602) -> q_gen_2611 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 52 ; () -> minus([z, y, z]) -> 52 ; () -> plus([n, z, n]) -> 52 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 58 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 58 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 58 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(z))) ; mm -> s(s(s(z))) ; n -> s(s(s(z))) }) ------------------------------------------- Step 64, which took 0.164079 s (model generation: 0.163155, model checking: 0.000924): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647, q_gen_2668}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629, q_gen_2649}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2649 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 53 ; () -> minus([z, y, z]) -> 53 ; () -> plus([n, z, n]) -> 53 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 58 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 58 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 61 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(s(s(z))))) ; mm -> s(s(z)) ; n -> s(s(s(z))) }) ------------------------------------------- Step 65, which took 0.173169 s (model generation: 0.171931, model checking: 0.001238): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647, q_gen_2668}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2605, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2605}, Delta= { (q_gen_2629) -> q_gen_2612 () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 (q_gen_2629) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2605 (q_gen_2603) -> q_gen_2605 (q_gen_2605) -> q_gen_2611 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 54 ; () -> minus([z, y, z]) -> 54 ; () -> plus([n, z, n]) -> 54 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 58 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 61 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 61 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(z) ; u -> s(s(s(z))) ; x2 -> s(s(z)) }) ------------------------------------------- Step 66, which took 0.160273 s (model generation: 0.159349, model checking: 0.000924): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647, q_gen_2668}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2605, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2605}, Delta= { (q_gen_2629) -> q_gen_2612 () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 (q_gen_2629) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2605 (q_gen_2603) -> q_gen_2605 (q_gen_2605) -> q_gen_2611 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 55 ; () -> minus([z, y, z]) -> 55 ; () -> plus([n, z, n]) -> 55 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 61 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 61 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 61 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(z) ; _pc -> s(s(s(z))) ; m -> s(z) ; n -> z }) ------------------------------------------- Step 67, which took 0.214821 s (model generation: 0.213963, model checking: 0.000858): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2625, q_gen_2647}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2625) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2599) -> q_gen_2625 (q_gen_2624) -> q_gen_2625 (q_gen_2619) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2610}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2610) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2610 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 56 ; () -> minus([z, y, z]) -> 56 ; () -> plus([n, z, n]) -> 56 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 61 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 61 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 64 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(s(z)))) ; mm -> s(s(s(z))) ; n -> s(s(s(s(z)))) }) ------------------------------------------- Step 68, which took 0.261613 s (model generation: 0.260875, model checking: 0.000738): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2625, q_gen_2647}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2625) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2599) -> q_gen_2625 (q_gen_2624) -> q_gen_2625 (q_gen_2619) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2610}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 57 ; () -> minus([z, y, z]) -> 57 ; () -> plus([n, z, n]) -> 57 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 61 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 64 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 64 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(z)) ; u -> s(s(s(s(z)))) ; x2 -> z }) ------------------------------------------- Step 69, which took 0.306196 s (model generation: 0.305398, model checking: 0.000798): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2625, q_gen_2647}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2619) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2625) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2599) -> q_gen_2625 (q_gen_2624) -> q_gen_2625 (q_gen_2619) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2610}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 58 ; () -> minus([z, y, z]) -> 58 ; () -> plus([n, z, n]) -> 58 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 64 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 64 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 64 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(s(z)))) ; _pc -> z ; m -> s(z) ; n -> s(s(z)) }) ------------------------------------------- Step 70, which took 0.257271 s (model generation: 0.256190, model checking: 0.001081): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2625, q_gen_2647}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2625) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2599) -> q_gen_2625 (q_gen_2624) -> q_gen_2625 (q_gen_2619) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2610}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 59 ; () -> minus([z, y, z]) -> 59 ; () -> plus([n, z, n]) -> 59 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 64 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 67 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 65 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(z))) ; u -> s(s(s(s(z)))) ; x2 -> s(z) }) ------------------------------------------- Step 71, which took 0.224674 s (model generation: 0.224103, model checking: 0.000571): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2625, q_gen_2647}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2625) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2599) -> q_gen_2625 (q_gen_2624) -> q_gen_2625 (q_gen_2619) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2605, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2605}, Delta= { (q_gen_2629) -> q_gen_2612 () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 (q_gen_2629) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2605 (q_gen_2603) -> q_gen_2605 (q_gen_2605) -> q_gen_2611 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 60 ; () -> minus([z, y, z]) -> 60 ; () -> plus([n, z, n]) -> 60 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 67 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 67 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 65 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(z))) ; _pc -> z ; m -> s(s(z)) ; n -> s(z) }) ------------------------------------------- Step 72, which took 0.331301 s (model generation: 0.330215, model checking: 0.001086): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647, q_gen_2668}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2600) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2614) -> q_gen_2600 (q_gen_2624) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2610}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 61 ; () -> minus([z, y, z]) -> 61 ; () -> plus([n, z, n]) -> 61 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 67 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 70 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 66 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(z)) ; u -> s(s(z)) ; x2 -> s(s(s(z))) }) ------------------------------------------- Step 73, which took 0.289656 s (model generation: 0.288525, model checking: 0.001131): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2623, q_gen_2624, q_gen_2625, q_gen_2647}, Q_f={q_gen_2599, q_gen_2623}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2625) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2623) -> q_gen_2623 (q_gen_2624) -> q_gen_2623 (q_gen_2647) -> q_gen_2623 (q_gen_2599) -> q_gen_2625 (q_gen_2624) -> q_gen_2625 (q_gen_2619) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2610}, Delta= { (q_gen_2629) -> q_gen_2612 () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 62 ; () -> minus([z, y, z]) -> 62 ; () -> plus([n, z, n]) -> 62 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 70 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 70 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 67 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(s(z)))) ; _pc -> s(s(z)) ; m -> s(z) ; n -> s(z) }) ------------------------------------------- Step 74, which took 0.378585 s (model generation: 0.377556, model checking: 0.001029): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647, q_gen_2668}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2601) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2600) -> q_gen_2600 (q_gen_2614) -> q_gen_2600 (q_gen_2624) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2647) -> q_gen_2600 (q_gen_2607) -> q_gen_2600 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2610}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 63 ; () -> minus([z, y, z]) -> 63 ; () -> plus([n, z, n]) -> 63 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 70 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 73 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 68 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(z) ; u -> s(s(z)) ; x2 -> z }) ------------------------------------------- Step 75, which took 0.380614 s (model generation: 0.379349, model checking: 0.001265): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2600, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647}, Q_f={q_gen_2599, q_gen_2600}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2601) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2600) -> q_gen_2600 (q_gen_2614) -> q_gen_2600 (q_gen_2624) -> q_gen_2600 (q_gen_2601) -> q_gen_2600 (q_gen_2607) -> q_gen_2600 (q_gen_2599) -> q_gen_2614 (q_gen_2630) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2624) -> q_gen_2630 (q_gen_2619) -> q_gen_2630 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2610}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 64 ; () -> minus([z, y, z]) -> 64 ; () -> plus([n, z, n]) -> 64 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 73 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 73 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 69 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(z)) ; _pc -> s(s(z)) ; m -> s(z) ; n -> s(z) }) ------------------------------------------- Step 76, which took 0.448855 s (model generation: 0.447836, model checking: 0.001019): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2613, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647}, Q_f={q_gen_2599, q_gen_2613}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2613) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2614) -> q_gen_2613 (q_gen_2599) -> q_gen_2614 (q_gen_2630) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2624) -> q_gen_2630 (q_gen_2619) -> q_gen_2630 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2610}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 65 ; () -> minus([z, y, z]) -> 65 ; () -> plus([n, z, n]) -> 65 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 73 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 76 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 70 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(z))) ; u -> s(s(s(z))) ; x2 -> s(s(z)) }) ------------------------------------------- Step 77, which took 0.446788 s (model generation: 0.445596, model checking: 0.001192): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2613, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647}, Q_f={q_gen_2599, q_gen_2613}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2613) -> q_gen_2613 (q_gen_2614) -> q_gen_2613 (q_gen_2599) -> q_gen_2614 (q_gen_2630) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2624) -> q_gen_2630 (q_gen_2619) -> q_gen_2630 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2610}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2610 (q_gen_2611) -> q_gen_2610 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 66 ; () -> minus([z, y, z]) -> 66 ; () -> plus([n, z, n]) -> 66 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 76 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 76 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 71 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(s(z)))) ; _pc -> s(z) ; m -> s(s(s(z))) ; n -> s(s(s(z))) }) ------------------------------------------- Step 78, which took 0.733457 s (model generation: 0.732820, model checking: 0.000637): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2606, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2647, q_gen_2668}, Q_f={q_gen_2599, q_gen_2606}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2606) -> q_gen_2606 (q_gen_2614) -> q_gen_2606 (q_gen_2624) -> q_gen_2606 (q_gen_2607) -> q_gen_2606 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2620, q_gen_2621, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2620}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2620) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 (q_gen_2621) -> q_gen_2620 (q_gen_2615) -> q_gen_2621 (q_gen_2622) -> q_gen_2621 (q_gen_2622) -> q_gen_2621 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 67 ; () -> minus([z, y, z]) -> 67 ; () -> plus([n, z, n]) -> 67 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 76 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 76 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 74 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(s(s(z))))) ; mm -> s(s(s(z))) ; n -> s(s(s(s(s(z))))) }) ------------------------------------------- Step 79, which took 1.021039 s (model generation: 1.019099, model checking: 0.001940): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2606, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647}, Q_f={q_gen_2599, q_gen_2606}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2606) -> q_gen_2606 (q_gen_2614) -> q_gen_2606 (q_gen_2624) -> q_gen_2606 (q_gen_2607) -> q_gen_2606 (q_gen_2599) -> q_gen_2614 (q_gen_2630) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2624) -> q_gen_2630 (q_gen_2619) -> q_gen_2630 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2620, q_gen_2621, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2620}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 (q_gen_2620) -> q_gen_2620 (q_gen_2621) -> q_gen_2620 (q_gen_2615) -> q_gen_2621 (q_gen_2622) -> q_gen_2621 (q_gen_2622) -> q_gen_2621 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 68 ; () -> minus([z, y, z]) -> 68 ; () -> plus([n, z, n]) -> 68 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 79 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 77 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 75 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(z))) ; _pc -> s(s(z)) ; m -> s(z) ; n -> s(s(z)) }) ------------------------------------------- Step 80, which took 0.492323 s (model generation: 0.491427, model checking: 0.000896): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2625, q_gen_2647, q_gen_2680}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2680) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2647) -> q_gen_2680 (q_gen_2619) -> q_gen_2680 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2680) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2625) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2680) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2599) -> q_gen_2625 (q_gen_2624) -> q_gen_2625 (q_gen_2619) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2628, q_gen_2629}, Q_f={q_gen_2598, q_gen_2610}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2610) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2611) -> q_gen_2610 (q_gen_2628) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2615) -> q_gen_2615 (q_gen_2629) -> q_gen_2628 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 69 ; () -> minus([z, y, z]) -> 69 ; () -> plus([n, z, n]) -> 69 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 79 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 77 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 78 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(s(s(z))))) ; mm -> s(s(s(z))) ; n -> s(s(s(z))) }) ------------------------------------------- Step 81, which took 0.743488 s (model generation: 0.742743, model checking: 0.000745): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2625, q_gen_2647, q_gen_2680}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2680) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2607) -> q_gen_2647 (q_gen_2647) -> q_gen_2680 (q_gen_2619) -> q_gen_2680 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2680) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2625) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2680) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2599) -> q_gen_2625 (q_gen_2624) -> q_gen_2625 (q_gen_2619) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629, q_gen_2649, q_gen_2678}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2678 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2649 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2678) -> q_gen_2598 () -> q_gen_2598 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 70 ; () -> minus([z, y, z]) -> 70 ; () -> plus([n, z, n]) -> 70 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 79 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 80 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 78 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(z)) ; u -> s(s(s(z))) ; x2 -> z }) ------------------------------------------- Step 82, which took 0.837158 s (model generation: 0.835372, model checking: 0.001786): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2625, q_gen_2647, q_gen_2680}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2680) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2647) -> q_gen_2680 (q_gen_2619) -> q_gen_2680 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2625) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2680) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2599) -> q_gen_2625 (q_gen_2624) -> q_gen_2625 (q_gen_2680) -> q_gen_2625 (q_gen_2619) -> q_gen_2625 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2620, q_gen_2621, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2620}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 (q_gen_2620) -> q_gen_2620 (q_gen_2621) -> q_gen_2620 (q_gen_2615) -> q_gen_2621 (q_gen_2622) -> q_gen_2621 (q_gen_2622) -> q_gen_2621 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 71 ; () -> minus([z, y, z]) -> 71 ; () -> plus([n, z, n]) -> 71 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 82 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 80 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 79 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(z))) ; _pc -> s(s(s(s(z)))) ; m -> s(z) ; n -> s(s(z)) }) ------------------------------------------- Step 83, which took 0.913620 s (model generation: 0.912403, model checking: 0.001217): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647, q_gen_2668, q_gen_2680}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2680) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2647) -> q_gen_2680 (q_gen_2619) -> q_gen_2680 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2680) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2630) -> q_gen_2630 (q_gen_2624) -> q_gen_2630 (q_gen_2680) -> q_gen_2630 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2620, q_gen_2621, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2620}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 (q_gen_2620) -> q_gen_2620 (q_gen_2621) -> q_gen_2620 (q_gen_2615) -> q_gen_2621 (q_gen_2622) -> q_gen_2621 (q_gen_2622) -> q_gen_2621 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 72 ; () -> minus([z, y, z]) -> 72 ; () -> plus([n, z, n]) -> 72 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 82 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 83 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 80 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(z))) ; u -> s(s(s(z))) ; x2 -> z }) ------------------------------------------- Step 84, which took 1.343547 s (model generation: 1.342625, model checking: 0.000922): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647, q_gen_2668, q_gen_2680}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2680) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2680 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2680) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2680) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2630) -> q_gen_2630 (q_gen_2624) -> q_gen_2630 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629, q_gen_2649, q_gen_2678}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2678 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2649 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2649) -> q_gen_2598 (q_gen_2678) -> q_gen_2598 () -> q_gen_2598 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 73 ; () -> minus([z, y, z]) -> 73 ; () -> plus([n, z, n]) -> 73 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 82 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 83 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 83 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(s(z)))) ; mm -> s(s(z)) ; n -> s(s(z)) }) ------------------------------------------- Step 85, which took 0.850430 s (model generation: 0.849352, model checking: 0.001078): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647, q_gen_2668, q_gen_2680}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 (q_gen_2680) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2680 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2680) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2630) -> q_gen_2630 (q_gen_2624) -> q_gen_2630 (q_gen_2680) -> q_gen_2668 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629, q_gen_2649, q_gen_2678}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2678 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2649 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2678) -> q_gen_2598 () -> q_gen_2598 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 74 ; () -> minus([z, y, z]) -> 74 ; () -> plus([n, z, n]) -> 74 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 85 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 83 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 83 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(s(z)))) ; _pc -> z ; m -> s(s(z)) ; n -> s(s(z)) }) ------------------------------------------- Step 86, which took 1.047290 s (model generation: 1.045940, model checking: 0.001350): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647, q_gen_2668, q_gen_2680}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2680) -> q_gen_2680 (q_gen_2619) -> q_gen_2680 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2680) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2630) -> q_gen_2630 (q_gen_2624) -> q_gen_2630 (q_gen_2680) -> q_gen_2668 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629, q_gen_2649, q_gen_2678}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2678 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2649 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2678) -> q_gen_2598 () -> q_gen_2598 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 75 ; () -> minus([z, y, z]) -> 75 ; () -> plus([n, z, n]) -> 75 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 85 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 83 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 86 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(z))) ; mm -> z ; n -> z }) ------------------------------------------- Step 87, which took 1.221926 s (model generation: 1.220676, model checking: 0.001250): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647, q_gen_2668, q_gen_2680}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2680) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2680 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2680) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2630) -> q_gen_2630 (q_gen_2624) -> q_gen_2630 (q_gen_2680) -> q_gen_2668 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629, q_gen_2649, q_gen_2678}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2678 (q_gen_2603) -> q_gen_2603 (q_gen_2678) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2649 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2678) -> q_gen_2598 () -> q_gen_2598 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 76 ; () -> minus([z, y, z]) -> 76 ; () -> plus([n, z, n]) -> 76 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 85 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 86 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 86 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(z) ; u -> s(s(s(z))) ; x2 -> z }) ------------------------------------------- Step 88, which took 1.214486 s (model generation: 1.212939, model checking: 0.001547): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647, q_gen_2668, q_gen_2680}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2680) -> q_gen_2680 (q_gen_2619) -> q_gen_2680 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2680) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2630) -> q_gen_2630 (q_gen_2624) -> q_gen_2630 (q_gen_2680) -> q_gen_2668 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2620, q_gen_2621, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2620}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 (q_gen_2620) -> q_gen_2620 (q_gen_2621) -> q_gen_2620 (q_gen_2615) -> q_gen_2621 (q_gen_2622) -> q_gen_2621 (q_gen_2622) -> q_gen_2621 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 77 ; () -> minus([z, y, z]) -> 77 ; () -> plus([n, z, n]) -> 77 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 88 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 86 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 86 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(s(z)))) ; _pc -> s(z) ; m -> s(s(z)) ; n -> s(z) }) ------------------------------------------- Step 89, which took 1.164547 s (model generation: 1.162866, model checking: 0.001681): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647, q_gen_2668, q_gen_2680}, Q_f={q_gen_2599}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2680) -> q_gen_2680 (q_gen_2619) -> q_gen_2680 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2630) -> q_gen_2630 (q_gen_2624) -> q_gen_2630 (q_gen_2680) -> q_gen_2668 (q_gen_2680) -> q_gen_2668 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2620, q_gen_2621, q_gen_2622, q_gen_2629}, Q_f={q_gen_2598, q_gen_2620}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2622 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 (q_gen_2620) -> q_gen_2620 (q_gen_2621) -> q_gen_2620 (q_gen_2615) -> q_gen_2621 (q_gen_2622) -> q_gen_2621 (q_gen_2622) -> q_gen_2621 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 78 ; () -> minus([z, y, z]) -> 78 ; () -> plus([n, z, n]) -> 78 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 88 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 89 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 87 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(z))) ; u -> s(s(s(s(s(z))))) ; x2 -> s(s(z)) }) ------------------------------------------- Step 90, which took 1.139603 s (model generation: 1.138233, model checking: 0.001370): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647, q_gen_2668, q_gen_2680}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2680) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2680 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2680) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2630) -> q_gen_2630 (q_gen_2624) -> q_gen_2630 (q_gen_2680) -> q_gen_2668 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629, q_gen_2649, q_gen_2678}, Q_f={q_gen_2598}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2678 (q_gen_2603) -> q_gen_2603 (q_gen_2678) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2649 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2678) -> q_gen_2598 () -> q_gen_2598 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 79 ; () -> minus([z, y, z]) -> 79 ; () -> plus([n, z, n]) -> 79 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 88 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 89 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 90 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(s(z)))) ; mm -> z ; n -> s(z) }) ------------------------------------------- Step 91, which took 1.668064 s (model generation: 1.667198, model checking: 0.000866): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647, q_gen_2668, q_gen_2680}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2680) -> q_gen_2680 (q_gen_2619) -> q_gen_2680 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2680) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2630) -> q_gen_2630 (q_gen_2624) -> q_gen_2630 (q_gen_2680) -> q_gen_2668 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629, q_gen_2649, q_gen_2678}, Q_f={q_gen_2598}, Delta= { (q_gen_2678) -> q_gen_2612 () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2678 (q_gen_2603) -> q_gen_2603 (q_gen_2678) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2649 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2678) -> q_gen_2598 () -> q_gen_2598 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 80 ; () -> minus([z, y, z]) -> 80 ; () -> plus([n, z, n]) -> 80 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 91 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 89 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 90 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(s(z)))) ; _pc -> s(z) ; m -> z ; n -> s(z) }) ------------------------------------------- Step 92, which took 2.587208 s (model generation: 2.586133, model checking: 0.001075): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2623, q_gen_2624, q_gen_2625, q_gen_2641, q_gen_2642, q_gen_2647}, Q_f={q_gen_2599, q_gen_2623}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2642 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2642) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2647) -> q_gen_2614 (q_gen_2624) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2623) -> q_gen_2623 (q_gen_2625) -> q_gen_2623 (q_gen_2624) -> q_gen_2623 (q_gen_2599) -> q_gen_2625 (q_gen_2641) -> q_gen_2625 (q_gen_2647) -> q_gen_2625 (q_gen_2642) -> q_gen_2641 (q_gen_2619) -> q_gen_2641 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629, q_gen_2649, q_gen_2678}, Q_f={q_gen_2598}, Delta= { (q_gen_2678) -> q_gen_2612 () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2678 (q_gen_2603) -> q_gen_2603 (q_gen_2678) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2649 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2678) -> q_gen_2598 () -> q_gen_2598 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 81 ; () -> minus([z, y, z]) -> 81 ; () -> plus([n, z, n]) -> 81 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 91 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 92 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 90 } Sat witness: Yes: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(z)) ; u -> s(s(s(s(z)))) ; x2 -> s(s(z)) }) ------------------------------------------- Step 93, which took 1.558021 s (model generation: 1.556916, model checking: 0.001105): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2647, q_gen_2668, q_gen_2680}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2680) -> q_gen_2680 (q_gen_2619) -> q_gen_2680 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2680) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2668) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2630) -> q_gen_2630 (q_gen_2624) -> q_gen_2630 (q_gen_2680) -> q_gen_2668 (q_gen_2619) -> q_gen_2668 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629, q_gen_2649}, Q_f={q_gen_2598, q_gen_2602, q_gen_2610}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2629) -> q_gen_2649 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2611) -> q_gen_2610 (q_gen_2602) -> q_gen_2611 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 82 ; () -> minus([z, y, z]) -> 82 ; () -> plus([n, z, n]) -> 82 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 91 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 92 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 93 } Sat witness: Yes: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(s(s(z))))) ; mm -> s(z) ; n -> s(s(s(s(z)))) }) ------------------------------------------- Step 94, which took 2.337840 s (model generation: 2.337001, model checking: 0.000839): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2624, q_gen_2630, q_gen_2640, q_gen_2647, q_gen_2680}, Q_f={q_gen_2599}, Delta= { (q_gen_2619) -> q_gen_2607 () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2680) -> q_gen_2680 (q_gen_2619) -> q_gen_2680 (q_gen_2614) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2624) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2680) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2640) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2647) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2624) -> q_gen_2630 (q_gen_2630) -> q_gen_2640 (q_gen_2680) -> q_gen_2640 (q_gen_2619) -> q_gen_2640 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2602, q_gen_2603, q_gen_2610, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2622, q_gen_2629, q_gen_2649}, Q_f={q_gen_2598, q_gen_2602, q_gen_2610}, Delta= { () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2629 (q_gen_2603) -> q_gen_2603 () -> q_gen_2603 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2649) -> q_gen_2649 (q_gen_2629) -> q_gen_2649 (q_gen_2603) -> q_gen_2598 () -> q_gen_2598 (q_gen_2610) -> q_gen_2602 (q_gen_2603) -> q_gen_2602 (q_gen_2611) -> q_gen_2610 (q_gen_2602) -> q_gen_2611 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 83 ; () -> minus([z, y, z]) -> 83 ; () -> plus([n, z, n]) -> 83 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 94 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 92 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 93 } Sat witness: Yes: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(z))) ; _pc -> z ; m -> s(s(z)) ; n -> s(s(s(z))) }) ------------------------------------------- Step 95, which took 2.009433 s (model generation: 2.009240, model checking: 0.000193): Model: |_ { minus -> {{{ Q={q_gen_2599, q_gen_2601, q_gen_2607, q_gen_2614, q_gen_2619, q_gen_2623, q_gen_2624, q_gen_2630, q_gen_2636, q_gen_2640, q_gen_2643, q_gen_2647}, Q_f={q_gen_2599, q_gen_2623, q_gen_2636}, Delta= { () -> q_gen_2607 (q_gen_2607) -> q_gen_2619 (q_gen_2619) -> q_gen_2619 (q_gen_2601) -> q_gen_2601 () -> q_gen_2601 (q_gen_2624) -> q_gen_2624 (q_gen_2607) -> q_gen_2624 (q_gen_2619) -> q_gen_2624 (q_gen_2647) -> q_gen_2647 (q_gen_2607) -> q_gen_2647 (q_gen_2619) -> q_gen_2647 (q_gen_2614) -> q_gen_2599 (q_gen_2636) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2601) -> q_gen_2599 (q_gen_2607) -> q_gen_2599 (q_gen_2619) -> q_gen_2599 () -> q_gen_2599 (q_gen_2599) -> q_gen_2614 (q_gen_2607) -> q_gen_2614 (q_gen_2624) -> q_gen_2623 (q_gen_2624) -> q_gen_2630 (q_gen_2623) -> q_gen_2636 (q_gen_2643) -> q_gen_2636 (q_gen_2630) -> q_gen_2640 (q_gen_2619) -> q_gen_2640 (q_gen_2640) -> q_gen_2643 (q_gen_2647) -> q_gen_2643 (q_gen_2647) -> q_gen_2643 } Datatype: Convolution form: complete }}} ; plus -> {{{ Q={q_gen_2598, q_gen_2603, q_gen_2611, q_gen_2612, q_gen_2615, q_gen_2617, q_gen_2622, q_gen_2629, q_gen_2649, q_gen_2651, q_gen_2678}, Q_f={q_gen_2598}, Delta= { (q_gen_2678) -> q_gen_2612 () -> q_gen_2612 (q_gen_2612) -> q_gen_2629 (q_gen_2629) -> q_gen_2678 () -> q_gen_2603 (q_gen_2603) -> q_gen_2617 (q_gen_2622) -> q_gen_2622 (q_gen_2612) -> q_gen_2622 (q_gen_2649) -> q_gen_2649 (q_gen_2629) -> q_gen_2649 (q_gen_2617) -> q_gen_2651 (q_gen_2678) -> q_gen_2651 (q_gen_2611) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2617) -> q_gen_2598 (q_gen_2651) -> q_gen_2598 (q_gen_2603) -> q_gen_2598 (q_gen_2617) -> q_gen_2598 (q_gen_2651) -> q_gen_2598 (q_gen_2678) -> q_gen_2598 () -> q_gen_2598 (q_gen_2615) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2622) -> q_gen_2611 (q_gen_2612) -> q_gen_2611 (q_gen_2598) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2649) -> q_gen_2615 (q_gen_2629) -> q_gen_2615 } Datatype: Convolution form: complete }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 83 ; () -> minus([z, y, z]) -> 83 ; () -> plus([n, z, n]) -> 86 ; (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 94 ; (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 92 ; (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 93 } Sat witness: Yes: (() -> plus([n, z, n]), { n -> s(s(s(s(z)))) }) Total time: 30.568983 Reason for stopping: DontKnow. Stopped because: timeout