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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(count, F:
{() -> count([x, nil, z])
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab])
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)])}
(count([_bb, _cb, _db]) /\ count([_bb, _cb, _eb])) -> eq_nat([_db, _eb])
)
}

properties:
{(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)])}


over-approximation: {count}
under-approximation: {}

Clause system for inference is:

{
() -> count([x, nil, z]) -> 0
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 0
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 0
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 0
}


Solving took 60.000281 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_320, q_gen_321, q_gen_322, q_gen_323, q_gen_324, q_gen_325, q_gen_326, q_gen_327, q_gen_328, q_gen_329, q_gen_330, q_gen_331, q_gen_332, q_gen_333, q_gen_334, q_gen_335, q_gen_336, q_gen_337, q_gen_338, q_gen_339, q_gen_340, q_gen_341, q_gen_342, q_gen_343, q_gen_344, q_gen_345, q_gen_346, q_gen_347, q_gen_348, q_gen_349, q_gen_350, q_gen_351, q_gen_352, q_gen_353, q_gen_354, q_gen_355, q_gen_356, q_gen_357, q_gen_358, q_gen_359, q_gen_360, q_gen_361, q_gen_362, q_gen_363, 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_f={},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<nil, z>() -> q_gen_321
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_331) -> q_gen_335
<cons, z>(q_gen_322, q_gen_324) -> q_gen_340
<cons, s>(q_gen_325, q_gen_321) -> q_gen_344
<cons, s>(q_gen_322, q_gen_321) -> q_gen_348
<cons, s>(q_gen_325, q_gen_331) -> q_gen_351
<cons, s>(q_gen_322, q_gen_351) -> q_gen_355
<cons, s>(q_gen_322, q_gen_355) -> q_gen_357
<cons, s>(q_gen_322, q_gen_340) -> q_gen_359
<cons, s>(q_gen_322, q_gen_363) -> q_gen_362
<cons, s>(q_gen_325, q_gen_348) -> q_gen_363
<cons, s>(q_gen_325, q_gen_362) -> q_gen_365
<cons, s>(q_gen_325, q_gen_368) -> q_gen_367
<cons, s>(q_gen_322, q_gen_348) -> q_gen_368
<cons, s>(q_gen_322, q_gen_371) -> q_gen_370
<cons, s>(q_gen_325, q_gen_359) -> q_gen_371
<cons, s>(q_gen_325, q_gen_371) -> q_gen_376
<cons, z>(q_gen_322, q_gen_337) -> q_gen_380
<cons, s>(q_gen_322, q_gen_344) -> q_gen_382
<cons, s>(q_gen_325, q_gen_344) -> q_gen_384
<b, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_320
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_323
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
<a, nil, z>() -> q_gen_327
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_328
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_329
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_330
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_332
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_333
<a, cons, s>(q_gen_325, q_gen_335) -> q_gen_334
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_336
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_338
<a, cons, s>(q_gen_325, q_gen_340) -> q_gen_339
<b, cons, s>(q_gen_325, q_gen_340) -> q_gen_341
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_342
<a, cons, s>(q_gen_325, q_gen_344) -> q_gen_343
<b, cons, s>(q_gen_322, q_gen_344) -> q_gen_345
<b, cons, s>(q_gen_325, q_gen_335) -> q_gen_346
<b, cons, s>(q_gen_322, q_gen_348) -> q_gen_347
<b, cons, s>(q_gen_325, q_gen_344) -> q_gen_349
<b, cons, s>(q_gen_325, q_gen_351) -> q_gen_350
<b, cons, s>(q_gen_322, q_gen_351) -> q_gen_352
<a, cons, s>(q_gen_325, q_gen_351) -> q_gen_353
<b, cons, s>(q_gen_322, q_gen_355) -> q_gen_354
<b, cons, s>(q_gen_322, q_gen_357) -> q_gen_356
<b, cons, s>(q_gen_325, q_gen_359) -> q_gen_358
<a, cons, s>(q_gen_325, q_gen_348) -> q_gen_360
<b, cons, s>(q_gen_325, q_gen_362) -> q_gen_361
<b, cons, s>(q_gen_322, q_gen_365) -> q_gen_364
<a, cons, s>(q_gen_322, q_gen_367) -> q_gen_366
<a, cons, s>(q_gen_322, q_gen_370) -> q_gen_369
<b, cons, s>(q_gen_322, q_gen_340) -> q_gen_372
<b, cons, s>(q_gen_322, q_gen_368) -> q_gen_373
<a, cons, s>(q_gen_325, q_gen_367) -> q_gen_374
<a, cons, s>(q_gen_322, q_gen_376) -> q_gen_375
<a, cons, s>(q_gen_322, q_gen_321) -> q_gen_377
<b, cons, s>(q_gen_322, q_gen_335) -> q_gen_378
<a, cons, s>(q_gen_322, q_gen_380) -> q_gen_379
<a, cons, s>(q_gen_325, q_gen_382) -> q_gen_381
<a, cons, s>(q_gen_325, q_gen_384) -> q_gen_383
<b, cons, s>(q_gen_322, q_gen_384) -> q_gen_385
<b, cons, s>(q_gen_325, q_gen_355) -> q_gen_386
<b, cons, s>(q_gen_322, q_gen_380) -> q_gen_387
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010970 s (model generation: 0.010476,  model checking: 0.000494):

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

}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 1
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 1
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 1
}
Sat witness: Found: (() -> count([x, nil, z]), {
x -> b
})

