Inference procedure has parameters: Ice fuel: 200 Timeout: 60s Convolution: right 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 67.309641 seconds. DontKnow. Stopped because: timeout Working model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_554, q_gen_557, q_gen_558, q_gen_559, q_gen_560, q_gen_565, q_gen_566, q_gen_568, q_gen_569, q_gen_573, q_gen_574, q_gen_575, q_gen_580, q_gen_581, q_gen_584, q_gen_585, q_gen_586, q_gen_587, q_gen_588, q_gen_591, q_gen_592, q_gen_593, q_gen_594, q_gen_596, q_gen_597, q_gen_598, q_gen_599, q_gen_600, q_gen_604, q_gen_605, q_gen_606, q_gen_607, q_gen_608, q_gen_613, q_gen_614, q_gen_615, q_gen_616, q_gen_617, q_gen_622, q_gen_623, q_gen_624, q_gen_625, q_gen_626, q_gen_633, q_gen_634, q_gen_635, q_gen_638, q_gen_639, q_gen_640, q_gen_644, q_gen_645, q_gen_646, q_gen_647, q_gen_648, q_gen_649, q_gen_650, q_gen_651, q_gen_652, q_gen_662, q_gen_663, q_gen_667, q_gen_668, q_gen_669, q_gen_670, q_gen_673, q_gen_674, q_gen_675, q_gen_676, q_gen_681, q_gen_682, q_gen_689, q_gen_690, q_gen_691, q_gen_692, q_gen_693, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698}, Q_f={}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_594 () -> q_gen_551 (q_gen_551) -> q_gen_560 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_586 (q_gen_594) -> q_gen_597 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_614 (q_gen_560) -> q_gen_616 (q_gen_600) -> q_gen_669 (q_gen_574) -> q_gen_692 (q_gen_698) -> q_gen_697 (q_gen_614) -> q_gen_698 () -> q_gen_549 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_554 (q_gen_558) -> q_gen_557 (q_gen_560) -> q_gen_559 (q_gen_566) -> q_gen_565 (q_gen_558) -> q_gen_566 (q_gen_569) -> q_gen_568 (q_gen_574) -> q_gen_573 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_580 (q_gen_550) -> q_gen_581 (q_gen_585) -> q_gen_584 (q_gen_586) -> q_gen_585 (q_gen_588) -> q_gen_587 (q_gen_580) -> q_gen_588 (q_gen_557) -> q_gen_591 (q_gen_573) -> q_gen_592 (q_gen_594) -> q_gen_593 (q_gen_597) -> q_gen_596 (q_gen_599) -> q_gen_598 (q_gen_600) -> q_gen_599 (q_gen_581) -> q_gen_604 (q_gen_606) -> q_gen_605 (q_gen_565) -> q_gen_606 (q_gen_608) -> q_gen_607 (q_gen_569) -> q_gen_608 (q_gen_614) -> q_gen_613 (q_gen_616) -> q_gen_615 (q_gen_560) -> q_gen_617 (q_gen_623) -> q_gen_622 (q_gen_614) -> q_gen_623 (q_gen_625) -> q_gen_624 (q_gen_626) -> q_gen_625 (q_gen_594) -> q_gen_626 (q_gen_634) -> q_gen_633 (q_gen_600) -> q_gen_634 (q_gen_575) -> q_gen_635 (q_gen_607) -> q_gen_638 (q_gen_640) -> q_gen_639 (q_gen_613) -> q_gen_640 (q_gen_596) -> q_gen_644 (q_gen_584) -> q_gen_645 (q_gen_647) -> q_gen_646 (q_gen_648) -> q_gen_647 (q_gen_568) -> q_gen_648 (q_gen_650) -> q_gen_649 (q_gen_651) -> q_gen_650 (q_gen_652) -> q_gen_651 (q_gen_586) -> q_gen_652 (q_gen_587) -> q_gen_662 (q_gen_616) -> q_gen_663 (q_gen_668) -> q_gen_667 (q_gen_669) -> q_gen_668 (q_gen_669) -> q_gen_670 (q_gen_635) -> q_gen_673 (q_gen_675) -> q_gen_674 (q_gen_676) -> q_gen_675 (q_gen_554) -> q_gen_676 (q_gen_604) -> q_gen_681 (q_gen_605) -> q_gen_682 (q_gen_638) -> q_gen_689 (q_gen_639) -> q_gen_690 (q_gen_692) -> q_gen_691 (q_gen_622) -> q_gen_693 (q_gen_624) -> q_gen_694 (q_gen_696) -> q_gen_695 (q_gen_697) -> q_gen_696 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_555, q_gen_556, q_gen_561, q_gen_562, q_gen_563, q_gen_564, q_gen_567, q_gen_570, q_gen_571, q_gen_572, q_gen_576, q_gen_577, q_gen_578, q_gen_579, q_gen_582, q_gen_583, q_gen_589, q_gen_590, q_gen_595, q_gen_601, q_gen_602, q_gen_603, q_gen_609, q_gen_610, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621, q_gen_627, q_gen_628, q_gen_629, q_gen_630, q_gen_631, q_gen_632, q_gen_636, q_gen_637, q_gen_641, q_gen_642, q_gen_643, q_gen_653, q_gen_654, q_gen_655, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_660, q_gen_661, q_gen_664, q_gen_665, q_gen_666, q_gen_671, q_gen_672, q_gen_677, q_gen_678, q_gen_679, q_gen_680, q_gen_683, q_gen_684, q_gen_685, q_gen_686, q_gen_687, q_gen_688, q_gen_699, q_gen_700, q_gen_701, q_gen_702, q_gen_703, q_gen_704, q_gen_705, q_gen_706}, Q_f={}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_660 (q_gen_660) -> q_gen_680 () -> q_gen_553 (q_gen_553) -> q_gen_556 (q_gen_564) -> q_gen_572 (q_gen_556) -> q_gen_583 (q_gen_572) -> q_gen_620 (q_gen_579) -> q_gen_632 (q_gen_632) -> q_gen_656 (q_gen_660) -> q_gen_672 () -> q_gen_548 (q_gen_553) -> q_gen_552 (q_gen_556) -> q_gen_555 (q_gen_553) -> q_gen_561 (q_gen_563) -> q_gen_562 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_571) -> q_gen_570 (q_gen_572) -> q_gen_571 (q_gen_572) -> q_gen_576 (q_gen_578) -> q_gen_577 (q_gen_579) -> q_gen_578 (q_gen_583) -> q_gen_582 (q_gen_576) -> q_gen_589 (q_gen_577) -> q_gen_590 (q_gen_556) -> q_gen_595 (q_gen_567) -> q_gen_601 (q_gen_603) -> q_gen_602 (q_gen_552) -> q_gen_603 (q_gen_610) -> q_gen_609 (q_gen_561) -> q_gen_610 (q_gen_612) -> q_gen_611 (q_gen_562) -> q_gen_612 (q_gen_619) -> q_gen_618 (q_gen_620) -> q_gen_619 (q_gen_620) -> q_gen_621 (q_gen_601) -> q_gen_627 (q_gen_602) -> q_gen_628 (q_gen_630) -> q_gen_629 (q_gen_631) -> q_gen_630 (q_gen_632) -> q_gen_631 (q_gen_589) -> q_gen_636 (q_gen_590) -> q_gen_637 (q_gen_642) -> q_gen_641 (q_gen_643) -> q_gen_642 (q_gen_632) -> q_gen_643 (q_gen_654) -> q_gen_653 (q_gen_655) -> q_gen_654 (q_gen_656) -> q_gen_655 (q_gen_658) -> q_gen_657 (q_gen_659) -> q_gen_658 (q_gen_660) -> q_gen_659 (q_gen_657) -> q_gen_661 (q_gen_665) -> q_gen_664 (q_gen_666) -> q_gen_665 (q_gen_595) -> q_gen_666 (q_gen_672) -> q_gen_671 (q_gen_672) -> q_gen_677 (q_gen_679) -> q_gen_678 (q_gen_680) -> q_gen_679 (q_gen_684) -> q_gen_683 (q_gen_685) -> q_gen_684 (q_gen_555) -> q_gen_685 (q_gen_687) -> q_gen_686 (q_gen_636) -> q_gen_687 (q_gen_621) -> q_gen_688 (q_gen_629) -> q_gen_699 (q_gen_611) -> q_gen_700 (q_gen_702) -> q_gen_701 (q_gen_703) -> q_gen_702 (q_gen_570) -> q_gen_703 (q_gen_705) -> q_gen_704 (q_gen_706) -> q_gen_705 (q_gen_688) -> q_gen_706 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.004947 s (model generation: 0.004513, model checking: 0.000434): Model: |_ { minus -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; plus -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} } -- 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: Found: (() -> plus([n, z, n]), { n -> z }) ------------------------------------------- Step 1, which took 0.004880 s (model generation: 0.004794, model checking: 0.000086): Model: |_ { minus -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548}, Q_f={q_gen_548}, Delta= { () -> q_gen_548 } Datatype: Convolution form: right }}} } -- 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: Found: (() -> minus([z, y, z]), { y -> z }) ------------------------------------------- Step 2, which took 0.005046 s (model generation: 0.004798, model checking: 0.000248): Model: |_ { minus -> {{{ Q={q_gen_549}, Q_f={q_gen_549}, Delta= { () -> q_gen_549 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548}, Q_f={q_gen_548}, Delta= { () -> q_gen_548 } Datatype: Convolution form: right }}} } -- 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: Found: (() -> minus([s(u), z, s(u)]), { u -> z }) ------------------------------------------- Step 3, which took 0.005934 s (model generation: 0.005857, model checking: 0.000077): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551}, Q_f={q_gen_549}, Delta= { () -> q_gen_551 (q_gen_551) -> q_gen_549 () -> q_gen_549 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548}, Q_f={q_gen_548}, Delta= { () -> q_gen_548 } Datatype: Convolution form: right }}} } -- 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: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> z ; mm -> z ; n -> z }) ------------------------------------------- Step 4, which took 0.004399 s (model generation: 0.004293, model checking: 0.000106): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551}, Q_f={q_gen_549}, Delta= { () -> q_gen_551 (q_gen_551) -> q_gen_549 () -> q_gen_549 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553}, Q_f={q_gen_548}, Delta= { () -> q_gen_553 (q_gen_553) -> q_gen_548 () -> q_gen_548 } Datatype: Convolution form: right }}} } -- 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: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> z ; u -> z ; x2 -> z }) ------------------------------------------- Step 5, which took 0.005241 s (model generation: 0.005011, model checking: 0.000230): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551}, Q_f={q_gen_549}, Delta= { () -> q_gen_551 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 () -> q_gen_549 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553}, Q_f={q_gen_548}, Delta= { () -> q_gen_553 (q_gen_553) -> q_gen_548 () -> q_gen_548 } Datatype: Convolution form: right }}} } -- 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: Found: (() -> plus([n, z, n]), { n -> s(s(z)) }) ------------------------------------------- Step 6, which took 0.006954 s (model generation: 0.006676, model checking: 0.000278): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551}, Q_f={q_gen_549}, Delta= { () -> q_gen_551 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 () -> q_gen_549 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553}, Q_f={q_gen_548}, Delta= { (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 } Datatype: Convolution form: right }}} } -- 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: Found: (() -> minus([z, y, z]), { y -> s(z) }) ------------------------------------------- Step 7, which took 0.014177 s (model generation: 0.010527, model checking: 0.003650): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 () -> q_gen_551 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553}, Q_f={q_gen_548}, Delta= { (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 } Datatype: Convolution form: right }}} } -- 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: Found: (() -> minus([s(u), z, s(u)]), { u -> s(z) }) ------------------------------------------- Step 8, which took 0.012457 s (model generation: 0.012034, model checking: 0.000423): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553}, Q_f={q_gen_548}, Delta= { (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 } Datatype: Convolution form: right }}} } -- 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: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(z) ; mm -> z ; n -> s(z) }) ------------------------------------------- Step 9, which took 0.006063 s (model generation: 0.005708, model checking: 0.000355): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_564}, Q_f={q_gen_548}, Delta= { () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_548) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_564) -> q_gen_548 () -> q_gen_548 } Datatype: Convolution form: right }}} } -- 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: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(z) ; u -> s(z) ; x2 -> z }) ------------------------------------------- Step 10, which took 0.016629 s (model generation: 0.016308, model checking: 0.000321): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_549) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_564}, Q_f={q_gen_548}, Delta= { () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_548) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_564) -> q_gen_548 () -> q_gen_548 } Datatype: Convolution form: right }}} } -- 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: Found: ((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.015385 s (model generation: 0.014855, model checking: 0.000530): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_549) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564}, Q_f={q_gen_548}, Delta= { () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_548) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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]) -> 7 (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: Found: (() -> minus([z, y, z]), { y -> s(s(z)) }) ------------------------------------------- Step 12, which took 0.017434 s (model generation: 0.015077, model checking: 0.002357): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558}, Q_f={q_gen_549}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_549) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564}, Q_f={q_gen_548}, Delta= { () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_548) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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]) -> 7 (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: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(z)) ; mm -> s(z) ; n -> s(z) }) ------------------------------------------- Step 13, which took 0.016652 s (model generation: 0.016313, model checking: 0.000339): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558}, Q_f={q_gen_549}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_549) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_564, q_gen_567}, Q_f={q_gen_548, q_gen_552}, Delta= { () -> q_gen_564 (q_gen_553) -> q_gen_553 (q_gen_564) -> q_gen_553 () -> q_gen_553 (q_gen_552) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_553) -> q_gen_552 (q_gen_564) -> q_gen_552 (q_gen_548) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 7 (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: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> z ; u -> z ; x2 -> s(z) }) ------------------------------------------- Step 14, which took 0.013527 s (model generation: 0.013254, model checking: 0.000273): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558}, Q_f={q_gen_549}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 (q_gen_558) -> q_gen_551 () -> q_gen_551 (q_gen_549) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_564, q_gen_567}, Q_f={q_gen_548, q_gen_552}, Delta= { () -> q_gen_564 (q_gen_553) -> q_gen_553 (q_gen_564) -> q_gen_553 () -> q_gen_553 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_552) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_564) -> q_gen_552 (q_gen_548) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 7 (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: Found: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(z) ; _pc -> s(z) ; m -> z ; n -> s(z) }) ------------------------------------------- Step 15, which took 0.012120 s (model generation: 0.010236, model checking: 0.001884): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566}, Q_f={q_gen_549}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 (q_gen_558) -> q_gen_551 () -> q_gen_551 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_564, q_gen_567}, Q_f={q_gen_548, q_gen_552}, Delta= { () -> q_gen_564 (q_gen_553) -> q_gen_553 (q_gen_564) -> q_gen_553 () -> q_gen_553 () -> q_gen_548 (q_gen_552) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_564) -> q_gen_552 (q_gen_548) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 8 (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: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(z)) ; mm -> z ; n -> s(z) }) ------------------------------------------- Step 16, which took 0.023403 s (model generation: 0.021695, model checking: 0.001708): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566}, Q_f={q_gen_549}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 (q_gen_558) -> q_gen_551 () -> q_gen_551 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_564, q_gen_567}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 (q_gen_564) -> q_gen_553 () -> q_gen_553 () -> q_gen_548 (q_gen_552) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_564) -> q_gen_552 (q_gen_548) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 9 (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: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(z)) ; u -> s(z) ; x2 -> z }) ------------------------------------------- Step 17, which took 0.023673 s (model generation: 0.022208, model checking: 0.001465): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 (q_gen_558) -> q_gen_551 () -> q_gen_551 (q_gen_550) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_558) -> q_gen_550 (q_gen_549) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_564, q_gen_567}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 (q_gen_564) -> q_gen_553 () -> q_gen_553 () -> q_gen_548 (q_gen_552) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_564) -> q_gen_552 (q_gen_548) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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: Found: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(z) ; _pc -> s(z) ; m -> z ; n -> z }) ------------------------------------------- Step 18, which took 0.022254 s (model generation: 0.021906, model checking: 0.000348): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_575}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 (q_gen_558) -> q_gen_551 () -> q_gen_551 () -> q_gen_549 (q_gen_550) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_558) -> q_gen_550 (q_gen_558) -> q_gen_550 (q_gen_549) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_556, q_gen_563, q_gen_564}, Q_f={q_gen_548}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 () -> q_gen_553 (q_gen_553) -> q_gen_556 (q_gen_564) -> q_gen_556 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_556) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_548) -> q_gen_563 (q_gen_556) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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]) -> 13 (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: Found: (() -> plus([n, z, n]), { n -> s(s(s(z))) }) ------------------------------------------- Step 19, which took 0.025678 s (model generation: 0.024277, model checking: 0.001401): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_574}, Q_f={q_gen_549}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 (q_gen_564) -> q_gen_553 () -> q_gen_553 () -> q_gen_548 (q_gen_552) -> q_gen_552 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_548) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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]) -> 13 (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)]) -> 14 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(s(z)))) ; u -> s(s(z)) ; x2 -> s(z) }) ------------------------------------------- Step 20, which took 0.017489 s (model generation: 0.016989, model checking: 0.000500): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 (q_gen_558) -> q_gen_551 () -> q_gen_551 (q_gen_566) -> q_gen_549 () -> q_gen_549 (q_gen_550) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_558) -> q_gen_550 (q_gen_549) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_556, q_gen_563, q_gen_564}, Q_f={q_gen_548}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 () -> q_gen_553 (q_gen_553) -> q_gen_556 (q_gen_556) -> q_gen_556 (q_gen_564) -> q_gen_556 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_556) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_548) -> q_gen_563 (q_gen_556) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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]) -> 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)]) -> 14 } Sat witness: Found: ((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 21, which took 0.024311 s (model generation: 0.023735, model checking: 0.000576): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_575}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 (q_gen_558) -> q_gen_551 () -> q_gen_551 () -> q_gen_549 (q_gen_550) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_558) -> q_gen_550 (q_gen_558) -> q_gen_550 (q_gen_549) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_556, q_gen_561, q_gen_564}, Q_f={q_gen_548}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_553 () -> q_gen_553 (q_gen_553) -> q_gen_556 (q_gen_556) -> q_gen_556 (q_gen_556) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_548) -> q_gen_561 (q_gen_561) -> q_gen_561 (q_gen_553) -> q_gen_561 (q_gen_564) -> q_gen_561 } Datatype: Convolution form: right }}} } -- 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]) -> 16 (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)]) -> 14 } Sat witness: Found: (() -> plus([n, z, n]), { n -> s(z) }) ------------------------------------------- Step 22, which took 0.029996 s (model generation: 0.028171, model checking: 0.001825): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_574, q_gen_575}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_574) -> q_gen_549 () -> q_gen_549 (q_gen_550) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_558) -> q_gen_550 (q_gen_558) -> q_gen_550 (q_gen_549) -> q_gen_575 (q_gen_575) -> q_gen_575 (q_gen_574) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_572}, Q_f={q_gen_548}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_548) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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]) -> 16 (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)]) -> 17 } Sat witness: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(z))) ; mm -> s(z) ; n -> s(s(z)) }) ------------------------------------------- Step 23, which took 0.031245 s (model generation: 0.029627, model checking: 0.001618): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_574, q_gen_575}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_574) -> q_gen_549 () -> q_gen_549 (q_gen_550) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_558) -> q_gen_550 (q_gen_558) -> q_gen_550 (q_gen_549) -> q_gen_575 (q_gen_575) -> q_gen_575 (q_gen_574) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_556, q_gen_563, q_gen_564}, Q_f={q_gen_548}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 () -> q_gen_553 (q_gen_553) -> q_gen_556 (q_gen_556) -> q_gen_556 (q_gen_564) -> q_gen_556 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_556) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_548) -> q_gen_563 (q_gen_556) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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]) -> 16 (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)]) -> 17 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(z) ; u -> s(z) ; x2 -> s(s(z)) }) ------------------------------------------- Step 24, which took 0.034586 s (model generation: 0.032909, model checking: 0.001677): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_574, q_gen_575}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_574) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_550) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_558) -> q_gen_550 (q_gen_549) -> q_gen_575 (q_gen_575) -> q_gen_575 (q_gen_574) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_556, q_gen_563, q_gen_564}, Q_f={q_gen_548}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 () -> q_gen_553 (q_gen_553) -> q_gen_556 (q_gen_556) -> q_gen_556 (q_gen_564) -> q_gen_556 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_556) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_548) -> q_gen_563 (q_gen_556) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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)]) -> 17 } Sat witness: Found: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(z) ; _pc -> z ; m -> s(z) ; n -> z }) ------------------------------------------- Step 25, which took 0.034979 s (model generation: 0.034455, model checking: 0.000524): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_556, q_gen_563, q_gen_564}, Q_f={q_gen_548}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 () -> q_gen_553 (q_gen_553) -> q_gen_556 (q_gen_556) -> q_gen_556 (q_gen_564) -> q_gen_556 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_556) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_548) -> q_gen_563 (q_gen_556) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 16 () -> minus([z, y, z]) -> 19 () -> 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)]) -> 17 } Sat witness: Found: (() -> minus([z, y, z]), { y -> s(s(s(z))) }) ------------------------------------------- Step 26, which took 0.036365 s (model generation: 0.035545, model checking: 0.000820): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_556, q_gen_563, q_gen_564}, Q_f={q_gen_548}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 () -> q_gen_553 (q_gen_553) -> q_gen_556 (q_gen_556) -> q_gen_556 (q_gen_564) -> q_gen_556 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_556) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_548) -> q_gen_563 (q_gen_556) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 17 () -> minus([z, y, z]) -> 19 () -> 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)]) -> 20 } Sat witness: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(z) ; mm -> s(z) ; n -> z }) ------------------------------------------- Step 27, which took 0.037089 s (model generation: 0.036065, model checking: 0.001024): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 (q_gen_564) -> q_gen_553 () -> q_gen_553 (q_gen_552) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_548) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 18 () -> minus([z, y, z]) -> 19 () -> 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)]) -> 20 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(s(z)))) ; u -> s(z) ; x2 -> z }) ------------------------------------------- Step 28, which took 0.040438 s (model generation: 0.038870, model checking: 0.001568): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 (q_gen_564) -> q_gen_553 () -> q_gen_553 (q_gen_552) -> q_gen_548 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_553) -> q_gen_552 (q_gen_548) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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)]) -> 20 } Sat witness: Found: ((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 29, which took 0.038940 s (model generation: 0.036854, model checking: 0.002086): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_574, q_gen_575}, Q_f={q_gen_549}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_575) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_572}, Q_f={q_gen_548}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_572) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_548) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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)]) -> 23 } Sat witness: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(z)) ; mm -> z ; n -> s(s(z)) }) ------------------------------------------- Step 30, which took 0.038056 s (model generation: 0.036249, model checking: 0.001807): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_562, q_gen_563, q_gen_564, q_gen_572}, Q_f={q_gen_548, q_gen_562}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_562) -> q_gen_562 (q_gen_563) -> q_gen_562 (q_gen_548) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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]) -> 21 (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)]) -> 23 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(z) ; u -> s(s(z)) ; x2 -> s(z) }) ------------------------------------------- Step 31, which took 0.041001 s (model generation: 0.039953, model checking: 0.001048): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_554, q_gen_558, q_gen_566, q_gen_574}, Q_f={q_gen_549, q_gen_554}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_551) -> q_gen_549 () -> q_gen_549 (q_gen_554) -> q_gen_554 (q_gen_566) -> q_gen_554 (q_gen_551) -> q_gen_554 (q_gen_574) -> q_gen_554 (q_gen_558) -> q_gen_554 (q_gen_549) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_555, q_gen_563, q_gen_564, q_gen_572}, Q_f={q_gen_548, q_gen_555}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_555) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_555 (q_gen_553) -> q_gen_555 (q_gen_548) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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]) -> 22 (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)]) -> 23 } Sat witness: Found: ((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 32, which took 0.046666 s (model generation: 0.044522, model checking: 0.002144): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_586}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_586) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564, q_gen_572}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_552) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_548) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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]) -> 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)]) -> 26 } Sat witness: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(z)) ; mm -> s(s(z)) ; n -> s(s(z)) }) ------------------------------------------- Step 33, which took 0.050529 s (model generation: 0.048490, model checking: 0.002039): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_565, q_gen_566, q_gen_574, q_gen_600}, Q_f={q_gen_549, q_gen_565}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_565) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_565 (q_gen_549) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_562, q_gen_563, q_gen_564, q_gen_572}, Q_f={q_gen_548, q_gen_562}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_562) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_562 (q_gen_548) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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]) -> 24 (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)]) -> 26 } Sat witness: Found: ((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 34, which took 0.060768 s (model generation: 0.058580, model checking: 0.002188): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_557, q_gen_558, q_gen_566, q_gen_574, q_gen_600}, Q_f={q_gen_549, q_gen_557}, Delta= { (q_gen_558) -> q_gen_558 () -> q_gen_558 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 () -> q_gen_549 (q_gen_557) -> q_gen_557 (q_gen_566) -> q_gen_557 (q_gen_574) -> q_gen_557 (q_gen_558) -> q_gen_557 (q_gen_549) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_562, q_gen_563, q_gen_564, q_gen_572}, Q_f={q_gen_548, q_gen_562}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_562) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_562 (q_gen_548) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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)]) -> 26 } Sat witness: Found: ((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 35, which took 0.062918 s (model generation: 0.060806, model checking: 0.002112): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_586}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_586) -> q_gen_549 (q_gen_569) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_562, q_gen_563, q_gen_564, q_gen_572}, Q_f={q_gen_548, q_gen_562}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_562) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_562 (q_gen_548) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 26 () -> minus([z, y, z]) -> 26 () -> 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)]) -> 29 } Sat witness: Found: ((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 36, which took 0.054991 s (model generation: 0.053532, model checking: 0.001459): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_600}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_569) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_555, q_gen_563, q_gen_564, q_gen_572}, Q_f={q_gen_548, q_gen_555}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_555) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_555 (q_gen_553) -> q_gen_555 (q_gen_548) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 27 () -> minus([z, y, z]) -> 27 () -> 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]) -> 31 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 29 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> z ; u -> s(s(z)) ; x2 -> z }) ------------------------------------------- Step 37, which took 0.067101 s (model generation: 0.065603, model checking: 0.001498): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_560, q_gen_566, q_gen_569, q_gen_574}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_551) -> q_gen_560 (q_gen_558) -> q_gen_560 (q_gen_558) -> q_gen_574 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_560) -> q_gen_549 (q_gen_569) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_560) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_555, q_gen_563, q_gen_564, q_gen_572}, Q_f={q_gen_548, q_gen_555}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_555) -> q_gen_555 (q_gen_563) -> q_gen_555 (q_gen_553) -> q_gen_555 (q_gen_548) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 30 () -> 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)]) -> 29 } Sat witness: Found: (() -> minus([s(u), z, s(u)]), { u -> s(s(z)) }) ------------------------------------------- Step 38, which took 0.075048 s (model generation: 0.074553, model checking: 0.000495): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_600}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_569) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_555, q_gen_563, q_gen_564, q_gen_572}, Q_f={q_gen_548, q_gen_555}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_555) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_555 (q_gen_553) -> q_gen_555 (q_gen_548) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 30 () -> 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)]) -> 29 } Sat witness: Found: ((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 39, which took 0.080594 s (model generation: 0.078930, model checking: 0.001664): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_560, q_gen_566, q_gen_569, q_gen_574}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_560) -> q_gen_551 () -> q_gen_551 (q_gen_551) -> q_gen_560 (q_gen_558) -> q_gen_560 (q_gen_569) -> q_gen_560 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_560) -> q_gen_549 (q_gen_569) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_560) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_555, q_gen_563, q_gen_564, q_gen_572}, Q_f={q_gen_548, q_gen_555}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_555) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_555 (q_gen_553) -> q_gen_555 (q_gen_548) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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)]) -> 32 } Sat witness: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(z))) ; mm -> z ; n -> s(s(s(z))) }) ------------------------------------------- Step 40, which took 0.095482 s (model generation: 0.094622, model checking: 0.000860): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_560, q_gen_566, q_gen_569, q_gen_574}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_551) -> q_gen_560 (q_gen_560) -> q_gen_560 (q_gen_558) -> q_gen_560 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_560) -> q_gen_549 (q_gen_569) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_560) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564, q_gen_572}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 (q_gen_572) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 () -> q_gen_548 (q_gen_552) -> q_gen_552 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_548) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 } Datatype: Convolution form: right }}} } -- 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)]) -> 32 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> z ; u -> s(z) ; x2 -> s(z) }) ------------------------------------------- Step 41, which took 0.084148 s (model generation: 0.083175, model checking: 0.000973): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_600}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_569) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 (q_gen_572) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_552) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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)]) -> 32 } Sat witness: Found: ((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 42, which took 0.075421 s (model generation: 0.073955, model checking: 0.001466): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_600}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_569) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_555, q_gen_563, q_gen_564, q_gen_567, q_gen_572}, Q_f={q_gen_548, q_gen_555}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_555) -> q_gen_555 (q_gen_563) -> q_gen_555 (q_gen_553) -> q_gen_555 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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)]) -> 33 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(z)) ; u -> s(s(s(s(z)))) ; x2 -> s(z) }) ------------------------------------------- Step 43, which took 0.108917 s (model generation: 0.108046, model checking: 0.000871): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_586}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_586) -> q_gen_549 (q_gen_569) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_552) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 34 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 37 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 36 } Sat witness: Found: ((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 44, which took 0.096003 s (model generation: 0.095099, model checking: 0.000904): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_586}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_586) -> q_gen_549 (q_gen_569) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_552) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_567) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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)]) -> 36 } Sat witness: Found: ((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 45, which took 0.097023 s (model generation: 0.095777, model checking: 0.001246): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_586}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_586) -> q_gen_549 (q_gen_569) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_558) -> q_gen_566 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579}, Q_f={q_gen_548}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 37 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 39 } Sat witness: Found: ((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 46, which took 0.109415 s (model generation: 0.108683, model checking: 0.000732): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_580, q_gen_586}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_580) -> q_gen_580 (q_gen_574) -> q_gen_580 (q_gen_586) -> q_gen_580 (q_gen_569) -> q_gen_580 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_552) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_567) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 37 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 40 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 39 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(z)) ; u -> s(s(z)) ; x2 -> z }) ------------------------------------------- Step 47, which took 0.121077 s (model generation: 0.120034, model checking: 0.001043): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_580, q_gen_586}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_549) -> q_gen_566 (q_gen_580) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_574) -> q_gen_580 (q_gen_569) -> q_gen_580 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_552) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_567) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 40 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 39 } Sat witness: Found: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(z)) ; _pc -> s(s(z)) ; m -> z ; n -> s(s(z)) }) ------------------------------------------- Step 48, which took 0.158618 s (model generation: 0.157513, model checking: 0.001105): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_552) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_567) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 40 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 40 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 42 } Sat witness: Found: ((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 49, which took 0.118952 s (model generation: 0.118043, model checking: 0.000909): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_586}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_575) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_552) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_572) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_567) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 40 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 43 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 42 } Sat witness: Found: ((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 50, which took 0.193199 s (model generation: 0.192221, model checking: 0.000978): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_575) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_552}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 (q_gen_579) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_552) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 43 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 43 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 42 } Sat witness: Found: ((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 51, which took 0.180470 s (model generation: 0.179740, model checking: 0.000730): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_586}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_550) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_586) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_575) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_562, q_gen_563, q_gen_564, q_gen_567, q_gen_572}, Q_f={q_gen_548, q_gen_562}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_562) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_562 (q_gen_572) -> q_gen_562 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_567) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 43 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 43 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 45 } Sat witness: Found: ((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 52, which took 0.146087 s (model generation: 0.145076, model checking: 0.001011): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_586}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_569) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_575) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_552}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 (q_gen_579) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 () -> q_gen_548 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_579) -> q_gen_552 (q_gen_552) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_567) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 43 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 46 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 45 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(s(s(z))))) ; u -> s(s(z)) ; x2 -> s(z) }) ------------------------------------------- Step 53, which took 0.181513 s (model generation: 0.180279, model checking: 0.001234): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_586}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_569) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_575) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_552}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 (q_gen_579) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 () -> q_gen_548 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_579) -> q_gen_552 (q_gen_552) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_567) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 46 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 45 } Sat witness: Found: ((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 54, which took 0.167277 s (model generation: 0.166309, model checking: 0.000968): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_586}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_550) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_575) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_562, q_gen_563, q_gen_564, q_gen_567, q_gen_572}, Q_f={q_gen_548, q_gen_562}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_562) -> q_gen_562 (q_gen_563) -> q_gen_562 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_567) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 46 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 49 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 46 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(z))) ; u -> s(s(s(z))) ; x2 -> s(s(s(s(s(z))))) }) ------------------------------------------- Step 55, which took 0.198005 s (model generation: 0.196546, model checking: 0.001459): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_569) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632}, Q_f={q_gen_548}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_632 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 46 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 49 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 49 } Sat witness: Found: ((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(z)) }) ------------------------------------------- Step 56, which took 0.294475 s (model generation: 0.293404, model checking: 0.001071): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_575) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632}, Q_f={q_gen_548}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 49 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 49 } Sat witness: Found: ((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 57, which took 0.277514 s (model generation: 0.276493, model checking: 0.001021): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_569) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_550) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_555, q_gen_563, q_gen_564, q_gen_567, q_gen_572}, Q_f={q_gen_548, q_gen_555}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_555) -> q_gen_555 (q_gen_563) -> q_gen_555 (q_gen_553) -> q_gen_555 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_567) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 49 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 52 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 50 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(z))) ; u -> s(z) ; x2 -> z }) ------------------------------------------- Step 58, which took 0.250525 s (model generation: 0.249861, model checking: 0.000664): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_586}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_558) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_550) -> q_gen_550 (q_gen_566) -> q_gen_550 (q_gen_574) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_569) -> q_gen_550 (q_gen_586) -> q_gen_566 (q_gen_574) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_575) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_562, q_gen_563, q_gen_564, q_gen_567, q_gen_572}, Q_f={q_gen_548, q_gen_562}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_562) -> q_gen_562 (q_gen_563) -> q_gen_562 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_567) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 52 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 50 } Sat witness: Found: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(z)) ; _pc -> s(s(s(z))) ; m -> s(z) ; n -> s(z) }) ------------------------------------------- Step 59, which took 0.316918 s (model generation: 0.315198, model checking: 0.001720): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_586, q_gen_600}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_586 (q_gen_569) -> q_gen_586 (q_gen_558) -> q_gen_600 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_575) -> q_gen_575 (q_gen_586) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_586) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_562, q_gen_563, q_gen_564, q_gen_567, q_gen_572}, Q_f={q_gen_548, q_gen_562}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_562) -> q_gen_562 (q_gen_563) -> q_gen_562 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 52 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 55 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 51 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> z ; u -> z ; x2 -> s(s(z)) }) ------------------------------------------- Step 60, which took 0.223018 s (model generation: 0.221571, model checking: 0.001447): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600, q_gen_614}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_614 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_614) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_614) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_562, q_gen_563, q_gen_564, q_gen_567, q_gen_572}, Q_f={q_gen_548, q_gen_562}, Delta= { (q_gen_564) -> q_gen_564 () -> q_gen_564 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_562) -> q_gen_562 (q_gen_563) -> q_gen_562 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_567) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 55 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 52 } Sat witness: Found: ((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 61, which took 0.261976 s (model generation: 0.261162, model checking: 0.000814): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_550) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_574) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_558) -> q_gen_550 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_575) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_562, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_562}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_562) -> q_gen_562 (q_gen_563) -> q_gen_562 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 55 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 55 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 55 } Sat witness: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(s(z)))) ; mm -> s(z) ; n -> s(s(z)) }) ------------------------------------------- Step 62, which took 0.238414 s (model generation: 0.236964, model checking: 0.001450): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_550) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_574) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_558) -> q_gen_550 (q_gen_569) -> q_gen_550 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632}, Q_f={q_gen_548}, Delta= { (q_gen_579) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 55 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 55 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 58 } Sat witness: Found: ((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 63, which took 0.229831 s (model generation: 0.229197, model checking: 0.000634): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_574) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_550) -> q_gen_550 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_575) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_562, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_562}, Delta= { (q_gen_579) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_562) -> q_gen_562 (q_gen_563) -> q_gen_562 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 55 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 58 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 58 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(z)) ; u -> s(s(s(z))) ; x2 -> s(z) }) ------------------------------------------- Step 64, which took 0.279684 s (model generation: 0.278630, model checking: 0.001054): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_550) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_574) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_569) -> q_gen_550 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_562, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_562}, Delta= { (q_gen_579) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_562) -> q_gen_562 (q_gen_563) -> q_gen_562 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 58 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 58 } Sat witness: Found: ((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(s(z)) }) ------------------------------------------- Step 65, which took 0.369195 s (model generation: 0.367365, model checking: 0.001830): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600, q_gen_614}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_614 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_614) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_614) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_578, q_gen_579}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_579) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 (q_gen_579) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 () -> q_gen_548 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_552) -> q_gen_563 (q_gen_578) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_567) -> q_gen_567 (q_gen_579) -> q_gen_578 } Datatype: Convolution form: right }}} } -- 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]) -> 58 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 61 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 59 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(s(s(z))))) ; u -> s(s(s(z))) ; x2 -> s(s(z)) }) ------------------------------------------- Step 66, which took 0.433035 s (model generation: 0.432056, model checking: 0.000979): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_550) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_552, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_578, q_gen_579}, Q_f={q_gen_548, q_gen_552}, Delta= { (q_gen_579) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 (q_gen_579) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 () -> q_gen_548 (q_gen_563) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_553) -> q_gen_552 (q_gen_552) -> q_gen_563 (q_gen_578) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_567) -> q_gen_567 (q_gen_579) -> q_gen_578 } Datatype: Convolution form: right }}} } -- 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)]) -> 59 } Sat witness: Found: ((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 67, which took 0.504202 s (model generation: 0.502862, model checking: 0.001340): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_550) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_555, q_gen_556, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_555}, Delta= { (q_gen_579) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 () -> q_gen_553 (q_gen_553) -> q_gen_556 (q_gen_556) -> q_gen_556 (q_gen_579) -> q_gen_556 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_555 (q_gen_556) -> q_gen_555 (q_gen_556) -> q_gen_555 (q_gen_555) -> q_gen_563 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 61 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 62 } Sat witness: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(s(z)))) ; mm -> s(s(s(s(z)))) ; n -> s(s(s(z))) }) ------------------------------------------- Step 68, which took 0.779730 s (model generation: 0.778831, model checking: 0.000899): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_574) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_550) -> q_gen_550 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_570, q_gen_571, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_570}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_563) -> q_gen_548 (q_gen_570) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 (q_gen_571) -> q_gen_570 (q_gen_567) -> q_gen_571 (q_gen_572) -> q_gen_571 (q_gen_572) -> q_gen_571 } Datatype: Convolution form: right }}} } -- 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]) -> 61 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 64 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 62 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(z))) ; u -> s(s(s(z))) ; x2 -> z }) ------------------------------------------- Step 69, which took 0.401160 s (model generation: 0.399996, model checking: 0.001164): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_600) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_550) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_569) -> q_gen_550 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632, q_gen_660}, Q_f={q_gen_548}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_660 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_660) -> q_gen_548 () -> q_gen_548 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 64 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 62 } Sat witness: Found: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(z))) ; _pc -> z ; m -> s(z) ; n -> s(s(z)) }) ------------------------------------------- Step 70, which took 0.396442 s (model generation: 0.394837, model checking: 0.001605): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_550) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_574) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_569) -> q_gen_550 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632, q_gen_660}, Q_f={q_gen_548}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_660 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_660) -> q_gen_548 () -> q_gen_548 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 64 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 64 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 65 } Sat witness: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(z))) ; mm -> z ; n -> z }) ------------------------------------------- Step 71, which took 0.432102 s (model generation: 0.430886, model checking: 0.001216): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_550) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_555, q_gen_563, q_gen_564, q_gen_567, q_gen_571, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_555}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_555) -> q_gen_548 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_571) -> q_gen_555 (q_gen_553) -> q_gen_555 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 (q_gen_567) -> q_gen_571 (q_gen_572) -> q_gen_571 (q_gen_572) -> q_gen_571 } Datatype: Convolution form: right }}} } -- 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]) -> 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: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(z))) ; u -> s(s(s(z))) ; x2 -> s(s(s(z))) }) ------------------------------------------- Step 72, which took 0.554647 s (model generation: 0.553602, model checking: 0.001045): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_550) -> q_gen_550 (q_gen_566) -> q_gen_550 (q_gen_574) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632, q_gen_660}, Q_f={q_gen_548}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_660 (q_gen_553) -> q_gen_553 (q_gen_660) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_660) -> q_gen_548 () -> q_gen_548 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 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: Found: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(z))) ; _pc -> s(s(s(z))) ; m -> s(z) ; n -> s(s(z)) }) ------------------------------------------- Step 73, which took 0.598354 s (model generation: 0.596488, model checking: 0.001866): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_550) -> q_gen_549 (q_gen_551) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_574) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_558) -> q_gen_550 (q_gen_569) -> q_gen_550 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632, q_gen_660}, Q_f={q_gen_548}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_660 (q_gen_553) -> q_gen_553 (q_gen_660) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_660) -> q_gen_548 () -> q_gen_548 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 67 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 67 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 68 } Sat witness: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(s(z)))) ; mm -> z ; n -> s(z) }) ------------------------------------------- Step 74, which took 0.690643 s (model generation: 0.689797, model checking: 0.000846): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_550) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_570, q_gen_571, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_570}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_563) -> q_gen_548 (q_gen_570) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 (q_gen_571) -> q_gen_570 (q_gen_567) -> q_gen_571 (q_gen_572) -> q_gen_571 (q_gen_572) -> q_gen_571 } Datatype: Convolution form: right }}} } -- 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]) -> 67 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 70 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 68 } Sat witness: Found: ((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 75, which took 0.639358 s (model generation: 0.638569, model checking: 0.000789): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_565, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_565}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_565) -> q_gen_565 (q_gen_566) -> q_gen_565 (q_gen_569) -> q_gen_565 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632, q_gen_660}, Q_f={q_gen_548}, Delta= { (q_gen_660) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_660 (q_gen_553) -> q_gen_553 (q_gen_660) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_660) -> q_gen_548 () -> q_gen_548 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 70 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 70 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 68 } Sat witness: Found: ((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 76, which took 0.849982 s (model generation: 0.848274, model checking: 0.001708): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_565, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_565}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_565) -> q_gen_565 (q_gen_566) -> q_gen_565 (q_gen_600) -> q_gen_565 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_570, q_gen_571, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_570}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 (q_gen_570) -> q_gen_570 (q_gen_571) -> q_gen_570 (q_gen_567) -> q_gen_571 (q_gen_572) -> q_gen_571 (q_gen_572) -> q_gen_571 } Datatype: Convolution form: right }}} } -- 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]) -> 70 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 73 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 69 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(z) ; u -> s(s(z)) ; x2 -> z }) ------------------------------------------- Step 77, which took 0.469237 s (model generation: 0.467719, model checking: 0.001518): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_554, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_554}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_554) -> q_gen_554 (q_gen_566) -> q_gen_554 (q_gen_551) -> q_gen_554 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632, q_gen_660}, Q_f={q_gen_548}, Delta= { (q_gen_660) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_660 (q_gen_553) -> q_gen_553 (q_gen_660) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_660) -> q_gen_548 () -> q_gen_548 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 73 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 73 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 70 } Sat witness: Found: ((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 78, which took 1.001303 s (model generation: 0.999468, model checking: 0.001835): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_565, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_565}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_565) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_565 (q_gen_569) -> q_gen_565 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632, q_gen_660}, Q_f={q_gen_548}, Delta= { (q_gen_660) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_660 (q_gen_553) -> q_gen_553 (q_gen_660) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_660) -> q_gen_548 () -> q_gen_548 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 73 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 76 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 71 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(s(s(z)))) ; u -> s(s(s(s(z)))) ; x2 -> s(s(s(z))) }) ------------------------------------------- Step 79, which took 0.905990 s (model generation: 0.904908, model checking: 0.001082): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_565, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_565}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_565) -> q_gen_565 (q_gen_566) -> q_gen_565 (q_gen_569) -> q_gen_565 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_570, q_gen_571, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_570}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_563) -> q_gen_548 (q_gen_570) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 (q_gen_571) -> q_gen_570 (q_gen_567) -> q_gen_571 (q_gen_572) -> q_gen_571 (q_gen_572) -> q_gen_571 } Datatype: Convolution form: right }}} } -- 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]) -> 73 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 76 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 74 } Sat witness: Found: ((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 80, which took 1.093017 s (model generation: 1.092299, model checking: 0.000718): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_565, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_565}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_565) -> q_gen_565 (q_gen_566) -> q_gen_565 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_570, q_gen_571, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_570}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 (q_gen_570) -> q_gen_570 (q_gen_571) -> q_gen_570 (q_gen_567) -> q_gen_571 (q_gen_572) -> q_gen_571 (q_gen_572) -> q_gen_571 } Datatype: Convolution form: right }}} } -- 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]) -> 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: Found: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(s(z)))) ; _pc -> s(s(s(z))) ; m -> s(z) ; n -> s(s(s(z))) }) ------------------------------------------- Step 81, which took 1.333286 s (model generation: 1.330793, model checking: 0.002493): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_568, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_550, q_gen_568}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_568) -> q_gen_566 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_550) -> q_gen_568 (q_gen_569) -> q_gen_568 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632, q_gen_660}, Q_f={q_gen_548}, Delta= { (q_gen_660) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_660 (q_gen_553) -> q_gen_553 (q_gen_660) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_660) -> q_gen_548 () -> q_gen_548 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 76 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 79 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 75 } Sat witness: Found: ((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(s(z))) }) ------------------------------------------- Step 82, which took 1.274269 s (model generation: 1.272522, model checking: 0.001747): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_565, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_600}, Q_f={q_gen_549, q_gen_565}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_565) -> q_gen_565 (q_gen_566) -> q_gen_565 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_620, q_gen_632, q_gen_660}, Q_f={q_gen_548}, Delta= { (q_gen_660) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_660 (q_gen_553) -> q_gen_553 (q_gen_660) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_572) -> q_gen_620 (q_gen_632) -> q_gen_620 (q_gen_579) -> q_gen_632 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_660) -> q_gen_548 () -> q_gen_548 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_620) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_620) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 76 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 79 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 78 } Sat witness: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(z))) ; mm -> s(s(z)) ; n -> s(z) }) ------------------------------------------- Step 83, which took 2.638518 s (model generation: 2.637518, model checking: 0.001000): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_580, q_gen_600, q_gen_614}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_614 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_614) -> q_gen_575 (q_gen_569) -> q_gen_575 (q_gen_580) -> q_gen_580 (q_gen_574) -> q_gen_580 (q_gen_614) -> q_gen_580 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632, q_gen_660}, Q_f={q_gen_548}, Delta= { (q_gen_660) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_660 (q_gen_553) -> q_gen_553 (q_gen_660) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_660) -> q_gen_548 () -> q_gen_548 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 79 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 79 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 78 } Sat witness: Found: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(s(z)))) ; _pc -> s(s(s(z))) ; m -> z ; n -> s(z) }) ------------------------------------------- Step 84, which took 1.238842 s (model generation: 1.237347, model checking: 0.001495): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_568, q_gen_569, q_gen_574, q_gen_575, q_gen_584, q_gen_600}, Q_f={q_gen_549, q_gen_568}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_568) -> q_gen_568 (q_gen_584) -> q_gen_568 (q_gen_574) -> q_gen_568 (q_gen_569) -> q_gen_568 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 (q_gen_575) -> q_gen_584 (q_gen_600) -> q_gen_584 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_570, q_gen_571, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_570}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 (q_gen_570) -> q_gen_570 (q_gen_571) -> q_gen_570 (q_gen_567) -> q_gen_571 (q_gen_572) -> q_gen_571 (q_gen_572) -> q_gen_571 } Datatype: Convolution form: right }}} } -- 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]) -> 79 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 82 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 79 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> z ; u -> s(z) ; x2 -> s(s(z)) }) ------------------------------------------- Step 85, which took 1.604590 s (model generation: 1.602064, model checking: 0.002526): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_580, q_gen_600, q_gen_614}, Q_f={q_gen_549}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_574) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_614 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_614) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_580) -> q_gen_575 (q_gen_614) -> q_gen_575 (q_gen_569) -> q_gen_575 (q_gen_574) -> q_gen_580 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_555, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632}, Q_f={q_gen_548, q_gen_555}, Delta= { (q_gen_579) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_555 (q_gen_553) -> q_gen_555 (q_gen_555) -> q_gen_563 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 82 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 82 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 80 } Sat witness: Found: ((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 86, which took 2.378991 s (model generation: 2.376328, model checking: 0.002663): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_586, q_gen_600, q_gen_614}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_574) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_586 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_614 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_586) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_614) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_614) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_570, q_gen_571, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_570}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 (q_gen_570) -> q_gen_570 (q_gen_571) -> q_gen_570 (q_gen_567) -> q_gen_571 (q_gen_572) -> q_gen_571 (q_gen_572) -> q_gen_571 } Datatype: Convolution form: right }}} } -- 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]) -> 82 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 85 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 81 } Sat witness: Found: ((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 87, which took 2.144020 s (model generation: 2.142062, model checking: 0.001958): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_586, q_gen_600, q_gen_614}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_574) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_586 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_614 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_586) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_614) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_614) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_555, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632}, Q_f={q_gen_548, q_gen_555}, Delta= { (q_gen_579) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_555 (q_gen_553) -> q_gen_555 (q_gen_632) -> q_gen_555 (q_gen_632) -> q_gen_555 (q_gen_555) -> q_gen_563 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 85 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 85 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 82 } Sat witness: Found: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(z))) ; _pc -> s(s(z)) ; m -> z ; n -> s(z) }) ------------------------------------------- Step 88, which took 2.576325 s (model generation: 2.573287, model checking: 0.003038): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_574, q_gen_575, q_gen_586, q_gen_600, q_gen_614}, Q_f={q_gen_549}, Delta= { (q_gen_569) -> q_gen_558 () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_574) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_586 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_614 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_586) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_614) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_586) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_549) -> q_gen_575 (q_gen_614) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_555, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_579, q_gen_632}, Q_f={q_gen_548, q_gen_555}, Delta= { (q_gen_579) -> q_gen_564 () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_563) -> q_gen_555 (q_gen_553) -> q_gen_555 (q_gen_555) -> q_gen_563 (q_gen_567) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 } Datatype: Convolution form: right }}} } -- 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]) -> 85 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 88 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 83 } Sat witness: Found: ((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 89, which took 2.884880 s (model generation: 2.882632, model checking: 0.002248): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_573, q_gen_574, q_gen_575, q_gen_584, q_gen_600}, Q_f={q_gen_549, q_gen_573}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_574) -> q_gen_551 () -> q_gen_551 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_558) -> q_gen_566 (q_gen_573) -> q_gen_573 (q_gen_584) -> q_gen_573 (q_gen_574) -> q_gen_573 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 (q_gen_575) -> q_gen_584 (q_gen_600) -> q_gen_584 (q_gen_600) -> q_gen_584 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_570, q_gen_571, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_570}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 (q_gen_570) -> q_gen_570 (q_gen_571) -> q_gen_570 (q_gen_567) -> q_gen_571 (q_gen_572) -> q_gen_571 (q_gen_572) -> q_gen_571 } Datatype: Convolution form: right }}} } -- 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]) -> 88 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 84 } Sat witness: Found: ((minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]), { _oc -> s(s(s(s(s(s(z)))))) ; _pc -> s(z) ; m -> s(s(s(z))) ; n -> s(s(s(s(z)))) }) ------------------------------------------- Step 90, which took 2.341324 s (model generation: 2.340715, model checking: 0.000609): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_568, q_gen_569, q_gen_574, q_gen_575, q_gen_584, q_gen_600}, Q_f={q_gen_549, q_gen_568}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_574) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_558) -> q_gen_566 (q_gen_568) -> q_gen_568 (q_gen_584) -> q_gen_568 (q_gen_569) -> q_gen_568 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 (q_gen_575) -> q_gen_584 (q_gen_600) -> q_gen_584 (q_gen_600) -> q_gen_584 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_555, q_gen_563, q_gen_564, q_gen_567, q_gen_571, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_555}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_555) -> q_gen_548 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_571) -> q_gen_555 (q_gen_553) -> q_gen_555 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 (q_gen_567) -> q_gen_571 (q_gen_572) -> q_gen_571 (q_gen_572) -> q_gen_571 } Datatype: Convolution form: right }}} } -- 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]) -> 88 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 88 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 87 } Sat witness: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(s(s(z))))) ; mm -> s(s(s(s(z)))) ; n -> s(s(s(s(z)))) }) ------------------------------------------- Step 91, which took 4.966314 s (model generation: 4.964857, model checking: 0.001457): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_573, q_gen_574, q_gen_575, q_gen_600, q_gen_614}, Q_f={q_gen_549, q_gen_550, q_gen_573}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_574) -> q_gen_551 () -> q_gen_551 (q_gen_614) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_614 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_573) -> q_gen_566 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_550) -> q_gen_573 (q_gen_574) -> q_gen_573 (q_gen_614) -> q_gen_573 (q_gen_549) -> q_gen_575 (q_gen_614) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_570, q_gen_571, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_570}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 (q_gen_570) -> q_gen_570 (q_gen_571) -> q_gen_570 (q_gen_567) -> q_gen_571 (q_gen_572) -> q_gen_571 (q_gen_572) -> q_gen_571 } Datatype: Convolution form: right }}} } -- 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]) -> 88 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 91 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 88 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(z) ; u -> s(s(s(z))) ; x2 -> z }) ------------------------------------------- Step 92, which took 6.046197 s (model generation: 6.044789, model checking: 0.001408): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_550, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_573, q_gen_574, q_gen_575, q_gen_600, q_gen_614}, Q_f={q_gen_549, q_gen_550, q_gen_573}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 (q_gen_574) -> q_gen_551 () -> q_gen_551 (q_gen_614) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_558) -> q_gen_600 (q_gen_600) -> q_gen_614 (q_gen_569) -> q_gen_614 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_566) -> q_gen_550 (q_gen_551) -> q_gen_550 (q_gen_573) -> q_gen_566 (q_gen_575) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_600) -> q_gen_566 (q_gen_614) -> q_gen_566 (q_gen_558) -> q_gen_566 (q_gen_550) -> q_gen_573 (q_gen_574) -> q_gen_573 (q_gen_549) -> q_gen_575 (q_gen_614) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_570, q_gen_571, q_gen_572, q_gen_579}, Q_f={q_gen_548, q_gen_570}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_579) -> q_gen_572 (q_gen_563) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 (q_gen_570) -> q_gen_570 (q_gen_571) -> q_gen_570 (q_gen_567) -> q_gen_571 (q_gen_572) -> q_gen_571 (q_gen_572) -> q_gen_571 } Datatype: Convolution form: right }}} } -- 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]) -> 91 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 89 } Sat witness: Found: ((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 93, which took 5.373654 s (model generation: 5.372292, model checking: 0.001362): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_569, q_gen_573, q_gen_574, q_gen_575, q_gen_584, q_gen_600}, Q_f={q_gen_549, q_gen_573}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_574) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 (q_gen_569) -> q_gen_549 () -> q_gen_549 (q_gen_558) -> q_gen_566 (q_gen_573) -> q_gen_573 (q_gen_584) -> q_gen_573 (q_gen_574) -> q_gen_573 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 (q_gen_575) -> q_gen_584 (q_gen_600) -> q_gen_584 (q_gen_600) -> q_gen_584 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_577, q_gen_579, q_gen_590, q_gen_620}, Q_f={q_gen_548, q_gen_590}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_564) -> q_gen_572 (q_gen_572) -> q_gen_620 (q_gen_620) -> q_gen_620 (q_gen_579) -> q_gen_620 (q_gen_563) -> q_gen_548 (q_gen_590) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_579) -> q_gen_567 (q_gen_567) -> q_gen_577 (q_gen_620) -> q_gen_577 (q_gen_620) -> q_gen_577 (q_gen_577) -> q_gen_590 } Datatype: Convolution form: right }}} } -- 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]) -> 91 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 91 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 92 } Sat witness: Found: ((plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]), { _jc -> s(s(s(s(s(s(z)))))) ; mm -> s(s(s(s(s(z))))) ; n -> s(s(s(s(z)))) }) ------------------------------------------- Step 94, which took 6.803783 s (model generation: 6.801969, model checking: 0.001814): Model: |_ { minus -> {{{ Q={q_gen_549, q_gen_551, q_gen_558, q_gen_566, q_gen_568, q_gen_569, q_gen_574, q_gen_575, q_gen_584, q_gen_600}, Q_f={q_gen_549, q_gen_568}, Delta= { () -> q_gen_558 (q_gen_558) -> q_gen_569 (q_gen_569) -> q_gen_569 (q_gen_551) -> q_gen_551 () -> q_gen_551 (q_gen_574) -> q_gen_574 (q_gen_558) -> q_gen_574 (q_gen_569) -> q_gen_574 (q_gen_600) -> q_gen_600 (q_gen_558) -> q_gen_600 (q_gen_569) -> q_gen_600 (q_gen_566) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_574) -> q_gen_549 (q_gen_551) -> q_gen_549 (q_gen_558) -> q_gen_549 () -> q_gen_549 (q_gen_558) -> q_gen_566 (q_gen_568) -> q_gen_568 (q_gen_584) -> q_gen_568 (q_gen_569) -> q_gen_568 (q_gen_549) -> q_gen_575 (q_gen_574) -> q_gen_575 (q_gen_569) -> q_gen_575 (q_gen_575) -> q_gen_584 (q_gen_600) -> q_gen_584 (q_gen_600) -> q_gen_584 } Datatype: Convolution form: right }}} ; plus -> {{{ Q={q_gen_548, q_gen_553, q_gen_563, q_gen_564, q_gen_567, q_gen_572, q_gen_577, q_gen_579, q_gen_590, q_gen_632}, Q_f={q_gen_548, q_gen_590}, Delta= { () -> q_gen_564 (q_gen_564) -> q_gen_579 (q_gen_579) -> q_gen_579 (q_gen_553) -> q_gen_553 () -> q_gen_553 (q_gen_572) -> q_gen_572 (q_gen_564) -> q_gen_572 (q_gen_632) -> q_gen_632 (q_gen_579) -> q_gen_632 (q_gen_563) -> q_gen_548 (q_gen_590) -> q_gen_548 (q_gen_553) -> q_gen_548 (q_gen_553) -> q_gen_548 () -> q_gen_548 (q_gen_572) -> q_gen_563 (q_gen_572) -> q_gen_563 (q_gen_564) -> q_gen_563 (q_gen_548) -> q_gen_567 (q_gen_632) -> q_gen_567 (q_gen_579) -> q_gen_567 (q_gen_567) -> q_gen_577 (q_gen_632) -> q_gen_577 (q_gen_577) -> q_gen_590 } Datatype: Convolution form: right }}} } -- Equality automata are defined for: {eq_nat} _| Teacher's answer: New clause system: { () -> minus([s(u), z, s(u)]) -> 84 () -> minus([z, y, z]) -> 84 () -> plus([n, z, n]) -> 84 (minus([_oc, n, _pc]) /\ plus([m, n, _oc])) -> eq_nat([_pc, m]) -> 91 (minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]) -> 94 (plus([n, mm, _jc])) -> plus([n, s(mm), s(_jc)]) -> 92 } Sat witness: Found: ((minus([u, x2, _ec])) -> minus([s(u), s(x2), _ec]), { _ec -> s(s(z)) ; u -> s(s(z)) ; x2 -> s(s(s(s(z)))) }) Total time: 67.309641 Reason for stopping: DontKnow. Stopped because: timeout