Solving ../../benchmarks/smtlib/true/mem_implies_positive_count.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: {
elist -> {econs, enil}  ;  elt -> {a, b}  ;  nat -> {s, z}
}
definition:
{
(mem_elt, P:
{
mem_elt(h, econs(h, t)) <= True
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))
False <= mem_elt(e, enil)
}
)
(count_elt, F:
{
count_elt(x, enil, z) <= True
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)
}
eq_nat(_axa, _bxa) <= count_elt(_ywa, _zwa, _axa) /\ count_elt(_ywa, _zwa, _bxa)
)
}

properties:
{
False <= count_elt(e, l, z) /\ mem_elt(e, l)
}


over-approximation: {count_elt, mem_elt}
under-approximation: {}

Clause system for inference is:

{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}


Solving took 1.671025 seconds.
Yes: |_
name: None

count_elt ->
[
count_elt : <elt * elist * nat>
{
  _r_1(a) <= True
  _r_2(b) <= True
  _r_3(econs(x_0_0, x_0_1)) <= _r_1(x_0_0) /\ _r_3(x_0_1)
  _r_3(enil) <= True
  _r_5(econs(x_0_0, x_0_1)) <= _r_2(x_0_0) /\ _r_5(x_0_1)
  _r_5(enil) <= True
  count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(a, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) /\ _r_5(x_1_1)
  count_elt(a, enil, z) <= True
  count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(b, econs(x_1_0, x_1_1), z) <= _r_1(x_1_0) /\ _r_3(x_1_1)
  count_elt(b, enil, z) <= True
}
]


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  _r_1(a) <= True
  _r_2(b) <= True
  _r_4(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_4(econs(x_0_0, x_0_1)) <= _r_4(x_0_1)
  _r_6(econs(x_0_0, x_0_1)) <= _r_2(x_0_0)
  _r_6(econs(x_0_0, x_0_1)) <= _r_6(x_0_1)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_1(x_1_0)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_4(x_1_1)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_2(x_1_0)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_6(x_1_1)
}
]



--
Equality automata are defined for: {elist, elt, nat}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005504 s (model generation: 0.005457,  model checking: 0.000047):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

count_elt ->
[
count_elt : <elt * elist * nat>
{
  
}
]


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
Yes: {
x -> b
}

mem_elt(h, econs(h, t)) <= True  :
Yes: {
h -> b
}

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
No: ()

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
No: ()

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
No: ()


-------------------------------------------
Step 1, which took 0.006257 s (model generation: 0.006189,  model checking: 0.000068):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{
count_elt(b, enil, z) <= True
mem_elt(b, econs(b, enil)) <= True
}

Current best model:
|_
name: None

count_elt ->
[
count_elt : <elt * elist * nat>
{
  count_elt(b, enil, z) <= True
}
]


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  mem_elt(b, econs(x_1_0, x_1_1)) <= True
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
Yes: {
x -> a
}

mem_elt(h, econs(h, t)) <= True  :
Yes: {
h -> a
}

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
No: ()

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
Yes: {
_wwa -> z  ;  t1 -> enil  ;  x -> b
}

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
Yes: {
_xwa -> z  ;  h1 -> a  ;  t1 -> enil  ;  x -> b
}

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
Yes: {
e -> b  ;  h -> a  ;  t -> enil
}


-------------------------------------------
Step 2, which took 0.015415 s (model generation: 0.015209,  model checking: 0.000206):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{
count_elt(a, enil, z) <= True
count_elt(b, econs(a, enil), z) <= True
count_elt(b, econs(b, enil), s(z)) <= True
count_elt(b, enil, z) <= True
mem_elt(a, econs(a, enil)) <= True
mem_elt(b, econs(b, enil)) <= True
mem_elt(b, enil) <= mem_elt(b, econs(a, enil))
}

Current best model:
|_
name: None

count_elt ->
[
count_elt : <elt * elist * nat>
{
  count_elt(a, enil, z) <= True
  count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(b, econs(x_1_0, x_1_1), z) <= True
  count_elt(b, enil, z) <= True
}
]


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  mem_elt(a, econs(x_1_0, x_1_1)) <= True
  mem_elt(b, econs(x_1_0, x_1_1)) <= True
  mem_elt(b, enil) <= True
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
No: ()

mem_elt(h, econs(h, t)) <= True  :
No: ()

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
Yes: {
e -> b  ;  l -> enil
}

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
Yes: {
_wwa -> z  ;  t1 -> enil  ;  x -> a
}

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
Yes: {
_xwa -> z  ;  h1 -> b  ;  t1 -> enil  ;  x -> a
}

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
Yes: {
e -> a  ;  h -> b  ;  t -> enil
}


