Solving ../../benchmarks/smtlib/false/prefix_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: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{
leq(z, s(nn2)) <= True
leq(z, z) <= True
leq(s(nn1), s(nn2)) <= leq(nn1, nn2)
leq(nn1, nn2) <= leq(s(nn1), s(nn2))
False <= leq(s(nn1), z)
}
)
(prefix, P:
{
prefix(nil, y) <= True
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))
eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys))
False <= prefix(cons(z, zs), nil)
}
)
(count, F:
{
count(x, nil, z) <= True
count(x, cons(x, t1), s(_icb)) <= count(x, t1, _icb)
eq_elt(h1, x) \/ count(x, cons(h1, t1), _jcb) <= count(x, t1, _jcb)
}
eq_nat(_mcb, _ncb) <= count(_kcb, _lcb, _mcb) /\ count(_kcb, _lcb, _ncb)
)
}

properties:
{
leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2)
}


over-approximation: {count, prefix}
under-approximation: {leq}

Clause system for inference is:

{
count(x, nil, z) <= True -> 0
prefix(nil, y) <= True -> 0
leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2) -> 0
count(x, cons(x, t1), s(_icb)) <= count(x, t1, _icb) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _jcb) <= count(x, t1, _jcb) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
}


Solving took 0.091846 seconds.
No: Contradictory set of ground constraints:
{
False <= True
count(a, 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, nil), s(z)) <= True
count(b, nil, z) <= True
leq(s(z), s(z)) <= True
leq(z, z) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
False <= count(b, cons(a, nil), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
prefix(cons(a, nil), nil) <= prefix(cons(a, cons(a, nil)), cons(a, nil))
leq(z, s(z)) <= prefix(cons(a, nil), nil)
}
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006628 s (model generation: 0.006539,  model checking: 0.000089):

Clauses:
{
count(x, nil, z) <= True -> 0
prefix(nil, y) <= True -> 0
leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2) -> 0
count(x, cons(x, t1), s(_icb)) <= count(x, t1, _icb) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _jcb) <= count(x, t1, _jcb) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


;
leq ->
[
leq : <nat * nat>
{
  
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  
}
]



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




Answer of teacher:

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

prefix(nil, y) <= True  :
Yes: {
y -> nil
}

leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2)  :
No: ()

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

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
No: ()


-------------------------------------------
Step 1, which took 0.006424 s (model generation: 0.006324,  model checking: 0.000100):

Clauses:
{
count(x, nil, z) <= True -> 0
prefix(nil, y) <= True -> 0
leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2) -> 0
count(x, cons(x, t1), s(_icb)) <= count(x, t1, _icb) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _jcb) <= count(x, t1, _jcb) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
}

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

Current best model:
|_
name: None

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


;
leq ->
[
leq : <nat * nat>
{
  
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

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

prefix(nil, y) <= True  :
Yes: {
y -> cons(_qyqqw_0, _qyqqw_1)
}

leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2)  :
Yes: {
_ocb -> z  ;  _pcb -> z  ;  l1 -> nil  ;  l2 -> nil  ;  x -> b
}

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

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
Yes: {
ys -> nil  ;  zs -> nil
}

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
No: ()


-------------------------------------------
Step 2, which took 0.009173 s (model generation: 0.009004,  model checking: 0.000169):

Clauses:
{
count(x, nil, z) <= True -> 0
prefix(nil, y) <= True -> 0
leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2) -> 0
count(x, cons(x, t1), s(_icb)) <= count(x, t1, _icb) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _jcb) <= count(x, t1, _jcb) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 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
leq(z, z) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= 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
}
]


;
leq ->
[
leq : <nat * nat>
{
  leq(z, z) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

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

prefix(nil, y) <= True  :
No: ()

leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2)  :
Yes: {
_ocb -> z  ;  _pcb -> s(_lzqqw_0)  ;  l1 -> cons(_mzqqw_0, _mzqqw_1)  ;  l2 -> cons(_nzqqw_0, _nzqqw_1)  ;  x -> b
}

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

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
Yes: {
nn1 -> z  ;  nn2 -> z
}

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
Yes: {
ys -> nil  ;  zs -> cons(_jarqw_0, _jarqw_1)
}


-------------------------------------------
Step 3, which took 0.010385 s (model generation: 0.010226,  model checking: 0.000159):

Clauses:
{
count(x, nil, z) <= True -> 0
prefix(nil, y) <= True -> 0
leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2) -> 0
count(x, cons(x, t1), s(_icb)) <= count(x, t1, _icb) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _jcb) <= count(x, t1, _jcb) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 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
leq(s(z), s(z)) <= True
leq(z, z) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
leq(z, s(z)) <= count(b, cons(a, nil), s(z))
prefix(cons(a, nil), nil) <= prefix(cons(a, cons(a, nil)), cons(a, nil))
}

Current best model:
|_
name: None

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


;
leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= True
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  prefix(cons(x_0_0, x_0_1), nil) <= True
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

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

