Solving ../../benchmarks/true/merge_length_leq.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{() -> leq([a, n2])
() -> leq([b, b])
(leq([b, a])) -> BOT}
)
(leqnat, P:
{() -> leqnat([z, n2])
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)])
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2])
(leqnat([s(nn1), z])) -> BOT}
)
(merge, F:
{() -> merge([cons(z, xs), nil, cons(z, xs)])
() -> merge([nil, y, y])
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)])
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)])}
(merge([_yw, _zw, _ax]) /\ merge([_yw, _zw, _bx])) -> eq_eltlist([_ax, _bx])
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)])}
(append([_dx, _ex, _fx]) /\ append([_dx, _ex, _gx])) -> eq_eltlist([_fx, _gx])
)
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)])}
(plus([_ix, _jx, _kx]) /\ plus([_ix, _jx, _lx])) -> eq_nat([_kx, _lx])
)
(length, F:
{() -> length([nil, z])
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)])}
(length([_nx, _ox]) /\ length([_nx, _px])) -> eq_nat([_ox, _px])
)
}

properties:
{(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]), (length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx])}


over-approximation: {append, length, merge, plus}
under-approximation: {append, leqnat, plus}

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([a, n2]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> leqnat([z, n2]) -> 0  ;  () -> merge([cons(z, xs), nil, cons(z, xs)]) -> 0  ;  () -> merge([nil, y, y]) -> 0  ;  () -> plus([n, z, n]) -> 0  ;  (append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 0  ;  (length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 0  ;  (length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 0  ;  (length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 0  ;  (leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 0  ;  (not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 0  ;  (leq([b, a])) -> BOT -> 0  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 0  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 0  ;  (leqnat([s(nn1), z])) -> BOT -> 0  ;  (plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 0
}


Solving took 30.008707 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_4560},
Q_f={},
Delta=
{
<nil, nil, nil>() -> q_gen_4560
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_4559},
Q_f={},
Delta=
{
<nil, z>() -> q_gen_4559
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_4557, q_gen_4558, q_gen_4564},
Q_f={},
Delta=
{
<b, b>() -> q_gen_4557
<a, b>() -> q_gen_4558
<b, a>() -> q_gen_4564
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4556, q_gen_4563},
Q_f={},
Delta=
{
<z, z>() -> q_gen_4556
<s, s>(q_gen_4556) -> q_gen_4563
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  merge -> 
{{{
Q={q_gen_4550, q_gen_4551, q_gen_4552, q_gen_4553, q_gen_4554, q_gen_4555, q_gen_4565, q_gen_4566, q_gen_4567, q_gen_4568, q_gen_4569, q_gen_4570, q_gen_4571, q_gen_4572, q_gen_4573, q_gen_4574, q_gen_4575},
Q_f={},
Delta=
{
<nil>() -> q_gen_4567
<b>() -> q_gen_4568
<nil, nil>() -> q_gen_4552
<nil, b>() -> q_gen_4553
<b, nil>() -> q_gen_4554
<b, b>() -> q_gen_4555
<nil, nil, nil>() -> q_gen_4550
<cons, nil, cons>(q_gen_4555, q_gen_4554, q_gen_4553, q_gen_4552) -> q_gen_4551
<cons, cons, cons>(q_gen_4575, q_gen_4574, q_gen_4573, q_gen_4572, q_gen_4571, q_gen_4570, q_gen_4569, q_gen_4566) -> q_gen_4565
<nil, nil, cons>(q_gen_4568, q_gen_4567) -> q_gen_4566
<nil, nil, a>() -> q_gen_4569
<nil, a, cons>(q_gen_4568, q_gen_4567) -> q_gen_4570
<nil, a, a>() -> q_gen_4571
<b, nil, cons>(q_gen_4568, q_gen_4567) -> q_gen_4572
<b, nil, a>() -> q_gen_4573
<b, a, cons>(q_gen_4568, q_gen_4567) -> q_gen_4574
<b, a, a>() -> q_gen_4575
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4549, q_gen_4561, q_gen_4562},
Q_f={},
Delta=
{
<z, z>() -> q_gen_4562
<z, z, z>() -> q_gen_4549
<z, s, s>(q_gen_4562) -> q_gen_4561
}

Datatype: <nat, nat, nat>
Convolution form: complete
}}}

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005062 s (model generation: 0.003988,  model checking: 0.001074):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([a, n2]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> leqnat([z, n2]) -> 0  ;  () -> merge([cons(z, xs), nil, cons(z, xs)]) -> 0  ;  () -> merge([nil, y, y]) -> 0  ;  () -> plus([n, z, n]) -> 3  ;  (append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1  ;  (length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1  ;  (length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1  ;  (length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1  ;  (leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1  ;  (not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1  ;  (leqnat([s(nn1), z])) -> BOT -> 1  ;  (plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.003849 s (model generation: 0.003551,  model checking: 0.000298):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4549},
Q_f={q_gen_4549},
Delta=
{
<z, z, z>() -> q_gen_4549
}

Datatype: <nat, nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([a, n2]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> leqnat([z, n2]) -> 0  ;  () -> merge([cons(z, xs), nil, cons(z, xs)]) -> 0  ;  () -> merge([nil, y, y]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1  ;  (length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1  ;  (length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1  ;  (length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1  ;  (leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1  ;  (not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1  ;  (leqnat([s(nn1), z])) -> BOT -> 1  ;  (plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Yes: (() -> merge([nil, y, y]), {
y -> nil
})

-------------------------------------------
Step 2, which took 0.003921 s (model generation: 0.003436,  model checking: 0.000485):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  merge -> 
{{{
Q={q_gen_4550},
Q_f={q_gen_4550},
Delta=
{
<nil, nil, nil>() -> q_gen_4550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4549},
Q_f={q_gen_4549},
Delta=
{
<z, z, z>() -> q_gen_4549
}

Datatype: <nat, nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([a, n2]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> leqnat([z, n2]) -> 0  ;  () -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3  ;  () -> merge([nil, y, y]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1  ;  (length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1  ;  (length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1  ;  (length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1  ;  (leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1  ;  (not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1  ;  (leqnat([s(nn1), z])) -> BOT -> 1  ;  (plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Yes: (() -> merge([cons(z, xs), nil, cons(z, xs)]), {
xs -> nil  ;  z -> b
})

-------------------------------------------
Step 3, which took 0.003602 s (model generation: 0.003568,  model checking: 0.000034):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  merge -> 
{{{
Q={q_gen_4550, q_gen_4552, q_gen_4553, q_gen_4554, q_gen_4555},
Q_f={q_gen_4550},
Delta=
{
<nil, nil>() -> q_gen_4552
<nil, b>() -> q_gen_4553
<b, nil>() -> q_gen_4554
<b, b>() -> q_gen_4555
<cons, nil, cons>(q_gen_4555, q_gen_4554, q_gen_4553, q_gen_4552) -> q_gen_4550
<nil, nil, nil>() -> q_gen_4550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4549},
Q_f={q_gen_4549},
Delta=
{
<z, z, z>() -> q_gen_4549
}

Datatype: <nat, nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([a, n2]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> leqnat([z, n2]) -> 3  ;  () -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3  ;  () -> merge([nil, y, y]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1  ;  (length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1  ;  (length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1  ;  (length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1  ;  (leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1  ;  (not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1  ;  (leqnat([s(nn1), z])) -> BOT -> 1  ;  (plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Yes: (() -> leqnat([z, n2]), {
n2 -> z
})

-------------------------------------------
Step 4, which took 0.003588 s (model generation: 0.003566,  model checking: 0.000022):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4556},
Q_f={q_gen_4556},
Delta=
{
<z, z>() -> q_gen_4556
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  merge -> 
{{{
Q={q_gen_4550, q_gen_4552, q_gen_4553, q_gen_4554, q_gen_4555},
Q_f={q_gen_4550},
Delta=
{
<nil, nil>() -> q_gen_4552
<nil, b>() -> q_gen_4553
<b, nil>() -> q_gen_4554
<b, b>() -> q_gen_4555
<cons, nil, cons>(q_gen_4555, q_gen_4554, q_gen_4553, q_gen_4552) -> q_gen_4550
<nil, nil, nil>() -> q_gen_4550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4549},
Q_f={q_gen_4549},
Delta=
{
<z, z, z>() -> q_gen_4549
}

Datatype: <nat, nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([a, n2]) -> 0  ;  () -> leq([b, b]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  () -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3  ;  () -> merge([nil, y, y]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1  ;  (length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1  ;  (length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1  ;  (length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1  ;  (leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1  ;  (not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1  ;  (leqnat([s(nn1), z])) -> BOT -> 1  ;  (plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Yes: (() -> leq([b, b]), {

})

-------------------------------------------
Step 5, which took 0.004412 s (model generation: 0.004358,  model checking: 0.000054):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_4557},
Q_f={q_gen_4557},
Delta=
{
<b, b>() -> q_gen_4557
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4556},
Q_f={q_gen_4556},
Delta=
{
<z, z>() -> q_gen_4556
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  merge -> 
{{{
Q={q_gen_4550, q_gen_4552, q_gen_4553, q_gen_4554, q_gen_4555},
Q_f={q_gen_4550},
Delta=
{
<nil, nil>() -> q_gen_4552
<nil, b>() -> q_gen_4553
<b, nil>() -> q_gen_4554
<b, b>() -> q_gen_4555
<cons, nil, cons>(q_gen_4555, q_gen_4554, q_gen_4553, q_gen_4552) -> q_gen_4550
<nil, nil, nil>() -> q_gen_4550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4549},
Q_f={q_gen_4549},
Delta=
{
<z, z, z>() -> q_gen_4549
}

Datatype: <nat, nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([a, n2]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  () -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3  ;  () -> merge([nil, y, y]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1  ;  (length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1  ;  (length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1  ;  (length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1  ;  (leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1  ;  (not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1  ;  (leqnat([s(nn1), z])) -> BOT -> 1  ;  (plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Yes: (() -> leq([a, n2]), {
n2 -> b
})

-------------------------------------------
Step 6, which took 0.008111 s (model generation: 0.007982,  model checking: 0.000129):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_4557},
Q_f={q_gen_4557},
Delta=
{
<a, b>() -> q_gen_4557
<b, b>() -> q_gen_4557
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4556},
Q_f={q_gen_4556},
Delta=
{
<z, z>() -> q_gen_4556
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  merge -> 
{{{
Q={q_gen_4550, q_gen_4552, q_gen_4553, q_gen_4554, q_gen_4555},
Q_f={q_gen_4550},
Delta=
{
<nil, nil>() -> q_gen_4552
<nil, b>() -> q_gen_4553
<b, nil>() -> q_gen_4554
<b, b>() -> q_gen_4555
<cons, nil, cons>(q_gen_4555, q_gen_4554, q_gen_4553, q_gen_4552) -> q_gen_4550
<nil, nil, nil>() -> q_gen_4550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4549},
Q_f={q_gen_4549},
Delta=
{
<z, z, z>() -> q_gen_4549
}

Datatype: <nat, nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, n2]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  () -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3  ;  () -> merge([nil, y, y]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1  ;  (length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1  ;  (length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1  ;  (length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1  ;  (leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1  ;  (not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1  ;  (leqnat([s(nn1), z])) -> BOT -> 1  ;  (plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Yes: (() -> length([nil, z]), {

})

-------------------------------------------
Step 7, which took 0.008151 s (model generation: 0.007799,  model checking: 0.000352):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_4559},
Q_f={q_gen_4559},
Delta=
{
<nil, z>() -> q_gen_4559
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_4557},
Q_f={q_gen_4557},
Delta=
{
<a, b>() -> q_gen_4557
<b, b>() -> q_gen_4557
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4556},
Q_f={q_gen_4556},
Delta=
{
<z, z>() -> q_gen_4556
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  merge -> 
{{{
Q={q_gen_4550, q_gen_4552, q_gen_4553, q_gen_4554, q_gen_4555},
Q_f={q_gen_4550},
Delta=
{
<nil, nil>() -> q_gen_4552
<nil, b>() -> q_gen_4553
<b, nil>() -> q_gen_4554
<b, b>() -> q_gen_4555
<cons, nil, cons>(q_gen_4555, q_gen_4554, q_gen_4553, q_gen_4552) -> q_gen_4550
<nil, nil, nil>() -> q_gen_4550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4549},
Q_f={q_gen_4549},
Delta=
{
<z, z, z>() -> q_gen_4549
}

Datatype: <nat, nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, n2]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  () -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3  ;  () -> merge([nil, y, y]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1  ;  (length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1  ;  (length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1  ;  (length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1  ;  (leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1  ;  (not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1  ;  (leqnat([s(nn1), z])) -> BOT -> 1  ;  (plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 8, which took 0.007426 s (model generation: 0.007184,  model checking: 0.000242):

Model:
|_
{
append -> 
{{{
Q={q_gen_4560},
Q_f={q_gen_4560},
Delta=
{
<nil, nil, nil>() -> q_gen_4560
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_4559},
Q_f={q_gen_4559},
Delta=
{
<nil, z>() -> q_gen_4559
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_4557},
Q_f={q_gen_4557},
Delta=
{
<a, b>() -> q_gen_4557
<b, b>() -> q_gen_4557
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4556},
Q_f={q_gen_4556},
Delta=
{
<z, z>() -> q_gen_4556
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  merge -> 
{{{
Q={q_gen_4550, q_gen_4552, q_gen_4553, q_gen_4554, q_gen_4555},
Q_f={q_gen_4550},
Delta=
{
<nil, nil>() -> q_gen_4552
<nil, b>() -> q_gen_4553
<b, nil>() -> q_gen_4554
<b, b>() -> q_gen_4555
<cons, nil, cons>(q_gen_4555, q_gen_4554, q_gen_4553, q_gen_4552) -> q_gen_4550
<nil, nil, nil>() -> q_gen_4550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4549},
Q_f={q_gen_4549},
Delta=
{
<z, z, z>() -> q_gen_4549
}

Datatype: <nat, nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, n2]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  () -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3  ;  () -> merge([nil, y, y]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1  ;  (length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1  ;  (length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1  ;  (length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1  ;  (leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1  ;  (not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1  ;  (leqnat([s(nn1), z])) -> BOT -> 1  ;  (plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Yes: ((plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]), {
_hx -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 9, which took 0.010052 s (model generation: 0.009987,  model checking: 0.000065):

Model:
|_
{
append -> 
{{{
Q={q_gen_4560},
Q_f={q_gen_4560},
Delta=
{
<nil, nil, nil>() -> q_gen_4560
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_4559},
Q_f={q_gen_4559},
Delta=
{
<nil, z>() -> q_gen_4559
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_4557},
Q_f={q_gen_4557},
Delta=
{
<a, b>() -> q_gen_4557
<b, b>() -> q_gen_4557
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4556},
Q_f={q_gen_4556},
Delta=
{
<z, z>() -> q_gen_4556
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  merge -> 
{{{
Q={q_gen_4550, q_gen_4552, q_gen_4553, q_gen_4554, q_gen_4555},
Q_f={q_gen_4550},
Delta=
{
<nil, nil>() -> q_gen_4552
<nil, b>() -> q_gen_4553
<b, nil>() -> q_gen_4554
<b, b>() -> q_gen_4555
<cons, nil, cons>(q_gen_4555, q_gen_4554, q_gen_4553, q_gen_4552) -> q_gen_4550
<nil, nil, nil>() -> q_gen_4550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4549, q_gen_4562},
Q_f={q_gen_4549},
Delta=
{
<z, z>() -> q_gen_4562
<z, s, s>(q_gen_4562) -> q_gen_4549
<z, z, z>() -> q_gen_4549
}

Datatype: <nat, nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, n2]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  () -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3  ;  () -> merge([nil, y, y]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1  ;  (length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1  ;  (length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1  ;  (length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1  ;  (leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1  ;  (not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2  ;  (leqnat([s(nn1), z])) -> BOT -> 2  ;  (plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Yes: ((leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 10, which took 0.015022 s (model generation: 0.010281,  model checking: 0.004741):

Model:
|_
{
append -> 
{{{
Q={q_gen_4560},
Q_f={q_gen_4560},
Delta=
{
<nil, nil, nil>() -> q_gen_4560
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_4559},
Q_f={q_gen_4559},
Delta=
{
<nil, z>() -> q_gen_4559
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_4557},
Q_f={q_gen_4557},
Delta=
{
<a, b>() -> q_gen_4557
<b, b>() -> q_gen_4557
}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4556},
Q_f={q_gen_4556},
Delta=
{
<s, s>(q_gen_4556) -> q_gen_4556
<z, z>() -> q_gen_4556
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  merge -> 
{{{
Q={q_gen_4550, q_gen_4552, q_gen_4553, q_gen_4554, q_gen_4555},
Q_f={q_gen_4550},
Delta=
{
<nil, nil>() -> q_gen_4552
<nil, b>() -> q_gen_4553
<b, nil>() -> q_gen_4554
<b, b>() -> q_gen_4555
<cons, nil, cons>(q_gen_4555, q_gen_4554, q_gen_4553, q_gen_4552) -> q_gen_4550
<nil, nil, nil>() -> q_gen_4550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4549, q_gen_4562},
Q_f={q_gen_4549},
Delta=
{
<z, z>() -> q_gen_4562
<z, s, s>(q_gen_4562) -> q_gen_4549
<z, z, z>() -> q_gen_4549
}

Datatype: <nat, nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, n2]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  () -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3  ;  () -> merge([nil, y, y]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1  ;  (length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1  ;  (length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1  ;  (length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1  ;  (leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1  ;  (not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 4  ;  (leq([b, a])) -> BOT -> 2  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2  ;  (leqnat([s(nn1), z])) -> BOT -> 2  ;  (plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Yes: ((not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]), {
_xw -> cons(b, nil)  ;  xs -> nil  ;  y2 -> a  ;  ys -> nil  ;  z -> b
})

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