-------------------------------------------
Step 3, which took 0.013800 s (model generation: 0.013659,  model checking: 0.000141):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{
count_elt(a, econs(a, enil), s(z)) <= True
count_elt(a, econs(b, enil), z) <= True
count_elt(a, enil, z) <= True
count_elt(b, econs(a, enil), z) <= True
count_elt(b, econs(b, enil), s(z)) <= True
count_elt(b, enil, z) <= True
mem_elt(a, econs(a, enil)) <= True
mem_elt(b, econs(b, enil)) <= True
mem_elt(a, enil) <= mem_elt(a, econs(b, enil))
False <= mem_elt(b, econs(a, enil))
False <= mem_elt(b, enil)
}

Current best model:
|_
name: None

count_elt ->
[
count_elt : <elt * elist * nat>
{
  count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(a, econs(x_1_0, x_1_1), z) <= True
  count_elt(a, enil, z) <= True
  count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(b, econs(x_1_0, x_1_1), z) <= True
  count_elt(b, enil, z) <= True
}
]


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  _r_1(b) <= True
  mem_elt(a, econs(x_1_0, x_1_1)) <= True
  mem_elt(a, enil) <= True
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_1(x_1_0)
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
No: ()

mem_elt(h, econs(h, t)) <= True  :
No: ()

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
Yes: {
e -> a  ;  l -> enil
}

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
No: ()

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
Yes: {
e -> b  ;  h -> a  ;  t -> econs(b, _navs_1)
}

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
No: ()


-------------------------------------------
Step 4, which took 0.023942 s (model generation: 0.023707,  model checking: 0.000235):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{
count_elt(a, econs(a, enil), s(z)) <= True
count_elt(a, econs(b, enil), z) <= True
count_elt(a, enil, z) <= True
count_elt(b, econs(a, enil), z) <= True
count_elt(b, econs(b, enil), s(z)) <= True
count_elt(b, enil, z) <= True
mem_elt(a, econs(a, enil)) <= True
mem_elt(b, econs(a, econs(b, enil))) <= True
mem_elt(b, econs(b, enil)) <= True
False <= mem_elt(a, econs(b, enil))
False <= mem_elt(a, enil)
False <= mem_elt(b, econs(a, enil))
False <= mem_elt(b, enil)
}

Current best model:
|_
name: None

count_elt ->
[
count_elt : <elt * elist * nat>
{
  count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(a, econs(x_1_0, x_1_1), z) <= True
  count_elt(a, enil, z) <= True
  count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(b, econs(x_1_0, x_1_1), z) <= True
  count_elt(b, enil, z) <= True
}
]


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  _r_1(b) <= True
  _r_2(a) <= True
  _r_3(econs(x_0_0, x_0_1)) <= True
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_2(x_1_0)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_1(x_1_0)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_3(x_1_1)
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
No: ()

mem_elt(h, econs(h, t)) <= True  :
No: ()

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
Yes: {
e -> b  ;  l -> econs(b, _bbvs_1)
}

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
No: ()

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
Yes: {
e -> a  ;  h -> b  ;  t -> econs(a, _gbvs_1)
}

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
Yes: {
e -> b  ;  h -> a  ;  t -> econs(a, enil)
}


-------------------------------------------
Step 5, which took 0.038325 s (model generation: 0.037843,  model checking: 0.000482):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{
count_elt(a, econs(a, enil), s(z)) <= True
count_elt(a, econs(b, enil), z) <= True
count_elt(a, enil, z) <= True
count_elt(b, econs(a, enil), z) <= True
count_elt(b, econs(b, enil), s(z)) <= True
count_elt(b, enil, z) <= True
mem_elt(a, econs(a, enil)) <= True
mem_elt(a, econs(b, econs(a, enil))) <= True
mem_elt(b, econs(a, econs(b, enil))) <= True
mem_elt(b, econs(b, enil)) <= True
False <= count_elt(b, econs(b, enil), z)
False <= mem_elt(a, econs(b, enil))
False <= mem_elt(a, enil)
False <= mem_elt(b, econs(a, econs(a, enil)))
False <= mem_elt(b, econs(a, enil))
False <= mem_elt(b, enil)
}

Current best model:
|_
name: None

