Solving ../../benchmarks/true/isaplanner_prop51.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), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)])}
(butlast([_nfa, _ofa]) /\ butlast([_nfa, _pfa])) -> eq_eltlist([_ofa, _pfa])
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)])}
(append([_rfa, _sfa, _tfa]) /\ append([_rfa, _sfa, _ufa])) -> eq_eltlist([_tfa, _ufa])
)
}

properties:
{(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys])}


over-approximation: {append, butlast}
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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 0  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 0  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 0
}


Solving took 30.017483 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2527, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2534, q_gen_2535, q_gen_2536, q_gen_2537, q_gen_2542, q_gen_2543, q_gen_2544, q_gen_2545, q_gen_2546, q_gen_2547, q_gen_2548, q_gen_2549, q_gen_2550, q_gen_2551, q_gen_2552, q_gen_2553, q_gen_2558, q_gen_2559, q_gen_2560, q_gen_2561, q_gen_2562, q_gen_2563, q_gen_2564, q_gen_2565, q_gen_2569, q_gen_2570, q_gen_2571, q_gen_2572, q_gen_2573, q_gen_2574, q_gen_2575, q_gen_2576, q_gen_2577, q_gen_2578, q_gen_2584, q_gen_2585, q_gen_2586, q_gen_2587, q_gen_2588, q_gen_2593, q_gen_2594, q_gen_2595, q_gen_2596, q_gen_2597},
Q_f={},
Delta=
{
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<b>() -> q_gen_2552
<cons>(q_gen_2552, q_gen_2546) -> q_gen_2564
<nil, nil>() -> q_gen_2528
<nil, b>() -> q_gen_2529
<b, nil>() -> q_gen_2530
<b, b>() -> q_gen_2531
<nil, a>() -> q_gen_2535
<a, nil>() -> q_gen_2536
<a, a>() -> q_gen_2537
<cons, cons>(q_gen_2537, q_gen_2536, q_gen_2535, q_gen_2528) -> q_gen_2544
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2545
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2548
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2550
<cons, b>(q_gen_2552, q_gen_2546) -> q_gen_2551
<b, cons>(q_gen_2552, q_gen_2546) -> q_gen_2553
<cons, a>(q_gen_2552, q_gen_2546) -> q_gen_2559
<a, cons>(q_gen_2552, q_gen_2546) -> q_gen_2560
<cons, cons>(q_gen_2531, q_gen_2553, q_gen_2551, q_gen_2550) -> q_gen_2562
<cons, b>(q_gen_2552, q_gen_2564) -> q_gen_2563
<b, cons>(q_gen_2552, q_gen_2564) -> q_gen_2565
<nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2595
<nil, cons>(q_gen_2552, q_gen_2546) -> q_gen_2597
<nil, nil, nil>() -> q_gen_2522
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2527
<nil, cons, cons>(q_gen_2537, q_gen_2536, q_gen_2535, q_gen_2528) -> q_gen_2534
<cons, nil, cons>(q_gen_2537, q_gen_2536, q_gen_2535, q_gen_2528) -> q_gen_2542
<cons, nil, cons>(q_gen_2531, q_gen_2548, q_gen_2545, q_gen_2544) -> q_gen_2543
<nil, cons, cons>(q_gen_2531, q_gen_2553, q_gen_2551, q_gen_2550) -> q_gen_2549
<cons, nil, cons>(q_gen_2537, q_gen_2560, q_gen_2559, q_gen_2550) -> q_gen_2558
<nil, cons, cons>(q_gen_2531, q_gen_2565, q_gen_2563, q_gen_2562) -> q_gen_2561
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2569
<cons, cons, cons>(q_gen_2578, q_gen_2577, q_gen_2576, q_gen_2575, q_gen_2574, q_gen_2573, q_gen_2572, q_gen_2571) -> q_gen_2570
<nil, nil, cons>(q_gen_2552, q_gen_2546) -> q_gen_2571
<nil, nil, b>() -> q_gen_2572
<nil, b, cons>(q_gen_2552, q_gen_2546) -> q_gen_2573
<nil, b, b>() -> q_gen_2574
<b, nil, cons>(q_gen_2552, q_gen_2546) -> q_gen_2575
<b, nil, b>() -> q_gen_2576
<b, b, cons>(q_gen_2552, q_gen_2546) -> q_gen_2577
<b, b, b>() -> q_gen_2578
<cons, cons, cons>(q_gen_2578, q_gen_2588, q_gen_2576, q_gen_2587, q_gen_2574, q_gen_2586, q_gen_2572, q_gen_2585) -> q_gen_2584
<nil, nil, cons>(q_gen_2552, q_gen_2564) -> q_gen_2585
<nil, b, cons>(q_gen_2552, q_gen_2564) -> q_gen_2586
<b, nil, cons>(q_gen_2552, q_gen_2564) -> q_gen_2587
<b, b, cons>(q_gen_2552, q_gen_2564) -> q_gen_2588
<nil, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2593
<cons, nil, cons>(q_gen_2531, q_gen_2548, q_gen_2529, q_gen_2595) -> q_gen_2594
<nil, cons, cons>(q_gen_2531, q_gen_2553, q_gen_2529, q_gen_2597) -> q_gen_2596
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2519, q_gen_2520, q_gen_2521, q_gen_2523, q_gen_2524, q_gen_2525, q_gen_2526, q_gen_2532, q_gen_2533, q_gen_2538, q_gen_2539, q_gen_2540, q_gen_2541, q_gen_2554, q_gen_2555, q_gen_2556, q_gen_2557, q_gen_2566, q_gen_2567, q_gen_2568, q_gen_2579, q_gen_2580, q_gen_2581, q_gen_2582, q_gen_2583, q_gen_2589, q_gen_2590, q_gen_2591, q_gen_2592},
Q_f={},
Delta=
{
<nil>() -> q_gen_2520
<b>() -> q_gen_2521
<a>() -> q_gen_2533
<cons>(q_gen_2521, q_gen_2520) -> q_gen_2556
<cons>(q_gen_2521, q_gen_2556) -> q_gen_2582
<nil, nil>() -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2519
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2519) -> q_gen_2523
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<b, nil>() -> q_gen_2525
<b, b>() -> q_gen_2526
<cons, nil>(q_gen_2533, q_gen_2520) -> q_gen_2532
<cons, cons>(q_gen_2541, q_gen_2540, q_gen_2539, q_gen_2519) -> q_gen_2538
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2539
<a, nil>() -> q_gen_2540
<a, a>() -> q_gen_2541
<cons, cons>(q_gen_2526, q_gen_2557, q_gen_2555, q_gen_2523) -> q_gen_2554
<cons, b>(q_gen_2521, q_gen_2556) -> q_gen_2555
<b, cons>(q_gen_2521, q_gen_2520) -> q_gen_2557
<cons, cons>(q_gen_2541, q_gen_2568, q_gen_2567, q_gen_2523) -> q_gen_2566
<cons, a>(q_gen_2521, q_gen_2556) -> q_gen_2567
<a, cons>(q_gen_2521, q_gen_2520) -> q_gen_2568
<cons, nil>(q_gen_2521, q_gen_2556) -> q_gen_2579
<cons, cons>(q_gen_2526, q_gen_2583, q_gen_2581, q_gen_2554) -> q_gen_2580
<cons, b>(q_gen_2521, q_gen_2582) -> q_gen_2581
<b, cons>(q_gen_2521, q_gen_2556) -> q_gen_2583
<cons, nil>(q_gen_2521, q_gen_2582) -> q_gen_2589
<cons, cons>(q_gen_2541, q_gen_2592, q_gen_2591, q_gen_2566) -> q_gen_2590
<cons, a>(q_gen_2533, q_gen_2582) -> q_gen_2591
<a, cons>(q_gen_2533, q_gen_2556) -> q_gen_2592
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004719 s (model generation: 0.003949,  model checking: 0.000770):

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

}

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

}

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 1  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 1  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 1
}
Sat witness: Yes: (() -> butlast([nil, nil]), {

})

