Solving ../../benchmarks/smtlib/true/isaplanner_prop4.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: Some(60.) (sec)
Teacher_type: Checks all clauses every time
Approximation method: remove every clause that can be safely removed



Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(count, F:
{
count(x, nil, z) <= True
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)
}
eq_nat(_gc, _hc) <= count(_ec, _fc, _gc) /\ count(_ec, _fc, _hc)
)
}

properties:
{
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)
}


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

Clause system for inference is:

{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}


Solving took 60.058692 seconds.
Maybe:  timeout during teacher: {
count(x, nil, z) <= True -> out of time
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> out of time
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> out of time
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> out of time
}Last solver state:

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, cons(a, nil)), s(s(z))) <= True
count(a, cons(a, cons(b, cons(a, nil))), s(s(z))) <= True
count(a, cons(a, cons(b, nil)), s(z)) <= True
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True
count(a, cons(b, cons(a, nil)), s(z)) <= True
count(a, cons(b, cons(b, cons(a, nil))), s(z)) <= True
count(a, cons(b, cons(b, nil)), z) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, cons(a, cons(b, nil))), s(z)) <= True
count(b, cons(a, cons(a, nil)), z) <= True
count(b, cons(a, cons(b, cons(b, nil))), s(s(z))) <= True
count(b, cons(a, cons(b, nil)), s(z)) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, cons(a, cons(a, nil))), s(z)) <= True
count(b, cons(b, cons(a, nil)), s(z)) <= True
count(b, cons(b, cons(b, nil)), s(s(z))) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(a, cons(a, cons(a, nil)), s(z))
False <= count(a, cons(a, cons(b, nil)), s(s(z)))
False <= count(a, cons(a, nil), s(s(z)))
False <= count(a, cons(a, nil), z)
False <= count(a, cons(b, cons(a, nil)), z)
False <= count(a, cons(b, nil), s(z))
count(b, cons(b, cons(a, cons(a, nil))), s(s(s(z)))) <= count(b, cons(a, cons(a, nil)), s(s(z)))
False <= count(b, cons(a, cons(a, nil)), s(z))
False <= count(b, cons(a, cons(b, nil)), z)
count(b, cons(b, cons(a, nil)), s(s(s(z)))) <= count(b, cons(a, nil), s(s(z)))
False <= count(b, cons(a, nil), s(z))
False <= count(b, cons(b, cons(a, cons(a, nil))), s(s(z)))
False <= count(b, cons(b, cons(a, cons(b, nil))), s(z))
False <= count(b, cons(b, cons(a, nil)), s(s(z)))
False <= count(b, cons(b, cons(b, cons(b, nil))), s(z)) /\ count(b, cons(b, cons(b, nil)), s(z))
False <= count(b, cons(b, nil), s(s(z)))
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(a, s(x_1_0)) <= True
  _r_1(b, z) <= True
  _r_2(a, z) <= True
  _r_2(b, s(x_1_0)) <= True
  _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1)
  _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_1) /\ _r_6(x_0_0)
  _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1)
  _r_4(cons(x_0_0, x_0_1)) <= _r_7(x_0_0)
  _r_5(nil) <= True
  _r_6(a) <= True
  _r_7(b) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_3(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_4(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_5(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_7(x_1_0)
  count(a, cons(x_1_0, x_1_1), z) <= _r_4(x_1_1)
  count(a, cons(x_1_0, x_1_1), z) <= _r_5(x_1_1) /\ _r_7(x_1_0)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_3(x_1_1) /\ _r_7(x_1_0)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_5(x_1_1) /\ _r_7(x_1_0)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_4(x_1_1)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) /\ _r_6(x_1_0)
  count(b, cons(x_1_0, x_1_1), z) <= _r_3(x_1_1)
  count(b, cons(x_1_0, x_1_1), z) <= _r_5(x_1_1) /\ _r_6(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|






-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005432 s (model generation: 0.005400,  model checking: 0.000032):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
Yes: {
x -> b
}

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
No: ()

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
No: ()

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
No: ()


-------------------------------------------
Step 1, which took 0.005605 s (model generation: 0.005531,  model checking: 0.000074):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(b, nil, z) <= True
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
Yes: {
x -> a
}

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
No: ()

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
Yes: {
_cc -> z  ;  t1 -> nil  ;  x -> b
}

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
Yes: {
_dc -> z  ;  h1 -> a  ;  t1 -> nil  ;  x -> b
}


-------------------------------------------
Step 2, which took 0.006925 s (model generation: 0.006853,  model checking: 0.000072):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, nil, z) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True
  count(b, cons(x_1_0, x_1_1), z) <= True
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> z  ;  _jc -> z  ;  l1 -> nil  ;  x -> b
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
Yes: {
_cc -> z  ;  t1 -> nil  ;  x -> a
}

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
Yes: {
_dc -> z  ;  h1 -> b  ;  t1 -> nil  ;  x -> a
}


-------------------------------------------
Step 3, which took 0.010045 s (model generation: 0.009895,  model checking: 0.000150):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(a) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= True
  count(a, cons(x_1_0, x_1_1), z) <= True
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True
  count(b, cons(x_1_0, x_1_1), z) <= _r_1(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> z  ;  _jc -> z  ;  l1 -> nil  ;  x -> a
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
No: ()

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
No: ()


-------------------------------------------
Step 4, which took 0.014598 s (model generation: 0.014322,  model checking: 0.000276):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(a, cons(a, nil), z)
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(a) <= True
  _r_2(b) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= True
  count(a, cons(x_1_0, x_1_1), z) <= _r_2(x_1_0)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True
  count(b, cons(x_1_0, x_1_1), z) <= _r_1(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> s(z)  ;  _jc -> s(_yshh_0)  ;  l1 -> cons(_zshh_0, _zshh_1)  ;  x -> a
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
No: ()

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
No: ()


-------------------------------------------
Step 5, which took 0.020839 s (model generation: 0.020445,  model checking: 0.000394):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(a, cons(a, cons(a, nil)), s(z))
False <= count(a, cons(a, nil), z)
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(nil) <= True
  _r_2(a) <= True
  _r_3(b) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1)
  count(a, cons(x_1_0, x_1_1), z) <= _r_3(x_1_0)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True
  count(b, cons(x_1_0, x_1_1), z) <= _r_2(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> s(z)  ;  _jc -> s(_mwhh_0)  ;  l1 -> cons(_nwhh_0, _nwhh_1)  ;  x -> b
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
Yes: {
_cc -> z  ;  t1 -> cons(b, _nxhh_1)  ;  x -> a
}

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
Yes: {
_dc -> s(_sxhh_0)  ;  h1 -> b  ;  t1 -> cons(_uxhh_0, nil)  ;  x -> a
}


-------------------------------------------
Step 6, which took 0.032403 s (model generation: 0.031681,  model checking: 0.000722):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, cons(b, nil)), s(z)) <= True
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, cons(a, nil)), s(z)) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(a, cons(a, cons(a, nil)), s(z))
False <= count(a, cons(a, nil), z)
False <= count(b, cons(a, nil), s(z)) /\ count(b, cons(b, cons(a, nil)), s(z))
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0)
  _r_1(nil) <= True
  _r_2(a) <= True
  _r_3(b) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0)
  count(a, cons(x_1_0, x_1_1), z) <= _r_3(x_1_0)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1)
  count(b, cons(x_1_0, x_1_1), z) <= _r_2(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> s(s(_vdih_0))  ;  _jc -> z  ;  l1 -> nil  ;  x -> b
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
Yes: {
_cc -> z  ;  t1 -> cons(a, _dcih_1)  ;  x -> b
}

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
Yes: {
_dc -> s(_ycih_0)  ;  h1 -> a  ;  t1 -> cons(a, nil)  ;  x -> b
}


-------------------------------------------
Step 7, which took 0.055402 s (model generation: 0.054491,  model checking: 0.000911):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, cons(b, nil)), s(z)) <= True
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, cons(a, nil)), s(z)) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, cons(a, nil)), s(z)) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(a, cons(a, cons(a, nil)), s(z))
False <= count(a, cons(a, nil), z)
False <= count(b, cons(a, nil), s(z))
False <= count(b, cons(b, nil), s(s(z)))
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(cons(x_0_0, x_0_1), z) <= True
  _r_2(cons(x_0_0, x_0_1), z) <= _r_3(x_0_0)
  _r_2(nil, z) <= True
  _r_3(b) <= True
  _r_4(a) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0)
  count(a, cons(x_1_0, x_1_1), z) <= _r_3(x_1_0)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_3(x_1_0)
  count(b, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> s(z)  ;  _jc -> s(z)  ;  l1 -> cons(b, nil)  ;  x -> a
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
Yes: {
_cc -> s(_rhih_0)  ;  t1 -> cons(b, _shih_1)  ;  x -> a
}

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
No: ()


-------------------------------------------
Step 8, which took 0.056000 s (model generation: 0.054630,  model checking: 0.001370):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, cons(b, nil)), s(z)) <= True
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, cons(a, nil)), s(z)) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, cons(a, nil)), s(z)) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(a, cons(a, cons(a, nil)), s(z))
False <= count(a, cons(a, nil), z)
False <= count(a, cons(b, nil), s(z))
False <= count(b, cons(a, nil), s(z))
False <= count(b, cons(b, nil), s(s(z)))
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(cons(x_0_0, x_0_1), z) <= True
  _r_2(cons(x_0_0, x_0_1), z) <= _r_4(x_0_0)
  _r_2(nil, z) <= True
  _r_3(a) <= True
  _r_4(b) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_0)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_3(x_1_0)
  count(a, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_4(x_1_0)
  count(b, cons(x_1_0, x_1_1), z) <= _r_3(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> s(z)  ;  _jc -> s(z)  ;  l1 -> cons(_eoih_0, cons(_bwih_0, _bwih_1))  ;  x -> b
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
Yes: {
_cc -> s(z)  ;  t1 -> cons(b, cons(_vvih_0, _vvih_1))  ;  x -> a
}

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
No: ()


-------------------------------------------
Step 9, which took 0.089110 s (model generation: 0.087377,  model checking: 0.001733):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, cons(b, cons(a, nil))), s(s(z))) <= True
count(a, cons(a, cons(b, nil)), s(z)) <= True
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, cons(a, nil)), s(z)) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, cons(a, nil)), s(z)) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(a, cons(a, cons(a, nil)), s(z))
False <= count(a, cons(a, nil), z)
False <= count(a, cons(b, nil), s(z))
False <= count(b, cons(a, cons(a, nil)), s(z)) /\ count(b, cons(b, cons(a, cons(a, nil))), s(z))
False <= count(b, cons(a, nil), s(z))
False <= count(b, cons(b, nil), s(s(z)))
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True
  _r_1(cons(x_0_0, x_0_1), z) <= _r_4(x_0_0)
  _r_1(nil, z) <= True
  _r_2(cons(x_0_0, x_0_1), z) <= True
  _r_3(a) <= True
  _r_4(b) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_3(x_1_0)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_4(x_1_0)
  count(a, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_0)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_4(x_1_0)
  count(b, cons(x_1_0, x_1_1), z) <= _r_3(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> s(s(_dhjh_0))  ;  _jc -> z  ;  l1 -> cons(a, _azih_1)  ;  x -> b
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
No: ()

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
Yes: {
_dc -> s(z)  ;  h1 -> a  ;  t1 -> cons(b, nil)  ;  x -> b
}


-------------------------------------------
Step 10, which took 0.201363 s (model generation: 0.200000,  model checking: 0.001363):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, cons(b, cons(a, nil))), s(s(z))) <= True
count(a, cons(a, cons(b, nil)), s(z)) <= True
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, cons(a, nil)), s(z)) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, cons(b, nil)), s(z)) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, cons(a, nil)), s(z)) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(a, cons(a, cons(a, nil)), s(z))
False <= count(a, cons(a, nil), z)
False <= count(a, cons(b, nil), s(z))
False <= count(b, cons(a, cons(a, nil)), s(z)) /\ count(b, cons(b, cons(a, cons(a, nil))), s(z))
False <= count(b, cons(a, nil), s(z))
False <= count(b, cons(b, cons(a, nil)), s(s(z)))
False <= count(b, cons(b, nil), s(s(z)))
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(cons(x_0_0, x_0_1), z) <= _r_4(x_0_0)
  _r_1(nil, z) <= True
  _r_2(a, s(x_1_0)) <= True
  _r_2(b, z) <= True
  _r_3(cons(x_0_0, x_0_1)) <= True
  _r_4(b) <= True
  _r_5(a) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_5(x_1_0)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_3(x_1_1)
  count(a, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_3(x_1_1)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0)
  count(b, cons(x_1_0, x_1_1), z) <= _r_5(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> s(s(_prjh_0))  ;  _jc -> z  ;  l1 -> cons(b, _djjh_1)  ;  x -> a
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
Yes: {
_cc -> s(z)  ;  t1 -> cons(b, _rnjh_1)  ;  x -> b
}

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
Yes: {
_dc -> s(s(_irjh_0))  ;  h1 -> b  ;  t1 -> cons(a, cons(_brjh_0, _brjh_1))  ;  x -> a
}


-------------------------------------------
Step 11, which took 0.387489 s (model generation: 0.384314,  model checking: 0.003175):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, cons(b, cons(a, nil))), s(s(z))) <= True
count(a, cons(a, cons(b, nil)), s(z)) <= True
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, cons(a, nil)), s(z)) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, cons(b, nil)), s(z)) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, cons(a, nil)), s(z)) <= True
count(b, cons(b, cons(b, nil)), s(s(z))) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= count(a, cons(a, cons(a, nil)), s(s(z)))
False <= count(a, cons(a, cons(a, nil)), s(z))
False <= count(a, cons(a, cons(b, nil)), s(s(z)))
False <= count(a, cons(a, nil), z)
False <= count(a, cons(b, nil), s(z))
False <= count(b, cons(a, cons(a, nil)), s(z)) /\ count(b, cons(b, cons(a, cons(a, nil))), s(z))
False <= count(b, cons(a, nil), s(z))
False <= count(b, cons(b, cons(a, nil)), s(s(z)))
False <= count(b, cons(b, nil), s(s(z)))
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(nil, z) <= True
  _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1, x_1_0)
  _r_2(cons(x_0_0, x_0_1), z) <= True
  _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_0)
  _r_4(a) <= True
  _r_5(b) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_0)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_3(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_5(x_1_0)
  count(a, cons(x_1_0, x_1_1), z) <= _r_5(x_1_0)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_5(x_1_0)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_5(x_1_0)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1)
  count(b, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> s(z)  ;  _jc -> s(_lwjh_0)  ;  l1 -> cons(b, cons(b, _fmkh_1))  ;  x -> b
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
Yes: {
_cc -> s(z)  ;  t1 -> cons(a, nil)  ;  x -> a
}

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
Yes: {
_dc -> s(_okkh_0)  ;  h1 -> a  ;  t1 -> cons(a, cons(b, _klkh_1))  ;  x -> b
}


-------------------------------------------
Step 12, which took 0.480269 s (model generation: 0.474041,  model checking: 0.006228):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, cons(a, nil)), s(s(z))) <= True
count(a, cons(a, cons(b, cons(a, nil))), s(s(z))) <= True
count(a, cons(a, cons(b, nil)), s(z)) <= True
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True
count(a, cons(b, cons(a, nil)), s(z)) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, cons(a, cons(b, nil))), s(z)) <= True
count(b, cons(a, cons(b, nil)), s(z)) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, cons(a, nil)), s(z)) <= True
count(b, cons(b, cons(b, nil)), s(s(z))) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(a, cons(a, cons(a, nil)), s(z))
False <= count(a, cons(a, cons(b, nil)), s(s(z)))
False <= count(a, cons(a, nil), z)
False <= count(a, cons(b, nil), s(z))
False <= count(b, cons(a, cons(a, nil)), s(z)) /\ count(b, cons(b, cons(a, cons(a, nil))), s(z))
False <= count(b, cons(a, nil), s(z))
False <= count(b, cons(b, cons(a, nil)), s(s(z)))
False <= count(b, cons(b, cons(b, cons(b, nil))), s(z)) /\ count(b, cons(b, cons(b, nil)), s(z))
False <= count(b, cons(b, nil), s(s(z)))
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_0)
  _r_1(cons(x_0_0, x_0_1), z) <= _r_5(x_0_0)
  _r_1(nil, z) <= True
  _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_3(x_0_1)
  _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_5(x_0_0)
  _r_2(cons(x_0_0, x_0_1), z) <= _r_3(x_0_1)
  _r_2(cons(x_0_0, x_0_1), z) <= _r_4(x_0_0)
  _r_2(nil, z) <= True
  _r_3(cons(x_0_0, x_0_1)) <= True
  _r_4(b) <= True
  _r_5(a) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_3(x_1_1) /\ _r_4(x_1_0)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_3(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_5(x_1_0)
  count(a, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_0)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_3(x_1_1) /\ _r_5(x_1_0)
  count(b, cons(x_1_0, x_1_1), z) <= _r_5(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> s(s(_cmlh_0))  ;  _jc -> z  ;  l1 -> cons(b, cons(_kllh_0, _kllh_1))  ;  x -> a
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
Yes: {
_cc -> s(s(_aslh_0))  ;  t1 -> cons(a, cons(a, _zrlh_1))  ;  x -> b
}

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
No: ()


-------------------------------------------
Step 13, which took 1.823656 s (model generation: 1.818230,  model checking: 0.005426):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, cons(a, nil)), s(s(z))) <= True
count(a, cons(a, cons(b, cons(a, nil))), s(s(z))) <= True
count(a, cons(a, cons(b, nil)), s(z)) <= True
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True
count(a, cons(b, cons(a, nil)), s(z)) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, cons(a, cons(b, nil))), s(z)) <= True
count(b, cons(a, cons(b, nil)), s(z)) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, cons(a, nil)), s(z)) <= True
count(b, cons(b, cons(b, nil)), s(s(z))) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(a, cons(a, cons(a, nil)), s(z))
False <= count(a, cons(a, cons(b, nil)), s(s(z)))
False <= count(a, cons(a, nil), z)
False <= count(a, cons(b, cons(a, nil)), z)
False <= count(a, cons(b, nil), s(z))
count(b, cons(b, cons(a, cons(a, nil))), s(s(s(z)))) <= count(b, cons(a, cons(a, nil)), s(s(z)))
False <= count(b, cons(a, cons(a, nil)), s(z)) /\ count(b, cons(b, cons(a, cons(a, nil))), s(z))
False <= count(b, cons(a, nil), s(z))
False <= count(b, cons(b, cons(a, nil)), s(s(z)))
False <= count(b, cons(b, cons(b, cons(b, nil))), s(z)) /\ count(b, cons(b, cons(b, nil)), s(z))
False <= count(b, cons(b, nil), s(s(z)))
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1, x_1_0)
  _r_1(cons(x_0_0, x_0_1), z) <= _r_3(x_0_1)
  _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= True
  _r_2(nil, z) <= True
  _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_0)
  _r_3(nil) <= True
  _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0)
  _r_4(nil) <= True
  _r_5(b) <= True
  _r_6(a) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_3(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_5(x_1_0)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_4(x_1_1) /\ _r_6(x_1_0)
  count(a, cons(x_1_0, x_1_1), z) <= _r_3(x_1_1) /\ _r_5(x_1_0)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_1)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_6(x_1_0)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_3(x_1_1) /\ _r_5(x_1_0)
  count(b, cons(x_1_0, x_1_1), z) <= _r_6(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> s(s(z))  ;  _jc -> z  ;  l1 -> cons(a, cons(_szmh_0, nil))  ;  x -> b
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
Yes: {
_cc -> z  ;  t1 -> cons(a, cons(a, _aanh_1))  ;  x -> b
}

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
Yes: {
_dc -> s(z)  ;  h1 -> b  ;  t1 -> cons(b, cons(a, nil))  ;  x -> a
}


-------------------------------------------
Step 14, which took 2.509947 s (model generation: 2.503975,  model checking: 0.005972):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, cons(a, nil)), s(s(z))) <= True
count(a, cons(a, cons(b, cons(a, nil))), s(s(z))) <= True
count(a, cons(a, cons(b, nil)), s(z)) <= True
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True
count(a, cons(b, cons(a, nil)), s(z)) <= True
count(a, cons(b, cons(b, cons(a, nil))), s(z)) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, cons(a, cons(b, nil))), s(z)) <= True
count(b, cons(a, cons(b, nil)), s(z)) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, cons(a, nil)), s(z)) <= True
count(b, cons(b, cons(b, nil)), s(s(z))) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(a, cons(a, cons(a, nil)), s(z))
False <= count(a, cons(a, cons(b, nil)), s(s(z)))
False <= count(a, cons(a, nil), z)
False <= count(a, cons(b, cons(a, nil)), z)
False <= count(a, cons(b, nil), s(z))
count(b, cons(b, cons(a, cons(a, nil))), s(s(s(z)))) <= count(b, cons(a, cons(a, nil)), s(s(z)))
False <= count(b, cons(a, cons(a, nil)), s(z)) /\ count(b, cons(b, cons(a, cons(a, nil))), s(z))
count(b, cons(b, cons(a, cons(a, nil))), s(z)) <= count(b, cons(a, cons(a, nil)), z)
False <= count(b, cons(a, cons(a, nil)), z) /\ count(b, cons(b, cons(a, cons(a, nil))), s(s(z)))
False <= count(b, cons(a, nil), s(z))
False <= count(b, cons(b, cons(a, nil)), s(s(z)))
False <= count(b, cons(b, cons(b, cons(b, nil))), s(z)) /\ count(b, cons(b, cons(b, nil)), s(z))
False <= count(b, cons(b, nil), s(s(z)))
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True
  _r_1(nil, z) <= True
  _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1, x_1_0)
  _r_2(cons(x_0_0, x_0_1), z) <= True
  _r_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0)
  _r_3(nil) <= True
  _r_4(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) /\ _r_5(x_0_0)
  _r_4(nil) <= True
  _r_5(a) <= True
  _r_6(b) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_1) /\ _r_5(x_1_0)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_3(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_6(x_1_0)
  count(a, cons(x_1_0, x_1_1), z) <= _r_3(x_1_1) /\ _r_6(x_1_0)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_3(x_1_1) /\ _r_6(x_1_0)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_4(x_1_1)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_5(x_1_0)
  count(b, cons(x_1_0, x_1_1), z) <= _r_3(x_1_1) /\ _r_5(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> s(z)  ;  _jc -> s(z)  ;  l1 -> cons(a, cons(b, _yuoh_1))  ;  x -> b
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
Yes: {
_cc -> s(z)  ;  t1 -> cons(a, cons(a, _jsoh_1))  ;  x -> b
}

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
Yes: {
_dc -> z  ;  h1 -> a  ;  t1 -> cons(a, nil)  ;  x -> b
}


-------------------------------------------
Step 15, which took 18.691896 s (model generation: 18.685573,  model checking: 0.006323):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, cons(a, nil)), s(s(z))) <= True
count(a, cons(a, cons(b, cons(a, nil))), s(s(z))) <= True
count(a, cons(a, cons(b, nil)), s(z)) <= True
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True
count(a, cons(b, cons(a, nil)), s(z)) <= True
count(a, cons(b, cons(b, cons(a, nil))), s(z)) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, cons(a, cons(b, nil))), s(z)) <= True
count(b, cons(a, cons(a, nil)), z) <= True
count(b, cons(a, cons(b, nil)), s(z)) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, cons(a, cons(a, nil))), s(z)) <= True
count(b, cons(b, cons(a, nil)), s(z)) <= True
count(b, cons(b, cons(b, nil)), s(s(z))) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(a, cons(a, cons(a, nil)), s(z))
False <= count(a, cons(a, cons(b, nil)), s(s(z)))
False <= count(a, cons(a, nil), z)
False <= count(a, cons(b, cons(a, nil)), z)
False <= count(a, cons(b, nil), s(z))
count(b, cons(b, cons(a, cons(a, nil))), s(s(s(z)))) <= count(b, cons(a, cons(a, nil)), s(s(z)))
False <= count(b, cons(a, cons(a, nil)), s(z))
False <= count(b, cons(a, nil), s(z))
False <= count(b, cons(b, cons(a, cons(a, nil))), s(s(z)))
False <= count(b, cons(b, cons(a, cons(b, nil))), s(z))
False <= count(b, cons(b, cons(a, nil)), s(s(z)))
False <= count(b, cons(b, cons(b, cons(b, nil))), s(z)) /\ count(b, cons(b, cons(b, nil)), s(z))
False <= count(b, cons(b, nil), s(s(z)))
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(a, s(x_1_0)) <= True
  _r_1(b, z) <= True
  _r_2(a, z) <= True
  _r_2(b, s(x_1_0)) <= True
  _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1)
  _r_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0)
  _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1)
  _r_4(cons(x_0_0, x_0_1)) <= _r_5(x_0_1) /\ _r_7(x_0_0)
  _r_5(nil) <= True
  _r_6(b) <= True
  _r_7(a) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_4(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_3(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_5(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_6(x_1_0)
  count(a, cons(x_1_0, x_1_1), z) <= _r_5(x_1_1) /\ _r_6(x_1_0)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_4(x_1_1) /\ _r_6(x_1_0)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_5(x_1_1)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_3(x_1_1)
  count(b, cons(x_1_0, x_1_1), z) <= _r_7(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> s(s(_fmqh_0))  ;  _jc -> z  ;  l1 -> cons(a, cons(b, _hlqh_1))  ;  x -> b
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
Yes: {
_cc -> z  ;  t1 -> cons(a, cons(b, nil))  ;  x -> b
}

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
Yes: {
_dc -> z  ;  h1 -> b  ;  t1 -> cons(b, nil)  ;  x -> a
}


-------------------------------------------
Step 16, which took 13.566181 s (model generation: 13.555318,  model checking: 0.010863):

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, cons(a, nil)), s(s(z))) <= True
count(a, cons(a, cons(b, cons(a, nil))), s(s(z))) <= True
count(a, cons(a, cons(b, nil)), s(z)) <= True
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True
count(a, cons(b, cons(a, nil)), s(z)) <= True
count(a, cons(b, cons(b, cons(a, nil))), s(z)) <= True
count(a, cons(b, cons(b, nil)), z) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, cons(a, cons(b, nil))), s(z)) <= True
count(b, cons(a, cons(a, nil)), z) <= True
count(b, cons(a, cons(b, nil)), s(z)) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, cons(a, cons(a, nil))), s(z)) <= True
count(b, cons(b, cons(a, nil)), s(z)) <= True
count(b, cons(b, cons(b, nil)), s(s(z))) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(a, cons(a, cons(a, nil)), s(z))
False <= count(a, cons(a, cons(b, nil)), s(s(z)))
False <= count(a, cons(a, nil), z)
False <= count(a, cons(b, cons(a, nil)), z)
False <= count(a, cons(b, nil), s(z))
count(b, cons(b, cons(a, cons(a, nil))), s(s(s(z)))) <= count(b, cons(a, cons(a, nil)), s(s(z)))
False <= count(b, cons(a, cons(a, nil)), s(z))
False <= count(b, cons(a, cons(b, nil)), z)
False <= count(b, cons(a, nil), s(z))
False <= count(b, cons(b, cons(a, cons(a, nil))), s(s(z)))
False <= count(b, cons(b, cons(a, cons(b, nil))), s(z))
False <= count(b, cons(b, cons(a, nil)), s(s(z)))
False <= count(b, cons(b, cons(b, cons(b, nil))), s(z)) /\ count(b, cons(b, cons(b, nil)), s(z))
False <= count(b, cons(b, nil), s(s(z)))
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(a, z) <= True
  _r_1(b, s(x_1_0)) <= True
  _r_2(a, s(x_1_0)) <= True
  _r_2(b, z) <= True
  _r_3(nil) <= True
  _r_4(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) /\ _r_7(x_0_0)
  _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1)
  _r_5(cons(x_0_0, x_0_1)) <= _r_5(x_0_1)
  _r_5(cons(x_0_0, x_0_1)) <= _r_6(x_0_0)
  _r_6(b) <= True
  _r_7(a) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_5(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_6(x_1_0)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_4(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) /\ _r_7(x_1_0)
  count(a, cons(x_1_0, x_1_1), z) <= _r_3(x_1_1) /\ _r_6(x_1_0)
  count(a, cons(x_1_0, x_1_1), z) <= _r_5(x_1_1)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_5(x_1_1)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_3(x_1_1)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_4(x_1_1) /\ _r_6(x_1_0)
  count(b, cons(x_1_0, x_1_1), z) <= _r_3(x_1_1) /\ _r_7(x_1_0)
  count(b, cons(x_1_0, x_1_1), z) <= _r_4(x_1_1)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

count(x, nil, z) <= True  :
No: ()

eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic)  :
Yes: {
_ic -> s(s(_wksh_0))  ;  _jc -> z  ;  l1 -> nil  ;  x -> a
}

