Solving ../../benchmarks/true/append_not_null.smt2...

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


Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)])}
(append([_iy, _jy, _ky]) /\ append([_iy, _jy, _ly])) -> eq_natlist([_ky, _ly])
)
(not_null, P:
{() -> not_null([cons(x, ll)])
(not_null([nil])) -> BOT}
)
}

properties:
{(append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my])}


over-approximation: {append}
under-approximation: {}

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0  ;  () -> not_null([cons(x, ll)]) -> 0  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 0  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 0  ;  (not_null([nil])) -> BOT -> 0
}


Solving took 30.030758 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_525, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_533, q_gen_534, q_gen_535, q_gen_536, q_gen_537, q_gen_538, q_gen_539, q_gen_540, q_gen_541, q_gen_542, q_gen_543, q_gen_544, q_gen_545, q_gen_546, q_gen_547, q_gen_548, q_gen_549, q_gen_550, q_gen_551, q_gen_552, q_gen_553, q_gen_554, q_gen_555, q_gen_556, q_gen_557, q_gen_558, q_gen_559, q_gen_560, q_gen_561, q_gen_562, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569, q_gen_570, q_gen_571, q_gen_572, q_gen_573, q_gen_574, q_gen_575, q_gen_576, q_gen_577, q_gen_578, q_gen_579, q_gen_580, q_gen_581, q_gen_582, q_gen_583, q_gen_584, q_gen_585, q_gen_586, q_gen_587, q_gen_588, q_gen_589, q_gen_590, q_gen_591, q_gen_592, q_gen_593, q_gen_594, q_gen_595, q_gen_596, q_gen_597, q_gen_598, q_gen_599, q_gen_600, q_gen_601, q_gen_602, q_gen_603, q_gen_604, q_gen_605, q_gen_606, q_gen_607, q_gen_608, q_gen_609, q_gen_610, q_gen_611, q_gen_612, q_gen_613, q_gen_614, q_gen_615, q_gen_616, q_gen_617, q_gen_618, q_gen_619, q_gen_620, q_gen_621, q_gen_622, q_gen_623, q_gen_624, q_gen_625, q_gen_626, q_gen_627, q_gen_628, q_gen_629, q_gen_630, q_gen_631, q_gen_632, q_gen_633, q_gen_634, q_gen_635, q_gen_636, q_gen_637, q_gen_638, q_gen_639, q_gen_640, q_gen_641, q_gen_642, q_gen_643, q_gen_644, q_gen_645, q_gen_646, q_gen_647, q_gen_648, q_gen_649, q_gen_650},
Q_f={},
Delta=
{
<s>(q_gen_536) -> q_gen_535
<z>() -> q_gen_536
<nil>() -> q_gen_543
<cons>(q_gen_536, q_gen_543) -> q_gen_548
<nil, nil>() -> q_gen_526
<nil, z>() -> q_gen_527
<z, nil>() -> q_gen_528
<z, z>() -> q_gen_529
<nil, s>(q_gen_535) -> q_gen_534
<s, nil>(q_gen_535) -> q_gen_537
<s, s>(q_gen_539) -> q_gen_538
<s, s>(q_gen_529) -> q_gen_539
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_541
<cons, z>(q_gen_536, q_gen_543) -> q_gen_542
<z, cons>(q_gen_536, q_gen_543) -> q_gen_544
<cons, cons>(q_gen_529, q_gen_544, q_gen_542, q_gen_541) -> q_gen_546
<cons, z>(q_gen_536, q_gen_548) -> q_gen_547
<z, cons>(q_gen_536, q_gen_548) -> q_gen_549
<cons, s>(q_gen_529, q_gen_527) -> q_gen_551
<s, cons>(q_gen_529, q_gen_528) -> q_gen_552
<cons, s>(q_gen_556, q_gen_555) -> q_gen_554
<nil, s>(q_gen_536) -> q_gen_555
<z, s>(q_gen_536) -> q_gen_556
<s, cons>(q_gen_559, q_gen_558) -> q_gen_557
<s, nil>(q_gen_536) -> q_gen_558
<s, z>(q_gen_536) -> q_gen_559
<nil, cons>(q_gen_536, q_gen_543) -> q_gen_571
<s, z>(q_gen_535) -> q_gen_600
<s, s>(q_gen_559) -> q_gen_621
<nil, nil, nil>() -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_525
<nil, cons, cons>(q_gen_538, q_gen_537, q_gen_534, q_gen_526) -> q_gen_533
<cons, nil, cons>(q_gen_529, q_gen_544, q_gen_542, q_gen_541) -> q_gen_540
<nil, cons, cons>(q_gen_529, q_gen_549, q_gen_547, q_gen_546) -> q_gen_545
<cons, nil, cons>(q_gen_539, q_gen_552, q_gen_551, q_gen_541) -> q_gen_550
<nil, cons, cons>(q_gen_538, q_gen_557, q_gen_554, q_gen_541) -> q_gen_553
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_560
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_562) -> q_gen_561
<nil, nil, cons>(q_gen_536, q_gen_543) -> q_gen_562
<nil, nil, z>() -> q_gen_563
<nil, z, cons>(q_gen_536, q_gen_543) -> q_gen_564
<nil, z, z>() -> q_gen_565
<z, nil, cons>(q_gen_536, q_gen_543) -> q_gen_566
<z, nil, z>() -> q_gen_567
<z, z, cons>(q_gen_536, q_gen_543) -> q_gen_568
<z, z, z>() -> q_gen_569
<cons, nil, cons>(q_gen_529, q_gen_544, q_gen_527, q_gen_571) -> q_gen_570
<nil, cons, cons>(q_gen_559, q_gen_558, q_gen_527, q_gen_526) -> q_gen_572
<cons, cons, cons>(q_gen_582, q_gen_579, q_gen_578, q_gen_577, q_gen_576, q_gen_575, q_gen_574, q_gen_562) -> q_gen_573
<nil, nil, s>(q_gen_535) -> q_gen_574
<nil, s, cons>(q_gen_529, q_gen_528) -> q_gen_575
<nil, s, s>(q_gen_556) -> q_gen_576
<s, nil, cons>(q_gen_559, q_gen_558) -> q_gen_577
<s, nil, s>(q_gen_539) -> q_gen_578
<s, s, cons>(q_gen_581, q_gen_580) -> q_gen_579
<s, z, nil>(q_gen_536) -> q_gen_580
<s, z, z>(q_gen_536) -> q_gen_581
<s, s, s>(q_gen_583) -> q_gen_582
<s, z, s>(q_gen_529) -> q_gen_583
<cons, cons, cons>(q_gen_583, q_gen_589, q_gen_588, q_gen_587, q_gen_586, q_gen_564, q_gen_585, q_gen_562) -> q_gen_584
<nil, nil, s>(q_gen_536) -> q_gen_585
<nil, z, s>(q_gen_536) -> q_gen_586
<s, nil, cons>(q_gen_529, q_gen_528) -> q_gen_587
<s, nil, s>(q_gen_529) -> q_gen_588
<s, z, cons>(q_gen_529, q_gen_528) -> q_gen_589
<cons, cons, cons>(q_gen_594, q_gen_592, q_gen_588, q_gen_587, q_gen_591, q_gen_575, q_gen_585, q_gen_562) -> q_gen_590
<nil, s, s>(q_gen_529) -> q_gen_591
<s, s, cons>(q_gen_569, q_gen_593) -> q_gen_592
<z, z, nil>() -> q_gen_593
<s, s, s>(q_gen_569) -> q_gen_594
<cons, cons, cons>(q_gen_598, q_gen_597, q_gen_567, q_gen_566, q_gen_596, q_gen_575, q_gen_563, q_gen_562) -> q_gen_595
<nil, s, z>(q_gen_536) -> q_gen_596
<z, s, cons>(q_gen_529, q_gen_528) -> q_gen_597
<z, s, z>(q_gen_536) -> q_gen_598
<nil, cons, cons>(q_gen_600, q_gen_537, q_gen_527, q_gen_526) -> q_gen_599
<cons, cons, cons>(q_gen_606, q_gen_604, q_gen_588, q_gen_587, q_gen_603, q_gen_602, q_gen_585, q_gen_562) -> q_gen_601
<nil, s, cons>(q_gen_559, q_gen_558) -> q_gen_602
<nil, s, s>(q_gen_559) -> q_gen_603
<s, s, cons>(q_gen_598, q_gen_605) -> q_gen_604
<z, s, nil>(q_gen_536) -> q_gen_605
<s, s, s>(q_gen_598) -> q_gen_606
<cons, cons, cons>(q_gen_612, q_gen_609, q_gen_578, q_gen_577, q_gen_608, q_gen_602, q_gen_574, q_gen_562) -> q_gen_607
<nil, s, s>(q_gen_539) -> q_gen_608
<s, s, cons>(q_gen_611, q_gen_610) -> q_gen_609
<s, s, nil>(q_gen_529) -> q_gen_610
<s, s, z>(q_gen_529) -> q_gen_611
<s, s, s>(q_gen_594) -> q_gen_612
<nil, cons, cons>(q_gen_539, q_gen_558, q_gen_555, q_gen_526) -> q_gen_613
<cons, cons, cons>(q_gen_594, q_gen_618, q_gen_588, q_gen_617, q_gen_591, q_gen_616, q_gen_585, q_gen_615) -> q_gen_614
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_615
<nil, s, cons>(q_gen_556, q_gen_528) -> q_gen_616
<s, nil, cons>(q_gen_556, q_gen_528) -> q_gen_617
<s, s, cons>(q_gen_619, q_gen_593) -> q_gen_618
<z, z, s>(q_gen_536) -> q_gen_619
<nil, cons, cons>(q_gen_621, q_gen_537, q_gen_555, q_gen_526) -> q_gen_620
<cons, cons, cons>(q_gen_606, q_gen_624, q_gen_588, q_gen_617, q_gen_603, q_gen_623, q_gen_585, q_gen_615) -> q_gen_622
<nil, s, cons>(q_gen_539, q_gen_558) -> q_gen_623
<s, s, cons>(q_gen_625, q_gen_605) -> q_gen_624
<z, s, s>(q_gen_529) -> q_gen_625
<nil, cons, cons>(q_gen_529, q_gen_544, q_gen_542, q_gen_541) -> q_gen_626
<cons, cons, cons>(q_gen_569, q_gen_633, q_gen_632, q_gen_631, q_gen_565, q_gen_630, q_gen_629, q_gen_628) -> q_gen_627
<nil, cons, cons>(q_gen_529, q_gen_544, q_gen_527, q_gen_571) -> q_gen_628
<nil, cons, z>(q_gen_536, q_gen_543) -> q_gen_629
<nil, z, cons>(q_gen_536, q_gen_548) -> q_gen_630
<z, cons, cons>(q_gen_529, q_gen_544, q_gen_527, q_gen_571) -> q_gen_631
<z, cons, z>(q_gen_536, q_gen_543) -> q_gen_632
<z, z, cons>(q_gen_536, q_gen_548) -> q_gen_633
<cons, cons, cons>(q_gen_569, q_gen_633, q_gen_567, q_gen_638, q_gen_637, q_gen_636, q_gen_635, q_gen_570) -> q_gen_634
<cons, nil, z>(q_gen_536, q_gen_543) -> q_gen_635
<cons, z, cons>(q_gen_529, q_gen_544, q_gen_527, q_gen_571) -> q_gen_636
<cons, z, z>(q_gen_536, q_gen_543) -> q_gen_637
<z, nil, cons>(q_gen_536, q_gen_548) -> q_gen_638
<cons, cons, cons>(q_gen_583, q_gen_643, q_gen_588, q_gen_642, q_gen_641, q_gen_636, q_gen_640, q_gen_570) -> q_gen_639
<cons, nil, s>(q_gen_529, q_gen_527) -> q_gen_640
<cons, z, s>(q_gen_529, q_gen_527) -> q_gen_641
<s, nil, cons>(q_gen_529, q_gen_544) -> q_gen_642
<s, z, cons>(q_gen_529, q_gen_544) -> q_gen_643
<cons, cons, cons>(q_gen_598, q_gen_647, q_gen_567, q_gen_638, q_gen_646, q_gen_645, q_gen_635, q_gen_570) -> q_gen_644
<cons, s, cons>(q_gen_569, q_gen_568, q_gen_565, q_gen_564) -> q_gen_645
<cons, s, z>(q_gen_529, q_gen_527) -> q_gen_646
<z, s, cons>(q_gen_529, q_gen_544) -> q_gen_647
<cons, cons, cons>(q_gen_594, q_gen_650, q_gen_588, q_gen_642, q_gen_649, q_gen_645, q_gen_640, q_gen_570) -> q_gen_648
<cons, s, s>(q_gen_569, q_gen_565) -> q_gen_649
<s, s, cons>(q_gen_569, q_gen_568) -> q_gen_650
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523, q_gen_530, q_gen_531, q_gen_532},
Q_f={},
Delta=
{
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<z>() -> q_gen_523
<cons>(q_gen_523, q_gen_531) -> q_gen_530
<cons>(q_gen_532, q_gen_522) -> q_gen_531
<s>(q_gen_523) -> q_gen_532
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004683 s (model generation: 0.003909,  model checking: 0.000774):

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

}

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

}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> not_null([cons(x, ll)]) -> 3  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 1  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 1  ;  (not_null([nil])) -> BOT -> 1
}
Sat witness: Yes: (() -> not_null([cons(x, ll)]), {
ll -> nil  ;  x -> z
})