-------------------------------------------
Step 1, which took 0.003512 s (model generation: 0.003431,  model checking: 0.000081):

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

}

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

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 1  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 1  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 1
}
Sat witness: Yes: (() -> butlast([cons(y, nil), nil]), {
y -> b
})

-------------------------------------------
Step 2, which took 0.004254 s (model generation: 0.003403,  model checking: 0.000851):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521},
Q_f={q_gen_2518},
Delta=
{
<nil>() -> q_gen_2520
<b>() -> q_gen_2521
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
}

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 1  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 1  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 1
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 3, which took 0.003746 s (model generation: 0.003421,  model checking: 0.000325):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521},
Q_f={q_gen_2518},
Delta=
{
<nil>() -> q_gen_2520
<b>() -> q_gen_2521
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
}

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 1  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 1  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 4
}
Sat witness: Yes: ((butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]), {
_mfa -> nil  ;  x2 -> b  ;  x3 -> nil  ;  y -> b
})

-------------------------------------------
Step 4, which took 0.004734 s (model generation: 0.003637,  model checking: 0.001097):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526},
Q_f={q_gen_2518},
Delta=
{
<nil>() -> q_gen_2520
<b>() -> q_gen_2521
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<b, nil>() -> q_gen_2525
<b, b>() -> q_gen_2526
}

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 4  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 2  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 4
}
Sat witness: Yes: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.005309 s (model generation: 0.004454,  model checking: 0.000855):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531},
Q_f={q_gen_2522},
Delta=
{
<nil, nil>() -> q_gen_2528
<nil, b>() -> q_gen_2529
<b, nil>() -> q_gen_2530
<b, b>() -> q_gen_2531
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526},
Q_f={q_gen_2518},
Delta=
{
<nil>() -> q_gen_2520
<b>() -> q_gen_2521
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<b, nil>() -> q_gen_2525
<b, b>() -> q_gen_2526
}

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 4  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 3  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 4
}
Sat witness: Yes: (() -> butlast([cons(y, nil), nil]), {
y -> a
})

