Solving ../../benchmarks/false/insert_length_eq.smt2...

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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{() -> leq([a, y])
() -> leq([b, b])
(leq([b, a])) -> BOT}
)
(insert, F:
{() -> insert([x, nil, cons(x, nil)])
(insert([x, z, _via]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _via)])
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))])}
(insert([_wia, _xia, _yia]) /\ insert([_wia, _xia, _zia])) -> eq_eltlist([_yia, _zia])
)
(length, F:
{() -> length([nil, z])
(length([ll, _aja])) -> length([cons(x, ll), s(_aja)])}
(length([_bja, _cja]) /\ length([_bja, _dja])) -> eq_nat([_cja, _dja])
)
(leqnat, P:
{() -> leqnat([z, s(nn2)])
() -> leqnat([z, z])
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)])
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2])
(leqnat([s(nn1), z])) -> BOT}
)
}

properties:
{(insert([x, l, _fja]) /\ length([_fja, _gja]) /\ length([l, _eja])) -> eq_nat([_eja, _gja])}


over-approximation: {insert, length, leqnat}
under-approximation: {leq, leqnat}

Clause system for inference is:

{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> leqnat([z, s(nn2)]) -> 0
() -> leqnat([z, z]) -> 0
(insert([x, l, _fja]) /\ length([_fja, _gja]) /\ length([l, _eja])) -> eq_nat([_eja, _gja]) -> 0
(insert([x, z, _via]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _via)]) -> 0
(length([ll, _aja])) -> length([cons(x, ll), s(_aja)]) -> 0
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 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
}


