Solving ../../benchmarks/true/isaplanner_prop49.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(butlast, F:
{() -> butlast([cons(y, nil), nil])
() -> butlast([nil, nil])
(butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)])}
(butlast([_th, _uh]) /\ butlast([_th, _vh])) -> eq_eltlist([_uh, _vh])
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)])}
(append([_xh, _yh, _ai]) /\ append([_xh, _yh, _zh])) -> eq_eltlist([_zh, _ai])
)
(butlastconcat, F:
{(append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di])
(butlast([x, _bi])) -> butlastconcat([x, nil, _bi])}
(butlastconcat([_ei, _fi, _gi]) /\ butlastconcat([_ei, _fi, _hi])) -> eq_eltlist([_gi, _hi])
)
}

properties:
{(append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki])}


over-approximation: {append, butlast, butlastconcat}
under-approximation: {}

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0  ;  () -> butlast([cons(y, nil), nil]) -> 0  ;  () -> butlast([nil, nil]) -> 0  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 0  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 0  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 0  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 0  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 0
}


Solving took 30.003531 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2459, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463, q_gen_2466, q_gen_2467, q_gen_2468, q_gen_2469, q_gen_2476, q_gen_2482, q_gen_2483, q_gen_2484, q_gen_2485, q_gen_2486, q_gen_2487, q_gen_2488, q_gen_2489, q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2493, q_gen_2505, q_gen_2506, q_gen_2507, q_gen_2508, q_gen_2509, q_gen_2510, q_gen_2511, q_gen_2512},
Q_f={},
Delta=
{
<nil>() -> q_gen_2486
<a>() -> q_gen_2487
<b>() -> q_gen_2492
<cons>(q_gen_2492, q_gen_2486) -> q_gen_2511
<nil, nil>() -> q_gen_2460
<nil, b>() -> q_gen_2461
<b, nil>() -> q_gen_2462
<b, b>() -> q_gen_2463
<nil, a>() -> q_gen_2467
<a, nil>() -> q_gen_2468
<a, a>() -> q_gen_2469
<cons, cons>(q_gen_2469, q_gen_2468, q_gen_2467, q_gen_2460) -> q_gen_2484
<cons, b>(q_gen_2487, q_gen_2486) -> q_gen_2485
<b, cons>(q_gen_2487, q_gen_2486) -> q_gen_2488
<cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2490
<cons, b>(q_gen_2492, q_gen_2486) -> q_gen_2491
<b, cons>(q_gen_2492, q_gen_2486) -> q_gen_2493
<cons, a>(q_gen_2492, q_gen_2486) -> q_gen_2506
<a, cons>(q_gen_2492, q_gen_2486) -> q_gen_2507
<cons, cons>(q_gen_2463, q_gen_2493, q_gen_2491, q_gen_2490) -> q_gen_2509
<cons, b>(q_gen_2492, q_gen_2511) -> q_gen_2510
<b, cons>(q_gen_2492, q_gen_2511) -> q_gen_2512
<nil, nil, nil>() -> q_gen_2450
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2459
<nil, cons, cons>(q_gen_2469, q_gen_2468, q_gen_2467, q_gen_2460) -> q_gen_2466
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2476
<cons, nil, cons>(q_gen_2469, q_gen_2468, q_gen_2467, q_gen_2460) -> q_gen_2482
<cons, nil, cons>(q_gen_2463, q_gen_2488, q_gen_2485, q_gen_2484) -> q_gen_2483
<nil, cons, cons>(q_gen_2463, q_gen_2493, q_gen_2491, q_gen_2490) -> q_gen_2489
<cons, nil, cons>(q_gen_2469, q_gen_2507, q_gen_2506, q_gen_2490) -> q_gen_2505
<nil, cons, cons>(q_gen_2463, q_gen_2512, q_gen_2510, q_gen_2509) -> q_gen_2508
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2447, q_gen_2448, q_gen_2449, q_gen_2451, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2464, q_gen_2465, q_gen_2470, q_gen_2471, q_gen_2472, q_gen_2473, q_gen_2494, q_gen_2495, q_gen_2496, q_gen_2497, q_gen_2498, q_gen_2513, q_gen_2514, q_gen_2515},
Q_f={},
Delta=
{
<nil>() -> q_gen_2448
<b>() -> q_gen_2449
<a>() -> q_gen_2465
<cons>(q_gen_2449, q_gen_2448) -> q_gen_2496
<nil, nil>() -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2447
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2447) -> q_gen_2451
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<b, nil>() -> q_gen_2453
<b, b>() -> q_gen_2454
<cons, nil>(q_gen_2465, q_gen_2448) -> q_gen_2464
<cons, cons>(q_gen_2473, q_gen_2472, q_gen_2471, q_gen_2447) -> q_gen_2470
<cons, a>(q_gen_2449, q_gen_2448) -> q_gen_2471
<a, nil>() -> q_gen_2472
<a, a>() -> q_gen_2473
<cons, cons>(q_gen_2454, q_gen_2497, q_gen_2495, q_gen_2451) -> q_gen_2494
<cons, b>(q_gen_2449, q_gen_2496) -> q_gen_2495
<b, cons>(q_gen_2449, q_gen_2448) -> q_gen_2497
<cons, nil>(q_gen_2449, q_gen_2496) -> q_gen_2498
<cons, cons>(q_gen_2473, q_gen_2515, q_gen_2514, q_gen_2451) -> q_gen_2513
<cons, a>(q_gen_2449, q_gen_2496) -> q_gen_2514
<a, cons>(q_gen_2449, q_gen_2448) -> q_gen_2515
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2456, q_gen_2457, q_gen_2458, q_gen_2474, q_gen_2475, q_gen_2477, q_gen_2478, q_gen_2479, q_gen_2480, q_gen_2481, q_gen_2499, q_gen_2500, q_gen_2501, q_gen_2502, q_gen_2503, q_gen_2504, q_gen_2516, q_gen_2517},
Q_f={},
Delta=
{
<nil>() -> q_gen_2457
<b>() -> q_gen_2458
<a>() -> q_gen_2475
<cons>(q_gen_2458, q_gen_2457) -> q_gen_2500
<cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2478
<cons, b>(q_gen_2458, q_gen_2457) -> q_gen_2479
<b, nil>() -> q_gen_2480
<b, b>() -> q_gen_2481
<cons, a>(q_gen_2458, q_gen_2457) -> q_gen_2502
<a, nil>() -> q_gen_2503
<a, a>() -> q_gen_2504
<nil, nil, nil>() -> q_gen_2455
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2456
<cons, nil, nil>(q_gen_2475, q_gen_2457) -> q_gen_2474
<nil, cons, cons>(q_gen_2481, q_gen_2480, q_gen_2479, q_gen_2478) -> q_gen_2477
<cons, nil, nil>(q_gen_2458, q_gen_2500) -> q_gen_2499
<nil, cons, cons>(q_gen_2504, q_gen_2503, q_gen_2502, q_gen_2478) -> q_gen_2501
<cons, nil, cons>(q_gen_2481, q_gen_2480, q_gen_2479, q_gen_2478) -> q_gen_2516
<nil, cons, nil>(q_gen_2458, q_gen_2500) -> q_gen_2517
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005099 s (model generation: 0.004054,  model checking: 0.001045):

Model:
|_
{
append -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> butlast([cons(y, nil), nil]) -> 0  ;  () -> butlast([nil, nil]) -> 3  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 1  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 1  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 1  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 1  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 1
}
Sat witness: Yes: (() -> butlast([nil, nil]), {

})

-------------------------------------------
Step 1, which took 0.003673 s (model generation: 0.003591,  model checking: 0.000082):

Model:
|_
{
append -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446},
Q_f={q_gen_2446},
Delta=
{
<nil, nil>() -> q_gen_2446
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> butlast([cons(y, nil), nil]) -> 3  ;  () -> butlast([nil, nil]) -> 3  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 1  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 1  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 1  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 1  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 1
}
Sat witness: Yes: (() -> butlast([cons(y, nil), nil]), {
y -> b
})

-------------------------------------------
Step 2, which took 0.003787 s (model generation: 0.003490,  model checking: 0.000297):

Model:
|_
{
append -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<b>() -> q_gen_2449
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> butlast([cons(y, nil), nil]) -> 3  ;  () -> butlast([nil, nil]) -> 3  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 1  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 1  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 1  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 1  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 1
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 3, which took 0.003992 s (model generation: 0.003545,  model checking: 0.000447):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450},
Q_f={q_gen_2450},
Delta=
{
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<b>() -> q_gen_2449
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> butlast([cons(y, nil), nil]) -> 3  ;  () -> butlast([nil, nil]) -> 3  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 1  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 1  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 1  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 1  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 4
}
Sat witness: Yes: ((butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]), {
_sh -> nil  ;  x2 -> b  ;  x3 -> nil  ;  y -> b
})