count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc)  :
Yes: {
_cc -> s(s(_qtsh_0))  ;  t1 -> cons(a, nil)  ;  x -> b
}

eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc)  :
Yes: {
_dc -> s(s(_dnsh_0))  ;  h1 -> a  ;  t1 -> cons(b, cons(b, _fnsh_1))  ;  x -> b
}


Total time: 60.058692
Learner time: 37.912076
Teacher time: 0.045084
Reasons for stopping: Maybe:  timeout during teacher: {
count(x, nil, z) <= True -> out of time
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> out of time
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> out of time
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> out of time
}Last solver state:

Clauses:
{
count(x, nil, z) <= True -> 0
eq_nat(_ic, s(_jc)) <= count(x, l1, _jc) /\ count(x, cons(x, l1), _ic) -> 0
count(x, cons(x, t1), s(_cc)) <= count(x, t1, _cc) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _dc) <= count(x, t1, _dc) -> 0
}

Accumulated learning constraints:
{
count(a, cons(a, cons(a, nil)), s(s(z))) <= True
count(a, cons(a, cons(b, cons(a, nil))), s(s(z))) <= True
count(a, cons(a, cons(b, nil)), s(z)) <= True
count(a, cons(a, nil), s(z)) <= True
count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True
count(a, cons(b, cons(a, nil)), s(z)) <= True
count(a, cons(b, cons(b, cons(a, nil))), s(z)) <= True
count(a, cons(b, cons(b, nil)), z) <= True
count(a, cons(b, nil), z) <= True
count(a, nil, z) <= True
count(b, cons(a, cons(a, cons(b, nil))), s(z)) <= True
count(b, cons(a, cons(a, nil)), z) <= True
count(b, cons(a, cons(b, cons(b, nil))), s(s(z))) <= True
count(b, cons(a, cons(b, nil)), s(z)) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, cons(a, cons(a, nil))), s(z)) <= True
count(b, cons(b, cons(a, nil)), s(z)) <= True
count(b, cons(b, cons(b, nil)), s(s(z))) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
False <= count(a, cons(a, cons(a, nil)), s(z))
False <= count(a, cons(a, cons(b, nil)), s(s(z)))
False <= count(a, cons(a, nil), s(s(z)))
False <= count(a, cons(a, nil), z)
False <= count(a, cons(b, cons(a, nil)), z)
False <= count(a, cons(b, nil), s(z))
count(b, cons(b, cons(a, cons(a, nil))), s(s(s(z)))) <= count(b, cons(a, cons(a, nil)), s(s(z)))
False <= count(b, cons(a, cons(a, nil)), s(z))
False <= count(b, cons(a, cons(b, nil)), z)
count(b, cons(b, cons(a, nil)), s(s(s(z)))) <= count(b, cons(a, nil), s(s(z)))
False <= count(b, cons(a, nil), s(z))
False <= count(b, cons(b, cons(a, cons(a, nil))), s(s(z)))
False <= count(b, cons(b, cons(a, cons(b, nil))), s(z))
False <= count(b, cons(b, cons(a, nil)), s(s(z)))
False <= count(b, cons(b, cons(b, cons(b, nil))), s(z)) /\ count(b, cons(b, cons(b, nil)), s(z))
False <= count(b, cons(b, nil), s(s(z)))
False <= count(b, cons(b, nil), z)
}