-------------------------------------------
Step 1, which took 0.010480 s (model generation: 0.010208,  model checking: 0.000272):

Model:
|_
{
count -> 
{{{
Q={q_gen_319},
Q_f={q_gen_319},
Delta=
{
<b, nil, z>() -> q_gen_319
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 1
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 1
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 4
}
Sat witness: Found: ((count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]), {
_za -> z  ;  t1 -> nil  ;  x -> b
})

-------------------------------------------
Step 2, which took 0.011210 s (model generation: 0.010728,  model checking: 0.000482):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil, z>() -> q_gen_321
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, nil, z>() -> q_gen_319
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 1
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 4
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 4
}
Sat witness: Found: ((count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]), {
_ab -> z  ;  h1 -> a  ;  t1 -> nil  ;  x -> b
})

-------------------------------------------
Step 3, which took 0.016001 s (model generation: 0.011137,  model checking: 0.004864):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324},
Q_f={q_gen_319},
Delta=
{
<a>() -> q_gen_322
<b>() -> q_gen_322
<nil>() -> q_gen_324
<nil, z>() -> q_gen_321
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<b, nil, z>() -> q_gen_319
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 4
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 4
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 4
}
Sat witness: Found: ((count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]), {
_fb -> z  ;  _gb -> z  ;  l1 -> nil  ;  x -> b
})

-------------------------------------------
Step 4, which took 0.011513 s (model generation: 0.011163,  model checking: 0.000350):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<nil, z>() -> q_gen_321
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, nil, z>() -> q_gen_319
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 6
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 4
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 4
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 4
}
Sat witness: Found: (() -> count([x, nil, z]), {
x -> a
})

-------------------------------------------
Step 5, which took 0.012244 s (model generation: 0.011593,  model checking: 0.000651):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<nil, z>() -> q_gen_321
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, nil, z>() -> q_gen_319
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 6
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 4
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 4
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 7
}
Sat witness: Found: ((count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]), {
_za -> z  ;  t1 -> nil  ;  x -> a
})

-------------------------------------------
Step 6, which took 0.014935 s (model generation: 0.014014,  model checking: 0.000921):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<nil, z>() -> q_gen_321
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, nil, z>() -> q_gen_319
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 6
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 4
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 7
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 7
}
Sat witness: Found: ((count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]), {
_ab -> z  ;  h1 -> b  ;  t1 -> nil  ;  x -> a
})

-------------------------------------------
Step 7, which took 0.016338 s (model generation: 0.012180,  model checking: 0.004158):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<nil, z>() -> q_gen_321
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, nil, z>() -> q_gen_319
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 7
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 5
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 7
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 10
}
Sat witness: Found: ((count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]), {
_za -> z  ;  t1 -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 8, which took 0.014659 s (model generation: 0.014008,  model checking: 0.000651):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons, z>(q_gen_325, q_gen_324) -> q_gen_321
<nil, z>() -> q_gen_321
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, nil, z>() -> q_gen_319
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 7
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 8
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 7
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 10
}
Sat witness: Found: ((count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]), {
_fb -> s(z)  ;  _gb -> s(z)  ;  l1 -> cons(a, nil)  ;  x -> a
})