-------------------------------------------
Step 4, which took 0.003901 s (model generation: 0.003620,  model checking: 0.000281):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450},
Q_f={q_gen_2450},
Delta=
{
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<b>() -> q_gen_2449
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<b, nil>() -> q_gen_2453
<b, b>() -> q_gen_2454
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> butlast([cons(y, nil), nil]) -> 3  ;  () -> butlast([nil, nil]) -> 3  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 1  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 1  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 1  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 4  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 4
}
Sat witness: Yes: ((butlast([x, _bi])) -> butlastconcat([x, nil, _bi]), {
_bi -> nil  ;  x -> nil
})

-------------------------------------------
Step 5, which took 0.005279 s (model generation: 0.004604,  model checking: 0.000675):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450},
Q_f={q_gen_2450},
Delta=
{
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<b>() -> q_gen_2449
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<b, nil>() -> q_gen_2453
<b, b>() -> q_gen_2454
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455},
Q_f={q_gen_2455},
Delta=
{
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> butlast([cons(y, nil), nil]) -> 3  ;  () -> butlast([nil, nil]) -> 3  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 1  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 4  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 2  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 4  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 4
}
Sat witness: Yes: ((append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]), {
_ci -> nil  ;  _di -> nil  ;  x -> nil  ;  x2 -> nil  ;  z -> b
})

