Inference procedure has parameters: Ice fuel: 200 Timeout: 60s Convolution: left Learning problem is: env: { elt -> {a, b} ; list -> {cons, nil} ; list2 -> {cons2, nil2} ; pair -> {pair2} } definition: { (zip, F: {() -> zip([cons2(z, x2), nil2, nil]) () -> zip([nil2, y, nil]) (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)])} (zip([_bda, _cda, _dda]) /\ zip([_bda, _cda, _eda])) -> eq_list([_dda, _eda]) ) (zip_concat, F: {() -> zip_concat([x, y, nil2, nil]) (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)])} (zip_concat([_gda, _hda, _ida, _jda]) /\ zip_concat([_gda, _hda, _ida, _kda])) -> eq_list([_jda, _kda]) ) } properties: {(zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)])} over-approximation: {zip, zip_concat} under-approximation: {zip_concat} Clause system for inference is: { () -> zip([cons2(z, x2), nil2, nil]) -> 0 () -> zip([nil2, y, nil]) -> 0 () -> zip_concat([x, y, nil2, nil]) -> 0 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 0 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 0 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 0 } Solving took 0.584551 seconds. Proved Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 (q_gen_8036, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8036, q_gen_8029) -> q_gen_8035 (q_gen_8029, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049, q_gen_8053, q_gen_8054}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 (q_gen_8033, q_gen_8049) -> q_gen_8049 () -> q_gen_8049 (q_gen_8033, q_gen_8049) -> q_gen_8031 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8054, q_gen_8053) -> q_gen_8053 (q_gen_8033, q_gen_8049) -> q_gen_8053 (q_gen_8032, q_gen_8031) -> q_gen_8053 () -> q_gen_8053 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.010870 s (model generation: 0.010065, model checking: 0.000805): Model: |_ { zip -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 0 () -> zip([nil2, y, nil]) -> 0 () -> zip_concat([x, y, nil2, nil]) -> 3 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 1 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 1 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 1 } Sat witness: Found: (() -> zip_concat([x, y, nil2, nil]), { x -> b ; y -> nil2 }) ------------------------------------------- Step 1, which took 0.010582 s (model generation: 0.010228, model checking: 0.000354): Model: |_ { zip -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 0 () -> zip([nil2, y, nil]) -> 3 () -> zip_concat([x, y, nil2, nil]) -> 3 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 1 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 1 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 1 } Sat witness: Found: (() -> zip([nil2, y, nil]), { y -> nil2 }) ------------------------------------------- Step 2, which took 0.008643 s (model generation: 0.008348, model checking: 0.000295): Model: |_ { zip -> {{{ Q={q_gen_8026}, Q_f={q_gen_8026}, Delta= { () -> q_gen_8026 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 3 () -> zip([nil2, y, nil]) -> 3 () -> zip_concat([x, y, nil2, nil]) -> 3 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 1 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 1 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 1 } Sat witness: Found: (() -> zip([cons2(z, x2), nil2, nil]), { x2 -> nil2 ; z -> b }) ------------------------------------------- Step 3, which took 0.020915 s (model generation: 0.020105, model checking: 0.000810): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029}, Q_f={q_gen_8026}, Delta= { () -> q_gen_8028 () -> q_gen_8029 (q_gen_8029, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 3 () -> zip([nil2, y, nil]) -> 3 () -> zip_concat([x, y, nil2, nil]) -> 3 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 1 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 1 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 4 } Sat witness: Found: ((zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]), { _fda -> nil ; x -> a ; y -> nil2 ; y2 -> a ; ys -> nil2 }) ------------------------------------------- Step 4, which took 0.020836 s (model generation: 0.020172, model checking: 0.000664): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029}, Q_f={q_gen_8026}, Delta= { () -> q_gen_8028 () -> q_gen_8029 (q_gen_8029, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 3 () -> zip([nil2, y, nil]) -> 3 () -> zip_concat([x, y, nil2, nil]) -> 3 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 4 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 2 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 4 } Sat witness: Found: ((zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]), { _ada -> nil ; x2 -> nil2 ; x3 -> a ; x4 -> nil2 ; z -> a }) ------------------------------------------- Step 5, which took 0.013440 s (model generation: 0.012959, model checking: 0.000481): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035}, Q_f={q_gen_8026}, Delta= { () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8029 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8029, q_gen_8029) -> q_gen_8035 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 3 () -> zip([nil2, y, nil]) -> 3 () -> zip_concat([x, y, nil2, nil]) -> 3 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 4 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 5 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 4 } Sat witness: Found: ((zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]), { _lda -> cons(pair2(b, b), nil) ; _mda -> nil ; x -> a ; xs -> nil2 ; y -> a ; ys -> nil2 }) ------------------------------------------- Step 6, which took 0.010910 s (model generation: 0.010427, model checking: 0.000483): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 3 () -> zip([nil2, y, nil]) -> 3 () -> zip_concat([x, y, nil2, nil]) -> 6 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 4 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 5 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 4 } Sat witness: Found: (() -> zip_concat([x, y, nil2, nil]), { x -> a ; y -> nil2 }) ------------------------------------------- Step 7, which took 0.012720 s (model generation: 0.011860, model checking: 0.000860): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 3 () -> zip([nil2, y, nil]) -> 6 () -> zip_concat([x, y, nil2, nil]) -> 6 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 4 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 5 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 4 } Sat witness: Found: (() -> zip([nil2, y, nil]), { y -> cons2(b, cons2(b, nil2)) }) ------------------------------------------- Step 8, which took 0.014123 s (model generation: 0.013458, model checking: 0.000665): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 6 () -> zip([nil2, y, nil]) -> 6 () -> zip_concat([x, y, nil2, nil]) -> 6 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 4 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 5 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 4 } Sat witness: Found: (() -> zip([cons2(z, x2), nil2, nil]), { x2 -> nil2 ; z -> a }) ------------------------------------------- Step 9, which took 0.011446 s (model generation: 0.010598, model checking: 0.000848): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 6 () -> zip([nil2, y, nil]) -> 6 () -> zip_concat([x, y, nil2, nil]) -> 6 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 4 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 5 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 7 } Sat witness: Found: ((zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]), { _fda -> nil ; x -> b ; y -> nil2 ; y2 -> b ; ys -> nil2 }) ------------------------------------------- Step 10, which took 0.011108 s (model generation: 0.010082, model checking: 0.001026): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 6 () -> zip([nil2, y, nil]) -> 6 () -> zip_concat([x, y, nil2, nil]) -> 6 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 7 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 5 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 7 } Sat witness: Found: ((zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]), { _ada -> nil ; x2 -> nil2 ; x3 -> b ; x4 -> nil2 ; z -> b }) ------------------------------------------- Step 11, which took 0.013465 s (model generation: 0.010715, model checking: 0.002750): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 6 () -> zip([nil2, y, nil]) -> 6 () -> zip_concat([x, y, nil2, nil]) -> 9 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 7 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 6 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 7 } Sat witness: Found: (() -> zip_concat([x, y, nil2, nil]), { x -> b ; y -> cons2(b, nil2) }) ------------------------------------------- Step 12, which took 0.013488 s (model generation: 0.010447, model checking: 0.003041): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 () -> q_gen_8049 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 6 () -> zip([nil2, y, nil]) -> 9 () -> zip_concat([x, y, nil2, nil]) -> 9 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 7 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 7 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 7 } Sat witness: Found: (() -> zip([nil2, y, nil]), { y -> cons2(b, cons2(a, nil2)) }) ------------------------------------------- Step 13, which took 0.012294 s (model generation: 0.011004, model checking: 0.001290): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 (q_gen_8036, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 () -> q_gen_8049 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 7 () -> zip([nil2, y, nil]) -> 9 () -> zip_concat([x, y, nil2, nil]) -> 9 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 7 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 7 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 10 } Sat witness: Found: ((zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]), { _fda -> nil ; x -> a ; y -> cons2(b, nil2) ; y2 -> a ; ys -> nil2 }) ------------------------------------------- Step 14, which took 0.016671 s (model generation: 0.012205, model checking: 0.004466): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 (q_gen_8036, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049, q_gen_8053, q_gen_8054}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 () -> q_gen_8049 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 () -> q_gen_8053 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 7 () -> zip([nil2, y, nil]) -> 9 () -> zip_concat([x, y, nil2, nil]) -> 9 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 10 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 8 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 10 } Sat witness: Found: ((zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]), { _ada -> nil ; x2 -> nil2 ; x3 -> a ; x4 -> nil2 ; z -> b }) ------------------------------------------- Step 15, which took 0.016548 s (model generation: 0.012289, model checking: 0.004259): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 (q_gen_8036, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049, q_gen_8053, q_gen_8054}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 () -> q_gen_8049 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 () -> q_gen_8053 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 8 () -> zip([nil2, y, nil]) -> 9 () -> zip_concat([x, y, nil2, nil]) -> 12 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 10 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 9 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 10 } Sat witness: Found: (() -> zip_concat([x, y, nil2, nil]), { x -> a ; y -> cons2(b, nil2) }) ------------------------------------------- Step 16, which took 0.017042 s (model generation: 0.012725, model checking: 0.004317): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 (q_gen_8036, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049, q_gen_8053, q_gen_8054}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 () -> q_gen_8049 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 () -> q_gen_8053 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 9 () -> zip([nil2, y, nil]) -> 12 () -> zip_concat([x, y, nil2, nil]) -> 12 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 10 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 10 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 10 } Sat witness: Found: (() -> zip([nil2, y, nil]), { y -> cons2(a, nil2) }) ------------------------------------------- Step 17, which took 0.014732 s (model generation: 0.012998, model checking: 0.001734): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 (q_gen_8036, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049, q_gen_8053, q_gen_8054}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 () -> q_gen_8049 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 () -> q_gen_8053 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 10 () -> zip([nil2, y, nil]) -> 12 () -> zip_concat([x, y, nil2, nil]) -> 12 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 10 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 10 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 13 } Sat witness: Found: ((zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]), { _fda -> nil ; x -> b ; y -> cons2(a, nil2) ; y2 -> b ; ys -> nil2 }) ------------------------------------------- Step 18, which took 0.022571 s (model generation: 0.016660, model checking: 0.005911): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 (q_gen_8036, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049, q_gen_8053, q_gen_8054}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 () -> q_gen_8049 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 () -> q_gen_8053 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 10 () -> zip([nil2, y, nil]) -> 12 () -> zip_concat([x, y, nil2, nil]) -> 12 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 13 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 11 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 13 } Sat witness: Found: ((zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]), { _ada -> nil ; x2 -> nil2 ; x3 -> b ; x4 -> nil2 ; z -> a }) ------------------------------------------- Step 19, which took 0.021126 s (model generation: 0.014567, model checking: 0.006559): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 (q_gen_8036, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8036, q_gen_8029) -> q_gen_8035 (q_gen_8029, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049, q_gen_8053, q_gen_8054}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 () -> q_gen_8049 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 () -> q_gen_8053 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 11 () -> zip([nil2, y, nil]) -> 12 () -> zip_concat([x, y, nil2, nil]) -> 15 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 13 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 12 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 13 } Sat witness: Found: (() -> zip_concat([x, y, nil2, nil]), { x -> b ; y -> cons2(b, cons2(b, nil2)) }) ------------------------------------------- Step 20, which took 0.024284 s (model generation: 0.016261, model checking: 0.008023): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 (q_gen_8036, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8036, q_gen_8029) -> q_gen_8035 (q_gen_8029, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049, q_gen_8053, q_gen_8054}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 (q_gen_8033, q_gen_8049) -> q_gen_8049 () -> q_gen_8049 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 () -> q_gen_8053 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 12 () -> zip([nil2, y, nil]) -> 13 () -> zip_concat([x, y, nil2, nil]) -> 15 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 13 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 13 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 16 } Sat witness: Found: ((zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]), { _fda -> nil ; x -> a ; y -> cons2(a, nil2) ; y2 -> a ; ys -> nil2 }) ------------------------------------------- Step 21, which took 0.035455 s (model generation: 0.015304, model checking: 0.020151): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 (q_gen_8036, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8036, q_gen_8029) -> q_gen_8035 (q_gen_8029, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049, q_gen_8053, q_gen_8054}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 (q_gen_8033, q_gen_8049) -> q_gen_8049 () -> q_gen_8049 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 () -> q_gen_8053 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 13 () -> zip([nil2, y, nil]) -> 14 () -> zip_concat([x, y, nil2, nil]) -> 16 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 14 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 14 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 19 } Sat witness: Found: ((zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]), { _fda -> nil ; x -> a ; y -> cons2(b, nil2) ; y2 -> b ; ys -> nil2 }) ------------------------------------------- Step 22, which took 0.035314 s (model generation: 0.017226, model checking: 0.018088): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 (q_gen_8036, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8036, q_gen_8029) -> q_gen_8035 (q_gen_8029, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049, q_gen_8053, q_gen_8054}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 (q_gen_8033, q_gen_8049) -> q_gen_8049 () -> q_gen_8049 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 () -> q_gen_8053 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 14 () -> zip([nil2, y, nil]) -> 15 () -> zip_concat([x, y, nil2, nil]) -> 17 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 15 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 15 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 22 } Sat witness: Found: ((zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]), { _fda -> nil ; x -> b ; y -> nil2 ; y2 -> b ; ys -> cons2(a, nil2) }) ------------------------------------------- Step 23, which took 0.040116 s (model generation: 0.021057, model checking: 0.019059): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 (q_gen_8036, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8036, q_gen_8029) -> q_gen_8035 (q_gen_8029, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049, q_gen_8053, q_gen_8054}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 (q_gen_8033, q_gen_8049) -> q_gen_8049 () -> q_gen_8049 (q_gen_8033, q_gen_8049) -> q_gen_8031 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 () -> q_gen_8053 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 15 () -> zip([nil2, y, nil]) -> 16 () -> zip_concat([x, y, nil2, nil]) -> 18 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 16 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 16 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 25 } Sat witness: Found: ((zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]), { _fda -> nil ; x -> b ; y -> cons2(b, cons2(b, nil2)) ; y2 -> b ; ys -> nil2 }) ------------------------------------------- Step 24, which took 0.047050 s (model generation: 0.020361, model checking: 0.026689): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 (q_gen_8036, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8036, q_gen_8029) -> q_gen_8035 (q_gen_8029, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049, q_gen_8053, q_gen_8054}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 (q_gen_8033, q_gen_8049) -> q_gen_8049 () -> q_gen_8049 (q_gen_8033, q_gen_8049) -> q_gen_8031 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8049) -> q_gen_8053 () -> q_gen_8053 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 16 () -> zip([nil2, y, nil]) -> 17 () -> zip_concat([x, y, nil2, nil]) -> 19 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 17 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 17 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 28 } Sat witness: Found: ((zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]), { _fda -> cons(pair2(a, b), nil) ; x -> b ; y -> cons2(a, nil2) ; y2 -> a ; ys -> cons2(b, nil2) }) ------------------------------------------- Step 25, which took 0.044501 s (model generation: 0.019495, model checking: 0.025006): Model: |_ { zip -> {{{ Q={q_gen_8026, q_gen_8028, q_gen_8029, q_gen_8035, q_gen_8036, q_gen_8037, q_gen_8038}, Q_f={q_gen_8026}, Delta= { (q_gen_8029, q_gen_8028) -> q_gen_8028 (q_gen_8036, q_gen_8028) -> q_gen_8028 () -> q_gen_8028 () -> q_gen_8029 () -> q_gen_8036 (q_gen_8035, q_gen_8026) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 (q_gen_8029, q_gen_8028) -> q_gen_8026 (q_gen_8036, q_gen_8028) -> q_gen_8026 () -> q_gen_8026 (q_gen_8036, q_gen_8036) -> q_gen_8035 (q_gen_8036, q_gen_8029) -> q_gen_8035 (q_gen_8029, q_gen_8036) -> q_gen_8035 (q_gen_8029, q_gen_8029) -> q_gen_8035 (q_gen_8038, q_gen_8026) -> q_gen_8037 (q_gen_8029, q_gen_8029) -> q_gen_8038 } Datatype: Convolution form: left }}} ; zip_concat -> {{{ Q={q_gen_8025, q_gen_8031, q_gen_8032, q_gen_8033, q_gen_8049, q_gen_8053, q_gen_8054}, Q_f={q_gen_8025}, Delta= { () -> q_gen_8033 () -> q_gen_8033 (q_gen_8033, q_gen_8049) -> q_gen_8049 () -> q_gen_8049 (q_gen_8033, q_gen_8049) -> q_gen_8031 () -> q_gen_8031 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8033) -> q_gen_8032 (q_gen_8033, q_gen_8049) -> q_gen_8053 (q_gen_8032, q_gen_8031) -> q_gen_8053 () -> q_gen_8053 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8033, q_gen_8033) -> q_gen_8054 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 (q_gen_8054, q_gen_8053) -> q_gen_8025 (q_gen_8033, q_gen_8049) -> q_gen_8025 (q_gen_8032, q_gen_8031) -> q_gen_8025 () -> q_gen_8025 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair} _| Teacher's answer: New clause system: { () -> zip([cons2(z, x2), nil2, nil]) -> 17 () -> zip([nil2, y, nil]) -> 18 () -> zip_concat([x, y, nil2, nil]) -> 20 (zip([x2, x4, _ada])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _ada)]) -> 18 (zip([xs, ys, _mda]) /\ zip([cons2(x, xs), cons2(y, ys), _lda])) -> eq_list([_lda, cons(pair2(x, y), _mda)]) -> 18 (zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]) -> 31 } Sat witness: Found: ((zip([y, ys, _fda])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _fda)]), { _fda -> cons(pair2(b, b), nil) ; x -> a ; y -> cons2(b, cons2(b, nil2)) ; y2 -> a ; ys -> cons2(b, nil2) }) Total time: 0.584551 Reason for stopping: Proved