-------------------------------------------
Step 9, which took 0.015714 s (model generation: 0.013319,  model checking: 0.002395):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<nil, z>() -> q_gen_321
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 7
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 8
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 10
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 10
}
Sat witness: Found: ((count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]), {
_ab -> s(z)  ;  h1 -> b  ;  t1 -> cons(a, nil)  ;  x -> a
})

-------------------------------------------
Step 10, which took 0.019651 s (model generation: 0.014171,  model checking: 0.005480):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<nil, z>() -> q_gen_321
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 8
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 9
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 10
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 13
}
Sat witness: Found: ((count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]), {
_za -> s(z)  ;  t1 -> cons(b, cons(a, nil))  ;  x -> a
})

-------------------------------------------
Step 11, which took 0.021434 s (model generation: 0.015540,  model checking: 0.005894):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 9
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 10
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 13
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 13
}
Sat witness: Found: ((count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]), {
_ab -> z  ;  h1 -> a  ;  t1 -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 12, which took 0.021054 s (model generation: 0.016421,  model checking: 0.004633):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<cons>(q_gen_325, q_gen_324) -> q_gen_324
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 10
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 13
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 13
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 13
}
Sat witness: Found: ((count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]), {
_fb -> s(s(z))  ;  _gb -> z  ;  l1 -> cons(b, cons(a, nil))  ;  x -> a
})

-------------------------------------------
Step 13, which took 0.021496 s (model generation: 0.017610,  model checking: 0.003886):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 11
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 13
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 13
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 16
}
Sat witness: Found: ((count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]), {
_za -> z  ;  t1 -> cons(b, nil)  ;  x -> a
})

-------------------------------------------
Step 14, which took 0.022347 s (model generation: 0.018685,  model checking: 0.003662):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<cons, z>(q_gen_322, q_gen_324) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 12
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 13
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 16
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 16
}
Sat witness: Found: ((count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]), {
_ab -> s(z)  ;  h1 -> a  ;  t1 -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 15, which took 0.024257 s (model generation: 0.019587,  model checking: 0.004670):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<cons, z>(q_gen_322, q_gen_324) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 13
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 16
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 16
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 16
}
Sat witness: Found: ((count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]), {
_fb -> s(z)  ;  _gb -> s(z)  ;  l1 -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 16, which took 0.026076 s (model generation: 0.020576,  model checking: 0.005500):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337, q_gen_340},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, z>(q_gen_322, q_gen_324) -> q_gen_340
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 14
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 16
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 16
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 19
}
Sat witness: Found: ((count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]), {
_za -> s(z)  ;  t1 -> cons(a, nil)  ;  x -> a
})

-------------------------------------------
Step 17, which took 0.025904 s (model generation: 0.023092,  model checking: 0.002812):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337, q_gen_340},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<cons, s>(q_gen_325, q_gen_321) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, z>(q_gen_322, q_gen_324) -> q_gen_340
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 15
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 16
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 19
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 19
}
Sat witness: Found: ((count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]), {
_ab -> s(s(z))  ;  h1 -> a  ;  t1 -> cons(b, cons(a, nil))  ;  x -> b
})

-------------------------------------------
Step 18, which took 0.038934 s (model generation: 0.025200,  model checking: 0.013734):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337, q_gen_340},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_325, q_gen_321) -> q_gen_340
<cons, z>(q_gen_322, q_gen_324) -> q_gen_340
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_340) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 16
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 17
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 19
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 22
}
Sat witness: Found: ((count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]), {
_za -> s(z)  ;  t1 -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 19, which took 0.043449 s (model generation: 0.028263,  model checking: 0.015186):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337, q_gen_340},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_325, q_gen_321) -> q_gen_340
<cons, z>(q_gen_322, q_gen_324) -> q_gen_340
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_340) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 17
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 18
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 22
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 22
}
Sat witness: Found: ((count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]), {
_ab -> s(s(z))  ;  h1 -> a  ;  t1 -> cons(a, cons(a, nil))  ;  x -> b
})