-------------------------------------------
Step 6, which took 0.008570 s (model generation: 0.007526,  model checking: 0.001044):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450},
Q_f={q_gen_2450},
Delta=
{
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<b>() -> q_gen_2449
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<b, nil>() -> q_gen_2453
<b, b>() -> q_gen_2454
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458},
Q_f={q_gen_2455},
Delta=
{
<nil>() -> q_gen_2457
<b>() -> q_gen_2458
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> butlast([cons(y, nil), nil]) -> 3  ;  () -> butlast([nil, nil]) -> 3  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 4  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 4  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 2  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 4  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 4
}
Sat witness: Yes: ((append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]), {
_wh -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.010796 s (model generation: 0.010377,  model checking: 0.000419):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463},
Q_f={q_gen_2450},
Delta=
{
<nil, nil>() -> q_gen_2460
<nil, b>() -> q_gen_2461
<b, nil>() -> q_gen_2462
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<b>() -> q_gen_2449
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<b, nil>() -> q_gen_2453
<b, b>() -> q_gen_2454
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458},
Q_f={q_gen_2455},
Delta=
{
<nil>() -> q_gen_2457
<b>() -> q_gen_2458
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> butlast([cons(y, nil), nil]) -> 6  ;  () -> butlast([nil, nil]) -> 4  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 4  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 4  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 3  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 4  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 4
}
Sat witness: Yes: (() -> butlast([cons(y, nil), nil]), {
y -> a
})

-------------------------------------------
Step 8, which took 0.010346 s (model generation: 0.009053,  model checking: 0.001293):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463},
Q_f={q_gen_2450},
Delta=
{
<nil, nil>() -> q_gen_2460
<nil, b>() -> q_gen_2461
<b, nil>() -> q_gen_2462
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<b, nil>() -> q_gen_2453
<b, b>() -> q_gen_2454
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458},
Q_f={q_gen_2455},
Delta=
{
<nil>() -> q_gen_2457
<b>() -> q_gen_2458
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> butlast([cons(y, nil), nil]) -> 6  ;  () -> butlast([nil, nil]) -> 4  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 4  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 4  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 4  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 4  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 4
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 9, which took 0.008843 s (model generation: 0.008195,  model checking: 0.000648):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463},
Q_f={q_gen_2450},
Delta=
{
<nil, nil>() -> q_gen_2460
<nil, a>() -> q_gen_2461
<nil, b>() -> q_gen_2461
<a, nil>() -> q_gen_2462
<b, nil>() -> q_gen_2462
<a, a>() -> q_gen_2463
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<b, nil>() -> q_gen_2453
<b, b>() -> q_gen_2454
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458},
Q_f={q_gen_2455},
Delta=
{
<nil>() -> q_gen_2457
<b>() -> q_gen_2458
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> butlast([cons(y, nil), nil]) -> 6  ;  () -> butlast([nil, nil]) -> 4  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 4  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 4  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 4  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 4  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 7
}
Sat witness: Yes: ((butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]), {
_sh -> nil  ;  x2 -> b  ;  x3 -> nil  ;  y -> a
})

-------------------------------------------
Step 10, which took 0.009099 s (model generation: 0.008539,  model checking: 0.000560):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463},
Q_f={q_gen_2450},
Delta=
{
<nil, nil>() -> q_gen_2460
<nil, a>() -> q_gen_2461
<nil, b>() -> q_gen_2461
<a, nil>() -> q_gen_2462
<b, nil>() -> q_gen_2462
<a, a>() -> q_gen_2463
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, a>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<a, nil>() -> q_gen_2453
<b, nil>() -> q_gen_2453
<a, a>() -> q_gen_2454
<b, b>() -> q_gen_2454
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458},
Q_f={q_gen_2455},
Delta=
{
<nil>() -> q_gen_2457
<b>() -> q_gen_2458
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> butlast([cons(y, nil), nil]) -> 6  ;  () -> butlast([nil, nil]) -> 4  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 4  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 4  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 4  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 7  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 7
}
Sat witness: Yes: ((butlast([x, _bi])) -> butlastconcat([x, nil, _bi]), {
_bi -> nil  ;  x -> cons(a, nil)
})

-------------------------------------------
Step 11, which took 0.009394 s (model generation: 0.008187,  model checking: 0.001207):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463},
Q_f={q_gen_2450},
Delta=
{
<nil, nil>() -> q_gen_2460
<nil, a>() -> q_gen_2461
<nil, b>() -> q_gen_2461
<a, nil>() -> q_gen_2462
<b, nil>() -> q_gen_2462
<a, a>() -> q_gen_2463
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, a>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<a, nil>() -> q_gen_2453
<b, nil>() -> q_gen_2453
<a, a>() -> q_gen_2454
<b, b>() -> q_gen_2454
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458},
Q_f={q_gen_2455},
Delta=
{
<nil>() -> q_gen_2457
<a>() -> q_gen_2458
<b>() -> q_gen_2458
<cons, nil, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> butlast([cons(y, nil), nil]) -> 6  ;  () -> butlast([nil, nil]) -> 4  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 4  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 7  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 5  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 7  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 7
}
Sat witness: Yes: ((append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]), {
_ci -> cons(b, nil)  ;  _di -> cons(b, nil)  ;  x -> nil  ;  x2 -> cons(b, nil)  ;  z -> b
})