-------------------------------------------
Step 6, which took 0.008676 s (model generation: 0.006030,  model checking: 0.002646):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531},
Q_f={q_gen_2522},
Delta=
{
<nil, nil>() -> q_gen_2528
<nil, b>() -> q_gen_2529
<b, nil>() -> q_gen_2530
<b, b>() -> q_gen_2531
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526},
Q_f={q_gen_2518},
Delta=
{
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<b, nil>() -> q_gen_2525
<b, b>() -> q_gen_2526
}

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 4  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 4  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 4
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 7, which took 0.009177 s (model generation: 0.008371,  model checking: 0.000806):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531},
Q_f={q_gen_2522},
Delta=
{
<nil, nil>() -> q_gen_2528
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, nil>() -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526},
Q_f={q_gen_2518},
Delta=
{
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<b, nil>() -> q_gen_2525
<b, b>() -> q_gen_2526
}

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 4  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 4  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 7
}
Sat witness: Yes: ((butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]), {
_mfa -> nil  ;  x2 -> b  ;  x3 -> nil  ;  y -> a
})

-------------------------------------------
Step 8, which took 0.016099 s (model generation: 0.008974,  model checking: 0.007125):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531},
Q_f={q_gen_2522},
Delta=
{
<nil, nil>() -> q_gen_2528
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, nil>() -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526},
Q_f={q_gen_2518},
Delta=
{
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<a, nil>() -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
}

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 7  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 5  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 7
}
Sat witness: Yes: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 9, which took 0.024955 s (model generation: 0.009065,  model checking: 0.015890):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2546, q_gen_2547},
Q_f={q_gen_2522},
Delta=
{
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2528
<nil, nil>() -> q_gen_2528
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2529
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, nil>() -> q_gen_2530
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526},
Q_f={q_gen_2518},
Delta=
{
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<a, nil>() -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
}

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 7  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 6  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 7
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 10, which took 0.017591 s (model generation: 0.005353,  model checking: 0.012238):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2546, q_gen_2547},
Q_f={q_gen_2522},
Delta=
{
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<b>() -> q_gen_2547
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2528
<nil, nil>() -> q_gen_2528
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2529
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, nil>() -> q_gen_2530
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526},
Q_f={q_gen_2518},
Delta=
{
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<a, nil>() -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
}

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 7  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 7  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 10
}
Sat witness: Yes: ((butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]), {
_mfa -> cons(b, nil)  ;  x2 -> b  ;  x3 -> cons(b, nil)  ;  y -> b
})