-------------------------------------------
Step 1, which took 0.004249 s (model generation: 0.003635,  model checking: 0.000614):

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

}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<nil>() -> q_gen_521
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> not_null([cons(x, ll)]) -> 3  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 1  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 1  ;  (not_null([nil])) -> BOT -> 1
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.003399 s (model generation: 0.003391,  model checking: 0.000008):

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

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<nil>() -> q_gen_521
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> not_null([cons(x, ll)]) -> 3  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 1  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 1  ;  (not_null([nil])) -> BOT -> 4
}
Sat witness: Yes: ((not_null([nil])) -> BOT, {

})

-------------------------------------------
Step 3, which took 0.003790 s (model generation: 0.003422,  model checking: 0.000368):

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

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> not_null([cons(x, ll)]) -> 3  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 1  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 4  ;  (not_null([nil])) -> BOT -> 4
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> nil  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.003900 s (model generation: 0.003665,  model checking: 0.000235):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529},
Q_f={q_gen_524},
Delta=
{
<nil, nil>() -> q_gen_526
<nil, z>() -> q_gen_527
<z, nil>() -> q_gen_528
<z, z>() -> q_gen_529
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> not_null([cons(x, ll)]) -> 6  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 2  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 4  ;  (not_null([nil])) -> BOT -> 4
}
Sat witness: Yes: (() -> not_null([cons(x, ll)]), {
ll -> cons(s(z), nil)  ;  x -> z
})

