Solving ../../benchmarks/false/prefix_append.smt2... Inference procedure has parameters: Ice fuel: 200 Timeout: 60s Convolution: left Learning problem is: env: { elt -> {a, b} ; eltlist -> {cons, nil} } definition: { (prefix, P: {() -> prefix([nil, y]) (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT (prefix([cons(z, zs), nil])) -> BOT} ) (append, F: {() -> append([nil, l2, l2]) (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)])} (append([_gia, _hia, _iia]) /\ append([_gia, _hia, _jia])) -> eq_eltlist([_iia, _jia]) ) } properties: {(append([l1, l2, _kia])) -> prefix([l2, _kia])} over-approximation: {append} under-approximation: {prefix} Clause system for inference is: { () -> append([nil, l2, l2]) -> 0 () -> prefix([nil, y]) -> 0 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 0 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 0 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 0 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 0 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 0 (prefix([cons(z, zs), nil])) -> BOT -> 0 } Solving took 0.631172 seconds. Disproved ------------------- STEPS: ------------------------------------------- Step 0, which took 0.016926 s (model generation: 0.016296, model checking: 0.000630): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 () -> prefix([nil, y]) -> 3 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 1 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 1 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 1 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 1 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 1 (prefix([cons(z, zs), nil])) -> BOT -> 1 } Sat witness: Found: (() -> prefix([nil, y]), { y -> nil }) ------------------------------------------- Step 1, which took 0.017623 s (model generation: 0.017321, model checking: 0.000302): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846}, Q_f={q_gen_8846}, Delta= { () -> q_gen_8846 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> prefix([nil, y]) -> 3 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 1 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 1 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 1 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 1 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 1 (prefix([cons(z, zs), nil])) -> BOT -> 1 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> nil }) ------------------------------------------- Step 2, which took 0.017464 s (model generation: 0.017087, model checking: 0.000377): Model: |_ { append -> {{{ Q={q_gen_8847}, Q_f={q_gen_8847}, Delta= { () -> q_gen_8847 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846}, Q_f={q_gen_8846}, Delta= { () -> q_gen_8846 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> prefix([nil, y]) -> 3 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 1 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 1 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 2 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 2 (prefix([cons(z, zs), nil])) -> BOT -> 2 } Sat witness: Found: ((prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]), { y2 -> b ; ys -> nil ; zs -> nil }) ------------------------------------------- Step 3, which took 0.018414 s (model generation: 0.017934, model checking: 0.000480): Model: |_ { append -> {{{ Q={q_gen_8847}, Q_f={q_gen_8847}, Delta= { () -> q_gen_8847 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849}, Q_f={q_gen_8846}, Delta= { (q_gen_8849, q_gen_8846) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> prefix([nil, y]) -> 3 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 1 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 4 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 2 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 2 (prefix([cons(z, zs), nil])) -> BOT -> 2 } Sat witness: Found: ((append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]), { _fia -> nil ; h1 -> b ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 4, which took 0.017851 s (model generation: 0.017585, model checking: 0.000266): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8851, q_gen_8852}, Q_f={q_gen_8847}, Delta= { () -> q_gen_8851 () -> q_gen_8852 (q_gen_8852, q_gen_8851) -> q_gen_8847 () -> q_gen_8847 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849}, Q_f={q_gen_8846}, Delta= { (q_gen_8849, q_gen_8846) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> prefix([nil, y]) -> 3 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 4 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 4 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 2 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 2 (prefix([cons(z, zs), nil])) -> BOT -> 2 } Sat witness: Found: ((append([l1, l2, _kia])) -> prefix([l2, _kia]), { _kia -> cons(b, nil) ; l1 -> cons(b, nil) ; l2 -> nil }) ------------------------------------------- Step 5, which took 0.023865 s (model generation: 0.018696, model checking: 0.005169): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8851, q_gen_8852}, Q_f={q_gen_8847}, Delta= { () -> q_gen_8851 () -> q_gen_8852 (q_gen_8852, q_gen_8851) -> q_gen_8847 () -> q_gen_8847 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849, q_gen_8854, q_gen_8855}, Q_f={q_gen_8846}, Delta= { () -> q_gen_8854 () -> q_gen_8855 (q_gen_8849, q_gen_8846) -> q_gen_8846 (q_gen_8855, q_gen_8854) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> prefix([nil, y]) -> 6 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 4 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 4 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 3 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 3 (prefix([cons(z, zs), nil])) -> BOT -> 3 } Sat witness: Found: (() -> prefix([nil, y]), { y -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 6, which took 0.022028 s (model generation: 0.019743, model checking: 0.002285): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8851, q_gen_8852}, Q_f={q_gen_8847}, Delta= { () -> q_gen_8851 () -> q_gen_8852 (q_gen_8852, q_gen_8851) -> q_gen_8847 () -> q_gen_8847 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849, q_gen_8854, q_gen_8855}, Q_f={q_gen_8846}, Delta= { (q_gen_8855, q_gen_8854) -> q_gen_8854 () -> q_gen_8854 () -> q_gen_8855 () -> q_gen_8855 (q_gen_8849, q_gen_8846) -> q_gen_8846 (q_gen_8855, q_gen_8854) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> prefix([nil, y]) -> 6 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 4 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 4 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 4 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 4 (prefix([cons(z, zs), nil])) -> BOT -> 4 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 7, which took 0.023455 s (model generation: 0.020431, model checking: 0.003024): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8851, q_gen_8852}, Q_f={q_gen_8847}, Delta= { (q_gen_8852, q_gen_8851) -> q_gen_8851 () -> q_gen_8851 () -> q_gen_8852 () -> q_gen_8852 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 () -> q_gen_8847 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849, q_gen_8854, q_gen_8855}, Q_f={q_gen_8846}, Delta= { (q_gen_8855, q_gen_8854) -> q_gen_8854 () -> q_gen_8854 () -> q_gen_8855 () -> q_gen_8855 (q_gen_8849, q_gen_8846) -> q_gen_8846 (q_gen_8855, q_gen_8854) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> prefix([nil, y]) -> 6 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 4 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 4 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 7 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 5 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 5 (prefix([cons(z, zs), nil])) -> BOT -> 5 } Sat witness: Found: ((prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]), { y2 -> a ; ys -> nil ; zs -> nil }) ------------------------------------------- Step 8, which took 0.024131 s (model generation: 0.021095, model checking: 0.003036): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8851, q_gen_8852}, Q_f={q_gen_8847}, Delta= { (q_gen_8852, q_gen_8851) -> q_gen_8851 () -> q_gen_8851 () -> q_gen_8852 () -> q_gen_8852 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 () -> q_gen_8847 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849, q_gen_8854, q_gen_8855}, Q_f={q_gen_8846}, Delta= { (q_gen_8855, q_gen_8854) -> q_gen_8854 () -> q_gen_8854 () -> q_gen_8855 () -> q_gen_8855 (q_gen_8849, q_gen_8846) -> q_gen_8846 (q_gen_8855, q_gen_8854) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 () -> q_gen_8849 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> prefix([nil, y]) -> 6 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 4 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 7 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 7 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 5 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 5 (prefix([cons(z, zs), nil])) -> BOT -> 5 } Sat witness: Found: ((append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]), { _fia -> cons(b, nil) ; h1 -> b ; l2 -> cons(b, nil) ; t1 -> nil }) ------------------------------------------- Step 9, which took 0.030952 s (model generation: 0.023733, model checking: 0.007219): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8851, q_gen_8852, q_gen_8867, q_gen_8868, q_gen_8869}, Q_f={q_gen_8847}, Delta= { () -> q_gen_8867 () -> q_gen_8868 (q_gen_8852, q_gen_8851) -> q_gen_8851 () -> q_gen_8851 () -> q_gen_8852 () -> q_gen_8852 (q_gen_8869, q_gen_8847) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8868, q_gen_8867) -> q_gen_8847 () -> q_gen_8847 () -> q_gen_8869 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849, q_gen_8854, q_gen_8855}, Q_f={q_gen_8846}, Delta= { (q_gen_8855, q_gen_8854) -> q_gen_8854 () -> q_gen_8854 () -> q_gen_8855 () -> q_gen_8855 (q_gen_8849, q_gen_8846) -> q_gen_8846 (q_gen_8855, q_gen_8854) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 () -> q_gen_8849 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 7 () -> prefix([nil, y]) -> 7 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 5 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 10 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 8 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 6 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 6 (prefix([cons(z, zs), nil])) -> BOT -> 6 } Sat witness: Found: ((append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]), { _fia -> cons(b, nil) ; h1 -> b ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 10, which took 0.038281 s (model generation: 0.029283, model checking: 0.008998): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8851, q_gen_8852, q_gen_8867, q_gen_8868, q_gen_8869}, Q_f={q_gen_8847}, Delta= { () -> q_gen_8867 () -> q_gen_8868 (q_gen_8852, q_gen_8851) -> q_gen_8851 (q_gen_8868, q_gen_8867) -> q_gen_8851 () -> q_gen_8851 () -> q_gen_8852 () -> q_gen_8852 (q_gen_8869, q_gen_8847) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8868, q_gen_8867) -> q_gen_8847 () -> q_gen_8847 () -> q_gen_8869 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849, q_gen_8854, q_gen_8855}, Q_f={q_gen_8846}, Delta= { (q_gen_8855, q_gen_8854) -> q_gen_8854 () -> q_gen_8854 () -> q_gen_8855 () -> q_gen_8855 (q_gen_8849, q_gen_8846) -> q_gen_8846 (q_gen_8855, q_gen_8854) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 () -> q_gen_8849 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 8 () -> prefix([nil, y]) -> 8 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 6 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 13 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 9 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 7 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 7 (prefix([cons(z, zs), nil])) -> BOT -> 7 } Sat witness: Found: ((append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]), { _fia -> cons(b, nil) ; h1 -> a ; l2 -> cons(b, nil) ; t1 -> nil }) ------------------------------------------- Step 11, which took 0.030395 s (model generation: 0.028886, model checking: 0.001509): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8851, q_gen_8852, q_gen_8867, q_gen_8868, q_gen_8869}, Q_f={q_gen_8847}, Delta= { () -> q_gen_8867 () -> q_gen_8868 (q_gen_8852, q_gen_8851) -> q_gen_8851 (q_gen_8868, q_gen_8867) -> q_gen_8851 () -> q_gen_8851 () -> q_gen_8852 () -> q_gen_8852 (q_gen_8869, q_gen_8847) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8868, q_gen_8867) -> q_gen_8847 () -> q_gen_8847 () -> q_gen_8869 () -> q_gen_8869 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849, q_gen_8854, q_gen_8855}, Q_f={q_gen_8846}, Delta= { (q_gen_8855, q_gen_8854) -> q_gen_8854 () -> q_gen_8854 () -> q_gen_8855 () -> q_gen_8855 (q_gen_8849, q_gen_8846) -> q_gen_8846 (q_gen_8855, q_gen_8854) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 () -> q_gen_8849 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 8 () -> prefix([nil, y]) -> 8 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 9 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 13 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 9 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 7 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 7 (prefix([cons(z, zs), nil])) -> BOT -> 7 } Sat witness: Found: ((append([l1, l2, _kia])) -> prefix([l2, _kia]), { _kia -> cons(a, nil) ; l1 -> cons(a, nil) ; l2 -> cons(b, nil) }) ------------------------------------------- Step 12, which took 0.031046 s (model generation: 0.030799, model checking: 0.000247): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8851, q_gen_8852, q_gen_8867, q_gen_8868, q_gen_8869}, Q_f={q_gen_8847}, Delta= { () -> q_gen_8867 () -> q_gen_8868 (q_gen_8852, q_gen_8851) -> q_gen_8851 (q_gen_8868, q_gen_8867) -> q_gen_8851 () -> q_gen_8851 () -> q_gen_8852 () -> q_gen_8852 (q_gen_8869, q_gen_8847) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8868, q_gen_8867) -> q_gen_8847 () -> q_gen_8847 () -> q_gen_8869 () -> q_gen_8869 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849, q_gen_8854, q_gen_8855}, Q_f={q_gen_8846}, Delta= { (q_gen_8855, q_gen_8854) -> q_gen_8854 () -> q_gen_8854 () -> q_gen_8855 () -> q_gen_8855 (q_gen_8849, q_gen_8846) -> q_gen_8846 (q_gen_8855, q_gen_8854) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 () -> q_gen_8849 () -> q_gen_8849 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 8 () -> prefix([nil, y]) -> 8 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 9 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 13 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 9 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 7 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 10 (prefix([cons(z, zs), nil])) -> BOT -> 8 } Sat witness: Found: ((prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT, { y2 -> a ; ys -> nil ; z -> b ; zs -> nil }) ------------------------------------------- Step 13, which took 0.049906 s (model generation: 0.038375, model checking: 0.011531): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8851, q_gen_8852, q_gen_8866, q_gen_8867, q_gen_8868, q_gen_8869}, Q_f={q_gen_8847}, Delta= { () -> q_gen_8867 () -> q_gen_8868 (q_gen_8852, q_gen_8851) -> q_gen_8851 (q_gen_8868, q_gen_8867) -> q_gen_8851 () -> q_gen_8851 () -> q_gen_8852 () -> q_gen_8852 (q_gen_8869, q_gen_8866) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 () -> q_gen_8847 (q_gen_8869, q_gen_8847) -> q_gen_8866 (q_gen_8868, q_gen_8867) -> q_gen_8866 () -> q_gen_8869 () -> q_gen_8869 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849, q_gen_8854, q_gen_8855, q_gen_8875, q_gen_8876}, Q_f={q_gen_8846}, Delta= { (q_gen_8855, q_gen_8854) -> q_gen_8854 () -> q_gen_8854 () -> q_gen_8855 () -> q_gen_8855 (q_gen_8849, q_gen_8846) -> q_gen_8846 (q_gen_8855, q_gen_8854) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 () -> q_gen_8849 (q_gen_8876, q_gen_8846) -> q_gen_8875 () -> q_gen_8876 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 9 () -> prefix([nil, y]) -> 9 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 12 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 13 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 10 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 8 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 10 (prefix([cons(z, zs), nil])) -> BOT -> 9 } Sat witness: Found: ((append([l1, l2, _kia])) -> prefix([l2, _kia]), { _kia -> cons(a, cons(b, nil)) ; l1 -> cons(a, nil) ; l2 -> cons(b, nil) }) ------------------------------------------- Step 14, which took 0.045273 s (model generation: 0.034986, model checking: 0.010287): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8851, q_gen_8852, q_gen_8866, q_gen_8867, q_gen_8868, q_gen_8869}, Q_f={q_gen_8847}, Delta= { () -> q_gen_8867 () -> q_gen_8868 (q_gen_8852, q_gen_8851) -> q_gen_8851 (q_gen_8868, q_gen_8867) -> q_gen_8851 () -> q_gen_8851 () -> q_gen_8852 () -> q_gen_8852 (q_gen_8869, q_gen_8866) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 () -> q_gen_8847 (q_gen_8869, q_gen_8847) -> q_gen_8866 (q_gen_8868, q_gen_8867) -> q_gen_8866 () -> q_gen_8869 () -> q_gen_8869 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8848, q_gen_8849, q_gen_8854, q_gen_8855, q_gen_8875, q_gen_8876}, Q_f={q_gen_8846, q_gen_8848}, Delta= { (q_gen_8855, q_gen_8854) -> q_gen_8854 () -> q_gen_8854 () -> q_gen_8855 () -> q_gen_8855 (q_gen_8876, q_gen_8848) -> q_gen_8846 () -> q_gen_8846 (q_gen_8849, q_gen_8846) -> q_gen_8848 (q_gen_8855, q_gen_8854) -> q_gen_8848 () -> q_gen_8849 () -> q_gen_8849 (q_gen_8876, q_gen_8846) -> q_gen_8875 () -> q_gen_8876 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 10 () -> prefix([nil, y]) -> 10 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 12 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 13 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 10 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 9 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 13 (prefix([cons(z, zs), nil])) -> BOT -> 10 } Sat witness: Found: ((prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT, { y2 -> a ; ys -> cons(b, nil) ; z -> b ; zs -> cons(b, nil) }) ------------------------------------------- Step 15, which took 0.042969 s (model generation: 0.030777, model checking: 0.012192): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8851, q_gen_8852, q_gen_8866, q_gen_8867, q_gen_8868, q_gen_8869}, Q_f={q_gen_8847}, Delta= { () -> q_gen_8867 () -> q_gen_8868 (q_gen_8852, q_gen_8851) -> q_gen_8851 (q_gen_8868, q_gen_8867) -> q_gen_8851 () -> q_gen_8851 () -> q_gen_8852 () -> q_gen_8852 (q_gen_8869, q_gen_8866) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 () -> q_gen_8847 (q_gen_8869, q_gen_8847) -> q_gen_8866 (q_gen_8868, q_gen_8867) -> q_gen_8866 () -> q_gen_8869 () -> q_gen_8869 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849, q_gen_8853, q_gen_8854, q_gen_8855, q_gen_8875, q_gen_8876}, Q_f={q_gen_8846, q_gen_8853}, Delta= { (q_gen_8855, q_gen_8854) -> q_gen_8854 () -> q_gen_8854 () -> q_gen_8855 () -> q_gen_8855 (q_gen_8849, q_gen_8846) -> q_gen_8846 (q_gen_8876, q_gen_8853) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 () -> q_gen_8849 (q_gen_8855, q_gen_8854) -> q_gen_8853 (q_gen_8876, q_gen_8846) -> q_gen_8875 () -> q_gen_8876 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 10 () -> prefix([nil, y]) -> 10 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 12 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 13 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 13 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 10 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 13 (prefix([cons(z, zs), nil])) -> BOT -> 11 } Sat witness: Found: ((prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]), { y2 -> b ; ys -> cons(a, nil) ; zs -> nil }) ------------------------------------------- Step 16, which took 0.053330 s (model generation: 0.037830, model checking: 0.015500): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8851, q_gen_8852, q_gen_8866, q_gen_8867, q_gen_8868, q_gen_8869}, Q_f={q_gen_8847}, Delta= { () -> q_gen_8867 () -> q_gen_8868 (q_gen_8852, q_gen_8851) -> q_gen_8851 (q_gen_8868, q_gen_8867) -> q_gen_8851 () -> q_gen_8851 () -> q_gen_8852 () -> q_gen_8852 (q_gen_8869, q_gen_8866) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8852, q_gen_8851) -> q_gen_8847 () -> q_gen_8847 (q_gen_8869, q_gen_8847) -> q_gen_8866 (q_gen_8868, q_gen_8867) -> q_gen_8866 () -> q_gen_8869 () -> q_gen_8869 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849, q_gen_8853, q_gen_8854, q_gen_8855, q_gen_8875, q_gen_8876}, Q_f={q_gen_8846, q_gen_8853}, Delta= { (q_gen_8855, q_gen_8854) -> q_gen_8854 () -> q_gen_8854 () -> q_gen_8855 () -> q_gen_8855 (q_gen_8849, q_gen_8846) -> q_gen_8846 (q_gen_8849, q_gen_8853) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 () -> q_gen_8849 (q_gen_8876, q_gen_8853) -> q_gen_8853 (q_gen_8855, q_gen_8854) -> q_gen_8853 (q_gen_8876, q_gen_8846) -> q_gen_8875 () -> q_gen_8876 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 11 () -> prefix([nil, y]) -> 11 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 15 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 13 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 13 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 11 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 13 (prefix([cons(z, zs), nil])) -> BOT -> 12 } Sat witness: Found: ((append([l1, l2, _kia])) -> prefix([l2, _kia]), { _kia -> cons(a, cons(b, nil)) ; l1 -> cons(a, cons(b, nil)) ; l2 -> cons(b, cons(b, nil)) }) ------------------------------------------- Step 17, which took 0.041126 s (model generation: 0.036212, model checking: 0.004914): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8851, q_gen_8852, q_gen_8861, q_gen_8864, q_gen_8867, q_gen_8868, q_gen_8869}, Q_f={q_gen_8847}, Delta= { () -> q_gen_8867 () -> q_gen_8868 (q_gen_8861, q_gen_8851) -> q_gen_8851 (q_gen_8868, q_gen_8867) -> q_gen_8851 () -> q_gen_8851 () -> q_gen_8852 () -> q_gen_8861 (q_gen_8852, q_gen_8851) -> q_gen_8847 (q_gen_8861, q_gen_8851) -> q_gen_8847 () -> q_gen_8847 (q_gen_8869, q_gen_8847) -> q_gen_8864 (q_gen_8869, q_gen_8864) -> q_gen_8864 (q_gen_8852, q_gen_8851) -> q_gen_8864 (q_gen_8868, q_gen_8867) -> q_gen_8864 () -> q_gen_8869 () -> q_gen_8869 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849, q_gen_8854, q_gen_8855, q_gen_8875, q_gen_8876}, Q_f={q_gen_8846}, Delta= { (q_gen_8855, q_gen_8854) -> q_gen_8854 () -> q_gen_8854 () -> q_gen_8855 () -> q_gen_8855 (q_gen_8849, q_gen_8846) -> q_gen_8846 (q_gen_8855, q_gen_8854) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 () -> q_gen_8849 (q_gen_8876, q_gen_8846) -> q_gen_8875 () -> q_gen_8876 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 14 () -> prefix([nil, y]) -> 12 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 15 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 13 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 13 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 12 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 13 (prefix([cons(z, zs), nil])) -> BOT -> 12 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(b, nil) }) ------------------------------------------- Step 18, which took 0.051448 s (model generation: 0.037047, model checking: 0.014401): Model: |_ { append -> {{{ Q={q_gen_8847, q_gen_8850, q_gen_8851, q_gen_8852, q_gen_8867, q_gen_8868, q_gen_8869, q_gen_8874}, Q_f={q_gen_8847, q_gen_8850}, Delta= { () -> q_gen_8867 () -> q_gen_8868 (q_gen_8852, q_gen_8851) -> q_gen_8851 (q_gen_8868, q_gen_8867) -> q_gen_8851 () -> q_gen_8851 () -> q_gen_8852 () -> q_gen_8852 () -> q_gen_8847 (q_gen_8869, q_gen_8850) -> q_gen_8850 (q_gen_8852, q_gen_8851) -> q_gen_8850 (q_gen_8852, q_gen_8851) -> q_gen_8850 (q_gen_8868, q_gen_8867) -> q_gen_8850 () -> q_gen_8869 () -> q_gen_8869 (q_gen_8869, q_gen_8847) -> q_gen_8874 (q_gen_8869, q_gen_8874) -> q_gen_8874 } Datatype: Convolution form: left }}} ; prefix -> {{{ Q={q_gen_8846, q_gen_8849, q_gen_8853, q_gen_8854, q_gen_8855, q_gen_8875, q_gen_8876}, Q_f={q_gen_8846, q_gen_8853}, Delta= { (q_gen_8855, q_gen_8854) -> q_gen_8854 () -> q_gen_8854 () -> q_gen_8855 () -> q_gen_8855 (q_gen_8849, q_gen_8846) -> q_gen_8846 () -> q_gen_8846 () -> q_gen_8849 () -> q_gen_8849 (q_gen_8849, q_gen_8853) -> q_gen_8853 (q_gen_8876, q_gen_8853) -> q_gen_8853 (q_gen_8855, q_gen_8854) -> q_gen_8853 (q_gen_8876, q_gen_8846) -> q_gen_8875 () -> q_gen_8876 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 14 () -> prefix([nil, y]) -> 13 (append([l1, l2, _kia])) -> prefix([l2, _kia]) -> 15 (append([t1, l2, _fia])) -> append([cons(h1, t1), l2, cons(h1, _fia)]) -> 13 (prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 13 (prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 13 (prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 16 (prefix([cons(z, zs), nil])) -> BOT -> 13 } Sat witness: Found: ((prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT, { y2 -> a ; ys -> cons(b, nil) ; z -> b ; zs -> nil }) Total time: 0.631172 Reason for stopping: Disproved