-------------------------------------------
Step 11, which took 0.013927 s (model generation: 0.006865,  model checking: 0.007062):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2546, q_gen_2547},
Q_f={q_gen_2522},
Delta=
{
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<b>() -> q_gen_2547
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2528
<nil, nil>() -> q_gen_2528
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2529
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, nil>() -> q_gen_2530
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526},
Q_f={q_gen_2518},
Delta=
{
<cons>(q_gen_2521, q_gen_2520) -> q_gen_2520
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<a, nil>() -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
}

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 10  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 8  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 10
}
Sat witness: Yes: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(b, nil)  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 12, which took 0.016097 s (model generation: 0.006564,  model checking: 0.009533):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2546, q_gen_2547},
Q_f={q_gen_2522},
Delta=
{
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<b>() -> q_gen_2547
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2528
<nil, nil>() -> q_gen_2528
<cons, a>(q_gen_2547, q_gen_2546) -> q_gen_2529
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2529
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<a, nil>() -> q_gen_2530
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526},
Q_f={q_gen_2518},
Delta=
{
<cons>(q_gen_2521, q_gen_2520) -> q_gen_2520
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<a, nil>() -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
}

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 10  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 9  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 10
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 13, which took 0.011166 s (model generation: 0.007267,  model checking: 0.003899):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2546, q_gen_2547},
Q_f={q_gen_2522},
Delta=
{
<cons>(q_gen_2547, q_gen_2546) -> q_gen_2546
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<b>() -> q_gen_2547
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2528
<nil, nil>() -> q_gen_2528
<cons, a>(q_gen_2547, q_gen_2546) -> q_gen_2529
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2529
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<a, nil>() -> q_gen_2530
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526},
Q_f={q_gen_2518},
Delta=
{
<cons>(q_gen_2521, q_gen_2520) -> q_gen_2520
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<a, nil>() -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
}

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 10  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 10  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 13
}
Sat witness: Yes: ((butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]), {
_mfa -> cons(b, nil)  ;  x2 -> b  ;  x3 -> cons(b, nil)  ;  y -> a
})

-------------------------------------------
Step 14, which took 0.013363 s (model generation: 0.007972,  model checking: 0.005391):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2546, q_gen_2547},
Q_f={q_gen_2522},
Delta=
{
<cons>(q_gen_2547, q_gen_2546) -> q_gen_2546
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<b>() -> q_gen_2547
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2528
<nil, nil>() -> q_gen_2528
<cons, a>(q_gen_2547, q_gen_2546) -> q_gen_2529
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2529
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<a, nil>() -> q_gen_2530
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526},
Q_f={q_gen_2518},
Delta=
{
<cons>(q_gen_2521, q_gen_2520) -> q_gen_2520
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<a, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<a, nil>() -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
}