-------------------------------------------
Step 12, which took 0.008641 s (model generation: 0.004705,  model checking: 0.003936):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463},
Q_f={q_gen_2450},
Delta=
{
<nil, nil>() -> q_gen_2460
<nil, a>() -> q_gen_2461
<nil, b>() -> q_gen_2461
<a, nil>() -> q_gen_2462
<b, nil>() -> q_gen_2462
<a, a>() -> q_gen_2463
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, a>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<a, nil>() -> q_gen_2453
<b, nil>() -> q_gen_2453
<a, a>() -> q_gen_2454
<b, b>() -> q_gen_2454
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458, q_gen_2478, q_gen_2479, q_gen_2480, q_gen_2481},
Q_f={q_gen_2455},
Delta=
{
<nil>() -> q_gen_2457
<a>() -> q_gen_2458
<b>() -> q_gen_2458
<cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2478
<cons, b>(q_gen_2458, q_gen_2457) -> q_gen_2479
<b, nil>() -> q_gen_2480
<b, b>() -> q_gen_2481
<cons, nil, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, cons, cons>(q_gen_2481, q_gen_2480, q_gen_2479, q_gen_2478) -> q_gen_2455
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> butlast([cons(y, nil), nil]) -> 6  ;  () -> butlast([nil, nil]) -> 4  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 7  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 7  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 5  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 7  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 7
}
Sat witness: Yes: ((append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]), {
_wh -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 13, which took 0.020504 s (model generation: 0.009489,  model checking: 0.011015):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463, q_gen_2486, q_gen_2487},
Q_f={q_gen_2450},
Delta=
{
<nil>() -> q_gen_2486
<a>() -> q_gen_2487
<cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2460
<nil, nil>() -> q_gen_2460
<cons, b>(q_gen_2487, q_gen_2486) -> q_gen_2461
<nil, a>() -> q_gen_2461
<nil, b>() -> q_gen_2461
<a, nil>() -> q_gen_2462
<b, cons>(q_gen_2487, q_gen_2486) -> q_gen_2462
<b, nil>() -> q_gen_2462
<a, a>() -> q_gen_2463
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, a>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<a, nil>() -> q_gen_2453
<b, nil>() -> q_gen_2453
<a, a>() -> q_gen_2454
<b, b>() -> q_gen_2454
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458, q_gen_2478, q_gen_2479, q_gen_2480, q_gen_2481},
Q_f={q_gen_2455},
Delta=
{
<nil>() -> q_gen_2457
<a>() -> q_gen_2458
<b>() -> q_gen_2458
<cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2478
<cons, b>(q_gen_2458, q_gen_2457) -> q_gen_2479
<b, nil>() -> q_gen_2480
<b, b>() -> q_gen_2481
<cons, nil, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, cons, cons>(q_gen_2481, q_gen_2480, q_gen_2479, q_gen_2478) -> q_gen_2455
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> butlast([cons(y, nil), nil]) -> 7  ;  () -> butlast([nil, nil]) -> 5  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 7  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 7  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 6  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 7  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 7
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 14, which took 0.021361 s (model generation: 0.007427,  model checking: 0.013934):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463, q_gen_2486, q_gen_2487},
Q_f={q_gen_2450},
Delta=
{
<nil>() -> q_gen_2486
<a>() -> q_gen_2487
<b>() -> q_gen_2487
<cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2460
<nil, nil>() -> q_gen_2460
<cons, b>(q_gen_2487, q_gen_2486) -> q_gen_2461
<nil, a>() -> q_gen_2461
<nil, b>() -> q_gen_2461
<a, nil>() -> q_gen_2462
<b, cons>(q_gen_2487, q_gen_2486) -> q_gen_2462
<b, nil>() -> q_gen_2462
<a, a>() -> q_gen_2463
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, a>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<a, nil>() -> q_gen_2453
<b, nil>() -> q_gen_2453
<a, a>() -> q_gen_2454
<b, b>() -> q_gen_2454
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458, q_gen_2478, q_gen_2479, q_gen_2480, q_gen_2481},
Q_f={q_gen_2455},
Delta=
{
<nil>() -> q_gen_2457
<a>() -> q_gen_2458
<b>() -> q_gen_2458
<cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2478
<cons, b>(q_gen_2458, q_gen_2457) -> q_gen_2479
<b, nil>() -> q_gen_2480
<b, b>() -> q_gen_2481
<cons, nil, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, cons, cons>(q_gen_2481, q_gen_2480, q_gen_2479, q_gen_2478) -> q_gen_2455
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> butlast([cons(y, nil), nil]) -> 7  ;  () -> butlast([nil, nil]) -> 6  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 7  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 7  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 7  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 7  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 10
}
Sat witness: Yes: ((butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]), {
_sh -> cons(b, nil)  ;  x2 -> b  ;  x3 -> cons(b, nil)  ;  y -> b
})