-------------------------------------------
Step 5, which took 0.016947 s (model generation: 0.004707,  model checking: 0.012240):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529},
Q_f={q_gen_524},
Delta=
{
<nil, nil>() -> q_gen_526
<nil, z>() -> q_gen_527
<z, nil>() -> q_gen_528
<z, z>() -> q_gen_529
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> not_null([cons(x, ll)]) -> 6  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 3  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 4  ;  (not_null([nil])) -> BOT -> 4
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 6, which took 0.038724 s (model generation: 0.004758,  model checking: 0.033966):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<nil, nil>() -> q_gen_526
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, nil>(q_gen_535) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<z, z>() -> q_gen_529
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> not_null([cons(x, ll)]) -> 6  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 4  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 7  ;  (not_null([nil])) -> BOT -> 5
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, nil)  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 7, which took 0.036007 s (model generation: 0.005218,  model checking: 0.030789):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<z, z>() -> q_gen_529
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> not_null([cons(x, ll)]) -> 7  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 5  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 7  ;  (not_null([nil])) -> BOT -> 6
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(z, cons(z, cons(z, nil)))
})

-------------------------------------------
Step 8, which took 0.008545 s (model generation: 0.005465,  model checking: 0.003080):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<z, z>() -> q_gen_529
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> not_null([cons(x, ll)]) -> 7  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 6  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 10  ;  (not_null([nil])) -> BOT -> 7
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, nil)  ;  h1 -> s(z)  ;  l2 -> nil  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 9, which took 0.062982 s (model generation: 0.005342,  model checking: 0.057640):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<z, z>() -> q_gen_529
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> not_null([cons(x, ll)]) -> 8  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 7  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 10  ;  (not_null([nil])) -> BOT -> 8
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(s(s(z)), cons(z, nil))
})