Datatype: <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, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 13  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 11  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 13
}
Sat witness: Yes: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.009563 s (model generation: 0.008677,  model checking: 0.000886):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2546, q_gen_2547, q_gen_2572, q_gen_2573, q_gen_2574, q_gen_2575, q_gen_2576, q_gen_2577, q_gen_2578},
Q_f={q_gen_2522},
Delta=
{
<cons>(q_gen_2547, q_gen_2546) -> q_gen_2546
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<b>() -> q_gen_2547
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2528
<nil, nil>() -> q_gen_2528
<cons, a>(q_gen_2547, q_gen_2546) -> q_gen_2529
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2529
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<a, nil>() -> q_gen_2530
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, cons, cons>(q_gen_2578, q_gen_2577, q_gen_2576, q_gen_2575, q_gen_2574, q_gen_2573, q_gen_2572, q_gen_2522) -> q_gen_2522
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
<nil, nil, b>() -> q_gen_2572
<nil, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2573
<nil, b, b>() -> q_gen_2574
<b, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2575
<b, nil, b>() -> q_gen_2576
<b, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2577
<b, b, b>() -> q_gen_2578
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526},
Q_f={q_gen_2518},
Delta=
{
<cons>(q_gen_2521, q_gen_2520) -> q_gen_2520
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<a, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<a, nil>() -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
}

Datatype: <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]) -> 11  ;  () -> butlast([nil, nil]) -> 11  ;  (append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 13  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 14  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 13
}
Sat witness: Yes: ((append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]), {
_vfa -> cons(b, cons(b, nil))  ;  _wfa -> nil  ;  x -> b  ;  ys -> cons(b, nil)
})

-------------------------------------------
Step 16, which took 1.002760 s (model generation: 0.009581,  model checking: 0.993179):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2546, q_gen_2547, q_gen_2572, q_gen_2573, q_gen_2574, q_gen_2575, q_gen_2576, q_gen_2577, q_gen_2578},
Q_f={q_gen_2522},
Delta=
{
<cons>(q_gen_2547, q_gen_2546) -> q_gen_2546
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<b>() -> q_gen_2547
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2528
<nil, nil>() -> q_gen_2528
<cons, a>(q_gen_2547, q_gen_2546) -> q_gen_2529
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2529
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<a, nil>() -> q_gen_2530
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, cons, cons>(q_gen_2578, q_gen_2577, q_gen_2576, q_gen_2575, q_gen_2574, q_gen_2573, q_gen_2572, q_gen_2522) -> q_gen_2522
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
<nil, nil, b>() -> q_gen_2572
<nil, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2573
<nil, b, b>() -> q_gen_2574
<b, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2575
<b, nil, b>() -> q_gen_2576
<b, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2577
<b, b, b>() -> q_gen_2578
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526, q_gen_2556, q_gen_2579},
Q_f={q_gen_2518},
Delta=
{
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons>(q_gen_2521, q_gen_2520) -> q_gen_2556
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, a>(q_gen_2521, q_gen_2556) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2556) -> q_gen_2524
<a, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<a, nil>() -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
<cons, nil>(q_gen_2521, q_gen_2556) -> q_gen_2579
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> butlast([cons(y, nil), nil]) -> 12  ;  () -> butlast([nil, nil]) -> 12  ;  (append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 13  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 14  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 16
}
Sat witness: Yes: ((butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]), {
_mfa -> cons(b, cons(b, nil))  ;  x2 -> b  ;  x3 -> cons(b, cons(b, nil))  ;  y -> b
})