Solving took 0.132664 seconds.
Disproved
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.012576 s (model generation: 0.009773,  model checking: 0.002803):

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

}

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> leqnat([z, s(nn2)]) -> 0
() -> leqnat([z, z]) -> 3
(insert([x, l, _fja]) /\ length([_fja, _gja]) /\ length([l, _eja])) -> eq_nat([_eja, _gja]) -> 1
(insert([x, z, _via]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _via)]) -> 1
(length([ll, _aja])) -> length([cons(x, ll), s(_aja)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 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
}
Sat witness: Found: (() -> leqnat([z, z]), {

})

-------------------------------------------
Step 1, which took 0.010167 s (model generation: 0.010040,  model checking: 0.000127):

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

}

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> leqnat([z, s(nn2)]) -> 3
() -> leqnat([z, z]) -> 3
(insert([x, l, _fja]) /\ length([_fja, _gja]) /\ length([l, _eja])) -> eq_nat([_eja, _gja]) -> 1
(insert([x, z, _via]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _via)]) -> 1
(length([ll, _aja])) -> length([cons(x, ll), s(_aja)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 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
}
Sat witness: Found: (() -> leqnat([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.010416 s (model generation: 0.010350,  model checking: 0.000066):

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

}

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 3
() -> leqnat([z, s(nn2)]) -> 3
() -> leqnat([z, z]) -> 3
(insert([x, l, _fja]) /\ length([_fja, _gja]) /\ length([l, _eja])) -> eq_nat([_eja, _gja]) -> 1
(insert([x, z, _via]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _via)]) -> 1
(length([ll, _aja])) -> length([cons(x, ll), s(_aja)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 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
}
Sat witness: Found: (() -> leq([b, b]), {

})

-------------------------------------------
Step 3, which took 0.010535 s (model generation: 0.010457,  model checking: 0.000078):

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

}

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

}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, s(nn2)]) -> 3
() -> leqnat([z, z]) -> 3
(insert([x, l, _fja]) /\ length([_fja, _gja]) /\ length([l, _eja])) -> eq_nat([_eja, _gja]) -> 1
(insert([x, z, _via]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _via)]) -> 1
(length([ll, _aja])) -> length([cons(x, ll), s(_aja)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 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
}
Sat witness: Found: (() -> leq([a, y]), {
y -> b
})

-------------------------------------------
Step 4, which took 0.010666 s (model generation: 0.010552,  model checking: 0.000114):

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

}

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

}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, s(nn2)]) -> 3
() -> leqnat([z, z]) -> 3
(insert([x, l, _fja]) /\ length([_fja, _gja]) /\ length([l, _eja])) -> eq_nat([_eja, _gja]) -> 1
(insert([x, z, _via]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _via)]) -> 1
(length([ll, _aja])) -> length([cons(x, ll), s(_aja)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 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
}
Sat witness: Found: (() -> length([nil, z]), {

})

-------------------------------------------
Step 5, which took 0.011004 s (model generation: 0.010760,  model checking: 0.000244):

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

}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, s(nn2)]) -> 3
() -> leqnat([z, z]) -> 3
(insert([x, l, _fja]) /\ length([_fja, _gja]) /\ length([l, _eja])) -> eq_nat([_eja, _gja]) -> 1
(insert([x, z, _via]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _via)]) -> 1
(length([ll, _aja])) -> length([cons(x, ll), s(_aja)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 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
}
Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 6, which took 0.015332 s (model generation: 0.015083,  model checking: 0.000249):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6605, q_gen_6606, q_gen_6607},
Q_f={q_gen_6605},
Delta=
{
<nil>() -> q_gen_6606
<b>() -> q_gen_6607
<b, nil, cons>(q_gen_6607, q_gen_6606) -> q_gen_6605
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, s(nn2)]) -> 3
() -> leqnat([z, z]) -> 3
(insert([x, l, _fja]) /\ length([_fja, _gja]) /\ length([l, _eja])) -> eq_nat([_eja, _gja]) -> 1
(insert([x, z, _via]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _via)]) -> 1
(length([ll, _aja])) -> length([cons(x, ll), s(_aja)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 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
}
Sat witness: Found: ((leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 7, which took 0.011887 s (model generation: 0.011293,  model checking: 0.000594):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6605, q_gen_6606, q_gen_6607},
Q_f={q_gen_6605},
Delta=
{
<nil>() -> q_gen_6606
<b>() -> q_gen_6607
<b, nil, cons>(q_gen_6607, q_gen_6606) -> q_gen_6605
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, s(nn2)]) -> 3
() -> leqnat([z, z]) -> 3
(insert([x, l, _fja]) /\ length([_fja, _gja]) /\ length([l, _eja])) -> eq_nat([_eja, _gja]) -> 1
(insert([x, z, _via]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _via)]) -> 1
(length([ll, _aja])) -> length([cons(x, ll), s(_aja)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 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
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 8, which took 0.011844 s (model generation: 0.011608,  model checking: 0.000236):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6605, q_gen_6606, q_gen_6607, q_gen_6610, q_gen_6611},
Q_f={q_gen_6605},
Delta=
{
<nil>() -> q_gen_6606
<b>() -> q_gen_6607
<nil, cons>(q_gen_6607, q_gen_6606) -> q_gen_6610
<b, b>() -> q_gen_6611
<b, cons, cons>(q_gen_6611, q_gen_6610) -> q_gen_6605
<b, nil, cons>(q_gen_6607, q_gen_6606) -> q_gen_6605
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, s(nn2)]) -> 3
() -> leqnat([z, z]) -> 3
(insert([x, l, _fja]) /\ length([_fja, _gja]) /\ length([l, _eja])) -> eq_nat([_eja, _gja]) -> 1
(insert([x, z, _via]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _via)]) -> 1
(length([ll, _aja])) -> length([cons(x, ll), s(_aja)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 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
}
Sat witness: Found: ((length([ll, _aja])) -> length([cons(x, ll), s(_aja)]), {
_aja -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 9, which took 0.015416 s (model generation: 0.012381,  model checking: 0.003035):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6605, q_gen_6606, q_gen_6607, q_gen_6610, q_gen_6611},
Q_f={q_gen_6605},
Delta=
{
<nil>() -> q_gen_6606
<b>() -> q_gen_6607
<nil, cons>(q_gen_6607, q_gen_6606) -> q_gen_6610
<b, b>() -> q_gen_6611
<b, cons, cons>(q_gen_6611, q_gen_6610) -> q_gen_6605
<b, nil, cons>(q_gen_6607, q_gen_6606) -> q_gen_6605
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6604, q_gen_6613},
Q_f={q_gen_6604},
Delta=
{
<b>() -> q_gen_6613
<cons, s>(q_gen_6613, q_gen_6604) -> q_gen_6604
<nil, z>() -> q_gen_6604
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, s(nn2)]) -> 3
() -> leqnat([z, z]) -> 3
(insert([x, l, _fja]) /\ length([_fja, _gja]) /\ length([l, _eja])) -> eq_nat([_eja, _gja]) -> 1
(insert([x, z, _via]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _via)]) -> 4
(length([ll, _aja])) -> length([cons(x, ll), s(_aja)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 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
}
Sat witness: Found: ((insert([x, z, _via]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _via)]), {
_via -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 10, which took 0.006504 s (model generation: 0.006147,  model checking: 0.000357):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6605, q_gen_6606, q_gen_6607, q_gen_6610, q_gen_6611},
Q_f={q_gen_6605},
Delta=
{
<nil>() -> q_gen_6606
<b>() -> q_gen_6607
<nil, cons>(q_gen_6607, q_gen_6606) -> q_gen_6610
<a, a>() -> q_gen_6611
<b, b>() -> q_gen_6611
<b, cons, cons>(q_gen_6611, q_gen_6610) -> q_gen_6605
<b, nil, cons>(q_gen_6607, q_gen_6606) -> q_gen_6605
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6604, q_gen_6613},
Q_f={q_gen_6604},
Delta=
{
<b>() -> q_gen_6613
<cons, s>(q_gen_6613, q_gen_6604) -> q_gen_6604
<nil, z>() -> q_gen_6604
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, s(nn2)]) -> 3
() -> leqnat([z, z]) -> 3
(insert([x, l, _fja]) /\ length([_fja, _gja]) /\ length([l, _eja])) -> eq_nat([_eja, _gja]) -> 4
(insert([x, z, _via]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _via)]) -> 4
(length([ll, _aja])) -> length([cons(x, ll), s(_aja)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 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
}
Sat witness: Found: ((insert([x, l, _fja]) /\ length([_fja, _gja]) /\ length([l, _eja])) -> eq_nat([_eja, _gja]), {
_eja -> z  ;  _fja -> cons(b, nil)  ;  _gja -> s(z)  ;  l -> nil  ;  x -> b
})

Total time: 0.132664
Reason for stopping: Disproved