-------------------------------------------
Step 10, which took 0.010369 s (model generation: 0.006869,  model checking: 0.003500):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> not_null([cons(x, ll)]) -> 9  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 8  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 13  ;  (not_null([nil])) -> BOT -> 9
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, nil)  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.037308 s (model generation: 0.007015,  model checking: 0.030293):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_524) -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
<nil, nil, z>() -> q_gen_563
<nil, z, cons>(q_gen_535, q_gen_543) -> q_gen_564
<nil, z, z>() -> q_gen_565
<z, nil, cons>(q_gen_535, q_gen_543) -> q_gen_566
<z, nil, z>() -> q_gen_567
<z, z, cons>(q_gen_535, q_gen_543) -> q_gen_568
<z, z, z>() -> q_gen_569
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> not_null([cons(x, ll)]) -> 10  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 9  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 16  ;  (not_null([nil])) -> BOT -> 10
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, nil)  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 0.531136 s (model generation: 0.008314,  model checking: 0.522822):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, cons>(q_gen_535, q_gen_543) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_524) -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
<nil, nil, z>() -> q_gen_563
<nil, z, cons>(q_gen_535, q_gen_543) -> q_gen_564
<nil, z, z>() -> q_gen_565
<z, nil, cons>(q_gen_535, q_gen_543) -> q_gen_566
<z, nil, z>() -> q_gen_567
<z, z, cons>(q_gen_535, q_gen_543) -> q_gen_568
<z, z, z>() -> q_gen_569
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14  ;  () -> not_null([cons(x, ll)]) -> 11  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 10  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 19  ;  (not_null([nil])) -> BOT -> 11
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, nil)  ;  h1 -> s(s(z))  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.162997 s (model generation: 0.009723,  model checking: 0.153274):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, cons>(q_gen_535, q_gen_543) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_524) -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
<nil, nil, s>(q_gen_535) -> q_gen_563
<nil, nil, z>() -> q_gen_563
<nil, s, cons>(q_gen_529, q_gen_528) -> q_gen_564
<nil, z, cons>(q_gen_535, q_gen_543) -> q_gen_564
<nil, s, s>(q_gen_529) -> q_gen_565
<nil, z, z>() -> q_gen_565
<s, nil, cons>(q_gen_529, q_gen_528) -> q_gen_566
<z, nil, cons>(q_gen_535, q_gen_543) -> q_gen_566
<s, nil, s>(q_gen_529) -> q_gen_567
<z, nil, z>() -> q_gen_567
<s, s, cons>(q_gen_569, q_gen_568) -> q_gen_568
<s, z, nil>(q_gen_535) -> q_gen_568
<z, z, cons>(q_gen_535, q_gen_543) -> q_gen_568
<s, s, s>(q_gen_569) -> q_gen_569
<s, z, s>(q_gen_529) -> q_gen_569
<s, z, z>(q_gen_535) -> q_gen_569
<z, z, z>() -> q_gen_569
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  () -> not_null([cons(x, ll)]) -> 12  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 11  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 22  ;  (not_null([nil])) -> BOT -> 12
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, nil)  ;  h1 -> s(z)  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.169165 s (model generation: 0.010312,  model checking: 0.158853):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, cons>(q_gen_535, q_gen_543) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_524) -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
<nil, nil, s>(q_gen_535) -> q_gen_563
<nil, nil, z>() -> q_gen_563
<nil, s, cons>(q_gen_529, q_gen_528) -> q_gen_564
<nil, z, cons>(q_gen_535, q_gen_543) -> q_gen_564
<nil, s, s>(q_gen_529) -> q_gen_565
<nil, z, s>(q_gen_535) -> q_gen_565
<nil, z, z>() -> q_gen_565
<s, nil, cons>(q_gen_529, q_gen_528) -> q_gen_566
<z, nil, cons>(q_gen_535, q_gen_543) -> q_gen_566
<s, nil, s>(q_gen_529) -> q_gen_567
<z, nil, z>() -> q_gen_567
<s, s, cons>(q_gen_569, q_gen_568) -> q_gen_568
<s, z, cons>(q_gen_529, q_gen_528) -> q_gen_568
<s, z, nil>(q_gen_535) -> q_gen_568
<z, z, cons>(q_gen_535, q_gen_543) -> q_gen_568
<s, s, s>(q_gen_569) -> q_gen_569
<s, z, s>(q_gen_529) -> q_gen_569
<s, z, z>(q_gen_535) -> q_gen_569
<z, z, z>() -> q_gen_569
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> not_null([cons(x, ll)]) -> 13  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 12  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 25  ;  (not_null([nil])) -> BOT -> 13
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, nil)  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.213744 s (model generation: 0.011135,  model checking: 0.202609):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, cons>(q_gen_535, q_gen_543) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_524) -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
<nil, nil, s>(q_gen_535) -> q_gen_563
<nil, nil, z>() -> q_gen_563
<nil, s, cons>(q_gen_529, q_gen_528) -> q_gen_564
<nil, z, cons>(q_gen_535, q_gen_543) -> q_gen_564
<nil, s, s>(q_gen_529) -> q_gen_565
<nil, z, s>(q_gen_535) -> q_gen_565
<nil, z, z>() -> q_gen_565
<s, nil, cons>(q_gen_529, q_gen_528) -> q_gen_566
<z, nil, cons>(q_gen_535, q_gen_543) -> q_gen_566
<s, nil, s>(q_gen_529) -> q_gen_567
<z, nil, z>() -> q_gen_567
<s, s, cons>(q_gen_569, q_gen_568) -> q_gen_568
<s, z, cons>(q_gen_529, q_gen_528) -> q_gen_568
<s, z, nil>(q_gen_535) -> q_gen_568
<z, z, cons>(q_gen_535, q_gen_543) -> q_gen_568
<z, z, nil>() -> q_gen_568
<s, s, s>(q_gen_569) -> q_gen_569
<s, z, s>(q_gen_529) -> q_gen_569
<s, z, z>(q_gen_535) -> q_gen_569
<z, z, z>() -> q_gen_569
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17  ;  () -> not_null([cons(x, ll)]) -> 14  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 13  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 28  ;  (not_null([nil])) -> BOT -> 14
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, nil)  ;  h1 -> z  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 0.168438 s (model generation: 0.012416,  model checking: 0.156022):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, cons>(q_gen_535, q_gen_543) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_524) -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
<nil, nil, s>(q_gen_535) -> q_gen_563
<nil, nil, z>() -> q_gen_563
<nil, s, cons>(q_gen_529, q_gen_528) -> q_gen_564
<nil, z, cons>(q_gen_535, q_gen_543) -> q_gen_564
<nil, s, s>(q_gen_529) -> q_gen_565
<nil, s, z>(q_gen_535) -> q_gen_565
<nil, z, s>(q_gen_535) -> q_gen_565
<nil, z, z>() -> q_gen_565
<s, nil, cons>(q_gen_529, q_gen_528) -> q_gen_566
<z, nil, cons>(q_gen_535, q_gen_543) -> q_gen_566
<s, nil, s>(q_gen_529) -> q_gen_567
<z, nil, z>() -> q_gen_567
<s, s, cons>(q_gen_569, q_gen_568) -> q_gen_568
<s, z, cons>(q_gen_529, q_gen_528) -> q_gen_568
<s, z, nil>(q_gen_535) -> q_gen_568
<z, s, cons>(q_gen_529, q_gen_528) -> q_gen_568
<z, z, cons>(q_gen_535, q_gen_543) -> q_gen_568
<z, z, nil>() -> q_gen_568
<s, s, s>(q_gen_569) -> q_gen_569
<s, z, s>(q_gen_529) -> q_gen_569
<s, z, z>(q_gen_535) -> q_gen_569
<z, s, z>(q_gen_535) -> q_gen_569
<z, z, z>() -> q_gen_569
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18  ;  () -> not_null([cons(x, ll)]) -> 15  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 14  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 31  ;  (not_null([nil])) -> BOT -> 15
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, nil)  ;  h1 -> s(z)  ;  l2 -> cons(s(s(z)), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 17, which took 0.396073 s (model generation: 0.015442,  model checking: 0.380631):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, cons>(q_gen_535, q_gen_543) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_524) -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
<nil, nil, s>(q_gen_535) -> q_gen_563
<nil, nil, z>() -> q_gen_563
<nil, s, cons>(q_gen_529, q_gen_528) -> q_gen_564
<nil, z, cons>(q_gen_535, q_gen_543) -> q_gen_564
<nil, s, s>(q_gen_529) -> q_gen_565
<nil, s, z>(q_gen_535) -> q_gen_565
<nil, z, s>(q_gen_535) -> q_gen_565
<nil, z, z>() -> q_gen_565
<s, nil, cons>(q_gen_529, q_gen_528) -> q_gen_566
<z, nil, cons>(q_gen_535, q_gen_543) -> q_gen_566
<s, nil, s>(q_gen_529) -> q_gen_567
<z, nil, z>() -> q_gen_567
<s, s, cons>(q_gen_569, q_gen_568) -> q_gen_568
<s, z, cons>(q_gen_529, q_gen_528) -> q_gen_568
<s, z, nil>(q_gen_535) -> q_gen_568
<z, s, cons>(q_gen_529, q_gen_528) -> q_gen_568
<z, s, nil>(q_gen_535) -> q_gen_568
<z, z, cons>(q_gen_535, q_gen_543) -> q_gen_568
<z, z, nil>() -> q_gen_568
<s, s, s>(q_gen_569) -> q_gen_569
<s, z, s>(q_gen_529) -> q_gen_569
<s, z, z>(q_gen_535) -> q_gen_569
<z, s, z>(q_gen_535) -> q_gen_569
<z, z, z>() -> q_gen_569
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19  ;  () -> not_null([cons(x, ll)]) -> 16  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 15  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 34  ;  (not_null([nil])) -> BOT -> 16
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, nil)  ;  h1 -> s(s(z))  ;  l2 -> cons(s(s(z)), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 18, which took 0.562892 s (model generation: 0.017299,  model checking: 0.545593):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, cons>(q_gen_535, q_gen_543) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_524) -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
<nil, nil, s>(q_gen_535) -> q_gen_563
<nil, nil, z>() -> q_gen_563
<nil, s, cons>(q_gen_529, q_gen_528) -> q_gen_564
<nil, z, cons>(q_gen_535, q_gen_543) -> q_gen_564
<nil, s, s>(q_gen_529) -> q_gen_565
<nil, s, z>(q_gen_535) -> q_gen_565
<nil, z, s>(q_gen_535) -> q_gen_565
<nil, z, z>() -> q_gen_565
<s, nil, cons>(q_gen_529, q_gen_528) -> q_gen_566
<z, nil, cons>(q_gen_535, q_gen_543) -> q_gen_566
<s, nil, s>(q_gen_529) -> q_gen_567
<z, nil, z>() -> q_gen_567
<s, s, cons>(q_gen_569, q_gen_568) -> q_gen_568
<s, s, nil>(q_gen_529) -> q_gen_568
<s, z, cons>(q_gen_529, q_gen_528) -> q_gen_568
<s, z, nil>(q_gen_535) -> q_gen_568
<z, s, cons>(q_gen_529, q_gen_528) -> q_gen_568
<z, s, nil>(q_gen_535) -> q_gen_568
<z, z, cons>(q_gen_535, q_gen_543) -> q_gen_568
<z, z, nil>() -> q_gen_568
<s, s, s>(q_gen_569) -> q_gen_569
<s, s, z>(q_gen_529) -> q_gen_569
<s, z, s>(q_gen_529) -> q_gen_569
<s, z, z>(q_gen_535) -> q_gen_569
<z, s, z>(q_gen_535) -> q_gen_569
<z, z, z>() -> q_gen_569
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20  ;  () -> not_null([cons(x, ll)]) -> 17  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 16  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 37  ;  (not_null([nil])) -> BOT -> 17
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(s(z), nil)  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.556226 s (model generation: 0.021727,  model checking: 0.534499):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, cons>(q_gen_535, q_gen_543) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_524) -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
<nil, nil, s>(q_gen_535) -> q_gen_563
<nil, nil, z>() -> q_gen_563
<nil, s, cons>(q_gen_529, q_gen_528) -> q_gen_564
<nil, z, cons>(q_gen_535, q_gen_543) -> q_gen_564
<nil, s, s>(q_gen_529) -> q_gen_565
<nil, s, z>(q_gen_535) -> q_gen_565
<nil, z, s>(q_gen_535) -> q_gen_565
<nil, z, z>() -> q_gen_565
<s, nil, cons>(q_gen_529, q_gen_528) -> q_gen_566
<z, nil, cons>(q_gen_535, q_gen_543) -> q_gen_566
<s, nil, s>(q_gen_529) -> q_gen_567
<z, nil, z>() -> q_gen_567
<s, s, cons>(q_gen_569, q_gen_568) -> q_gen_568
<s, s, nil>(q_gen_529) -> q_gen_568
<s, z, cons>(q_gen_529, q_gen_528) -> q_gen_568
<s, z, nil>(q_gen_535) -> q_gen_568
<z, s, cons>(q_gen_529, q_gen_528) -> q_gen_568
<z, s, nil>(q_gen_535) -> q_gen_568
<z, z, cons>(q_gen_535, q_gen_543) -> q_gen_568
<z, z, nil>() -> q_gen_568
<s, s, s>(q_gen_569) -> q_gen_569
<s, s, z>(q_gen_529) -> q_gen_569
<s, z, s>(q_gen_529) -> q_gen_569
<s, z, z>(q_gen_535) -> q_gen_569
<z, s, z>(q_gen_535) -> q_gen_569
<z, z, s>(q_gen_535) -> q_gen_569
<z, z, z>() -> q_gen_569
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 21  ;  () -> not_null([cons(x, ll)]) -> 18  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 17  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 40  ;  (not_null([nil])) -> BOT -> 18
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(s(z), nil)  ;  h1 -> s(z)  ;  l2 -> cons(s(s(z)), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 20, which took 0.596804 s (model generation: 0.025214,  model checking: 0.571590):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, cons>(q_gen_535, q_gen_543) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_524) -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
<nil, nil, s>(q_gen_535) -> q_gen_563
<nil, nil, z>() -> q_gen_563
<nil, s, cons>(q_gen_529, q_gen_528) -> q_gen_564
<nil, z, cons>(q_gen_535, q_gen_543) -> q_gen_564
<nil, s, s>(q_gen_529) -> q_gen_565
<nil, s, z>(q_gen_535) -> q_gen_565
<nil, z, s>(q_gen_535) -> q_gen_565
<nil, z, z>() -> q_gen_565
<s, nil, cons>(q_gen_529, q_gen_528) -> q_gen_566
<z, nil, cons>(q_gen_535, q_gen_543) -> q_gen_566
<s, nil, s>(q_gen_529) -> q_gen_567
<z, nil, z>() -> q_gen_567
<s, s, cons>(q_gen_569, q_gen_568) -> q_gen_568
<s, s, nil>(q_gen_529) -> q_gen_568
<s, z, cons>(q_gen_529, q_gen_528) -> q_gen_568
<s, z, nil>(q_gen_535) -> q_gen_568
<z, s, cons>(q_gen_529, q_gen_528) -> q_gen_568
<z, s, nil>(q_gen_535) -> q_gen_568
<z, z, cons>(q_gen_535, q_gen_543) -> q_gen_568
<z, z, nil>() -> q_gen_568
<s, s, s>(q_gen_569) -> q_gen_569
<s, s, z>(q_gen_529) -> q_gen_569
<s, z, s>(q_gen_529) -> q_gen_569
<s, z, z>(q_gen_535) -> q_gen_569
<z, s, s>(q_gen_529) -> q_gen_569
<z, s, z>(q_gen_535) -> q_gen_569
<z, z, s>(q_gen_535) -> q_gen_569
<z, z, z>() -> q_gen_569
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22  ;  () -> not_null([cons(x, ll)]) -> 19  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 18  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 43  ;  (not_null([nil])) -> BOT -> 19
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, cons(z, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 1.702693 s (model generation: 0.047012,  model checking: 1.655681):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, cons>(q_gen_535, q_gen_543) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_524) -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
<nil, cons, z>(q_gen_535, q_gen_543) -> q_gen_563
<nil, nil, s>(q_gen_535) -> q_gen_563
<nil, nil, z>() -> q_gen_563
<nil, s, cons>(q_gen_529, q_gen_528) -> q_gen_564
<nil, z, cons>(q_gen_535, q_gen_543) -> q_gen_564
<nil, s, s>(q_gen_529) -> q_gen_565
<nil, s, z>(q_gen_535) -> q_gen_565
<nil, z, s>(q_gen_535) -> q_gen_565
<nil, z, z>() -> q_gen_565
<s, nil, cons>(q_gen_529, q_gen_528) -> q_gen_566
<z, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_566
<z, nil, cons>(q_gen_535, q_gen_543) -> q_gen_566
<s, nil, s>(q_gen_529) -> q_gen_567
<z, cons, z>(q_gen_535, q_gen_543) -> q_gen_567
<z, nil, z>() -> q_gen_567
<s, s, cons>(q_gen_569, q_gen_568) -> q_gen_568
<s, s, nil>(q_gen_529) -> q_gen_568
<s, z, cons>(q_gen_529, q_gen_528) -> q_gen_568
<s, z, nil>(q_gen_535) -> q_gen_568
<z, s, cons>(q_gen_529, q_gen_528) -> q_gen_568
<z, s, nil>(q_gen_535) -> q_gen_568
<z, z, cons>(q_gen_535, q_gen_543) -> q_gen_568
<z, z, nil>() -> q_gen_568
<s, s, s>(q_gen_569) -> q_gen_569
<s, s, z>(q_gen_529) -> q_gen_569
<s, z, s>(q_gen_529) -> q_gen_569
<s, z, z>(q_gen_535) -> q_gen_569
<z, s, s>(q_gen_529) -> q_gen_569
<z, s, z>(q_gen_535) -> q_gen_569
<z, z, s>(q_gen_535) -> q_gen_569
<z, z, z>() -> q_gen_569
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23  ;  () -> not_null([cons(x, ll)]) -> 20  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 19  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 46  ;  (not_null([nil])) -> BOT -> 20
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 22, which took 1.545609 s (model generation: 0.038673,  model checking: 1.506936):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, cons>(q_gen_535, q_gen_543) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_524) -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
<cons, nil, z>(q_gen_535, q_gen_543) -> q_gen_563
<nil, cons, z>(q_gen_535, q_gen_543) -> q_gen_563
<nil, nil, s>(q_gen_535) -> q_gen_563
<nil, nil, z>() -> q_gen_563
<cons, z, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_564
<nil, s, cons>(q_gen_529, q_gen_528) -> q_gen_564
<nil, z, cons>(q_gen_535, q_gen_543) -> q_gen_564
<cons, z, z>(q_gen_535, q_gen_543) -> q_gen_565
<nil, s, s>(q_gen_529) -> q_gen_565
<nil, s, z>(q_gen_535) -> q_gen_565
<nil, z, s>(q_gen_535) -> q_gen_565
<nil, z, z>() -> q_gen_565
<s, nil, cons>(q_gen_529, q_gen_528) -> q_gen_566
<z, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_566
<z, nil, cons>(q_gen_535, q_gen_543) -> q_gen_566
<s, nil, s>(q_gen_529) -> q_gen_567
<z, cons, z>(q_gen_535, q_gen_543) -> q_gen_567
<z, nil, z>() -> q_gen_567
<s, s, cons>(q_gen_569, q_gen_568) -> q_gen_568
<s, s, nil>(q_gen_529) -> q_gen_568
<s, z, cons>(q_gen_529, q_gen_528) -> q_gen_568
<s, z, nil>(q_gen_535) -> q_gen_568
<z, s, cons>(q_gen_529, q_gen_528) -> q_gen_568
<z, s, nil>(q_gen_535) -> q_gen_568
<z, z, cons>(q_gen_535, q_gen_543) -> q_gen_568
<z, z, nil>() -> q_gen_568
<s, s, s>(q_gen_569) -> q_gen_569
<s, s, z>(q_gen_529) -> q_gen_569
<s, z, s>(q_gen_529) -> q_gen_569
<s, z, z>(q_gen_535) -> q_gen_569
<z, s, s>(q_gen_529) -> q_gen_569
<z, s, z>(q_gen_535) -> q_gen_569
<z, z, s>(q_gen_535) -> q_gen_569
<z, z, z>() -> q_gen_569
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24  ;  () -> not_null([cons(x, ll)]) -> 21  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 20  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 49  ;  (not_null([nil])) -> BOT -> 21
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(z, nil)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 23, which took 11.303959 s (model generation: 0.044260,  model checking: 11.259699):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, cons>(q_gen_535, q_gen_543) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_524) -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
<cons, nil, s>(q_gen_529, q_gen_527) -> q_gen_563
<cons, nil, z>(q_gen_535, q_gen_543) -> q_gen_563
<nil, cons, z>(q_gen_535, q_gen_543) -> q_gen_563
<nil, nil, s>(q_gen_535) -> q_gen_563
<nil, nil, z>() -> q_gen_563
<cons, z, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_564
<nil, s, cons>(q_gen_529, q_gen_528) -> q_gen_564
<nil, z, cons>(q_gen_535, q_gen_543) -> q_gen_564
<cons, z, s>(q_gen_529, q_gen_527) -> q_gen_565
<cons, z, z>(q_gen_535, q_gen_543) -> q_gen_565
<nil, s, s>(q_gen_529) -> q_gen_565
<nil, s, z>(q_gen_535) -> q_gen_565
<nil, z, s>(q_gen_535) -> q_gen_565
<nil, z, z>() -> q_gen_565
<s, nil, cons>(q_gen_529, q_gen_528) -> q_gen_566
<z, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_566
<z, nil, cons>(q_gen_535, q_gen_543) -> q_gen_566
<s, nil, s>(q_gen_529) -> q_gen_567
<z, cons, z>(q_gen_535, q_gen_543) -> q_gen_567
<z, nil, z>() -> q_gen_567
<s, s, cons>(q_gen_569, q_gen_568) -> q_gen_568
<s, s, nil>(q_gen_529) -> q_gen_568
<s, z, cons>(q_gen_529, q_gen_528) -> q_gen_568
<s, z, nil>(q_gen_535) -> q_gen_568
<z, s, cons>(q_gen_529, q_gen_528) -> q_gen_568
<z, s, nil>(q_gen_535) -> q_gen_568
<z, z, cons>(q_gen_535, q_gen_543) -> q_gen_568
<z, z, nil>() -> q_gen_568
<s, s, s>(q_gen_569) -> q_gen_569
<s, s, z>(q_gen_529) -> q_gen_569
<s, z, s>(q_gen_529) -> q_gen_569
<s, z, z>(q_gen_535) -> q_gen_569
<z, s, s>(q_gen_529) -> q_gen_569
<z, s, z>(q_gen_535) -> q_gen_569
<z, z, s>(q_gen_535) -> q_gen_569
<z, z, z>() -> q_gen_569
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 25  ;  () -> not_null([cons(x, ll)]) -> 22  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 21  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 52  ;  (not_null([nil])) -> BOT -> 22
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(s(z), nil)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 24, which took 11.407882 s (model generation: 0.056722,  model checking: 11.351160):