-------------------------------------------
Step 17, which took 0.012973 s (model generation: 0.009620,  model checking: 0.003353):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2535, q_gen_2542, q_gen_2546, q_gen_2547, q_gen_2572, q_gen_2573, q_gen_2574, q_gen_2575, q_gen_2576, q_gen_2577, q_gen_2578},
Q_f={q_gen_2522},
Delta=
{
<cons>(q_gen_2547, q_gen_2546) -> q_gen_2546
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<b>() -> q_gen_2547
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2528
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2535, q_gen_2528) -> q_gen_2528
<nil, nil>() -> q_gen_2528
<cons, a>(q_gen_2547, q_gen_2546) -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<a, nil>() -> q_gen_2530
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2535
<nil, a>() -> q_gen_2535
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2535, q_gen_2528) -> q_gen_2522
<nil, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
<cons, cons, cons>(q_gen_2578, q_gen_2577, q_gen_2576, q_gen_2575, q_gen_2574, q_gen_2573, q_gen_2572, q_gen_2522) -> q_gen_2542
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2535, q_gen_2528) -> q_gen_2542
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2542
<nil, nil, b>() -> q_gen_2572
<nil, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2573
<nil, b, b>() -> q_gen_2574
<b, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2575
<b, nil, b>() -> q_gen_2576
<b, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2577
<b, b, b>() -> q_gen_2578
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526},
Q_f={q_gen_2518},
Delta=
{
<cons>(q_gen_2521, q_gen_2520) -> q_gen_2520
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<a, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<a, nil>() -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> butlast([cons(y, nil), nil]) -> 13  ;  () -> butlast([nil, nil]) -> 13  ;  (append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 16  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 14  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 16
}
Sat witness: Yes: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> nil  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 18, which took 0.012108 s (model generation: 0.008811,  model checking: 0.003297):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2536, q_gen_2546, q_gen_2547, q_gen_2569, q_gen_2572, q_gen_2573, q_gen_2574, q_gen_2575, q_gen_2576, q_gen_2577, q_gen_2578},
Q_f={q_gen_2522},
Delta=
{
<cons>(q_gen_2547, q_gen_2546) -> q_gen_2546
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<b>() -> q_gen_2547
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2528
<cons, cons>(q_gen_2531, q_gen_2536, q_gen_2529, q_gen_2528) -> q_gen_2528
<nil, nil>() -> q_gen_2528
<cons, a>(q_gen_2547, q_gen_2546) -> q_gen_2529
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2529
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<a, nil>() -> q_gen_2536
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2536
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<cons, nil, cons>(q_gen_2531, q_gen_2536, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2536, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
<cons, cons, cons>(q_gen_2578, q_gen_2577, q_gen_2576, q_gen_2575, q_gen_2574, q_gen_2573, q_gen_2572, q_gen_2569) -> q_gen_2569
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2569
<nil, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2569
<nil, nil, b>() -> q_gen_2572
<nil, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2573
<nil, b, b>() -> q_gen_2574
<b, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2575
<b, nil, b>() -> q_gen_2576
<b, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2577
<b, b, b>() -> q_gen_2578
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526},
Q_f={q_gen_2518},
Delta=
{
<cons>(q_gen_2521, q_gen_2520) -> q_gen_2520
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<a, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<a, nil>() -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> butlast([cons(y, nil), nil]) -> 14  ;  () -> butlast([nil, nil]) -> 14  ;  (append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 16  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 14  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 16
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 19, which took 0.009368 s (model generation: 0.008965,  model checking: 0.000403):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2546, q_gen_2547, q_gen_2572, q_gen_2573, q_gen_2574, q_gen_2575, q_gen_2576, q_gen_2577, q_gen_2578},
Q_f={q_gen_2522},
Delta=
{
<cons>(q_gen_2547, q_gen_2546) -> q_gen_2546
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<b>() -> q_gen_2547
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2528
<nil, nil>() -> q_gen_2528
<cons, a>(q_gen_2547, q_gen_2546) -> q_gen_2529
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2529
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<a, nil>() -> q_gen_2530
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, cons, cons>(q_gen_2578, q_gen_2577, q_gen_2576, q_gen_2575, q_gen_2574, q_gen_2573, q_gen_2572, q_gen_2522) -> q_gen_2522
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
<nil, nil, b>() -> q_gen_2572
<nil, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2573
<nil, b, b>() -> q_gen_2574
<b, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2575
<b, nil, b>() -> q_gen_2576
<b, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2577
<b, b, b>() -> q_gen_2578
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526, q_gen_2556, q_gen_2579},
Q_f={q_gen_2518},
Delta=
{
<cons>(q_gen_2521, q_gen_2556) -> q_gen_2520
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons>(q_gen_2521, q_gen_2520) -> q_gen_2556
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, a>(q_gen_2521, q_gen_2556) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2556) -> q_gen_2524
<a, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<a, nil>() -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2556) -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
<cons, nil>(q_gen_2521, q_gen_2556) -> q_gen_2579
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> butlast([cons(y, nil), nil]) -> 14  ;  () -> butlast([nil, nil]) -> 14  ;  (append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 16  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 17  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 16
}
Sat witness: Yes: ((append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]), {
_vfa -> cons(b, cons(b, cons(b, nil)))  ;  _wfa -> nil  ;  x -> b  ;  ys -> cons(b, nil)
})