-------------------------------------------
Step 20, which took 0.045526 s (model generation: 0.034784,  model checking: 0.010742):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337, q_gen_340},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, s>(q_gen_325, q_gen_331) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_325, q_gen_321) -> q_gen_340
<cons, z>(q_gen_322, q_gen_324) -> q_gen_340
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_340) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 18
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 21
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 22
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 22
}
Sat witness: Found: ((count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]), {
_fb -> s(s(z))  ;  _gb -> s(s(z))  ;  l1 -> cons(a, cons(a, nil))  ;  x -> b
})

-------------------------------------------
Step 21, which took 0.047238 s (model generation: 0.037975,  model checking: 0.009263):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_335, q_gen_337},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_325, q_gen_321) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_331) -> q_gen_335
<cons, s>(q_gen_325, q_gen_331) -> q_gen_335
<cons, z>(q_gen_322, q_gen_324) -> q_gen_335
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_335) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 19
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 24
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 22
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 22
}
Sat witness: Found: ((count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]), {
_fb -> s(s(z))  ;  _gb -> s(s(z))  ;  l1 -> cons(a, cons(a, nil))  ;  x -> a
})

-------------------------------------------
Step 22, which took 0.046135 s (model generation: 0.040009,  model checking: 0.006126):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_335, q_gen_337},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_325, q_gen_321) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_325, q_gen_331) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_321) -> q_gen_335
<cons, s>(q_gen_322, q_gen_331) -> q_gen_335
<cons, z>(q_gen_322, q_gen_324) -> q_gen_335
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_335) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 20
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 24
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 22
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 25
}
Sat witness: Found: ((count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]), {
_za -> s(s(s(z)))  ;  t1 -> cons(b, cons(b, cons(a, cons(a, nil))))  ;  x -> b
})

-------------------------------------------
Step 23, which took 0.048328 s (model generation: 0.044938,  model checking: 0.003390):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_335, q_gen_337},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_325, q_gen_321) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_335) -> q_gen_331
<cons, s>(q_gen_325, q_gen_331) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_321) -> q_gen_335
<cons, s>(q_gen_322, q_gen_331) -> q_gen_335
<cons, z>(q_gen_322, q_gen_324) -> q_gen_335
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_335) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 21
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 24
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 25
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 25
}
Sat witness: Found: ((count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]), {
_ab -> s(s(z))  ;  h1 -> a  ;  t1 -> cons(b, cons(b, nil))  ;  x -> b
})

-------------------------------------------
Step 24, which took 0.054748 s (model generation: 0.048945,  model checking: 0.005803):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_335, q_gen_337},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_325, q_gen_321) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_325, q_gen_331) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_321) -> q_gen_335
<cons, s>(q_gen_322, q_gen_331) -> q_gen_335
<cons, s>(q_gen_322, q_gen_335) -> q_gen_335
<cons, z>(q_gen_322, q_gen_324) -> q_gen_335
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_335) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 22
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 27
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 25
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 25
}
Sat witness: Found: ((count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]), {
_fb -> s(s(z))  ;  _gb -> z  ;  l1 -> cons(b, nil)  ;  x -> a
})

-------------------------------------------
Step 25, which took 0.059731 s (model generation: 0.051429,  model checking: 0.008302):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_335, q_gen_337},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_325, q_gen_321) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, s>(q_gen_325, q_gen_331) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_331) -> q_gen_335
<cons, s>(q_gen_322, q_gen_335) -> q_gen_335
<cons, z>(q_gen_322, q_gen_324) -> q_gen_335
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_335) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 23
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 27
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 25
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 28
}
Sat witness: Found: ((count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]), {
_za -> s(s(s(s(z))))  ;  t1 -> cons(a, cons(b, cons(a, cons(b, nil))))  ;  x -> b
})