Model:
|_
{
append -> 
{{{
Q={q_gen_524, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_535, q_gen_543, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_567, q_gen_568, q_gen_569},
Q_f={q_gen_524},
Delta=
{
<s>(q_gen_535) -> q_gen_535
<z>() -> q_gen_535
<cons>(q_gen_535, q_gen_543) -> q_gen_543
<nil>() -> q_gen_543
<cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_526
<nil, cons>(q_gen_535, q_gen_543) -> q_gen_526
<nil, nil>() -> q_gen_526
<cons, s>(q_gen_529, q_gen_527) -> q_gen_527
<cons, z>(q_gen_535, q_gen_543) -> q_gen_527
<nil, s>(q_gen_535) -> q_gen_527
<nil, z>() -> q_gen_527
<s, cons>(q_gen_529, q_gen_528) -> q_gen_528
<s, nil>(q_gen_535) -> q_gen_528
<z, cons>(q_gen_535, q_gen_543) -> q_gen_528
<z, nil>() -> q_gen_528
<s, s>(q_gen_529) -> q_gen_529
<s, z>(q_gen_535) -> q_gen_529
<z, s>(q_gen_535) -> q_gen_529
<z, z>() -> q_gen_529
<cons, cons, cons>(q_gen_569, q_gen_568, q_gen_567, q_gen_566, q_gen_565, q_gen_564, q_gen_563, q_gen_524) -> q_gen_524
<cons, nil, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_524
<nil, nil, cons>(q_gen_535, q_gen_543) -> q_gen_524
<nil, nil, nil>() -> q_gen_524
<cons, nil, s>(q_gen_529, q_gen_527) -> q_gen_563
<cons, nil, z>(q_gen_535, q_gen_543) -> q_gen_563
<nil, cons, z>(q_gen_535, q_gen_543) -> q_gen_563
<nil, nil, s>(q_gen_535) -> q_gen_563
<nil, nil, z>() -> q_gen_563
<cons, s, cons>(q_gen_569, q_gen_568, q_gen_565, q_gen_564) -> q_gen_564
<cons, z, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_564
<nil, s, cons>(q_gen_529, q_gen_528) -> q_gen_564
<nil, z, cons>(q_gen_535, q_gen_543) -> q_gen_564
<cons, s, z>(q_gen_529, q_gen_527) -> q_gen_565
<cons, z, s>(q_gen_529, q_gen_527) -> q_gen_565
<cons, z, z>(q_gen_535, q_gen_543) -> q_gen_565
<nil, s, s>(q_gen_529) -> q_gen_565
<nil, s, z>(q_gen_535) -> q_gen_565
<nil, z, s>(q_gen_535) -> q_gen_565
<nil, z, z>() -> q_gen_565
<s, nil, cons>(q_gen_529, q_gen_528) -> q_gen_566
<z, cons, cons>(q_gen_529, q_gen_528, q_gen_527, q_gen_526) -> q_gen_566
<z, nil, cons>(q_gen_535, q_gen_543) -> q_gen_566
<s, nil, s>(q_gen_529) -> q_gen_567
<z, cons, z>(q_gen_535, q_gen_543) -> q_gen_567
<z, nil, z>() -> q_gen_567
<s, s, cons>(q_gen_569, q_gen_568) -> q_gen_568
<s, s, nil>(q_gen_529) -> q_gen_568
<s, z, cons>(q_gen_529, q_gen_528) -> q_gen_568
<s, z, nil>(q_gen_535) -> q_gen_568
<z, s, cons>(q_gen_529, q_gen_528) -> q_gen_568
<z, s, nil>(q_gen_535) -> q_gen_568
<z, z, cons>(q_gen_535, q_gen_543) -> q_gen_568
<z, z, nil>() -> q_gen_568
<s, s, s>(q_gen_569) -> q_gen_569
<s, s, z>(q_gen_529) -> q_gen_569
<s, z, s>(q_gen_529) -> q_gen_569
<s, z, z>(q_gen_535) -> q_gen_569
<z, s, s>(q_gen_529) -> q_gen_569
<z, s, z>(q_gen_535) -> q_gen_569
<z, z, s>(q_gen_535) -> q_gen_569
<z, z, z>() -> q_gen_569
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_521, q_gen_522, q_gen_523},
Q_f={q_gen_521},
Delta=
{
<cons>(q_gen_523, q_gen_521) -> q_gen_521
<cons>(q_gen_523, q_gen_522) -> q_gen_521
<nil>() -> q_gen_522
<s>(q_gen_523) -> q_gen_523
<z>() -> q_gen_523
}

Datatype: <natlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26  ;  () -> not_null([cons(x, ll)]) -> 23  ;  (append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 22  ;  (append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 55  ;  (not_null([nil])) -> BOT -> 23
}
Sat witness: Yes: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> cons(z, cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> cons(z, nil)
})

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