Inference procedure has parameters:
Ice fuel: 200
Timeout: 60s
Convolution: left


Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)])}
(append([_za, _ab, _bb]) /\ append([_za, _ab, _cb])) -> eq_natlist([_bb, _cb])
)
(not_null, P:
{() -> not_null([cons(x, ll)])
(not_null([nil])) -> BOT}
)
}

properties:
{(append([cons(i, l1), l2, _db])) -> not_null([_db])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> not_null([cons(x, ll)]) -> 0
(append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 0
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 0
(not_null([nil])) -> BOT -> 0
}


Solving took 60.000052 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_357, q_gen_358, q_gen_359, q_gen_360, q_gen_364, q_gen_365, q_gen_366, q_gen_367, q_gen_368, q_gen_369, q_gen_370, q_gen_371, q_gen_372, q_gen_373, q_gen_374, q_gen_375, q_gen_376, q_gen_377, q_gen_378, q_gen_379, q_gen_380, q_gen_381, q_gen_382, q_gen_383, q_gen_384, q_gen_385, q_gen_386, q_gen_387, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_392, q_gen_393, q_gen_394, q_gen_395, q_gen_396, q_gen_397, q_gen_398, q_gen_399, q_gen_400, q_gen_401, q_gen_402, q_gen_403, q_gen_404, q_gen_405, q_gen_406, q_gen_407, q_gen_408, q_gen_409, q_gen_410, q_gen_411, q_gen_412, q_gen_413, q_gen_414, q_gen_415, q_gen_416, q_gen_417, q_gen_418, q_gen_419, q_gen_420, q_gen_421, q_gen_422, q_gen_423, q_gen_424, q_gen_425, q_gen_426, q_gen_427, q_gen_428, q_gen_429, q_gen_430, q_gen_431, q_gen_432},
Q_f={},
Delta=
{
<nil>() -> q_gen_370
<z>() -> q_gen_371
<cons>(q_gen_371, q_gen_370) -> q_gen_378
<s>(q_gen_371) -> q_gen_384
<s>(q_gen_408) -> q_gen_407
<s>(q_gen_384) -> q_gen_408
<nil, nil>() -> q_gen_359
<z, z>() -> q_gen_360
<cons, cons>(q_gen_366, q_gen_359) -> q_gen_365
<s, s>(q_gen_360) -> q_gen_366
<nil, cons>(q_gen_371, q_gen_370) -> q_gen_374
<cons, cons>(q_gen_366, q_gen_374) -> q_gen_391
<nil, cons>(q_gen_384, q_gen_378) -> q_gen_394
<s, z>(q_gen_371) -> q_gen_395
<s, s>(q_gen_395) -> q_gen_410
<z, s>(q_gen_371) -> q_gen_417
<nil, nil, nil>() -> q_gen_357
<cons, nil, cons>(q_gen_360, q_gen_359) -> q_gen_358
<nil, cons, cons>(q_gen_366, q_gen_365) -> q_gen_364
<nil, cons, cons>(q_gen_360, q_gen_359) -> q_gen_367
<cons, cons, cons>(q_gen_372, q_gen_369) -> q_gen_368
<nil, nil, cons>(q_gen_371, q_gen_370) -> q_gen_369
<z, z, z>() -> q_gen_372
<cons, nil, cons>(q_gen_360, q_gen_374) -> q_gen_373
<nil, cons, cons>(q_gen_360, q_gen_374) -> q_gen_375
<cons, cons, cons>(q_gen_372, q_gen_377) -> q_gen_376
<nil, nil, cons>(q_gen_371, q_gen_378) -> q_gen_377
<cons, cons, cons>(q_gen_380, q_gen_377) -> q_gen_379
<s, z, s>(q_gen_360) -> q_gen_380
<nil, cons, cons>(q_gen_366, q_gen_374) -> q_gen_381
<cons, cons, cons>(q_gen_385, q_gen_383) -> q_gen_382
<nil, nil, cons>(q_gen_384, q_gen_378) -> q_gen_383
<s, s, s>(q_gen_372) -> q_gen_385
<cons, cons, cons>(q_gen_385, q_gen_357) -> q_gen_386
<cons, cons, cons>(q_gen_389, q_gen_388) -> q_gen_387
<cons, nil, cons>(q_gen_366, q_gen_359) -> q_gen_388
<z, s, z>(q_gen_371) -> q_gen_389
<nil, cons, cons>(q_gen_360, q_gen_391) -> q_gen_390
<cons, cons, cons>(q_gen_380, q_gen_393) -> q_gen_392
<nil, cons, cons>(q_gen_395, q_gen_394) -> q_gen_393
<cons, cons, cons>(q_gen_398, q_gen_397) -> q_gen_396
<cons, cons, cons>(q_gen_389, q_gen_357) -> q_gen_397
<s, z, s>(q_gen_395) -> q_gen_398
<cons, cons, cons>(q_gen_380, q_gen_400) -> q_gen_399
<cons, cons, cons>(q_gen_401, q_gen_358) -> q_gen_400
<s, s, s>(q_gen_402) -> q_gen_401
<s, z, z>(q_gen_371) -> q_gen_402
<cons, cons, cons>(q_gen_409, q_gen_404) -> q_gen_403
<cons, cons, cons>(q_gen_406, q_gen_405) -> q_gen_404
<cons, cons, cons>(q_gen_372, q_gen_357) -> q_gen_405
<z, s, z>(q_gen_407) -> q_gen_406
<s, z, s>(q_gen_410) -> q_gen_409
<cons, cons, cons>(q_gen_380, q_gen_412) -> q_gen_411
<cons, cons, cons>(q_gen_414, q_gen_413) -> q_gen_412
<cons, cons, cons>(q_gen_372, q_gen_358) -> q_gen_413
<s, s, s>(q_gen_415) -> q_gen_414
<s, s, s>(q_gen_416) -> q_gen_415
<s, s, z>(q_gen_417) -> q_gen_416
<cons, cons, cons>(q_gen_402, q_gen_419) -> q_gen_418
<cons, cons, cons>(q_gen_422, q_gen_420) -> q_gen_419
<cons, cons, cons>(q_gen_422, q_gen_421) -> q_gen_420
<nil, cons, cons>(q_gen_395, q_gen_359) -> q_gen_421
<s, z, s>(q_gen_417) -> q_gen_422
<cons, cons, cons>(q_gen_380, q_gen_424) -> q_gen_423
<cons, cons, cons>(q_gen_402, q_gen_425) -> q_gen_424
<cons, cons, cons>(q_gen_422, q_gen_426) -> q_gen_425
<cons, cons, cons>(q_gen_427, q_gen_369) -> q_gen_426
<s, s, s>(q_gen_428) -> q_gen_427
<z, z, s>(q_gen_371) -> q_gen_428
<cons, cons, cons>(q_gen_428, q_gen_421) -> q_gen_429
<cons, cons, cons>(q_gen_372, q_gen_431) -> q_gen_430
<cons, cons, cons>(q_gen_432, q_gen_369) -> q_gen_431
<z, s, s>(q_gen_360) -> q_gen_432
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356, q_gen_361, q_gen_362, q_gen_363},
Q_f={},
Delta=
{
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<z>() -> q_gen_356
<cons>(q_gen_356, q_gen_362) -> q_gen_361
<cons>(q_gen_363, q_gen_355) -> q_gen_362
<s>(q_gen_356) -> q_gen_363
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007347 s (model generation: 0.007050,  model checking: 0.000297):

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

}

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

}

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

}
--
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([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 1
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 1
(not_null([nil])) -> BOT -> 1
}
Sat witness: Found: (() -> not_null([cons(x, ll)]), {
ll -> nil  ;  x -> z
})

-------------------------------------------
Step 1, which took 0.007545 s (model generation: 0.007400,  model checking: 0.000145):

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

}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_354) -> q_gen_354
<nil>() -> q_gen_354
<z>() -> q_gen_356
}

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

}
--
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([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 1
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 1
(not_null([nil])) -> BOT -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.010695 s (model generation: 0.010672,  model checking: 0.000023):

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

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_354) -> q_gen_354
<nil>() -> q_gen_354
<z>() -> q_gen_356
}

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

}
--
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([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 1
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 1
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((not_null([nil])) -> BOT, {

})

-------------------------------------------
Step 3, which took 0.010710 s (model generation: 0.010449,  model checking: 0.000261):

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

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<z>() -> q_gen_356
}

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

}
--
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([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 4
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 2
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]), {
_ya -> nil  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.008495 s (model generation: 0.008225,  model checking: 0.000270):

Model:
|_
{
append -> 
{{{
Q={q_gen_357, q_gen_359, q_gen_360},
Q_f={q_gen_357},
Delta=
{
<nil, nil>() -> q_gen_359
<z, z>() -> q_gen_360
<cons, nil, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, nil, nil>() -> q_gen_357
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<z>() -> q_gen_356
}

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

}
--
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([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 4
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 3
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: (() -> not_null([cons(x, ll)]), {
ll -> cons(s(z), nil)  ;  x -> z
})

-------------------------------------------
Step 5, which took 0.008701 s (model generation: 0.008277,  model checking: 0.000424):

Model:
|_
{
append -> 
{{{
Q={q_gen_357, q_gen_359, q_gen_360},
Q_f={q_gen_357},
Delta=
{
<nil, nil>() -> q_gen_359
<z, z>() -> q_gen_360
<cons, nil, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, nil, nil>() -> q_gen_357
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_354) -> q_gen_354
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<s>(q_gen_356) -> q_gen_356
<z>() -> q_gen_356
}

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

}
--
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([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 4
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 4
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(s(z), cons(s(z), nil))
})

-------------------------------------------
Step 6, which took 0.010147 s (model generation: 0.008900,  model checking: 0.001247):

Model:
|_
{
append -> 
{{{
Q={q_gen_357, q_gen_359, q_gen_360},
Q_f={q_gen_357},
Delta=
{
<cons, cons>(q_gen_360, q_gen_359) -> q_gen_359
<nil, nil>() -> q_gen_359
<s, s>(q_gen_360) -> q_gen_360
<z, z>() -> q_gen_360
<cons, nil, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, cons, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, nil, nil>() -> q_gen_357
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_354) -> q_gen_354
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<s>(q_gen_356) -> q_gen_356
<z>() -> q_gen_356
}

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

}
--
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([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 7
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 5
(not_null([nil])) -> BOT -> 5
}
Sat witness: Found: ((append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]), {
_ya -> cons(z, nil)  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.012093 s (model generation: 0.011153,  model checking: 0.000940):

Model:
|_
{
append -> 
{{{
Q={q_gen_357, q_gen_359, q_gen_360, q_gen_370, q_gen_371, q_gen_372},
Q_f={q_gen_357},
Delta=
{
<nil>() -> q_gen_370
<z>() -> q_gen_371
<cons, cons>(q_gen_360, q_gen_359) -> q_gen_359
<nil, nil>() -> q_gen_359
<s, s>(q_gen_360) -> q_gen_360
<z, z>() -> q_gen_360
<cons, cons, cons>(q_gen_372, q_gen_357) -> q_gen_357
<cons, nil, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, cons, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, nil, cons>(q_gen_371, q_gen_370) -> q_gen_357
<nil, nil, nil>() -> q_gen_357
<z, z, z>() -> q_gen_372
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_354) -> q_gen_354
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<s>(q_gen_356) -> q_gen_356
<z>() -> q_gen_356
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> not_null([cons(x, ll)]) -> 7
(append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 10
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 6
(not_null([nil])) -> BOT -> 6
}
Sat witness: Found: ((append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]), {
_ya -> cons(z, nil)  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 8, which took 0.011933 s (model generation: 0.010318,  model checking: 0.001615):

Model:
|_
{
append -> 
{{{
Q={q_gen_357, q_gen_359, q_gen_360, q_gen_370, q_gen_371, q_gen_372},
Q_f={q_gen_357},
Delta=
{
<nil>() -> q_gen_370
<z>() -> q_gen_371
<cons, cons>(q_gen_360, q_gen_359) -> q_gen_359
<nil, cons>(q_gen_371, q_gen_370) -> q_gen_359
<nil, nil>() -> q_gen_359
<s, s>(q_gen_360) -> q_gen_360
<z, z>() -> q_gen_360
<cons, cons, cons>(q_gen_372, q_gen_357) -> q_gen_357
<cons, nil, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, cons, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, nil, cons>(q_gen_371, q_gen_370) -> q_gen_357
<nil, nil, nil>() -> q_gen_357
<z, z, z>() -> q_gen_372
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_354) -> q_gen_354
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<s>(q_gen_356) -> q_gen_356
<z>() -> q_gen_356
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> not_null([cons(x, ll)]) -> 8
(append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 13
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 7
(not_null([nil])) -> BOT -> 7
}
Sat witness: Found: ((append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]), {
_ya -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 9, which took 0.014295 s (model generation: 0.011711,  model checking: 0.002584):

Model:
|_
{
append -> 
{{{
Q={q_gen_357, q_gen_359, q_gen_360, q_gen_370, q_gen_371, q_gen_372},
Q_f={q_gen_357},
Delta=
{
<cons>(q_gen_371, q_gen_370) -> q_gen_370
<nil>() -> q_gen_370
<z>() -> q_gen_371
<cons, cons>(q_gen_360, q_gen_359) -> q_gen_359
<nil, cons>(q_gen_371, q_gen_370) -> q_gen_359
<nil, nil>() -> q_gen_359
<s, s>(q_gen_360) -> q_gen_360
<z, z>() -> q_gen_360
<cons, cons, cons>(q_gen_372, q_gen_357) -> q_gen_357
<cons, nil, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, cons, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, nil, cons>(q_gen_371, q_gen_370) -> q_gen_357
<nil, nil, nil>() -> q_gen_357
<z, z, z>() -> q_gen_372
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_354) -> q_gen_354
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<s>(q_gen_356) -> q_gen_356
<z>() -> q_gen_356
}

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

}
--
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)]) -> 9
(append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 16
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 8
(not_null([nil])) -> BOT -> 8
}
Sat witness: Found: ((append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]), {
_ya -> cons(z, cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.015962 s (model generation: 0.012341,  model checking: 0.003621):

Model:
|_
{
append -> 
{{{
Q={q_gen_357, q_gen_359, q_gen_360, q_gen_370, q_gen_371, q_gen_372},
Q_f={q_gen_357},
Delta=
{
<cons>(q_gen_371, q_gen_370) -> q_gen_370
<nil>() -> q_gen_370
<z>() -> q_gen_371
<cons, cons>(q_gen_360, q_gen_359) -> q_gen_359
<nil, cons>(q_gen_371, q_gen_370) -> q_gen_359
<nil, nil>() -> q_gen_359
<s, s>(q_gen_360) -> q_gen_360
<z, z>() -> q_gen_360
<cons, cons, cons>(q_gen_372, q_gen_357) -> q_gen_357
<cons, nil, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, cons, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, nil, cons>(q_gen_371, q_gen_370) -> q_gen_357
<nil, nil, nil>() -> q_gen_357
<s, z, s>(q_gen_360) -> q_gen_372
<z, z, z>() -> q_gen_372
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_354) -> q_gen_354
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<s>(q_gen_356) -> q_gen_356
<z>() -> q_gen_356
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> not_null([cons(x, ll)]) -> 10
(append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 19
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 9
(not_null([nil])) -> BOT -> 9
}
Sat witness: Found: ((append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]), {
_ya -> cons(s(z), cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.025613 s (model generation: 0.020795,  model checking: 0.004818):

Model:
|_
{
append -> 
{{{
Q={q_gen_357, q_gen_359, q_gen_360, q_gen_370, q_gen_371, q_gen_372},
Q_f={q_gen_357},
Delta=
{
<cons>(q_gen_371, q_gen_370) -> q_gen_370
<nil>() -> q_gen_370
<s>(q_gen_371) -> q_gen_371
<z>() -> q_gen_371
<cons, cons>(q_gen_360, q_gen_359) -> q_gen_359
<nil, cons>(q_gen_371, q_gen_370) -> q_gen_359
<nil, nil>() -> q_gen_359
<s, s>(q_gen_360) -> q_gen_360
<z, z>() -> q_gen_360
<cons, cons, cons>(q_gen_372, q_gen_357) -> q_gen_357
<cons, nil, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, cons, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, nil, cons>(q_gen_371, q_gen_370) -> q_gen_357
<nil, nil, nil>() -> q_gen_357
<s, s, s>(q_gen_372) -> q_gen_372
<s, z, s>(q_gen_360) -> q_gen_372
<z, z, z>() -> q_gen_372
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_354) -> q_gen_354
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<s>(q_gen_356) -> q_gen_356
<z>() -> q_gen_356
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> not_null([cons(x, ll)]) -> 11
(append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 22
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 10
(not_null([nil])) -> BOT -> 10
}
Sat witness: Found: ((append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]), {
_ya -> cons(s(z), nil)  ;  h1 -> z  ;  l2 -> cons(s(z), nil)  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 12, which took 0.026043 s (model generation: 0.017987,  model checking: 0.008056):

Model:
|_
{
append -> 
{{{
Q={q_gen_357, q_gen_359, q_gen_360, q_gen_370, q_gen_371, q_gen_372},
Q_f={q_gen_357},
Delta=
{
<cons>(q_gen_371, q_gen_370) -> q_gen_370
<nil>() -> q_gen_370
<s>(q_gen_371) -> q_gen_371
<z>() -> q_gen_371
<cons, cons>(q_gen_360, q_gen_359) -> q_gen_359
<nil, cons>(q_gen_371, q_gen_370) -> q_gen_359
<nil, nil>() -> q_gen_359
<s, s>(q_gen_360) -> q_gen_360
<z, z>() -> q_gen_360
<cons, cons, cons>(q_gen_372, q_gen_357) -> q_gen_357
<cons, nil, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, cons, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, nil, cons>(q_gen_371, q_gen_370) -> q_gen_357
<nil, nil, nil>() -> q_gen_357
<s, s, s>(q_gen_372) -> q_gen_372
<s, z, s>(q_gen_360) -> q_gen_372
<z, s, z>(q_gen_371) -> q_gen_372
<z, z, z>() -> q_gen_372
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_354) -> q_gen_354
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<s>(q_gen_356) -> q_gen_356
<z>() -> q_gen_356
}

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

}
--
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)]) -> 12
(append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 25
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 11
(not_null([nil])) -> BOT -> 11
}
Sat witness: Found: ((append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]), {
_ya -> cons(z, cons(s(z), cons(z, nil)))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(s(z), nil))  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.038679 s (model generation: 0.022108,  model checking: 0.016571):

Model:
|_
{
append -> 
{{{
Q={q_gen_357, q_gen_359, q_gen_360, q_gen_370, q_gen_371, q_gen_372},
Q_f={q_gen_357},
Delta=
{
<cons>(q_gen_371, q_gen_370) -> q_gen_370
<nil>() -> q_gen_370
<s>(q_gen_371) -> q_gen_371
<z>() -> q_gen_371
<cons, cons>(q_gen_360, q_gen_359) -> q_gen_359
<nil, cons>(q_gen_371, q_gen_370) -> q_gen_359
<nil, nil>() -> q_gen_359
<s, s>(q_gen_360) -> q_gen_360
<s, z>(q_gen_371) -> q_gen_360
<z, z>() -> q_gen_360
<cons, cons, cons>(q_gen_372, q_gen_357) -> q_gen_357
<cons, nil, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, cons, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, nil, cons>(q_gen_371, q_gen_370) -> q_gen_357
<nil, nil, nil>() -> q_gen_357
<s, s, s>(q_gen_372) -> q_gen_372
<s, z, s>(q_gen_360) -> q_gen_372
<z, s, z>(q_gen_371) -> q_gen_372
<z, z, z>() -> q_gen_372
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_354) -> q_gen_354
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<s>(q_gen_356) -> q_gen_356
<z>() -> q_gen_356
}

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

}
--
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)]) -> 13
(append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 28
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 12
(not_null([nil])) -> BOT -> 12
}
Sat witness: Found: ((append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]), {
_ya -> cons(s(z), cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(s(z), nil))  ;  t1 -> cons(s(s(z)), cons(z, nil))
})

-------------------------------------------
Step 14, which took 0.058330 s (model generation: 0.035245,  model checking: 0.023085):

Model:
|_
{
append -> 
{{{
Q={q_gen_357, q_gen_359, q_gen_360, q_gen_370, q_gen_371, q_gen_372},
Q_f={q_gen_357},
Delta=
{
<cons>(q_gen_371, q_gen_370) -> q_gen_370
<nil>() -> q_gen_370
<s>(q_gen_371) -> q_gen_371
<z>() -> q_gen_371
<cons, cons>(q_gen_360, q_gen_359) -> q_gen_359
<nil, cons>(q_gen_371, q_gen_370) -> q_gen_359
<nil, nil>() -> q_gen_359
<s, s>(q_gen_360) -> q_gen_360
<s, z>(q_gen_371) -> q_gen_360
<z, z>() -> q_gen_360
<cons, cons, cons>(q_gen_372, q_gen_357) -> q_gen_357
<cons, nil, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, cons, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, nil, cons>(q_gen_371, q_gen_370) -> q_gen_357
<nil, nil, nil>() -> q_gen_357
<s, s, s>(q_gen_372) -> q_gen_372
<s, z, s>(q_gen_360) -> q_gen_372
<s, z, z>(q_gen_371) -> q_gen_372
<z, s, z>(q_gen_371) -> q_gen_372
<z, z, z>() -> q_gen_372
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_354) -> q_gen_354
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<s>(q_gen_356) -> q_gen_356
<z>() -> q_gen_356
}

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

}
--
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)]) -> 14
(append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 31
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 13
(not_null([nil])) -> BOT -> 13
}
Sat witness: Found: ((append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]), {
_ya -> cons(s(s(z)), cons(z, cons(z, nil)))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(s(s(s(s(z)))), cons(z, nil)))  ;  t1 -> cons(s(s(s(z))), cons(z, cons(z, nil)))
})

-------------------------------------------
Step 15, which took 0.105775 s (model generation: 0.074225,  model checking: 0.031550):

Model:
|_
{
append -> 
{{{
Q={q_gen_357, q_gen_359, q_gen_360, q_gen_370, q_gen_371, q_gen_372},
Q_f={q_gen_357},
Delta=
{
<cons>(q_gen_371, q_gen_370) -> q_gen_370
<nil>() -> q_gen_370
<s>(q_gen_371) -> q_gen_371
<z>() -> q_gen_371
<cons, cons>(q_gen_360, q_gen_359) -> q_gen_359
<nil, cons>(q_gen_371, q_gen_370) -> q_gen_359
<nil, nil>() -> q_gen_359
<s, s>(q_gen_360) -> q_gen_360
<s, z>(q_gen_371) -> q_gen_360
<z, s>(q_gen_371) -> q_gen_360
<z, z>() -> q_gen_360
<cons, cons, cons>(q_gen_372, q_gen_357) -> q_gen_357
<cons, nil, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, cons, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, nil, cons>(q_gen_371, q_gen_370) -> q_gen_357
<nil, nil, nil>() -> q_gen_357
<s, s, s>(q_gen_372) -> q_gen_372
<s, s, z>(q_gen_360) -> q_gen_372
<s, z, s>(q_gen_360) -> q_gen_372
<s, z, z>(q_gen_371) -> q_gen_372
<z, s, z>(q_gen_371) -> q_gen_372
<z, z, z>() -> q_gen_372
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_354) -> q_gen_354
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<s>(q_gen_356) -> q_gen_356
<z>() -> q_gen_356
}

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

}
--
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)]) -> 15
(append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 34
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 14
(not_null([nil])) -> BOT -> 14
}
Sat witness: Found: ((append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]), {
_ya -> cons(z, cons(s(s(z)), cons(s(s(z)), cons(z, nil))))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(z, cons(z, cons(s(z), nil))))  ;  t1 -> cons(s(z), cons(s(z), cons(s(z), nil)))
})

-------------------------------------------
Step 16, which took 0.121776 s (model generation: 0.101181,  model checking: 0.020595):

Model:
|_
{
append -> 
{{{
Q={q_gen_357, q_gen_359, q_gen_360, q_gen_370, q_gen_371, q_gen_372},
Q_f={q_gen_357},
Delta=
{
<cons>(q_gen_371, q_gen_370) -> q_gen_370
<nil>() -> q_gen_370
<s>(q_gen_371) -> q_gen_371
<z>() -> q_gen_371
<cons, cons>(q_gen_360, q_gen_359) -> q_gen_359
<nil, cons>(q_gen_371, q_gen_370) -> q_gen_359
<nil, nil>() -> q_gen_359
<s, s>(q_gen_360) -> q_gen_360
<s, z>(q_gen_371) -> q_gen_360
<z, s>(q_gen_371) -> q_gen_360
<z, z>() -> q_gen_360
<cons, cons, cons>(q_gen_372, q_gen_357) -> q_gen_357
<cons, nil, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, cons, cons>(q_gen_360, q_gen_359) -> q_gen_357
<nil, nil, cons>(q_gen_371, q_gen_370) -> q_gen_357
<nil, nil, nil>() -> q_gen_357
<s, s, s>(q_gen_372) -> q_gen_372
<s, s, z>(q_gen_360) -> q_gen_372
<s, z, s>(q_gen_360) -> q_gen_372
<s, z, z>(q_gen_371) -> q_gen_372
<z, s, z>(q_gen_371) -> q_gen_372
<z, z, s>(q_gen_371) -> q_gen_372
<z, z, z>() -> q_gen_372
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_354, q_gen_355, q_gen_356},
Q_f={q_gen_354},
Delta=
{
<cons>(q_gen_356, q_gen_354) -> q_gen_354
<cons>(q_gen_356, q_gen_355) -> q_gen_354
<nil>() -> q_gen_355
<s>(q_gen_356) -> q_gen_356
<z>() -> q_gen_356
}

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

}
--
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)]) -> 16
(append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]) -> 37
(append([cons(i, l1), l2, _db])) -> not_null([_db]) -> 15
(not_null([nil])) -> BOT -> 15
}
Sat witness: Found: ((append([t1, l2, _ya])) -> append([cons(h1, t1), l2, cons(h1, _ya)]), {
_ya -> cons(s(z), cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, cons(s(z), nil))  ;  t1 -> cons(z, nil)
})

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