-------------------------------------------
Step 20, which took 0.151570 s (model generation: 0.016788,  model checking: 0.134782):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2546, q_gen_2547, q_gen_2572, q_gen_2573, q_gen_2574, q_gen_2575, q_gen_2576, q_gen_2577, q_gen_2578},
Q_f={q_gen_2522},
Delta=
{
<cons>(q_gen_2547, q_gen_2546) -> q_gen_2546
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<b>() -> q_gen_2547
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2528
<nil, nil>() -> q_gen_2528
<cons, a>(q_gen_2547, q_gen_2546) -> q_gen_2529
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2529
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<a, nil>() -> q_gen_2530
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, cons, cons>(q_gen_2578, q_gen_2577, q_gen_2576, q_gen_2575, q_gen_2574, q_gen_2573, q_gen_2572, q_gen_2522) -> q_gen_2522
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
<nil, nil, b>() -> q_gen_2572
<nil, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2573
<nil, b, b>() -> q_gen_2574
<b, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2575
<b, nil, b>() -> q_gen_2576
<b, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2577
<b, b, b>() -> q_gen_2578
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526, q_gen_2556, q_gen_2579},
Q_f={q_gen_2518},
Delta=
{
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons>(q_gen_2521, q_gen_2520) -> q_gen_2556
<cons>(q_gen_2521, q_gen_2556) -> q_gen_2556
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, a>(q_gen_2521, q_gen_2556) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2556) -> q_gen_2524
<a, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<a, nil>() -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2556) -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
<cons, nil>(q_gen_2521, q_gen_2556) -> q_gen_2579
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> butlast([cons(y, nil), nil]) -> 15  ;  () -> butlast([nil, nil]) -> 15  ;  (append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 16  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 17  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 19
}
Sat witness: Yes: ((butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]), {
_mfa -> cons(a, cons(b, nil))  ;  x2 -> a  ;  x3 -> cons(b, cons(b, nil))  ;  y -> a
})

-------------------------------------------
Step 21, which took 0.034904 s (model generation: 0.011559,  model checking: 0.023345):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2546, q_gen_2547, q_gen_2572, q_gen_2573, q_gen_2574, q_gen_2575, q_gen_2576, q_gen_2577, q_gen_2578},
Q_f={q_gen_2522},
Delta=
{
<cons>(q_gen_2547, q_gen_2546) -> q_gen_2546
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<b>() -> q_gen_2547
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2528
<nil, nil>() -> q_gen_2528
<cons, a>(q_gen_2547, q_gen_2546) -> q_gen_2529
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2529
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<a, nil>() -> q_gen_2530
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, cons, cons>(q_gen_2578, q_gen_2577, q_gen_2576, q_gen_2575, q_gen_2574, q_gen_2573, q_gen_2572, q_gen_2522) -> q_gen_2522
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
<nil, nil, b>() -> q_gen_2572
<nil, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2573
<nil, b, b>() -> q_gen_2574
<b, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2575
<b, nil, b>() -> q_gen_2576
<b, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2577
<b, b, b>() -> q_gen_2578
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526, q_gen_2556, q_gen_2579},
Q_f={q_gen_2518},
Delta=
{
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons>(q_gen_2521, q_gen_2520) -> q_gen_2556
<cons>(q_gen_2521, q_gen_2556) -> q_gen_2556
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, a>(q_gen_2521, q_gen_2556) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2556) -> q_gen_2524
<a, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<a, cons>(q_gen_2521, q_gen_2556) -> q_gen_2525
<a, nil>() -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2556) -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
<cons, nil>(q_gen_2521, q_gen_2556) -> q_gen_2579
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> butlast([cons(y, nil), nil]) -> 16  ;  () -> butlast([nil, nil]) -> 16  ;  (append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 19  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 17  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 19
}
Sat witness: Yes: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 22, which took 0.014916 s (model generation: 0.011948,  model checking: 0.002968):