-------------------------------------------
Step 15, which took 0.007735 s (model generation: 0.006268,  model checking: 0.001467):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463, q_gen_2486, q_gen_2487},
Q_f={q_gen_2450},
Delta=
{
<nil>() -> q_gen_2486
<a>() -> q_gen_2487
<b>() -> q_gen_2487
<cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2460
<nil, nil>() -> q_gen_2460
<cons, b>(q_gen_2487, q_gen_2486) -> q_gen_2461
<nil, a>() -> q_gen_2461
<nil, b>() -> q_gen_2461
<a, nil>() -> q_gen_2462
<b, cons>(q_gen_2487, q_gen_2486) -> q_gen_2462
<b, nil>() -> q_gen_2462
<a, a>() -> q_gen_2463
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2446},
Delta=
{
<cons>(q_gen_2449, q_gen_2448) -> q_gen_2448
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, a>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<a, nil>() -> q_gen_2453
<b, cons>(q_gen_2449, q_gen_2448) -> q_gen_2453
<b, nil>() -> q_gen_2453
<a, a>() -> q_gen_2454
<b, b>() -> q_gen_2454
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458, q_gen_2478, q_gen_2479, q_gen_2480, q_gen_2481},
Q_f={q_gen_2455},
Delta=
{
<nil>() -> q_gen_2457
<a>() -> q_gen_2458
<b>() -> q_gen_2458
<cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2478
<cons, b>(q_gen_2458, q_gen_2457) -> q_gen_2479
<b, nil>() -> q_gen_2480
<b, b>() -> q_gen_2481
<cons, nil, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, cons, cons>(q_gen_2481, q_gen_2480, q_gen_2479, q_gen_2478) -> q_gen_2455
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> butlast([cons(y, nil), nil]) -> 7  ;  () -> butlast([nil, nil]) -> 7  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 7  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 7  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 7  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 10  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 10
}
Sat witness: Yes: ((butlast([x, _bi])) -> butlastconcat([x, nil, _bi]), {
_bi -> nil  ;  x -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 16, which took 0.007901 s (model generation: 0.007137,  model checking: 0.000764):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463, q_gen_2486, q_gen_2487},
Q_f={q_gen_2450},
Delta=
{
<nil>() -> q_gen_2486
<a>() -> q_gen_2487
<b>() -> q_gen_2487
<cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2460
<nil, nil>() -> q_gen_2460
<cons, b>(q_gen_2487, q_gen_2486) -> q_gen_2461
<nil, a>() -> q_gen_2461
<nil, b>() -> q_gen_2461
<a, nil>() -> q_gen_2462
<b, cons>(q_gen_2487, q_gen_2486) -> q_gen_2462
<b, nil>() -> q_gen_2462
<a, a>() -> q_gen_2463
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454},
Q_f={q_gen_2446},
Delta=
{
<cons>(q_gen_2449, q_gen_2448) -> q_gen_2448
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, a>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<a, nil>() -> q_gen_2453
<b, cons>(q_gen_2449, q_gen_2448) -> q_gen_2453
<b, nil>() -> q_gen_2453
<a, a>() -> q_gen_2454
<b, b>() -> q_gen_2454
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458, q_gen_2478, q_gen_2479, q_gen_2480, q_gen_2481},
Q_f={q_gen_2455},
Delta=
{
<cons>(q_gen_2458, q_gen_2457) -> q_gen_2457
<nil>() -> q_gen_2457
<a>() -> q_gen_2458
<b>() -> q_gen_2458
<cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2478
<cons, b>(q_gen_2458, q_gen_2457) -> q_gen_2479
<b, nil>() -> q_gen_2480
<b, b>() -> q_gen_2481
<cons, nil, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, cons, cons>(q_gen_2481, q_gen_2480, q_gen_2479, q_gen_2478) -> q_gen_2455
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> butlast([cons(y, nil), nil]) -> 7  ;  () -> butlast([nil, nil]) -> 7  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 7  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 7  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 10  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 10  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 10
}
Sat witness: Yes: ((append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]), {
_ii -> cons(b, cons(b, nil))  ;  _ji -> nil  ;  _ki -> cons(b, nil)  ;  xs -> nil  ;  ys -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 17, which took 0.019322 s (model generation: 0.012552,  model checking: 0.006770):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463, q_gen_2486, q_gen_2487},
Q_f={q_gen_2450},
Delta=
{
<nil>() -> q_gen_2486
<a>() -> q_gen_2487
<b>() -> q_gen_2487
<cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2460
<nil, nil>() -> q_gen_2460
<cons, b>(q_gen_2487, q_gen_2486) -> q_gen_2461
<nil, a>() -> q_gen_2461
<nil, b>() -> q_gen_2461
<a, nil>() -> q_gen_2462
<b, cons>(q_gen_2487, q_gen_2486) -> q_gen_2462
<b, nil>() -> q_gen_2462
<a, a>() -> q_gen_2463
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2496, q_gen_2498},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons>(q_gen_2449, q_gen_2448) -> q_gen_2496
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, a>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2496) -> q_gen_2452
<a, nil>() -> q_gen_2453
<b, cons>(q_gen_2449, q_gen_2448) -> q_gen_2453
<b, nil>() -> q_gen_2453
<a, a>() -> q_gen_2454
<b, b>() -> q_gen_2454
<cons, nil>(q_gen_2449, q_gen_2496) -> q_gen_2498
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458, q_gen_2478, q_gen_2479, q_gen_2480, q_gen_2481},
Q_f={q_gen_2455},
Delta=
{
<cons>(q_gen_2458, q_gen_2457) -> q_gen_2457
<nil>() -> q_gen_2457
<a>() -> q_gen_2458
<b>() -> q_gen_2458
<cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2478
<cons, b>(q_gen_2458, q_gen_2457) -> q_gen_2479
<b, nil>() -> q_gen_2480
<b, b>() -> q_gen_2481
<cons, nil, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, cons, cons>(q_gen_2481, q_gen_2480, q_gen_2479, q_gen_2478) -> q_gen_2455
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> butlast([cons(y, nil), nil]) -> 7  ;  () -> butlast([nil, nil]) -> 7  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 7  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 10  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 10  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 10  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 10
}
Sat witness: Yes: ((append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]), {
_ci -> cons(a, nil)  ;  _di -> cons(a, nil)  ;  x -> nil  ;  x2 -> cons(b, nil)  ;  z -> a
})