-------------------------------------------
Step 26, which took 0.071609 s (model generation: 0.063872,  model checking: 0.007737):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_335, q_gen_337},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_325, q_gen_321) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, s>(q_gen_322, q_gen_335) -> q_gen_331
<cons, s>(q_gen_325, q_gen_331) -> q_gen_331
<cons, s>(q_gen_325, q_gen_335) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_331) -> q_gen_335
<cons, z>(q_gen_322, q_gen_324) -> q_gen_335
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_335) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 24
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 27
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 28
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 28
}
Sat witness: Found: ((count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]), {
_ab -> s(s(s(s(z))))  ;  h1 -> b  ;  t1 -> cons(b, cons(a, cons(b, cons(b, nil))))  ;  x -> a
})

-------------------------------------------
Step 27, which took 0.069801 s (model generation: 0.063680,  model checking: 0.006121):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_335, q_gen_337},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_325, q_gen_321) -> q_gen_321
<cons, s>(q_gen_325, q_gen_335) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, s>(q_gen_322, q_gen_335) -> q_gen_331
<cons, s>(q_gen_325, q_gen_331) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_331) -> q_gen_335
<cons, z>(q_gen_322, q_gen_324) -> q_gen_335
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_335) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_321) -> q_gen_326
<a, cons, s>(q_gen_322, q_gen_335) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 25
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 30
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 28
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 28
}
Sat witness: Found: ((count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]), {
_fb -> s(z)  ;  _gb -> s(z)  ;  l1 -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 28, which took 0.079375 s (model generation: 0.076427,  model checking: 0.002948):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_335, q_gen_337},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_325, q_gen_321) -> q_gen_321
<cons, s>(q_gen_325, q_gen_335) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, s>(q_gen_325, q_gen_331) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_331) -> q_gen_335
<cons, s>(q_gen_322, q_gen_335) -> q_gen_335
<cons, z>(q_gen_322, q_gen_324) -> q_gen_335
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_321) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_335) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 26
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 30
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 28
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 31
}
Sat witness: Found: ((count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]), {
_za -> s(s(z))  ;  t1 -> cons(b, cons(b, nil))  ;  x -> b
})

-------------------------------------------
Step 29, which took 0.086694 s (model generation: 0.083351,  model checking: 0.003343):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337, q_gen_340, q_gen_344},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<cons, s>(q_gen_325, q_gen_340) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, s>(q_gen_325, q_gen_331) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_340) -> q_gen_340
<cons, z>(q_gen_322, q_gen_324) -> q_gen_340
<cons, s>(q_gen_325, q_gen_321) -> q_gen_344
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_344) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_344) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_340) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_344) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_344) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 27
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 30
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 31
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 31
}
Sat witness: Found: ((count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]), {
_ab -> s(s(s(s(z))))  ;  h1 -> b  ;  t1 -> cons(a, cons(a, cons(b, cons(b, nil))))  ;  x -> a
})

-------------------------------------------
Step 30, which took 0.091226 s (model generation: 0.087547,  model checking: 0.003679):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337, q_gen_340, q_gen_344},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<cons, s>(q_gen_322, q_gen_344) -> q_gen_321
<cons, s>(q_gen_325, q_gen_344) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, s>(q_gen_325, q_gen_331) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_340) -> q_gen_340
<cons, z>(q_gen_322, q_gen_324) -> q_gen_340
<cons, s>(q_gen_325, q_gen_321) -> q_gen_344
<cons, s>(q_gen_325, q_gen_340) -> q_gen_344
<a, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_344) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_344) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_340) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_344) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_344) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 28
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 33
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 31
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 31
}
Sat witness: Found: ((count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]), {
_fb -> s(z)  ;  _gb -> s(z)  ;  l1 -> cons(b, nil)  ;  x -> a
})

-------------------------------------------
Step 31, which took 0.087247 s (model generation: 0.084320,  model checking: 0.002927):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_335, q_gen_337, q_gen_348},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_348) -> q_gen_321
<cons, s>(q_gen_325, q_gen_321) -> q_gen_321
<cons, s>(q_gen_325, q_gen_348) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_331) -> q_gen_335
<cons, s>(q_gen_322, q_gen_335) -> q_gen_335
<cons, s>(q_gen_325, q_gen_335) -> q_gen_335
<cons, z>(q_gen_322, q_gen_324) -> q_gen_335
<cons, s>(q_gen_322, q_gen_321) -> q_gen_348
<cons, s>(q_gen_325, q_gen_331) -> q_gen_348
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_335) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_348) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_335) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_348) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_321) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_348) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_335) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 29
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 33
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 31
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 34
}
Sat witness: Found: ((count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]), {
_za -> s(z)  ;  t1 -> cons(b, cons(a, nil))  ;  x -> b
})