count_elt ->
[
count_elt : <elt * elist * nat>
{
  _r_2(a) <= True
  count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(a, econs(x_1_0, x_1_1), z) <= True
  count_elt(a, enil, z) <= True
  count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(b, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0)
  count_elt(b, enil, z) <= True
}
]


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  _r_1(b) <= True
  _r_2(a) <= True
  _r_3(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_4(econs(x_0_0, x_0_1)) <= True
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_2(x_1_0)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_4(x_1_1)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_1(x_1_0)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_3(x_1_1)
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
No: ()

mem_elt(h, econs(h, t)) <= True  :
No: ()

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
Yes: {
e -> a  ;  l -> econs(a, _pcvs_1)
}

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
No: ()

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
Yes: {
e -> b  ;  h -> a  ;  t -> econs(a, econs(b, _sevs_1))
}

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
Yes: {
e -> a  ;  h -> b  ;  t -> econs(b, enil)
}


-------------------------------------------
Step 6, which took 0.047711 s (model generation: 0.047090,  model checking: 0.000621):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{
count_elt(a, econs(a, enil), s(z)) <= True
count_elt(a, econs(b, enil), z) <= True
count_elt(a, enil, z) <= True
count_elt(b, econs(a, enil), z) <= True
count_elt(b, econs(b, enil), s(z)) <= True
count_elt(b, enil, z) <= True
mem_elt(a, econs(a, enil)) <= True
mem_elt(a, econs(b, econs(a, enil))) <= True
mem_elt(b, econs(a, econs(a, econs(b, enil)))) <= True
mem_elt(b, econs(a, econs(b, enil))) <= True
mem_elt(b, econs(b, enil)) <= True
False <= count_elt(a, econs(a, enil), z)
False <= count_elt(b, econs(b, enil), z)
False <= mem_elt(a, econs(b, econs(b, enil)))
False <= mem_elt(a, econs(b, enil))
False <= mem_elt(a, enil)
False <= mem_elt(b, econs(a, econs(a, enil)))
False <= mem_elt(b, econs(a, enil))
False <= mem_elt(b, enil)
}

Current best model:
|_
name: None

count_elt ->
[
count_elt : <elt * elist * nat>
{
  _r_1(b) <= True
  _r_2(a) <= True
  count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(a, econs(x_1_0, x_1_1), z) <= _r_1(x_1_0)
  count_elt(a, enil, z) <= True
  count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(b, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0)
  count_elt(b, enil, z) <= True
}
]


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  _r_1(b) <= True
  _r_2(a) <= True
  _r_3(econs(x_0_0, x_0_1)) <= _r_2(x_0_0)
  _r_4(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_4(econs(x_0_0, x_0_1)) <= _r_4(x_0_1)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_2(x_1_0)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_3(x_1_1)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_1(x_1_0)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_4(x_1_1)
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
No: ()

mem_elt(h, econs(h, t)) <= True  :
No: ()

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
Yes: {
e -> b  ;  l -> econs(a, econs(b, _qhvs_1))
}

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
No: ()

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
Yes: {
e -> a  ;  h -> b  ;  t -> econs(b, econs(a, _shvs_1))
}

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
No: ()


-------------------------------------------
Step 7, which took 0.085357 s (model generation: 0.084669,  model checking: 0.000688):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{
count_elt(a, econs(a, enil), s(z)) <= True
count_elt(a, econs(b, enil), z) <= True
count_elt(a, enil, z) <= True
count_elt(b, econs(a, enil), z) <= True
count_elt(b, econs(b, enil), s(z)) <= True
count_elt(b, enil, z) <= True
mem_elt(a, econs(a, enil)) <= True
mem_elt(a, econs(b, econs(a, enil))) <= True
mem_elt(a, econs(b, econs(b, econs(a, enil)))) <= True
mem_elt(b, econs(a, econs(a, econs(b, enil)))) <= True
mem_elt(b, econs(a, econs(b, enil))) <= True
mem_elt(b, econs(b, enil)) <= True
False <= count_elt(a, econs(a, enil), z)
False <= count_elt(b, econs(a, econs(b, enil)), z)
False <= count_elt(b, econs(b, enil), z)
False <= mem_elt(a, econs(b, econs(b, enil)))
False <= mem_elt(a, econs(b, enil))
False <= mem_elt(a, enil)
False <= mem_elt(b, econs(a, econs(a, enil)))
False <= mem_elt(b, econs(a, enil))
False <= mem_elt(b, enil)
}

Current best model:
|_
name: None

count_elt ->
[
count_elt : <elt * elist * nat>
{
  _r_1(b) <= True
  _r_2(a) <= True
  _r_3(enil) <= True
  count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(a, econs(x_1_0, x_1_1), z) <= _r_1(x_1_0)
  count_elt(a, enil, z) <= True
  count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(b, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) /\ _r_3(x_1_1)
  count_elt(b, enil, z) <= True
}
]


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  _r_1(b) <= True
  _r_2(a) <= True
  _r_4(econs(x_0_0, x_0_1)) <= _r_2(x_0_0)
  _r_4(econs(x_0_0, x_0_1)) <= _r_4(x_0_1)
  _r_5(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_5(econs(x_0_0, x_0_1)) <= _r_5(x_0_1)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_2(x_1_0)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_4(x_1_1)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_1(x_1_0)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_5(x_1_1)
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
No: ()

mem_elt(h, econs(h, t)) <= True  :
No: ()

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
Yes: {
e -> a  ;  l -> econs(b, econs(a, _olvs_1))
}

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
No: ()

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
Yes: {
_xwa -> z  ;  h1 -> a  ;  t1 -> econs(a, enil)  ;  x -> b
}

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
No: ()


-------------------------------------------
Step 8, which took 0.089918 s (model generation: 0.089121,  model checking: 0.000797):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{
count_elt(a, econs(a, enil), s(z)) <= True
count_elt(a, econs(b, enil), z) <= True
count_elt(a, enil, z) <= True
count_elt(b, econs(a, econs(a, enil)), z) <= True
count_elt(b, econs(a, enil), z) <= True
count_elt(b, econs(b, enil), s(z)) <= True
count_elt(b, enil, z) <= True
mem_elt(a, econs(a, enil)) <= True
mem_elt(a, econs(b, econs(a, enil))) <= True
mem_elt(a, econs(b, econs(b, econs(a, enil)))) <= True
mem_elt(b, econs(a, econs(a, econs(b, enil)))) <= True
mem_elt(b, econs(a, econs(b, enil))) <= True
mem_elt(b, econs(b, enil)) <= True
False <= count_elt(a, econs(a, enil), z)
False <= count_elt(a, econs(b, econs(a, enil)), z)
False <= count_elt(b, econs(a, econs(b, enil)), z)
False <= count_elt(b, econs(b, enil), z)
False <= mem_elt(a, econs(b, econs(b, enil)))
False <= mem_elt(a, econs(b, enil))
False <= mem_elt(a, enil)
False <= mem_elt(b, econs(a, econs(a, enil)))
False <= mem_elt(b, econs(a, enil))
False <= mem_elt(b, enil)
}

Current best model:
|_
name: None

count_elt ->
[
count_elt : <elt * elist * nat>
{
  _r_1(a) <= True
  _r_2(b) <= True
  _r_3(enil) <= True
  _r_5(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_5(econs(x_0_0, x_0_1)) <= _r_5(x_0_1)
  count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(a, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) /\ _r_3(x_1_1)
  count_elt(a, enil, z) <= True
  count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(b, econs(x_1_0, x_1_1), z) <= _r_1(x_1_0) /\ _r_3(x_1_1)
  count_elt(b, econs(x_1_0, x_1_1), z) <= _r_5(x_1_1)
  count_elt(b, enil, z) <= True
}
]


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  _r_1(a) <= True
  _r_2(b) <= True
  _r_4(econs(x_0_0, x_0_1)) <= _r_2(x_0_0)
  _r_4(econs(x_0_0, x_0_1)) <= _r_4(x_0_1)
  _r_5(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_5(econs(x_0_0, x_0_1)) <= _r_5(x_0_1)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_1(x_1_0)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_5(x_1_1)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_2(x_1_0)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_4(x_1_1)
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
No: ()

mem_elt(h, econs(h, t)) <= True  :
No: ()

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
Yes: {
e -> b  ;  l -> econs(b, econs(a, _mqvs_1))
}

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
No: ()

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
Yes: {
_xwa -> z  ;  h1 -> b  ;  t1 -> econs(b, enil)  ;  x -> a
}

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
No: ()


-------------------------------------------
Step 9, which took 0.102609 s (model generation: 0.101320,  model checking: 0.001289):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{
count_elt(a, econs(a, enil), s(z)) <= True
count_elt(a, econs(b, econs(b, enil)), z) <= True
count_elt(a, econs(b, enil), z) <= True
count_elt(a, enil, z) <= True
count_elt(b, econs(a, econs(a, enil)), z) <= True
count_elt(b, econs(a, enil), z) <= True
count_elt(b, econs(b, enil), s(z)) <= True
count_elt(b, enil, z) <= True
mem_elt(a, econs(a, enil)) <= True
mem_elt(a, econs(b, econs(a, enil))) <= True
mem_elt(a, econs(b, econs(b, econs(a, enil)))) <= True
mem_elt(b, econs(a, econs(a, econs(b, enil)))) <= True
mem_elt(b, econs(a, econs(b, enil))) <= True
mem_elt(b, econs(b, enil)) <= True
False <= count_elt(a, econs(a, enil), z)
False <= count_elt(a, econs(b, econs(a, enil)), z)
False <= count_elt(b, econs(a, econs(b, enil)), z)
False <= count_elt(b, econs(b, econs(a, enil)), z) /\ mem_elt(b, econs(b, econs(a, enil)))
False <= count_elt(b, econs(b, enil), z)
False <= mem_elt(a, econs(b, econs(b, enil)))
False <= mem_elt(a, econs(b, enil))
False <= mem_elt(a, enil)
False <= mem_elt(b, econs(a, econs(a, enil)))
False <= mem_elt(b, econs(a, enil))
False <= mem_elt(b, enil)
}

Current best model:
|_
name: None

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


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  _r_1(a) <= True
  _r_2(b) <= True
  _r_4(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_4(econs(x_0_0, x_0_1)) <= _r_4(x_0_1)
  _r_5(econs(x_0_0, x_0_1)) <= _r_2(x_0_0)
  _r_5(econs(x_0_0, x_0_1)) <= _r_5(x_0_1)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_1(x_1_0)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_4(x_1_1)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_2(x_1_0)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_5(x_1_1)
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
No: ()

mem_elt(h, econs(h, t)) <= True  :
No: ()

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
Yes: {
e -> a  ;  l -> econs(a, econs(b, _dxvs_1))
}

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
No: ()

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
No: ()


-------------------------------------------
Step 10, which took 0.098632 s (model generation: 0.097142,  model checking: 0.001490):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{
count_elt(a, econs(a, enil), s(z)) <= True
count_elt(a, econs(b, econs(b, enil)), z) <= True
count_elt(a, econs(b, enil), z) <= True
count_elt(a, enil, z) <= True
count_elt(b, econs(a, econs(a, enil)), z) <= True
count_elt(b, econs(a, enil), z) <= True
count_elt(b, econs(b, enil), s(z)) <= True
count_elt(b, enil, z) <= True
mem_elt(a, econs(a, enil)) <= True
mem_elt(a, econs(b, econs(a, enil))) <= True
mem_elt(a, econs(b, econs(b, econs(a, enil)))) <= True
mem_elt(b, econs(a, econs(a, econs(b, enil)))) <= True
mem_elt(b, econs(a, econs(b, enil))) <= True
mem_elt(b, econs(b, enil)) <= True
False <= count_elt(a, econs(a, econs(b, enil)), z) /\ mem_elt(a, econs(a, econs(b, enil)))
False <= count_elt(a, econs(a, enil), z)
False <= count_elt(a, econs(b, econs(a, enil)), z)
False <= count_elt(b, econs(a, econs(b, enil)), z)
False <= count_elt(b, econs(b, econs(a, enil)), z) /\ mem_elt(b, econs(b, econs(a, enil)))
False <= count_elt(b, econs(b, enil), z)
False <= mem_elt(a, econs(b, econs(b, enil)))
False <= mem_elt(a, econs(b, enil))
False <= mem_elt(a, enil)
False <= mem_elt(b, econs(a, econs(a, enil)))
False <= mem_elt(b, econs(a, enil))
False <= mem_elt(b, enil)
}

Current best model:
|_
name: None

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


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  _r_1(a) <= True
  _r_2(b) <= True
  _r_3(econs(x_0_0, x_0_1)) <= _r_2(x_0_0)
  _r_3(econs(x_0_0, x_0_1)) <= _r_3(x_0_1)
  _r_5(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_5(econs(x_0_0, x_0_1)) <= _r_5(x_0_1)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_1(x_1_0)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_5(x_1_1)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_2(x_1_0)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_3(x_1_1)
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
No: ()

mem_elt(h, econs(h, t)) <= True  :
No: ()

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
Yes: {
e -> a  ;  l -> econs(b, econs(a, econs(b, _efws_1)))
}

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
No: ()

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
No: ()


-------------------------------------------
Step 11, which took 0.101871 s (model generation: 0.099869,  model checking: 0.002002):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{
count_elt(a, econs(a, enil), s(z)) <= True
count_elt(a, econs(b, econs(b, enil)), z) <= True
count_elt(a, econs(b, enil), z) <= True
count_elt(a, enil, z) <= True
count_elt(b, econs(a, econs(a, enil)), z) <= True
count_elt(b, econs(a, enil), z) <= True
count_elt(b, econs(b, enil), s(z)) <= True
count_elt(b, enil, z) <= True
mem_elt(a, econs(a, enil)) <= True
mem_elt(a, econs(b, econs(a, enil))) <= True
mem_elt(a, econs(b, econs(b, econs(a, enil)))) <= True
mem_elt(b, econs(a, econs(a, econs(b, enil)))) <= True
mem_elt(b, econs(a, econs(b, enil))) <= True
mem_elt(b, econs(b, enil)) <= True
False <= count_elt(a, econs(a, econs(b, enil)), z) /\ mem_elt(a, econs(a, econs(b, enil)))
False <= count_elt(a, econs(a, enil), z)
False <= count_elt(a, econs(b, econs(a, econs(b, enil))), z) /\ mem_elt(a, econs(b, econs(a, econs(b, enil))))
False <= count_elt(a, econs(b, econs(a, enil)), z)
False <= count_elt(b, econs(a, econs(b, enil)), z)
False <= count_elt(b, econs(b, econs(a, enil)), z) /\ mem_elt(b, econs(b, econs(a, enil)))
False <= count_elt(b, econs(b, enil), z)
False <= mem_elt(a, econs(b, econs(b, enil)))
False <= mem_elt(a, econs(b, enil))
False <= mem_elt(a, enil)
False <= mem_elt(b, econs(a, econs(a, enil)))
False <= mem_elt(b, econs(a, enil))
False <= mem_elt(b, enil)
}

Current best model:
|_
name: None

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


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  _r_1(b) <= True
  _r_2(a) <= True
  _r_3(enil) <= True
  _r_4(econs(x_0_0, x_0_1)) <= _r_2(x_0_0) /\ _r_3(x_0_1)
  _r_4(econs(x_0_0, x_0_1)) <= _r_4(x_0_1)
  _r_5(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_5(econs(x_0_0, x_0_1)) <= _r_5(x_0_1)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_2(x_1_0)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_4(x_1_1)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_1(x_1_0)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_5(x_1_1)
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
No: ()

mem_elt(h, econs(h, t)) <= True  :
No: ()

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
Yes: {
e -> b  ;  l -> econs(a, econs(b, econs(a, enil)))
}

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
No: ()

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
Yes: {
e -> a  ;  h -> b  ;  t -> econs(a, econs(b, enil))
}

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
No: ()


-------------------------------------------
Step 12, which took 0.111032 s (model generation: 0.108903,  model checking: 0.002129):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{
count_elt(a, econs(a, enil), s(z)) <= True
count_elt(a, econs(b, econs(b, enil)), z) <= True
count_elt(a, econs(b, enil), z) <= True
count_elt(a, enil, z) <= True
count_elt(b, econs(a, econs(a, enil)), z) <= True
count_elt(b, econs(a, enil), z) <= True
count_elt(b, econs(b, enil), s(z)) <= True
count_elt(b, enil, z) <= True
mem_elt(a, econs(a, enil)) <= True
mem_elt(a, econs(b, econs(a, enil))) <= True
mem_elt(a, econs(b, econs(b, econs(a, enil)))) <= True
mem_elt(b, econs(a, econs(a, econs(b, enil)))) <= True
mem_elt(b, econs(a, econs(b, enil))) <= True
mem_elt(b, econs(b, enil)) <= True
False <= count_elt(a, econs(a, econs(b, enil)), z) /\ mem_elt(a, econs(a, econs(b, enil)))
False <= count_elt(a, econs(a, enil), z)
False <= count_elt(a, econs(b, econs(a, econs(b, enil))), z) /\ mem_elt(a, econs(b, econs(a, econs(b, enil))))
False <= count_elt(a, econs(b, econs(a, enil)), z)
False <= count_elt(b, econs(a, econs(b, econs(a, enil))), z) /\ mem_elt(b, econs(a, econs(b, econs(a, enil))))
False <= count_elt(b, econs(a, econs(b, enil)), z)
False <= count_elt(b, econs(b, econs(a, enil)), z) /\ mem_elt(b, econs(b, econs(a, enil)))
False <= count_elt(b, econs(b, enil), z)
mem_elt(a, econs(b, econs(a, econs(b, enil)))) <= mem_elt(a, econs(a, econs(b, enil)))
False <= mem_elt(a, econs(b, econs(b, enil)))
False <= mem_elt(a, econs(b, enil))
False <= mem_elt(a, enil)
False <= mem_elt(b, econs(a, econs(a, enil)))
False <= mem_elt(b, econs(a, enil))
False <= mem_elt(b, enil)
}

Current best model:
|_
name: None

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


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  _r_1(b) <= True
  _r_2(a) <= True
  _r_3(econs(x_0_0, x_0_1)) <= _r_1(x_0_0) /\ _r_4(x_0_1)
  _r_3(econs(x_0_0, x_0_1)) <= _r_3(x_0_1)
  _r_4(enil) <= True
  _r_5(econs(x_0_0, x_0_1)) <= _r_2(x_0_0) /\ _r_4(x_0_1)
  _r_5(econs(x_0_0, x_0_1)) <= _r_5(x_0_1)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_2(x_1_0) /\ _r_4(x_1_1)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_5(x_1_1)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_1(x_1_0) /\ _r_4(x_1_1)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_3(x_1_1)
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
No: ()

mem_elt(h, econs(h, t)) <= True  :
Yes: {
h -> a  ;  t -> econs(b, enil)
}

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
No: ()

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
No: ()

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
No: ()


-------------------------------------------
Step 13, which took 0.250458 s (model generation: 0.249694,  model checking: 0.000764):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{
count_elt(a, econs(a, enil), s(z)) <= True
count_elt(a, econs(b, econs(b, enil)), z) <= True
count_elt(a, econs(b, enil), z) <= True
count_elt(a, enil, z) <= True
count_elt(b, econs(a, econs(a, enil)), z) <= True
count_elt(b, econs(a, enil), z) <= True
count_elt(b, econs(b, enil), s(z)) <= True
count_elt(b, enil, z) <= True
mem_elt(a, econs(a, econs(b, enil))) <= True
mem_elt(a, econs(a, enil)) <= True
mem_elt(a, econs(b, econs(a, econs(b, enil)))) <= True
mem_elt(a, econs(b, econs(a, enil))) <= True
mem_elt(a, econs(b, econs(b, econs(a, enil)))) <= True
mem_elt(b, econs(a, econs(a, econs(b, enil)))) <= True
mem_elt(b, econs(a, econs(b, enil))) <= True
mem_elt(b, econs(b, enil)) <= True
False <= count_elt(a, econs(a, econs(b, enil)), z)
False <= count_elt(a, econs(a, enil), z)
False <= count_elt(a, econs(b, econs(a, econs(b, enil))), z)
False <= count_elt(a, econs(b, econs(a, enil)), z)
False <= count_elt(b, econs(a, econs(b, econs(a, enil))), z) /\ mem_elt(b, econs(a, econs(b, econs(a, enil))))
False <= count_elt(b, econs(a, econs(b, enil)), z)
False <= count_elt(b, econs(b, econs(a, enil)), z) /\ mem_elt(b, econs(b, econs(a, enil)))
False <= count_elt(b, econs(b, enil), z)
False <= mem_elt(a, econs(b, econs(b, enil)))
False <= mem_elt(a, econs(b, enil))
False <= mem_elt(a, enil)
False <= mem_elt(b, econs(a, econs(a, enil)))
False <= mem_elt(b, econs(a, enil))
False <= mem_elt(b, enil)
}

Current best model:
|_
name: None

count_elt ->
[
count_elt : <elt * elist * nat>
{
  _r_1(b) <= True
  _r_2(a) <= True
  _r_4(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_4(enil) <= True
  _r_5(econs(x_0_0, x_0_1)) <= _r_2(x_0_0)
  _r_5(enil) <= True
  count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1)
  count_elt(a, econs(x_1_0, x_1_1), z) <= _r_1(x_1_0) /\ _r_4(x_1_1)
  count_elt(a, enil, z) <= True
  count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1)
  count_elt(b, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) /\ _r_5(x_1_1)
  count_elt(b, enil, z) <= True
}
]


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  _r_1(b) <= True
  _r_2(a) <= True
  _r_3(econs(x_0_0, x_0_1)) <= _r_2(x_0_0)
  _r_3(econs(x_0_0, x_0_1)) <= _r_3(x_0_1)
  _r_6(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_6(econs(x_0_0, x_0_1)) <= _r_6(x_0_1)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_2(x_1_0)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_3(x_1_1)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_1(x_1_0)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_6(x_1_1)
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
No: ()

mem_elt(h, econs(h, t)) <= True  :
No: ()

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
Yes: {
e -> b  ;  l -> econs(a, econs(a, econs(b, _xhxs_1)))
}

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
Yes: {
_wwa -> s(_wcxs_0)  ;  t1 -> econs(b, enil)  ;  x -> a
}

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
Yes: {
_xwa -> s(_odxs_0)  ;  h1 -> b  ;  t1 -> econs(b, enil)  ;  x -> a
}

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
No: ()


-------------------------------------------
Step 14, which took 0.285795 s (model generation: 0.284955,  model checking: 0.000840):

Clauses:
{
count_elt(x, enil, z) <= True -> 0
mem_elt(h, econs(h, t)) <= True -> 0
False <= count_elt(e, l, z) /\ mem_elt(e, l) -> 0
count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa) -> 0
eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa) -> 0
eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t) -> 0
eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t)) -> 0
}

Accumulated learning constraints:
{
count_elt(a, econs(a, enil), s(z)) <= True
count_elt(a, econs(b, econs(b, enil)), z) <= True
count_elt(a, econs(b, enil), z) <= True
count_elt(a, enil, z) <= True
count_elt(b, econs(a, econs(a, enil)), z) <= True
count_elt(b, econs(a, enil), z) <= True
count_elt(b, econs(b, enil), s(z)) <= True
count_elt(b, enil, z) <= True
mem_elt(a, econs(a, econs(b, enil))) <= True
mem_elt(a, econs(a, enil)) <= True
mem_elt(a, econs(b, econs(a, econs(b, enil)))) <= True
mem_elt(a, econs(b, econs(a, enil))) <= True
mem_elt(a, econs(b, econs(b, econs(a, enil)))) <= True
mem_elt(b, econs(a, econs(a, econs(b, enil)))) <= True
mem_elt(b, econs(a, econs(b, enil))) <= True
mem_elt(b, econs(b, enil)) <= True
False <= count_elt(a, econs(a, econs(b, enil)), z)
False <= count_elt(a, econs(a, enil), z)
False <= count_elt(a, econs(b, econs(a, econs(b, enil))), z)
False <= count_elt(a, econs(b, econs(a, enil)), z)
count_elt(a, econs(a, econs(b, enil)), s(s(z))) <= count_elt(a, econs(b, enil), s(z))
count_elt(a, econs(b, econs(b, enil)), s(z)) <= count_elt(a, econs(b, enil), s(z))
False <= count_elt(b, econs(a, econs(a, econs(b, enil))), z)
False <= count_elt(b, econs(a, econs(b, econs(a, enil))), z) /\ mem_elt(b, econs(a, econs(b, econs(a, enil))))
False <= count_elt(b, econs(a, econs(b, enil)), z)
False <= count_elt(b, econs(b, econs(a, enil)), z) /\ mem_elt(b, econs(b, econs(a, enil)))
False <= count_elt(b, econs(b, enil), z)
False <= mem_elt(a, econs(b, econs(b, enil)))
False <= mem_elt(a, econs(b, enil))
False <= mem_elt(a, enil)
False <= mem_elt(b, econs(a, econs(a, enil)))
False <= mem_elt(b, econs(a, enil))
False <= mem_elt(b, enil)
}

Current best model:
|_
name: None

count_elt ->
[
count_elt : <elt * elist * nat>
{
  _r_1(b) <= True
  _r_2(a) <= True
  _r_3(econs(x_0_0, x_0_1)) <= _r_2(x_0_0) /\ _r_3(x_0_1)
  _r_3(enil) <= True
  _r_5(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_5(enil) <= True
  count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(a, econs(x_1_0, x_1_1), z) <= _r_1(x_1_0) /\ _r_5(x_1_1)
  count_elt(a, enil, z) <= True
  count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1)
  count_elt(b, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) /\ _r_3(x_1_1)
  count_elt(b, enil, z) <= True
}
]


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  _r_1(b) <= True
  _r_2(a) <= True
  _r_4(econs(x_0_0, x_0_1)) <= _r_2(x_0_0)
  _r_4(econs(x_0_0, x_0_1)) <= _r_4(x_0_1)
  _r_6(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_6(econs(x_0_0, x_0_1)) <= _r_6(x_0_1)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_2(x_1_0)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_4(x_1_1)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_1(x_1_0)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_6(x_1_1)
}
]



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




Answer of teacher:

count_elt(x, enil, z) <= True  :
No: ()

mem_elt(h, econs(h, t)) <= True  :
No: ()

False <= count_elt(e, l, z) /\ mem_elt(e, l)  :
Yes: {
e -> a  ;  l -> econs(b, econs(b, econs(a, _cnxs_1)))
}

count_elt(x, econs(x, t1), s(_wwa)) <= count_elt(x, t1, _wwa)  :
Yes: {
_wwa -> s(_sixs_0)  ;  t1 -> econs(a, enil)  ;  x -> b
}

eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _xwa) <= count_elt(x, t1, _xwa)  :
Yes: {
_xwa -> s(_rjxs_0)  ;  h1 -> a  ;  t1 -> econs(a, enil)  ;  x -> b
}

eq_elt(e, h) \/ mem_elt(e, econs(h, t)) <= mem_elt(e, t)  :
No: ()

eq_elt(e, h) \/ mem_elt(e, t) <= mem_elt(e, econs(h, t))  :
No: ()


Total time: 1.671025
Learner time: 1.264828
Teacher time: 0.011799
Reasons for stopping: Yes: |_
name: None

count_elt ->
[
count_elt : <elt * elist * nat>
{
  _r_1(a) <= True
  _r_2(b) <= True
  _r_3(econs(x_0_0, x_0_1)) <= _r_1(x_0_0) /\ _r_3(x_0_1)
  _r_3(enil) <= True
  _r_5(econs(x_0_0, x_0_1)) <= _r_2(x_0_0) /\ _r_5(x_0_1)
  _r_5(enil) <= True
  count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(a, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) /\ _r_5(x_1_1)
  count_elt(a, enil, z) <= True
  count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= True
  count_elt(b, econs(x_1_0, x_1_1), z) <= _r_1(x_1_0) /\ _r_3(x_1_1)
  count_elt(b, enil, z) <= True
}
]


;
mem_elt ->
[
mem_elt : <elt * elist>
{
  _r_1(a) <= True
  _r_2(b) <= True
  _r_4(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_4(econs(x_0_0, x_0_1)) <= _r_4(x_0_1)
  _r_6(econs(x_0_0, x_0_1)) <= _r_2(x_0_0)
  _r_6(econs(x_0_0, x_0_1)) <= _r_6(x_0_1)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_1(x_1_0)
  mem_elt(a, econs(x_1_0, x_1_1)) <= _r_4(x_1_1)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_2(x_1_0)
  mem_elt(b, econs(x_1_0, x_1_1)) <= _r_6(x_1_1)
}
]



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