Model:
|_
{
append -> 
{{{
Q={q_gen_2522, q_gen_2528, q_gen_2529, q_gen_2530, q_gen_2531, q_gen_2546, q_gen_2547, q_gen_2572, q_gen_2573, q_gen_2574, q_gen_2575, q_gen_2576, q_gen_2577, q_gen_2578},
Q_f={q_gen_2522},
Delta=
{
<cons>(q_gen_2547, q_gen_2546) -> q_gen_2546
<nil>() -> q_gen_2546
<a>() -> q_gen_2547
<b>() -> q_gen_2547
<cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2528
<nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2528
<nil, nil>() -> q_gen_2528
<cons, a>(q_gen_2547, q_gen_2546) -> q_gen_2529
<cons, b>(q_gen_2547, q_gen_2546) -> q_gen_2529
<nil, a>() -> q_gen_2529
<nil, b>() -> q_gen_2529
<a, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<a, nil>() -> q_gen_2530
<b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2530
<b, nil>() -> q_gen_2530
<a, a>() -> q_gen_2531
<b, b>() -> q_gen_2531
<cons, cons, cons>(q_gen_2578, q_gen_2577, q_gen_2576, q_gen_2575, q_gen_2574, q_gen_2573, q_gen_2572, q_gen_2522) -> q_gen_2522
<cons, nil, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, cons, cons>(q_gen_2531, q_gen_2530, q_gen_2529, q_gen_2528) -> q_gen_2522
<nil, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2522
<nil, nil, nil>() -> q_gen_2522
<nil, nil, b>() -> q_gen_2572
<nil, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2573
<nil, b, b>() -> q_gen_2574
<b, nil, cons>(q_gen_2547, q_gen_2546) -> q_gen_2575
<b, nil, b>() -> q_gen_2576
<b, b, cons>(q_gen_2547, q_gen_2546) -> q_gen_2577
<b, b, b>() -> q_gen_2578
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  butlast -> 
{{{
Q={q_gen_2518, q_gen_2520, q_gen_2521, q_gen_2524, q_gen_2525, q_gen_2526, q_gen_2556, q_gen_2579},
Q_f={q_gen_2518},
Delta=
{
<nil>() -> q_gen_2520
<a>() -> q_gen_2521
<b>() -> q_gen_2521
<cons>(q_gen_2521, q_gen_2520) -> q_gen_2556
<cons>(q_gen_2521, q_gen_2556) -> q_gen_2556
<cons, cons>(q_gen_2526, q_gen_2525, q_gen_2524, q_gen_2518) -> q_gen_2518
<cons, nil>(q_gen_2521, q_gen_2520) -> q_gen_2518
<nil, nil>() -> q_gen_2518
<cons, a>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, a>(q_gen_2521, q_gen_2556) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2520) -> q_gen_2524
<cons, b>(q_gen_2521, q_gen_2556) -> q_gen_2524
<a, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<a, cons>(q_gen_2521, q_gen_2556) -> q_gen_2525
<a, nil>() -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2520) -> q_gen_2525
<b, cons>(q_gen_2521, q_gen_2556) -> q_gen_2525
<b, nil>() -> q_gen_2525
<a, a>() -> q_gen_2526
<b, b>() -> q_gen_2526
<cons, nil>(q_gen_2521, q_gen_2556) -> q_gen_2579
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17  ;  () -> butlast([cons(y, nil), nil]) -> 17  ;  () -> butlast([nil, nil]) -> 17  ;  (append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 19  ;  (append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 20  ;  (butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 19
}
Sat witness: Yes: ((append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]), {
_vfa -> cons(b, cons(b, nil))  ;  _wfa -> cons(b, nil)  ;  x -> b  ;  ys -> nil
})

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