-------------------------------------------
Step 18, which took 0.030961 s (model generation: 0.017162,  model checking: 0.013799):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463, q_gen_2486, q_gen_2487},
Q_f={q_gen_2450},
Delta=
{
<nil>() -> q_gen_2486
<a>() -> q_gen_2487
<b>() -> q_gen_2487
<cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2460
<nil, nil>() -> q_gen_2460
<cons, b>(q_gen_2487, q_gen_2486) -> q_gen_2461
<nil, a>() -> q_gen_2461
<nil, b>() -> q_gen_2461
<a, nil>() -> q_gen_2462
<b, cons>(q_gen_2487, q_gen_2486) -> q_gen_2462
<b, nil>() -> q_gen_2462
<a, a>() -> q_gen_2463
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2496, q_gen_2498},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons>(q_gen_2449, q_gen_2448) -> q_gen_2496
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, a>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2496) -> q_gen_2452
<a, nil>() -> q_gen_2453
<b, cons>(q_gen_2449, q_gen_2448) -> q_gen_2453
<b, nil>() -> q_gen_2453
<a, a>() -> q_gen_2454
<b, b>() -> q_gen_2454
<cons, nil>(q_gen_2449, q_gen_2496) -> q_gen_2498
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458, q_gen_2478, q_gen_2479, q_gen_2480, q_gen_2481},
Q_f={q_gen_2455},
Delta=
{
<cons>(q_gen_2458, q_gen_2457) -> q_gen_2457
<nil>() -> q_gen_2457
<a>() -> q_gen_2458
<b>() -> q_gen_2458
<cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2478
<cons, a>(q_gen_2458, q_gen_2457) -> q_gen_2479
<cons, b>(q_gen_2458, q_gen_2457) -> q_gen_2479
<a, nil>() -> q_gen_2480
<b, nil>() -> q_gen_2480
<a, a>() -> q_gen_2481
<b, b>() -> q_gen_2481
<cons, nil, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, cons, cons>(q_gen_2481, q_gen_2480, q_gen_2479, q_gen_2478) -> q_gen_2455
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> butlast([cons(y, nil), nil]) -> 7  ;  () -> butlast([nil, nil]) -> 7  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 10  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 10  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 10  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 10  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 10
}
Sat witness: Yes: ((append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]), {
_wh -> cons(b, nil)  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 19, which took 0.029120 s (model generation: 0.013663,  model checking: 0.015457):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463, q_gen_2486, q_gen_2487},
Q_f={q_gen_2450},
Delta=
{
<nil>() -> q_gen_2486
<a>() -> q_gen_2487
<b>() -> q_gen_2487
<cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2460
<nil, nil>() -> q_gen_2460
<cons, a>(q_gen_2487, q_gen_2486) -> q_gen_2461
<cons, b>(q_gen_2487, q_gen_2486) -> q_gen_2461
<nil, a>() -> q_gen_2461
<nil, b>() -> q_gen_2461
<a, cons>(q_gen_2487, q_gen_2486) -> q_gen_2462
<a, nil>() -> q_gen_2462
<b, cons>(q_gen_2487, q_gen_2486) -> q_gen_2462
<b, nil>() -> q_gen_2462
<a, a>() -> q_gen_2463
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2496, q_gen_2498},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons>(q_gen_2449, q_gen_2448) -> q_gen_2496
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, a>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2496) -> q_gen_2452
<a, nil>() -> q_gen_2453
<b, cons>(q_gen_2449, q_gen_2448) -> q_gen_2453
<b, nil>() -> q_gen_2453
<a, a>() -> q_gen_2454
<b, b>() -> q_gen_2454
<cons, nil>(q_gen_2449, q_gen_2496) -> q_gen_2498
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458, q_gen_2478, q_gen_2479, q_gen_2480, q_gen_2481},
Q_f={q_gen_2455},
Delta=
{
<cons>(q_gen_2458, q_gen_2457) -> q_gen_2457
<nil>() -> q_gen_2457
<a>() -> q_gen_2458
<b>() -> q_gen_2458
<cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2478
<cons, a>(q_gen_2458, q_gen_2457) -> q_gen_2479
<cons, b>(q_gen_2458, q_gen_2457) -> q_gen_2479
<a, nil>() -> q_gen_2480
<b, nil>() -> q_gen_2480
<a, a>() -> q_gen_2481
<b, b>() -> q_gen_2481
<cons, nil, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, cons, cons>(q_gen_2481, q_gen_2480, q_gen_2479, q_gen_2478) -> q_gen_2455
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> butlast([cons(y, nil), nil]) -> 8  ;  () -> butlast([nil, nil]) -> 8  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 10  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 10  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 10  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 10  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 10
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 20, which took 0.036573 s (model generation: 0.009191,  model checking: 0.027382):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463, q_gen_2486, q_gen_2487},
Q_f={q_gen_2450},
Delta=
{
<cons>(q_gen_2487, q_gen_2486) -> q_gen_2486
<nil>() -> q_gen_2486
<a>() -> q_gen_2487
<b>() -> q_gen_2487
<cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2460
<nil, nil>() -> q_gen_2460
<cons, a>(q_gen_2487, q_gen_2486) -> q_gen_2461
<cons, b>(q_gen_2487, q_gen_2486) -> q_gen_2461
<nil, a>() -> q_gen_2461
<nil, b>() -> q_gen_2461
<a, cons>(q_gen_2487, q_gen_2486) -> q_gen_2462
<a, nil>() -> q_gen_2462
<b, cons>(q_gen_2487, q_gen_2486) -> q_gen_2462
<b, nil>() -> q_gen_2462
<a, a>() -> q_gen_2463
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2496, q_gen_2498},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons>(q_gen_2449, q_gen_2448) -> q_gen_2496
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, a>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2496) -> q_gen_2452
<a, nil>() -> q_gen_2453
<b, cons>(q_gen_2449, q_gen_2448) -> q_gen_2453
<b, nil>() -> q_gen_2453
<a, a>() -> q_gen_2454
<b, b>() -> q_gen_2454
<cons, nil>(q_gen_2449, q_gen_2496) -> q_gen_2498
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458, q_gen_2478, q_gen_2479, q_gen_2480, q_gen_2481},
Q_f={q_gen_2455},
Delta=
{
<cons>(q_gen_2458, q_gen_2457) -> q_gen_2457
<nil>() -> q_gen_2457
<a>() -> q_gen_2458
<b>() -> q_gen_2458
<cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2478
<cons, a>(q_gen_2458, q_gen_2457) -> q_gen_2479
<cons, b>(q_gen_2458, q_gen_2457) -> q_gen_2479
<a, nil>() -> q_gen_2480
<b, nil>() -> q_gen_2480
<a, a>() -> q_gen_2481
<b, b>() -> q_gen_2481
<cons, nil, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, cons, cons>(q_gen_2481, q_gen_2480, q_gen_2479, q_gen_2478) -> q_gen_2455
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> butlast([cons(y, nil), nil]) -> 9  ;  () -> butlast([nil, nil]) -> 9  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 10  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 10  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 10  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 10  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 13
}
Sat witness: Yes: ((butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]), {
_sh -> cons(b, nil)  ;  x2 -> b  ;  x3 -> cons(b, nil)  ;  y -> a
})