Current best model:
|_
name: None

count ->
[
count : <elt * eltlist * nat>
{
  _r_1(a, s(x_1_0)) <= True
  _r_1(b, z) <= True
  _r_2(a, z) <= True
  _r_2(b, s(x_1_0)) <= True
  _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1)
  _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_1) /\ _r_6(x_0_0)
  _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1)
  _r_4(cons(x_0_0, x_0_1)) <= _r_7(x_0_0)
  _r_5(nil) <= True
  _r_6(a) <= True
  _r_7(b) <= True
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_3(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_4(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_5(x_1_1)
  count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_7(x_1_0)
  count(a, cons(x_1_0, x_1_1), z) <= _r_4(x_1_1)
  count(a, cons(x_1_0, x_1_1), z) <= _r_5(x_1_1) /\ _r_7(x_1_0)
  count(a, nil, z) <= True
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_3(x_1_1) /\ _r_7(x_1_0)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_5(x_1_1) /\ _r_7(x_1_0)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_4(x_1_1)
  count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) /\ _r_6(x_1_0)
  count(b, cons(x_1_0, x_1_1), z) <= _r_3(x_1_1)
  count(b, cons(x_1_0, x_1_1), z) <= _r_5(x_1_1) /\ _r_6(x_1_0)
  count(b, nil, z) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|