prefix(nil, y) <= True  :
No: ()

leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2)  :
Yes: {
_ocb -> s(_zarqw_0)  ;  _pcb -> z  ;  l1 -> nil  ;  l2 -> cons(_cbrqw_0, _cbrqw_1)  ;  x -> b
}

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

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
Yes: {
nn1 -> s(_ebrqw_0)  ;  nn2 -> z
}

False <= leq(s(nn1), z)  :
No: ()

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
No: ()


-------------------------------------------
Step 4, which took 0.010683 s (model generation: 0.010598,  model checking: 0.000085):

Clauses:
{
count(x, nil, z) <= True -> 0
prefix(nil, y) <= True -> 0
leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2) -> 0
count(x, cons(x, t1), s(_icb)) <= count(x, t1, _icb) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _jcb) <= count(x, t1, _jcb) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 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
leq(s(z), s(z)) <= True
leq(z, z) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
leq(s(z), z) <= count(b, cons(a, nil), s(z))
leq(z, s(z)) <= count(b, cons(a, nil), s(z))
leq(s(z), z) <= leq(s(s(z)), s(z))
prefix(cons(a, nil), nil) <= prefix(cons(a, cons(a, nil)), cons(a, nil))
}

Current best model:
|_
name: None

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


;
leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= True
  leq(s(x_0_0), z) <= True
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  prefix(cons(x_0_0, x_0_1), nil) <= True
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

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

prefix(nil, y) <= True  :
No: ()

leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2)  :
No: ()

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

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
Yes: {

}

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
No: ()


-------------------------------------------
Step 5, which took 0.014662 s (model generation: 0.014397,  model checking: 0.000265):

Clauses:
{
count(x, nil, z) <= True -> 0
prefix(nil, y) <= True -> 0
leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2) -> 0
count(x, cons(x, t1), s(_icb)) <= count(x, t1, _icb) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _jcb) <= count(x, t1, _jcb) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 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
leq(s(z), s(z)) <= True
leq(z, z) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
False <= count(b, cons(a, nil), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
prefix(cons(a, nil), nil) <= prefix(cons(a, cons(a, nil)), cons(a, nil))
}

Current best model:
|_
name: None

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


;
leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, z) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  prefix(cons(x_0_0, x_0_1), nil) <= True
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

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

prefix(nil, y) <= True  :
No: ()

leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2)  :
Yes: {
_ocb -> z  ;  _pcb -> s(_rbrqw_0)  ;  l1 -> cons(_sbrqw_0, _sbrqw_1)  ;  l2 -> nil  ;  x -> a
}

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

eq_elt(h1, x) \/ count(x, cons(h1, t1), _jcb) <= count(x, t1, _jcb)  :
Yes: {
_jcb -> s(_ndrqw_0)  ;  h1 -> a  ;  t1 -> cons(b, _pdrqw_1)  ;  x -> b
}

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
No: ()


-------------------------------------------
Step 6, which took 0.023441 s (model generation: 0.022952,  model checking: 0.000489):

Clauses:
{
count(x, nil, z) <= True -> 0
prefix(nil, y) <= True -> 0
leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2) -> 0
count(x, cons(x, t1), s(_icb)) <= count(x, t1, _icb) -> 0
eq_elt(h1, x) \/ count(x, cons(h1, t1), _jcb) <= count(x, t1, _jcb) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 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, cons(b, nil)), s(z)) <= True
count(b, cons(a, nil), z) <= True
count(b, cons(b, nil), s(z)) <= True
count(b, nil, z) <= True
leq(s(z), s(z)) <= True
leq(z, z) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
False <= count(b, cons(a, nil), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
prefix(cons(a, nil), nil) <= prefix(cons(a, cons(a, nil)), cons(a, nil))
leq(z, s(z)) <= prefix(cons(a, nil), nil)
}

Current best model:
|_
name: None

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


;
leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  prefix(cons(x_0_0, x_0_1), nil) <= True
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

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

prefix(nil, y) <= True  :
No: ()

leq(_ocb, _pcb) <= count(x, l1, _pcb) /\ count(x, l2, _ocb) /\ prefix(l1, l2)  :
Yes: {
_ocb -> s(_merqw_0)  ;  _pcb -> z  ;  l1 -> nil  ;  l2 -> cons(_perqw_0, _perqw_1)  ;  x -> a
}

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

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
No: ()


Total time: 0.091846
Learner time: 0.080040
Teacher time: 0.001356
Reasons for stopping: No: Contradictory set of ground constraints:
{
False <= True
count(a, 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, nil), s(z)) <= True
count(b, nil, z) <= True
leq(s(z), s(z)) <= True
leq(z, z) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
False <= count(b, cons(a, nil), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
prefix(cons(a, nil), nil) <= prefix(cons(a, cons(a, nil)), cons(a, nil))
leq(z, s(z)) <= prefix(cons(a, nil), nil)
}