-------------------------------------------
Step 21, which took 0.032625 s (model generation: 0.008818,  model checking: 0.023807):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463, q_gen_2486, q_gen_2487},
Q_f={q_gen_2450},
Delta=
{
<cons>(q_gen_2487, q_gen_2486) -> q_gen_2486
<nil>() -> q_gen_2486
<a>() -> q_gen_2487
<b>() -> q_gen_2487
<cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2460
<nil, nil>() -> q_gen_2460
<cons, a>(q_gen_2487, q_gen_2486) -> q_gen_2461
<cons, b>(q_gen_2487, q_gen_2486) -> q_gen_2461
<nil, a>() -> q_gen_2461
<nil, b>() -> q_gen_2461
<a, cons>(q_gen_2487, q_gen_2486) -> q_gen_2462
<a, nil>() -> q_gen_2462
<b, cons>(q_gen_2487, q_gen_2486) -> q_gen_2462
<b, nil>() -> q_gen_2462
<a, a>() -> q_gen_2463
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2496, q_gen_2498},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons>(q_gen_2449, q_gen_2448) -> q_gen_2496
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, a>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, a>(q_gen_2449, q_gen_2496) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2496) -> q_gen_2452
<a, cons>(q_gen_2449, q_gen_2448) -> q_gen_2453
<a, nil>() -> q_gen_2453
<b, cons>(q_gen_2449, q_gen_2448) -> q_gen_2453
<b, nil>() -> q_gen_2453
<a, a>() -> q_gen_2454
<b, b>() -> q_gen_2454
<cons, nil>(q_gen_2449, q_gen_2496) -> q_gen_2498
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458, q_gen_2478, q_gen_2479, q_gen_2480, q_gen_2481},
Q_f={q_gen_2455},
Delta=
{
<cons>(q_gen_2458, q_gen_2457) -> q_gen_2457
<nil>() -> q_gen_2457
<a>() -> q_gen_2458
<b>() -> q_gen_2458
<cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2478
<cons, a>(q_gen_2458, q_gen_2457) -> q_gen_2479
<cons, b>(q_gen_2458, q_gen_2457) -> q_gen_2479
<a, nil>() -> q_gen_2480
<b, nil>() -> q_gen_2480
<a, a>() -> q_gen_2481
<b, b>() -> q_gen_2481
<cons, nil, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, cons, cons>(q_gen_2481, q_gen_2480, q_gen_2479, q_gen_2478) -> q_gen_2455
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> butlast([cons(y, nil), nil]) -> 10  ;  () -> butlast([nil, nil]) -> 10  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 10  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 10  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 10  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 13  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 13
}
Sat witness: Yes: ((butlast([x, _bi])) -> butlastconcat([x, nil, _bi]), {
_bi -> cons(b, nil)  ;  x -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 22, which took 0.010072 s (model generation: 0.009267,  model checking: 0.000805):

Model:
|_
{
append -> 
{{{
Q={q_gen_2450, q_gen_2460, q_gen_2461, q_gen_2462, q_gen_2463, q_gen_2486, q_gen_2487},
Q_f={q_gen_2450},
Delta=
{
<cons>(q_gen_2487, q_gen_2486) -> q_gen_2486
<nil>() -> q_gen_2486
<a>() -> q_gen_2487
<b>() -> q_gen_2487
<cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2460
<nil, nil>() -> q_gen_2460
<cons, a>(q_gen_2487, q_gen_2486) -> q_gen_2461
<cons, b>(q_gen_2487, q_gen_2486) -> q_gen_2461
<nil, a>() -> q_gen_2461
<nil, b>() -> q_gen_2461
<a, cons>(q_gen_2487, q_gen_2486) -> q_gen_2462
<a, nil>() -> q_gen_2462
<b, cons>(q_gen_2487, q_gen_2486) -> q_gen_2462
<b, nil>() -> q_gen_2462
<a, a>() -> q_gen_2463
<b, b>() -> q_gen_2463
<cons, nil, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, cons, cons>(q_gen_2463, q_gen_2462, q_gen_2461, q_gen_2460) -> q_gen_2450
<nil, nil, nil>() -> q_gen_2450
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2446, q_gen_2448, q_gen_2449, q_gen_2452, q_gen_2453, q_gen_2454, q_gen_2496, q_gen_2498},
Q_f={q_gen_2446},
Delta=
{
<nil>() -> q_gen_2448
<a>() -> q_gen_2449
<b>() -> q_gen_2449
<cons>(q_gen_2449, q_gen_2448) -> q_gen_2496
<cons, cons>(q_gen_2454, q_gen_2453, q_gen_2452, q_gen_2446) -> q_gen_2446
<cons, nil>(q_gen_2449, q_gen_2448) -> q_gen_2446
<nil, nil>() -> q_gen_2446
<cons, a>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, a>(q_gen_2449, q_gen_2496) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2448) -> q_gen_2452
<cons, b>(q_gen_2449, q_gen_2496) -> q_gen_2452
<a, cons>(q_gen_2449, q_gen_2448) -> q_gen_2453
<a, nil>() -> q_gen_2453
<b, cons>(q_gen_2449, q_gen_2448) -> q_gen_2453
<b, nil>() -> q_gen_2453
<a, a>() -> q_gen_2454
<b, b>() -> q_gen_2454
<cons, nil>(q_gen_2449, q_gen_2496) -> q_gen_2498
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlastconcat -> 
{{{
Q={q_gen_2455, q_gen_2457, q_gen_2458, q_gen_2478, q_gen_2479, q_gen_2480, q_gen_2481},
Q_f={q_gen_2455},
Delta=
{
<cons>(q_gen_2458, q_gen_2457) -> q_gen_2457
<nil>() -> q_gen_2457
<a>() -> q_gen_2458
<b>() -> q_gen_2458
<cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2478
<cons, a>(q_gen_2458, q_gen_2457) -> q_gen_2479
<cons, b>(q_gen_2458, q_gen_2457) -> q_gen_2479
<a, nil>() -> q_gen_2480
<b, nil>() -> q_gen_2480
<a, a>() -> q_gen_2481
<b, b>() -> q_gen_2481
<cons, nil, cons>(q_gen_2481, q_gen_2480, q_gen_2479, q_gen_2478) -> q_gen_2455
<cons, nil, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, cons, cons>(q_gen_2481, q_gen_2480, q_gen_2479, q_gen_2478) -> q_gen_2455
<nil, cons, nil>(q_gen_2458, q_gen_2457) -> q_gen_2455
<nil, nil, nil>() -> q_gen_2455
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> butlast([cons(y, nil), nil]) -> 10  ;  () -> butlast([nil, nil]) -> 10  ;  (append([t1, l2, _wh])) -> append([cons(h1, t1), l2, cons(h1, _wh)]) -> 10  ;  (append([x, _ci, _di]) /\ butlast([cons(z, x2), _ci])) -> butlastconcat([x, cons(z, x2), _di]) -> 10  ;  (append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]) -> 13  ;  (butlast([x, _bi])) -> butlastconcat([x, nil, _bi]) -> 13  ;  (butlast([cons(x2, x3), _sh])) -> butlast([cons(y, cons(x2, x3)), cons(y, _sh)]) -> 13
}
Sat witness: Yes: ((append([xs, ys, _ii]) /\ butlast([_ii, _ji]) /\ butlastconcat([xs, ys, _ki])) -> eq_eltlist([_ji, _ki]), {
_ii -> cons(b, cons(b, nil))  ;  _ji -> cons(b, nil)  ;  _ki -> nil  ;  xs -> nil  ;  ys -> cons(b, cons(b, nil))
})

Total time: 30.003531
Reason for stopping: DontKnow. Stopped because: timeout