Solving ../../benchmarks/false/prefix_count.smt2...

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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{() -> leq([z, s(nn2)])
() -> leq([z, z])
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)])
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2])
(leq([s(nn1), z])) -> BOT}
)
(prefix, P:
{() -> prefix([nil, y])
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)])
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys])
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT
(prefix([cons(z, zs), nil])) -> BOT}
)
(count, F:
{() -> count([x, nil, z])
(count([x, t1, _ila])) -> count([x, cons(x, t1), s(_ila)])
(count([x, t1, _jla]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _jla])}
(count([_kla, _lla, _mla]) /\ count([_kla, _lla, _nla])) -> eq_nat([_mla, _nla])
)
}

properties:
{(count([x, l1, _pla]) /\ count([x, l2, _ola]) /\ prefix([l1, l2])) -> leq([_ola, _pla])}


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

Clause system for inference is:

{
() -> count([x, nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 0
() -> prefix([nil, y]) -> 0
(count([x, l1, _pla]) /\ count([x, l2, _ola]) /\ prefix([l1, l2])) -> leq([_ola, _pla]) -> 0
(count([x, t1, _ila])) -> count([x, cons(x, t1), s(_ila)]) -> 0
(count([x, t1, _jla]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _jla]) -> 0
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0
(leq([s(nn1), z])) -> BOT -> 0
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 0
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 0
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 0
(prefix([cons(z, zs), nil])) -> BOT -> 0
}


Solving took 0.230639 seconds.
Disproved
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.017408 s (model generation: 0.016658,  model checking: 0.000750):

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

}

Datatype: <elt, eltlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 0
() -> prefix([nil, y]) -> 3
(count([x, l1, _pla]) /\ count([x, l2, _ola]) /\ prefix([l1, l2])) -> leq([_ola, _pla]) -> 1
(count([x, t1, _ila])) -> count([x, cons(x, t1), s(_ila)]) -> 1
(count([x, t1, _jla]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _jla]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 1
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 1
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 1
(prefix([cons(z, zs), nil])) -> BOT -> 1
}
Sat witness: Found: (() -> prefix([nil, y]), {
y -> nil
})

-------------------------------------------
Step 1, which took 0.016143 s (model generation: 0.016040,  model checking: 0.000103):

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

}