-------------------------------------------
Step 32, which took 0.095382 s (model generation: 0.091223,  model checking: 0.004159):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337, q_gen_340, q_gen_344},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, s>(q_gen_325, q_gen_331) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_340) -> q_gen_340
<cons, s>(q_gen_325, q_gen_340) -> q_gen_340
<cons, z>(q_gen_322, q_gen_324) -> q_gen_340
<cons, s>(q_gen_325, q_gen_321) -> q_gen_344
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_340) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_344) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_321) -> q_gen_326
<a, cons, s>(q_gen_322, q_gen_344) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_340) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_344) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_344) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 30
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 33
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 34
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 34
}
Sat witness: Found: ((count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]), {
_ab -> s(z)  ;  h1 -> b  ;  t1 -> cons(b, cons(a, nil))  ;  x -> a
})

-------------------------------------------
Step 33, which took 0.098921 s (model generation: 0.095820,  model checking: 0.003101):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337, q_gen_340, q_gen_351},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, s>(q_gen_322, q_gen_351) -> q_gen_331
<cons, s>(q_gen_325, q_gen_351) -> q_gen_331
<cons, z>(q_gen_322, q_gen_337) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_340) -> q_gen_340
<cons, s>(q_gen_325, q_gen_321) -> q_gen_340
<cons, z>(q_gen_322, q_gen_324) -> q_gen_340
<cons, s>(q_gen_325, q_gen_331) -> q_gen_351
<cons, s>(q_gen_325, q_gen_340) -> q_gen_351
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_340) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_351) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_321) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_351) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_340) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_351) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 31
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 36
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 34
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 34
}
Sat witness: Found: ((count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]), {
_fb -> s(s(s(z)))  ;  _gb -> s(z)  ;  l1 -> cons(b, cons(a, nil))  ;  x -> a
})

-------------------------------------------
Step 34, which took 0.099903 s (model generation: 0.097178,  model checking: 0.002725):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337, q_gen_340, q_gen_344},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, s>(q_gen_322, q_gen_344) -> q_gen_331
<cons, s>(q_gen_325, q_gen_331) -> q_gen_331
<cons, s>(q_gen_325, q_gen_344) -> q_gen_331
<cons, z>(q_gen_322, q_gen_337) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_340) -> q_gen_340
<cons, z>(q_gen_322, q_gen_324) -> q_gen_340
<cons, s>(q_gen_325, q_gen_321) -> q_gen_344
<cons, s>(q_gen_325, q_gen_340) -> q_gen_344
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_344) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_321) -> q_gen_326
<a, cons, s>(q_gen_322, q_gen_344) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_340) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_344) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_344) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 32
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 36
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 34
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 37
}
Sat witness: Found: ((count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]), {
_za -> s(s(z))  ;  t1 -> cons(a, cons(a, nil))  ;  x -> a
})

-------------------------------------------
Step 35, which took 0.104011 s (model generation: 0.101301,  model checking: 0.002710):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337, q_gen_340, q_gen_351},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<cons, s>(q_gen_325, q_gen_340) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, s>(q_gen_322, q_gen_351) -> q_gen_331
<cons, s>(q_gen_325, q_gen_351) -> q_gen_331
<cons, z>(q_gen_322, q_gen_337) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_325, q_gen_321) -> q_gen_340
<cons, z>(q_gen_322, q_gen_324) -> q_gen_340
<cons, s>(q_gen_322, q_gen_340) -> q_gen_351
<cons, s>(q_gen_325, q_gen_331) -> q_gen_351
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_351) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_351) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_321) -> q_gen_326
<a, cons, s>(q_gen_322, q_gen_340) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_351) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_340) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_351) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 33
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 36
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 37
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 37
}
Sat witness: Found: ((count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]), {
_ab -> s(s(s(z)))  ;  h1 -> a  ;  t1 -> cons(b, cons(a, cons(a, nil)))  ;  x -> b
})