Datatype: <elt, eltlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_9010},
Q_f={q_gen_9010},
Delta=
{
<nil, nil>() -> q_gen_9010
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 3
() -> prefix([nil, y]) -> 3
(count([x, l1, _pla]) /\ count([x, l2, _ola]) /\ prefix([l1, l2])) -> leq([_ola, _pla]) -> 1
(count([x, t1, _ila])) -> count([x, cons(x, t1), s(_ila)]) -> 1
(count([x, t1, _jla]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _jla]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 1
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 1
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 1
(prefix([cons(z, zs), nil])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([z, z]), {

})

-------------------------------------------
Step 2, which took 0.016675 s (model generation: 0.016525,  model checking: 0.000150):

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

}

Datatype: <elt, eltlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_9011},
Q_f={q_gen_9011},
Delta=
{
<z, z>() -> q_gen_9011
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_9010},
Q_f={q_gen_9010},
Delta=
{
<nil, nil>() -> q_gen_9010
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> prefix([nil, y]) -> 3
(count([x, l1, _pla]) /\ count([x, l2, _ola]) /\ prefix([l1, l2])) -> leq([_ola, _pla]) -> 1
(count([x, t1, _ila])) -> count([x, cons(x, t1), s(_ila)]) -> 1
(count([x, t1, _jla]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _jla]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 1
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 1
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 1
(prefix([cons(z, zs), nil])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 3, which took 0.017263 s (model generation: 0.017046,  model checking: 0.000217):

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

}

Datatype: <elt, eltlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_9011, q_gen_9013},
Q_f={q_gen_9011},
Delta=
{
<z>() -> q_gen_9013
<z, s>(q_gen_9013) -> q_gen_9011
<z, z>() -> q_gen_9011
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_9010},
Q_f={q_gen_9010},
Delta=
{
<nil, nil>() -> q_gen_9010
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> prefix([nil, y]) -> 3
(count([x, l1, _pla]) /\ count([x, l2, _ola]) /\ prefix([l1, l2])) -> leq([_ola, _pla]) -> 1
(count([x, t1, _ila])) -> count([x, cons(x, t1), s(_ila)]) -> 1
(count([x, t1, _jla]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _jla]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 1
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 1
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 1
(prefix([cons(z, zs), nil])) -> BOT -> 1
}
Sat witness: Found: (() -> count([x, nil, z]), {
x -> b
})

-------------------------------------------
Step 4, which took 0.018288 s (model generation: 0.017320,  model checking: 0.000968):

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

Datatype: <elt, eltlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_9011, q_gen_9013},
Q_f={q_gen_9011},
Delta=
{
<z>() -> q_gen_9013
<z, s>(q_gen_9013) -> q_gen_9011
<z, z>() -> q_gen_9011
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_9010},
Q_f={q_gen_9010},
Delta=
{
<nil, nil>() -> q_gen_9010
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> prefix([nil, y]) -> 3
(count([x, l1, _pla]) /\ count([x, l2, _ola]) /\ prefix([l1, l2])) -> leq([_ola, _pla]) -> 1
(count([x, t1, _ila])) -> count([x, cons(x, t1), s(_ila)]) -> 1
(count([x, t1, _jla]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _jla]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 2
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 2
(prefix([cons(z, zs), nil])) -> BOT -> 2
}
Sat witness: Found: ((prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]), {
y2 -> b  ;  ys -> nil  ;  zs -> nil
})

-------------------------------------------
Step 5, which took 0.018039 s (model generation: 0.017759,  model checking: 0.000280):

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

Datatype: <elt, eltlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_9011, q_gen_9013},
Q_f={q_gen_9011},
Delta=
{
<z>() -> q_gen_9013
<z, s>(q_gen_9013) -> q_gen_9011
<z, z>() -> q_gen_9011
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_9010, q_gen_9016},
Q_f={q_gen_9010},
Delta=
{
<cons, cons>(q_gen_9016, q_gen_9010) -> q_gen_9010
<nil, nil>() -> q_gen_9010
<b, b>() -> q_gen_9016
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> prefix([nil, y]) -> 3
(count([x, l1, _pla]) /\ count([x, l2, _ola]) /\ prefix([l1, l2])) -> leq([_ola, _pla]) -> 1
(count([x, t1, _ila])) -> count([x, cons(x, t1), s(_ila)]) -> 1
(count([x, t1, _jla]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _jla]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 2
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 2
(prefix([cons(z, zs), nil])) -> BOT -> 2
}
Sat witness: Found: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 6, which took 0.018803 s (model generation: 0.018398,  model checking: 0.000405):

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

Datatype: <elt, eltlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_9011, q_gen_9013},
Q_f={q_gen_9011},
Delta=
{
<z>() -> q_gen_9013
<s, s>(q_gen_9011) -> q_gen_9011
<z, s>(q_gen_9013) -> q_gen_9011
<z, z>() -> q_gen_9011
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_9010, q_gen_9016},
Q_f={q_gen_9010},
Delta=
{
<cons, cons>(q_gen_9016, q_gen_9010) -> q_gen_9010
<nil, nil>() -> q_gen_9010
<b, b>() -> q_gen_9016
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> prefix([nil, y]) -> 3
(count([x, l1, _pla]) /\ count([x, l2, _ola]) /\ prefix([l1, l2])) -> leq([_ola, _pla]) -> 1
(count([x, t1, _ila])) -> count([x, cons(x, t1), s(_ila)]) -> 1
(count([x, t1, _jla]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _jla]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 2
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 2
(prefix([cons(z, zs), nil])) -> BOT -> 2
}
Sat witness: Found: ((count([x, t1, _jla]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _jla]), {
_jla -> z  ;  h1 -> a  ;  t1 -> nil  ;  x -> b
})

-------------------------------------------
Step 7, which took 0.020115 s (model generation: 0.019692,  model checking: 0.000423):

Model:
|_
{
count -> 
{{{
Q={q_gen_9014, q_gen_9019, q_gen_9020},
Q_f={q_gen_9014},
Delta=
{
<nil>() -> q_gen_9019
<a>() -> q_gen_9020
<b, cons, z>(q_gen_9020, q_gen_9019) -> q_gen_9014
<b, nil, z>() -> q_gen_9014
}

Datatype: <elt, eltlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_9011, q_gen_9013},
Q_f={q_gen_9011},
Delta=
{
<z>() -> q_gen_9013
<s, s>(q_gen_9011) -> q_gen_9011
<z, s>(q_gen_9013) -> q_gen_9011
<z, z>() -> q_gen_9011
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_9010, q_gen_9016},
Q_f={q_gen_9010},
Delta=
{
<cons, cons>(q_gen_9016, q_gen_9010) -> q_gen_9010
<nil, nil>() -> q_gen_9010
<b, b>() -> q_gen_9016
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> prefix([nil, y]) -> 3
(count([x, l1, _pla]) /\ count([x, l2, _ola]) /\ prefix([l1, l2])) -> leq([_ola, _pla]) -> 1
(count([x, t1, _ila])) -> count([x, cons(x, t1), s(_ila)]) -> 4
(count([x, t1, _jla]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _jla]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 2
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 2
(prefix([cons(z, zs), nil])) -> BOT -> 2
}
Sat witness: Found: ((count([x, t1, _ila])) -> count([x, cons(x, t1), s(_ila)]), {
_ila -> z  ;  t1 -> nil  ;  x -> b
})

-------------------------------------------
Step 8, which took 0.022284 s (model generation: 0.020110,  model checking: 0.002174):

Model:
|_
{
count -> 
{{{
Q={q_gen_9014, q_gen_9019, q_gen_9020, q_gen_9022},
Q_f={q_gen_9014},
Delta=
{
<nil>() -> q_gen_9019
<a>() -> q_gen_9020
<b, z>() -> q_gen_9022
<b, cons, s>(q_gen_9022, q_gen_9019) -> q_gen_9014
<b, cons, z>(q_gen_9020, q_gen_9019) -> q_gen_9014
<b, nil, z>() -> q_gen_9014
}

Datatype: <elt, eltlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_9011, q_gen_9013},
Q_f={q_gen_9011},
Delta=
{
<z>() -> q_gen_9013
<s, s>(q_gen_9011) -> q_gen_9011
<z, s>(q_gen_9013) -> q_gen_9011
<z, z>() -> q_gen_9011
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_9010, q_gen_9016},
Q_f={q_gen_9010},
Delta=
{
<cons, cons>(q_gen_9016, q_gen_9010) -> q_gen_9010
<nil, nil>() -> q_gen_9010
<b, b>() -> q_gen_9016
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> prefix([nil, y]) -> 6
(count([x, l1, _pla]) /\ count([x, l2, _ola]) /\ prefix([l1, l2])) -> leq([_ola, _pla]) -> 2
(count([x, t1, _ila])) -> count([x, cons(x, t1), s(_ila)]) -> 4
(count([x, t1, _jla]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _jla]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3
(leq([s(nn1), z])) -> BOT -> 3
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 3
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 3
(prefix([cons(z, zs), nil])) -> BOT -> 3
}
Sat witness: Found: (() -> prefix([nil, y]), {
y -> cons(b, nil)
})

-------------------------------------------
Step 9, which took 0.021323 s (model generation: 0.020770,  model checking: 0.000553):

Model:
|_
{
count -> 
{{{
Q={q_gen_9014, q_gen_9019, q_gen_9020, q_gen_9022},
Q_f={q_gen_9014},
Delta=
{
<nil>() -> q_gen_9019
<a>() -> q_gen_9020
<b, z>() -> q_gen_9022
<b, cons, s>(q_gen_9022, q_gen_9019) -> q_gen_9014
<b, cons, z>(q_gen_9020, q_gen_9019) -> q_gen_9014
<b, nil, z>() -> q_gen_9014
}

Datatype: <elt, eltlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_9011, q_gen_9013},
Q_f={q_gen_9011},
Delta=
{
<z>() -> q_gen_9013
<s, s>(q_gen_9011) -> q_gen_9011
<z, s>(q_gen_9013) -> q_gen_9011
<z, z>() -> q_gen_9011
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_9010, q_gen_9016, q_gen_9024, q_gen_9025},
Q_f={q_gen_9010},
Delta=
{
<nil>() -> q_gen_9024
<b>() -> q_gen_9025
<cons, cons>(q_gen_9016, q_gen_9010) -> q_gen_9010
<nil, cons>(q_gen_9025, q_gen_9024) -> q_gen_9010
<nil, nil>() -> q_gen_9010
<b, b>() -> q_gen_9016
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> prefix([nil, y]) -> 6
(count([x, l1, _pla]) /\ count([x, l2, _ola]) /\ prefix([l1, l2])) -> leq([_ola, _pla]) -> 5
(count([x, t1, _ila])) -> count([x, cons(x, t1), s(_ila)]) -> 4
(count([x, t1, _jla]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _jla]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3
(leq([s(nn1), z])) -> BOT -> 3
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 3
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 3
(prefix([cons(z, zs), nil])) -> BOT -> 3
}
Sat witness: Found: ((count([x, l1, _pla]) /\ count([x, l2, _ola]) /\ prefix([l1, l2])) -> leq([_ola, _pla]), {
_ola -> s(z)  ;  _pla -> z  ;  l1 -> nil  ;  l2 -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 10, which took 0.024038 s (model generation: 0.020907,  model checking: 0.003131):

Model:
|_
{
count -> 
{{{
Q={q_gen_9014, q_gen_9019, q_gen_9020, q_gen_9022},
Q_f={q_gen_9014},
Delta=
{
<nil>() -> q_gen_9019
<a>() -> q_gen_9020
<b, z>() -> q_gen_9022
<b, cons, s>(q_gen_9022, q_gen_9019) -> q_gen_9014
<b, cons, z>(q_gen_9020, q_gen_9019) -> q_gen_9014
<b, nil, z>() -> q_gen_9014
}

Datatype: <elt, eltlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_9011, q_gen_9013},
Q_f={q_gen_9011},
Delta=
{
<z>() -> q_gen_9013
<s, s>(q_gen_9011) -> q_gen_9011
<s, z>(q_gen_9013) -> q_gen_9011
<z, s>(q_gen_9013) -> q_gen_9011
<z, z>() -> q_gen_9011
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  prefix -> 
{{{
Q={q_gen_9010, q_gen_9016, q_gen_9024, q_gen_9025},
Q_f={q_gen_9010},
Delta=
{
<nil>() -> q_gen_9024
<b>() -> q_gen_9025
<cons, cons>(q_gen_9016, q_gen_9010) -> q_gen_9010
<nil, cons>(q_gen_9025, q_gen_9024) -> q_gen_9010
<nil, nil>() -> q_gen_9010
<b, b>() -> q_gen_9016
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> prefix([nil, y]) -> 6
(count([x, l1, _pla]) /\ count([x, l2, _ola]) /\ prefix([l1, l2])) -> leq([_ola, _pla]) -> 5
(count([x, t1, _ila])) -> count([x, cons(x, t1), s(_ila)]) -> 4
(count([x, t1, _jla]) /\ not eq_elt([h1, x])) -> count([x, cons(h1, t1), _jla]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3
(leq([s(nn1), z])) -> BOT -> 6
(prefix([zs, ys])) -> prefix([cons(y2, zs), cons(y2, ys)]) -> 4
(prefix([cons(y2, zs), cons(y2, ys)])) -> prefix([zs, ys]) -> 4
(prefix([cons(z, zs), cons(y2, ys)]) /\ not eq_elt([z, y2])) -> BOT -> 4
(prefix([cons(z, zs), nil])) -> BOT -> 4
}
Sat witness: Found: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

Total time: 0.230639
Reason for stopping: Disproved