-------------------------------------------
Step 36, which took 0.112148 s (model generation: 0.109014,  model checking: 0.003134):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337, q_gen_340, q_gen_344},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, s>(q_gen_322, q_gen_344) -> q_gen_331
<cons, s>(q_gen_325, q_gen_331) -> q_gen_331
<cons, s>(q_gen_325, q_gen_340) -> q_gen_331
<cons, z>(q_gen_322, q_gen_337) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_322, q_gen_340) -> q_gen_340
<cons, s>(q_gen_325, q_gen_344) -> q_gen_340
<cons, z>(q_gen_322, q_gen_324) -> q_gen_340
<cons, s>(q_gen_325, q_gen_321) -> q_gen_344
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_344) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_321) -> q_gen_326
<a, cons, s>(q_gen_322, q_gen_344) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_340) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_344) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_344) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 34
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 39
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 37
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 37
}
Sat witness: Found: ((count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]), {
_fb -> s(z)  ;  _gb -> s(z)  ;  l1 -> cons(b, cons(a, nil))  ;  x -> b
})

-------------------------------------------
Step 37, which took 0.105257 s (model generation: 0.103171,  model checking: 0.002086):

Model:
|_
{
count -> 
{{{
Q={q_gen_319, q_gen_321, q_gen_322, q_gen_324, q_gen_325, q_gen_326, q_gen_331, q_gen_337, q_gen_340, q_gen_351},
Q_f={q_gen_319},
Delta=
{
<b>() -> q_gen_322
<nil>() -> q_gen_324
<a>() -> q_gen_325
<cons>(q_gen_325, q_gen_324) -> q_gen_337
<cons, s>(q_gen_322, q_gen_331) -> q_gen_321
<nil, z>() -> q_gen_321
<cons, s>(q_gen_322, q_gen_321) -> q_gen_331
<cons, s>(q_gen_325, q_gen_351) -> q_gen_331
<cons, z>(q_gen_325, q_gen_324) -> q_gen_331
<cons, s>(q_gen_325, q_gen_321) -> q_gen_340
<cons, s>(q_gen_325, q_gen_340) -> q_gen_340
<cons, z>(q_gen_322, q_gen_324) -> q_gen_340
<cons, s>(q_gen_322, q_gen_340) -> q_gen_351
<cons, s>(q_gen_322, q_gen_351) -> q_gen_351
<cons, s>(q_gen_325, q_gen_331) -> q_gen_351
<cons, z>(q_gen_322, q_gen_337) -> q_gen_351
<a, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_351) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_321) -> q_gen_319
<a, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<a, cons, z>(q_gen_322, q_gen_324) -> q_gen_319
<a, nil, z>() -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_321) -> q_gen_319
<b, cons, s>(q_gen_322, q_gen_331) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_340) -> q_gen_319
<b, cons, s>(q_gen_325, q_gen_351) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_324) -> q_gen_319
<b, cons, z>(q_gen_325, q_gen_337) -> q_gen_319
<b, nil, z>() -> q_gen_319
<a, cons, s>(q_gen_322, q_gen_321) -> q_gen_326
<a, cons, s>(q_gen_322, q_gen_340) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_331) -> q_gen_326
<a, cons, s>(q_gen_325, q_gen_351) -> q_gen_326
<a, cons, z>(q_gen_322, q_gen_337) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_340) -> q_gen_326
<b, cons, s>(q_gen_322, q_gen_351) -> q_gen_326
<b, cons, s>(q_gen_325, q_gen_321) -> q_gen_326
<b, cons, z>(q_gen_322, q_gen_324) -> q_gen_326
}

Datatype: <elt, eltlist, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 35
(count([x, l1, _gb]) /\ count([x, cons(x, l1), _fb])) -> eq_nat([_fb, s(_gb)]) -> 39
(count([x, t1, _ab]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _ab]) -> 37
(count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]) -> 40
}
Sat witness: Found: ((count([x, t1, _za])) -> count([x, cons(x, t1), s(_za)]), {
_za -> s(s(z))  ;  t1 -> cons(a, cons(a, nil))  ;  x -> b
})

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